summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Makefile7
-rw-r--r--src/ExtractToFStar.ml5
-rw-r--r--src/FunIdentifier.ml1
-rw-r--r--src/InterpreterExpressions.ml114
-rw-r--r--src/Print.ml1
-rw-r--r--src/Pure.ml1
6 files changed, 75 insertions, 54 deletions
diff --git a/Makefile b/Makefile
index 1e62dfd5..4dc1475b 100644
--- a/Makefile
+++ b/Makefile
@@ -31,8 +31,8 @@ build:
.PHONY: test
test: build trans-no_nested_borrows trans-paper \
trans-hashmap trans-hashmap_main \
- trans-external trans-nll-betree_nll \
- trans-nll-betree_main
+ trans-external trans-constants \
+ trans-nll-betree_nll trans-nll-betree_main \
# Add specific options to some tests
trans-no_nested_borrows trans-paper: \
@@ -48,6 +48,9 @@ trans-hashmap_main: SUBDIR:=hashmap_on_disk
trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
trans-nll-betree_nll: SUBDIR:=misc
+trans-constants: TRANS_OPTIONS += -no-split-files -no-state -no-decreases-clauses
+trans-constants: SUBDIR:=misc
+
trans-external: TRANS_OPTIONS +=
trans-external: SUBDIR:=misc
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]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 12:14:14 +0000