diff options
| author | Son Ho | 2023-03-07 09:05:45 +0100 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | db8cca3c3177fec2e66634366a6621ca979c0dc9 (patch) | |
| tree | c84958eb00667700cf628f55aabc5128ca4a55d5 /compiler/Translate.ml | |
| parent | 73b95970460fb7d8c90e2ea97fa6457d7850af07 (diff) | |
Update the generation of termination and decreases_by templates for Lean
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 3a75c885..b2cab4c2 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -562,11 +562,15 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let extract_decrease decl = let has_decr_clause = has_decreases_clause decl in if has_decr_clause then - if !Config.backend = Lean then - Extract.extract_termination_and_decreasing ctx.extract_ctx fmt - decl - else - Extract.extract_template_decreases_clause ctx.extract_ctx fmt decl + 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") in extract_decrease fwd; List.iter extract_decrease loop_fwds) |