diff options
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/AssociatedTypes.ml | 25 | ||||
-rw-r--r-- | compiler/Extract.ml | 137 | ||||
-rw-r--r-- | compiler/ExtractBase.ml | 2 | ||||
-rw-r--r-- | compiler/ExtractTypes.ml | 7 | ||||
-rw-r--r-- | compiler/InterpreterExpressions.ml | 53 | ||||
-rw-r--r-- | compiler/InterpreterStatements.ml | 52 | ||||
-rw-r--r-- | compiler/InterpreterUtils.ml | 2 | ||||
-rw-r--r-- | compiler/Print.ml | 4 | ||||
-rw-r--r-- | compiler/PrintPure.ml | 18 | ||||
-rw-r--r-- | compiler/Pure.ml | 26 | ||||
-rw-r--r-- | compiler/PureTypeCheck.ml | 4 | ||||
-rw-r--r-- | compiler/RegionsHierarchy.ml | 2 | ||||
-rw-r--r-- | compiler/SymbolicAst.ml | 5 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 75 | ||||
-rw-r--r-- | compiler/SynthesizeSymbolic.ml | 6 | ||||
-rw-r--r-- | compiler/Translate.ml | 3 | ||||
-rw-r--r-- | compiler/TypesUtils.ml | 3 |
17 files changed, 263 insertions, 161 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 054c8169..7b928566 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -51,9 +51,10 @@ let compute_norm_trait_types_from_preds that it would be enough to only visit the field [ty] of the trait type constraint, but for safety we visit all the fields *) assert (trait_type_constraint_no_regions c); - let trait_ty = TTraitType (c.trait_ref, c.generics, c.type_name) in + let { trait_ref; type_name; ty } : trait_type_constraint = c in + let trait_ty = TTraitType (trait_ref, type_name) in let trait_ty_ref = get_ref trait_ty in - let ty_ref = get_ref c.ty in + let ty_ref = get_ref ty in let new_repr = UnionFind.get ty_ref in let merged = UnionFind.union trait_ty_ref ty_ref in (* Not sure the set operation is necessary, but I want to control which @@ -72,9 +73,7 @@ let compute_norm_trait_types_from_preds List.filter_map (fun (k, v) -> match k with - | TTraitType (trait_ref, generics, type_name) -> - assert (generics = empty_generic_args); - Some ({ trait_ref; type_name }, v) + | TTraitType (trait_ref, type_name) -> Some ({ trait_ref; type_name }, v) | _ -> None) rbindings in @@ -225,20 +224,15 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = let inputs = List.map (norm_ctx_normalize_ty ctx) inputs in let output = norm_ctx_normalize_ty ctx output in TArrow (regions, inputs, output) - | TTraitType (trait_ref, generics, type_name) -> ( + | TTraitType (trait_ref, type_name) -> ( log#ldebug (lazy ("norm_ctx_normalize_ty:\n- trait type: " ^ ty_to_string ctx ty ^ "\n- trait_ref: " ^ trait_ref_to_string ctx trait_ref - ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref - ^ "\n- generics:\n" - ^ generic_args_to_string ctx generics)); + ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); (* Normalize and attempt to project the type from the trait ref *) let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in - let generics = norm_ctx_normalize_generic_args ctx generics in - (* For now, we don't support higher order types *) - assert (generics = empty_generic_args); let ty : ty = match trait_ref.trait_id with | TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ } @@ -284,7 +278,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); (* We can't project *) assert (trait_instance_id_is_local_clause trait_ref.trait_id); - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) in let tr : trait_type_ref = { trait_ref; type_name } in (* Lookup the representative, if there is *) @@ -484,11 +478,10 @@ and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx) let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx) (ttc : trait_type_constraint) : trait_type_constraint = - let { trait_ref; generics; type_name; ty } = ttc in + let { trait_ref; type_name; ty } : trait_type_constraint = ttc in let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in - let generics = norm_ctx_normalize_generic_args ctx generics in let ty = norm_ctx_normalize_ty ctx ty in - { trait_ref; generics; type_name; ty } + { trait_ref; type_name; ty } let mk_norm_ctx (ctx : eval_ctx) : norm_ctx = { diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 46f6a1ca..aa097a4f 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -185,9 +185,17 @@ let extract_adt_g_value | _ -> raise (Failure "Inconsistent typed value") (* Extract globals in the same way as variables *) -let extract_global (ctx : extraction_ctx) (fmt : F.formatter) - (id : A.GlobalDeclId.id) : unit = - F.pp_print_string fmt (ctx_get_global id ctx) +let extract_global (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) + (id : A.GlobalDeclId.id) (generics : generic_args) : unit = + let use_brackets = inside && generics <> empty_generic_args in + F.pp_open_hvbox fmt ctx.indent_incr; + if use_brackets then F.pp_print_string fmt "("; + (* Extract the global name *) + F.pp_print_string fmt (ctx_get_global id ctx); + (* Extract the generics *) + extract_generic_args ctx fmt TypeDeclId.Set.empty generics; + if use_brackets then F.pp_print_string fmt ")"; + F.pp_close_box fmt () (* Filter the generics of a function if it is builtin *) let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list) @@ -321,16 +329,15 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) match qualif.id with | FunOrOp fun_id -> extract_function_call ctx fmt inside fun_id qualif.generics args - | Global global_id -> extract_global ctx fmt global_id + | Global global_id -> + assert (args = []); + extract_global ctx fmt inside global_id qualif.generics | 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 - | 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; + | TraitConst (trait_ref, const_name) -> + 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 @@ -338,7 +345,6 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) let add_brackets (s : string) = if !backend = Coq then "(" ^ s ^ ")" else s in - if use_brackets then F.pp_print_string fmt ")"; F.pp_print_string fmt ("." ^ add_brackets name)) | _ -> (* "Regular" expression *) @@ -1695,7 +1701,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) of those declarations. See {!extract_global_decl} for more explanations. *) let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) - (kind : decl_kind) (name : string) (ty : ty) + (kind : decl_kind) (name : string) (generics : generic_params) + (type_params : string list) (cg_params : string list) + (trait_clauses : string list) (ty : ty) (extract_body : (F.formatter -> unit) Option.t) : unit = let is_opaque = Option.is_none extract_body in @@ -1712,9 +1720,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hvbox fmt 0; F.pp_open_hvbox fmt ctx.indent_incr; - (* Open "QUALIF NAME : TYPE =" box (depth=1) *) + (* Open "QUALIF NAME PARAMS : TYPE =" box (depth=1) *) F.pp_open_hovbox fmt ctx.indent_incr; - (* Print "QUALIF NAME " *) + (* Print "QUALIF NAME PARAMS " *) (match fun_decl_kind_to_qualif kind with | Some qualif -> F.pp_print_string fmt qualif; @@ -1723,6 +1731,12 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt name; F.pp_print_space fmt (); + (* Extract the generic parameters *) + let space = ref true in + extract_generic_params ctx fmt TypeDeclId.Set.empty ~space:(Some space) + generics type_params cg_params trait_clauses; + if not !space then F.pp_print_space fmt (); + (* Open ": TYPE =" box (depth=2) *) F.pp_open_hvbox fmt 0; (* Print ": " *) @@ -1779,7 +1793,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) but I could not find a better way. *) let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) - (name : string) (ty : ty) : unit = + (name : string) (generics : generic_params) (ty : ty) : unit = + (* TODO: non-empty generics *) + assert (generics = empty_generic_params); (* Open the definition boxe (depth=0) *) F.pp_open_hvbox fmt ctx.indent_incr; (* [val ..._def = new_constant ("...",] *) @@ -1819,58 +1835,94 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) and {!extract_fun_decl}. *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) - (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = + (global : global_decl) (body : fun_decl) (interface : bool) : unit = assert body.is_global_decl_body; assert (body.signature.inputs = []); - assert (body.signature.generics = empty_generic_params); (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; let name = if !Config.extract_external_name_patterns && not global.is_local then - Some global.name + Some global.llbc_name else None in extract_comment_with_span ctx fmt - [ "[" ^ name_to_string ctx global.name ^ "]" ] + [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] name global.meta.span; F.pp_print_space fmt (); let decl_name = ctx_get_global global.def_id ctx in let body_name = - ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body), None)) ctx + ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body_id), None)) ctx in - let decl_ty, body_ty = let ty = body.signature.output in if body.signature.fwd_info.effect_info.can_fail then (unwrap_result_ty ty, ty) else (ty, mk_result_ty ty) in + (* Add the type parameters *) + let ctx, type_params, cg_params, trait_clauses = + ctx_add_generic_params global.llbc_name global.llbc_generics global.generics + ctx + in match body.body with | None -> (* No body: only generate a [val x_c : u32] declaration *) let kind = if interface then Declared else Assumed in if !backend = HOL4 then - extract_global_decl_hol4_opaque ctx fmt decl_name decl_ty - else extract_global_decl_body_gen ctx fmt kind decl_name decl_ty None + extract_global_decl_hol4_opaque ctx fmt decl_name global.generics + decl_ty + else + extract_global_decl_body_gen ctx fmt kind decl_name global.generics + type_params cg_params trait_clauses decl_ty None | Some body -> (* There is a body *) (* Generate: [let x_body : result u32 = Return 3] *) - extract_global_decl_body_gen ctx fmt SingleNonRec body_name body_ty + extract_global_decl_body_gen ctx fmt SingleNonRec body_name + global.generics type_params cg_params trait_clauses body_ty (Some (fun fmt -> extract_texpression ctx fmt false body.body)); F.pp_print_break fmt 0 0; (* Generate: [let x_c : u32 = eval_global x_body] *) - extract_global_decl_body_gen ctx fmt SingleNonRec decl_name decl_ty + extract_global_decl_body_gen ctx fmt SingleNonRec decl_name + global.generics type_params cg_params trait_clauses decl_ty (Some (fun fmt -> - let body = + 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) + all_params + in + let use_brackets = all_params <> [] in + (* Extract the name *) + let before, after = match !backend with - | FStar | Lean -> "eval_global " ^ body_name - | Coq -> body_name ^ "%global" - | HOL4 -> "get_return_value " ^ body_name + | FStar | Lean -> + ( (fun () -> + F.pp_print_string fmt "eval_global"; + F.pp_print_space fmt ()), + fun () -> () ) + | Coq -> + ((fun () -> ()), fun () -> F.pp_print_string fmt "%global") + | HOL4 -> + ( (fun () -> + F.pp_print_string fmt "get_return_value"; + F.pp_print_space fmt ()), + fun () -> () ) in - F.pp_print_string fmt body)); + before (); + if use_brackets then F.pp_print_string fmt "("; + F.pp_print_string fmt body_name; + (* Extract the generic params *) + extract_params (); + if use_brackets then F.pp_print_string fmt ")"; + (* *) + after ())); (* Add a break to insert lines between declarations *) F.pp_print_break fmt 0 0 @@ -2589,18 +2641,39 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) * Extract the items *) let trait_decl_id = impl.impl_trait.trait_decl_id in + let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in + let trait_decl_provided_consts = + List.map (fun (_, (_, x)) -> x) trait_decl.consts + in (* The constants *) List.iter - (fun (name, (_, id)) -> + (fun (provided_id, (name, (_, id))) -> let item_name = ctx_get_trait_const trait_decl_id name ctx in + (* The parameters are not the same depending on whether the constant + is a provided constant or not *) + let print_params () = + if provided_id = Some id then + extract_generic_args ctx fmt TypeDeclId.Set.empty + impl.impl_trait.decl_generics + else + let all_params = + List.concat [ type_params; cg_params; trait_clauses ] + in + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + all_params + in let ty () = F.pp_print_space fmt (); - F.pp_print_string fmt (ctx_get_global id ctx) + F.pp_print_string fmt (ctx_get_global id ctx); + print_params () in extract_trait_impl_item ctx fmt item_name ty) - impl.consts; + (List.combine trait_decl_provided_consts impl.consts); (* The types *) List.iter diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 5e97cd21..297a1d22 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1682,7 +1682,7 @@ let ctx_compute_var_basename (ctx : extraction_ctx) (basename : string option) | TLiteral lty -> ( match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i") | TArrow _ -> "f" - | TTraitType (_, _, name) -> name_from_type_ident name) + | TTraitType (_, name) -> name_from_type_ident name) (** Generates a type variable basename. *) let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) : diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 9d4131d2..bbd5fae4 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -528,7 +528,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); extract_rec false ret_ty; if inside then F.pp_print_string fmt ")" - | TTraitType (trait_ref, generics, type_name) -> ( + | TTraitType (trait_ref, type_name) -> ( if !parameterize_trait_types then raise (Failure "Unimplemented") else let type_name = @@ -547,7 +547,6 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) *) match trait_ref.trait_id with | Self -> - assert (generics = empty_generic_args); assert (trait_ref.generics = empty_generic_args); extract_trait_instance_id_with_dot ctx fmt no_params_tys false trait_ref.trait_id; @@ -555,11 +554,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) | _ -> (* HOL4 doesn't have 1st class types *) assert (!backend <> HOL4); - let use_brackets = generics <> empty_generic_args in - if use_brackets then F.pp_print_string fmt "("; extract_trait_ref ctx fmt no_params_tys false trait_ref; - extract_generic_args ctx fmt no_params_tys generics; - if use_brackets then F.pp_print_string fmt ")"; F.pp_print_string fmt ("." ^ add_brackets type_name)) and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter) diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 8536b4ab..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 @@ -263,40 +262,24 @@ let eval_operand_no_reorganize (config : config) (op : operand) match cv.value with | CLiteral lit -> cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx - | CTraitConst (trait_ref, generics, const_name) -> ( - assert (generics = empty_generic_args); - 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, generics, const_name), - e )))) + | CTraitConst (trait_ref, const_name) -> ( + 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. diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 0cf8b88a..95a2956b 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -769,12 +769,8 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) ("trait method call:\n- call: " ^ call_to_string ctx call ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" ^ generic_args_to_string ctx func.generics - ^ "\n- trait and method generics:\n" - ^ generic_args_to_string ctx - (Option.get func.trait_and_method_generic_args))); - (* When instantiating, we need to group the generics for the trait ref - and the method *) - let generics = Option.get func.trait_and_method_generic_args in + ^ "\n- trait_ref.trait_decl_ref: " + ^ trait_decl_ref_to_string ctx trait_ref.trait_decl_ref)); (* Lookup the trait method signature - there are several possibilities depending on whethere we call a top-level trait method impl or the method from a local clause *) @@ -794,6 +790,11 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) | Some (_, id) -> (* This is a required method *) let method_def = ctx_lookup_fun_decl ctx id in + (* We have to concatenate the generics for the impl + and the generics for the method *) + let generics = + merge_generic_args trait_ref.generics func.generics + in (* Instantiate *) let tr_self = TraitRef trait_ref in let fid : fun_id = FRegular id in @@ -898,6 +899,12 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); (* Instantiate *) + (* When instantiating, we need to group the generics for the + trait ref and the generics for the method *) + let generics = + TypesUtils.merge_generic_args + trait_ref.trait_decl_ref.decl_generics func.generics + in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies @@ -942,9 +949,9 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = | Assign (p, rvalue) -> ( (* We handle global assignments separately *) match rvalue with - | Global gid -> + | Global (gid, generics) -> (* Evaluate the global *) - eval_global config p gid cf ctx + eval_global config p gid generics cf ctx | _ -> (* Evaluate the rvalue *) let cf_eval_rvalue = eval_rvalue_not_global config rvalue in @@ -1014,32 +1021,37 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = (* Compose and apply *) comp cc cf_eval_st cf ctx -and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) : - st_cm_fun = +and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) + (generics : generic_args) : st_cm_fun = fun cf ctx -> let global = ctx_lookup_global_decl ctx gid in match config.mode with | ConcreteMode -> - (* Treat the evaluation of the global as a call to the global body (without arguments) *) - let func = - { - func = FunId (FRegular global.body); - generics = TypesUtils.empty_generic_args; - trait_and_method_generic_args = None; - } - in + (* Treat the evaluation of the global as a call to the global body *) + let func = { func = FunId (FRegular global.body); generics } in let call = { func = FnOpRegular func; args = []; dest } in (eval_transparent_function_call_concrete config global.body call) cf ctx | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) assert (ty_no_regions global.ty); - let sval = mk_fresh_symbolic_value global.ty in + (* Instantiate the type *) + (* There shouldn't be any reference to Self *) + let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in + let generics = Subst.generic_args_erase_regions generics in + let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = + Subst.make_subst_from_generics global.generics generics tr_self + in + let ty = + Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self + global.ty + in + let sval = mk_fresh_symbolic_value ty in let cc = assign_to_place config (mk_typed_value_from_symbolic_value sval) dest in let e = cc (cf Unit) ctx in - S.synthesize_global_eval gid sval e + S.synthesize_global_eval gid generics sval e (** Evaluate a switch *) and eval_switch (config : config) (switch : switch) : st_cm_fun = diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 667c5080..243cf67b 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -43,6 +43,8 @@ let fun_sig_to_string = Print.EvalCtx.fun_sig_to_string let inst_fun_sig_to_string = Print.EvalCtx.inst_fun_sig_to_string let ty_to_string = Print.EvalCtx.ty_to_string let generic_args_to_string = Print.EvalCtx.generic_args_to_string +let trait_ref_to_string = Print.EvalCtx.trait_ref_to_string +let trait_decl_ref_to_string = Print.EvalCtx.trait_decl_ref_to_string let fun_id_or_trait_method_ref_to_string = Print.EvalCtx.fun_id_or_trait_method_ref_to_string diff --git a/compiler/Print.ml b/compiler/Print.ml index 0c69bd05..36aa2cb9 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -531,6 +531,10 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in trait_ref_to_string env x + let trait_decl_ref_to_string (ctx : eval_ctx) (x : trait_decl_ref) : string = + let env = eval_ctx_to_fmt_env ctx in + trait_decl_ref_to_string env x + let trait_instance_id_to_string (ctx : eval_ctx) (x : trait_instance_id) : string = let env = eval_ctx_to_fmt_env ctx in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 21ca7f08..a401594d 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -159,14 +159,9 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string = ty_to_string env true arg_ty ^ " -> " ^ ty_to_string env false ret_ty in if inside then "(" ^ ty ^ ")" else ty - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = trait_ref_to_string env false trait_ref in - let s = - if generics = empty_generic_args then trait_ref ^ "::" ^ type_name - else - let generics = generic_args_to_string env generics in - "(" ^ trait_ref ^ " " ^ generics ^ ")::" ^ type_name - in + let s = trait_ref ^ "::" ^ type_name in if inside then "(" ^ s ^ ")" else s and generic_args_to_strings (env : fmt_env) (inside : bool) @@ -624,14 +619,9 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string) let field_s = adt_field_to_string env adt_id field_id in (* Adopting an F*-like syntax *) (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, []) - | TraitConst (trait_ref, generics, const_name) -> + | TraitConst (trait_ref, const_name) -> let trait_ref = trait_ref_to_string env true trait_ref in - let generics_s = generic_args_to_string env generics in - let qualif = - if generics <> empty_generic_args then - "(" ^ trait_ref ^ generics_s ^ ")." ^ const_name - else trait_ref ^ "." ^ const_name - in + let qualif = trait_ref ^ "." ^ const_name in (qualif, [])) | _ -> (* "Regular" expression case *) diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 33c23cc3..cf6710aa 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -283,7 +283,7 @@ type ty = | TVar of type_var_id | TLiteral of literal_type | TArrow of ty * ty - | TTraitType of trait_ref * generic_args * string + | TTraitType of trait_ref * string (** The string is for the name of the associated type *) and trait_ref = { @@ -374,7 +374,6 @@ type generic_params = { type trait_type_constraint = { trait_ref : trait_ref; - generics : generic_args; type_name : trait_item_name; ty : ty; } @@ -599,8 +598,7 @@ type qualif_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 *) + | TraitConst of trait_ref * string (** A trait associated constant *) [@@deriving show] (** An instantiated qualifier. @@ -1089,6 +1087,26 @@ type fun_decl = { } [@@deriving show] +type global_decl = { + meta : meta; + def_id : GlobalDeclId.id; + is_local : bool; + llbc_name : llbc_name; (** The original LLBC name. *) + name : string; + (** We use the name only for printing purposes (for debugging): + the name used at extraction time will be derived from the + llbc_name. + *) + llbc_generics : Types.generic_params; + (** See the comment for [llbc_generics] in fun_decl. *) + generics : generic_params; + preds : predicates; + ty : ty; + kind : item_kind; + body_id : FunDeclId.id; +} +[@@deriving show] + type trait_decl = { def_id : trait_decl_id; is_local : bool; diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index a989fd3b..fc94fa4c 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -208,7 +208,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = get_adt_field_types ctx.type_decls adt_id variant_id adt_generics in List.iter - (fun (fid, fe) -> + (fun ((fid, fe) : _ * texpression) -> let expected_field_ty = FieldId.nth expected_field_tys fid in assert (expected_field_ty = fe.ty); check_texpression ctx fe) @@ -218,7 +218,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = Collections.List.to_cons_nil adt_generics.types in List.iter - (fun (_, fe) -> + (fun ((_, fe) : _ * texpression) -> assert (expected_field_ty = fe.ty); check_texpression ctx fe) supd.updates diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 80b67a54..0b589453 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -169,7 +169,7 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) (* Continue *) explore_ty outer ty | TRawPtr (ty, _) -> explore_ty outer ty - | TTraitType (trait_ref, _generic_args, _) -> + | TTraitType (trait_ref, _) -> (* The trait should reference a clause, and not an implementation (otherwise it should have been normalized) *) assert ( diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 7252a020..cc74a16b 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -141,7 +141,7 @@ type expression = The context is the evaluation context from after evaluating the asserted value. It has the same purpose as for the {!Return} case. *) - | EvalGlobal of global_decl_id * symbolic_value * expression + | EvalGlobal of global_decl_id * generic_args * symbolic_value * expression (** Evaluate a global to a fresh symbolic value *) | Assertion of Contexts.eval_ctx * typed_value * expression (** An assertion. @@ -251,8 +251,7 @@ and value_aggregate = | VaCgValue of const_generic_var_id (** This is used when evaluating a const generic value: in the interpreter, we introduce a fresh symbolic value. *) - | VaTraitConstValue of trait_ref * generic_args * string - (** A trait constant value *) + | VaTraitConstValue of trait_ref * string (** A trait constant value *) [@@deriving show, visitors diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 922f0375..58fb6d04 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -474,10 +474,9 @@ let rec translate_sty (ty : T.ty) : ty = let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = translate_strait_ref trait_ref in - let generics = translate_sgeneric_args generics in - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) | TArrow _ -> raise (Failure "TODO") and translate_sgeneric_args (generics : T.generic_args) : generic_args = @@ -497,11 +496,10 @@ let translate_trait_clause (clause : T.trait_clause) : trait_clause = let translate_strait_type_constraint (ttc : T.trait_type_constraint) : trait_type_constraint = - let { T.trait_ref; generics; type_name; ty } = ttc in + let { T.trait_ref; type_name; ty } = ttc in let trait_ref = translate_strait_ref trait_ref in - let generics = translate_sgeneric_args generics in let ty = translate_sty ty in - { trait_ref; generics; type_name; ty } + { trait_ref; type_name; ty } let translate_predicates (preds : T.predicates) : predicates = let trait_type_constraints = @@ -638,10 +636,9 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = translate_fwd_trait_ref type_infos trait_ref in - let generics = translate_fwd_generic_args type_infos generics in - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) | TArrow _ -> raise (Failure "TODO") and translate_fwd_generic_args (type_infos : type_infos) @@ -737,16 +734,14 @@ let rec translate_back_ty (type_infos : type_infos) | TRawPtr _ -> (* TODO: not sure what to do here *) None - | TTraitType (trait_ref, generics, type_name) -> - assert (generics.regions = []); + | TTraitType (trait_ref, type_name) -> assert ( AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id); if inside_mut then - (* Translate the trait ref and the generics as "forward" generics - + (* Translate the trait ref as a "forward" trait ref - we do not want to filter any type *) let trait_ref = translate_fwd_trait_ref type_infos trait_ref in - let generics = translate_fwd_generic_args type_infos generics in - Some (TTraitType (trait_ref, generics, type_name)) + Some (TTraitType (trait_ref, type_name)) else None | TArrow _ -> raise (Failure "TODO") @@ -1895,7 +1890,8 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = | Panic -> translate_panic ctx | FunCall (call, e) -> translate_function_call call e ctx | EndAbstraction (ectx, abs, e) -> translate_end_abstraction ectx abs e ctx - | EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx + | EvalGlobal (gid, generics, sv, e) -> + translate_global_eval gid generics sv e ctx | Assertion (ectx, v, e) -> translate_assertion ectx v e ctx | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx | IntroSymbolic (ectx, p, sv, v, e) -> @@ -2667,11 +2663,12 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) (* Create the let-binding *) mk_let effect_info.can_fail output call next_e) -and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value) - (e : S.expression) (ctx : bs_ctx) : texpression = +and translate_global_eval (gid : A.GlobalDeclId.id) (generics : T.generic_args) + (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression = let ctx, var = fresh_var_for_symbolic_value sval ctx in let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in - let global_expr = { id = Global gid; generics = empty_generic_args } in + let generics = ctx_translate_fwd_generic_args ctx generics in + let global_expr = { id = Global gid; generics } in (* We use translate_fwd_ty to translate the global type *) let ty = ctx_translate_fwd_ty ctx decl.ty in let gval = { e = Qualif global_expr; ty } in @@ -2956,11 +2953,10 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) in { e = StructUpdate su; ty = var.ty } | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty } - | VaTraitConstValue (trait_ref, generics, const_name) -> + | VaTraitConstValue (trait_ref, const_name) -> let type_infos = ctx.type_ctx.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 = TraitConst (trait_ref, const_name) in let qualif = { id = qualif_id; generics = empty_generic_args } in { e = Qualif qualif; ty = var.ty } in @@ -3844,3 +3840,40 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) required_methods; provided_methods; } + +let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : + global_decl = + let { + A.meta; + def_id; + is_local; + name = llbc_name; + generics = llbc_generics; + preds; + ty; + kind; + body = body_id; + } = + decl + in + let name = + Print.Types.name_to_string + (Print.Contexts.decls_ctx_to_fmt_env ctx) + llbc_name + in + let generics = translate_generic_params llbc_generics in + let preds = translate_predicates preds in + let ty = translate_fwd_ty ctx.type_ctx.type_infos ty in + { + meta; + def_id; + is_local; + llbc_name; + name; + llbc_generics; + generics; + preds; + ty; + kind; + body_id; + } diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 20bc107e..a42c43ac 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -119,9 +119,9 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) FunCall (call, e)) e -let synthesize_global_eval (gid : GlobalDeclId.id) (dest : symbolic_value) - (e : expression option) : expression option = - Option.map (fun e -> EvalGlobal (gid, dest, e)) e +let synthesize_global_eval (gid : GlobalDeclId.id) (generics : generic_args) + (dest : symbolic_value) (e : expression option) : expression option = + Option.map (fun e -> EvalGlobal (gid, generics, dest, e)) e let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref) (call_id : FunCallId.id) (ctx : Contexts.eval_ctx) (sg : fun_sig) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 48a3685b..9af3c71b 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -469,6 +469,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) groups are always singletons, so the [extract_global_decl] function takes care of generating the delimiters. *) + let global = SymbolicToPure.translate_global ctx.trans_ctx global in Extract.extract_global_decl ctx fmt global body config.interface (** Utility. @@ -1086,7 +1087,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : let exe_dir = Filename.dirname Sys.argv.(0) in let primitives_src_dest = match !Config.backend with - | FStar -> Some ("/backends/fstar/merge/Primitives.fst", "Primitives.fst") + | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst") | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v") | Lean -> None | HOL4 -> None diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml index 28db59ec..f5dd7df4 100644 --- a/compiler/TypesUtils.ml +++ b/compiler/TypesUtils.ml @@ -105,9 +105,8 @@ let generic_args_no_regions (x : generic_args) : bool = (** Return [true] if the trait type constraint doesn't contain regions (including erased regions) *) let trait_type_constraint_no_regions (x : trait_type_constraint) : bool = try - let { trait_ref; generics; type_name = _; ty } = x in + let { trait_ref; type_name = _; ty } = x in raise_if_region_ty_visitor#visit_trait_ref () trait_ref; - raise_if_region_ty_visitor#visit_generic_args () generics; raise_if_region_ty_visitor#visit_ty () ty; true with Found -> false |