5.15. Unification

Start ocaml section to src/flx_unify.mli[1 /1 ]
     1: # 4 "./lpsrc/flx_unify.ipk"
     2: (** this module provides type unification
     3: and utilities
     4: *)
     5: 
     6: open Flx_types
     7: open Flx_mtypes1
     8: open Flx_mtypes2
     9: 
    10: (** obtain the mgu of a set of type equations with specified
    11:   dependent variable set, throws Not_found if cannot unify
    12: *)
    13: val unification:
    14:   bool -> (* true if lvalue degrade is allowed *)
    15:   symbol_table_t -> (* just for diagnostics *)
    16:   (btypecode_t * btypecode_t) list ->
    17:   IntSet.t -> (* dependent variable set *)
    18:   (int * btypecode_t) list
    19: 
    20: 
    21: (** obtain the mgu of a set of type equations *)
    22: val maybe_unification:
    23:   symbol_table_t -> (* just for diagnostics *)
    24:   (btypecode_t * btypecode_t) list ->
    25:   (int * btypecode_t) list option
    26: 
    27: (** obtain the mgu of a set of type equations,
    28: for matching parameters against arguments: allows
    29: special subtyping for lvalues
    30: *)
    31: val maybe_matches:
    32:   symbol_table_t -> (* just for diagnostics *)
    33:   (btypecode_t * btypecode_t) list ->
    34:   (int * btypecode_t) list option
    35: 
    36: val maybe_specialisation:
    37:   symbol_table_t -> (* just for diagnostics *)
    38:   (btypecode_t * btypecode_t) list ->
    39:   (int * btypecode_t) list option
    40: 
    41: (** test if two types unify *)
    42: val unifies:
    43:   symbol_table_t -> (* just for diagnostics *)
    44:   btypecode_t ->
    45:   btypecode_t ->
    46:   bool
    47: 
    48: (** compare type for structural/unificational ordering *)
    49: val compare_sigs:
    50:   symbol_table_t ->
    51:   btypecode_t ->
    52:   btypecode_t ->
    53:   partial_order_result_t
    54: 
    55: (** check if the two types unify: update the
    56: variable definitions in sym_state ??? Only
    57: useful if type variables are global, which is
    58: the function return type unknown variable case..
    59: *)
    60: val do_unify:
    61:   sym_state_t ->
    62:   btypecode_t ->
    63:   btypecode_t ->
    64:   bool
    65: 
    66: (** compare for iso-equality *)
    67: val type_eq:
    68:   symbol_table_t ->
    69:   btypecode_t ->
    70:   btypecode_t ->
    71:   bool
    72: 
    73: (** compare parameter with argument type,
    74:   argument may have extra lvalue in it
    75: *)
    76: val type_match:
    77:   symbol_table_t ->
    78:   btypecode_t ->
    79:   btypecode_t ->
    80:   bool
    81: 
    82: (** [lstrip t] returns t all lvalue combinators elided
    83: *)
    84: val lstrip:
    85:   symbol_table_t ->
    86:   btypecode_t ->
    87:   btypecode_t
    88: 
    89: (** [unfold t] returns t with each fix variable
    90:   denoting t replaced with t
    91: *)
    92: val unfold:
    93:   symbol_table_t ->
    94:   btypecode_t ->
    95:   btypecode_t
    96: 
    97: (** undo an unfold *)
    98: val fold:
    99:   symbol_table_t ->
   100:   btypecode_t ->
   101:   btypecode_t
   102: 
   103: (** minimise the representation of a type
   104: with respect to recursion
   105: *)
   106: 
   107: val minimise:
   108:   symbol_table_t ->
   109:   btypecode_t ->
   110:   btypecode_t
   111: 
   112: (** replace variables in the term using
   113: the mapping in a list *)
   114: val list_subst:
   115:   (int * btypecode_t) list ->
   116:   btypecode_t ->
   117:   btypecode_t
   118: 
   119: (** make a varmap using vs and ts list *)
   120: val mk_varmap:
   121:   (string * int) list -> (* vs list *)
   122:   btypecode_t list ->  (* ts list *)
   123:   (int,btypecode_t) Hashtbl.t
   124: 
   125: (** replace variables using vs and ts list to
   126: determine mapping *)
   127: val tsubst :
   128:   (string * int) list -> (* vs list *)
   129:   btypecode_t list ->  (* ts list *)
   130:   btypecode_t ->
   131:   btypecode_t
   132: 
   133: (** replace variables in the term using
   134: the mapping in the hashtable
   135: *)
   136: val varmap_subst:
   137:   (int,btypecode_t) Hashtbl.t ->
   138:   btypecode_t ->
   139:   btypecode_t
   140: 
   141: (** check for variables *)
   142: val var_occurs:
   143:   btypecode_t ->
   144:   bool
   145: 
   146: (** check for a particular variable *)
   147: val var_i_occurs:
   148:   int ->
   149:   btypecode_t ->
   150:   bool
   151: 
   152: (** check for variables *)
   153: val var_list_occurs:
   154:   int list ->
   155:   btypecode_t ->
   156:   bool
   157: 
   158: (** normalise returns count of the type variables
   159:   occuring in a type, and the type rewritten so the type variables
   160:   are systematically numbered from 0 - n-1
   161: *)
   162: val normalise_type:
   163:   btypecode_t -> int list * btypecode_t
   164: 
   165: (** check for bad recursions *)
   166: val check_recursion:
   167:   btypecode_t -> unit
   168: 
   169: (** construct the dual of a type *)
   170: val dual:
   171:   btypecode_t -> btypecode_t
   172: 
   173: val expr_maybe_matches:
   174:   symbol_table_t -> (* just for diagnostics *)
   175:   int list -> (* type variables *)
   176:   int list -> (* variables *)
   177:   tbexpr_t -> (* match term *)
   178:   tbexpr_t   (* candidate *)
   179:   ->
   180:   (
   181:     (int * btypecode_t) list * (* type mgu *)
   182:     (int * tbexpr_t) list      (* expr mgu *)
   183:   )
   184:   option
   185: 
   186: val expr_term_subst:
   187:   tbexpr_t -> (* candidate *)
   188:   int ->      (* variable index *)
   189:   tbexpr_t -> (* variable value *)
   190:   tbexpr_t    (* candidate with index -> value *)
   191: 
End ocaml section to src/flx_unify.mli[1]
Start ocaml section to src/flx_unify.ml[1 /1 ]
     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: 
End ocaml section to src/flx_unify.ml[1]