Only one fail now and that's due to some remaining issues with typesets.

src/compiler/flx_bind/flx_bind_bexe.ml

@@ -862,13 +862,13 @@ print_endline ("assign after beta-reduction: RHST = " ^ sbt bsym_table rhst);
         let bexe = bexe_assign (sr,lhs_index,bexpr_coerce (rx, lhst)) in
         [bexe]
       else
-      clierrx "[flx_bind/flx_bind_bexe.ml:867: E36] " sr
+      clierrx "[flx_bind/flx_bind_bexe.ml:865: E36] " sr
       (
         "[bind_exe: assign ] Assignment "^
           sbe bsym_table lx^"="^
           sbe bsym_table rx^";\n"^
         "LHS type: " ^ sbt bsym_table lhst^
-        "\nmust have be super type of\n"^
+        "\nmust be super type of\n"^
         "RHS type: " ^ sbt bsym_table rhst ^
         record_field_diag bsym_table lhst rhst
       )

src/compiler/flx_core/flx_beta.ml

@@ -245,31 +245,6 @@ print_endline ("Beta reduce failed with Failure");
 *)
   t2
 
-and type_list_index counter bsym_table (ls: (Flx_btype.t * int) list) t =
-  (*
-  print_endline ("Comparing : " ^ sbt bsym_table t ^ " with ..");
-  *)
-  let rec aux ls = match ls with
-  | [] -> None
-  | (hd, depth) :: tl ->
-    (*
-    print_endline ("Candidate : " ^ sbt bsym_table hd);
-    *)
-    if
-      begin try type_eq bsym_table counter hd t
-      with x ->
-        print_endline ("Exception: " ^ Printexc.to_string x);
-        false
-      end
-    then begin 
-(*
-      print_endline ("Type list index found term " ^ Flx_btype.st hd ^ " in trail depth " ^ string_of_int depth);
-*)
-      Some depth
-    end
-    else aux tl 
-  in aux ls 
-
 and beta_reduce' calltag counter bsym_table sr depth (termlist: (Flx_btype.t * int) list) t =
 let spc = "  *** " in
 (*
@@ -295,7 +270,7 @@ let spc = "  *** " in
   end;
   let tli = 
     try 
-      type_list_index counter bsym_table termlist t 
+      Flx_type_list_index.type_list_index counter bsym_table termlist t 
     with exc -> 
       print_endline ("type list index function failed  " ^ Printexc.to_string exc);
       assert false
@@ -323,7 +298,7 @@ print_endline "Type list index returned None";
   match t with
   (* STAND ALONE TYPEDEF *)
   | BTYP_inst (`Alias, index,ts,mt) -> 
-    let ts = List.map br ts in
+    (* let ts = List.map br ts in *)
     begin try 
       let bsym = Flx_bsym_table.find bsym_table index in
 (*
@@ -527,8 +502,11 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
   | BTYP_type_map (t1,t2) -> btyp_type_map (br t1, br 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 depth termlist t t1 t2
+    (* 
+      (* NOTE: suspect because trail comparison would be screwed up! *)
+    let t1 = Flx_alpha.alpha_convert counter t1 in 
+    *)
+    Flx_type_fun.type_apply beta_reduce' calltag counter bsym_table sr depth termlist t1 t2
 
   | BTYP_type_match (tt,pts) ->
   begin
@@ -571,9 +549,7 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
         let mgu = unification bsym_table counter [p', tt] dvars in
         (* 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'); *)
-        adjust bsym_table t'
+        beta_reduce' calltag counter bsym_table sr depth termlist t'
       with 
        | Not_found ->
          (* print_endline ("Match failed to reduce redex, return original term"); *)
@@ -589,10 +565,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 =
         {
@@ -627,11 +600,7 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
         print_endline "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');
-        *)
-        adjust bsym_table t'
+        beta_reduce' calltag counter bsym_table sr depth termlist t'
       | None -> btyp_subtype_match (tt,pts)
       end
   end

src/compiler/flx_core/flx_type_fun.ml

@@ -12,7 +12,7 @@ open Flx_kind
 
 let adjust bsym_table t = Flx_btype_rec.adjust_fixpoint t
 
-let rec type_apply br beta_reduce' calltag counter bsym_table sr depth (termlist: (Flx_btype.t * int) list) t f arg = 
+let rec type_apply beta_reduce' calltag counter bsym_table sr depth (termlist: (Flx_btype.t * int) list) f arg = 
   match f with 
   | BTYP_finst (index, ks, dom, cod) ->
     begin try
@@ -50,7 +50,7 @@ let rec type_apply br beta_reduce' calltag counter bsym_table sr depth (termlist
             alias
           end
         in 
-        type_apply br beta_reduce' calltag counter bsym_table sr depth termlist t f arg
+        type_apply beta_reduce' calltag counter bsym_table sr depth termlist f arg
       | _ ->
         print_endline ("Expexted finst to refer to type function");
         assert false
@@ -68,7 +68,7 @@ let rec type_apply br beta_reduce' calltag counter bsym_table sr depth (termlist
        | Flx_bbdcl.BBDCL_structural_type_alias (bvs, alias) 
        | Flx_bbdcl.BBDCL_nominal_type_alias (bvs, alias) ->
          let salias = Flx_btype_subst.tsubst sr bvs ts alias in
-         type_apply br beta_reduce' calltag counter bsym_table sr depth termlist t alias arg
+         type_apply beta_reduce' calltag counter bsym_table sr depth termlist alias arg
        | _ ->  assert false
        end
      with Not_found -> 
@@ -77,24 +77,53 @@ let rec type_apply br beta_reduce' calltag counter bsym_table sr depth (termlist
      end
 
   | BTYP_type_function (ps,r,body) ->
-    let params' =
-      match ps with
-      | [] -> []
-      | [i,_] -> [i,arg]
-      | _ ->
-        let ts = match br arg with
-        | BTYP_type_tuple ts -> ts
-        | _ -> 
-          print_endline ("Expected Argument  to type function to be type tuple, got " ^ Flx_print.sbt bsym_table arg);
-          assert false
-        in
-        if List.length ps <> List.length ts
-        then failwith "Wrong number of arguments to typefun"
-        else List.map2 (fun (i,_) t -> i, t) ps ts
-    in
-    let t' = list_subst counter params' body in
-    let t' = beta_reduce' calltag counter bsym_table sr (depth-2) termlist t' in
-    t'
+    (* Fixpoint handling here *)
+    let appl = Flx_btype.btyp_type_apply (f, arg) in
+    begin match Flx_type_list_index.type_list_index counter bsym_table termlist appl with
+    | Some j -> 
+      let t = btyp_fix (j-depth) r in
+(*
+print_endline ("Flx_type_fun: installing fixpoint " ^ Flx_btype.st t);
+*)
+      t
+    | None -> 
+(* NOTE: the typefun term MUST be alpha converted here so the substitution does not lead to false captures in NESTED
+typefun terms. Note, there cannot be a capture of any of the current paraneters because they're all being replaced,
+and the replacement does not rescan the replacement. However the body of the type function can contain another
+type term and we are substituting "under the lambda" and the replacement may contain a free variable that is
+a parameter of THAT nested lambda.
+
+Unfortunately this means the trail comparison must use alpha equivalance, not equality of the term encoding.
+
+NOTE: alpha equiv is easy, we alph convert both terms using the SAME initial counter then 
+do normal comparison .. but I think maybe the type equality routine should do this.
+*)
+      let f = Flx_alpha.alpha_convert counter f in
+      match f with 
+      | BTYP_type_function (ps,r,body) ->
+      let params' =
+        match ps with
+        | [] -> []
+        | [i,_] -> [i,arg]
+        | _ ->
+          let ts = match (* beta_reduce' "Flx_type_fun:argment" counter bsym_table sr (depth+1) termlist *) arg with
+          | BTYP_type_tuple ts -> ts
+          | _ -> 
+            print_endline ("Expected Argument  to type function to be type tuple, got " ^ Flx_print.sbt bsym_table arg);
+            assert false
+          in
+          if List.length ps <> List.length ts
+          then failwith "Wrong number of arguments to typefun"
+          else List.map2 (fun (i,_) t -> i, t) ps ts
+      in
+      let t' = list_subst counter params' body in
+(*
+print_endline ("Flx_type_fun: calling beta trailing " ^ Flx_btype.st appl ^ " depth=" ^ string_of_int depth);
+*)
+      let t' = beta_reduce' calltag counter bsym_table sr depth ((appl,depth)::termlist) t' in
+      t'
+    | _ -> assert false
+    end
 
   | _ ->
     let t = btyp_type_apply (f,arg) in

src/compiler/flx_core/flx_type_list_index.ml

@@ -0,0 +1,26 @@
+let type_list_index counter bsym_table (ls: (Flx_btype.t * int) list) t =
+  (*
+  print_endline ("Comparing : " ^ sbt bsym_table t ^ " with ..");
+  *)
+  let rec aux ls = match ls with
+  | [] -> None
+  | (hd, depth) :: tl ->
+    (*
+    print_endline ("Candidate : " ^ sbt bsym_table hd);
+    *)
+    if
+      begin try Flx_unify.type_eq bsym_table counter hd t
+      with x ->
+        print_endline ("Exception: " ^ Printexc.to_string x);
+        false
+      end
+    then begin 
+(*
+      print_endline ("Type list index found term " ^ Flx_btype.st hd ^ " in trail depth " ^ string_of_int depth);
+*)
+      Some depth
+    end
+    else aux tl 
+  in aux ls 
+
+