Migrating to Monomorphised LLBC

Makefile

@@ -57,7 +57,7 @@ clean-and-test:
 .PRECIOUS: %.llbc
 %.llbc: %.rs .charon_version
 	# --mir elaborated --add-drop-bounds 
-	$(CHARON) rustc --preset=eurydice --dest-file "$@" $(CHARON_EXTRA) -- $<
+	$(CHARON) rustc --monomorphize --preset=eurydice --dest-file "$@" $(CHARON_EXTRA) -- $<
 
 out/test-%/main.c: test/main.c
 	mkdir -p out/test-$*
@@ -73,7 +73,7 @@ test/issue_105.llbc: CHARON_EXTRA = \
   --include=core::cmp::* \
   --include=core::convert::*
 
-test/array2d.llbc: CHARON_EXTRA = --include=core::array::equality::*
+# test/array2d.llbc: CHARON_EXTRA = --include=core::array::equality::*
 
 test/core_num.llbc: CHARON_EXTRA = \
   --include=core::num::*::BITS \
@@ -83,6 +83,9 @@ test/println.llbc: CHARON_EXTRA = \
   --include=core::fmt::Arguments --include=core::fmt::rt::*::new_const \
   --include=core::fmt::rt::Argument
 
+# test-where_clauses_closures: CHARON_EXTRA = \
+# 	--include=core::convert::*
+
 test/option.llbc: CHARON_EXTRA = \
   --include=core::option::*
 

bin/main.ml

@@ -235,8 +235,9 @@ Supported options:|}
   (* Must happen now, before Monomorphization.datatypes, because otherwise
      MonomorphizationState.state gets filled with lids that later on get eliminated on the basis
      that they were empty structs to begin with, which would send Checker off the rails *)
-  let files = Krml.DataTypes.remove_empty_structs files in
+  let files = Eurydice.Cleanup2.remove_empty_structs files in
   let files = Krml.Monomorphization.datatypes files in
+  let files = Eurydice.Cleanup2.drop_unused_type files in
   (* Cannot use remove_unit_buffers as it is technically incorrect *)
   let files = Krml.DataTypes.remove_unit_fields#visit_files () files in
   Eurydice.Logging.log "Phase2.13" "%a" pfiles files;
@@ -264,7 +265,7 @@ Supported options:|}
   let errors, files = Krml.Checker.check_everything ~warn:true files in
   if errors then
     fail __FILE__ __LINE__;
-  let files = Krml.Inlining.drop_unused files in
+  (*let files = Krml.Inlining.drop_unused files in*)
   let files = Eurydice.Cleanup2.remove_array_temporaries#visit_files () files in
   Eurydice.Logging.log "Phase2.25" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_array_repeats#visit_files false files in
@@ -289,7 +290,7 @@ Supported options:|}
   let files = Eurydice.Cleanup2.remove_array_from_fn files in
   Eurydice.Logging.log "Phase2.6" "%a" pfiles files;
   (* remove_array_from_fn, above, creates further opportunities for removing unused functions. *)
-  let files = Krml.Inlining.drop_unused files in
+  (* let files = Krml.Inlining.drop_unused files in *)
   let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files () files in
   (* Creates opportunities for removing unused variables *)
   let files = Eurydice.Cleanup2.remove_assign_return#visit_files () files in
@@ -312,6 +313,8 @@ Supported options:|}
   let files = Eurydice.Cleanup2.float_comments files in
   Eurydice.Logging.log "Phase2.95" "%a" pfiles files;
   let files = Eurydice.Cleanup2.bonus_cleanups#visit_files [] files in
+  let files = Krml.Inlining.drop_unused files in
+  let files = Eurydice.Cleanup2.drop_unused_monoed_func files in
   (* Macros stemming from globals -- FIXME why is this not Krml.AstToCStar.mk_macros_set? *)
   let files, macros = Eurydice.Cleanup2.build_macros files in
 

cremepat/cremepat.ml

@@ -157,13 +157,16 @@ let compile_parse_tree (env : env) loc
         (* EApp (ETApp (e, ts), es) *)
         ppat_cons_many ~loc "EApp"
           [
-            ppat_cons_many ~loc "ETApp"
-              [
-                compile env head;
-                compile_expr_list_pattern env cgs;
-                compile_expr_list_pattern env methods;
-                compile_typ_list_pattern env ts;
-              ];
+            (if cgs = [] && methods = [] && ts = [] then
+               compile env head
+             else
+               ppat_cons_many ~loc "ETApp"
+                 [
+                   compile env head;
+                   compile_expr_list_pattern env cgs;
+                   compile_expr_list_pattern env methods;
+                   compile_typ_list_pattern env ts;
+                 ]);
             ppat_list ~loc (List.map (compile env) args);
           ]
     | Addr e -> ppat_cons_one ~loc "EAddrOf" (compile env e)

include/eurydice_glue.h

@@ -132,6 +132,9 @@ typedef struct {
                  end) /* x is already at an array type, no need for cast */
 #define Eurydice_array_to_subslice(_arraylen, x, r, t, _0, _1)                 \
   EURYDICE_SLICE((t *)x, r.start, r.end)
+// The mono version is exactly the same, just with a different name
+#define Eurydice_array_to_subslice_mono(_arraylen, x, r, t, _0, _1)            \
+  EURYDICE_SLICE((t *)x, r.start, r.end)
 
 // Same as above, variant for when start and end are statically known
 #define Eurydice_array_to_subslice3(x, start, end, t_ptr)                      \
@@ -146,6 +149,11 @@ typedef struct {
   EURYDICE_SLICE((t *)x, 0, r)
 #define Eurydice_array_to_subslice_from(size, x, r, t, _range_t, _0)           \
   EURYDICE_SLICE((t *)x, r, size)
+// The mono versions are exactly the same, just different names
+#define Eurydice_array_to_subslice_to_mono(_size, x, r, t, _range_t, _0)       \
+  EURYDICE_SLICE((t *)x, 0, r)
+#define Eurydice_array_to_subslice_from_mono(size, x, r, t, _range_t, _0)      \
+  EURYDICE_SLICE((t *)x, r, size)
 
 // Copy a slice with memcopy
 #define Eurydice_slice_copy(dst, src, t)                                       \
@@ -329,6 +337,17 @@ core_convert_num__core__convert__From_u16__for_usize__from(uint16_t x) {
   return x;
 }
 
+// for monoed where-clauses_simple
+static inline uint64_t
+core_convert_num__core__convert__From___u64__u16___from(uint16_t x) {
+  return x;
+}
+
+static inline size_t
+core_convert_num__core__convert__From___usize__u16___from(uint16_t x) {
+  return x;
+}
+
 static inline uint32_t core_num__u8__count_ones(uint8_t x0) {
 #ifdef _MSC_VER
   return __popcnt(x0);
@@ -549,6 +568,7 @@ typedef const char *Prims_string;
 // This is temporary. Ultimately we want to be able to extract all of this.
 
 typedef void *core_fmt_Formatter;
+typedef void *core_fmt_Formatter_____;
 #define core_fmt_rt__core__fmt__rt__Argument__a___new_display(x1, x2, x3, x4)  \
   NULL