diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 8 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 49 |
2 files changed, 22 insertions, 35 deletions
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. |