Add support for the trait associated constants

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 *)