diff options
| -rw-r--r-- | compiler/Assumed.ml | 2 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 6 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 2 | ||||
| -rw-r--r-- | compiler/PrintPure.ml | 6 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/Substitute.ml | 4 | ||||
| -rw-r--r-- | compiler/SymbolicAst.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 4 |
9 files changed, 15 insertions, 15 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index d8f19173..5622ef26 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -43,7 +43,7 @@ module Sig = struct let tvar_id_0 = T.TypeVarId.of_int 0 let tvar_0 : T.ty = T.TypeVar tvar_id_0 let cgvar_id_0 = T.ConstGenericVarId.of_int 0 - let cgvar_0 : T.const_generic = T.ConstGenericVar cgvar_id_0 + let cgvar_0 : T.const_generic = T.CGVar cgvar_id_0 (** Region 'a of id 0 *) let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" } diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 48273023..902b7e25 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1119,11 +1119,11 @@ let extract_arrow (fmt : F.formatter) () : unit = let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (cg : const_generic) : unit = match cg with - | ConstGenericGlobal id -> + | CGGlobal id -> let s = ctx_get_global id ctx in F.pp_print_string fmt s - | ConstGenericValue v -> ctx.fmt.extract_literal fmt inside v - | ConstGenericVar id -> + | CGValue v -> ctx.fmt.extract_literal fmt inside v + | CGVar id -> let s = ctx_get_const_generic_var id ctx in F.pp_print_string fmt s diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index bc28bcd6..b1178aa7 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -74,7 +74,7 @@ let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (sg : A.fun_sig) let types = List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) types in let const_generics = List.map - (fun (v : T.const_generic_var) -> T.ConstGenericVar v.T.index) + (fun (v : T.const_generic_var) -> T.CGVar v.T.index) const_generics in (* Annoying that we have to generate this substitution here *) diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index f4430c77..c7fcc1af 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -329,7 +329,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) ( ctx0, None, value_as_symbolic v.value, - SymbolicAst.VaConstGenericValue vid, + SymbolicAst.VaCGValue vid, e ))) | E.CFnPtr _ -> raise (Failure "TODO")) | E.Copy p -> diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index cd156215..7c52c423 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -211,9 +211,9 @@ let type_id_to_string (fmt : type_formatter) (id : type_id) : string = let const_generic_to_string (fmt : type_formatter) (cg : T.const_generic) : string = match cg with - | ConstGenericGlobal id -> fmt.global_decl_id_to_string id - | ConstGenericVar id -> fmt.const_generic_var_id_to_string id - | ConstGenericValue lit -> literal_to_string lit + | CGGlobal id -> fmt.global_decl_id_to_string id + | CGVar id -> fmt.const_generic_var_id_to_string id + | CGValue lit -> literal_to_string lit let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string = match ty with diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 5e46d551..49c8dd70 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -111,7 +111,7 @@ let ty_substitute (subst : subst) (ty : ty) : ty = object inherit [_] map_ty method! visit_TypeVar _ var_id = subst.ty_subst var_id - method! visit_ConstGenericVar _ var_id = subst.cg_subst var_id + method! visit_CGVar _ var_id = subst.cg_subst var_id method! visit_Clause _ id = subst.tr_subst id method! visit_Self _ = subst.tr_self end diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index b4eee9f8..490574a2 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -29,7 +29,7 @@ let st_substitute_visitor (subst : subst) = (* We should never get here because we reimplemented [visit_TypeVar] *) raise (Failure "Unexpected") - method! visit_ConstGenericVar _ id = subst.cg_subst id + method! visit_CGVar _ id = subst.cg_subst id method! visit_const_generic_var_id _ _ = (* We should never get here because we reimplemented [visit_Var] *) @@ -68,7 +68,7 @@ let erase_regions_subst : subst = { r_subst = (fun _ -> T.RErased); ty_subst = (fun vid -> T.TypeVar vid); - cg_subst = (fun id -> T.ConstGenericVar id); + cg_subst = (fun id -> T.CGVar id); tr_subst = (fun id -> T.Clause id); tr_self = T.Self; } diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 927544b2..d114f18d 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -243,7 +243,7 @@ and value_aggregate = | VaSingleValue of V.typed_value (** Regular case *) | VaArray of V.typed_value list (** This is used when introducing array aggregates *) - | VaConstGenericValue of T.const_generic_var_id + | VaCGValue of T.const_generic_var_id (** This is used when evaluating a const generic value: in the interpreter, we introduce a fresh symbolic value. *) | VaTraitConstValue of T.trait_ref * T.generic_args * string diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 97755438..91edbf04 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2487,7 +2487,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) { struct_id = TAssumed Array; init = None; updates = values } in { e = StructUpdate su; ty = var.ty } - | VaConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty } + | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty } | VaTraitConstValue (trait_ref, generics, const_name) -> let type_infos = ctx.type_context.type_infos in let trait_ref = translate_fwd_trait_ref type_infos trait_ref in @@ -2740,7 +2740,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = in let const_generics = List.map - (fun (cg : T.const_generic_var) -> T.ConstGenericVar cg.T.index) + (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index) const_generics in let trait_refs = |