From 0f0e4be7dc746e2676db33f850bbeddf239eaec8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 13 Oct 2023 00:40:37 +0200
Subject: Add sup

---
 compiler/Assumed.ml               | 15 +++++++++++++++
 compiler/Driver.ml                |  2 ++
 compiler/Extract.ml               |  4 +++-
 compiler/InterpreterStatements.ml |  2 +-
 compiler/PrintPure.ml             |  1 +
 compiler/PureMicroPasses.ml       |  2 +-
 6 files changed, 23 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index e156c335..109175af 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -298,6 +298,19 @@ module Sig = struct
   let array_subslice_sig (is_mut : bool) =
     mk_array_slice_subslice_sig true is_mut
 
+  let array_repeat_sig =
+    let generics =
+      (* <T, N> *)
+      mk_generic_params [] [ type_param_0 ] [ cg_param_0 ]
+    in
+    let regions_hierarchy = [] (* <> *) in
+    let inputs = [ tvar_0 (* T *) ] in
+    let output =
+      (* [T; N] *)
+      mk_array_ty tvar_0 cgvar_0
+    in
+    mk_sig generics regions_hierarchy inputs output
+
   let slice_subslice_sig (is_mut : bool) =
     mk_array_slice_subslice_sig false is_mut
 
@@ -384,6 +397,8 @@ let assumed_infos : assumed_info list =
       Sig.array_subslice_sig true,
       true,
       to_name [ "@ArraySubsliceMut" ] );
+    (* Array Repeat *)
+    (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ]);
     (* Slice Index *)
     ( SliceIndexShared,
       Sig.slice_index_sig false,
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 0fde1d74..8a30ead9 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -24,6 +24,8 @@ let _ =
   main_log#set_level EL.Info;
   llbc_of_json_logger#set_level EL.Info;
   pre_passes_log#set_level EL.Info;
+  associated_types_log#set_level EL.Info;
+  contexts_log#set_level EL.Info;
   interpreter_log#set_level EL.Info;
   statements_log#set_level EL.Info;
   loops_match_ctxs_log#set_level EL.Info;
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index ce423acf..99ea14a4 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -338,6 +338,7 @@ let assumed_llbc_functions () :
         (ArraySubsliceShared, None, "array_subslice_shared");
         (ArraySubsliceMut, None, "array_subslice_mut_fwd");
         (ArraySubsliceMut, rg0, "array_subslice_mut_back");
+        (ArrayRepeat, None, "array_repeat");
         (SliceIndexShared, None, "slice_index_shared");
         (SliceIndexMut, None, "slice_index_mut_fwd");
         (SliceIndexMut, rg0, "slice_index_mut_back");
@@ -369,6 +370,7 @@ let assumed_llbc_functions () :
         (ArraySubsliceShared, None, "Array.subslice_shared");
         (ArraySubsliceMut, None, "Array.subslice_mut");
         (ArraySubsliceMut, rg0, "Array.subslice_mut_back");
+        (ArrayRepeat, None, "Array.repeat");
         (SliceIndexShared, None, "Slice.index_shared");
         (SliceIndexMut, None, "Slice.index_mut");
         (SliceIndexMut, rg0, "Slice.index_mut_back");
@@ -3212,7 +3214,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_open_hvbox fmt ctx.indent_incr;
         let need_paren = inside in
         if need_paren then F.pp_print_string fmt "(";
-        (* Open the box for `Array.mk T N [` *)
+        (* Open the box for `Array.replicate T N [` *)
         F.pp_open_hovbox fmt ctx.indent_incr;
         (* Print the array constructor *)
         let cs = ctx_get_struct false (Assumed Array) ctx in
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 42073f0b..36bc3492 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -646,7 +646,7 @@ let eval_assumed_function_call_concrete (config : C.config)
               eval_vec_function_concrete config fid generics
           | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
           | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut
-          | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
+          | ArrayRepeat | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
           | SliceSubsliceMut | SliceLen ->
               raise (Failure "Unimplemented")
         in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index d539dcf6..5fb5978b 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -610,6 +610,7 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
   | ArrayToSliceMut -> "@ArrayToSliceMut"
   | ArraySubsliceShared -> "@ArraySubsliceShared"
   | ArraySubsliceMut -> "@ArraySubsliceMut"
+  | ArrayRepeat -> "@ArrayRepeat"
   | SliceLen -> "@SliceLen"
   | SliceIndexShared -> "@SliceIndexShared"
   | SliceIndexMut -> "@SliceIndexMut"
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 2130d5c2..cedc3559 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1563,7 +1563,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     | ArraySubsliceMut | SliceIndexShared | SliceIndexMut
                     | SliceSubsliceShared | SliceSubsliceMut | ArrayIndexShared
                     | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
-                    | SliceLen ),
+                    | ArrayRepeat | SliceLen ),
                     _ ) ->
                     super#visit_texpression env e)
             | _ -> super#visit_texpression env e)
-- 
cgit v1.2.3