1: # 21 "./lpsrc/flx_beta.ipk"
2: open Flx_util
3: open Flx_ast
4: open Flx_types
5: open Flx_mtypes1
6: open Flx_mtypes2
7:
8: open Flx_print
9: open Flx_exceptions
10: open Flx_typing
11: open List
12: open Flx_srcref
13: open Flx_unify
14: open Flx_maps
15:
16: exception BTfound of btypecode_t
17:
18: (* params is list of string * bound_typecode *)
19: let rec metatype syms (params:(int * btypecode_t) list) term =
20: (*
21: print_endline ("Find Metatype of: " ^ string_of_btypecode syms.dfns term);
22: *)
23: let t = metatype' syms params term in
24: (*
25: print_endline "Done";
26: *)
27: t
28:
29: and metatype' syms (params:(int * btypecode_t) list) term =
30: let st t = string_of_btypecode syms.dfns t in
31: let mt t = metatype' syms params t in
32: match term with
33: | `BTYP_typefun (a,b,c) ->
34: let ps = List.map snd a in
35: let argt =
36: match ps with
37: | [x] -> x
38: | _ -> `BTYP_tuple ps
39: in
40: let rt = metatype syms (a @ params) c in
41: if b<>rt
42: then
43: failwith
44: (
45: "In abstraction\n" ^
46: st term ^
47: "\nFunction body metatype \n"^
48: st rt^
49: "\ndoesn't agree with declared type \n" ^
50: st b
51: )
52: else `BTYP_function (argt,b)
53:
54: | `BTYP_type_tuple ts ->
55: `BTYP_tuple (List.map (metatype syms params) ts)
56:
57: | `BTYP_apply (a,b) ->
58: begin
59: let ta = mt a
60: and tb = mt b
61: in match ta with
62: | `BTYP_function (x,y) ->
63: if x = tb then y
64: else
65: failwith "Metatype error: function argument wrong metatype"
66: | _ -> failwith "Metatype error: function required for LHS of application"
67: end
68: | `BTYP_var (i,mt) -> mt
69: (*
70: begin try
71: List.assoc i params
72: with
73: Not_found ->
74: print_endline "assoc list = ";
75: List.iter
76: (fun (i,s) ->
77: print_string
78: (
79: string_of_int i ^
80: ": " ^
81: string_of_btypecode syms.dfns s ^
82: " "
83: )
84: )
85: params
86: ;
87: print_endline "";
88: failwith
89: (
90: "[metatype] Type variable " ^ string_of_int i ^ " not found in generic assoc list"
91: )
92: end
93: *)
94:
95: | _ -> `BTYP_type (* THIS ISN'T RIGHT *)
96:
97:
98:
99: (* fixpoint reduction: reduce
100: Fix f. Lam x. e ==> Lam x. Fix z. e [f x -> z]
101: to replace a recursive function
102: with a recursive data structure
103: *)
104:
105: and fixup syms ps body =
106: let param = match ps with
107: | [] -> assert false
108: | [i,mt] -> `BTYP_var (i,mt)
109: | x -> `BTYP_type_tuple (List.map (fun (i,mt) -> `BTYP_var (i,mt)) x)
110: in
111: (*
112: print_endline ("Body = " ^ sbt syms.dfns body);
113: print_endline ("Param = " ^ sbt syms.dfns param);
114: *)
115: let rec aux term depth =
116: let fx t = aux t (depth+1) in
117: match map_btype fx term with
118: | `BTYP_apply (`BTYP_fix i, arg)
119: when arg = param
120: && i + depth +1 = 0 (* looking inside application, one more level *)
121: -> `BTYP_fix (i+2) (* elide application AND skip under lambda abstraction *)
122:
123: | `BTYP_typefun (a,b,c) ->
124: (* NOTE we have to add 2 to depth here, an extra
125: level for the lambda binder.
126: NOTE also: this is NOT a recusive call to fixup!
127: It doesn't fixup this function.
128: *)
129:
130: `BTYP_typefun (a, fx b, aux c (depth + 2))
131: | x -> x
132: in
133: (* note depth 1: we seek a fix to an abstraction
134: of which we're given only the body, that's an
135: extra level in the term structure
136: *)
137: aux body 1
138:
139: and mk_prim_type_inst syms i args =
140: print_endline "MK_PRIM_TYPE";
141: let t = `BTYP_inst (i,args) in
142: (*
143: let _,t' = normalise_type t in
144: let args = match t' with
145: | `BTYP_inst (_,args) -> args
146: | _ -> assert false
147: in
148: if not (Hashtbl.mem syms.prim_inst (i,args))
149: then begin
150: let n = !(syms.counter) in
151: incr (syms.counter);
152: Hashtbl.add syms.prim_inst (i, args) n;
153: Hashtbl.add syms.rev_prim_inst n (i, args)
154: end;
155: *)
156: t
157:
158:
159: and beta_reduce syms (btvars:(int * btypecode_t) list) t =
160: (*
161: print_endline ("Beta reduce " ^ sbt syms.dfns t);
162: *)
163: let t =
164: try
165: beta_reduce' syms btvars [] t
166: with Failure s -> failwith ("beta-reduce failed in " ^ sbt syms.dfns t ^ "msg: " ^ s)
167: in
168: (*
169: print_endline (" reduced= " ^ sbt syms.dfns t);
170: *)
171: t
172:
173: and beta_reduce' syms (btvars:(int * btypecode_t) list) termlist t =
174: (*
175: print_endline ("BETA REDUCE " ^ string_of_btypecode syms.dfns t);
176: *)
177: match list_index termlist t with
178: | Some i -> print_endline ("Beta find fixpoint " ^ si (-i-1)); `BTYP_fix (-i - 1)
179: | None ->
180: let br t' = beta_reduce' syms btvars (t::termlist) t' in
181: let st t = string_of_btypecode syms.dfns t in
182: let mt t = metatype syms btvars t in
183: (* hhmm .. this has to handle a free fixpoint, because it
184: is called during construction of a recursive type .. so
185: we can't do an unfold.. but them beta-reduce won't
186: find fix points .. hmm .. hmm .. we could fix that by
187: replacing a fixpoint with a copy of the recursed expression ..
188: then let beta-reduce find it..
189: *)
190: match t with
191: | `BTYP_inst (i,ts) ->
192: let ts = map br ts in
193: begin try match Hashtbl.find syms.dfns i with
194: | {id=id; symdef=`SYMDEF_type_alias _ } ->
195: failwith ("Beta reduce found a type instance of "^id^" to be an alias, which it can't handle")
196: | _ -> `BTYP_inst (i,ts)
197: with Not_found -> `BTYP_inst (i,ts) (* could be reparented class *)
198: end
199: | `BTYP_tuple ls -> `BTYP_tuple (map br ls)
200: | `BTYP_array (i,t) -> `BTYP_array (i, br t)
201: | `BTYP_sum ls -> `BTYP_sum (map br ls)
202: | `BTYP_record ts ->
203: let ss,ls = split ts in
204: `BTYP_record (combine ss (map br ls))
205:
206: | `BTYP_variant ts ->
207: let ss,ls = split ts in
208: `BTYP_variant (combine ss (map br ls))
209:
210: (* Intersection type reduction rule: if any term is 0,
211: the result is 0, otherwise the result is the intersection
212: of the reduced terms with 1 terms removed: if there
213: are no terms return 1, if a single term return it,
214: otherwise return the intersection of non units
215: (at least two)
216: *)
217: | `BTYP_intersect ls ->
218: let ls = map br ls in
219: if mem `BTYP_void ls then `BTYP_void
220: else let ls = filter (fun i -> i <> `BTYP_tuple []) ls in
221: begin match ls with
222: | [] -> `BTYP_tuple []
223: | [t] -> t
224: | ls -> `BTYP_intersect ls
225: end
226:
227: | `BTYP_typeset ls -> `BTYP_typeset (map br ls)
228:
229: | `BTYP_typesetunion ls ->
230: let ls = rev_map br ls in
231: (* split into explicit typesets and other terms
232: at the moment, there shouldn't be any 'other'
233: terms (since there are no typeset variables ..
234: *)
235: let rec aux ts ot ls = match ls with
236: | [] ->
237: begin match ot with
238: | [] -> `BTYP_typeset ts
239: | _ ->
240: print_endline "WARNING UNREDUCED TYPESET UNION";
241: `BTYP_typesetunion (`BTYP_typeset ts :: ot)
242: end
243:
244: | `BTYP_typeset xs :: t -> aux (xs @ ts) ot t
245: | h :: t -> aux ts (h :: ot) t
246: in aux [] [] ls
247:
248: (* NOTE: sets have no unique unit *)
249: (* WARNING: this representation is dangerous:
250: we can only calculate the real intersection
251: of discrete types *without type variables*
252:
253: If there are pattern variables, we may be able
254: to apply unification as a reduction. However
255: we have to be very careful doing that: we can't
256: unify variables bound by universal or lambda quantifiers
257: or the environment: technically I think we can only
258: unify existentials. For example the intersection
259:
260: 'a * int & long & 'b
261:
262: may seem to be long * int, but only if 'a and 'b are
263: pattern variables, i.e. dependent variables we're allowed
264: to assign. If they're actually function parameters, or
265: just names for types in the environment, we have to stop
266: the unification algorithm from assigning them (since they're
267: actually particular constants at that point).
268:
269: but the beta-reduction can be applied anywhere .. so I'm
270: not at all confident of the right reduction rule yet.
271:
272: Bottom line: the rule below is a hack.
273: *)
274: | `BTYP_typesetintersection ls ->
275: let ls = map br ls in
276: if mem (`BTYP_typeset []) ls then `BTYP_typeset []
277: else begin match ls with
278: | [t] -> t
279: | ls -> `BTYP_typesetintersection ls
280: end
281:
282:
283: | `BTYP_type_tuple ls -> `BTYP_type_tuple (map br ls)
284: | `BTYP_function (a,b) -> `BTYP_function (br a, br b)
285: | `BTYP_cfunction (a,b) -> `BTYP_cfunction (br a, br b)
286: | `BTYP_pointer a -> `BTYP_pointer (br a)
287: | `BTYP_lvalue a -> `BTYP_lvalue (br a)
288:
289: | `BTYP_void -> t
290: | `BTYP_type -> t
291: | `BTYP_fix _ -> t
292: | `BTYP_var _ -> t
293: | `BTYP_unitsum _ -> t
294:
295: | `BTYP_apply (t1,t2) ->
296: (*
297: print_endline "-----------------------";
298: print_endline ("Application " ^ st t);
299: print_endline "";
300: print_endline ("Unreduced function is " ^ st t1);
301: print_endline ("Unreduced Argument is " ^ st t2);
302: *)
303: let t2 = br t2 in (* eager evaluation *)
304: let t1 = br t1 in (* eager evaluation *)
305: (*
306: print_endline ("reduced function is " ^ st t1);
307: print_endline ("reduced Argument is " ^ st t2);
308: *)
309: let mt1 = mt t1
310: and mt2 = mt t2
311: in
312: (*
313: print_endline ("Function metatype is" ^ st mt1);
314: print_endline ("Argument metatype is" ^ st mt2);
315: *)
316: begin match t1 with
317: | `BTYP_fix _ -> `BTYP_apply(t1,t2)
318: | _ ->
319: begin match mt1 with
320: | `BTYP_function (a,b) ->
321: if a <> mt2
322: then failwith ("Argument metatype not same as function parameter")
323: | _ ->
324: failwith (
325: "[beta_reduce] Expected LHS of application to be type function, got\n" ^
326: st t1^"\nmeta type: " ^ st mt1
327: )
328: end
329: ;
330: begin match t1 with
331: | `BTYP_typefun (ps,r,body) ->
332: let v = Hashtbl.create 97 in
333: begin match ps with
334: | [] -> ()
335: | [i,_] -> Hashtbl.add v i t2
336: | _ ->
337: let ts = match t2 with
338: | `BTYP_type_tuple ts -> ts
339: | _ -> assert false
340: in
341: if List.length ps <> List.length ts
342: then failwith "Wrong number of arguments to typefun"
343: else List.iter2 (fun (i,_) y -> Hashtbl.add v i y) ps ts
344: end
345: ;
346: (*
347: print_endline "Variable assignments are ";
348: Hashtbl.iter
349: (fun i t -> print_endline (string_of_int i ^ " -> " ^ st t))
350: v
351: ;
352: print_endline ("Body is " ^ st body);
353: *)
354: let t = varmap_subst v body in
355: (*
356: print_endline ("Result of application = " ^ st t);
357: *)
358: br t
359:
360: | `BTYP_var _ -> t (* can't reduce it yet *)
361: | `BTYP_fix _ -> t (* can't reduce it yet *)
362:
363: | _ -> failwith
364: (
365: "[beta-reduce] Expected type function or variable, got " ^
366: string_of_btypecode syms.dfns t1
367: )
368: end
369: end
370:
371: | `BTYP_typefun (p,r,b) ->
372: let p' = List.map (fun (i,t) -> (i, br t)) p in
373: (*
374: print_endline ("fixing up function " ^ st t);
375: *)
376: (*
377: print_endline ("body is " ^ st b);
378: *)
379: let b = fixup syms p b in
380: (*
381: print_endline ("After fixup body is " ^ st b);
382: *)
383: let b' = beta_reduce syms (p' @ btvars) b in
384: (*
385: print_endline ("Reducing body inside lambda, result is" ^ sbt syms.dfns b');
386: *)
387: `BTYP_typefun (p', br r, b')
388:
389: | `BTYP_type_match (tt,pts) ->
390: (*
391: print_endline ("Typematch [before reduction] " ^ sbt syms.dfns t);
392: *)
393: let tt = br tt in
394: let pts =
395: map (fun (tp,t) ->
396: {
397: tp with pattern=br tp.pattern;
398: assignments= map (fun (j,t) -> j, br t) tp.assignments
399: }, br t
400: )
401: pts
402: in
403: (*
404: let xx = `BTYP_type_match (tt,pts) in
405: print_endline ("Typematch [after reduction] " ^ sbt syms.dfns xx);
406: *)
407: let new_matches = ref [] in
408: iter (fun (({pattern=p'; pattern_vars=dvars; assignments=eqns}, t') as x) ->
409: (*
410: print_endline ("Tring to unify argument with " ^ sbt syms.dfns p');
411: *)
412: match maybe_unification syms.dfns [p',tt] with
413: | Some _ -> new_matches := x :: !new_matches
414: | None ->
415: (*
416: print_endline ("Discarding pattern " ^ sbt syms.dfns p');
417: *)
418: ()
419: )
420: pts
421: ;
422: let pts = rev !new_matches in
423: match pts with
424: | [] ->
425: failwith "[beta-reduce] typematch failure"
426: | ({pattern=p';pattern_vars=dvars;assignments=eqns},t') :: _ ->
427: try
428: let mgu = unification false syms.dfns [p', tt] dvars in
429: let t' = list_subst eqns t' in
430: list_subst mgu t'
431: with Not_found -> `BTYP_type_match (tt,pts)
432:
1: # 17 "./lpsrc/flx_tpat.ipk"
2: open Flx_ast
3: open List
4: open Flx_mtypes2
5:
6: let type_of_tpattern syms p :
7: typecode_t *
8: (int * string) list * (* variables for '?' terms *)
9: int list * (* variables for 'any' terms *)
10: (int * string) list * (* variables for 'as' terms *)
11: (int * typecode_t) list (* assignments for as terms *)
12: =
13: let sr = "unk",0,0,0,0 in
14: let explicit_vars = ref [] in
15: let any_vars = ref [] in
16: let as_vars = ref [] in
17: let eqns = ref [] in
18: let rec tp p =
19: match p with
20: | `TPAT_function (a,b) -> `TYP_function (tp a, tp b)
21: | `TPAT_tuple ps -> `TYP_tuple (map tp ps)
22: | `TPAT_sum ps -> `TYP_sum (map tp ps)
23: | `TPAT_pointer p -> `TYP_pointer (tp p)
24: | `TPAT_name (n,ps) -> `AST_name (sr,n,map tp ps)
25: | `TPAT_void -> `AST_void sr
26:
27: | `TPAT_var n ->
28: let j = !(syms.counter) in
29: incr (syms.counter);
30: explicit_vars := (j,n) :: !explicit_vars;
31: `TYP_var j
32:
33: | `TPAT_any ->
34: let j = !(syms.counter) in
35: incr (syms.counter);
36: any_vars := j :: !any_vars;
37: `TYP_var j
38:
39: | `TPAT_as (t,n) ->
40: let t = tp t in
41: let j = !(syms.counter) in
42: incr (syms.counter);
43: as_vars := (j,n) :: !as_vars;
44: eqns := (j,t) :: !eqns;
45: t
46:
47: | `TPAT_unitsum j -> `TYP_unitsum j
48: | `TPAT_type_tuple ts -> `TYP_type_tuple (map tp ts)
49: in
50: let t = tp p in
51: t,!explicit_vars, !any_vars, !as_vars, !eqns
52:
53: