Good progress

bin/main.ml

@@ -127,6 +127,12 @@ Supported options:|}
       let missing = Eurydice.RuntimeCg.enumerate_cg_monomorphizations files in
       Eurydice.RuntimeCg.debug missing;
       Krml.MonomorphizationState.debug ();
+      let extra_file = [ Eurydice.RuntimeCg.build_missing_decls missing ] in
+      let extra_file = List.hd (Krml.Monomorphization.datatypes extra_file) in
+      let files, last_file = Krml.KList.split_at_last files in
+      let files = files @ [ fst last_file, snd last_file @ snd extra_file ] in
+      let files = Eurydice.RuntimeCg.replace#visit_files () files in
+      Eurydice.Logging.log "Phase2.6" "%a" pfiles files;
       files
     else
       files

lib/RuntimeCg.ml

@@ -8,7 +8,10 @@ module H = Krml.Helpers
 (* In some cases, we wish to disable const-generic monomorphization to e.g.
    avoid code-size bloat. For the moment, this is a global switch, but in the
    future, one could conceivably use an attribute, or a pass a list of functions
-   that should opt-out of monomorphization via the command-line. *)
+   that should opt-out of monomorphization via the command-line.
+
+   The first step consists in turning monomorphizing calls (ETApps) into regular
+   function calls, so as to avoid those functions getting cg-specialized. *)
 let disable_cg_monomorphization = object(self)
   inherit [_] map as super
 
@@ -35,9 +38,17 @@ let disable_cg_monomorphization = object(self)
 end
 
 
-(* But for types, we *do* need to monomorphize them still. For that, we
-   symbolically traverse the function-call and type declaration graph and, for
-   each cg-monomorphization found, record it and insert it into the files. *)
+(* But for types, we *do* need to monomorphize them still. Base types like
+   uint8_t[$0] (using $ to signify "cg var") can be suitably handled all
+   throughout and stack-allocated with VLAs. But for data type declarations
+   (which, of course, abound), there is no such mechanism, so we need to do
+   something.
+
+   The strategy is to traverse, symbolically, the function-call graph, and
+   for each cg-monomorphization found, record it. Concretely, if there is a call
+   to f::<32>() and the body of f mentions `[u32; N] * [u32; N]`, we record
+   `[u32; 32] * [u32; 32]` as an extra monomorphization that *will* be needed
+   to support the runtime execution of that cg code. *)
 let enumerate_cg_monomorphizations files =
   let map = H.build_map files (fun map -> function
     | DFunction (cc, flags, n_cgs, n, t, name, b, body) ->
@@ -96,8 +107,8 @@ let enumerate_cg_monomorphizations files =
       | _ ->
           ()
 
-    (* Completely substitute types and cgs in the callee's body. About just as
-       expensive as monomorphization. *)
+    (* Completely substitute types and cgs in the callee's body. Not sure how
+       much more expensive this is than monomorphization. *)
     method! visit_EApp _ e es =
       (* This is an EApp not an ETApp because the earlier phase just removed
          those! *)
@@ -120,9 +131,12 @@ let enumerate_cg_monomorphizations files =
                   (* Krml.KPrint.bprintf "After subst: %a\n" Krml.PrintAst.Ops.pexpr body; *)
                   self#visit_expr_w () body
 
-(*                   let ret = Krml.DeBruijn.subst_ctn 0 (1* all closed terms *1) cgs (Krml.DeBruijn.subst_tn ts ret) in *)
-(*                   Krml.KPrint.bprintf "After subst: %a\n" Krml.PrintAst.Ops.ptyp ret; *)
-(*                   self#visit_typ () ret *)
+                  (* These should be visited as part of the body... we are
+                     talking about parameters and return expressions, unless
+                     some parameters are unused...? *)
+                  (* let ret = Krml.DeBruijn.subst_ctn 0 (* all closed terms *) cgs (Krml.DeBruijn.subst_tn ts ret) in
+                  Krml.KPrint.bprintf "After subst: %a\n" Krml.PrintAst.Ops.ptyp ret;
+                  self#visit_typ () ret *)
                 end
             | _ ->
                 ()
@@ -154,6 +168,8 @@ let enumerate_cg_monomorphizations files =
      too. *)
   known_concrete_arguments
 
+(* It helps to compare this with what's already caught by regular
+   monomorphization. *)
 let debug missing =
   Krml.KPrint.bprintf "DEBUG RUNTIME MONOMORPHIZATION:\n";
   Hashtbl.iter (fun lid args ->
@@ -165,12 +181,104 @@ let debug missing =
     ) args
   ) missing
 
+(* So once we've captured the missing instances of monomorphization that aren't
+   otherwise reached with regular, non-cg functions, we gather them in a
+   separate file to be fed separately to data type monomorphization. *)
+let build_missing_decls missing =
+  let i = ref 0 in
+  "", Hashtbl.fold (fun lid args acc ->
+    List.fold_left (fun acc (ts, cgs) ->
+      let abbrev_lid = [], "special" ^ string_of_int !i in
+      incr i;
+      DType (abbrev_lid, [ Krml.Common.AutoGenerated ], 0, 0, Abbrev (fold_tapp (lid, ts, cgs))) :: acc
+    ) acc args
+  ) missing []
+
+(* Now these things have been monomorphized, and have a corresponding lid
+   allocated and recorded in MonomorphizationState. This is where it gets
+   interesting... because I didn't carry explicit substitutions, I now have to
+   do something equivalent where for each syntactic form of type that *still*
+   has const generics in it, I try to figure out which monomorphized types could
+   possibly, at run-time, be one of the corresponding candidates. *)
+let replace =
+  let rec matches_t t1 t2 =
+    let r =
+      match t1, t2 with
+      | TTuple ts1, TTuple ts2 ->
+          List.for_all2 matches_t ts1 ts2
+      | TApp (t1, ts1), TApp (t2, ts2) ->
+          t1 = t2 && List.for_all2 matches_t ts1 ts2
+      | TCgArray (t1, cg1), TCgArray (t2, cg2) ->
+          matches_t t1 t2 && cg1 = cg2
+      | TArray (t1, _), TCgArray (t2, _) ->
+          (* TODO: compute mappings and check they coincide *)
+          matches_t t1 t2
+      | TCgApp (t1, cg1), TCgApp (t2, cg2) ->
+          matches_t t1 t2 && matches_cg cg1 cg2
+      | TApp _, TCgApp _ ->
+          let t1, ts1, cgs1 = flatten_tapp t1 in
+          let t2, ts2, cgs2 = flatten_tapp t2 in
+          t1 = t2 && List.for_all2 matches_t ts1 ts2 && List.for_all2 matches_cg cgs1 cgs2
+      | t1, t2 ->
+          t1 = t2
+    in
+    Krml.(let open PrintAst.Ops in KPrint.bprintf "  MATCH: %a | %a ? %b\n" ptyp t1 ptyp t2 r);
+    r
+
+  and matches_cg cg1 cg2 =
+    match cg1, cg2 with
+    | _, CgVar _ -> true
+    | CgConst c1, CgConst c2 -> c1 = c2
+    | _ -> false
+  in
+
+  let replace t ts cgs =
+    let builtin = match List.hd (fst t) with "Eurydice" | "core" -> true | _ -> false in
+    if not builtin then begin
+      Krml.(let open PrintAst.Ops in KPrint.bprintf "REPLACE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs);
+      (* let candidates = Hashtbl.find missing t in *)
+      (* Pull ALL the candidates from monomorphization *)
+      let candidates = Hashtbl.fold (fun (lid, ts, cgs) (_, mono_lid) acc ->
+        if lid = t then (ts, cgs, mono_lid) :: acc else acc
+      ) Krml.MonomorphizationState.state [] in
+      (* Keep those that match *)
+      let candidates = List.filter (fun (ts', cgs', _) ->
+        List.for_all2 matches_t ts' ts && List.for_all2 matches_cg cgs' cgs
+      ) candidates in
+      match candidates with
+      | [] -> fold_tapp (t, ts, cgs)
+      | [ ts', cgs', lid ] ->
+          Krml.(let open PrintAst.Ops in KPrint.bprintf "  FOUND: %a: %a ++ %a\n" plid t ptyps ts' pcgs cgs');
+          Krml.(let open PrintAst.Ops in KPrint.bprintf "  AKA: %a\n" plid lid);
+          TQualified lid
+      | _ ->
+          List.iter (fun (ts, cgs, _) ->
+            Krml.(let open PrintAst.Ops in KPrint.bprintf "  CANDIDATE: %a: %a ++ %a\n" plid t ptyps ts pcgs cgs)
+          ) candidates;
+          failwith "TODO: multiple candidates, need to be subtler"
+    end else
+      fold_tapp (t, ts, cgs)
+  in
+  object(_self)
+    inherit [_] map
+
+    method! visit_TCgApp () t cg =
+      let lid, ts, cgs = flatten_tapp (TCgApp (t, cg)) in
+      replace lid ts cgs
+
+    method! visit_TApp _ t ts =
+      let lid, ts, cgs = flatten_tapp (TApp (t, ts)) in
+      replace lid ts cgs
+
+    method! visit_TTuple _ ts =
+      replace tuple_lid ts []
+  end
 
-(* The previous phase left n_cgs in place over DFunctions so that
-   remove_implicit_array_copies could convert length arguments of TCgArray's to
-   runtime expressions, in order to implement blit operations to materialize
-   array copies. We now remove those, and manually decay TCgArrays into TBufs,
-   relying on Checker to validate this pass. *)
+(* This happens much later. The previous phases left n_cgs in place over
+   DFunctions so that remove_implicit_array_copies could convert length
+   arguments of TCgArray's to runtime expressions, in order to implement blit
+   operations to materialize array copies. We now remove those, and manually
+   decay TCgArrays into TBufs, relying on Checker to validate this pass. *)
 let erase_and_decay_cgs = object(self)
   inherit Krml.DeBruijn.map_counting_cg as super