Get at least one fixpoint right: any = fix 0.

src/compiler/flx_bind/flx_bind_bexe.ml

@@ -137,6 +137,7 @@ let cal_call state bsym_table sr ((be1,t1) as tbe1) ((_,t2) as tbe2) =
       end
     end
   in
+  let t1 = Flx_beta.beta_reduce "Flx_bind_bexe:cal_call" state.counter bsym_table sr t1 in
   match unfold "flx_bind_bexe" t1 with
 
   (* special handling of non-returning function. Instead of returning

src/compiler/flx_bind/flx_bind_symbol.ml

@@ -451,6 +451,7 @@ print_endline ("join: binding return type");
 *)
     (* We don't need to bind the intermediary type. *)
     let brt = bt' rt in
+    let brt = Flx_beta.beta_reduce "Flx_bind_symbol:bexes" state.counter bsym_table sym.Flx_sym.sr brt in 
 (*
 if sym.Flx_sym.id = "join" then 
 print_endline ("join: bound return type");

src/compiler/flx_bind/flx_overload.ml

@@ -133,9 +133,9 @@ if name = debugid then
   let curry_domains = spec_domain :: curry_domains in
 
   if name = debugid then begin
-    print_endline ("Argument  sigs= " ^  catmap "->" (sbt bsym_table) arg_types);
-    print_endline ("spec_result = " ^  catmap "->" (sbt bsym_table) curry_domains);
-    print_endline ("Candidate sigs= " ^  catmap "->" (sbt bsym_table) curry_domains);
+    print_endline ("Argument  sigs= " ^  catmap ", " (sbt bsym_table) arg_types);
+    print_endline ("spec_result = " ^  catmap ", " (sbt bsym_table) curry_domains);
+    print_endline ("Candidate sigs= " ^  catmap ", " (sbt bsym_table) curry_domains);
   end;
 
   (* equations for user specified assignments *)
@@ -145,7 +145,7 @@ if name = debugid then
 
   if name = debugid then begin
     print_endline "TS EQUATIONS ARE:";
-    List.iter (fun (t1,t2) -> print_endline (sbt bsym_table t1 ^ " = " ^ sbt bsym_table t2))
+    List.iter (fun (t1,t2) -> print_endline (Flx_btype.st t1 ^ " = " ^ Flx_btype.st t2))
     eqns
   end;
 
@@ -187,12 +187,9 @@ if name = debugid then begin
   List.iter (fun (t1,t2) -> print_endline (sbt bsym_table t1 ^ " = " ^ sbt bsym_table t2))
   eqns
 end;
-  (* WRONG!! dunno why, but it is! *)
-(*
+if name = debugid then 
   print_endline ("DEPENDENT VARIABLES ARE " ^ catmap "," si
-    (BidSet.fold (fun i l-> i::l) !dvars []));
-  print_endline "...";
-*)
+    (BidSet.elements !dvars));
 (*
 if name = debugid then print_endline "Trying unification";
 *)
@@ -322,7 +319,7 @@ print_endline ("Scanning type variable " ^ s ^ "<" ^ si j' ^ ">: " ^ str_of_kind
         (* this is not really right, kinds do act as constraints *)
         match tp with
         | KND_tpattern t -> 
-(* if id = debugid then *)
+if id = debugid then
 print_endline (" .. found tpattern .. analysing .. " ^ string_of_typecode t);
           type_of_tpattern counter t
         | KND_generic (* overload treats this as a type variable in this routine *)
@@ -717,10 +714,7 @@ let consider
 : overload_result option =
   (* Helper function to simplify the bind type function. *)
   let bt sr t = bt sr entry_kind.base_sym t in
-
-(*
-if name = debugid then print_endline ("Considering .." ^ name);
-*)
+if name = debugid then print_endline ("Considering .." ^ name ^ "<" ^ string_of_int entry_kind.base_sym ^ ">");
   let id, sr, base_vs, parent_vs, con, domain, base_result, arg_types =
     Flx_resolve.resolve sym_table bsym_table entry_kind.base_sym bt be arg_types 
   in
@@ -745,19 +739,18 @@ if name = debugid then print_endline ("Resolve done for " ^ name);
   end
   ;
   *)
-(*
+if name = debugid then 
   print_endline ("CONSIDER: " ^ id ^ "|-> " ^string_of_myentry bsym_table entry_kind);
-*)
-(*
+if name = debugid then 
   begin
-    print_endline ("PARENT VS=" ^ catmap "," (fun (s,i,mt)->s^"<"^si i^">:" ^ string_of_typecode mt) parent_vs);
-    print_endline ("base VS=" ^ catmap "," (fun (s,i,mt)->s^"<"^si i^">" ^ string_of_typecode mt) base_vs);
+    print_endline ("PARENT VS=" ^ catmap "," (fun (s,i,mt)->s^"<"^si i^">:" ^ str_of_kindcode mt) parent_vs);
+    print_endline ("base VS=" ^ catmap "," (fun (s,i,mt)->s^"<"^si i^">" ^ str_of_kindcode mt) base_vs);
     print_endline ("sub TS=" ^ catmap "," (sbt bsym_table) entry_kind.sub_ts);
-    print_endline ("spec VS=" ^ catmap "," (fun (s,i)->s^"<"^si i^">") entry_kind.spec_vs);
+    print_endline ("spec VS=" ^ catmap "," (fun (s,i, k)->s^"<"^si i^":"^Flx_kind.sk k ^">") entry_kind.spec_vs);
     print_endline ("input TS=" ^ catmap "," (sbt bsym_table) input_ts);
   end
   ;
-*)
+
   (* these are wrong .. ? or is it just shitty table?
      or is the mismatch due to unresolved variables? *)
   if (List.length base_vs != List.length entry_kind.sub_ts) then begin
@@ -830,15 +823,22 @@ if name = "accumulate" then print_endline "Considering function .. ";
       clierrx "[flx_bind/flx_overload.ml:1028: E250] " sr ("Failed to bind candidate return type! fn='" ^ name ^
         "', type=" ^ sbt bsym_table base_result)
   in
+if name = debugid then 
+  print_endline ("Spec result input to make_equations " ^ sbt bsym_table spec_result);
+
   let spec_result = beta_reduce "flx_overload: consider(1) " counter bsym_table sr spec_result in
+if name = debugid then 
+  print_endline ("Spec result input to make_equations post beta " ^ sbt bsym_table spec_result);
 
   let spec_domain = 
     specialize_domain sr base_vs entry_kind.sub_ts domain
   in
-  let spec_domain = beta_reduce "flx_overload: consider(2) " counter bsym_table sr spec_domain in
-(*
+if name = debugid then 
   print_endline ("Spec domain input to make_equations " ^ sbt bsym_table spec_domain);
-*)
+
+  let spec_domain = beta_reduce "flx_overload: consider(2) " counter bsym_table sr spec_domain in
+if name = debugid then 
+  print_endline ("Spec domain input to make_equations post beta " ^ sbt bsym_table spec_domain);
 
 (*
 if name = debugid then 
@@ -926,6 +926,7 @@ if name = debugid then
         let r = match con with | `TYP_tuple [] -> bbool true | _ -> bt rs call_sr ix con in
 *)
         let r = bt rs call_sr ix con in
+        let r = Flx_beta.beta_reduce "Flx_overload:overload':env_traint" counter bsym_table call_sr r in
         r
       ) 
       env

src/compiler/flx_bind/flx_tconstraint.ml

@@ -41,7 +41,7 @@ print_endline ("Build type constraints for type variable " ^string_of_int i ^":
   | KND_function _ 
   | KND_tuple _ -> bbool true
 
-  | KND_tpattern p1 -> assert false; (* I don't think this is used anymore *)
+  | KND_tpattern p1 -> 
   begin
   (* special case, no constraint, represent by just 'true' (unit type) *)
   match p1 with
@@ -114,7 +114,9 @@ print_endline ("Build type constraints for type variable " ^string_of_int i ^":
   | t -> [t]
   in
   let tyset ls =
+(*
 print_endline ("Generating type match for typeset " ^ Flx_util.catmap ", " Flx_btype.st ls);
+*)
     let e = BidSet.empty in
     let un = bbool true in
     let lss = rev_map (fun t -> {pattern=t; pattern_vars=e; assignments=[]},un) ls in

src/compiler/flx_core/flx_beta.ml

@@ -224,7 +224,7 @@ and beta_reduce calltag counter bsym_table sr t1 =
 *)
   let t2 =
   try
-  beta_reduce' calltag counter bsym_table sr [] t1
+  beta_reduce' calltag counter bsym_table sr 0 [] t1
   with exn -> t1
 (*
     | Not_found ->
@@ -238,19 +238,20 @@ print_endline ("Beta reduce failed with Failure");
       raise exn
   
   in
+*)
+  in 
 (*
   print_endline ("============" ^ calltag^ "   reduced= " ^ sbt bsym_table t2 ^ "=" ^ Flx_btype.st t2);
 *)
-*)
-  in t2
+  t2
 
-and type_list_index counter bsym_table ls t =
+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 n = match ls with
+  let rec aux ls = match ls with
   | [] -> None
-  | hd :: tl ->
+  | (hd, depth) :: tl ->
     (*
     print_endline ("Candidate : " ^ sbt bsym_table hd);
     *)
@@ -260,11 +261,14 @@ and type_list_index counter bsym_table ls t =
         print_endline ("Exception: " ^ Printexc.to_string x);
         false
       end
-    then Some n
-    else aux tl (n+1)
-  in aux ls 0
+    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 termlist t =
+and beta_reduce' calltag counter bsym_table sr depth (termlist: (Flx_btype.t * int) list) t =
 let spc = "  *** " in
 (*
   print_endline ("BETA REDUCE' " ^ sbt bsym_table t ^ " trail length = " ^
@@ -283,7 +287,7 @@ let spc = "  *** " in
 *)
   if List.length termlist > 200
   then begin
-    print_endline ("Trail=" ^ catmap "\n" (sbt bsym_table) termlist);
+    print_endline ("Trail=" ^ catmap "\n" (fun (t,depth) -> string_of_int depth ^ ": " ^sbt bsym_table t) termlist);
     failwith  ("Trail overflow, infinite expansion: BETA REDUCE " ^
     sbt bsym_table t ^ "\ntrail length = " ^ si (List.length termlist))
   end;
@@ -302,39 +306,31 @@ let spc = "  *** " in
 print_endline ("Flx_beta: beta-reduce: hacking metatype of fixpoint, type is " ^ sbt bsym_table t);
 print_endline ("Flx_beta: kind is " ^ sk mt);
 *)
-    let fp = btyp_fix (-j - 1) mt  in
-(*
+    let fp = btyp_fix (j-depth) mt  in
 print_endline ("Beta-reduce: type list index found term in trail, returning fixpoint " ^ sbt bsym_table fp);
-*)
     fp
 
   | None ->
 (*
 print_endline "Type list index returned None";
 *)
-  let br t' = beta_reduce' calltag counter bsym_table sr (t::termlist) t' in
+  let br t' = beta_reduce' calltag counter bsym_table sr (depth+1) termlist t' in
   let st t = sbt bsym_table t in
   match t with
   (* STAND ALONE TYPEDEF *)
   | BTYP_inst (`Alias, index,ts,mt) -> 
     let ts = List.map br ts in
     begin try 
       let bsym = Flx_bsym_table.find bsym_table index in
+      if bsym.Flx_bsym.id = "any" then print_endline ("Beta reduce any!");
+
       let bbdcl = Flx_bsym.bbdcl bsym in
       begin match bbdcl with
       | Flx_bbdcl.BBDCL_structural_type_alias (bvs, alias) 
       | Flx_bbdcl.BBDCL_nominal_type_alias (bvs, alias) ->
-(*
-print_endline ("Found typedef " ^ Flx_bsym.id bsym ^ "<"^string_of_int index^"> alias=" ^ Flx_btype.st alias);
-print_endline ("bvs/tvs= " ^ catmap ", " (fun ((s,i), t) -> s^"<" ^ string_of_int i ^ "> <-- " ^ Flx_btype.st t) (List.combine bvs ts));
-*)
-       let salias = Flx_btype_subst.tsubst sr bvs ts alias in
-       (* NOTE: the reference is NOT put on the trail because this would upset the depth count *)
-       beta_reduce' calltag counter bsym_table sr termlist alias
-(*
-print_endline ("typedef " ^ Flx_bsym.id bsym ^ " after substitution =" ^ Flx_btype.st alias);
-*)
-
+       let alias = Flx_btype_subst.tsubst sr bvs ts alias in
+       let alias = beta_reduce' calltag counter bsym_table sr  depth ((t,depth)::termlist) alias in
+       alias 
       | _ ->  
 (*
 print_endline ("Found non-typedef" ^ Flx_bsym.id bsym ^ "<" ^ string_of_int k ^ ">");
@@ -527,7 +523,7 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
 
   | 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
+    Flx_type_fun.type_apply br beta_reduce' calltag counter bsym_table sr depth termlist t t1 t2
 
   | BTYP_type_match (tt,pts) ->
   begin

src/compiler/flx_core/flx_print.ml

@@ -2955,7 +2955,7 @@ let full_string_of_entry_kind sym_table bsym_table {base_sym=i; spec_vs=vs; sub_
       with Not_found -> failwith ("full_string_of_entry_kind: Help, can't find index " ^ string_of_int
       i ^ " in sym table")
   in
-  string_of_symdef sym.Flx_sym.symdef sym.Flx_sym.id sym.Flx_sym.vs ^
+  string_of_int i ^ ": " ^ string_of_symdef sym.Flx_sym.symdef sym.Flx_sym.id sym.Flx_sym.vs ^
   "\n  defined at " ^ Flx_srcref.short_string_of_src sym.Flx_sym.sr ^ "\n  with view" ^
   " vs=" ^ string_of_bvs vs ^
   " ts=" ^ catmap "," (sbt bsym_table) ts

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 termlist t f arg = 
+let rec type_apply br beta_reduce' calltag counter bsym_table sr depth (termlist: (Flx_btype.t * int) list) t 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 termlist t f ar
             alias
           end
         in 
-        type_apply br beta_reduce' calltag counter bsym_table sr termlist t f arg
+        type_apply br beta_reduce' calltag counter bsym_table sr depth termlist t 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 termlist t f ar
        | 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 termlist t alias arg
+         type_apply br beta_reduce' calltag counter bsym_table sr depth termlist t alias arg
        | _ ->  assert false
        end
      with Not_found -> 
@@ -93,8 +93,7 @@ let rec type_apply br beta_reduce' calltag counter bsym_table sr termlist t f ar
         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 (t::termlist) t' in
-    let t' = adjust bsym_table t' in
+    let t' = beta_reduce' calltag counter bsym_table sr (depth-2) termlist t' in
     t'
 
   | _ ->