diff options
Diffstat (limited to 'compiler/ExtractBase.ml')
-rw-r--r-- | compiler/ExtractBase.ml | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 152dfc99..77170b5b 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -203,6 +203,21 @@ type formatter = { the same purpose as in {!field:fun_name}. - loop identifier, if this is for a loop *) + terminates_clause_name : + A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string; + (** Generates the name of the measure 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. + + Inputs: + - function id: this is especially useful to identify whether the + function is an assumed function or a local function + - function basename + - the number of loops in the parent function. This is used for + the same purpose as in {!field:fun_name}. + - loop identifier, if this is for a loop + *) + var_basename : StringSet.t -> string option -> ty -> string; (** Generates a variable basename. @@ -285,6 +300,12 @@ type id = the body of those clauses must be defined by the user, in the proper files. *) + | TerminatesClauseId 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. + *) | TypeId of type_id | StructId of type_id (** We use this when we manipulate the names of the structure @@ -486,6 +507,19 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | Some lid -> ", loop: " ^ LoopId.to_string lid in "decreases clause for function: " ^ fun_name ^ loop + | TerminatesClauseId (fid, lid) -> + let fun_name = + match fid with + | Regular fid -> + Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name + | Assumed aid -> A.show_assumed_fun_id aid + in + let loop = + match lid with + | None -> "" + | Some lid -> ", loop: " ^ LoopId.to_string lid + in + "terminates clause 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) -> @@ -596,6 +630,10 @@ let ctx_get_decreases_clause (def_id : A.FunDeclId.id) (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = ctx_get (DecreasesClauseId (Regular def_id, loop_id)) ctx +let ctx_get_terminates_clause (def_id : A.FunDeclId.id) + (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = + ctx_get (TerminatesClauseId (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) (ctx : extraction_ctx) : extraction_ctx * string = @@ -688,6 +726,14 @@ let ctx_add_decreases_clause (def : fun_decl) (ctx : extraction_ctx) : in ctx_add (DecreasesClauseId (Regular def.def_id, def.loop_id)) name ctx +let ctx_add_terminates_clause (def : fun_decl) (ctx : extraction_ctx) : + extraction_ctx = + let name = + ctx.fmt.terminates_clause_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 + let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = let name = ctx.fmt.global_name def.name in |