From 84066ffa2a0d3d620a7b0776e251052f1876dce9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 18 Mar 2024 01:52:55 +0100
Subject: Fix the extraction of trait constants

---
 compiler/Extract.ml                |  8 ++++---
 compiler/InterpreterExpressions.ml | 49 +++++++++++++-------------------------
 2 files changed, 22 insertions(+), 35 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 3c5ea15b..667d269a 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -337,7 +337,7 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       | Proj proj ->
           extract_field_projector ctx fmt inside app proj qualif.generics args
       | TraitConst (trait_ref, const_name) ->
-          extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref;
+          extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref;
           let name =
             ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id
               const_name ctx
@@ -1888,13 +1888,15 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
         global.generics type_params cg_params trait_clauses decl_ty
         (Some
            (fun fmt ->
-             let all_params = [ type_params; cg_params; trait_clauses ] in
+             let all_params =
+               List.concat [ type_params; cg_params; trait_clauses ]
+             in
              let extract_params () =
                List.iter
                  (fun p ->
                    F.pp_print_space fmt ();
                    F.pp_print_string fmt p)
-                 (List.concat all_params)
+                 all_params
              in
              let use_brackets = all_params <> [] in
              (* Extract the name *)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index dc100fe3..afbf4605 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -1,6 +1,5 @@
 open Types
 open Values
-open LlbcAst
 open Scalars
 open Expressions
 open Utils
@@ -264,37 +263,23 @@ let eval_operand_no_reorganize (config : config) (op : operand)
       | CLiteral lit ->
           cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx
       | CTraitConst (trait_ref, const_name) -> (
-          match trait_ref.trait_id with
-          | 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 =
-                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 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.VaTraitConstValue (trait_ref, const_name),
-                         e ))))
+          let ctx0 = ctx in
+          (* Simply introduce a fresh symbolic value *)
+          let ty = cv.ty in
+          let v = mk_fresh_symbolic_typed_value ty in
+          (* Continue the evaluation *)
+          let e = cf v ctx in
+          (* Wrap the generated expression *)
+          match e with
+          | None -> None
+          | Some e ->
+              Some
+                (SymbolicAst.IntroSymbolic
+                   ( ctx0,
+                     None,
+                     value_as_symbolic v.value,
+                     SymbolicAst.VaTraitConstValue (trait_ref, const_name),
+                     e )))
       | CVar vid -> (
           let ctx0 = ctx in
           (* In concrete mode: lookup the const generic value.
-- 
cgit v1.2.3