Rewrite alpha conversion.

src/compiler/flx_bind/flx_bind_bexe.ml

@@ -747,7 +747,11 @@ print_endline ("Flx_bind_bexe: UNIFICATION DONE, result= " ^ string_of_bool ures
           index
           parent_ts
       in
+
+      let lhst = Flx_beta.beta_reduce "Flx_bind_bexe:iinit.lhst" state.counter bsym_table sr lhst in
+      let rhst = Flx_beta.beta_reduce "Flx_bind_bexe:iinit.rhst" state.counter bsym_table sr rhst in
       let rhst = Flx_fold.minimise bsym_table state.counter rhst in
+
       if type_match bsym_table state.counter lhst rhst
       then begin 
             let bexe = bexe_init (sr,index,(e',rhst)) in

src/compiler/flx_core/flx_alpha.ml

@@ -0,0 +1,59 @@
+open Flx_btype
+open Flx_exceptions
+open Flx_bid
+
+let remap map i = try List.assoc i map with Not_found -> i
+
+let rec alpha counter map t = 
+  match t with
+  | BTYP_type_var (i, knd) -> 
+    btyp_type_var (remap map i, knd)
+
+  | BTYP_type_function (ps,r,b) ->
+    let map = List.fold_left (fun acc (i,_) -> (i, fresh_bid counter)::acc) map ps in
+    let ps = List.map (fun (i,k) -> remap map i, k) ps in
+    let b = alpha counter map b in
+    btyp_type_function (ps, r, b)
+
+  | BTYP_type_match (arg, pss) ->
+    let arg = alpha counter map arg in
+    let pss = 
+      List.map (fun ({pattern=p; assignments=a; pattern_vars=dvars},handler) ->
+        (* variables to remap are the pattern variables and assignments *)
+        let map = BidSet.fold (fun i acc -> (i, fresh_bid counter)::acc) dvars map in
+        let map = List.fold_left  (fun acc (i,_) -> (i, fresh_bid counter)::acc) map a in
+
+        let p = alpha counter map p in
+        let dvars = BidSet.map (remap map) dvars in
+        let a = List.map (fun (i,t) -> remap map i, alpha counter map t) a in
+        {pattern=p; assignments=a; pattern_vars=dvars}, alpha counter map handler
+      ) 
+      pss
+    in 
+    btyp_type_match (arg,pss)
+
+  | BTYP_subtype_match (arg, pss) ->
+    let arg = alpha counter map arg in
+    let pss = 
+      List.map (fun ({pattern=p; assignments=a; pattern_vars=dvars},handler) ->
+        (* variables to remap are the pattern variables and assignments *)
+        let map = BidSet.fold (fun i acc -> (i, fresh_bid counter)::acc) dvars map in
+        let map = List.fold_left  (fun acc (i,_) -> (i, fresh_bid counter)::acc) map a in
+
+        let p = alpha counter map p in
+        let dvars = BidSet.map (remap map) dvars in
+        let a = List.map (fun (i,t) -> remap map i, alpha counter map t) a in
+        {pattern=p; assignments=a; pattern_vars=dvars}, alpha counter map handler
+      ) 
+      pss
+    in 
+    btyp_subtype_match (arg,pss)
+
+
+  | t -> Flx_btype.map ~f_btype:(alpha counter map) t
+
+
+
+let alpha_convert counter t = alpha counter [] t
+
+

src/compiler/flx_core/flx_alpha.mli

@@ -0,0 +1,3 @@
+
+val alpha_convert: int ref -> Flx_btype.t -> Flx_btype.t
+

src/compiler/flx_core/flx_beta.ml

@@ -224,6 +224,7 @@ and type_list_index counter bsym_table ls t =
   in aux ls 0
 
 and beta_reduce' calltag counter bsym_table sr termlist t =
+let spc = "  *** " in
 (*
   print_endline ("BETA REDUCE' " ^ sbt bsym_table t ^ " trail length = " ^
     si (List.length termlist));
@@ -457,7 +458,10 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
   (* can't reduce *)
   | BTYP_type_map (t1,t2) -> btyp_type_map (br t1, br t2)
 
-  | BTYP_type_apply (t1,t2) -> Flx_type_fun.type_apply br beta_reduce' calltag counter bsym_table sr termlist t t1 t2
+  | BTYP_type_apply (t1,t2) -> 
+    let t1 = Flx_alpha.alpha_convert counter t1 in
+    Flx_type_fun.type_apply br beta_reduce' calltag counter bsym_table sr termlist t t1 t2
+
   | BTYP_type_match (tt,pts) ->
   begin
 (*
@@ -466,10 +470,7 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
     let tt = br tt in
     let new_matches = ref [] in
     List.iter (fun ({pattern=p; pattern_vars=dvars; assignments=eqns}, t') ->
-      (*
-      print_endline (spc ^"Tring to unify argument with " ^
-        sbt bsym_table p');
-      *)
+      (* print_endline (spc ^"Tring to unify argument with " ^ sbt bsym_table p); *)
       let p =  br p in
       let x =
         {
@@ -479,38 +480,39 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
         }, t'
       in
       match maybe_unification bsym_table counter [p,tt] with
-      | Some _ -> new_matches := x :: !new_matches
+      | Some _ -> 
+        (* print_endline (spc ^"Argument unifies with  " ^ sbt bsym_table p); *)
+        new_matches := x :: !new_matches
       | None ->
-        (*
-        print_endline (spc ^"Discarding pattern " ^ sbt bsym_table p');
-        *)
+        (* print_endline (spc ^"Discarding pattern " ^ sbt bsym_table p); *)
         ()
     )
     pts
     ;
     let pts = List.rev !new_matches in
+(* print_endline (spc ^ "Found " ^ string_of_int (List.length pts) ^ " unifies"); *)
     match pts with
     | [] ->
-      (*
       print_endline ("[beta-reduce] typematch failure " ^ sbt bsym_table t);
-      *)
       t 
 
     | ({pattern=p';pattern_vars=dvars;assignments=eqns},t') :: _ ->
       try
+        (* print_endline (spc ^ "Redo unification now setting dependent vars"); *)
+        (* print_endline ( spc ^ "Dvars = { " ^ catmap ", " si (Flx_bid.BidSet.elements dvars) ^ "}"); *)
         let mgu = unification bsym_table counter [p', tt] dvars in
-        (*
-        print_endline "Typematch success";
-        *)
+        (* print_endline (spc ^ "Typematch success"); *)
         let t' = list_subst counter (mgu @ eqns) t' in
         let t' = br t' in
-        (*
-        print_endline ("type match reduction result=" ^ sbt bsym_table t');
-        *)
+        (* print_endline ("type match reduction result=" ^ sbt bsym_table t'); *)
         adjust bsym_table t'
-      with Not_found -> btyp_type_match (tt,pts)
+      with 
+       | Not_found ->
+         (* print_endline ("Match failed to reduce redex, return original term"); *)
+         btyp_type_match (tt,pts)
 
   end
+
   | BTYP_subtype_match (tt,pts) ->
   begin
 (*

src/compiler/flx_core/flx_btype.ml

@@ -35,7 +35,7 @@ let str_of_instkind = function
 type btpattern_t = {
   pattern: t;
 
-  (* pattern type variables, including 'any' vars *)
+  (* pattern type variables, including 'any' vars, these are the dependent variables to use in unification *)
   pattern_vars: BidSet.t;
 
   (* assignments for 'as' vars *)
@@ -1091,9 +1091,9 @@ let rec map ?(f_bid=fun i -> i) ?(f_btype=fun t -> t) ?(f_kind=fun k->k) = funct
         List.map begin fun (tp, t) ->
           { tp with
             pattern = f_btype tp.pattern;
-            assignments = List.map
-              (fun (i, t) -> f_bid i, f_btype t)
-              tp.assignments },
+            pattern_vars = BidSet.map f_bid tp.pattern_vars;
+            assignments = List.map (fun (i, t) -> f_bid i, f_btype t) tp.assignments
+          },
           f_btype t
         end ps
       in

src/compiler/flx_core/flx_btype_subst.ml

@@ -14,39 +14,6 @@ let var_subst t (i, j) =
 
 let vars_subst ls t = List.fold_left var_subst t ls
 
-(* NOTE: BUG perhaps .. this ONLY converts function parameters! *)
-let rec alpha counter t =
-  match t with
-  | BTYP_type_function (ps,r,b) ->
-      let remap_list = List.map (fun (i,_) -> i, fresh_bid counter) ps in
-      let remap i = List.assoc i remap_list in
-      let cvt t = alpha counter (vars_subst remap_list t) in
-      let ps = List.map (fun (i,t) -> remap i,t) ps in
-      btyp_type_function (ps, r, cvt b)
-  | t -> Flx_btype.map ~f_btype:(alpha counter) t
-
-let alpha_convert counter t =
-  let t = alpha counter t in (* convert function parameters first *)
-  let remap_list = ref [] in
-  let remap i = 
-    try List.assoc i !remap_list
-    with Not_found ->
-      let j = fresh_bid counter in
-      remap_list := (i,j) :: !remap_list;
-      j
-  in
-  let rec aux t = match t with
-  | BTYP_type_function (ps,r,b) ->
-    (* now leave function parameters alone, they're bound and already converted *)
-    List.iter (fun (i,_) -> remap_list := (i,i) :: !remap_list) ps; 
-    btyp_type_function (ps, r, aux b)
-
-  | BTYP_type_var (i,mt) -> btyp_type_var (remap i, mt)
-
-  | t -> Flx_btype.map ~f_btype:aux t
-  in aux t
-
-
 let term_subst counter src i arg =
   let rec aux level t =
     match t with
@@ -70,12 +37,9 @@ let term_subst counter src i arg =
   in
   aux 0 src 
 
-let list_subst counter x t =
-  let t = alpha counter t in
-  List.fold_left (fun t1 (i,t2) ->
-    term_subst counter t1 i (alpha counter t2))
-  t
-  x
+let list_subst counter ls t =
+  let t = Flx_alpha.alpha_convert counter t in
+  List.fold_left (fun t1 (i,t2) -> term_subst counter t1 i t2) t ls
 
 let varmap0_subst varmap t =
   let rec f_btype t =

src/compiler/flx_core/flx_unify.ml

@@ -728,7 +728,7 @@ let str_of_cmp = function
 | `Greater-> " > "
 
 let compare_sigs bsym_table counter a b =
-  let b = Flx_btype_subst.alpha_convert counter b in (* alpha convert one of the terms *)
+  let b = Flx_alpha.alpha_convert counter b in (* alpha convert one of the terms *)
   let ab = ge bsym_table counter a b in
   let ba =  ge bsym_table counter b a in
   let result = match ab,ba with