diff options
| author | Emilio Jesus Gallego Arias | 2019-07-19 14:01:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-23 14:31:02 +0200 |
| commit | d68f695b5a953c50bcf5e80182ef317682de1a05 (patch) | |
| tree | f0f349ee62145e1075a85ff52c944a078502c884 /vernac/vernacexpr.ml | |
| parent | ae82afbaebb7f3a328498d4cc541d299423a7637 (diff) | |
[vernacexpr] Refactor fixpoint AST.
We turn the tuples used for (co)-fixpoints into records, cleaning up
their users.
More cleanup is be possible, in particular a few functions can now
shared among co and fixpoints, also `structured_fixpoint_expr` could
like be folded into the new record.
Feedback on the naming of the records fields is welcome.
This is a step towards cleaning up code in `funind`, as it is the main
consumer of this data structure, as it does quite a bit of fixpoint
manipulation.
cc: #6019
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ee1f839b8d..8b8123bd30 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -128,18 +128,25 @@ type definition_expr = | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option -type fixpoint_expr = - ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option +type decl_notation = lstring * constr_expr * scope_name option + +type 'a fix_expr_gen = + { id_decl : ident_decl + ; rec_order : 'a + ; binders : local_binder_expr list + ; rtype : constr_expr + ; body_def : constr_expr option + ; notations : decl_notation list + } -type cofixpoint_expr = - ident_decl * local_binder_expr list * constr_expr * constr_expr option +type fixpoint_expr = recursion_order_expr option fix_expr_gen +type cofixpoint_expr = unit fix_expr_gen type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) -type decl_notation = lstring * constr_expr * scope_name option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a @@ -283,8 +290,8 @@ type nonrec vernac_expr = | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list + | VernacFixpoint of discharge * fixpoint_expr list + | VernacCoFixpoint of discharge * cofixpoint_expr list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list |