Merge pull request #32 from AeneasVerif/son_arrays

Add support for arrays/slices and const generics

1 files changed, 12 insertions, 6 deletions

diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index 9ba73c7e..ba5e237b 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -32,33 +32,39 @@ type pure_fun_translation = fun_and_loops * fun_and_loops list
 
 let type_decl_to_string (ctx : trans_ctx) (def : Pure.type_decl) : string =
   let type_params = def.type_params in
+  let cg_params = def.const_generic_params in
   let type_decls = ctx.type_context.type_decls in
-  let fmt = PrintPure.mk_type_formatter type_decls type_params in
+  let global_decls = ctx.global_context.global_decls in
+  let fmt =
+    PrintPure.mk_type_formatter type_decls global_decls type_params cg_params
+  in
   PrintPure.type_decl_to_string fmt def
 
-let type_id_to_string (ctx : trans_ctx) (def : Pure.type_decl) : string =
-  let type_params = def.type_params in
-  let type_decls = ctx.type_context.type_decls in
-  let fmt = PrintPure.mk_type_formatter type_decls type_params in
-  PrintPure.type_decl_to_string fmt def
+let type_id_to_string (ctx : trans_ctx) (id : Pure.TypeDeclId.id) : string =
+  Print.fun_name_to_string
+    (Pure.TypeDeclId.Map.find id ctx.type_context.type_decls).name
 
 let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
   let type_params = sg.type_params in
+  let cg_params = sg.const_generic_params in
   let type_decls = ctx.type_context.type_decls in
   let fun_decls = ctx.fun_context.fun_decls in
   let global_decls = ctx.global_context.global_decls in
   let fmt =
     PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
+      cg_params
   in
   PrintPure.fun_sig_to_string fmt sg
 
 let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
   let type_params = def.signature.type_params in
+  let cg_params = def.signature.const_generic_params in
   let type_decls = ctx.type_context.type_decls in
   let fun_decls = ctx.fun_context.fun_decls in
   let global_decls = ctx.global_context.global_decls in
   let fmt =
     PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
+      cg_params
   in
   PrintPure.fun_decl_to_string fmt def