diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/extend.mli | 47 | ||||
| -rw-r--r-- | intf/notation_term.mli | 17 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 8 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 8 |
4 files changed, 42 insertions, 38 deletions
diff --git a/intf/extend.mli b/intf/extend.mli index 10713745e4..7ba332f709 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -8,6 +8,8 @@ (** Entry keys for constr notations *) +type 'a entry = 'a Compat.GrammarMake(CLexer).entry + type side = Left | Right type gram_assoc = NonA | RightA | LeftA @@ -53,51 +55,38 @@ type simple_constr_prod_entry_key = (** {5 AST for user-provided entries} *) -type user_symbol = -| Ulist1 : user_symbol -> user_symbol -| Ulist1sep : user_symbol * string -> user_symbol -| Ulist0 : user_symbol -> user_symbol -| Ulist0sep : user_symbol * string -> user_symbol -| Uopt : user_symbol -> user_symbol -| Uentry : string -> user_symbol -| Uentryl : string * int -> user_symbol +type 'a user_symbol = +| Ulist1 of 'a user_symbol +| Ulist1sep of 'a user_symbol * string +| Ulist0 of 'a user_symbol +| Ulist0sep of 'a user_symbol * string +| Uopt of 'a user_symbol +| Uentry of 'a +| Uentryl of 'a * int (** {5 Type-safe grammar extension} *) -(** (a, b, r) adj => [a = x₁ -> ... xₙ -> r] & [b = x₁ * (... (xₙ * unit))]. *) -type (_, _, _) adj = -| Adj0 : ('r, unit, 'r) adj -| AdjS : ('s, 'b, 'r) adj -> ('a -> 's, 'a * 'b, 'r) adj - -type _ index = -| I0 : 'a -> ('a * 'r) index -| IS : 'a index -> ('b * 'a) index - -(** This type should be marshallable, this is why we use a convoluted - representation in the [Arules] constructor instead of putting a function. *) type ('self, 'a) symbol = | Atoken : Tok.t -> ('self, string) symbol | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol -| Alist1sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol +| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol -| Alist0sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol +| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol | Aself : ('self, 'self) symbol | Anext : ('self, 'self) symbol -| Aentry : 'a Entry.t -> ('self, 'a) symbol -| Aentryl : 'a Entry.t * int -> ('self, 'a) symbol -| Arules : 'a rules -> ('self, 'a index) symbol +| Aentry : 'a entry -> ('self, 'a) symbol +| Aentryl : 'a entry * int -> ('self, 'a) symbol +| Arules : 'a rules list -> ('self, 'a) symbol and ('self, _, 'r) rule = | Stop : ('self, 'r, 'r) rule | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule +and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule } + and 'a rules = -| Rule0 : unit rules -| RuleS : - ('any, 'act, Loc.t -> Loc.t * 'a) rule * - ('act, 'a, Loc.t -> Loc.t * 'a) adj * - 'b rules -> ((Loc.t * 'a) * 'b) rules +| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules type 'a production_rule = | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 39a36310d1..883b017727 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -42,7 +42,6 @@ type notation_constr = (Name.t * notation_constr option * notation_constr) list array * notation_constr array * notation_constr array | NSort of glob_sort - | NPatVar of patvar | NCast of notation_constr * notation_constr cast_type (** Note concerning NList: first constr is iterator, second is terminator; @@ -79,3 +78,19 @@ type notation_interp_env = { ninterp_rec_vars : Id.t Id.Map.t; mutable ninterp_only_parse : bool; } + +type grammar_constr_prod_item = + | GramConstrTerminal of Tok.t + | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option + | GramConstrListMark of int * bool + (* tells action rule to make a list of the n previous parsed items; + concat with last parsed list if true *) + +type notation_grammar = { + notgram_level : int; + notgram_assoc : Extend.gram_assoc option; + notgram_notation : Constrexpr.notation; + notgram_prods : grammar_constr_prod_item list list; + notgram_typs : notation_var_internalization_type list; + notgram_onlyprinting : bool; +} diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 875ad3d160..379dd59d39 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -120,7 +120,7 @@ type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Id.Set.t -type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern +type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern type 'a delayed_open = 'a Pretyping.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } @@ -139,8 +139,6 @@ type intro_pattern_naming = intro_pattern_naming_expr located type 'a gen_atomic_tactic_expr = (* Basic tactics *) | TacIntroPattern of 'dtrm intro_pattern_expr located list - | TacIntroMove of Id.t option * 'nam move_location - | TacExact of 'trm | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * ('nam * 'dtrm intro_pattern_expr located option) option | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option @@ -157,10 +155,6 @@ type 'a gen_atomic_tactic_expr = (* Derived basic tactics *) | TacInductionDestruct of rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list - | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis - - (* Context management *) - | TacRename of ('nam *'nam) list (* Conversion *) | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ae9328fcc0..cfa30a4d54 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -206,6 +206,7 @@ type syntax_modifier = | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing of Flags.compat_version + | SetOnlyPrinting | SetFormat of string * string located type proof_end = @@ -454,7 +455,7 @@ type vernac_type = | VtStartProof of vernac_start | VtSideff of vernac_sideff_type | VtQed of vernac_qed_type - | VtProofStep of bool (* parallelize *) + | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * report_with | VtStm of vernac_control * vernac_part_of_script @@ -476,6 +477,11 @@ and vernac_control = and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and proof_step = { (* TODO: inline with OCaml 4.03 *) + parallel : bool; + proof_block_detection : proof_block_name option +} +and proof_block_name = string (* open type of delimiters *) type vernac_when = | VtNow | VtLater |