diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 672 |
1 files changed, 390 insertions, 282 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 70ef5e3d..a3d96023 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -5,6 +5,7 @@ module T = Types module A = LlbcAst module SA = SymbolicAst module Micro = PureMicroPasses +module C = Contexts open PureUtils open TranslateCore @@ -28,18 +29,12 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl) ("translate_function_to_symbolics: " ^ Print.fun_name_to_string fdef.A.name)); - let { type_context; fun_context; global_context } = trans_ctx in - let fun_context = { C.fun_decls = fun_context.fun_decls } in - match fdef.body with | None -> None | Some _ -> (* Evaluate *) let synthesize = true in - let inputs, symb = - evaluate_function_symbolic synthesize type_context fun_context - global_context fdef - in + let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in Some (inputs, Option.get symb) (** Translate a function, by generating its forward and backward translations. @@ -57,7 +52,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (lazy ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name)); - let { type_context; fun_context; global_context } = trans_ctx in let def_id = fdef.def_id in (* Compute the symbolic ASTs, if the function is transparent *) @@ -67,7 +61,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Initialize the context *) let forward_sig = - RegularFunIdNotLoopMap.find (A.Regular def_id, None) fun_sigs + RegularFunIdNotLoopMap.find (E.Regular def_id, None) fun_sigs in let sv_to_var = V.SymbolicValueId.Map.empty in let var_counter = Pure.VarId.generator_zero in @@ -82,25 +76,25 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (List.filter_map (fun (tid, g) -> match g with Charon.GAst.NonRec _ -> None | Rec _ -> Some tid) - (T.TypeDeclId.Map.bindings trans_ctx.type_context.type_decls_groups)) + (T.TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups)) in let type_context = { - SymbolicToPure.type_infos = type_context.type_infos; - llbc_type_decls = type_context.type_decls; + SymbolicToPure.type_infos = trans_ctx.type_ctx.type_infos; + llbc_type_decls = trans_ctx.type_ctx.type_decls; type_decls = pure_type_decls; recursive_decls = recursive_type_decls; } in let fun_context = { - SymbolicToPure.llbc_fun_decls = fun_context.fun_decls; + SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls; fun_sigs; - fun_infos = fun_context.fun_infos; + fun_infos = trans_ctx.fun_ctx.fun_infos; } in let global_context = - { SymbolicToPure.llbc_global_decls = global_context.global_decls } + { SymbolicToPure.llbc_global_decls = trans_ctx.global_ctx.global_decls } in (* Compute the set of loops, and find better ids for them (starting at 0). @@ -148,6 +142,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx) type_context; fun_context; global_context; + trait_decls_ctx = trans_ctx.trait_decls_ctx.trait_decls; + trait_impls_ctx = trans_ctx.trait_impls_ctx.trait_impls; fun_decl = fdef; forward_inputs = []; (* Empty for now *) @@ -204,7 +200,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Initialize the context - note that the ret_ty is not really * useful as we don't translate a body *) let backward_sg = - RegularFunIdNotLoopMap.find (A.Regular def_id, Some back_id) fun_sigs + RegularFunIdNotLoopMap.find (Regular def_id, Some back_id) fun_sigs in let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in @@ -215,7 +211,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) variables required by the backward function. *) let backward_sg = - RegularFunIdNotLoopMap.find (A.Regular def_id, Some back_id) fun_sigs + RegularFunIdNotLoopMap.find (Regular def_id, Some back_id) fun_sigs in (* We need to ignore the forward inputs, and the state input (if there is) *) let backward_inputs = @@ -274,21 +270,18 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Return *) (pure_forward, pure_backwards) +(* TODO: factor out the return type *) let translate_crate_to_pure (crate : A.crate) : - trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list = + trans_ctx + * Pure.type_decl list + * pure_fun_translation list + * Pure.trait_decl list + * Pure.trait_impl list = (* Debug *) log#ldebug (lazy "translate_crate_to_pure"); - (* Compute the type and function contexts *) - let type_context, fun_context, global_context = - compute_type_fun_global_contexts crate - in - let fun_infos = - FA.analyze_module crate fun_context.C.fun_decls - global_context.C.global_decls !Config.use_state - in - let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in - let trans_ctx = { type_context; fun_context; global_context } in + (* Compute the translation context *) + let trans_ctx = compute_contexts crate in (* Translate all the type definitions *) let type_decls = @@ -304,9 +297,11 @@ let translate_crate_to_pure (crate : A.crate) : (* Translate all the function *signatures* *) let assumed_sigs = List.map - (fun (id, sg, _, _) -> - (A.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg)) - Assumed.assumed_infos + (fun (info : Assumed.assumed_fun_info) -> + ( E.Assumed info.fun_id, + List.map (fun _ -> None) info.fun_sig.inputs, + info.fun_sig )) + Assumed.assumed_fun_infos in let local_sigs = List.map @@ -319,14 +314,11 @@ let translate_crate_to_pure (crate : A.crate) : (fun (v : A.var) -> v.name) (LlbcAstUtils.fun_body_get_input_vars body) in - (A.Regular fdef.def_id, input_names, fdef.signature)) + (E.Regular fdef.def_id, input_names, fdef.signature)) (A.FunDeclId.Map.values crate.functions) in let sigs = List.append assumed_sigs local_sigs in - let fun_sigs = - SymbolicToPure.translate_fun_signatures fun_context.fun_infos - type_context.type_infos sigs - in + let fun_sigs = SymbolicToPure.translate_fun_signatures trans_ctx sigs in (* Translate all the *transparent* functions *) let pure_translations = @@ -335,28 +327,38 @@ let translate_crate_to_pure (crate : A.crate) : (A.FunDeclId.Map.values crate.functions) in + (* Translate the trait declarations *) + let type_infos = trans_ctx.type_ctx.type_infos in + let trait_decls = + List.map + (SymbolicToPure.translate_trait_decl type_infos) + (T.TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) + in + + (* Translate the trait implementations *) + let trait_impls = + List.map + (SymbolicToPure.translate_trait_impl type_infos) + (T.TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) + in + (* Apply the micro-passes *) let pure_translations = Micro.apply_passes_to_pure_fun_translations trans_ctx pure_translations in (* Return *) - (trans_ctx, type_decls, pure_translations) - -(** Extraction context *) -type gen_ctx = { - crate : A.crate; - extract_ctx : ExtractBase.extraction_ctx; - trans_types : Pure.type_decl Pure.TypeDeclId.Map.t; - trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t; - functions_with_decreases_clause : PureUtils.FunLoopIdSet.t; -} + (trans_ctx, type_decls, pure_translations, trait_decls, trait_impls) + +type gen_ctx = ExtractBase.extraction_ctx type gen_config = { extract_types : bool; extract_decreases_clauses : bool; extract_template_decreases_clauses : bool; extract_fun_decls : bool; + extract_trait_decls : bool; + extract_trait_impls : bool; extract_transparent : bool; (** If [true], extract the transparent declarations, otherwise ignore. *) extract_opaque : bool; @@ -383,21 +385,23 @@ type gen_config = { test_trans_unit_functions : bool; } -(** Returns the pair: (has opaque type decls, has opaque fun decls) *) -let module_has_opaque_decls (ctx : gen_ctx) : bool * bool = - let has_opaque_types = - Pure.TypeDeclId.Map.exists - (fun _ (d : Pure.type_decl) -> - match d.kind with Opaque -> true | _ -> false) - ctx.trans_types - in - let has_opaque_funs = - A.FunDeclId.Map.exists - (fun _ ((_, ((t_fwd, _), _)) : bool * pure_fun_translation) -> - Option.is_none t_fwd.body) - ctx.trans_funs +(** Returns the pair: (has opaque type decls, has opaque fun decls). + + [filter_assumed]: if [true], do not consider as opaque the external definitions + that we will map to definitions from the standard library. + *) +let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) : + bool * bool = + let types, funs = + LlbcAstUtils.crate_get_opaque_non_builtin_decls ctx.crate filter_assumed in - (has_opaque_types, has_opaque_funs) + log#ldebug + (lazy + ("Opaque decls:" ^ "\n- types:\n" + ^ String.concat ",\n" (List.map T.show_type_decl types) + ^ "\n- functions:\n" + ^ String.concat ",\n" (List.map A.show_fun_decl funs))); + (types <> [], funs <> []) (** Export a type declaration. @@ -423,15 +427,19 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (true, kind) in (* Extract, if the config instructs to do so (depending on whether the type - * is opaque or not) *) - if + is opaque or not). Remark: we don't check if the definitions are builtin + here but in the function [export_types_group]: the reason is that if one + definition in the group is builtin, then we must check that all the + definitions are marked builtin *) + let extract = (is_opaque && config.extract_opaque) || ((not is_opaque) && config.extract_transparent) - then ( + in + if extract then ( if extract_decl then - Extract.extract_type_decl ctx.extract_ctx fmt type_decl_group kind def; + Extract.extract_type_decl ctx fmt type_decl_group kind def; if extract_extra_info then - Extract.extract_type_decl_extra_info ctx.extract_ctx fmt kind def) + Extract.extract_type_decl_extra_info ctx fmt kind def) (** Export a group of types. @@ -462,41 +470,58 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids in - (* Extract the type declarations. - - Because some declaration groups are delimited, we wrap the declarations - between [{start,end}_type_decl_group]. + (* Check if the definition are builtin - if yes they must be ignored. + Note that if one definition in the group is builtin, then all the + definitions must be builtin *) + let builtin = + let open ExtractBuiltin in + let types_map = builtin_types_map () in + List.map + (fun (def : Pure.type_decl) -> + let sname = name_to_simple_name def.name in + SimpleNameMap.find_opt sname types_map <> None) + defs + in - Ex.: - ==== - When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate - the [Datatype] and [End] delimiters in the snippet of code below: + if List.exists (fun b -> b) builtin then + (* Sanity check *) + assert (List.for_all (fun b -> b) builtin) + else ( + (* Extract the type declarations. + + Because some declaration groups are delimited, we wrap the declarations + between [{start,end}_type_decl_group]. + + Ex.: + ==== + When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate + the [Datatype] and [End] delimiters in the snippet of code below: + + {[ + Datatype: + tree = + TLeaf 'a + | TNode node ; + + node = + Node (tree list) + End + ]} + *) + Extract.start_type_decl_group ctx fmt is_rec defs; + List.iteri + (fun i def -> + let kind = kind_from_index i in + export_type_decl kind def) + defs; + Extract.end_type_decl_group fmt is_rec defs; - {[ - Datatype: - tree = - TLeaf 'a - | TNode node ; - - node = - Node (tree list) - End - ]} - *) - Extract.start_type_decl_group ctx.extract_ctx fmt is_rec defs; - List.iteri - (fun i def -> - let kind = kind_from_index i in - export_type_decl kind def) - defs; - Extract.end_type_decl_group fmt is_rec defs; - - (* Export the extra information (ex.: [Arguments] instructions in Coq) *) - List.iteri - (fun i def -> - let kind = kind_from_index i in - export_type_extra_info kind def) - defs + (* Export the extra information (ex.: [Arguments] instructions in Coq) *) + List.iteri + (fun i def -> + let kind = kind_from_index i in + export_type_extra_info kind def) + defs) (** Export a global declaration. @@ -504,26 +529,34 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) *) let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (id : A.GlobalDeclId.id) : unit = - let global_decls = ctx.extract_ctx.trans_ctx.global_context.global_decls in + let global_decls = ctx.trans_ctx.global_ctx.global_decls in let global = A.GlobalDeclId.Map.find id global_decls in - let _, ((body, loop_fwds), body_backs) = - A.FunDeclId.Map.find global.body_id ctx.trans_funs - in - assert (body_backs = []); - assert (loop_fwds = []); + let trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in + assert (trans.fwd.loops = []); + assert (trans.backs = []); + let body = trans.fwd.f in let is_opaque = Option.is_none body.Pure.body in - if + (* Check if we extract the global *) + let extract = config.extract_globals && (((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque)) - then + in + (* Check if it is a builtin global - if yes, we ignore it because we + map the definition to one in the standard library *) + let open ExtractBuiltin in + let sname = name_to_simple_name global.name in + let extract = + extract && SimpleNameMap.find_opt sname builtin_globals_map = None + in + if extract then (* We don't wrap global declaration groups between calls to functions [{start, end}_global_decl_group] (which don't exist): global declaration groups are always singletons, so the [extract_global_decl] function takes care of generating the delimiters. *) - Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface + Extract.extract_global_decl ctx fmt global body config.interface (** Utility. @@ -604,14 +637,13 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) then Some (fun () -> - Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause - def) + Extract.extract_fun_decl ctx fmt kind has_decr_clause def) else None) decls in let extract_defs = List.filter_map (fun x -> x) extract_defs in if extract_defs <> [] then ( - Extract.start_fun_decl_group ctx.extract_ctx fmt is_rec decls; + Extract.start_fun_decl_group ctx fmt is_rec decls; List.iter (fun f -> f ()) extract_defs; Extract.end_fun_decl_group fmt is_rec decls) @@ -621,82 +653,137 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) check if the forward and backward functions are mutually recursive. *) let export_functions_group (fmt : Format.formatter) (config : gen_config) - (ctx : gen_ctx) (pure_ls : (bool * pure_fun_translation) list) : unit = - (* Utility to check a function has a decrease clause *) - let has_decreases_clause (def : Pure.fun_decl) : bool = - PureUtils.FunLoopIdSet.mem (def.def_id, def.loop_id) - ctx.functions_with_decreases_clause + (ctx : gen_ctx) (pure_ls : pure_fun_translation list) : unit = + (* Check if the definition are builtin - if yes they must be ignored. + Note that if one definition in the group is builtin, then all the + definitions must be builtin *) + let builtin = + let open ExtractBuiltin in + let funs_map = builtin_funs_map () in + List.map + (fun (trans : pure_fun_translation) -> + let sname = name_to_simple_name trans.fwd.f.basename in + SimpleNameMap.find_opt sname funs_map <> None) + pure_ls in - (* Extract the decrease clauses template bodies *) - if config.extract_template_decreases_clauses then - List.iter - (fun (_, ((fwd, loop_fwds), _)) -> - (* We only generate decreases clauses for the forward functions, because - the termination argument should only depend on the forward inputs. - The backward functions thus use the same decreases clauses as the - forward function. - - Rem.: we might filter backward functions in {!PureMicroPasses}, but - we don't remove forward functions. Instead, we remember if we should - filter those functions at extraction time with a boolean (see the - type of the [pure_ls] input parameter). - *) - let extract_decrease decl = - let has_decr_clause = has_decreases_clause decl in - if has_decr_clause then - match !Config.backend with - | Lean -> - Extract.extract_template_lean_termination_and_decreasing - ctx.extract_ctx fmt decl - | FStar -> - Extract.extract_template_fstar_decreases_clause ctx.extract_ctx - fmt decl - | Coq -> - raise (Failure "Coq doesn't have decreases/termination clauses") - | HOL4 -> - raise - (Failure "HOL4 doesn't have decreases/termination clauses") - in - extract_decrease fwd; - List.iter extract_decrease loop_fwds) - pure_ls; - - (* Concatenate the function definitions, filtering the useless forward - * functions. *) - let decls = - List.concat - (List.map - (fun (keep_fwd, ((fwd, fwd_loops), (back_ls : fun_and_loops list))) -> - let fwd = if keep_fwd then List.append fwd_loops [ fwd ] else [] in - let back : Pure.fun_decl list = - List.concat - (List.map - (fun (back, loop_backs) -> List.append loop_backs [ back ]) - back_ls) - in - List.append fwd back) - pure_ls) - in + if List.exists (fun b -> b) builtin then + (* Sanity check *) + assert (List.for_all (fun b -> b) builtin) + else + (* Utility to check a function has a decrease clause *) + let has_decreases_clause (def : Pure.fun_decl) : bool = + PureUtils.FunLoopIdSet.mem (def.def_id, def.loop_id) + ctx.functions_with_decreases_clause + in - (* Extract the function definitions *) - (if config.extract_fun_decls then - (* Group the mutually recursive definitions *) - let subgroups = ReorderDecls.group_reorder_fun_decls decls in + (* Extract the decrease clauses template bodies *) + if config.extract_template_decreases_clauses then + List.iter + (fun { fwd; _ } -> + (* We only generate decreases clauses for the forward functions, because + the termination argument should only depend on the forward inputs. + The backward functions thus use the same decreases clauses as the + forward function. + + Rem.: we might filter backward functions in {!PureMicroPasses}, but + we don't remove forward functions. Instead, we remember if we should + filter those functions at extraction time with a boolean (see the + type of the [pure_ls] input parameter). + *) + let extract_decrease decl = + let has_decr_clause = has_decreases_clause decl in + if has_decr_clause then + match !Config.backend with + | Lean -> + Extract.extract_template_lean_termination_and_decreasing ctx + fmt decl + | FStar -> + Extract.extract_template_fstar_decreases_clause ctx fmt decl + | Coq -> + raise + (Failure "Coq doesn't have decreases/termination clauses") + | HOL4 -> + raise + (Failure "HOL4 doesn't have decreases/termination clauses") + in + extract_decrease fwd.f; + List.iter extract_decrease fwd.loops) + pure_ls; + + (* Concatenate the function definitions, filtering the useless forward + * functions. *) + let decls = + List.concat + (List.map + (fun { keep_fwd; fwd; backs } -> + let fwd = + if keep_fwd then List.append fwd.loops [ fwd.f ] else [] + in + let backs : Pure.fun_decl list = + List.concat + (List.map + (fun back -> List.append back.loops [ back.f ]) + backs) + in + List.append fwd backs) + pure_ls) + in - (* Extract the subgroups *) - let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit = - export_functions_group_scc fmt config ctx is_rec decls - in - List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups); - - (* Insert unit tests if necessary *) - if config.test_trans_unit_functions then - List.iter - (fun (keep_fwd, ((fwd, _), _)) -> - if keep_fwd then - Extract.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd) - pure_ls + (* Extract the function definitions *) + (if config.extract_fun_decls then + (* Group the mutually recursive definitions *) + let subgroups = ReorderDecls.group_reorder_fun_decls decls in + + (* Extract the subgroups *) + let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit = + export_functions_group_scc fmt config ctx is_rec decls + in + List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups); + + (* Insert unit tests if necessary *) + if config.test_trans_unit_functions then + List.iter + (fun trans -> + if trans.keep_fwd then + Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f) + pure_ls + +(** Export a trait declaration. *) +let export_trait_decl (fmt : Format.formatter) (_config : gen_config) + (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) (extract_decl : bool) + (extract_extra_info : bool) : unit = + let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in + (* Check if the trait declaration is builtin, in which case we ignore it *) + let open ExtractBuiltin in + let sname = name_to_simple_name trait_decl.name in + if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then ( + let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in + if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl; + if extract_extra_info then + Extract.extract_trait_decl_extra_info ctx fmt trait_decl) + else () + +(** Export a trait implementation. *) +let export_trait_impl (fmt : Format.formatter) (_config : gen_config) + (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit = + (* Lookup the definition *) + let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in + let trait_decl = + Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id + ctx.trans_trait_decls + in + (* Check if the trait implementation is builtin *) + let builtin_info = + let open ExtractBuiltin in + let type_sname = name_to_simple_name trait_impl.name in + let trait_sname = name_to_simple_name trait_decl.name in + SimpleNamePairMap.find_opt (type_sname, trait_sname) + (builtin_trait_impls_map ()) + in + match builtin_info with + | None -> Extract.extract_trait_impl ctx fmt trait_impl + | Some _ -> () (** A generic utility to generate the extracted definitions: as we may want to split the definitions between different files (or not), we can control @@ -712,12 +799,19 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) let export_functions_group = export_functions_group fmt config ctx in let export_global = export_global fmt config ctx in let export_types_group = export_types_group fmt config ctx in + let export_trait_decl_group id = + export_trait_decl fmt config ctx id true false + in + let export_trait_decl_group_extra_info id = + export_trait_decl fmt config ctx id false true + in + let export_trait_impl = export_trait_impl fmt config ctx in let export_state_type () : unit = let kind = if config.interface then ExtractBase.Declared else ExtractBase.Assumed in - Extract.extract_state_type fmt ctx.extract_ctx kind + Extract.extract_state_type fmt ctx kind in let export_decl_group (dg : A.declaration_group) : unit = @@ -725,11 +819,18 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) | Type (NonRec id) -> if config.extract_types then export_types_group false [ id ] | Type (Rec ids) -> if config.extract_types then export_types_group true ids - | Fun (NonRec id) -> + | Fun (NonRec id) -> ( (* Lookup *) let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in - (* Translate *) - export_functions_group [ pure_fun ] + (* Special case: we skip trait method *declarations* (we will + extract their type directly in the records we generate for + the trait declarations themselves, there is no point in having + separate type definitions) *) + match pure_fun.fwd.f.Pure.kind with + | TraitMethodDecl _ -> () + | _ -> + (* Translate *) + export_functions_group [ pure_fun ]) | Fun (Rec ids) -> (* General case of mutually recursive functions *) (* Lookup *) @@ -739,11 +840,19 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) (* Translate *) export_functions_group pure_funs | Global id -> export_global id + | TraitDecl id -> + (* TODO: update to extract groups *) + if config.extract_trait_decls && config.extract_transparent then ( + export_trait_decl_group id; + export_trait_decl_group_extra_info id) + | TraitImpl id -> + if config.extract_trait_impls && config.extract_transparent then + export_trait_impl id in (* If we need to export the state type: we try to export it after we defined * the type definitions, because if the user wants to define a model for the - * type, he might want to reuse those in the state type. + * type, they might want to reuse those in the state type. * More specifically: if we extract functions in the same file as the type, * we have no choice but to define the state type before the functions, * because they may reuse this state type: in this case, we define/declare @@ -752,37 +861,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if config.extract_state_type && config.extract_fun_decls then export_state_type (); - (* Obsolete: (TODO: remove) For Lean we parameterize the entire development by a section - variable called opaque_defs, of type OpaqueDefs. The code below emits the type - definition for OpaqueDefs, which is a structure, in which each field is one of the - functions marked as Opaque. We emit the `structure ...` bit here, then rely on - `extract_fun_decl` to be aware of this, and skip the keyword (e.g. "axiom" or "val") - so as to generate valid syntax for records. - - We also generate such a structure only if there actually are opaque definitions. *) - let wrap_in_sig = - config.extract_opaque && config.extract_fun_decls - && !Config.wrap_opaque_in_sig - && - let _, opaque_funs = module_has_opaque_decls ctx in - opaque_funs - in - if wrap_in_sig then ( - (* We change the name of the structure depending on whether we *only* - extract opaque definitions, or if we extract all definitions *) - let struct_name = - if config.extract_transparent then "Definitions" else "OpaqueDefs" - in - Format.pp_print_break fmt 0 0; - Format.pp_open_vbox fmt ctx.extract_ctx.indent_incr; - Format.pp_print_string fmt ("structure " ^ struct_name ^ " where"); - Format.pp_print_break fmt 0 0); List.iter export_decl_group ctx.crate.declarations; if config.extract_state_type && not config.extract_fun_decls then - export_state_type (); - - if wrap_in_sig then Format.pp_close_box fmt () + export_state_type () type extract_file_info = { filename : string; @@ -904,7 +986,9 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : unit = (* Translate the module to the pure AST *) - let trans_ctx, trans_types, trans_funs = translate_crate_to_pure crate in + let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls = + translate_crate_to_pure crate + in (* Initialize the extraction context - for now we extract only to F*. * We initialize the names map by registering the keywords used in the @@ -916,41 +1000,27 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : in (* Initialize the names map (we insert the names of the "primitives" declarations, and insert the names of the local declarations later) *) - let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in - let fmt, names_map = - mk_formatter_and_names_map trans_ctx crate.name + let fmt, names_maps = + Extract.mk_formatter_and_names_maps trans_ctx crate.name variant_concatenate_type_name in - (* Put everything in the context *) - let ctx = - { - ExtractBase.trans_ctx; - names_map; - unsafe_names_map = { id_to_name = ExtractBase.IdMap.empty }; - fmt; - indent_incr = 2; - use_opaque_pre = !Config.split_files; - use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses; - fun_name_info = PureUtils.RegularFunIdMap.empty; - } - in (* We need to compute which functions are recursive, in order to know * whether we should generate a decrease clause or not. *) let rec_functions = List.map - (fun (_, ((fwd, loop_fwds), _)) -> - let fwd = - if fwd.Pure.signature.info.effect_info.is_rec then - [ (fwd.def_id, None) ] + (fun { fwd; _ } -> + let fwd_f = + if fwd.f.Pure.signature.info.effect_info.is_rec then + [ (fwd.f.def_id, None) ] else [] in let loop_fwds = List.map (fun (def : Pure.fun_decl) -> [ (def.def_id, def.loop_id) ]) - loop_fwds + fwd.loops in - fwd :: loop_fwds) + fwd_f :: loop_fwds) trans_funs in let rec_functions : PureUtils.fun_loop_id list = @@ -958,22 +1028,70 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : in let rec_functions = PureUtils.FunLoopIdSet.of_list rec_functions in - (* Register unique names for all the top-level types, globals and functions. + (* Put the translated definitions in maps *) + let trans_types = + Pure.TypeDeclId.Map.of_list + (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types) + in + let trans_funs : pure_fun_translation A.FunDeclId.Map.t = + A.FunDeclId.Map.of_list + (List.map + (fun (trans : pure_fun_translation) -> (trans.fwd.f.def_id, trans)) + trans_funs) + in + + (* Put everything in the context *) + let ctx = + let trans_trait_decls = + T.TraitDeclId.Map.of_list + (List.map + (fun (d : Pure.trait_decl) -> (d.def_id, d)) + trans_trait_decls) + in + let trans_trait_impls = + T.TraitImplId.Map.of_list + (List.map + (fun (d : Pure.trait_impl) -> (d.def_id, d)) + trans_trait_impls) + in + { + ExtractBase.crate; + trans_ctx; + names_maps; + fmt; + indent_incr = 2; + use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses; + fun_name_info = PureUtils.RegularFunIdMap.empty; + trait_decl_id = None (* None by default *); + is_provided_method = false (* false by default *); + trans_trait_decls; + trans_trait_impls; + trans_types; + trans_funs; + functions_with_decreases_clause = rec_functions; + types_filter_type_args_map = Pure.TypeDeclId.Map.empty; + funs_filter_type_args_map = Pure.FunDeclId.Map.empty; + trait_impls_filter_type_args_map = Pure.TraitImplId.Map.empty; + } + in + + (* Register unique names for all the top-level types, globals, functions... * Note that the order in which we generate the names doesn't matter: * we just need to generate a mapping from identifier to name, and make * sure there are no name clashes. *) let ctx = List.fold_left (fun ctx def -> Extract.extract_type_decl_register_names ctx def) - ctx trans_types + ctx + (Pure.TypeDeclId.Map.values trans_types) in let ctx = List.fold_left - (fun ctx (keep_fwd, defs) -> + (fun ctx (trans : pure_fun_translation) -> (* If requested by the user, register termination measures and decreases proofs for all the recursive functions *) - let fwd_def = fst (fst defs) in + let fwd_def = trans.fwd.f in let gen_decr_clause (def : Pure.fun_decl) = !Config.extract_decreases_clauses && PureUtils.FunLoopIdSet.mem @@ -984,10 +1102,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : * those are handled later *) let is_global = fwd_def.Pure.is_global_decl_body in if is_global then ctx - else - Extract.extract_fun_decl_register_names ctx keep_fwd gen_decr_clause - defs) - ctx trans_funs + else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans) + ctx + (A.FunDeclId.Map.values trans_funs) in let ctx = @@ -995,6 +1112,16 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (A.GlobalDeclId.Map.values crate.globals) in + let ctx = + List.fold_left Extract.extract_trait_decl_register_names ctx + trans_trait_decls + in + + let ctx = + List.fold_left Extract.extract_trait_impl_register_names ctx + trans_trait_impls + in + (* Open the output file *) (* First compute the filename by replacing the extension and converting the * case (rust module names are snake case) *) @@ -1023,19 +1150,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (namespace, crate_name, Filename.concat dest_dir crate_name) in - (* Put the translated definitions in maps *) - let trans_types = - Pure.TypeDeclId.Map.of_list - (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types) - in - let trans_funs = - A.FunDeclId.Map.of_list - (List.map - (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) -> - ((fst fd).def_id, (keep_fwd, (fd, bdl)))) - trans_funs) - in - let mkdir_if dest_dir = if not (Sys.file_exists dest_dir) then ( log#linfo (lazy ("Creating missing directory: " ^ dest_dir)); @@ -1091,16 +1205,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : in (* Extract the file(s) *) - let gen_ctx = - { - crate; - extract_ctx = ctx; - trans_types; - trans_funs; - functions_with_decreases_clause = rec_functions; - } - in - let module_delimiter = match !Config.backend with | FStar -> "." @@ -1136,6 +1240,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : extract_decreases_clauses = !Config.extract_decreases_clauses; extract_template_decreases_clauses = false; extract_fun_decls = false; + extract_trait_decls = false; + extract_trait_impls = false; extract_transparent = true; extract_opaque = false; extract_state_type = false; @@ -1147,7 +1253,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (* Check if there are opaque types and functions - in which case we need * to split *) - let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in + let has_opaque_types, has_opaque_funs = + crate_has_opaque_non_builtin_decls ctx true + in let has_opaque_types = has_opaque_types || !Config.use_state in (* Extract the types *) @@ -1168,6 +1276,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : { base_gen_config with extract_types = true; + extract_trait_decls = true; extract_opaque = true; extract_state_type = !Config.use_state; interface = has_opaque_types; @@ -1186,7 +1295,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : custom_includes = []; } in - extract_file types_config gen_ctx file_info; + extract_file types_config ctx file_info; (* Extract the template clauses *) (if needs_clauses_module && !Config.extract_template_decreases_clauses then @@ -1214,9 +1323,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : custom_includes = []; } in - extract_file template_clauses_config gen_ctx file_info); + extract_file template_clauses_config ctx file_info); - (* Extract the opaque functions, if needed *) + (* Extract the opaque declarations, if needed *) let opaque_funs_module = if has_opaque_funs then ( (* In the case of Lean we generate a template file *) @@ -1244,17 +1353,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : { base_gen_config with extract_fun_decls = true; + extract_trait_impls = true; + extract_globals = true; extract_transparent = false; extract_opaque = true; interface = true; } in - let gen_ctx = - { - gen_ctx with - extract_ctx = { gen_ctx.extract_ctx with use_opaque_pre = false }; - } - in let file_info = { filename = opaque_filename; @@ -1268,7 +1373,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : custom_includes = [ types_module ]; } in - extract_file opaque_config gen_ctx file_info; + extract_file opaque_config ctx file_info; (* Return the additional dependencies *) [ opaque_imported_module ]) else [] @@ -1281,6 +1386,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : { base_gen_config with extract_fun_decls = true; + extract_trait_impls = true; extract_globals = true; test_trans_unit_functions = !Config.test_trans_unit_functions; } @@ -1307,7 +1413,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : [ types_module ] @ opaque_funs_module @ clauses_module; } in - extract_file fun_config gen_ctx file_info) + extract_file fun_config ctx file_info) else let gen_config = { @@ -1316,6 +1422,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : extract_template_decreases_clauses = !Config.extract_template_decreases_clauses; extract_fun_decls = true; + extract_trait_decls = true; + extract_trait_impls = true; extract_transparent = true; extract_opaque = true; extract_state_type = !Config.use_state; @@ -1337,7 +1445,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : custom_includes = []; } in - extract_file gen_config gen_ctx file_info); + extract_file gen_config ctx file_info); (* Generate the build file *) match !Config.backend with |