Various missing cases in checker, monomorphization, and fixing a type…

… error in removing struct literals

lib/AstToCStar.ml

@@ -803,7 +803,7 @@ and mk_return_type env = function
   | TAnonymous t ->
       mk_type_def env t
   | TCgArray _ ->
-      fatal_error "Internal failure: TCgArray not desugared here"
+      CStar.Qualified (["Eurydice"], "error_t_cg_array")
   | TCgApp _ ->
       fatal_error "Internal failure: TCgApp not desugared here"
 

lib/Checker.ml

@@ -161,7 +161,10 @@ let rec check_everything ?warn files: bool * file list =
 and check_program env r (name, decls) =
   let env = locate env (File name) in
   let by_lid = Hashtbl.create 41 in
-  let decls = KList.filter_map (fun d ->
+  let total = List.length decls in
+  let decls = KList.filter_mapi (fun i d ->
+    if Options.debug "checker" then
+      KPrint.bprintf "CHECKER PROGRESS: %d/%d\n" (i + 1) total;
     try
       check_decl env d;
       Some d
@@ -1123,12 +1126,24 @@ and subtype env t1 t2 =
   | TAnonymous (Flat [ Some f, (t, _) ]), TAnonymous (Union ts) ->
       List.exists (fun (f', t') -> f = f' && subtype env t t') ts
 
+  | TTuple ts, _ when Hashtbl.mem MonomorphizationState.state (tuple_lid, ts, []) ->
+      subtype env (TQualified (snd (Hashtbl.find MonomorphizationState.state (tuple_lid, ts, [])))) t2
+
+  | _, TTuple ts when Hashtbl.mem MonomorphizationState.state (tuple_lid, ts, []) ->
+      subtype env t1 (TQualified (snd (Hashtbl.find MonomorphizationState.state (tuple_lid, ts, []))))
+
   | TApp (lid, ts), _ when Hashtbl.mem MonomorphizationState.state (lid, ts, []) ->
       subtype env (TQualified (snd (Hashtbl.find MonomorphizationState.state (lid, ts, [])))) t2
 
   | _, TApp (lid, ts) when Hashtbl.mem MonomorphizationState.state (lid, ts, []) ->
       subtype env t1 (TQualified (snd (Hashtbl.find MonomorphizationState.state (lid, ts, []))))
 
+  | TCgApp _, _ when Hashtbl.mem MonomorphizationState.state (flatten_tapp t1) ->
+      subtype env (TQualified (snd (Hashtbl.find MonomorphizationState.state (flatten_tapp t1)))) t2
+
+  | _, TCgApp _ when Hashtbl.mem MonomorphizationState.state (flatten_tapp t2) ->
+      subtype env t1 (TQualified (snd (Hashtbl.find MonomorphizationState.state (flatten_tapp t2))))
+
   | _ ->
       false
 

lib/DeBruijn.ml

@@ -250,7 +250,7 @@ let open_branch bs pat expr =
 
 class map_counting_cg = object
   (* The environment [i] has type [int*int]. *)
-  inherit [_] map
+  inherit [_] map as super
   (* The environment is a pair [i, i']. The first component [i] is the DeBruijn
     index we are looking for, after entering ONLY the cg binders. It it set by
     the caller and does not increase afterwards since the only cg binders are at
@@ -259,6 +259,9 @@ class map_counting_cg = object
     at each binder, in expressions. *)
   method! extend ((i: int), i') (_: binder) =
     i, i' + 1
+
+  method! visit_ETApp ((i, i'), env) e cgs ts =
+    super#visit_ETApp ((i + List.length cgs, i'), env) e cgs ts
 end
 
 (* Converting an expression into a suitable const generic usable in types, knowing
@@ -297,8 +300,8 @@ class subst_ct (c: cg) = object (self)
         else
           TCgArray (t, if j < i then j else j-1)
 
-  method! visit_TCgApp (i as env) t arg =
-    let t = self#visit_typ env t in
+  method! visit_TCgApp i t arg =
+    let t = self#visit_typ i t in
     (* We are seeking to replace i with c in TCgApp (t, arg) *)
     match arg with
     | CgVar j ->

lib/Helpers.ml

@@ -185,7 +185,7 @@ let fold_arrow ts t_ret =
    rather than a hardcoded list in krml *)
 let is_aligned_type = function ["Lib"; "IntVector"; "Intrinsics"], ("vec128"|"vec256"|"vec512") -> true | _ -> false
 
-let is_array = function TArray _ -> true | _ -> false
+let is_array = function TCgArray _ | TArray _ -> true | _ -> false
 
 let is_union = function TAnonymous (Union _) -> true | _ -> false
 

lib/Monomorphization.ml

@@ -59,7 +59,34 @@ let build_def_map files =
 
 include MonomorphizationState
 
-let has_variables = List.exists (function TBound _ -> assert !Options.allow_tapps; true | _ -> false)
+let has_variables ts=
+  let r =
+    (object
+      inherit [_] reduce
+      method zero = false
+      method plus = (||)
+      method! visit_TBound _ _ =
+        true
+    end)#visit_TApp () ([], "") ts
+  in
+  if r then
+    assert !Options.allow_tapps;
+  r
+
+let has_cg_array ts =
+  let r =
+    (object
+      inherit [_] reduce
+      method zero = false
+      method plus = (||)
+      method! visit_TCgArray _ _ _ =
+        true
+    end)#visit_TApp () ([], "") ts
+  in
+  if r then
+    assert !Options.allow_tapps;
+  r
+
 let has_cg_variables = List.exists (function CgVar _ -> assert !Options.allow_tapps; true | _ -> false)
 
 let monomorphize_data_types map = object(self)
@@ -177,6 +204,7 @@ let monomorphize_data_types map = object(self)
           let subst fields = List.map (fun (field, (t, m)) ->
             field, (DeBruijn.subst_ctn' cgs (DeBruijn.subst_tn args t), m)
           ) fields in
+          assert (not (Hashtbl.mem map lid) || not (has_variables args) && not (has_cg_variables cgs));
           begin match Hashtbl.find map lid with
           | exception Not_found ->
               (* Unknown, external non-polymorphic lid, e.g. Prims.int *)
@@ -348,13 +376,16 @@ let monomorphize_data_types map = object(self)
     PRecord (List.mapi (fun i p -> self#field_at i, self#visit_pattern under_ref p) pats)
 
   method! visit_TTuple under_ref ts =
-    TQualified (self#visit_node under_ref (tuple_lid, ts, []))
+    if not (has_variables ts) && not (has_cg_array ts) then
+      TQualified (self#visit_node under_ref (tuple_lid, ts, []))
+    else
+      super#visit_TTuple under_ref ts
 
   method! visit_TQualified under_ref lid =
     TQualified (self#visit_node under_ref (lid, [], []))
 
   method! visit_TApp under_ref lid ts =
-    if Hashtbl.mem map lid && not (has_variables ts) then
+    if Hashtbl.mem map lid && not (has_variables ts) && not (has_cg_array ts) then
       TQualified (self#visit_node under_ref (lid, ts, []))
     else
       super#visit_TApp under_ref lid ts

lib/PrintAst.ml

@@ -302,7 +302,7 @@ and print_expr { node; typ } =
       braces_with_nesting (print_expr e4)
   | EBufCreateL (l, es) ->
       print_lifetime l ^/^
-      string "newbuf" ^/^ braces_with_nesting (separate_map (comma ^^ break1) print_expr es)
+      string "newbuf" ^/^ braces_with_nesting (flow (comma ^^ break1) (List.map print_expr es))
   | ECons (ident, es) ->
       string ident ^/^
       if List.length es > 0 then

lib/PrintCommon.ml

@@ -78,8 +78,11 @@ let print_cc = function
   | StdCall -> string "__stdcall"
   | FastCall -> string "__fastcall"
 
+let xstring s =
+  string (String.concat "␣" (KString.split_on_char ' ' s))
+
 let print_lident (idents, ident) =
-  separate_map dot string (idents @ [ ident ])
+  separate_map dot xstring (idents @ [ ident ])
 
 let print_program p decls =
   separate_map (hardline ^^ hardline) p decls

lib/Structs.ml

@@ -741,19 +741,19 @@ let to_addr is_struct =
 let remove_literals = object (self)
   inherit [_] map as super
 
-  method private mk_path (e: expr) (t: typ) (fields: ident list) =
-    List.fold_left (fun acc f -> with_type t (EField (acc, f))) e fields
+  method private mk_path (e: expr) (fields: (ident * typ) list) =
+    List.fold_left (fun acc (f, t) -> with_type t (EField (acc, f))) e fields
 
-  method private explode (acc: expr list) (path: ident list) (e: expr) (dst: expr) =
+  method private explode (acc: expr list) (path: (ident * typ) list) (e: expr) (dst: expr): expr list =
     match e.node with
     | EFlat fields ->
         List.fold_left (fun acc (f, e) ->
           let f = Option.must f in
-          self#explode acc (f :: path) e dst
+          self#explode acc ((f, e.typ) :: path) e dst
         ) acc fields
     | _ ->
         let e = self#visit_expr_w () e in
-        with_type TUnit (EAssign (self#mk_path dst e.typ (List.rev path), e)) :: acc
+        with_type TUnit (EAssign (self#mk_path dst (List.rev path), e)) :: acc
 
   method! visit_ELet ((_, t) as env) b e1 e2 =
     match e1.node with