summaryrefslogtreecommitdiff
path: root/compiler/Translate.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Translate.ml')
-rw-r--r--compiler/Translate.ml964
1 files changed, 583 insertions, 381 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 70ef5e3d..37f58140 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1,8 +1,9 @@
-open InterpreterStatements
open Interpreter
-module L = Logging
-module T = Types
-module A = LlbcAst
+open Expressions
+open Types
+open Values
+open LlbcAst
+open Contexts
module SA = SymbolicAst
module Micro = PureMicroPasses
open PureUtils
@@ -15,31 +16,24 @@ let log = TranslateCore.log
- the list of symbolic values used for the input values
- the generated symbolic AST
*)
-type symbolic_fun_translation = V.symbolic_value list * SA.expression
+type symbolic_fun_translation = symbolic_value list * SA.expression
(** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
for the forward function and the backward functions.
*)
-let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl)
- : symbolic_fun_translation option =
+let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
+ symbolic_fun_translation option =
(* Debug *)
log#ldebug
(lazy
- ("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
+ ("translate_function_to_symbolics: " ^ name_to_string trans_ctx fdef.name));
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.
@@ -50,14 +44,12 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl)
*)
let translate_function_to_pure (trans_ctx : trans_ctx)
(fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdNotLoopMap.t)
- (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl)
- : pure_fun_translation_no_loops =
+ (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : fun_decl) :
+ pure_fun_translation_no_loops =
(* Debug *)
log#ldebug
- (lazy
- ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name));
+ (lazy ("translate_function_to_pure: " ^ name_to_string trans_ctx fdef.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,40 +59,43 @@ 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 (FRegular def_id, None) fun_sigs
in
- let sv_to_var = V.SymbolicValueId.Map.empty in
+ let sv_to_var = SymbolicValueId.Map.empty in
let var_counter = Pure.VarId.generator_zero in
let state_var, var_counter = Pure.VarId.fresh var_counter in
let back_state_var, var_counter = Pure.VarId.fresh var_counter in
let fuel0, var_counter = Pure.VarId.fresh var_counter in
let fuel, var_counter = Pure.VarId.fresh var_counter in
- let calls = V.FunCallId.Map.empty in
- let abstractions = V.AbstractionId.Map.empty in
+ let calls = FunCallId.Map.empty in
+ let abstractions = AbstractionId.Map.empty in
let recursive_type_decls =
- T.TypeDeclId.Set.of_list
+ TypeDeclId.Set.of_list
(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))
+ match g with
+ | Charon.GAst.NonRecGroup _ -> None
+ | RecGroup _ -> Some tid)
+ (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;
+ regions_hierarchies = trans_ctx.fun_ctx.regions_hierarchies;
}
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).
@@ -109,9 +104,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
*)
let loop_ids_map =
match symbolic_trans with
- | None -> V.LoopId.Map.empty
+ | None -> LoopId.Map.empty
| Some (_, ast) ->
- let m = ref V.LoopId.Map.empty in
+ let m = ref LoopId.Map.empty in
let _, fresh_loop_id = Pure.LoopId.fresh_stateful_generator () in
let visitor =
@@ -120,10 +115,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
method! visit_loop env loop =
let _ =
- match V.LoopId.Map.find_opt loop.loop_id !m with
+ match LoopId.Map.find_opt loop.loop_id !m with
| Some _ -> ()
- | None ->
- m := V.LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m
+ | None -> m := LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m
in
super#visit_loop env loop
end
@@ -148,12 +142,14 @@ 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 *)
- backward_inputs = T.RegionGroupId.Map.empty;
+ backward_inputs = RegionGroupId.Map.empty;
(* Empty for now *)
- backward_outputs = T.RegionGroupId.Map.empty;
+ backward_outputs = RegionGroupId.Map.empty;
loop_backward_outputs = None;
(* Empty for now *)
calls;
@@ -174,7 +170,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
| Some body, Some (input_svs, _) ->
let forward_input_vars = LlbcAstUtils.fun_body_get_input_vars body in
let forward_input_varnames =
- List.map (fun (v : A.var) -> v.name) forward_input_vars
+ List.map (fun (v : var) -> v.name) forward_input_vars
in
let input_svs = List.combine forward_input_varnames input_svs in
let ctx, forward_inputs =
@@ -192,7 +188,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
in
(* Translate the backward functions *)
- let translate_backward (rg : T.region_var_group) : Pure.fun_decl =
+ let translate_backward (rg : region_group) : Pure.fun_decl =
(* For the backward inputs/outputs initialization: we use the fact that
* there are no nested borrows for now, and so that the region groups
* can't have parents *)
@@ -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 (FRegular 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 (FRegular 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 =
@@ -247,10 +243,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
SymbolicToPure.fresh_vars backward_outputs ctx
in
let backward_inputs =
- T.RegionGroupId.Map.singleton back_id backward_inputs
+ RegionGroupId.Map.singleton back_id backward_inputs
in
let backward_outputs =
- T.RegionGroupId.Map.singleton back_id backward_outputs
+ RegionGroupId.Map.singleton back_id backward_outputs
in
(* Put everything in the context *)
@@ -267,33 +263,30 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
(* Translate *)
SymbolicToPure.translate_fun_decl ctx (Some symbolic)
in
- let pure_backwards =
- List.map translate_backward fdef.signature.regions_hierarchy
+ let regions_hierarchy =
+ LlbcAstUtils.FunIdMap.find (FRegular fdef.def_id)
+ fun_context.regions_hierarchies
in
+ let pure_backwards = List.map translate_backward regions_hierarchy in
(* Return *)
(pure_forward, pure_backwards)
-let translate_crate_to_pure (crate : A.crate) :
- trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
+(* TODO: factor out the return type *)
+let translate_crate_to_pure (crate : crate) :
+ 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 =
- SymbolicToPure.translate_type_decls (T.TypeDeclId.Map.values crate.types)
- in
+ let type_decls = SymbolicToPure.translate_type_decls trans_ctx in
(* Compute the type definition map *)
let type_decls_map =
@@ -304,35 +297,48 @@ 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) ->
+ ( FAssumed info.fun_id,
+ List.map (fun _ -> None) info.fun_sig.inputs,
+ info.fun_sig ))
+ Assumed.assumed_fun_infos
in
let local_sigs =
List.map
- (fun (fdef : A.fun_decl) ->
+ (fun (fdef : fun_decl) ->
let input_names =
match fdef.body with
| None -> List.map (fun _ -> None) fdef.signature.inputs
| Some body ->
List.map
- (fun (v : A.var) -> v.name)
+ (fun (v : var) -> v.name)
(LlbcAstUtils.fun_body_get_input_vars body)
in
- (A.Regular fdef.def_id, input_names, fdef.signature))
- (A.FunDeclId.Map.values crate.functions)
+ (FRegular fdef.def_id, input_names, fdef.signature))
+ (FunDeclId.Map.values crate.fun_decls)
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 =
List.map
(translate_function_to_pure trans_ctx fun_sigs type_decls_map)
- (A.FunDeclId.Map.values crate.functions)
+ (FunDeclId.Map.values crate.fun_decls)
+ in
+
+ (* Translate the trait declarations *)
+ let trait_decls =
+ List.map
+ (SymbolicToPure.translate_trait_decl trans_ctx)
+ (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
+ in
+
+ (* Translate the trait implementations *)
+ let trait_impls =
+ List.map
+ (SymbolicToPure.translate_trait_impl trans_ctx)
+ (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
in
(* Apply the micro-passes *)
@@ -341,22 +347,17 @@ let translate_crate_to_pure (crate : A.crate) :
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 +384,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 show_type_decl types)
+ ^ "\n- functions:\n"
+ ^ String.concat ",\n" (List.map show_fun_decl funs)));
+ (types <> [], funs <> [])
(** Export a type declaration.
@@ -423,15 +426,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,68 +469,102 @@ 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.
+ (* 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) ->
+ match_name_find_opt ctx.trans_ctx def.llbc_name types_map <> None)
+ defs
+ in
- Because some declaration groups are delimited, we wrap the declarations
- between [{start,end}_type_decl_group].
+ let dont_extract (d : Pure.type_decl) : bool =
+ match d.kind with
+ | Enum _ | Struct _ -> not config.extract_transparent
+ | Opaque -> not config.extract_opaque
+ 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 if List.exists dont_extract defs then
+ (* Check if we have to ignore declarations *)
+ (* Sanity check *)
+ assert (List.for_all dont_extract defs)
+ 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.
TODO: check correct behavior with opaque globals.
*)
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 = 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 = []);
+ (id : GlobalDeclId.id) : unit =
+ let global_decls = ctx.trans_ctx.global_ctx.global_decls in
+ let global = GlobalDeclId.Map.find id global_decls in
+ let trans = FunDeclId.Map.find global.body 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 extract =
+ extract
+ && match_name_find_opt ctx.trans_ctx global.name 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 +645,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 +661,141 @@ 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) ->
+ match_name_find_opt ctx.trans_ctx trans.fwd.f.llbc_name 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 = 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
+ if
+ match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
+ (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 = 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 trait_impl =
+ TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
+ in
+ match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name
+ trait_impl.impl_trait.decl_generics
+ (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,38 +811,61 @@ 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 =
+ let export_decl_group (dg : declaration_group) : unit =
match dg with
- | Type (NonRec id) ->
+ | TypeGroup (NonRecGroup 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) ->
+ | TypeGroup (RecGroup ids) ->
+ if config.extract_types then export_types_group true ids
+ | FunGroup (NonRecGroup id) -> (
(* Lookup *)
- let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in
- (* Translate *)
- export_functions_group [ pure_fun ]
- | Fun (Rec ids) ->
+ let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
+ (* 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 ])
+ | FunGroup (RecGroup ids) ->
(* General case of mutually recursive functions *)
(* Lookup *)
let pure_funs =
- List.map (fun id -> A.FunDeclId.Map.find id ctx.trans_funs) ids
+ List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
in
(* Translate *)
export_functions_group pure_funs
- | Global id -> export_global id
+ | GlobalGroup id -> export_global id
+ | TraitDeclGroup 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)
+ | TraitImplGroup 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,42 +874,16 @@ 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;
namespace : string;
in_namespace : bool;
+ open_namespace : bool;
crate_name : string;
rust_module_name : string;
module_name : string;
@@ -846,8 +942,22 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
(* Add the custom includes *)
List.iter
(fun m ->
- Printf.fprintf out "Require Export %s.\n" m;
- Printf.fprintf out "Import %s.\n" m)
+ (* TODO: I don't really understand how the "Require Export",
+ "Require Import", "Include" work.
+ I used to have:
+ {[
+ Require Export %s.
+ Import %s.
+ ]}
+
+ I now have:
+ {[
+ Require Import %s.
+ Include %s.
+ ]}
+ *)
+ Printf.fprintf out "Require Import %s.\n" m;
+ Printf.fprintf out "Include %s.\n" m)
fi.custom_includes;
Printf.fprintf out "Module %s.\n" fi.module_name
| Lean ->
@@ -858,9 +968,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes;
(* Always open the Primitives namespace *)
Printf.fprintf out "open Primitives\n";
- (* If we are inside the namespace: declare it, otherwise: open it *)
- if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace
- else Printf.fprintf out "open %s\n" fi.namespace
+ (* If we are inside the namespace: declare it *)
+ if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace;
+ (* We might need to open the namespace *)
+ if fi.open_namespace then Printf.fprintf out "open %s\n" fi.namespace
| HOL4 ->
Printf.fprintf out "open primitivesLib divDefLib\n";
(* Add the custom imports and includes *)
@@ -892,7 +1003,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
| FStar -> ()
| Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
| HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
- | Coq -> Printf.fprintf out "End %s .\n" fi.module_name);
+ | Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
(* Some logging *)
log#linfo (lazy ("Generated: " ^ fi.filename));
@@ -901,56 +1012,34 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
close_out out
(** Translate a crate and write the synthesized code to an output file. *)
-let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
+let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
unit =
(* Translate the module to the pure AST *)
- let trans_ctx, trans_types, trans_funs = 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
- * language, as well as some primitive names ("u32", etc.) *)
- let variant_concatenate_type_name =
- (* For Lean, we exploit the fact that the variant name should always be
- prefixed with the type name to prevent collisions *)
- match !Config.backend with Coq | FStar | HOL4 -> true | Lean -> false
- 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
- 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;
- }
+ let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls =
+ translate_crate_to_pure crate
in
+ (* Initialize the names map by registering the keywords used in the
+ language, as well as some primitive names ("u32", etc.).
+ We insert the names of the local declarations later. *)
+ let names_maps = Extract.initialize_names_maps () 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 +1047,69 @@ 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 FunDeclId.Map.t =
+ 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 =
+ TraitDeclId.Map.of_list
+ (List.map
+ (fun (d : Pure.trait_decl) -> (d.def_id, d))
+ trans_trait_decls)
+ in
+ let trans_trait_impls =
+ 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;
+ 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,15 +1120,24 @@ 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
+ (FunDeclId.Map.values trans_funs)
in
let ctx =
List.fold_left Extract.extract_global_decl_register_names ctx
- (A.GlobalDeclId.Map.values crate.globals)
+ (GlobalDeclId.Map.values crate.global_decls)
+ 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 *)
@@ -1023,19 +1168,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));
@@ -1074,33 +1206,30 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
match primitives_src_dest with
| None -> ()
| Some (primitives_src, primitives_destname) -> (
- let src = open_in (exe_dir ^ primitives_src) in
- let tgt_filename = Filename.concat dest_dir primitives_destname in
- let tgt = open_out tgt_filename in
- (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
try
- while true do
- (* We copy line by line *)
- let line = input_line src in
- Printf.fprintf tgt "%s\n" line
- done
- with End_of_file ->
- close_in src;
- close_out tgt;
- log#linfo (lazy ("Copied: " ^ tgt_filename)))
+ (* TODO: stop copying the primitives file *)
+ let src = open_in (exe_dir ^ primitives_src) in
+ let tgt_filename = Filename.concat dest_dir primitives_destname in
+ let tgt = open_out tgt_filename in
+ (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
+ try
+ while true do
+ (* We copy line by line *)
+ let line = input_line src in
+ Printf.fprintf tgt "%s\n" line
+ done
+ with End_of_file ->
+ close_in src;
+ close_out tgt;
+ log#linfo (lazy ("Copied: " ^ tgt_filename))
+ with Sys_error _ ->
+ log#error
+ "Could not copy the primitives file: %s.\n\
+ You will have to copy it/set up the project by hand."
+ primitives_src)
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 +1265,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,15 +1278,77 @@ 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 *)
+ (*
+ * Extract the types
+ *)
(* If there are opaque types, we extract in an interface *)
- (* TODO: for Lean and Coq: generate a template file *)
+ (* Extract the opaque type declarations, if needed *)
+ let opaque_types_module =
+ if has_opaque_types then (
+ (* For F*, we generate an .fsti, and let the user write the .fst.
+ For the other backends, we generate a template file as a model
+ for the file the user has to provide. *)
+ let module_suffix, opaque_imported_suffix, custom_msg =
+ match !Config.backend with
+ | FStar ->
+ ("TypesExternal", "TypesExternal", ": external type declarations")
+ | HOL4 | Coq | Lean ->
+ ( (* The name of the file we generate *)
+ "TypesExternal_Template",
+ (* The name of the file that will be imported by the Types
+ module, and that the user has to provide. *)
+ "TypesExternal",
+ ": external types.\n\
+ -- This is a template file: rename it to \
+ \"TypesExternal.lean\" and fill the holes." )
+ in
+ let opaque_filename =
+ extract_filebasename ^ file_delimiter ^ module_suffix ^ opaque_ext
+ in
+ let opaque_module = crate_name ^ module_delimiter ^ module_suffix in
+ let opaque_imported_module =
+ crate_name ^ module_delimiter ^ opaque_imported_suffix
+ in
+ let opaque_config =
+ {
+ base_gen_config with
+ extract_opaque = true;
+ extract_transparent = false;
+ extract_types = true;
+ extract_trait_decls = true;
+ extract_state_type = !Config.use_state;
+ interface = true;
+ }
+ in
+ let file_info =
+ {
+ filename = opaque_filename;
+ namespace;
+ in_namespace = false;
+ open_namespace = false;
+ crate_name;
+ rust_module_name = crate.name;
+ module_name = opaque_module;
+ custom_msg;
+ custom_imports = [];
+ custom_includes = [];
+ }
+ in
+ extract_file opaque_config ctx file_info;
+ (* Return the additional dependencies *)
+ [ opaque_imported_module ])
+ else []
+ in
+
+ (* Extract the non opaque types *)
let types_filename_ext =
match !Config.backend with
- | FStar -> if has_opaque_types then ".fsti" else ".fst"
+ | FStar -> ".fst"
| Coq -> ".v"
| Lean -> ".lean"
| HOL4 -> "Script.sml"
@@ -1168,8 +1361,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
{
base_gen_config with
extract_types = true;
- extract_opaque = true;
- extract_state_type = !Config.use_state;
+ extract_trait_decls = true;
+ extract_opaque = false;
interface = has_opaque_types;
}
in
@@ -1178,15 +1371,16 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
filename = types_filename;
namespace;
in_namespace = true;
+ open_namespace = false;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = types_module;
custom_msg = ": type definitions";
custom_imports = [];
- custom_includes = [];
+ custom_includes = opaque_types_module;
}
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
@@ -1206,26 +1400,34 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
filename = template_clauses_filename;
namespace;
in_namespace = true;
+ open_namespace = false;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = template_clauses_module;
custom_msg = ": templates for the decreases clauses";
custom_imports = [ types_module ];
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 fun declarations, if needed *)
let opaque_funs_module =
if has_opaque_funs then (
- (* In the case of Lean we generate a template file *)
+ (* For F*, we generate an .fsti, and let the user write the .fst.
+ For the other backends, we generate a template file as a model
+ for the file the user has to provide. *)
let module_suffix, opaque_imported_suffix, custom_msg =
match !Config.backend with
- | FStar | Coq | HOL4 ->
- ("Opaque", "Opaque", ": external function declarations")
- | Lean ->
- ( "FunsExternal_Template",
+ | FStar ->
+ ( "FunsExternal",
+ "FunsExternal",
+ ": external function declarations" )
+ | HOL4 | Coq | Lean ->
+ ( (* The name of the file we generate *)
+ "FunsExternal_Template",
+ (* The name of the file that will be imported by the Funs
+ module, and that the user has to provide. *)
"FunsExternal",
": external functions.\n\
-- This is a template file: rename it to \
@@ -1236,39 +1438,34 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
in
let opaque_module = crate_name ^ module_delimiter ^ module_suffix in
let opaque_imported_module =
- if !Config.backend = Lean then
- crate_name ^ module_delimiter ^ opaque_imported_suffix
- else opaque_module
+ crate_name ^ module_delimiter ^ opaque_imported_suffix
in
let opaque_config =
{
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;
namespace;
in_namespace = false;
+ open_namespace = true;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = opaque_module;
custom_msg;
custom_imports = [];
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 +1478,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;
}
@@ -1298,8 +1496,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
filename = fun_filename;
namespace;
in_namespace = true;
+ open_namespace = false;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = fun_module;
custom_msg = ": function definitions";
custom_imports = [];
@@ -1307,7 +1506,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 +1515,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;
@@ -1329,15 +1530,16 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
filename = extract_filebasename ^ ext;
namespace;
in_namespace = true;
+ open_namespace = false;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = crate_name;
custom_msg = "";
custom_imports = [];
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