diff options
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/Contexts.ml | 9 | ||||
-rw-r--r-- | compiler/Extract.ml | 3 | ||||
-rw-r--r-- | compiler/Interpreter.ml | 10 | ||||
-rw-r--r-- | compiler/InterpreterBorrows.ml | 3 | ||||
-rw-r--r-- | compiler/InterpreterExpressions.ml | 41 | ||||
-rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 3 | ||||
-rw-r--r-- | compiler/InterpreterStatements.ml | 198 | ||||
-rw-r--r-- | compiler/InterpreterUtils.ml | 3 | ||||
-rw-r--r-- | compiler/PrintPure.ml | 5 | ||||
-rw-r--r-- | compiler/Pure.ml | 2 | ||||
-rw-r--r-- | compiler/PureMicroPasses.ml | 7 | ||||
-rw-r--r-- | compiler/PureTypeCheck.ml | 5 | ||||
-rw-r--r-- | compiler/PureUtils.ml | 3 | ||||
-rw-r--r-- | compiler/SymbolicAst.ml | 20 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 49 | ||||
-rw-r--r-- | compiler/Values.ml | 2 |
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 *) |