diff options
Diffstat (limited to 'compiler/ExtractBase.ml')
| -rw-r--r-- | compiler/ExtractBase.ml | 63 |
1 files changed, 40 insertions, 23 deletions
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 = |