From c6b88a2e54b7697262ad3677ad7500471c68e332 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 10 Sep 2023 21:07:06 +0200
Subject: Add support for the trait associated constants

---
 compiler/SymbolicToPure.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

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 *)
-- 
cgit v1.2.3