crude generation working - missing unit tests & special constants handling

5 files changed, 70 insertions, 52 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 9766ddaf..b85c146b 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -902,7 +902,10 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       | AdtCons adt_cons_id ->
           extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
       | Proj proj ->
-          extract_field_projector ctx fmt inside app proj qualif.type_args args)
+          extract_field_projector ctx fmt inside app proj qualif.type_args args
+      (* TODO | Global global_id ->
+          extract_global_ref ctx fmt inside global_id*)
+    )
   | _ ->
       (* "Regular" expression *)
       (* Open parentheses *)
diff --git a/src/FunIdentifier.ml b/src/FunIdentifier.ml
index dd7e9318..956fce3f 100644
--- a/src/FunIdentifier.ml
+++ b/src/FunIdentifier.ml
@@ -1,2 +1,3 @@
 open Identifiers
 module FunDeclId = IdGen ()
+module GlobalDeclId = IdGen ()
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 4549365d..ee26d00d 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -1,5 +1,6 @@
 module T = Types
 module V = Values
+module LA = LlbcAst
 open Scalars
 module E = Expressions
 open Errors
@@ -71,53 +72,67 @@ let prepare_rplace (config : C.config) (expand_prim_copy : bool)
   comp cc read_place cf ctx
 
 (** Convert an operand constant operand value to a typed value *)
-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 (adt_id, region_params, type_params),
-      ConstantAdt (variant_id, field_values) ) ->
-      assert (region_params = []);
-      (* Compute the types of the fields *)
-      let field_tys =
-        match adt_id with
-        | T.AdtId def_id ->
-            let def = C.ctx_lookup_type_decl ctx def_id in
-            assert (def.region_params = []);
-            Subst.type_decl_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 =
-        List.map
-          (fun (ty, v) -> operand_constant_value_to_typed_value ctx ty v)
+let rec eval_operand_constant_value (ty : T.ety)
+    (cv : E.operand_constant_value) (cf : V.typed_value -> m_fun) : m_fun =
+  fun ctx ->
+    (* Check the type while converting - we actually need some information
+    * contained in the type *)
+    log#ldebug
+      (lazy
+        ("eval_operand_constant_value:" ^ "\n- ty: "
+      ^ ety_to_string ctx ty ^ "\n- cv: "
+        ^ operand_constant_value_to_string ctx cv));
+    match (ty, cv) with
+    (* Adt *)
+    | ( T.Adt (adt_id, region_params, type_params),
+        ConstantAdt (variant_id, field_values) ) ->
+        assert (region_params = []);
+        (* Compute the types of the fields *)
+        let field_tys =
+          match adt_id with
+          | T.AdtId def_id ->
+              let def = C.ctx_lookup_type_decl ctx def_id in
+              assert (def.region_params = []);
+              Subst.type_decl_get_instantiated_field_etypes def variant_id
+                type_params
+          | T.Tuple -> type_params
+          | T.Assumed _ -> failwith "Unreachable"
+        in
+        let adt_cf = fun fields ctx ->
+          let value = V.Adt { variant_id; field_values = fields } in
+          cf { value; ty } ctx
+        in
+        (* Map the field values & types to the continuation above *)
+        fold_left_apply_continuation
+          (fun (ty, v) cf ctx -> eval_operand_constant_value ty v cf ctx)
           (List.combine field_tys field_values)
-      in
-      (* Put together *)
-      let value = V.Adt { variant_id; field_values } in
-      { value; ty }
-  (* Scalar, boolean... *)
-  | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty }
-  | T.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty }
-  | T.Str, ConstantValue (String v) -> { V.value = V.Concrete (String v); ty }
-  | T.Integer int_ty, ConstantValue (V.Scalar v) ->
-      (* Check the type and the ranges *)
-      assert (int_ty = v.int_ty);
-      assert (check_scalar_value_in_range v);
-      { V.value = V.Concrete (V.Scalar v); ty }
-  (* Remaining cases (invalid) - listing as much as we can on purpose
-     (allows to catch errors at compilation if the definitions change) *)
-  | _, ConstantAdt _ | _, ConstantValue _ ->
-      failwith "Improperly typed constant value"
+          adt_cf ctx
+    (* Scalar, boolean... *)
+    | T.Bool, ConstantValue (Bool v)   -> cf { V.value = V.Concrete (Bool v);   ty } ctx
+    | T.Char, ConstantValue (Char v)   -> cf { V.value = V.Concrete (Char v);   ty } ctx
+    | T.Str,  ConstantValue (String v) -> cf { V.value = V.Concrete (String v); ty } ctx
+    | T.Integer int_ty, ConstantValue (V.Scalar v) ->
+        (* Check the type and the ranges *)
+        assert (int_ty = v.int_ty);
+        assert (check_scalar_value_in_range v);
+        cf { V.value = V.Concrete (V.Scalar v); ty } ctx
+    (* Constant expression identifier *)
+    | ty, ConstantId id ->
+        let dest = mk_fresh_symbolic_value V.FunCallRet (ety_no_regions_to_rty ty) in
+
+        (* Call the continuation *)
+        let expr = cf (mk_typed_value_from_symbolic_value dest) ctx in
+        
+        (* TODO Should it really be a new call ID ? *)
+        let call = SA.Fun (LA.Regular id, C.fresh_fun_call_id ()) in
+          
+        S.synthesize_function_call call [] [] [] []
+          dest None(*TODO meta-info*) expr
+
+    (* Remaining cases (invalid) - listing as much as we can on purpose
+      (allows to catch errors at compilation if the definitions change) *)
+    | _, ConstantAdt _ | _, ConstantValue _ ->
+        failwith "Improperly typed constant value"
 
 (** Prepare the evaluation of an operand.
 
@@ -157,8 +172,7 @@ let eval_operand_prepare (config : C.config) (op : E.operand)
    fun ctx ->
     match op with
     | Expressions.Constant (ty, cv) ->
-        let v = operand_constant_value_to_typed_value ctx ty cv in
-        cf v ctx
+        eval_operand_constant_value ty cv cf ctx
     | Expressions.Copy p ->
         (* Access the value *)
         let access = Read in
@@ -191,9 +205,7 @@ let eval_operand (config : C.config) (op : E.operand)
      ^ eval_ctx_to_string ctx ^ "\n"));
   (* Evaluate *)
   match op with
-  | Expressions.Constant (ty, cv) ->
-      let v = operand_constant_value_to_typed_value ctx ty cv in
-      cf v ctx
+  | Expressions.Constant (ty, cv) -> eval_operand_constant_value ty cv cf ctx
   | Expressions.Copy p ->
       (* Access the value *)
       let access = Read in
diff --git a/src/Print.ml b/src/Print.ml
index 28040181..9e2ff3cd 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -863,6 +863,7 @@ module LlbcAst = struct
   let rec operand_constant_value_to_string (fmt : ast_formatter)
       (cv : E.operand_constant_value) : string =
     match cv with
+    | E.ConstantId id -> fmt.fun_decl_id_to_string id
     | E.ConstantValue cv -> PV.constant_value_to_string cv
     | E.ConstantAdt (variant_id, field_values) ->
         (* This is a bit annoying, because we don't have context information
diff --git a/src/Pure.ml b/src/Pure.ml
index 05f78e35..256a872a 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -305,6 +305,7 @@ type qualif_id =
   | Func of fun_id
   | AdtCons of adt_cons_id  (** A function or ADT constructor identifier *)
   | Proj of projection  (** Field projector *)
+  (* TODO | Global of GlobalDeclId.id*)
 [@@deriving show]
 
 type qualif = { id : qualif_id; type_args : ty list } [@@deriving show]