summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/AssociatedTypes.ml25
-rw-r--r--compiler/Extract.ml6
-rw-r--r--compiler/ExtractBase.ml2
-rw-r--r--compiler/ExtractTypes.ml7
-rw-r--r--compiler/InterpreterExpressions.ml6
-rw-r--r--compiler/InterpreterStatements.ml20
-rw-r--r--compiler/InterpreterUtils.ml2
-rw-r--r--compiler/Print.ml4
-rw-r--r--compiler/PrintPure.ml18
-rw-r--r--compiler/Pure.ml6
-rw-r--r--compiler/RegionsHierarchy.ml2
-rw-r--r--compiler/SymbolicAst.ml3
-rw-r--r--compiler/SymbolicToPure.ml28
-rw-r--r--compiler/Translate.ml2
-rw-r--r--compiler/TypesUtils.ml3
15 files changed, 54 insertions, 80 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 054c8169..7b928566 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -51,9 +51,10 @@ let compute_norm_trait_types_from_preds
that it would be enough to only visit the field [ty] of the trait type
constraint, but for safety we visit all the fields *)
assert (trait_type_constraint_no_regions c);
- let trait_ty = TTraitType (c.trait_ref, c.generics, c.type_name) in
+ let { trait_ref; type_name; ty } : trait_type_constraint = c in
+ let trait_ty = TTraitType (trait_ref, type_name) in
let trait_ty_ref = get_ref trait_ty in
- let ty_ref = get_ref c.ty in
+ let ty_ref = get_ref ty in
let new_repr = UnionFind.get ty_ref in
let merged = UnionFind.union trait_ty_ref ty_ref in
(* Not sure the set operation is necessary, but I want to control which
@@ -72,9 +73,7 @@ let compute_norm_trait_types_from_preds
List.filter_map
(fun (k, v) ->
match k with
- | TTraitType (trait_ref, generics, type_name) ->
- assert (generics = empty_generic_args);
- Some ({ trait_ref; type_name }, v)
+ | TTraitType (trait_ref, type_name) -> Some ({ trait_ref; type_name }, v)
| _ -> None)
rbindings
in
@@ -225,20 +224,15 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
let inputs = List.map (norm_ctx_normalize_ty ctx) inputs in
let output = norm_ctx_normalize_ty ctx output in
TArrow (regions, inputs, output)
- | TTraitType (trait_ref, generics, type_name) -> (
+ | TTraitType (trait_ref, type_name) -> (
log#ldebug
(lazy
("norm_ctx_normalize_ty:\n- trait type: " ^ ty_to_string ctx ty
^ "\n- trait_ref: "
^ trait_ref_to_string ctx trait_ref
- ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref
- ^ "\n- generics:\n"
- ^ generic_args_to_string ctx generics));
+ ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref));
(* Normalize and attempt to project the type from the trait ref *)
let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in
- let generics = norm_ctx_normalize_generic_args ctx generics in
- (* For now, we don't support higher order types *)
- assert (generics = empty_generic_args);
let ty : ty =
match trait_ref.trait_id with
| TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ }
@@ -284,7 +278,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref));
(* We can't project *)
assert (trait_instance_id_is_local_clause trait_ref.trait_id);
- TTraitType (trait_ref, generics, type_name)
+ TTraitType (trait_ref, type_name)
in
let tr : trait_type_ref = { trait_ref; type_name } in
(* Lookup the representative, if there is *)
@@ -484,11 +478,10 @@ and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx)
let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx)
(ttc : trait_type_constraint) : trait_type_constraint =
- let { trait_ref; generics; type_name; ty } = ttc in
+ let { trait_ref; type_name; ty } : trait_type_constraint = ttc in
let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in
- let generics = norm_ctx_normalize_generic_args ctx generics in
let ty = norm_ctx_normalize_ty ctx ty in
- { trait_ref; generics; type_name; ty }
+ { trait_ref; type_name; ty }
let mk_norm_ctx (ctx : eval_ctx) : norm_ctx =
{
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 46f6a1ca..a93ed6e4 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -326,11 +326,8 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args
| Proj proj ->
extract_field_projector ctx fmt inside app proj qualif.generics args
- | TraitConst (trait_ref, generics, const_name) ->
- let use_brackets = generics <> empty_generic_args in
- if use_brackets then F.pp_print_string fmt "(";
+ | TraitConst (trait_ref, const_name) ->
extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref;
- extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
let name =
ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id
const_name ctx
@@ -338,7 +335,6 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
let add_brackets (s : string) =
if !backend = Coq then "(" ^ s ^ ")" else s
in
- if use_brackets then F.pp_print_string fmt ")";
F.pp_print_string fmt ("." ^ add_brackets name))
| _ ->
(* "Regular" expression *)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 5e97cd21..297a1d22 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1682,7 +1682,7 @@ let ctx_compute_var_basename (ctx : extraction_ctx) (basename : string option)
| TLiteral lty -> (
match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
| TArrow _ -> "f"
- | TTraitType (_, _, name) -> name_from_type_ident name)
+ | TTraitType (_, name) -> name_from_type_ident name)
(** Generates a type variable basename. *)
let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 9d4131d2..bbd5fae4 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -528,7 +528,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
extract_rec false ret_ty;
if inside then F.pp_print_string fmt ")"
- | TTraitType (trait_ref, generics, type_name) -> (
+ | TTraitType (trait_ref, type_name) -> (
if !parameterize_trait_types then raise (Failure "Unimplemented")
else
let type_name =
@@ -547,7 +547,6 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
*)
match trait_ref.trait_id with
| Self ->
- assert (generics = empty_generic_args);
assert (trait_ref.generics = empty_generic_args);
extract_trait_instance_id_with_dot ctx fmt no_params_tys false
trait_ref.trait_id;
@@ -555,11 +554,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
| _ ->
(* HOL4 doesn't have 1st class types *)
assert (!backend <> HOL4);
- let use_brackets = generics <> empty_generic_args in
- if use_brackets then F.pp_print_string fmt "(";
extract_trait_ref ctx fmt no_params_tys false trait_ref;
- extract_generic_args ctx fmt no_params_tys generics;
- if use_brackets then F.pp_print_string fmt ")";
F.pp_print_string fmt ("." ^ add_brackets type_name))
and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 8536b4ab..dc100fe3 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -263,8 +263,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
match cv.value with
| CLiteral lit ->
cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx
- | CTraitConst (trait_ref, generics, const_name) -> (
- assert (generics = empty_generic_args);
+ | CTraitConst (trait_ref, const_name) -> (
match trait_ref.trait_id with
| TraitImpl _ ->
(* This shouldn't happen: if we refer to a concrete implementation, we
@@ -294,8 +293,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
( ctx0,
None,
value_as_symbolic v.value,
- SymbolicAst.VaTraitConstValue
- (trait_ref, generics, const_name),
+ SymbolicAst.VaTraitConstValue (trait_ref, const_name),
e ))))
| CVar vid -> (
let ctx0 = ctx in
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 0cf8b88a..eef9e2c9 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -769,12 +769,8 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
("trait method call:\n- call: " ^ call_to_string ctx call
^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n"
^ generic_args_to_string ctx func.generics
- ^ "\n- trait and method generics:\n"
- ^ generic_args_to_string ctx
- (Option.get func.trait_and_method_generic_args)));
- (* When instantiating, we need to group the generics for the trait ref
- and the method *)
- let generics = Option.get func.trait_and_method_generic_args in
+ ^ "\n- trait_ref.trait_decl_ref: "
+ ^ trait_decl_ref_to_string ctx trait_ref.trait_decl_ref));
(* Lookup the trait method signature - there are several possibilities
depending on whethere we call a top-level trait method impl or the
method from a local clause *)
@@ -794,6 +790,11 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
| Some (_, id) ->
(* This is a required method *)
let method_def = ctx_lookup_fun_decl ctx id in
+ (* We have to concatenate the generics for the impl
+ and the generics for the method *)
+ let generics =
+ merge_generic_args trait_ref.generics func.generics
+ in
(* Instantiate *)
let tr_self = TraitRef trait_ref in
let fid : fun_id = FRegular id in
@@ -898,6 +899,12 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
log#ldebug
(lazy ("method:\n" ^ fun_decl_to_string ctx method_def));
(* Instantiate *)
+ (* When instantiating, we need to group the generics for the
+ trait ref and the generics for the method *)
+ let generics =
+ TypesUtils.merge_generic_args
+ trait_ref.trait_decl_ref.decl_generics func.generics
+ in
let regions_hierarchy =
LlbcAstUtils.FunIdMap.find (FRegular method_id)
ctx.fun_ctx.regions_hierarchies
@@ -1025,7 +1032,6 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) :
{
func = FunId (FRegular global.body);
generics = TypesUtils.empty_generic_args;
- trait_and_method_generic_args = None;
}
in
let call = { func = FnOpRegular func; args = []; dest } in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 667c5080..243cf67b 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -43,6 +43,8 @@ let fun_sig_to_string = Print.EvalCtx.fun_sig_to_string
let inst_fun_sig_to_string = Print.EvalCtx.inst_fun_sig_to_string
let ty_to_string = Print.EvalCtx.ty_to_string
let generic_args_to_string = Print.EvalCtx.generic_args_to_string
+let trait_ref_to_string = Print.EvalCtx.trait_ref_to_string
+let trait_decl_ref_to_string = Print.EvalCtx.trait_decl_ref_to_string
let fun_id_or_trait_method_ref_to_string =
Print.EvalCtx.fun_id_or_trait_method_ref_to_string
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 0c69bd05..36aa2cb9 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -531,6 +531,10 @@ module EvalCtx = struct
let env = eval_ctx_to_fmt_env ctx in
trait_ref_to_string env x
+ let trait_decl_ref_to_string (ctx : eval_ctx) (x : trait_decl_ref) : string =
+ let env = eval_ctx_to_fmt_env ctx in
+ trait_decl_ref_to_string env x
+
let trait_instance_id_to_string (ctx : eval_ctx) (x : trait_instance_id) :
string =
let env = eval_ctx_to_fmt_env ctx in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 21ca7f08..a401594d 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -159,14 +159,9 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
ty_to_string env true arg_ty ^ " -> " ^ ty_to_string env false ret_ty
in
if inside then "(" ^ ty ^ ")" else ty
- | TTraitType (trait_ref, generics, type_name) ->
+ | TTraitType (trait_ref, type_name) ->
let trait_ref = trait_ref_to_string env false trait_ref in
- let s =
- if generics = empty_generic_args then trait_ref ^ "::" ^ type_name
- else
- let generics = generic_args_to_string env generics in
- "(" ^ trait_ref ^ " " ^ generics ^ ")::" ^ type_name
- in
+ let s = trait_ref ^ "::" ^ type_name in
if inside then "(" ^ s ^ ")" else s
and generic_args_to_strings (env : fmt_env) (inside : bool)
@@ -624,14 +619,9 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string)
let field_s = adt_field_to_string env adt_id field_id in
(* Adopting an F*-like syntax *)
(ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, [])
- | TraitConst (trait_ref, generics, const_name) ->
+ | TraitConst (trait_ref, const_name) ->
let trait_ref = trait_ref_to_string env true trait_ref in
- let generics_s = generic_args_to_string env generics in
- let qualif =
- if generics <> empty_generic_args then
- "(" ^ trait_ref ^ generics_s ^ ")." ^ const_name
- else trait_ref ^ "." ^ const_name
- in
+ let qualif = trait_ref ^ "." ^ const_name in
(qualif, []))
| _ ->
(* "Regular" expression case *)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 33c23cc3..a735667e 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -283,7 +283,7 @@ type ty =
| TVar of type_var_id
| TLiteral of literal_type
| TArrow of ty * ty
- | TTraitType of trait_ref * generic_args * string
+ | TTraitType of trait_ref * string
(** The string is for the name of the associated type *)
and trait_ref = {
@@ -374,7 +374,6 @@ type generic_params = {
type trait_type_constraint = {
trait_ref : trait_ref;
- generics : generic_args;
type_name : trait_item_name;
ty : ty;
}
@@ -599,8 +598,7 @@ type qualif_id =
| Global of global_decl_id
| AdtCons of adt_cons_id (** A function or ADT constructor identifier *)
| Proj of projection (** Field projector *)
- | TraitConst of trait_ref * generic_args * string
- (** A trait associated constant *)
+ | TraitConst of trait_ref * string (** A trait associated constant *)
[@@deriving show]
(** An instantiated qualifier.
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index 80b67a54..0b589453 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -169,7 +169,7 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t)
(* Continue *)
explore_ty outer ty
| TRawPtr (ty, _) -> explore_ty outer ty
- | TTraitType (trait_ref, _generic_args, _) ->
+ | TTraitType (trait_ref, _) ->
(* The trait should reference a clause, and not an implementation
(otherwise it should have been normalized) *)
assert (
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 7252a020..79c03e58 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -251,8 +251,7 @@ and value_aggregate =
| VaCgValue of const_generic_var_id
(** This is used when evaluating a const generic value: in the interpreter,
we introduce a fresh symbolic value. *)
- | VaTraitConstValue of trait_ref * generic_args * string
- (** A trait constant value *)
+ | VaTraitConstValue of trait_ref * string (** A trait constant value *)
[@@deriving
show,
visitors
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 922f0375..27279327 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -474,10 +474,9 @@ let rec translate_sty (ty : T.ty) : ty =
let ty = translate ty in
let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
TAdt (TAssumed (TRawPtr mut), generics)
- | TTraitType (trait_ref, generics, type_name) ->
+ | TTraitType (trait_ref, type_name) ->
let trait_ref = translate_strait_ref trait_ref in
- let generics = translate_sgeneric_args generics in
- TTraitType (trait_ref, generics, type_name)
+ TTraitType (trait_ref, type_name)
| TArrow _ -> raise (Failure "TODO")
and translate_sgeneric_args (generics : T.generic_args) : generic_args =
@@ -497,11 +496,10 @@ let translate_trait_clause (clause : T.trait_clause) : trait_clause =
let translate_strait_type_constraint (ttc : T.trait_type_constraint) :
trait_type_constraint =
- let { T.trait_ref; generics; type_name; ty } = ttc in
+ let { T.trait_ref; type_name; ty } = ttc in
let trait_ref = translate_strait_ref trait_ref in
- let generics = translate_sgeneric_args generics in
let ty = translate_sty ty in
- { trait_ref; generics; type_name; ty }
+ { trait_ref; type_name; ty }
let translate_predicates (preds : T.predicates) : predicates =
let trait_type_constraints =
@@ -638,10 +636,9 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty =
let ty = translate ty in
let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
TAdt (TAssumed (TRawPtr mut), generics)
- | TTraitType (trait_ref, generics, type_name) ->
+ | TTraitType (trait_ref, type_name) ->
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
- let generics = translate_fwd_generic_args type_infos generics in
- TTraitType (trait_ref, generics, type_name)
+ TTraitType (trait_ref, type_name)
| TArrow _ -> raise (Failure "TODO")
and translate_fwd_generic_args (type_infos : type_infos)
@@ -737,16 +734,14 @@ let rec translate_back_ty (type_infos : type_infos)
| TRawPtr _ ->
(* TODO: not sure what to do here *)
None
- | TTraitType (trait_ref, generics, type_name) ->
- assert (generics.regions = []);
+ | TTraitType (trait_ref, type_name) ->
assert (
AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id);
if inside_mut then
- (* Translate the trait ref and the generics as "forward" generics -
+ (* Translate the trait ref as a "forward" trait ref -
we do not want to filter any type *)
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
- let generics = translate_fwd_generic_args type_infos generics in
- Some (TTraitType (trait_ref, generics, type_name))
+ Some (TTraitType (trait_ref, type_name))
else None
| TArrow _ -> raise (Failure "TODO")
@@ -2956,11 +2951,10 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
in
{ e = StructUpdate su; ty = var.ty }
| VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
- | VaTraitConstValue (trait_ref, generics, const_name) ->
+ | VaTraitConstValue (trait_ref, const_name) ->
let type_infos = ctx.type_ctx.type_infos in
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
- let generics = translate_fwd_generic_args type_infos generics in
- let qualif_id = TraitConst (trait_ref, generics, const_name) in
+ let qualif_id = TraitConst (trait_ref, const_name) in
let qualif = { id = qualif_id; generics = empty_generic_args } in
{ e = Qualif qualif; ty = var.ty }
in
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 48a3685b..fba1dfb0 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1086,7 +1086,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
let exe_dir = Filename.dirname Sys.argv.(0) in
let primitives_src_dest =
match !Config.backend with
- | FStar -> Some ("/backends/fstar/merge/Primitives.fst", "Primitives.fst")
+ | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
| Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
| Lean -> None
| HOL4 -> None
diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
index 28db59ec..f5dd7df4 100644
--- a/compiler/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
@@ -105,9 +105,8 @@ let generic_args_no_regions (x : generic_args) : bool =
(** Return [true] if the trait type constraint doesn't contain regions (including erased regions) *)
let trait_type_constraint_no_regions (x : trait_type_constraint) : bool =
try
- let { trait_ref; generics; type_name = _; ty } = x in
+ let { trait_ref; type_name = _; ty } = x in
raise_if_region_ty_visitor#visit_trait_ref () trait_ref;
- raise_if_region_ty_visitor#visit_generic_args () generics;
raise_if_region_ty_visitor#visit_ty () ty;
true
with Found -> false
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 19:18:55 +0000