summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml13
-rw-r--r--compiler/InterpreterBorrows.ml2
-rw-r--r--compiler/InterpreterExpressions.ml40
-rw-r--r--compiler/InterpreterUtils.ml2
-rw-r--r--compiler/PrintPure.ml8
-rw-r--r--compiler/Pure.ml4
-rw-r--r--compiler/PureTypeCheck.ml1
-rw-r--r--compiler/ReorderDecls.ml4
-rw-r--r--compiler/SymbolicAst.ml8
-rw-r--r--compiler/SymbolicToPure.ml12
-rw-r--r--compiler/Values.ml2
11 files changed, 83 insertions, 13 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 8baa3c88..d000c447 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2544,7 +2544,18 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
| AdtCons adt_cons_id ->
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)
+ 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 "(";
+ 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
+ in
+ if use_brackets then F.pp_print_string fmt ")";
+ F.pp_print_string fmt ("." ^ name))
| _ ->
(* "Regular" expression *)
(* Open parentheses *)
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index f908d060..e97795a1 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -453,7 +453,7 @@ let give_back_symbolic_value (_config : C.config)
->
()
| FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate
- | ConstGeneric ->
+ | ConstGeneric | TraitConst ->
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 51f6ff05..29826233 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -271,9 +271,41 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
match cv.value with
| E.CLiteral lit ->
cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx
- | E.TraitConst (_trait_ref, _generics, _const_name) ->
- (* TODO *)
- raise (Failure "Unimplemented")
+ | E.TraitConst (trait_ref, generics, const_name) -> (
+ assert (generics = TypesUtils.mk_empty_generic_args);
+ match trait_ref.trait_id with
+ | T.TraitImpl _ ->
+ (* This shouldn't happen: if we refer to a concrete implementation, we
+ should directly refer to the top-level constant *)
+ raise (Failure "Unreachable")
+ | _ -> (
+ (* We refer to a constant defined in a local clause: simply
+ introduce a fresh symbolic value *)
+ let ctx0 = ctx in
+ (* Lookup the trait declaration to retrieve the type of the symbolic value *)
+ let trait_decl =
+ C.ctx_lookup_trait_decl ctx
+ trait_ref.trait_decl_ref.trait_decl_id
+ in
+ let _, (ty, _) =
+ List.find (fun (name, _) -> name = const_name) trait_decl.consts
+ in
+ (* Introduce a fresh symbolic value *)
+ let v = mk_fresh_symbolic_typed_value_from_ety V.TraitConst ty in
+ (* Continue the evaluation *)
+ let e = cf v ctx in
+ (* We have to wrap the generated expression *)
+ match e with
+ | None -> None
+ | Some e ->
+ Some
+ (SymbolicAst.IntroSymbolic
+ ( ctx0,
+ None,
+ value_as_symbolic v.value,
+ SymbolicAst.TraitConstValue
+ (trait_ref, generics, const_name),
+ e ))))
| E.CVar vid -> (
let ctx0 = ctx in
(* Lookup the const generic value *)
@@ -283,7 +315,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
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 *)
+ (* We have to wrap the generated expression *)
match e with
| None -> None
| Some e ->
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 1513465c..0986c53b 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -256,7 +256,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
else ()
| V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
| V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate
- | V.ConstGeneric ->
+ | V.ConstGeneric | V.TraitConst ->
()
end
in
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index fc39074d..c7f59ec9 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -733,6 +733,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
match app.e with
| Qualif qualif ->
(* Qualifier case *)
+ let ty_fmt = ast_to_type_formatter fmt in
(* Convert the qualifier identifier *)
let qualif_s =
match qualif.id with
@@ -751,9 +752,14 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
let field_s = adt_field_to_string value_fmt adt_id field_id in
(* Adopting an F*-like syntax *)
ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s
+ | TraitConst (trait_ref, generics, const_name) ->
+ let trait_ref = trait_ref_to_string ty_fmt true trait_ref in
+ let generics_s = generic_args_to_string ty_fmt generics in
+ if generics <> empty_generic_args then
+ "(" ^ trait_ref ^ generics_s ^ ")." ^ const_name
+ else trait_ref ^ "." ^ const_name
in
(* Convert the type instantiation *)
- let ty_fmt = ast_to_type_formatter fmt in
let generics = generic_args_to_strings ty_fmt true qualif.generics in
(* *)
(qualif_s, generics)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 6c9f41f1..81060c43 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -567,9 +567,11 @@ type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show]
type qualif_id =
| FunOrOp of fun_or_op_id (** A function or an operation *)
- | Global of GlobalDeclId.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 *)
[@@deriving show]
(** An instantiated qualifier.
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 27736ecb..b80ff72f 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -142,6 +142,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
match qualif.id with
| FunOrOp _ -> () (* TODO *)
| Global _ -> () (* TODO *)
+ | TraitConst _ -> () (* TODO *)
| Proj { adt_id = proj_adt_id; field_id } ->
(* Note we can only project fields of structures (not enumerations) *)
(* Deconstruct the projector type *)
diff --git a/compiler/ReorderDecls.ml b/compiler/ReorderDecls.ml
index fc4744bc..db646a87 100644
--- a/compiler/ReorderDecls.ml
+++ b/compiler/ReorderDecls.ml
@@ -38,7 +38,9 @@ let compute_body_fun_deps (e : texpression) : FunIdSet.t =
method! visit_qualif _ id =
match id.id with
- | FunOrOp (Unop _ | Binop _) | Global _ | AdtCons _ | Proj _ -> ()
+ | FunOrOp (Unop _ | Binop _)
+ | Global _ | AdtCons _ | Proj _ | TraitConst _ ->
+ ()
| FunOrOp (Fun fid) -> (
match fid with
| Pure _ -> ()
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 0f107897..b170ebe5 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -120,6 +120,9 @@ class ['self] iter_expression_base =
method visit_symbolic_expansion : 'env -> V.symbolic_expansion -> unit =
fun _ _ -> ()
+
+ method visit_etrait_ref : 'env -> T.etrait_ref -> unit = fun _ _ -> ()
+ method visit_egeneric_args : 'env -> T.egeneric_args -> unit = fun _ _ -> ()
end
(** **Rem.:** here, {!expression} is not at all equivalent to the expressions
@@ -174,7 +177,8 @@ type expression =
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).
+ (while losing precision of course). We also use it to introduce symbolic
+ values when evaluating constant generics, or trait constants.
The context is the evaluation context from before introducing the new
value. It has the same purpose as for the {!Return} case.
@@ -256,6 +260,8 @@ and value_aggregate =
| 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. *)
+ | TraitConstValue of T.etrait_ref * T.egeneric_args * string
+ (** A trait constant value *)
[@@deriving
show,
visitors
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 46eef953..3312e22d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2411,8 +2411,9 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
(* Translate the next expression *)
let next_e = translate_expression e ctx in
- (* Translate the value: there are two cases, depending on whether this
- is a "regular" let-binding or an array aggregate.
+ (* Translate the value: there are several cases, depending on whether this
+ is a "regular" let-binding, an array aggregate, a const generic or
+ a trait associated constant.
*)
let v =
match v with
@@ -2428,6 +2429,13 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
in
{ e = StructUpdate su; ty = var.ty }
| ConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
+ | TraitConstValue (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
+ let generics = translate_fwd_generic_args type_infos generics in
+ let qualif_id = TraitConst (trait_ref, generics, const_name) in
+ let qualif = { id = qualif_id; generics = empty_generic_args } in
+ { e = Qualif qualif; ty = var.ty }
in
(* Make the let-binding *)
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 58737557..de27e7a9 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -54,6 +54,8 @@ type sv_kind =
(** 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 *)
+ | TraitConst
+ (** A symbolic value we introduce when evaluating a trait associated constant *)
[@@deriving show, ord]
(** Ancestor for {!symbolic_value} iter visitor *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 03:26:37 +0000