Fix some issues

8 files changed, 124 insertions, 88 deletions

diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index a1d5faaa..c7bc4ce8 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -366,7 +366,7 @@ let rec operand_constant_value_of_json (js : json) :
     (E.operand_constant_value, string) result =
   combine_error_msgs js "operand_constant_value_of_json"
     (match js with
-    | `Assoc [ ("ConstantValue", cv) ] ->
+    | `Assoc [ ("ConstantValue", `List [ cv ]) ] ->
         let* cv = constant_value_of_json cv in
         Ok (E.ConstantValue cv)
     | `Assoc [ ("ConstantAdt", `List [ variant_id; field_values ]) ] ->
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index db09b316..aecd6c68 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -95,7 +95,7 @@ let fstar_keywords =
   List.concat [ named_unops; named_binops; misc ]
 
 let fstar_assumed_adts : (assumed_ty * string) list =
-  [ (Result, "result"); (Option, "option") ]
+  [ (Result, "result"); (Option, "option"); (Vec, "vec") ]
 
 let fstar_assumed_structs : (assumed_ty * string) list = []
 
@@ -397,7 +397,13 @@ let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) :
   let ctx =
     match def.kind with
     | Struct fields ->
-        fst (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx)
+        (* Add the fields *)
+        let ctx =
+          fst
+            (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx)
+        in
+        (* Add the constructor name *)
+        fst (ctx_add_struct def ctx)
     | Enum variants ->
         fst
           (ctx_add_variants def
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 17e74ad3..9e4466b8 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -75,16 +75,26 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
     (cv : E.operand_constant_value) : V.typed_value =
   (* Check the type while converting - we actually need some information
    * contained in the type *)
+  log#ldebug
+    (lazy
+      ("operand_constant_value_to_typed_value:" ^ "\n- ty: "
+     ^ ety_to_string ctx ty ^ "\n- cv: "
+      ^ operand_constant_value_to_string ctx cv));
   match (ty, cv) with
   (* Adt *)
-  | ( T.Adt (T.AdtId def_id, region_params, type_params),
+  | ( T.Adt (adt_id, region_params, type_params),
       ConstantAdt (variant_id, field_values) ) ->
       assert (region_params = []);
       (* Compute the types of the fields *)
-      let def = C.ctx_lookup_type_def ctx def_id in
-      assert (def.region_params = []);
       let field_tys =
-        Subst.type_def_get_instantiated_field_etypes def variant_id type_params
+        match adt_id with
+        | T.AdtId def_id ->
+            let def = C.ctx_lookup_type_def ctx def_id in
+            assert (def.region_params = []);
+            Subst.type_def_get_instantiated_field_etypes def variant_id
+              type_params
+        | T.Tuple -> type_params
+        | T.Assumed _ -> failwith "Unreachable"
       in
       (* Compute the field values *)
       let field_values =
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 20657945..bbdd038f 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -33,6 +33,8 @@ let typed_value_to_string = PA.typed_value_to_string
 
 let typed_avalue_to_string = PA.typed_avalue_to_string
 
+let operand_constant_value_to_string = PA.operand_constant_value_to_string
+
 let place_to_string = PA.place_to_string
 
 let operand_to_string = PA.operand_to_string
diff --git a/src/Print.ml b/src/Print.ml
index b31be6ae..2db92d41 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -1142,6 +1142,11 @@ module EvalCtxCfimAst = struct
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
     PV.typed_avalue_to_string fmt v
 
+  let operand_constant_value_to_string (ctx : C.eval_ctx)
+      (cv : E.operand_constant_value) : string =
+    let fmt = PA.eval_ctx_to_ast_formatter ctx in
+    PA.operand_constant_value_to_string fmt cv
+
   let place_to_string (ctx : C.eval_ctx) (op : E.place) : string =
     let fmt = PA.eval_ctx_to_ast_formatter ctx in
     PA.place_to_string fmt op
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index f0e5df77..cf865a54 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -129,7 +129,8 @@ let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
   match id with
   | AdtId id -> fmt.type_def_id_to_string id
   | Tuple -> ""
-  | Assumed aty -> ( match aty with Result -> "Result")
+  | Assumed aty -> (
+      match aty with Result -> "Result" | Option -> "Option" | Vec -> "Vec")
 
 let rec ty_to_string (fmt : type_formatter) (ty : ty) : string =
   match ty with
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 518e0a7d..04d65423 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -287,92 +287,98 @@ type extraction_ctx = {
     functions, etc.
  *)
 
+(** Debugging function *)
+let id_to_string (id : id) (ctx : extraction_ctx) : string =
+  let fun_defs = ctx.trans_ctx.fun_context.fun_defs in
+  let type_defs = ctx.trans_ctx.type_context.type_defs in
+  (* TODO: factorize the pretty-printing with what is in PrintPure *)
+  let get_type_name (id : type_id) : string =
+    match id with
+    | AdtId id ->
+        let def = TypeDefId.Map.find id type_defs in
+        Print.name_to_string def.name
+    | Assumed aty -> show_assumed_ty aty
+    | Tuple -> failwith "Unreachable"
+  in
+  match id with
+  | FunId (fid, rg_id) ->
+      let fun_name =
+        match fid with
+        | A.Local fid ->
+            Print.name_to_string (FunDefId.Map.find fid fun_defs).name
+        | A.Assumed aid -> A.show_assumed_fun_id aid
+      in
+      let fun_kind =
+        match rg_id with
+        | None -> "forward"
+        | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id
+      in
+      "fun name (" ^ fun_kind ^ "): " ^ fun_name
+  | TypeId id -> "type name: " ^ get_type_name id
+  | StructId id -> "struct constructor of: " ^ get_type_name id
+  | VariantId (id, variant_id) ->
+      let variant_name =
+        match id with
+        | Tuple -> failwith "Unreachable"
+        | Assumed Result ->
+            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
+            | Struct _ -> failwith "Unreachable"
+            | Enum variants ->
+                let variant = VariantId.nth variants variant_id in
+                Print.name_to_string def.name ^ "::" ^ variant.variant_name)
+      in
+      "variant name: " ^ variant_name
+  | FieldId (id, field_id) ->
+      let field_name =
+        match id with
+        | Tuple -> 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
+            | Enum _ -> failwith "Unreachable"
+            | Struct fields ->
+                let field = FieldId.nth fields field_id in
+                let field_name =
+                  match field.field_name with
+                  | None -> FieldId.to_string field_id
+                  | Some name -> name
+                in
+                Print.name_to_string def.name ^ "." ^ field_name)
+      in
+      "field name: " ^ field_name
+  | UnknownId -> "keyword"
+  | TypeVarId _ | VarId _ ->
+      (* We should never get there: we add indices to make sure variable
+       * names are unique *)
+      failwith "Unreachable"
+
 let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
   (* The id_to_string function to print nice debugging messages if there are
    * collisions *)
-  let id_to_string (id : id) : string =
-    let fun_defs = ctx.trans_ctx.fun_context.fun_defs in
-    let type_defs = ctx.trans_ctx.type_context.type_defs in
-    (* TODO: factorize the pretty-printing with what is in PrintPure *)
-    let get_type_name (id : type_id) : string =
-      match id with
-      | AdtId id ->
-          let def = TypeDefId.Map.find id type_defs in
-          Print.name_to_string def.name
-      | Assumed aty -> show_assumed_ty aty
-      | Tuple -> failwith "Unreachable"
-    in
-    match id with
-    | FunId (fid, rg_id) ->
-        let fun_name =
-          match fid with
-          | A.Local fid ->
-              Print.name_to_string (FunDefId.Map.find fid fun_defs).name
-          | A.Assumed aid -> A.show_assumed_fun_id aid
-        in
-        let fun_kind =
-          match rg_id with
-          | None -> "forward"
-          | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id
-        in
-        "fun name (" ^ fun_kind ^ "): " ^ fun_name
-    | TypeId id -> "type name: " ^ get_type_name id
-    | StructId id -> "struct constructor of: " ^ get_type_name id
-    | VariantId (id, variant_id) ->
-        let variant_name =
-          match id with
-          | Tuple -> failwith "Unreachable"
-          | Assumed Result ->
-              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
-              | Struct _ -> failwith "Unreachable"
-              | Enum variants ->
-                  let variant = VariantId.nth variants variant_id in
-                  Print.name_to_string def.name ^ "::" ^ variant.variant_name)
-        in
-        "variant name: " ^ variant_name
-    | FieldId (id, field_id) ->
-        let field_name =
-          match id with
-          | Tuple -> 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
-              | Enum _ -> failwith "Unreachable"
-              | Struct fields ->
-                  let field = FieldId.nth fields field_id in
-                  let field_name =
-                    match field.field_name with
-                    | None -> FieldId.to_string field_id
-                    | Some name -> name
-                  in
-                  Print.name_to_string def.name ^ "." ^ field_name)
-        in
-        "field name: " ^ field_name
-    | UnknownId -> "keyword"
-    | TypeVarId _ | VarId _ ->
-        (* We should never get there: we add indices to make sure variable
-         * names are unique *)
-        failwith "Unreachable"
-  in
+  let id_to_string (id : id) : string = id_to_string id ctx in
   let names_map = names_map_add id_to_string id name ctx.names_map in
   { ctx with names_map }
 
 let ctx_get (id : id) (ctx : extraction_ctx) : string =
-  IdMap.find id ctx.names_map.id_to_name
+  match IdMap.find_opt id ctx.names_map.id_to_name with
+  | Some s -> s
+  | None ->
+      log#serror ("Could not find: " ^ id_to_string id ctx);
+      raise Not_found
 
 let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
@@ -485,6 +491,12 @@ let ctx_add_variants (def : type_def) (variants : (VariantId.id * variant) list)
     (fun ctx (vid, v) -> ctx_add_variant def vid v ctx)
     ctx variants
 
+let ctx_add_struct (def : type_def) (ctx : extraction_ctx) :
+    extraction_ctx * string =
+  let name = ctx.fmt.struct_constructor def.name in
+  let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in
+  (ctx, name)
+
 let ctx_add_fun_def (def : fun_def) (ctx : extraction_ctx) : extraction_ctx =
   (* Lookup the CFIM def to compute the region group information *)
   let def_id = def.def_id in
diff --git a/src/main.ml b/src/main.ml
index b8673023..c30c43f2 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -95,7 +95,7 @@ let () =
   interpreter_log#set_level EL.Debug;
   statements_log#set_level EL.Debug;
   paths_log#set_level EL.Warning;
-  expressions_log#set_level EL.Warning;
+  expressions_log#set_level EL.Debug;
   expansion_log#set_level EL.Warning;
   borrows_log#set_level EL.Warning;
   invariants_log#set_level EL.Warning;