summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Contexts.ml9
-rw-r--r--compiler/Extract.ml3
-rw-r--r--compiler/Interpreter.ml10
-rw-r--r--compiler/InterpreterBorrows.ml3
-rw-r--r--compiler/InterpreterExpressions.ml41
-rw-r--r--compiler/InterpreterLoopsJoinCtxs.ml3
-rw-r--r--compiler/InterpreterStatements.ml198
-rw-r--r--compiler/InterpreterUtils.ml3
-rw-r--r--compiler/PrintPure.ml5
-rw-r--r--compiler/Pure.ml2
-rw-r--r--compiler/PureMicroPasses.ml7
-rw-r--r--compiler/PureTypeCheck.ml5
-rw-r--r--compiler/PureUtils.ml3
-rw-r--r--compiler/SymbolicAst.ml20
-rw-r--r--compiler/SymbolicToPure.ml49
-rw-r--r--compiler/Values.ml2
16 files changed, 220 insertions, 143 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 2ca5653d..14b5d559 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -263,6 +263,10 @@ type eval_ctx = {
region_groups : RegionGroupId.id list;
type_vars : type_var list;
const_generic_vars : const_generic_var list;
+ const_generic_vars_map : typed_value Types.ConstGenericVarId.Map.t;
+ (** The map from const generic vars to their values. Those values
+ can be symbolic values or concrete values (in the latter case:
+ if we run in interpreter mode) *)
env : env;
ended_regions : RegionId.Set.t;
}
@@ -312,6 +316,11 @@ let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value =
env_lookup_var_value ctx.env vid
+(** Retrieve a const generic value in an evaluation context *)
+let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
+ : typed_value =
+ Types.ConstGenericVarId.Map.find vid ctx.const_generic_vars_map
+
(** Update a variable's value in the current frame.
This is a helper function: it can break invariants and doesn't perform
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index c4238d83..7daec16f 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2249,6 +2249,9 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
| Var var_id ->
let var_name = ctx_get_var var_id ctx in
F.pp_print_string fmt var_name
+ | CVar var_id ->
+ let var_name = ctx_get_const_generic_var var_id ctx in
+ F.pp_print_string fmt var_name
| Const cv -> ctx.fmt.extract_literal fmt inside cv
| App _ ->
let app, args = destruct_apps e in
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 154c5a21..37eeb333 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -34,6 +34,15 @@ let initialize_eval_context (type_context : C.type_context)
(region_groups : T.RegionGroupId.id list) (type_vars : T.type_var list)
(const_generic_vars : T.const_generic_var list) : C.eval_ctx =
C.reset_global_counters ();
+ let const_generic_vars_map =
+ T.ConstGenericVarId.Map.of_list
+ (List.map
+ (fun (cg : T.const_generic_var) ->
+ let ty = TypesUtils.ety_no_regions_to_rty (T.Literal cg.ty) in
+ let cv = mk_fresh_symbolic_typed_value V.ConstGeneric ty in
+ (cg.index, cv))
+ const_generic_vars)
+ in
{
C.type_context;
C.fun_context;
@@ -41,6 +50,7 @@ let initialize_eval_context (type_context : C.type_context)
C.region_groups;
C.type_vars;
C.const_generic_vars;
+ C.const_generic_vars_map;
C.env = [ C.Frame ];
C.ended_regions = T.RegionId.Set.empty;
}
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 4d67a4e4..f908d060 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -452,7 +452,8 @@ let give_back_symbolic_value (_config : C.config)
| V.SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
->
()
- | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate ->
+ | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate
+ | ConstGeneric ->
raise (Failure "Unreachable"));
(* Store the given-back value as a meta-value for synthesis purposes *)
let mv = nsv in
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 8b2070c6..2f6a7b49 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -230,17 +230,16 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
let prepare : cm_fun =
fun cf ctx ->
match op with
- | Expressions.Constant (ty, cv) ->
+ | E.Constant _ ->
(* No need to reorganize the context *)
- literal_to_typed_value (TypesUtils.ty_as_literal ty) cv |> ignore;
cf ctx
- | Expressions.Copy p ->
+ | E.Copy p ->
(* Access the value *)
let access = Read in
(* Expand the symbolic values, if necessary *)
let expand_prim_copy = true in
access_rplace_reorganize config expand_prim_copy access p cf ctx
- | Expressions.Move p ->
+ | E.Move p ->
(* Access the value *)
let access = Move in
let expand_prim_copy = false in
@@ -260,9 +259,35 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
(* Evaluate *)
match op with
- | Expressions.Constant (ty, cv) ->
- cf (literal_to_typed_value (TypesUtils.ty_as_literal ty) cv) ctx
- | Expressions.Copy p ->
+ | E.Constant cv -> (
+ match cv.value with
+ | E.CLiteral lit ->
+ cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx
+ | E.CVar vid -> (
+ let ctx0 = ctx in
+ (* Lookup the const generic value *)
+ let cv = C.ctx_lookup_const_generic_value ctx vid in
+ (* Copy the value *)
+ let allow_adt_copy = false in
+ let ctx, v = copy_value allow_adt_copy config ctx cv in
+ (* Continue *)
+ let e = cf v ctx in
+ (* We have to wrap the expression to introduce *)
+ match e with
+ | None -> None
+ | Some e ->
+ (* If we are synthesizing a symbolic AST, it means that we are in symbolic
+ mode: the value of the const generic is necessarily symbolic. *)
+ assert (is_symbolic cv.V.value);
+ (* *)
+ Some
+ (SymbolicAst.IntroSymbolic
+ ( ctx0,
+ None,
+ value_as_symbolic v.value,
+ SymbolicAst.ConstGenericValue vid,
+ e ))))
+ | E.Copy p ->
(* Access the value *)
let access = Read in
let cc = read_place access p in
@@ -283,7 +308,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
in
(* Compose and apply *)
comp cc copy cf ctx
- | Expressions.Move p ->
+ | E.Move p ->
(* Access the value *)
let access = Move in
let cc = read_place access p in
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index bf88e055..10205c27 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -557,6 +557,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
region_groups;
type_vars;
const_generic_vars;
+ const_generic_vars_map;
env = _;
ended_regions = ended_regions0;
} =
@@ -569,6 +570,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
region_groups = _;
type_vars = _;
const_generic_vars = _;
+ const_generic_vars_map = _;
env = _;
ended_regions = ended_regions1;
} =
@@ -583,6 +585,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
region_groups;
type_vars;
const_generic_vars;
+ const_generic_vars_map;
env;
ended_regions;
}
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 045c4484..6d520059 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -421,16 +421,16 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
(** 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)
- (_cg_params : T.const_generic list) : cm_fun =
+ (_cg_args : T.const_generic list) : cm_fun =
fun _cf _ctx -> raise Unimplemented
(** Auxiliary function - see {!eval_non_local_function_call} *)
let eval_box_new_concrete (config : C.config)
(region_params : T.erased_region list) (type_params : T.ety list)
- (cg_params : T.const_generic list) : cm_fun =
+ (cg_args : T.const_generic list) : cm_fun =
fun cf ctx ->
(* Check and retrieve the arguments *)
- match (region_params, type_params, cg_params, ctx.env) with
+ match (region_params, type_params, cg_args, ctx.env) with
| ( [],
[ boxed_ty ],
[],
@@ -470,10 +470,10 @@ let eval_box_new_concrete (config : C.config)
and [std::DerefMut::deref_mut] - see {!eval_non_local_function_call} *)
let eval_box_deref_mut_or_shared_concrete (config : C.config)
(region_params : T.erased_region list) (type_params : T.ety list)
- (cg_params : T.const_generic list) (is_mut : bool) : cm_fun =
+ (cg_args : T.const_generic list) (is_mut : bool) : cm_fun =
fun cf ctx ->
(* Check the arguments *)
- match (region_params, type_params, cg_params, ctx.env) with
+ match (region_params, type_params, cg_args, ctx.env) with
| ( [],
[ boxed_ty ],
[],
@@ -517,18 +517,18 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
(** Auxiliary function - see {!eval_non_local_function_call} *)
let eval_box_deref_concrete (config : C.config)
(region_params : T.erased_region list) (type_params : T.ety list)
- (cg_params : T.const_generic list) : cm_fun =
+ (cg_args : T.const_generic list) : cm_fun =
let is_mut = false in
- eval_box_deref_mut_or_shared_concrete config region_params type_params
- cg_params is_mut
+ eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args
+ is_mut
(** Auxiliary function - see {!eval_non_local_function_call} *)
let eval_box_deref_mut_concrete (config : C.config)
(region_params : T.erased_region list) (type_params : T.ety list)
- (cg_params : T.const_generic list) : cm_fun =
+ (cg_args : T.const_generic list) : cm_fun =
let is_mut = true in
- eval_box_deref_mut_or_shared_concrete config region_params type_params
- cg_params is_mut
+ eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args
+ is_mut
(** Auxiliary function - see {!eval_non_local_function_call}.
@@ -550,10 +550,10 @@ let eval_box_deref_mut_concrete (config : C.config)
the destination (by setting it to [()]).
*)
let eval_box_free (config : C.config) (region_params : T.erased_region list)
- (type_params : T.ety list) (cg_params : T.const_generic list)
+ (type_params : T.ety list) (cg_args : T.const_generic list)
(args : E.operand list) (dest : E.place) : cm_fun =
fun cf ctx ->
- match (region_params, type_params, cg_params, args) with
+ match (region_params, type_params, cg_args, args) with
| [], [ boxed_ty ], [], [ E.Move input_box_place ] ->
(* Required type checking *)
let input_box = InterpreterPaths.read_place Write input_box_place ctx in
@@ -573,14 +573,17 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
(** 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)
- (_cg_params : T.const_generic list) : cm_fun =
+ (_cg_args : T.const_generic 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)
(fid : A.assumed_fun_id) (region_params : T.erased_region list)
- (type_params : T.ety list) (cg_params : T.const_generic list)
+ (type_params : T.ety list) (cg_args : T.const_generic list)
(args : E.operand list) (dest : E.place) : cm_fun =
+ (* Sanity check: we don't fully handle the const generic vars environment
+ in concrete mode yet *)
+ assert (cg_args = []);
(* There are two cases (and this is extremely annoying):
- the function is not box_free
- the function is box_free
@@ -589,7 +592,7 @@ let eval_non_local_function_call_concrete (config : C.config)
match fid with
| A.BoxFree ->
(* Degenerate case: box_free *)
- eval_box_free config region_params type_params cg_params args dest
+ eval_box_free config region_params type_params cg_args args dest
| _ ->
(* "Normal" case: not box_free *)
(* Evaluate the operands *)
@@ -612,7 +615,7 @@ let eval_non_local_function_call_concrete (config : C.config)
let ret_vid = E.VarId.zero in
let ret_ty =
get_non_local_function_return_type fid region_params type_params
- cg_params
+ cg_args
in
let ret_var = mk_var ret_vid (Some "@return") ret_ty in
let cc = comp cc (push_uninitialized_var ret_var) in
@@ -631,19 +634,19 @@ let eval_non_local_function_call_concrete (config : C.config)
let cf_eval_body : cm_fun =
match fid with
| A.Replace ->
- eval_replace_concrete config region_params type_params cg_params
+ eval_replace_concrete config region_params type_params cg_args
| BoxNew ->
- eval_box_new_concrete config region_params type_params cg_params
+ eval_box_new_concrete config region_params type_params cg_args
| BoxDeref ->
- eval_box_deref_concrete config region_params type_params cg_params
+ eval_box_deref_concrete config region_params type_params cg_args
| BoxDerefMut ->
eval_box_deref_mut_concrete config region_params type_params
- cg_params
+ cg_args
| BoxFree ->
(* Should have been treated above *) raise (Failure "Unreachable")
| VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
eval_vec_function_concrete config fid region_params type_params
- cg_params
+ cg_args
| ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
| ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut
| SliceIndexShared | SliceIndexMut | SliceSubsliceShared
@@ -663,7 +666,7 @@ let eval_non_local_function_call_concrete (config : C.config)
comp cf_eval_ops cf_eval_call
let instantiate_fun_sig (type_params : T.ety list)
- (cg_params : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig =
+ (cg_args : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig =
(* Generate fresh abstraction ids and create a substitution from region
* group ids to abstraction ids *)
let rg_abs_ids_bindings =
@@ -694,7 +697,7 @@ let instantiate_fun_sig (type_params : T.ety list)
let rtype_params = List.map ety_no_regions_to_rty type_params in
let tsubst = Subst.make_type_subst_from_vars sg.type_params rtype_params in
let cgsubst =
- Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_params
+ Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_args
in
(* Substitute the signature *)
let inst_sig = Subst.substitute_signature asubst rsubst tsubst cgsubst sg in
@@ -1054,81 +1057,86 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
(_region_args : T.erased_region list) (type_args : T.ety list)
(cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
st_cm_fun =
- fun cf ctx ->
- (* Retrieve the (correctly instantiated) body *)
- let def = C.ctx_lookup_fun_decl ctx fid in
- (* We can evaluate the function call only if it is not opaque *)
- let body =
- match def.body with
- | None ->
- raise
- (Failure
- ("Can't evaluate a call to an opaque function: "
- ^ Print.name_to_string def.name))
- | Some body -> body
- in
- let tsubst =
- Subst.make_type_subst_from_vars def.A.signature.type_params type_args
- in
- let cgsubst =
- Subst.make_const_generic_subst_from_vars
- def.A.signature.const_generic_params cg_args
- in
- let locals, body_st = Subst.fun_body_substitute_in_body tsubst cgsubst body in
-
- (* Evaluate the input operands *)
- assert (List.length args = body.A.arg_count);
- let cc = eval_operands config args in
-
- (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
- * of the operands evaluation from above to the functions afterwards, while
- * ignoring it in this function *)
- let cc = comp_transmit cc push_frame in
-
- (* Compute the initial values for the local variables *)
- (* 1. Push the return value *)
- let ret_var, locals =
- match locals with
- | ret_ty :: locals -> (ret_ty, locals)
- | _ -> raise (Failure "Unreachable")
- in
- let input_locals, locals =
- Collections.List.split_at locals body.A.arg_count
- in
-
- let cc = comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) in
-
- (* 2. Push the input values *)
- let cf_push_inputs cf args =
- let inputs = List.combine input_locals args in
- (* Note that this function checks that the variables and their values
- * have the same type (this is important) *)
- push_vars inputs cf
- in
- let cc = comp cc cf_push_inputs in
+ (* Sanity check: we don't fully handle the const generic vars environment
+ in concrete mode yet *)
+ assert (cg_args = []);
+ fun cf ctx ->
+ (* Retrieve the (correctly instantiated) body *)
+ let def = C.ctx_lookup_fun_decl ctx fid in
+ (* We can evaluate the function call only if it is not opaque *)
+ let body =
+ match def.body with
+ | None ->
+ raise
+ (Failure
+ ("Can't evaluate a call to an opaque function: "
+ ^ Print.name_to_string def.name))
+ | Some body -> body
+ in
+ let tsubst =
+ Subst.make_type_subst_from_vars def.A.signature.type_params type_args
+ in
+ let cgsubst =
+ Subst.make_const_generic_subst_from_vars
+ def.A.signature.const_generic_params cg_args
+ in
+ let locals, body_st =
+ Subst.fun_body_substitute_in_body tsubst cgsubst body
+ in
- (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
- let cc = comp cc (push_uninitialized_vars locals) in
+ (* Evaluate the input operands *)
+ assert (List.length args = body.A.arg_count);
+ let cc = eval_operands config args in
+
+ (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
+ * of the operands evaluation from above to the functions afterwards, while
+ * ignoring it in this function *)
+ let cc = comp_transmit cc push_frame in
+
+ (* Compute the initial values for the local variables *)
+ (* 1. Push the return value *)
+ let ret_var, locals =
+ match locals with
+ | ret_ty :: locals -> (ret_ty, locals)
+ | _ -> raise (Failure "Unreachable")
+ in
+ let input_locals, locals =
+ Collections.List.split_at locals body.A.arg_count
+ in
- (* Execute the function body *)
- let cc = comp cc (eval_function_body config body_st) in
+ let cc = comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) in
- (* Pop the stack frame and move the return value to its destination *)
- let cf_finish cf res =
- match res with
- | Panic -> cf Panic
- | Return ->
- (* Pop the stack frame, retrieve the return value, move it to
- * its destination and continue *)
- pop_frame_assign config dest (cf Unit)
- | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
- | EndContinue _ ->
- raise (Failure "Unreachable")
- in
- let cc = comp cc cf_finish in
+ (* 2. Push the input values *)
+ let cf_push_inputs cf args =
+ let inputs = List.combine input_locals args in
+ (* Note that this function checks that the variables and their values
+ * have the same type (this is important) *)
+ push_vars inputs cf
+ in
+ let cc = comp cc cf_push_inputs in
+
+ (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
+ let cc = comp cc (push_uninitialized_vars locals) in
+
+ (* Execute the function body *)
+ let cc = comp cc (eval_function_body config body_st) in
+
+ (* Pop the stack frame and move the return value to its destination *)
+ let cf_finish cf res =
+ match res with
+ | Panic -> cf Panic
+ | Return ->
+ (* Pop the stack frame, retrieve the return value, move it to
+ * its destination and continue *)
+ pop_frame_assign config dest (cf Unit)
+ | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
+ | EndContinue _ ->
+ raise (Failure "Unreachable")
+ in
+ let cc = comp cc cf_finish in
- (* Continue *)
- cc cf ctx
+ (* Continue *)
+ cc cf ctx
(** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 7bd37550..637f1b1e 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -255,7 +255,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
raise Found
else ()
| V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
- | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate ->
+ | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate
+ | V.ConstGeneric ->
()
end
in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index cfb63ec2..dfb2c9fd 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -559,9 +559,8 @@ let fun_or_op_id_to_string (fmt : ast_formatter) (fun_id : fun_or_op_id) :
let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
(indent : string) (indent_incr : string) (e : texpression) : string =
match e.e with
- | Var var_id ->
- let s = fmt.var_id_to_string var_id in
- if inside then "(" ^ s ^ ")" else s
+ | Var var_id -> fmt.var_id_to_string var_id
+ | CVar cg_id -> fmt.const_generic_var_id_to_string cg_id
| Const cv -> literal_to_string cv
| App _ ->
(* Recursively destruct the app, to have a pair (app, arguments list) *)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ac4ca081..55513cc2 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -37,6 +37,7 @@ module ConstGenericVarId = T.ConstGenericVarId
type integer_type = T.integer_type [@@deriving show, ord]
type const_generic_var = T.const_generic_var [@@deriving show, ord]
type const_generic = T.const_generic [@@deriving show, ord]
+type const_generic_var_id = T.const_generic_var_id [@@deriving show, ord]
(** The assumed types for the pure AST.
@@ -536,6 +537,7 @@ class virtual ['self] mapreduce_expression_base =
*)
type expression =
| Var of var_id (** a variable *)
+ | CVar of const_generic_var_id (** a const generic var *)
| Const of literal
| App of texpression * texpression
(** Application of a function to an argument.
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b6025df4..65dc7ff2 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -376,8 +376,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let ty = e.ty in
let ctx, e =
match e.e with
- | Var _ -> (* Nothing to do *) (ctx, e.e)
- | Const _ -> (* Nothing to do *) (ctx, e.e)
+ | Var _ | CVar _ | Const _ -> (* Nothing to do *) (ctx, e.e)
| App (app, arg) ->
let ctx, app = update_texpression app ctx in
let ctx, arg = update_texpression arg ctx in
@@ -834,7 +833,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
method! visit_texpression env e =
match e.e with
- | Var _ | Const _ -> fun _ -> false
+ | Var _ | CVar _ | Const _ -> fun _ -> false
| StructUpdate _ ->
(* There shouldn't be monadic calls in structure updates - also
note that by returning [false] we are conservative: we might
@@ -930,7 +929,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
method! visit_expression env e =
match e with
- | Var _ | Const _ | App _ | Qualif _
+ | Var _ | CVar _ | Const _ | App _ | Qualif _
| Switch (_, _)
| Meta (_, _)
| StructUpdate _ | Abs _ ->
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 8d28bb8a..d145ce93 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -65,6 +65,8 @@ type tc_ctx = {
global_decls : A.global_decl A.GlobalDeclId.Map.t;
(** The global declarations *)
env : ty VarId.Map.t; (** Environment from variables to types *)
+ const_generics : ty T.ConstGenericVarId.Map.t;
+ (** The types of the const generics *)
}
let check_literal (v : literal) (ty : literal_type) : unit =
@@ -115,6 +117,9 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
match VarId.Map.find_opt var_id ctx.env with
| None -> ()
| Some ty -> assert (ty = e.ty))
+ | CVar cg_id ->
+ let ty = T.ConstGenericVarId.Map.find cg_id ctx.const_generics in
+ assert (ty = e.ty)
| Const cv -> check_literal cv (ty_as_literal e.ty)
| App (app, arg) ->
let input_ty, output_ty = destruct_arrow app.ty in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 1c8d8921..461098f2 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -164,7 +164,8 @@ let fun_sig_substitute (tsubst : TypeVarId.id -> ty)
*)
let rec let_group_requires_parentheses (e : texpression) : bool =
match e.e with
- | Var _ | Const _ | App _ | Abs _ | Qualif _ | StructUpdate _ -> false
+ | Var _ | CVar _ | Const _ | App _ | Abs _ | Qualif _ | StructUpdate _ ->
+ false
| Let (monadic, _, _, next_e) ->
if monadic then true else let_group_requires_parentheses next_e
| Switch (_, _) -> false
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 7dc94dcd..17cdcabc 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -79,6 +79,9 @@ class ['self] iter_expression_base =
method visit_loop_id : 'env -> V.loop_id -> unit = fun _ _ -> ()
method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
+ method visit_const_generic_var_id : 'env -> T.const_generic_var_id -> unit =
+ fun _ _ -> ()
+
method visit_symbolic_value_id : 'env -> V.symbolic_value_id -> unit =
fun _ _ -> ()
@@ -171,14 +174,14 @@ type expression =
* expression
(** We introduce a new symbolic value, equal to some other value.
- This is used for instance when reorganizing the environment to compute
- fixed points: we duplicate some shared symbolic values to destructure
- the shared values, in order to make the environment a bit more general
- (while losing precision of course).
+ This is used for instance when reorganizing the environment to compute
+ fixed points: we duplicate some shared symbolic values to destructure
+ the shared values, in order to make the environment a bit more general
+ (while losing precision of course).
- The context is the evaluation context from before introducing the new
- value. It has the same purpose as for the {!Return} case.
- *)
+ The context is the evaluation context from before introducing the new
+ value. It has the same purpose as for the {!Return} case.
+ *)
| ForwardEnd of
Contexts.eval_ctx
* V.typed_value symbolic_value_id_map option
@@ -253,6 +256,9 @@ and value_aggregate =
| SingleValue of V.typed_value (** Regular case *)
| Array of V.typed_value list
(** This is used when introducing array aggregates *)
+ | ConstGenericValue of T.const_generic_var_id
+ (** This is used when evaluating a const generic value: in the interpreter,
+ we introduce a fresh symbolic value. *)
[@@deriving
show,
visitors
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3512270a..7dda1f22 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -201,29 +201,6 @@ type bs_ctx = {
}
[@@deriving show]
-let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
- let env = VarId.Map.empty in
- let ctx =
- {
- PureTypeCheck.type_decls = ctx.type_context.type_decls;
- global_decls = ctx.global_context.llbc_global_decls;
- env;
- }
- in
- let _ = PureTypeCheck.check_typed_pattern ctx v in
- ()
-
-let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
- let env = VarId.Map.empty in
- let ctx =
- {
- PureTypeCheck.type_decls = ctx.type_context.type_decls;
- global_decls = ctx.global_context.llbc_global_decls;
- env;
- }
- in
- PureTypeCheck.check_texpression ctx e
-
(* TODO: move *)
let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
@@ -589,6 +566,31 @@ let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
let type_infos = ctx.type_context.type_infos in
translate_back_ty type_infos keep_region inside_mut ty
+let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
+ let const_generics =
+ T.ConstGenericVarId.Map.of_list
+ (List.map
+ (fun (cg : T.const_generic_var) ->
+ (cg.index, ctx_translate_fwd_ty ctx (T.Literal cg.ty)))
+ ctx.sg.const_generic_params)
+ in
+ let env = VarId.Map.empty in
+ {
+ PureTypeCheck.type_decls = ctx.type_context.type_decls;
+ global_decls = ctx.global_context.llbc_global_decls;
+ env;
+ const_generics;
+ }
+
+let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
+ let ctx = mk_type_check_ctx ctx in
+ let _ = PureTypeCheck.check_typed_pattern ctx v in
+ ()
+
+let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
+ let ctx = mk_type_check_ctx ctx in
+ PureTypeCheck.check_texpression ctx e
+
(** List the ancestors of an abstraction *)
let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs)
(call_id : V.FunCallId.id) : V.AbstractionId.id list =
@@ -2298,6 +2300,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
{ struct_id = Assumed Array; init = None; updates = values }
in
{ e = StructUpdate su; ty = var.ty }
+ | ConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
in
(* Make the let-binding *)
diff --git a/compiler/Values.ml b/compiler/Values.ml
index d884c319..58737557 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -52,6 +52,8 @@ type sv_kind =
(** The result of a loop join (when computing loop fixed points) *)
| Aggregate
(** A symbolic value we introduce in place of an aggregate value *)
+ | ConstGeneric
+ (** A symbolic value we introduce when using a const generic as a value *)
[@@deriving show, ord]
(** Ancestor for {!symbolic_value} iter visitor *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 19:30:19 +0000