summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-11-12 19:35:24 +0100
committerSon Ho2023-11-12 19:35:24 +0100
commit0a5859fbb7bcd99bfa221eaf1af029ff660bf963 (patch)
tree2fc90c855ac49b1649b115f0e0e9b179dc993439 /compiler
parentb9f33bdd871a1bd7a1bd29f148dd05bd7990548b (diff)
Rename some variants
Diffstat (limited to '')
-rw-r--r--compiler/Assumed.ml2
-rw-r--r--compiler/ExtractTypes.ml6
-rw-r--r--compiler/Interpreter.ml2
-rw-r--r--compiler/InterpreterExpressions.ml2
-rw-r--r--compiler/PrintPure.ml6
-rw-r--r--compiler/PureUtils.ml2
-rw-r--r--compiler/Substitute.ml4
-rw-r--r--compiler/SymbolicAst.ml2
-rw-r--r--compiler/SymbolicToPure.ml4
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 =