diff options
| -rw-r--r-- | compiler/Config.ml | 23 | ||||
| -rw-r--r-- | compiler/Driver.ml | 24 | ||||
| -rw-r--r-- | compiler/Extract.ml | 49 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 63 | ||||
| -rw-r--r-- | compiler/Translate.ml | 10 |
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 *) |