1: # 196 "./lpsrc/flx_unify.ipk"
2: open Flx_types
3: open Flx_mtypes1
4: open Flx_mtypes2
5: open Flx_print
6: open Flx_maps
7: open Flx_util
8: open List
9: open Flx_exceptions
10:
11: let unit_t = `BTYP_tuple []
12:
13: let rec dual t =
14: match map_btype dual t with
15: | `BTYP_sum ls ->
16: begin match ls with
17: | [t] -> t
18: | ls -> `BTYP_tuple ls
19: end
20:
21: | `BTYP_tuple ls ->
22: begin match ls with
23: | [] -> `BTYP_void
24: | [t] -> t
25: | ls -> `BTYP_sum ls
26: end
27:
28: | `BTYP_function (a,b) -> `BTYP_function (b,a)
29: | `BTYP_cfunction (a,b) -> `BTYP_cfunction (b,a)
30: | `BTYP_array (a,b) -> `BTYP_array (b,a)
31:
32: | `BTYP_pointer t -> `BTYP_pointer (dual t)
33: | `BTYP_lvalue t -> `BTYP_lvalue (dual t)
34: | `BTYP_void -> unit_t
35: | `BTYP_unitsum k ->
36: let rec aux ds k = if k = 0 then ds else aux (unit_t::ds) (k-1) in
37: `BTYP_tuple (aux [] k)
38:
39: | `BTYP_typeset ts -> `BTYP_intersect (map dual ts)
40: | `BTYP_intersect ts -> `BTYP_typeset (map dual ts)
41: | `BTYP_record ts -> `BTYP_variant ts
42: | t -> t
43:
44: (* top down check for fix point not under sum or pointer *)
45: let rec check_recursion t = match t with
46: | `BTYP_pointer _
47: | `BTYP_sum _
48: | `BTYP_function _
49: | `BTYP_cfunction _
50: -> ()
51:
52: | `BTYP_fix i
53: -> raise Bad_recursion
54:
55: | x -> iter_btype check_recursion x
56:
57: let term_subst t1 i t2 =
58: let rec s t = match map_btype s t with
59: | `BTYP_var (j,_) when i = j -> t2
60: | t -> t
61: in s t1
62:
63: let list_subst x t1 =
64: fold_left (fun t1 (i,t2) -> term_subst t1 i t2) t1 x
65:
66: let varmap0_subst varmap t =
67: let rec s t = match map_btype s t with
68: | `BTYP_var (i,_) as x ->
69: if Hashtbl.mem varmap i
70: then Hashtbl.find varmap i
71: else x
72: | x -> x
73: in s t
74:
75: let varmap_subst varmap t =
76: let rec s t = match map_btype s t with
77: | `BTYP_var (i,_) as x ->
78: if Hashtbl.mem varmap i
79: then Hashtbl.find varmap i
80: else x
81: | `BTYP_typefun (p,r,b) ->
82: let
83: p = map (fun (name,kind) -> (name, s kind)) p and
84: r = s r and
85: b = s b
86: in
87: `BTYP_typefun (p,r,b)
88: | x -> x
89: in s t
90:
91: (* the type arguments are matched up with the type
92: variables in order so that
93: vs_i -> ts_i
94: where vs_t might be (fred,var j)
95: *)
96: let mk_varmap
97: (vs:(string * int) list)
98: (ts:btypecode_t list)
99: =
100: if length ts <> length vs
101: then
102: failwith
103: (
104: "[tsubst] wrong number of type args, expected vs=" ^
105: si (length vs) ^
106: ", got ts=" ^
107: si (length ts)
108: )
109: ;
110: let varmap = Hashtbl.create 97 in
111: iter2
112: (fun (_, varidx) typ -> Hashtbl.add varmap varidx typ)
113: vs ts
114: ;
115: varmap
116:
117: let tsubst
118: (vs:(string * int) list)
119: (ts:btypecode_t list)
120: (t:btypecode_t)
121: =
122: varmap_subst (mk_varmap vs ts) t
123:
124:
125: (* returns the most general unifier (mgu)
126: of a set of type equations as a list
127: of variable assignments i -> t
128: or raises Not_found if there is no solution
129:
130: HOW IT WORKS:
131:
132: We start with some set of type equations
133: t1 = t2
134: t3 = t4 (1)
135: ...
136:
137: in which the LHS and RHS are general terms that
138: may contain type variables.
139:
140: We want to say whether the equations are consistent,
141: and if so, to return a solution of the form
142: of a set of equations:
143:
144: v1 = u1
145: v2 = u2 (2)
146:
147: where v1 .. vn are type variable
148: which do not occur in any of the
149: terms u1 .. un
150:
151: Such a set is a solution if by replacing v1 with u1,
152: v2 with u2 .. vn with un,
153: everywhere they occur in t1, t2 .... tn,
154: the original equations are reduced to
155: equations terms which are structurally equal
156:
157: The technique is to pick one equation,
158: and match up the outermost structure,
159: making new equations out of the pieces in the middle,
160: or failing if the outer structure does not match.
161:
162: We discard the original equation,
163: add the new equations to the set,
164: and then for any variable assignments of form (2)
165: found, we eliminate that variable in the
166: all the other equations by substitution.
167:
168:
169: At the end we are guarrateed to either have found
170: the equations have no solution, or computed one,
171: although it may be that the terms u1 .. u2 ..
172: contain some type variables.
173:
174: There is a caveat though: we may obtain
175: an equation
176:
177: v = t
178:
179: where v occurs in t, that is, a recursive equation.
180: If that happens, we eliminate the occurences
181: of v in t before replacement in other equations:
182: we do this by replacing the RHS occurences of
183: v with a fixpoint operator.
184:
185: *)
186:
187:
188: let var_i_occurs i t =
189: let rec aux t:unit = match t with
190: | `BTYP_var (j,_) when i = j -> raise Not_found
191: | _ -> iter_btype aux t
192: in
193: try
194: aux t;
195: false
196: with Not_found -> true
197:
198: let rec vars_in t =
199: let vs = ref IntSet.empty in
200: let add_var i = vs := IntSet.add i !vs in
201: let rec aux t = match t with
202: | `BTYP_var (i,_) -> add_var i
203: | _ -> iter_btype aux t
204: in aux t; !vs
205:
206: let fix i t =
207: let rec aux n t =
208: let aux t = aux (n - 1) t in
209: match t with
210: | `BTYP_var (k,_) -> if k = i then `BTYP_fix n else t
211: | `BTYP_inst (k,ts) -> `BTYP_inst (k, map aux ts)
212: | `BTYP_tuple ts -> `BTYP_tuple (map aux ts)
213: | `BTYP_sum ts -> `BTYP_sum (map aux ts)
214: | `BTYP_intersect ts -> `BTYP_intersect (map aux ts)
215: | `BTYP_typeset ts -> `BTYP_typeset (map aux ts)
216: | `BTYP_function (a,b) -> `BTYP_function (aux a, aux b)
217: | `BTYP_cfunction (a,b) -> `BTYP_cfunction (aux a, aux b)
218: | `BTYP_pointer a -> `BTYP_pointer (aux a)
219: | `BTYP_lvalue a -> `BTYP_lvalue (aux a)
220: | `BTYP_array (a,b) -> `BTYP_array (aux a, aux b)
221:
222: | `BTYP_record ts ->
223: `BTYP_record (map (fun (s,t) -> s, aux t) ts)
224:
225: | `BTYP_variant ts ->
226: `BTYP_variant (map (fun (s,t) -> s, aux t) ts)
227:
228: | `BTYP_unitsum _
229: | `BTYP_void
230: | `BTYP_fix _
231: | `BTYP_apply _
232: | `BTYP_typefun _
233: | `BTYP_type
234: | `BTYP_type_tuple _
235: | `BTYP_type_match _
236: | `BTYP_typesetunion _ -> t
237: | `BTYP_typesetintersection _ -> t
238: in
239: aux 0 t
240:
241: let var_list_occurs ls t =
242: let yes = ref false in
243: iter (fun i -> yes := !yes || var_i_occurs i t) ls;
244: !yes
245:
246: let lstrip dfns t =
247: let rec aux trail t' =
248: let uf t = aux (0::trail) t in
249: match t' with
250: | `BTYP_sum ls -> `BTYP_sum (map uf ls)
251: | `BTYP_tuple ls -> `BTYP_tuple (map uf ls)
252: | `BTYP_array (a,b) -> `BTYP_array (uf a, uf b)
253: | `BTYP_record ts -> `BTYP_record (map (fun (s,t) -> s,uf t) ts)
254: | `BTYP_variant ts -> `BTYP_variant (map (fun (s,t) -> s,uf t) ts)
255:
256: (* I think this is WRONG .. *)
257: | `BTYP_function (a,b) -> `BTYP_function (uf a, uf b)
258: | `BTYP_cfunction (a,b) -> `BTYP_cfunction (uf a, uf b)
259:
260: | `BTYP_pointer a -> `BTYP_pointer (uf a)
261: | `BTYP_lvalue a -> aux (1::trail) a
262: | `BTYP_fix i ->
263: let k = ref i in
264: let j = ref 0 in
265: let trail = ref trail in
266: while !k < 0 do
267: j := !j + hd !trail;
268: trail := tl !trail;
269: incr k
270: done;
271: `BTYP_fix (i + !j)
272:
273: | `BTYP_inst (i,ts) -> `BTYP_inst (i,map uf ts)
274: | _ -> t'
275: in aux [] t
276:
277:
278:
279: (* NOTE: this algorithm unifies EQUATIONS
280: not inequations, therefore it doesn't
281: handle any subtyping
282: *)
283:
284: (* NOTE: at the moment,
285: unification doesn't care about type variable
286: meta types: we should probably require them
287: to be the same for an assignment or fail
288: the unification .. however that requires
289: comparing the metatypes for equality, and to that
290: that right requires unification .. :)
291: *)
292:
293: let rec unification allow_lval dfns
294: (eqns: (btypecode_t * btypecode_t) list)
295: (dvars: IntSet.t)
296: : (int * btypecode_t) list =
297: (*
298: print_endline ( "Dvars = { " ^ catmap ", " si (IntSet.elements dvars) ^ "}");
299: *)
300: let eqns = ref eqns in
301: let mgu = ref [] in
302: let rec loop () : unit =
303: match !eqns with
304: | [] -> ()
305: | h :: t ->
306: eqns := t;
307: let s = ref None in
308: begin match h with
309: | (`BTYP_var (i,mi) as ti), (`BTYP_var (j,mj) as tj)->
310: (*
311: print_endline ("Equated variables " ^ si i ^ " <-> " ^ si j);
312: *)
313:
314: (* meta type have to agree *)
315: if mi <> mj then raise Not_found;
316:
317: if i <> j then
318: if IntSet.mem i dvars then
319: s := Some (i,tj)
320: else if IntSet.mem j dvars then
321: s := Some (j,ti)
322: else raise Not_found
323:
324: | `BTYP_lvalue t1, `BTYP_lvalue t2 ->
325: eqns := (t1,t2) :: !eqns
326:
327: (* This says an argument of type lvalue t can match
328: a parameter of type t -- not the other way around tho
329:
330: This must be done FIRST, before matching against
331: `BTYP_var i, t
332: to ensure t can't be an lvalue
333: *)
334: | t1, `BTYP_lvalue t2 when allow_lval ->
335: eqns := (t1,t2) :: !eqns
336:
337: (*
338: | `BTYP_lvalue t1, t2 when allow_lval ->
339: print_endline "WARNING LVALUE ON LEFT UNEXPECTED ..";
340: eqns := (t1,t2) :: !eqns
341: *)
342:
343: | `BTYP_var (i,_), t
344: | t,`BTYP_var (i,_) ->
345: (*
346: print_endline ("variable assignment " ^ si i ^ " -> " ^ sbt dfns t);
347: *)
348:
349: (* WE SHOULD CHECK THAT t has the right meta type .. but
350: the metatype routine isn't defined yet ..
351: *)
352: if not (IntSet.mem i dvars) then raise Not_found;
353: if var_i_occurs i t
354: then begin
355: print_endline
356: (
357: "recursion in unification, terms: " ^
358: match h with (a,b) ->
359: sbt dfns a ^ " = " ^ sbt dfns b
360: );
361: s := Some (i, fix i t)
362: end else begin
363: let t = lstrip dfns t in
364: (*
365: print_endline "Adding substitution";
366: *)
367: s := Some (i,t)
368: end
369:
370: | `BTYP_intersect ts,t
371: | t,`BTYP_intersect ts ->
372: iter (function t' -> eqns := (t,t') :: !eqns) ts
373:
374: | `BTYP_pointer t1, `BTYP_pointer t2 ->
375: eqns := (t1,t2) :: !eqns
376:
377: | `BTYP_unitsum i, `BTYP_unitsum j when i = j -> ()
378:
379: | `BTYP_unitsum k, `BTYP_sum ls
380: | `BTYP_sum ls, `BTYP_unitsum k when length ls = k ->
381: iter
382: (function
383: | `BTYP_var _ as v ->
384: eqns := (v,unit_t) :: !eqns
385: | _ -> raise Not_found
386: )
387: ls
388:
389: | `BTYP_array (t11, t12), `BTYP_array (t21, t22)
390: | `BTYP_function (t11, t12), `BTYP_function (t21, t22)
391: | `BTYP_cfunction (t11, t12), `BTYP_cfunction (t21, t22) ->
392: eqns := (t11,t21) :: (t12,t22) :: !eqns
393:
394: | `BTYP_record [],`BTYP_tuple []
395: | `BTYP_tuple [],`BTYP_record [] -> ()
396:
397: | `BTYP_record t1,`BTYP_record t2 ->
398: if length t1 = length t2
399: then begin
400: let rcmp (s1,_) (s2,_) = compare s1 s2 in
401: let t1 = sort rcmp t1 in
402: let t2 = sort rcmp t2 in
403: if (map fst t1) <> (map fst t2) then raise Not_found;
404: let rec merge e a b = match a,b with
405: | [],[] -> e
406: | ah :: at, bh :: bt -> merge ((ah,bh) :: e) at bt
407: | _ -> assert false
408: in
409: eqns := merge !eqns (map snd t1) (map snd t2);
410: s := None
411: end
412: else raise Not_found
413:
414: | `BTYP_variant [],`BTYP_void
415: | `BTYP_void,`BTYP_variant [] -> ()
416:
417: | `BTYP_variant t1,`BTYP_variant t2 ->
418: if length t1 = length t2
419: then begin
420: let rcmp (s1,_) (s2,_) = compare s1 s2 in
421: let t1 = sort rcmp t1 in
422: let t2 = sort rcmp t2 in
423: if (map fst t1) <> (map fst t2) then raise Not_found;
424: let rec merge e a b = match a,b with
425: | [],[] -> e
426: | ah :: at, bh :: bt -> merge ((ah,bh) :: e) at bt
427: | _ -> assert false
428: in
429: eqns := merge !eqns (map snd t1) (map snd t2);
430: s := None
431: end
432: else raise Not_found
433:
434: | `BTYP_type,`BTYP_type-> ()
435: | `BTYP_void,`BTYP_void -> ()
436:
437: | `BTYP_inst (i1,ts1),`BTYP_inst (i2,ts2) ->
438: if i1 <> i2 then raise Not_found
439: else if length ts1 <> length ts2 then raise Not_found
440: else
441: begin
442: let rec merge e a b = match a,b with
443: | [],[] -> e
444: | ah :: at, bh :: bt -> merge ((ah,bh) :: e) at bt
445: | _ -> assert false
446: in
447: eqns := merge !eqns ts1 ts2;
448: s := None
449: end
450:
451: | `BTYP_fix i,`BTYP_fix j ->
452: if i <> j then raise Not_found
453:
454: | `BTYP_tuple ls, `BTYP_array (ta,`BTYP_unitsum n)
455: | `BTYP_array (ta,`BTYP_unitsum n), `BTYP_tuple ls
456: when n = length ls ->
457: iter (fun t -> eqns := (t,ta) :: !eqns) ls
458:
459: (* type tuple is handled same as a tuple type .. not
460: really sure this is right. Certainly, the corresponding
461: terms in both must unify, however possibly we should
462: return distinct MGU for each case for the type tuple,
463: possibly with distinct bindings for the same variable..
464: *)
465:
466: | (`BTYP_type_tuple ls1, `BTYP_type_tuple ls2)
467: | (`BTYP_tuple ls1, `BTYP_tuple ls2)
468: | (`BTYP_sum ls1, `BTYP_sum ls2)
469: when length ls1 = length ls2 ->
470: begin
471: let rec merge e a b = match a,b with
472: | [],[] -> e
473: | ah :: at, bh :: bt -> merge ((ah,bh) :: e) at bt
474: | _ -> assert false
475: in
476: eqns := merge !eqns ls1 ls2;
477: s := None
478: end
479:
480: | x,y ->
481: (*
482: print_endline ("Terms do not match: " ^ sbt dfns x ^ " <-> " ^ sbt dfns y);
483: *)
484: raise Not_found
485: end
486: ;
487: begin match !s with
488: | None -> ()
489: | Some (i,t) ->
490: (*
491: print_endline ("Substituting " ^ si i ^ " -> " ^ sbt dfns t);
492: *)
493: eqns :=
494: map
495: (fun (a,b) ->
496: term_subst a i t,
497: term_subst b i t
498: )
499: !eqns
500: ;
501: assert(not (mem_assoc i !mgu));
502: mgu :=
503: (i,t) ::
504: (map
505: (fun (j,t') -> j,term_subst t' i t)
506: !mgu
507: )
508: end
509: ;
510: loop ()
511: in
512: loop ();
513: !mgu
514:
515: let find_vars_eqns eqns =
516: let lhs_vars = ref IntSet.empty in
517: let rhs_vars = ref IntSet.empty in
518: iter (fun (l,r) ->
519: lhs_vars := IntSet.union !lhs_vars (vars_in l);
520: rhs_vars := IntSet.union !rhs_vars (vars_in r)
521: )
522: eqns
523: ;
524: !lhs_vars,!rhs_vars
525:
526: let maybe_unification dfns eqns =
527: let l,r = find_vars_eqns eqns in
528: let dvars = IntSet.union l r in
529: try Some (unification false dfns eqns dvars)
530: with Not_found -> None
531:
532: let maybe_matches dfns eqns =
533: let l,r = find_vars_eqns eqns in
534: let dvars = IntSet.union l r in
535: try Some (unification true dfns eqns dvars)
536: with Not_found -> None
537:
538: let maybe_specialisation dfns eqns =
539: let l,_ = find_vars_eqns eqns in
540: try Some (unification true dfns eqns l)
541: with Not_found -> None
542:
543: let unifies dfns t1 t2 =
544: let eqns = [t1,t2] in
545: match maybe_unification dfns eqns with
546: | None -> false
547: | Some _ -> true
548:
549: let ge dfns a b =
550: (*
551: print_endline ("Compare terms " ^ sbt dfns a ^ " >? " ^ sbt dfns b);
552: *)
553: match maybe_specialisation dfns [a,b] with
554: | None -> false
555: | Some mgu ->
556: (*
557: print_endline ("MGU from specialisation = ");
558: iter (fun (i, t) -> print_endline (si i ^ " --> " ^ sbt dfns t)) mgu;
559: print_endline "";
560: *)
561: true
562:
563: let compare_sigs dfns a b =
564: match ge dfns a b, ge dfns b a with
565: | true, true -> `Equal
566: | false, false -> `Incomparable
567: | true, false -> `Greater
568: | false, true -> `Less
569:
570:
571: (* returns true if a and b have an mgu,
572: and also adds each element of the mgu to
573: the varmap if it isn't already present
574: this routine is ONLY to be used for
575: calculating the return types of functions,
576: where we're unifying the type of the
577: return statements... probably fails
578: for generic functions .. since the two
579: kinds of type variables aren't distinguished
580: (Fun ret type var is an unknown type, not a
581: variable one .. it must be eliminated, but
582: type parameters must not be [since they're
583: instantiated to multiple values .. ..])
584:
585: The subtyping rule for lvalues also applies
586: here. An lvalue type for a returned expression
587: is compatible with a non-value function return.
588:
589: The unification algorithm can account for this,
590: it requires the LHS = RHS equation to support
591: an extra 'lvalue' in the RHS, but not the other
592: way around. So the expression type has to be the RHS
593: and the declared type the LHS.
594: *)
595:
596: let do_unify syms a b =
597: let eqns =
598: [
599: varmap_subst syms.varmap a,
600: varmap_subst syms.varmap b
601: ]
602: in
603: let l,r = find_vars_eqns eqns in
604: let dvars = IntSet.union l r in
605: try
606: (*
607: print_endline "Calling unification";
608: *)
609: let mgu = unification true syms.dfns eqns dvars in
610: (*
611: print_endline "mgu=";
612: iter
613: (fun (i, t) ->
614: print_endline (string_of_int i ^ " -> " ^ string_of_btypecode syms.dfns t)
615: )
616: mgu;
617: *)
618:
619: (* This crud is used to find the return types of
620: functions initially marked TYP_none, which really
621: means the type is unknown and should be calculated.
622: The system binds each TYP_none to a SPECIAL type variable,
623: and this code is supposed to store type computed by
624: some random unification in a hashtable for such variables.
625:
626: The variables are marked as SPECIAL by using the same
627: index as the function whose return type is unknown.
628: *)
629: iter
630: (fun (i, t) ->
631: if Hashtbl.mem syms.varmap i
632: then
633: begin
634: (*
635: print_endline "Var already in varmap ..";
636: *)
637: let t' = Hashtbl.find syms.varmap i in
638: if t' <> t then
639: failwith
640: (
641: "[do_unify] binding for type variable " ^ string_of_int i ^
642: " is inconsistent\n"
643: )
644: else ()
645: end
646: else
647: begin
648: match Hashtbl.find syms.dfns i with
649: | { symdef=`SYMDEF_glr _ }
650: | { symdef=`SYMDEF_function _ } ->
651: (*
652: print_endline ("Adding variable " ^ string_of_int i ^ " type " ^ string_of_btypecode syms.dfns t);
653: *)
654: Hashtbl.add syms.varmap i t
655:
656: (* if it's a declared type variable, leave it alone *)
657: | {symdef=`SYMDEF_typevar _ } -> ()
658:
659: | _ ->
660: failwith
661: (
662: "[do_unify] attempt to add non-function return unknown type variable "^
663: si i^", type "^sbt syms.dfns t^" to hashtble"
664: )
665: end
666: )
667: mgu
668: ;
669: true
670: with Not_found -> false
671:
672: let rec memq trail (a,b) = match trail with
673: | [] -> false
674: | (i,j)::t -> i == a && j == b || memq t (a,b)
675:
676: let rec type_eq' dfns allow_lval ltrail ldepth rtrail rdepth trail t1 t2 =
677: (* print_endline (sbt dfns t1 ^ " =? " ^ sbt dfns t2); *)
678: if memq trail (t1,t2) then true
679: else let te a b = type_eq' dfns allow_lval
680: ((ldepth,t1)::ltrail) (ldepth+1)
681: ((rdepth,t2)::rtrail) (rdepth+1)
682: ((t1,t2)::trail)
683: a b
684: in
685: match t1,t2 with
686: | `BTYP_inst (i1,ts1),`BTYP_inst (i2,ts2) ->
687: i1 = i2 &&
688: length ts1 = length ts2 &&
689: fold_left2
690: (fun tr a b -> tr && te a b)
691: true ts1 ts2
692:
693: | `BTYP_unitsum i,`BTYP_unitsum j -> i = j
694:
695: | `BTYP_sum ts1, `BTYP_sum ts2
696: | `BTYP_tuple ts1,`BTYP_tuple ts2 ->
697: if length ts1 = length ts2
698: then
699: fold_left2
700: (fun tr a b -> tr && te a b)
701: true ts1 ts2
702: else false
703:
704: | `BTYP_record [],`BTYP_tuple []
705: | `BTYP_tuple [],`BTYP_record [] -> true
706:
707: | `BTYP_record t1,`BTYP_record t2 ->
708: if length t1 = length t2
709: then begin
710: let rcmp (s1,_) (s2,_) = compare s1 s2 in
711: let t1 = sort rcmp t1 in
712: let t2 = sort rcmp t2 in
713: map fst t1 = map fst t2 &&
714: fold_left2
715: (fun tr a b -> tr && te a b)
716: true (map snd t1) (map snd t2)
717: end else false
718:
719: | `BTYP_variant [],`BTYP_tuple []
720: | `BTYP_tuple [],`BTYP_variant [] -> true
721:
722: | `BTYP_variant t1,`BTYP_variant t2 ->
723: if length t1 = length t2
724: then begin
725: let rcmp (s1,_) (s2,_) = compare s1 s2 in
726: let t1 = sort rcmp t1 in
727: let t2 = sort rcmp t2 in
728: map fst t1 = map fst t2 &&
729: fold_left2
730: (fun tr a b -> tr && te a b)
731: true (map snd t1) (map snd t2)
732: end else false
733:
734:
735: | `BTYP_array (s1,d1),`BTYP_array (s2,d2)
736: | `BTYP_function (s1,d1),`BTYP_function (s2,d2)
737: | `BTYP_cfunction (s1,d1),`BTYP_cfunction (s2,d2)
738: | `BTYP_apply(s1,d1),`BTYP_apply(s2,d2)
739: -> te s1 s2 && te d1 d2
740:
741: (* order is important for lvalues .. *)
742: | `BTYP_array (ta,`BTYP_unitsum n),`BTYP_tuple ts
743: when length ts = n ->
744: fold_left (fun tr t -> tr && te ta t) true ts
745:
746:
747: | `BTYP_tuple ts,`BTYP_array (ta,`BTYP_unitsum n)
748: when length ts = n ->
749: fold_left (fun tr t -> tr && te t ta) true ts
750:
751: | `BTYP_pointer p1,`BTYP_pointer p2
752: -> te p1 p2
753:
754: | `BTYP_lvalue p1,`BTYP_lvalue p2
755: -> te p1 p2
756:
757: | p1,(`BTYP_lvalue p2 as lt) when allow_lval
758: ->
759: type_eq' dfns allow_lval
760: ltrail ldepth
761: ((rdepth,lt)::rtrail) (rdepth+1)
762: ((p1,lt)::trail)
763: p1 p2
764:
765: | `BTYP_void,`BTYP_void
766: -> true
767:
768: | `BTYP_var i, `BTYP_var j ->
769: i = j
770:
771: | `BTYP_fix i,`BTYP_fix j ->
772: let a = assoc (ldepth+i) ltrail in
773: let b = assoc (rdepth+j) rtrail in
774: (* print_endline "Matching fixpoints"; *)
775: type_eq' dfns allow_lval ltrail ldepth rtrail rdepth trail a b
776:
777: | `BTYP_fix i,t ->
778: (* print_endline "LHS fixpoint"; *)
779: let a = assoc (ldepth+i) ltrail in
780: type_eq' dfns allow_lval ltrail ldepth rtrail rdepth trail a t
781:
782: | t,`BTYP_fix j ->
783: (* print_endline "RHS fixpoint"; *)
784: let b = assoc (rdepth+j) rtrail in
785: type_eq' dfns allow_lval ltrail ldepth rtrail rdepth trail t b
786:
787: | _ -> false
788:
789: let type_eq dfns t1 t2 = (* print_endline "TYPE EQ"; *)
790: type_eq' dfns false [] 0 [] 0 [] t1 t2
791:
792: let type_match dfns t1 t2 = (* print_endline "TYPE MATCH"; *)
793: type_eq' dfns true [] 0 [] 0 [] t1 t2
794:
795: (* NOTE: only works on explicit fixpoint operators,
796: i.e. it won't work on typedefs: no name lookup,
797: these should be removed first ..
798: another view: only works on non-generative types.
799: *)
800:
801: let unfold dfns t =
802: let rec aux depth t' =
803: let uf t = aux (depth+1) t in
804: match t' with
805: | `BTYP_sum ls -> `BTYP_sum (map uf ls)
806: | `BTYP_tuple ls -> `BTYP_tuple (map uf ls)
807: | `BTYP_record ls -> `BTYP_record (map (fun (s,t) -> s,uf t) ls)
808: | `BTYP_variant ls -> `BTYP_variant (map (fun (s,t) -> s,uf t) ls)
809: | `BTYP_array (a,b) -> `BTYP_array (uf a, uf b)
810: | `BTYP_function (a,b) -> `BTYP_function (uf a, uf b)
811: | `BTYP_cfunction (a,b) -> `BTYP_cfunction (uf a, uf b)
812: | `BTYP_pointer a -> `BTYP_pointer (uf a)
813: | `BTYP_lvalue a -> `BTYP_lvalue (uf a)
814: | `BTYP_fix i when (-i) = depth -> t
815: | `BTYP_fix i when (-i) > depth ->
816: failwith ("[unfold] Fix point outside term, depth="^string_of_int i)
817:
818: | `BTYP_apply (a,b) -> `BTYP_apply(uf a, uf b)
819: | `BTYP_inst (i,ts) -> `BTYP_inst (i,map uf ts)
820: | _ -> t'
821: in aux 0 t
822:
823: exception Found of btypecode_t
824:
825: (* this undoes an unfold: it won't minimise an arbitrary type *)
826: let fold dfns t =
827: let rec aux trail depth t' =
828: let ax t = aux ((depth,t')::trail) (depth+1) t in
829: match t' with
830: | `BTYP_intersect ls
831: | `BTYP_sum ls
832: | `BTYP_inst (_,ls)
833: | `BTYP_tuple ls -> iter ax ls
834: | `BTYP_record ls -> iter (fun (s,t) -> ax t) ls
835: | `BTYP_variant ls -> iter (fun (s,t) -> ax t) ls
836:
837: | `BTYP_array (a,b)
838: | `BTYP_function (a,b) -> ax a; ax b
839: | `BTYP_cfunction (a,b) -> ax a; ax b
840:
841: | `BTYP_pointer a -> ax a
842: | `BTYP_lvalue a -> ax a
843:
844: | `BTYP_void
845: | `BTYP_unitsum _
846: | `BTYP_var _
847: | `BTYP_fix 0 -> ()
848:
849: | `BTYP_fix i ->
850: let k = depth + i in
851: begin try
852: let t'' = assoc k trail in
853: if type_eq dfns t'' t then raise (Found t'')
854: with Not_found -> ()
855: end
856:
857: | `BTYP_apply (a,b) -> ax a; ax b
858:
859: | `BTYP_typesetintersection _
860: | `BTYP_typesetunion _
861: | `BTYP_typeset _
862: | `BTYP_typefun _
863: | `BTYP_type
864: | `BTYP_type_tuple _
865: | `BTYP_type_match _ -> () (* assume fixpoint can't span these boundaries *)
866: (* failwith ("[fold] unexpected metatype " ^ sbt dfns t') *)
867: in
868: try aux [] 0 t; t
869: with Found t -> t
870:
871: (* produces a unique minimal representation of a type
872: by folding at every node *)
873:
874: let minimise dfns t = match map_btype (fold dfns) t with x -> fold dfns x
875:
876: let var_occurs t =
877: let rec aux t =
878: match t with
879: | `BTYP_intersect ls
880: | `BTYP_typeset ls
881: | `BTYP_typesetintersection ls
882: | `BTYP_typesetunion ls
883: | `BTYP_sum ls
884: | `BTYP_inst (_,ls)
885: | `BTYP_tuple ls -> iter aux ls
886: | `BTYP_record ls -> iter (fun (s,t) -> aux t) ls
887: | `BTYP_variant ls -> iter (fun (s,t) -> aux t) ls
888:
889: | `BTYP_array (a,b)
890: | `BTYP_function (a,b) -> aux a; aux b
891: | `BTYP_cfunction (a,b) -> aux a; aux b
892:
893: | `BTYP_pointer a -> aux a
894: | `BTYP_lvalue a -> aux a
895:
896: | `BTYP_unitsum _
897: | `BTYP_void
898: | `BTYP_fix _ -> ()
899:
900: | `BTYP_var _ -> raise Not_found
901: | _ -> failwith "[var_occurs] unexpected metatype"
902:
903: in try aux t; false with Not_found -> true
904:
905: let normalise_type t =
906: let counter = ref 0 in
907: let varmap = ref [] in
908: let rec aux t = match map_btype aux t with
909: | `BTYP_record [] -> `BTYP_tuple []
910: | `BTYP_variant [] -> `BTYP_void
911: | `BTYP_var (i,mt) ->
912: `BTYP_var
913: ((
914: match list_index !varmap i with
915: | Some j -> j
916: | None ->
917: let n = !counter in
918: incr counter;
919: varmap := !varmap @ [i];
920: n
921: ),mt)
922: | x -> x
923: in
924: let x = aux t in
925: !varmap, x
926:
927: let ident x = x
928:
929: (* not really right! Need to map the types as well,
930: since we're instantiating a polymorphic term with
931: a more specialised one
932:
933: Also won't substitute into LHS of things like direct_apply.
934: *)
935: let expr_term_subst e1 i e2 =
936: let rec s e = match map_tbexpr ident s ident e with
937: | `BEXPR_name (j,_),_ when i = j -> e2
938: | e -> e
939: in s e1
940:
941: let rec expr_unification dfns
942: (eqns: (tbexpr_t * tbexpr_t) list)
943: (tdvars: IntSet.t)
944: (edvars: IntSet.t)
945: :
946: (int * btypecode_t) list *
947: (int * tbexpr_t) list
948: =
949: (*
950: print_endline ( "Dvars = { " ^ catmap ", " si (IntSet.elements dvars) ^ "}");
951: *)
952: let teqns = ref [] in
953: let eqns = ref eqns in
954: let mgu = ref [] in
955: let rec loop () : unit =
956: match !eqns with
957: | [] -> ()
958: | h :: t ->
959: eqns := t;
960: let s = ref None in
961: let (lhse,lhst),(rhse,rhst) = h in
962: teqns := (lhst,rhst) :: !teqns;
963:
964: (* WE COULD UNIFY TYPES HERE -- but there is no need!
965: if the terms unify, the types MUST
966: We DO need to unify the types -- but only after
967: we've found matching terms.
968:
969: Note: the types in the ts lists DO have to be
970: unified! It's only the types OF terms that
971: don't require processing .. since they're just
972: convenience caches of the term type, which can
973: be computed directly from the term.
974: *)
975: begin match (lhse,rhse) with
976: | (`BEXPR_name (i,[]) as ei), (`BEXPR_name (j,[]) as ej)->
977: (*
978: print_endline ("Equated variables " ^ si i ^ " <-> " ^ si j);
979: *)
980:
981: if i <> j then
982: if IntSet.mem i edvars then
983: s := Some (i,(ej,rhst))
984: else if IntSet.mem j edvars then
985: s := Some (j,(ei,lhst))
986: else raise Not_found
987:
988: | `BEXPR_name (i,_),x ->
989: if not (IntSet.mem i edvars) then raise Not_found;
990: s := Some (i,(x,rhst))
991:
992: | x,`BEXPR_name (i,_) ->
993: if not (IntSet.mem i edvars) then raise Not_found;
994: s := Some (i,(x,lhst))
995:
996: | `BEXPR_apply (f1,e1),`BEXPR_apply(f2,e2) ->
997: eqns := (f1,f2) :: (e1,e2) :: !eqns
998:
999: | `BEXPR_closure (i,ts1),`BEXPR_closure(j,ts2) when i = j -> ()
1000:
1001: | `BEXPR_apply_prim (i,ts1,e1),`BEXPR_apply_prim(j,ts2,e2)
1002: | `BEXPR_apply ( (`BEXPR_closure (i,ts1),_), e1),`BEXPR_apply_prim(j,ts2,e2)
1003: | `BEXPR_apply_prim (i,ts1,e1),`BEXPR_apply( (`BEXPR_closure(j,ts2),_),e2)
1004:
1005: | `BEXPR_apply_direct (i,ts1,e1),`BEXPR_apply_direct(j,ts2,e2)
1006: | `BEXPR_apply ( (`BEXPR_closure (i,ts1),_), e1),`BEXPR_apply_direct(j,ts2,e2)
1007: | `BEXPR_apply_direct (i,ts1,e1),`BEXPR_apply( (`BEXPR_closure(j,ts2),_),e2)
1008: when i = j
1009: ->
1010: assert (length ts1 = length ts2);
1011: teqns := combine ts1 ts2 @ !teqns;
1012: eqns := (e1,e2) :: !eqns
1013:
1014: | `BEXPR_coerce (e,t),`BEXPR_coerce (e',t') ->
1015: teqns := (t,t') :: !teqns;
1016: eqns := (e,e') :: !eqns
1017:
1018: | (`BEXPR_tuple ls1, `BEXPR_tuple ls2)
1019: when length ls1 = length ls2 ->
1020: begin
1021: let rec merge e a b = match a,b with
1022: | [],[] -> e
1023: | ah :: at, bh :: bt -> merge ((ah,bh) :: e) at bt
1024: | _ -> assert false
1025: in
1026: eqns := merge !eqns ls1 ls2;
1027: s := None
1028: end
1029:
1030: | x,y ->
1031: (*
1032: print_endline ("Terms do not match: " ^ sbt dfns x ^ " <-> " ^ sbt dfns y);
1033: *)
1034: raise Not_found
1035: end
1036: ;
1037: begin match !s with
1038: | None -> ()
1039: | Some (i,t) ->
1040: (*
1041: print_endline ("Substituting " ^ si i ^ " -> " ^ sbt dfns t);
1042: *)
1043: eqns :=
1044: map
1045: (fun (a,b) ->
1046: expr_term_subst a i t,
1047: expr_term_subst b i t
1048: )
1049: !eqns
1050: ;
1051: assert(not (mem_assoc i !mgu));
1052: mgu :=
1053: (i,t) ::
1054: (map
1055: (fun (j,t') -> j,expr_term_subst t' i t)
1056: !mgu
1057: )
1058: end
1059: ;
1060: loop ()
1061: in
1062: loop ();
1063: let tmgu = unification true dfns !teqns tdvars in
1064: tmgu,
1065: !mgu
1066:
1067: let setoflist ls = fold_left (fun s i -> IntSet.add i s) IntSet.empty ls
1068:
1069: let expr_maybe_matches (dfns:symbol_table_t)
1070: (tvars:int list) (evars:int list)
1071: (le: tbexpr_t)
1072: (re:tbexpr_t)
1073: :
1074: ((int * btypecode_t) list *
1075: (int * tbexpr_t) list) option
1076: =
1077: let tvars = setoflist tvars in
1078: let evars = setoflist evars in
1079: let eqns = [le,re] in
1080: try Some (expr_unification dfns eqns tvars evars)
1081: with Not_found -> None
1082:
1083: