Make progress on implementing support for types and functions like

Option and Vec

8 files changed, 74 insertions, 30 deletions

diff --git a/src/Assumed.ml b/src/Assumed.ml
index 97cd2c78..5a9fb51b 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -245,6 +245,9 @@ let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list =
     (VecIndexMut, Sig.vec_index_mut_sig);
   ]
 
+let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig =
+  snd (List.find (fun (id', _) -> id = id') assumed_sigs)
+
 let assumed_names : (A.assumed_fun_id * Identifiers.name) list =
   [
     (Replace, [ "core"; "mem"; "replace" ]);
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 636c68d3..db09b316 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -284,6 +284,8 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
                 (* The "pair" case is frequent enough to have its special treatment *)
                 if List.length tys = 2 then "p" else "t"
             | Assumed Result -> "r"
+            | Assumed Option -> "opt"
+            | Assumed Vec -> "v"
             | AdtId adt_id ->
                 let def =
                   TypeDefId.Map.find adt_id ctx.type_context.type_defs
@@ -719,7 +721,7 @@ let extract_place (ctx : extraction_ctx) (fmt : F.formatter) (p : place) : unit
         let def_id =
           match pe.pkind with
           | E.ProjAdt (def_id, None) -> def_id
-          | E.ProjAdt (_, Some _) | E.ProjTuple _ ->
+          | E.ProjAdt (_, Some _) | E.ProjOption _ | E.ProjTuple _ ->
               (* We can't have field accesses on enumerations (variables for
                * the fields are introduced upon the moment we match over the
                * enumeration). We also forbid field access on tuples, because
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index c926c63a..375f3dec 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -9,6 +9,7 @@ open TypesUtils
 open ValuesUtils
 module Inv = Invariants
 module S = SynthesizeSymbolic
+open Errors
 open Cps
 open InterpreterUtils
 open InterpreterProjectors
@@ -350,9 +351,10 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
   comp cf_pop cf_assign
 
 (** Auxiliary function - see [eval_non_local_function_call] *)
-let eval_replace_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
- fun cf ctx -> raise Unimplemented
+let eval_replace_concrete (_config : C.config)
+    (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun
+    =
+ fun _cf _ctx -> raise Unimplemented
 
 (** Auxiliary function - see [eval_non_local_function_call] *)
 let eval_box_new_concrete (config : C.config)
@@ -492,9 +494,10 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
   | _ -> failwith "Inconsistent state"
 
 (** Auxiliary function - see [eval_non_local_function_call] *)
-let eval_vec_function_concrete (config : C.config) (fid : A.assumed_fun id)
-    (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
- fun cf ctx -> raise Unimplemented
+let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
+    (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun
+    =
+ fun _cf _ctx -> raise Unimplemented
 
 (** Evaluate a non-local function call in concrete mode *)
 let eval_non_local_function_call_concrete (config : C.config)
@@ -549,7 +552,7 @@ let eval_non_local_function_call_concrete (config : C.config)
          * access to a body. *)
         let cf_eval_body : cm_fun =
           match fid with
-          | A.Replace -> eval_replace config region_params type_params
+          | A.Replace -> eval_replace_concrete config region_params type_params
           | BoxNew -> eval_box_new_concrete config region_params type_params
           | BoxDeref -> eval_box_deref_concrete config region_params type_params
           | BoxDerefMut ->
@@ -1128,13 +1131,10 @@ and eval_non_local_function_call_symbolic (config : C.config)
        * instantiated signatures, and delegate the work to an auxiliary function *)
       let inst_sig =
         match fid with
-        | A.BoxNew -> instantiate_fun_sig type_params Assumed.box_new_sig
-        | A.BoxDeref ->
-            instantiate_fun_sig type_params Assumed.box_deref_shared_sig
-        | A.BoxDerefMut ->
-            instantiate_fun_sig type_params Assumed.box_deref_mut_sig
-        | A.BoxFree -> failwith "Unreachable"
-        (* should have been treated above *)
+        | A.BoxFree ->
+            (* should have been treated above *)
+            failwith "Unreachable"
+        | _ -> instantiate_fun_sig type_params (Assumed.get_assumed_sig fid)
       in
 
       (* Evaluate the function call *)
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 5c25f2bd..f0e5df77 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -265,7 +265,23 @@ let adt_g_value_to_string (fmt : value_formatter)
           else if variant_id = result_fail_id then (
             assert (field_values = []);
             "@Result::Fail")
-          else failwith "Unreachable: improper variant id for result type")
+          else failwith "Unreachable: improper variant id for result type"
+      | Option ->
+          let variant_id = Option.get variant_id in
+          if variant_id = option_some_id then
+            match field_values with
+            | [ v ] -> "@Option::Some " ^ v
+            | _ -> failwith "Option::Some takes exactly one value"
+          else if variant_id = option_none_id then (
+            assert (field_values = []);
+            "@Option::None")
+          else failwith "Unreachable: improper variant id for result type"
+      | Vec ->
+          assert (variant_id = None);
+          let field_values =
+            List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
+          in
+          "Vec [" ^ String.concat "; " field_values ^ "]")
   | _ -> failwith "Inconsistent typed value"
 
 let rec typed_lvalue_to_string (fmt : value_formatter) (v : typed_lvalue) :
diff --git a/src/Pure.ml b/src/Pure.ml
index c773d613..d706a366 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -20,21 +20,23 @@ module VarId = IdGen ()
 
 type integer_type = T.integer_type [@@deriving show, ord]
 
-type assumed_ty =
-  | Result
-      (** The assumed types for the pure AST.
-
-          In comparison with CFIM:
-          - we removed `Box` (because it is translated as the identity: `Box T == T`)
-          - we added `Result`, which is the type used in the error monad. This allows
-            us to have a unified treatment of expressions.
-        *)
-[@@deriving show, ord]
+(** The assumed types for the pure AST.
+
+    In comparison with CFIM:
+    - we removed `Box` (because it is translated as the identity: `Box T == T`)
+    - we added `Result`, which is the type used in the error monad. This allows
+      us to have a unified treatment of expressions.
+  *)
+type assumed_ty = Result | Vec | Option [@@deriving show, ord]
 
 let result_return_id = VariantId.of_int 0
 
 let result_fail_id = VariantId.of_int 1
 
+let option_some_id = T.option_some_id
+
+let option_none_id = T.option_none_id
+
 type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty
 [@@deriving show, ord]
 
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index ceee71dd..5ac2af4e 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -730,7 +730,11 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_def) : fun_def =
                   | _ -> failwith "Unreachable"
                 in
                 arg.e
-            | A.BoxFree, _ -> (mk_value_expression unit_rvalue None).e)
+            | A.BoxFree, _ -> (mk_value_expression unit_rvalue None).e
+            | ( ( A.Replace | A.VecNew | A.VecPush | A.VecInsert | A.VecLen
+                | A.VecIndex | A.VecIndexMut ),
+                _ ) ->
+                super#visit_Call env call)
         | _ -> super#visit_Call env call
     end
   in
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index b563ba15..518e0a7d 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -326,6 +326,11 @@ let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
               if variant_id = result_return_id then "@result::Return"
               else if variant_id = result_fail_id then "@result::Fail"
               else failwith "Unreachable"
+          | Assumed Option ->
+              if variant_id = option_some_id then "@option::Some"
+              else if variant_id = option_none_id then "@option::None"
+              else failwith "Unreachable"
+          | Assumed Vec -> failwith "Unreachable"
           | AdtId id -> (
               let def = TypeDefId.Map.find id type_defs in
               match def.kind with
@@ -339,7 +344,10 @@ let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
         let field_name =
           match id with
           | Tuple -> failwith "Unreachable"
-          | Assumed Result -> failwith "Unreachable"
+          | Assumed (Result | Option) -> failwith "Unreachable"
+          | Assumed Vec ->
+              (* We can't directly have access to the fields of a vector *)
+              failwith "Unreachable"
           | AdtId id -> (
               let def = TypeDefId.Map.find id type_defs in
               match def.kind with
diff --git a/src/main.ml b/src/main.ml
index 95bebf39..b8673023 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -27,6 +27,8 @@ let () =
   let decompose_monads = ref false in
   let unfold_monads = ref true in
   let filter_unused_calls = ref true in
+  let test_units = ref false in
+  let test_trans_units = ref false in
 
   let spec =
     [
@@ -48,6 +50,13 @@ let () =
       ( "-filter-unused-calls",
         Arg.Set filter_unused_calls,
         " Filter the unused function calls, when possible" );
+      ( "-test-units",
+        Arg.Set test_units,
+        " Test the unit functions with the concrete interpreter" );
+      ( "-test-trans-units",
+        Arg.Set test_trans_units,
+        " Test the translated unit functions with the target theorem prover's \
+         normalizer" );
     ]
   in
   let spec = Arg.align spec in
@@ -113,7 +122,7 @@ let () =
       in
 
       (* Test the unit functions with the concrete interpreter *)
-      I.Test.test_unit_functions config m;
+      if !test_units then I.Test.test_unit_functions config m;
 
       (* Evaluate the symbolic interpreter on the functions, ignoring the
        * functions which contain loops - TODO: remove *)
@@ -121,7 +130,7 @@ let () =
       I.Test.test_functions_symbolic config synthesize m;
 
       (* Translate the functions *)
-      let test_unit_functions = true in
+      let test_unit_functions = !test_trans_units in
       let micro_passes_config =
         {
           Micro.decompose_monadic_let_bindings = !decompose_monads;