summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Config.ml23
-rw-r--r--compiler/Driver.ml24
-rw-r--r--compiler/Extract.ml49
-rw-r--r--compiler/ExtractBase.ml63
-rw-r--r--compiler/Translate.ml10
5 files changed, 108 insertions, 61 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 1c3d14ff..1baed7fa 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -9,7 +9,11 @@ let backend_names = [ "fstar"; "coq"; "lean" ]
(** Utility to compute the backend from an input parameter *)
let backend_of_string (b : string) : backend option =
- match b with "fstar" -> Some FStar | "coq" -> Some Coq | "lean" -> Some Lean | _ -> None
+ match b with
+ | "fstar" -> Some FStar
+ | "coq" -> Some Coq
+ | "lean" -> Some Lean
+ | _ -> None
let opt_backend : backend option ref = ref None
@@ -174,16 +178,21 @@ let test_unit_functions = ref false
*)
let test_trans_unit_functions = ref false
-(** If [true], insert [decreases] clauses for all the recursive definitions.
+(** If [true], use decreases clauses/termination measures for all the recursive definitions.
- The body of such clauses must be defined by the user.
+ More precisely:
+ - for F*, we generate definitions which use decreases clauses
+ - for Lean, we generate definitions which use termination measures and
+ decreases proofs
+
+ The body of such clauses/proofs must be defined by the user.
*)
let extract_decreases_clauses = ref false
-(** In order to help the user, we can generate "template" decrease clauses
- (i.e., definitions with proper signatures but dummy bodies) in a
- dedicated file.
- *)
+(** In order to help the user, we can generate "template" decrease clauses/ termination
+ measures (i.e., definitions with proper signatures but dummy bodies) in a dedicated
+ file.
+*)
let extract_template_decreases_clauses = ref false
(** {1 Micro passes} *)
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 149e2aad..e0504903 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -66,24 +66,26 @@ let () =
[
( "-backend",
Arg.Symbol (backend_names, set_backend),
- " Specify the backend to which to extract" );
+ " Specify the target backend" );
("-dest", Arg.Set_string dest_dir, " Specify the output directory");
( "-no-filter-useless-calls",
Arg.Clear filter_useless_monadic_calls,
- " Do not filter the useless function calls, when possible" );
+ " Do not filter the useless function calls" );
( "-no-filter-useless-funs",
Arg.Clear filter_useless_functions,
" Do not filter the useless forward/backward functions" );
( "-test-units",
Arg.Set test_unit_functions,
- " Test the unit functions with the concrete interpreter" );
+ " Test the unit functions with the concrete (i.e., not symbolic) \
+ interpreter" );
( "-test-trans-units",
Arg.Set test_trans_unit_functions,
- " Test the translated unit functions with the target theorem\n\
- \ prover's normalizer" );
+ " Test the translated unit functions with the target theorem prover's \
+ normalizer" );
( "-decreases-clauses",
Arg.Set extract_decreases_clauses,
- " Use decreases clauses for the recursive definitions" );
+ " Use decreases clauses/termination measures for the recursive \
+ definitions" );
( "-no-state",
Arg.Clear use_state,
" Do not use state-error monads, simply use error monads" );
@@ -95,16 +97,16 @@ let () =
" Forbid backward functions from updating the state" );
( "-template-clauses",
Arg.Set extract_template_decreases_clauses,
- " Generate templates for the required decreases clauses, in a \
- dedicated file. Implies -decreases-clauses" );
+ " Generate templates for the required decreases clauses/termination \
+ measures, in a dedicated file. Implies -decreases-clauses" );
( "-no-split-files",
Arg.Clear split_files,
- " Don't split the definitions between different files for types, \
+ " Do not split the definitions between different files for types, \
functions, etc." );
( "-no-check-inv",
Arg.Clear check_invariants,
- " Deactivate the invariant sanity checks performed at every step of \
- evaluation. Dramatically saves speed." );
+ " Deactivate the invariant sanity checks performed at every evaluation \
+ step. Dramatically increases speed." );
]
in
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 35e5d64c..95ba2f02 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -492,22 +492,31 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
fname ^ suffix
in
- let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name)
+ let termination_measure_name (_fid : A.FunDeclId.id) (fname : fun_name)
(num_loops : int) (loop_id : LoopId.id option) : string =
let fname = fun_name_to_snake_case fname in
let lp_suffix = default_fun_loop_suffix num_loops loop_id in
(* Compute the suffix *)
- let suffix = "_decreases" in
+ let suffix =
+ match !Config.backend with
+ | FStar -> "_decreases"
+ | Lean -> "_terminates"
+ | Coq -> raise (Failure "Unexpected")
+ in
(* Concatenate *)
fname ^ lp_suffix ^ suffix
in
- let terminates_clause_name (_fid : A.FunDeclId.id) (fname : fun_name)
+ let decreases_proof_name (_fid : A.FunDeclId.id) (fname : fun_name)
(num_loops : int) (loop_id : LoopId.id option) : string =
let fname = fun_name_to_snake_case fname in
let lp_suffix = default_fun_loop_suffix num_loops loop_id in
(* Compute the suffix *)
- let suffix = "_terminates" in
+ let suffix =
+ match !Config.backend with
+ | Lean -> "_decreases"
+ | FStar | Coq -> raise (Failure "Unexpected")
+ in
(* Concatenate *)
fname ^ lp_suffix ^ suffix
in
@@ -640,8 +649,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
type_name;
global_name;
fun_name;
- decreases_clause_name;
- terminates_clause_name;
+ termination_measure_name;
+ decreases_proof_name;
var_basename;
type_var_basename;
append_index;
@@ -1370,8 +1379,12 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
(* Register the decrease clauses, if necessary *)
let register_decreases ctx def =
if has_decreases_clause def then
- let ctx = ctx_add_decreases_clause def ctx in
- ctx_add_terminates_clause def ctx
+ (* Add the termination measure *)
+ let ctx = ctx_add_termination_measure def ctx in
+ (* Add the decreases proof for Lean only *)
+ match !Config.backend with
+ | Coq | FStar -> ctx
+ | Lean -> ctx_add_decreases_proof def ctx
else ctx
in
let ctx = List.fold_left register_decreases ctx (fwd :: loop_fwds) in
@@ -2085,7 +2098,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
assert (!backend = FStar);
(* Retrieve the function name *)
- let def_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
+ let def_name = ctx_get_termination_measure def.def_id def.loop_id ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
@@ -2142,9 +2155,11 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
assert (!backend = Lean);
-
+ (*
+ * Extract a template for the termination measure
+ *)
(* Retrieve the function name *)
- let def_name = ctx_get_terminates_clause def.def_id def.loop_id ctx in
+ let def_name = ctx_get_termination_measure def.def_id def.loop_id ctx in
let def_body = Option.get def.body in
(* Add a break before *)
F.pp_print_break fmt 0 0;
@@ -2197,8 +2212,10 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(* Add breaks to insert new lines between definitions *)
F.pp_print_break fmt 0 0;
- (* Now extract a template for the termination proof *)
- let def_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
+ (*
+ * Extract a template for the decreases proof
+ *)
+ let def_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
(* syntax <def_name> term ... term : tactic *)
F.pp_print_break fmt 0 0;
extract_comment fmt
@@ -2329,7 +2346,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the decreases term *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* The name of the decrease clause *)
- let decr_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
+ let decr_name = ctx_get_termination_measure def.def_id def.loop_id ctx in
F.pp_print_string fmt decr_name;
(* Print the type parameters *)
List.iter
@@ -2401,7 +2418,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* termination_by *)
let terminates_name =
- ctx_get_terminates_clause def.def_id def.loop_id ctx
+ ctx_get_termination_measure def.def_id def.loop_id ctx
in
F.pp_print_break fmt 0 0;
(* Open a box for the whole [termination_by CALL => DECREASES] *)
@@ -2443,7 +2460,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_break fmt 0 0;
(* Open a box for the [decreasing by ...] *)
F.pp_open_hvbox fmt ctx.indent_incr;
- let decreases_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
+ let decreases_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
F.pp_print_string fmt "decreasing_by";
F.pp_print_space fmt ();
F.pp_open_hvbox fmt ctx.indent_incr;
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index e96a80f9..55963289 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -189,12 +189,14 @@ type formatter = {
filtered some of them.
TODO: use the fun id for the assumed functions.
*)
- decreases_clause_name :
+ termination_measure_name :
A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string;
- (** Generates the name of the definition used to prove/reason about
+ (** Generates the name of the termination measure used to prove/reason about
termination. The generated code uses this clause where needed,
but its body must be defined by the user.
+ F* and Lean only.
+
Inputs:
- function id: this is especially useful to identify whether the
function is an assumed function or a local function
@@ -203,11 +205,13 @@ type formatter = {
the same purpose as in {!field:fun_name}.
- loop identifier, if this is for a loop
*)
- terminates_clause_name :
+ decreases_proof_name :
A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string;
- (** Generates the name of the measure used to prove/reason about
+ (** Generates the name of the proof used to prove/reason about
termination. The generated code uses this clause where needed,
- but its body must be defined by the user. Lean only.
+ but its body must be defined by the user.
+
+ Lean only.
Inputs:
- function id: this is especially useful to identify whether the
@@ -294,17 +298,30 @@ type id =
| GlobalId of A.GlobalDeclId.id
| FunId of fun_id
| DeclaredId of fun_id
- | DecreasesClauseId of (A.fun_id * LoopId.id option)
- (** The definition which provides the decreases/termination clause.
+ | TerminationMeasureId of (A.fun_id * LoopId.id option)
+ (** The definition which provides the decreases/termination measure.
We insert calls to this clause to prove/reason about termination:
the body of those clauses must be defined by the user, in the
proper files.
+
+ More specifically:
+ - in F*, this is the content of the [decreases] clause.
+ Example:
+ ========
+ {[
+ let rec sum (ls : list nat) : Tot nat (decreases ls) = ...
+ ]}
+ - in Lean, this is the content of the [termination_by] clause.
*)
- | TerminatesClauseId of (A.fun_id * LoopId.id option)
- (** The definition which provides the decreases/termination measure.
+ | DecreasesProofId of (A.fun_id * LoopId.id option)
+ (** The definition which provides the decreases/termination proof.
We insert calls to this clause to prove/reason about termination:
the body of those clauses must be defined by the user, in the
proper files.
+
+ More specifically:
+ - F* doesn't use this.
+ - in Lean, this is the tactic used by the [decreases_by] annotations.
*)
| TypeId of type_id
| StructId of type_id
@@ -494,7 +511,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
in
"fun name (" ^ lp_kind ^ fwd_back_kind ^ "): " ^ fun_name
| Pure fid -> PrintPure.pure_assumed_fun_id_to_string fid)
- | DecreasesClauseId (fid, lid) ->
+ | DecreasesProofId (fid, lid) ->
let fun_name =
match fid with
| Regular fid ->
@@ -506,8 +523,8 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| None -> ""
| Some lid -> ", loop: " ^ LoopId.to_string lid
in
- "decreases clause for function: " ^ fun_name ^ loop
- | TerminatesClauseId (fid, lid) ->
+ "decreases proof for function: " ^ fun_name ^ loop
+ | TerminationMeasureId (fid, lid) ->
let fun_name =
match fid with
| Regular fid ->
@@ -519,7 +536,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| None -> ""
| Some lid -> ", loop: " ^ LoopId.to_string lid
in
- "terminates clause for function: " ^ fun_name ^ loop
+ "termination measure for function: " ^ fun_name ^ loop
| TypeId id -> "type name: " ^ get_type_name id
| StructId id -> "struct constructor of: " ^ get_type_name id
| VariantId (id, variant_id) ->
@@ -629,13 +646,13 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
(ctx : extraction_ctx) : string =
ctx_get (VariantId (def_id, variant_id)) ctx
-let ctx_get_decreases_clause (def_id : A.FunDeclId.id)
+let ctx_get_decreases_proof (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- ctx_get (DecreasesClauseId (Regular def_id, loop_id)) ctx
+ ctx_get (DecreasesProofId (Regular def_id, loop_id)) ctx
-let ctx_get_terminates_clause (def_id : A.FunDeclId.id)
+let ctx_get_termination_measure (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- ctx_get (TerminatesClauseId (Regular def_id, loop_id)) ctx
+ ctx_get (TerminationMeasureId (Regular def_id, loop_id)) ctx
(** Generate a unique type variable name and add it to the context *)
let ctx_add_type_var (basename : string) (id : TypeVarId.id)
@@ -721,21 +738,21 @@ let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) :
let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in
(ctx, name)
-let ctx_add_decreases_clause (def : fun_decl) (ctx : extraction_ctx) :
+let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
let name =
- ctx.fmt.decreases_clause_name def.def_id def.basename def.num_loops
+ ctx.fmt.decreases_proof_name def.def_id def.basename def.num_loops
def.loop_id
in
- ctx_add (DecreasesClauseId (Regular def.def_id, def.loop_id)) name ctx
+ ctx_add (DecreasesProofId (Regular def.def_id, def.loop_id)) name ctx
-let ctx_add_terminates_clause (def : fun_decl) (ctx : extraction_ctx) :
+let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
let name =
- ctx.fmt.terminates_clause_name def.def_id def.basename def.num_loops
+ ctx.fmt.termination_measure_name def.def_id def.basename def.num_loops
def.loop_id
in
- ctx_add (TerminatesClauseId (Regular def.def_id, def.loop_id)) name ctx
+ ctx_add (TerminationMeasureId (Regular def.def_id, def.loop_id)) name ctx
let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
extraction_ctx =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index b2cab4c2..139f8891 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -825,12 +825,14 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
let ctx =
List.fold_left
(fun ctx (keep_fwd, defs) ->
- (* We generate a decrease clause for all the recursive functions *)
+ (* If requested by the user, register termination measures and decreases
+ proofs for all the recursive functions *)
let fwd_def = fst (fst defs) in
let gen_decr_clause (def : Pure.fun_decl) =
- PureUtils.FunLoopIdSet.mem
- (def.Pure.def_id, def.Pure.loop_id)
- rec_functions
+ !Config.extract_decreases_clauses
+ && PureUtils.FunLoopIdSet.mem
+ (def.Pure.def_id, def.Pure.loop_id)
+ rec_functions
in
(* Register the names, only if the function is not a global body -
* those are handled later *)