Fiddle with the kinding system.

Two cases still fail due to not beta-reducing. Not sure why, it's possible the fixpoint term has the wrong numerical index.
felix-lang · May 14, 2022 · 3825795 · 3825795
1 parent 4fb47d3
commit 3825795
Show file tree

Hide file tree

Showing 6 changed files with 37 additions and 11 deletions.
diff --git a/src/compiler/flx_bind/flx_bind_bexe.ml b/src/compiler/flx_bind/flx_bind_bexe.ml
@@ -787,7 +787,8 @@ print_endline ("Flx_bind_bexe: UNIFICATION DONE, result= " ^ string_of_bool ures
           parent_ts
       in
 (* NOTE: this shoud already be done.... *)
-      let lhst = Flx_beta.beta_reduce "flx_bind_bexe: EXE_init" state.counter bsym_table sr lhst in
+      let lhst = Flx_beta.beta_reduce "flx_bind_bexe: EXE_init:lhs" state.counter bsym_table sr lhst in
+      let rhst = Flx_beta.beta_reduce "flx_bind_bexe: EXE_init:rhs" state.counter bsym_table sr rhst in
 (*
 print_endline ("Beta reduced LHS is not actually reduced: " ^ sbt bsym_table lhst);
 *)

diff --git a/src/compiler/flx_bind/flx_bind_type.ml b/src/compiler/flx_bind/flx_bind_type.ml
@@ -357,7 +357,7 @@ print_endline ("Flx_bind_type `TYP_var " ^ string_of_int i);
 (*
 print_endline ("FUDGE: Binding `TYP_var " ^ si i ^ ", HACKING KIND TO TYPE");
 *)
-      btyp_type_var (i, Flx_kind.KIND_linear)
+      btyp_type_var (i, Flx_kind.KIND_var "AnyKind")
     end
 
   | `TYP_as (t,s) ->

diff --git a/src/compiler/flx_bind/flx_cal_ret_type.ml b/src/compiler/flx_bind/flx_cal_ret_type.ml
@@ -38,7 +38,7 @@ let cal_ret_type'
   | { Flx_sym.id=id;
       sr=sr;
       dirs=dirs;
-      symdef=SYMDEF_function ((ps,_),rt,effects,props,exes)
+      symdef=SYMDEF_function ((ps,_),rt',effects,props,exes)
     } ->
 (*
 print_endline ("+++++++++++++++++++++++++++++");
@@ -47,7 +47,19 @@ print_endline ("+++++ UNBOUND return type is " ^ string_of_typecode rt);
     begin match rt with | `TYP_var j when j = index -> print_endline ("RETURN TYPE UNSPECIFIED") | _ -> () end;
 print_endline ("Trying to bind type .. if function index variable, we get a recurse?");
 *)
-    let rt = bind_type' state bsym_table env rs sr rt args mkenv in
+    let declared_ret = not (index = (match rt' with `TYP_var k -> k | _ -> 0)) in
+
+    let rt = 
+      if declared_ret then
+        bind_type' state bsym_table env rs sr rt' args mkenv
+      else
+       (* since we don't know the kind of the type we have to use a kind variable,
+          unfortunately unification checks but does not return a kind mgu and
+          so the kind is lost
+       *)
+       let kv = Flx_kind.kind_var "Dummy" in 
+       btyp_type_var (index, kv) 
+    in
 (*
 print_endline ("Type bound; " ^ sbt bsym_table rt);
 *)
@@ -133,13 +145,16 @@ print_endline ("Calling bind_epression'");
         in
         let t = beta_reduce "flx_lookup: cal_ret_type, return expr type" state.counter bsym_table sr t in
 (*
+print_endline ("Return expression type = " ^ Flx_btype.st t);
+*)
+(*
 print_endline "Flx_lookup: about to check calculated and registered return type";
 print_endline ("Return type = " ^ Flx_btype.st !ret_type);
 print_endline ("Return expression type = " ^ Flx_btype.st t);
 *)
         if pvtype then
           () (* use the declared return type, let the coercion be inserted later *) 
-        else
+        else 
         begin 
           let result = Flx_do_unify.do_unify
              state.counter
@@ -170,9 +185,10 @@ print_endline ("Return expression type = " ^ Flx_btype.st t);
             (
               "[cal_ret_type2] Inconsistent return type of " ^ id ^ "<" ^
               string_of_bid index ^ ">" ^
-              "\nDeclared Return type       : " ^ str_of_btype rt ^ "\n  = " ^ sbt bsym_table rt ^
-              "\nProgressive infered type   : " ^ str_of_btype !ret_type ^ "\n  = " ^ sbt bsym_table !ret_type ^
-              "\nType of Return Instruction : " ^ str_of_btype t ^ "\n  = " ^ sbt bsym_table t
+              "\nDeclared Unbound Return type : " ^ Flx_print.string_of_typecode rt' ^
+              "\nDeclared Return type         : " ^ str_of_btype rt ^ "\n  = " ^ sbt bsym_table rt ^
+              "\nProgressive infered type     : " ^ str_of_btype !ret_type ^ "\n  = " ^ sbt bsym_table !ret_type ^
+              "\nType of Return Argument      : " ^ str_of_btype t ^ "\n  = " ^ sbt bsym_table t
             )
           end
        end

diff --git a/src/compiler/flx_bind/flx_guess_meta_type.ml b/src/compiler/flx_bind/flx_guess_meta_type.ml
@@ -174,8 +174,9 @@ let guess_meta_type state bsym_table bt index : kind =
     match entry with
     | SYMDEF_instance_type t
     | SYMDEF_type_function (_,t)  -> 
-      print_endline ("Guess meta type of type function...");
-      guess_metatype sr t
+      let k = guess_metatype sr t in
+      print_endline ("Guess meta type of type function... " ^ Flx_kind.sk k);
+      k
 
     | SYMDEF_type_alias t  -> 
       guess_metatype sr t

diff --git a/src/compiler/flx_core/flx_print.ml b/src/compiler/flx_core/flx_print.ml
@@ -458,7 +458,7 @@ and st prec tc : string =
       ^
       "\nendmatch"
 
-    | `TYP_var i -> 0,"<var " ^ string_of_bid i ^ ">"
+    | `TYP_var i -> 0,"<typevar " ^ string_of_bid i ^ ">"
     | `TYP_unitsum k ->
       0,
       begin match k with

diff --git a/src/compiler/flx_core/flx_unify.ml b/src/compiler/flx_core/flx_unify.ml
@@ -229,6 +229,14 @@ and solve_subsumption nominal_subtype counter lhs rhs  dvars (s:vassign_t option
         add_eqn (t1,t2)
 
 
+(* NOTE: This case allows SUBKINDING! This should NOT be allowed in
+   the subsumption routine .. it should only be allowed in the
+   subtyping routine .. but it isn't in there so we need to preserve
+   this code for the moment
+
+   In fact we need to extra the kind level MGU and return that
+   too ......
+*)
       | (BTYP_type_var (i,mi) as ti), (BTYP_type_var (j,mj) as tj)->
         (* meta type have to agree *)
         if i <> j then