1: # 22 "./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: let rec metatype syms sr term =
19: (*
20: print_endline ("Find Metatype of: " ^ string_of_btypecode syms.dfns term);
21: *)
22: let t = metatype' syms sr term in
23: (*
24: print_endline ("Metatype of: " ^ string_of_btypecode syms.dfns term ^ " is " ^ sbt syms.dfns t);
25: print_endline "Done";
26: *)
27: t
28:
29: and metatype' syms sr term =
30: let st t = string_of_btypecode syms.dfns t in
31: let mt t = metatype' syms sr t in
32: match term with
33: | `BTYP_lift t -> t
34: | `BTYP_case _ -> `BTYP_function (`BTYP_type 0, `BTYP_type 0)
35:
36: | `BTYP_typefun (a,b,c) ->
37: let ps = List.map snd a in
38: let argt =
39: match ps with
40: | [x] -> x
41: | _ -> `BTYP_tuple ps
42: in
43: let rt = metatype syms sr c in
44: if b<>rt
45: then
46: clierr sr
47: (
48: "In abstraction\n" ^
49: st term ^
50: "\nFunction body metatype \n"^
51: st rt^
52: "\ndoesn't agree with declared type \n" ^
53: st b
54: )
55: else `BTYP_function (argt,b)
56:
57: | `BTYP_type_tuple ts ->
58: `BTYP_tuple (map mt ts)
59:
60: | `BTYP_apply (a,b) ->
61: begin
62: let ta = mt a
63: and tb = mt b
64: in match ta with
65: | `BTYP_function (x,y) ->
66: if x = tb then y
67: else
68: clierr sr (
69: "Metatype error: function argument wrong metatype, expected:\n" ^
70: sbt syms.dfns x ^
71: "\nbut got:\n" ^
72: sbt syms.dfns tb
73: )
74:
75: | _ -> clierr sr
76: (
77: "Metatype error: function required for LHS of application:\n"^
78: sbt syms.dfns term ^
79: ", got metatype:\n" ^
80: sbt syms.dfns ta
81: )
82: end
83: | `BTYP_var (i,mt) ->
84: (*
85: print_endline ("Type variable " ^ si i^ " has encoded meta type " ^ sbt syms.dfns mt);
86: (
87: try
88: let symdef = Hashtbl.find syms.dfns i in begin match symdef with
89: | {symdef=`SYMDEF_typevar mt} -> print_endline ("Table shows metatype is " ^ string_of_typecode mt);
90: | _ -> print_endline "Type variable isn't a type variable?"
91: end
92: with Not_found -> print_endline "Cannot find type variable in symbol table"
93: );
94: *)
95: mt
96:
97: | `BTYP_type i -> `BTYP_type (i+1)
98: | `BTYP_inst (index,ts) ->
99: let {id=id; symdef=entry} =
100: try Hashtbl.find syms.dfns index
101: with Not_found -> failwith ("[metatype'] can't find type instance index " ^ si index)
102: in
103: (*
104: print_endline ("Yup .. instance id=" ^ id);
105: *)
106:
107: (* this is hacked: we should really bind the types and take
108: the metatype of them but we don't have access to the
109: bind type routine due to module factoring .. we could pass
110: in the bind-type routine as an argument .. yuck ..
111: *)
112: begin match entry with
113: | `SYMDEF_nonconst_ctor (_,ut,_,_,argt) ->
114: `BTYP_function (`BTYP_type 0,`BTYP_type 0)
115:
116: | `SYMDEF_const_ctor (_,t,_,_) ->
117: `BTYP_type 0
118:
119: | `SYMDEF_abs _ -> `BTYP_type 0
120:
121: | _ -> clierr sr ("Unexpected argument to metatype: " ^ sbt syms.dfns term)
122: end
123:
124:
125: | _ ->
126: print_endline ("Questionable meta typing of term: " ^ sbt syms.dfns term);
127: `BTYP_type 0 (* THIS ISN'T RIGHT *)
128:
129:
130:
131: (* fixpoint reduction: reduce
132: Fix f. Lam x. e ==> Lam x. Fix z. e [f x -> z]
133: to replace a recursive function
134: with a recursive data structure.
135:
136: Example: consider:
137:
138: list t = t * list t
139:
140: which is
141:
142: list = fix f. lam t. t * f t
143:
144: We can apply list to int:
145:
146: list int = (fix f. lam t. t * f t) int
147:
148: unfolding:
149:
150: list int = (lam t. t * (fix f. lam t. t * f t)) int
151: = int * (fix f. lam t. t * f t) int
152: = int * list int
153:
154: which is just
155:
156: list int = fix z. int * z
157:
158: The rule ONLY works when a recursive function f
159: is applied in its own definition to its own parameter.
160:
161: The rule traps in infinite expansion of a data type,
162: and creates instead an recursive data type, eliminating
163: the function.
164:
165: The normal beta reduction rule is
166:
167: (lam t. b) a => b [t->a]
168:
169: For a recursive function:
170:
171: (fix f. lam t. b) a => b[f-> fix f. lam t. b; t-> a]
172:
173: and the result must be reduced again.
174:
175: *)
176:
177: and fixup syms ps body =
178: let param = match ps with
179: | [] -> assert false
180: | [i,mt] -> `BTYP_var (i,mt)
181: | x -> `BTYP_type_tuple (List.map (fun (i,mt) -> `BTYP_var (i,mt)) x)
182: in
183: (*
184: print_endline ("Body = " ^ sbt syms.dfns body);
185: print_endline ("Param = " ^ sbt syms.dfns param);
186: *)
187: let rec aux term depth =
188: let fx t = aux t (depth+1) in
189: match map_btype fx term with
190: | `BTYP_apply (`BTYP_fix i, arg)
191: when arg = param
192: && i + depth +1 = 0 (* looking inside application, one more level *)
193: -> print_endline "SPECIAL REDUCTION";
194: `BTYP_fix (i+2) (* elide application AND skip under lambda abstraction *)
195:
196: | `BTYP_typefun (a,b,c) ->
197: (* NOTE we have to add 2 to depth here, an extra
198: level for the lambda binder.
199: NOTE also: this is NOT a recusive call to fixup!
200: It doesn't fixup this function.
201: *)
202:
203: `BTYP_typefun (a, fx b, aux c (depth + 2))
204: | x -> x
205: in
206: (* note depth 1: we seek a fix to an abstraction
207: of which we're given only the body, that's an
208: extra level in the term structure
209: *)
210: aux body 1
211:
212: (* generic fixpoint adjuster: add amt to the fixpoint
213: to make it span less deep term, to compensate
214: for removing the top combinator of the term as a result
215: of a one level adjustment eg: reduce a type match
216: *)
217:
218: and adjust t =
219: let rec adj depth t =
220: let fx t = adj (depth + 1) t in
221: match map_btype fx t with
222: | `BTYP_fix i when i + depth < 0 -> `BTYP_fix (i+1)
223: | x -> x
224: in adj 0 t
225:
226: and mk_prim_type_inst syms i args =
227: print_endline "MK_PRIM_TYPE";
228: let t = `BTYP_inst (i,args) in
229: (*
230: let _,t' = normalise_type t in
231: let args = match t' with
232: | `BTYP_inst (_,args) -> args
233: | _ -> assert false
234: in
235: if not (Hashtbl.mem syms.prim_inst (i,args))
236: then begin
237: let n = !(syms.counter) in
238: incr (syms.counter);
239: Hashtbl.add syms.prim_inst (i, args) n;
240: Hashtbl.add syms.rev_prim_inst n (i, args)
241: end;
242: *)
243: t
244:
245:
246: and beta_reduce syms sr t1 =
247: (*
248: print_endline ("---------- Beta reduce " ^ sbt syms.dfns t1);
249: *)
250: let t2 =
251: try
252: beta_reduce' syms sr [] t1
253: with Failure s -> failwith ("beta-reduce failed in " ^ sbt syms.dfns t1 ^ "msg: " ^ s)
254: in
255: (*
256: print_endline ("============ reduced= " ^ sbt syms.dfns t2);
257: if t1 <> t2 then print_endline "!!!!!!!!!!!! CHANGED";
258: *)
259: t2
260:
261: and beta_reduce' syms sr termlist t =
262: (*
263: print_endline (spc ^ "BETA REDUCE " ^ string_of_btypecode syms.dfns t);
264: *)
265: match list_index termlist t with
266: | Some j ->
267: (*
268: print_endline "+++Trail:";
269: let i = ref 0 in
270: iter (fun t -> print_endline (
271: " " ^ si (!i) ^ " ---> " ^sbt syms.dfns t)
272: ; decr i
273: )
274: (t::termlist)
275: ;
276: print_endline "++++End";
277: print_endline ("Beta find fixpoint " ^ si (-j-1));
278: print_endline ("Repeated term " ^ sbt syms.dfns t);
279: *)
280: `BTYP_fix (-j - 1)
281:
282: | None ->
283:
284: let br t' = beta_reduce' syms sr (t::termlist) t' in
285: let st t = string_of_btypecode syms.dfns t in
286: let mt t = metatype syms sr t in
287: match t with
288: | `BTYP_lift t -> `BTYP_lift (br t)
289: | `BTYP_fix _ -> t
290: | `BTYP_var (i,_) -> t
291:
292: | `BTYP_typefun (p,r,b) ->
293: let b = fixup syms p b in
294: let b' = beta_reduce' syms sr (t::termlist) b in
295: let t = `BTYP_typefun (p, br r, b') in
296: t
297:
298: | `BTYP_inst (i,ts) ->
299: let ts = map br ts in
300: begin try match Hashtbl.find syms.dfns i with
301: | {id=id; symdef=`SYMDEF_type_alias _ } ->
302: failwith ("Beta reduce found a type instance of "^id^" to be an alias, which it can't handle")
303: | _ -> `BTYP_inst (i,ts)
304: with Not_found -> `BTYP_inst (i,ts) (* could be reparented class *)
305: end
306:
307: | `BTYP_case (a,b,c) -> `BTYP_case (br a, b, br c)
308: | `BTYP_tuple ls -> `BTYP_tuple (map br ls)
309: | `BTYP_array (i,t) -> `BTYP_array (i, br t)
310: | `BTYP_sum ls -> `BTYP_sum (map br ls)
311: | `BTYP_record ts ->
312: let ss,ls = split ts in
313: `BTYP_record (combine ss (map br ls))
314:
315: | `BTYP_variant ts ->
316: let ss,ls = split ts in
317: `BTYP_variant (combine ss (map br ls))
318:
319: (* Intersection type reduction rule: if any term is 0,
320: the result is 0, otherwise the result is the intersection
321: of the reduced terms with 1 terms removed: if there
322: are no terms return 1, if a single term return it,
323: otherwise return the intersection of non units
324: (at least two)
325: *)
326: | `BTYP_intersect ls ->
327: let ls = map br ls in
328: if mem `BTYP_void ls then `BTYP_void
329: else let ls = filter (fun i -> i <> `BTYP_tuple []) ls in
330: begin match ls with
331: | [] -> `BTYP_tuple []
332: | [t] -> t
333: | ls -> `BTYP_intersect ls
334: end
335:
336: | `BTYP_typeset ls -> `BTYP_typeset (map br ls)
337:
338: | `BTYP_typesetunion ls ->
339: let ls = rev_map br ls in
340: (* split into explicit typesets and other terms
341: at the moment, there shouldn't be any 'other'
342: terms (since there are no typeset variables ..
343: *)
344: let rec aux ts ot ls = match ls with
345: | [] ->
346: begin match ot with
347: | [] -> `BTYP_typeset ts
348: | _ ->
349: (*
350: print_endline "WARNING UNREDUCED TYPESET UNION";
351: *)
352: `BTYP_typesetunion (`BTYP_typeset ts :: ot)
353: end
354:
355: | `BTYP_typeset xs :: t -> aux (xs @ ts) ot t
356: | h :: t -> aux ts (h :: ot) t
357: in aux [] [] ls
358:
359: (* NOTE: sets have no unique unit *)
360: (* WARNING: this representation is dangerous:
361: we can only calculate the real intersection
362: of discrete types *without type variables*
363:
364: If there are pattern variables, we may be able
365: to apply unification as a reduction. However
366: we have to be very careful doing that: we can't
367: unify variables bound by universal or lambda quantifiers
368: or the environment: technically I think we can only
369: unify existentials. For example the intersection
370:
371: 'a * int & long & 'b
372:
373: may seem to be long * int, but only if 'a and 'b are
374: pattern variables, i.e. dependent variables we're allowed
375: to assign. If they're actually function parameters, or
376: just names for types in the environment, we have to stop
377: the unification algorithm from assigning them (since they're
378: actually particular constants at that point).
379:
380: but the beta-reduction can be applied anywhere .. so I'm
381: not at all confident of the right reduction rule yet.
382:
383: Bottom line: the rule below is a hack.
384: *)
385: | `BTYP_typesetintersection ls ->
386: let ls = map br ls in
387: if mem (`BTYP_typeset []) ls then `BTYP_typeset []
388: else begin match ls with
389: | [t] -> t
390: | ls -> `BTYP_typesetintersection ls
391: end
392:
393:
394: | `BTYP_type_tuple ls -> `BTYP_type_tuple (map br ls)
395: | `BTYP_function (a,b) -> `BTYP_function (br a, br b)
396: | `BTYP_cfunction (a,b) -> `BTYP_cfunction (br a, br b)
397: | `BTYP_pointer a -> `BTYP_pointer (br a)
398: | `BTYP_lvalue a -> `BTYP_lvalue (br a)
399:
400: | `BTYP_void -> t
401: | `BTYP_type _ -> t
402: | `BTYP_unitsum _ -> t
403:
404: | `BTYP_apply (t1,t2) ->
405: let t1 = br t1 in (* eager evaluation *)
406: let t2 = br t2 in (* eager evaluation *)
407: let t1 =
408: match t1 with
409: | `BTYP_fix j ->
410: (*
411: print_endline ("++++Fixpoint application " ^ si j);
412: print_endline "+++Trail:";
413: let i = ref 0 in
414: iter (fun t -> print_endline (
415: " " ^ si (!i) ^ " ---> " ^sbt syms.dfns t)
416: ; decr i
417: )
418: (t1::t::termlist)
419: ;
420: print_endline "++++End";
421: *)
422: let whole = nth termlist (-2-j) in
423: (*
424: print_endline ("Recfun = " ^ sbt syms.dfns whole);
425: *)
426: begin match whole with
427: | `BTYP_typefun _ -> ()
428: | _ -> assert false
429: end;
430: whole
431:
432: | _ -> t1
433: in
434: (*
435: print_endline ("Function = " ^ sbt syms.dfns t1);
436: print_endline ("Argument = " ^ sbt syms.dfns t2);
437: print_endline ("Unfolded = " ^ sbt syms.dfns (unfold syms.dfns t1));
438: *)
439: begin match unfold syms.dfns t1 with
440: | `BTYP_typefun (ps,r,body) ->
441: let params' =
442: match ps with
443: | [] -> []
444: | [i,_] -> [i,t2]
445: | _ ->
446: let ts = match t2 with
447: | `BTYP_type_tuple ts -> ts
448: | _ -> assert false
449: in
450: if List.length ps <> List.length ts
451: then failwith "Wrong number of arguments to typefun"
452: else List.map2 (fun (i,_) t -> i, t) ps ts
453: in
454: (*
455: print_endline ("Body before subs" ^ sbt syms.dfns body);
456: *)
457: let t' = list_subst params' body in
458: (*
459: print_endline ("Body after subs" ^ sbt syms.dfns t');
460: *)
461: let t' = beta_reduce' syms sr (t::termlist) t' in
462: (*
463: print_endline ("Body after reduction" ^ sbt syms.dfns t');
464: *)
465: let t' = adjust t' in
466: t'
467:
468: | _ ->
469: (*
470: print_endline "Apply nonfunction .. can't reduce";
471: *)
472: `BTYP_apply (t1,t2)
473: end
474:
475: | `BTYP_type_match (tt,pts) ->
476: (*
477: print_endline ("Typematch [before reduction] " ^ sbt syms.dfns t);
478: *)
479: let tt = br tt in
480: let new_matches = ref [] in
481: iter (fun ({pattern=p; pattern_vars=dvars; assignments=eqns}, t') ->
482: (*
483: print_endline (spc ^"Tring to unify argument with " ^ sbt syms.dfns p');
484: *)
485: let p = br p in
486: let x =
487: {
488: pattern=p;
489: assignments= map (fun (j,t) -> j, br t) eqns;
490: pattern_vars=dvars;
491: }, t'
492: in
493: match maybe_unification syms.dfns [p,tt] with
494: | Some _ -> new_matches := x :: !new_matches
495: | None ->
496: (*
497: print_endline (spc ^"Discarding pattern " ^ sbt syms.dfns p');
498: *)
499: ()
500: )
501: pts
502: ;
503: let pts = rev !new_matches in
504: match pts with
505: | [] ->
506: failwith "[beta-reduce] typematch failure"
507: | ({pattern=p';pattern_vars=dvars;assignments=eqns},t') :: _ ->
508: try
509: let mgu = unification false syms.dfns [p', tt] dvars in
510: (*
511: print_endline "Typematch success";
512: *)
513: let t' = list_subst (mgu @ eqns) t' in
514: let t' = br t' in
515: (*
516: print_endline ("type match reduction result=" ^ sbt syms.dfns t');
517: *)
518: adjust t'
519: with Not_found -> `BTYP_type_match (tt,pts)
520:
1: # 27 "./lpsrc/flx_tpat.ipk"
2: open Flx_ast
3: open List
4: open Flx_mtypes2
5: open Flx_maps
6:
7: (*
8: let type_of_tpattern syms p :
9: typecode_t *
10: (int * string) list * (* variables for '?' terms *)
11: int list * (* variables for 'any' terms *)
12: (int * string) list * (* variables for 'as' terms *)
13: (int * typecode_t) list (* assignments for as terms *)
14: =
15: let sr = "unk",0,0,0,0 in
16: let explicit_vars = ref [] in
17: let any_vars = ref [] in
18: let as_vars = ref [] in
19: let eqns = ref [] in
20: let rec tp p =
21: match p with
22: | `TPAT_function (a,b) -> `TYP_function (tp a, tp b)
23: | `TPAT_tuple ps -> `TYP_tuple (map tp ps)
24: | `TPAT_sum ps -> `TYP_sum (map tp ps)
25: | `TPAT_pointer p -> `TYP_pointer (tp p)
26: | `TPAT_name (n,ps) -> `AST_name (sr,n,map tp ps)
27: | `TPAT_void -> `AST_void sr
28:
29: | `TPAT_var n ->
30: let j = !(syms.counter) in
31: incr (syms.counter);
32: explicit_vars := (j,n) :: !explicit_vars;
33: `TYP_var j
34:
35: | `TPAT_any ->
36: let j = !(syms.counter) in
37: incr (syms.counter);
38: any_vars := j :: !any_vars;
39: `TYP_var j
40:
41: | `TPAT_as (t,n) ->
42: let t = tp t in
43: let j = !(syms.counter) in
44: incr (syms.counter);
45: as_vars := (j,n) :: !as_vars;
46: eqns := (j,t) :: !eqns;
47: t
48:
49: | `TPAT_unitsum j -> `TYP_unitsum j
50: | `TPAT_type_tuple ts -> `TYP_type_tuple (map tp ts)
51: in
52: let t = tp p in
53: t,!explicit_vars, !any_vars, !as_vars, !eqns
54:
55: *)
56: let type_of_tpattern syms p :
57: typecode_t *
58: (int * string) list * (* variables for '?' terms *)
59: int list * (* variables for 'any' terms *)
60: (int * string) list * (* variables for 'as' terms *)
61: (int * typecode_t) list (* assignments for as terms *)
62: =
63: let sr = "unk",0,0,0,0 in
64: let explicit_vars = ref [] in
65: let any_vars = ref [] in
66: let as_vars = ref [] in
67: let eqns = ref [] in
68:
69: let rec tp p = match map_type tp p with
70: | `AST_patvar (sr,n) ->
71: let j = !(syms.counter) in
72: incr (syms.counter);
73: explicit_vars := (j,n) :: !explicit_vars;
74: `TYP_var j
75:
76: | `AST_patany _ ->
77: let j = !(syms.counter) in
78: incr (syms.counter);
79: any_vars := j :: !any_vars;
80: `TYP_var j
81:
82: (* NOTE CONFUSION! Is this a pattern assignment,
83: or is it fixpoint binder? Or is this the
84: same thing ..?
85:
86: Treated here as pattern assignment.
87:
88: 1 + int * list as list => list
89: *)
90: | `TYP_as (t,n) ->
91: let t = tp t in
92: let j = !(syms.counter) in
93: incr (syms.counter);
94: as_vars := (j,n) :: !as_vars;
95: eqns := (j,t) :: !eqns;
96: t
97:
98: | x -> x
99: in
100: let t = tp p in
101: t,!explicit_vars, !any_vars, !as_vars, !eqns
102:
103: