diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-20 22:23:02 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-27 15:18:08 +0200 |
commit | 311e87f261b5e7f1dca61ac19d9b7b695b411ce0 (patch) | |
tree | ba75b995a5b9a58b76d016f46adc934dfe9e29ba /vernac | |
parent | b2f746e41abf53fc481f90804ba4d70edd73fc86 (diff) |
[api] [parsing] Move Egram* to `vernac/`
The extension mechanism is specific to metasyntax and vernacinterp,
thus it makes sense to place them next to each other.
We also fix the META entry for the `grammar` camlp5 plugin.
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/egramcoq.ml | 483 | ||||
-rw-r--r-- | vernac/egramcoq.mli | 19 | ||||
-rw-r--r-- | vernac/egramml.ml | 84 | ||||
-rw-r--r-- | vernac/egramml.mli | 33 | ||||
-rw-r--r-- | vernac/ppvernac.ml | 1219 | ||||
-rw-r--r-- | vernac/ppvernac.mli | 26 | ||||
-rw-r--r-- | vernac/vernac.mllib | 11 |
7 files changed, 1871 insertions, 4 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml new file mode 100644 index 000000000..5f63d21c4 --- /dev/null +++ b/vernac/egramcoq.ml @@ -0,0 +1,483 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open CErrors +open Util +open Pcoq +open Constrexpr +open Notation_term +open Extend +open Libnames +open Names + +(**********************************************************************) +(* This determines (depending on the associativity of the current + level and on the expected associativity) if a reference to constr_n is + a reference to the current level (to be translated into "SELF" on the + left border and into "constr LEVEL n" elsewhere), to the level below + (to be translated into "NEXT") or to an below wrt associativity (to be + translated in camlp5 into "constr" without level) or to another level + (to be translated into "constr LEVEL n") + + The boolean is true if the entry was existing _and_ empty; this to + circumvent a weakness of camlp5 whose undo mechanism is not the + converse of the extension mechanism *) + +let constr_level = string_of_int + +let default_levels = + [200,Extend.RightA,false; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 90,Extend.RightA,true; + 10,Extend.LeftA,false; + 9,Extend.RightA,false; + 8,Extend.RightA,true; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let default_pattern_levels = + [200,Extend.RightA,true; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 90,Extend.RightA,true; + 10,Extend.LeftA,false; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let default_constr_levels = (default_levels, default_pattern_levels) + +(* At a same level, LeftA takes precedence over RightA and NoneA *) +(* In case, several associativity exists for a level, we make two levels, *) +(* first LeftA, then RightA and NoneA together *) + +let admissible_assoc = function + | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false + | Extend.RightA, Some Extend.LeftA -> false + | _ -> true + +let create_assoc = function + | None -> Extend.RightA + | Some a -> a + +let error_level_assoc p current expected = + let open Pp in + let pr_assoc = function + | Extend.LeftA -> str "left" + | Extend.RightA -> str "right" + | Extend.NonA -> str "non" in + user_err + (str "Level " ++ int p ++ str " is already declared " ++ + pr_assoc current ++ str " associative while it is now expected to be " ++ + pr_assoc expected ++ str " associative.") + +let create_pos = function + | None -> Extend.First + | Some lev -> Extend.After (constr_level lev) + +let find_position_gen current ensure assoc lev = + match lev with + | None -> + current, (None, None, None, None) + | Some n -> + let after = ref None in + let init = ref None in + let rec add_level q = function + | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l + | (p,a,reinit)::l when Int.equal p n -> + if reinit then + let a' = create_assoc assoc in + (init := Some (a',create_pos q); (p,a',false)::l) + else if admissible_assoc (a,assoc) then + raise Exit + else + error_level_assoc p a (Option.get assoc) + | l -> after := q; (n,create_assoc assoc,ensure)::l + in + try + let updated = add_level None current in + let assoc = create_assoc assoc in + begin match !init with + | None -> + (* Create the entry *) + updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) + | _ -> + (* The reinit flag has been updated *) + updated, (Some (Extend.Level (constr_level n)), None, None, !init) + end + with + (* Nothing has changed *) + Exit -> + (* Just inherit the existing associativity and name (None) *) + current, (Some (Extend.Level (constr_level n)), None, None, None) + +let rec list_mem_assoc_triple x = function + | [] -> false + | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l + +let register_empty_levels accu forpat levels = + let rec filter accu = function + | [] -> ([], accu) + | n :: rem -> + let rem, accu = filter accu rem in + let (clev, plev) = accu in + let levels = if forpat then plev else clev in + if not (list_mem_assoc_triple n levels) then + let nlev, ans = find_position_gen levels true None (Some n) in + let nlev = if forpat then (clev, nlev) else (nlev, plev) in + ans :: rem, nlev + else rem, accu + in + filter accu levels + +let find_position accu forpat assoc level = + let (clev, plev) = accu in + let levels = if forpat then plev else clev in + let nlev, ans = find_position_gen levels false assoc level in + let nlev = if forpat then (clev, nlev) else (nlev, plev) in + (ans, nlev) + +(**************************************************************************) +(* + * --- Note on the mapping of grammar productions to camlp5 actions --- + * + * Translation of environments: a production + * [ nt1(x1) ... nti(xi) ] -> act(x1..xi) + * is written (with camlp5 conventions): + * (fun vi -> .... (fun v1 -> act(v1 .. vi) )..) + * where v1..vi are the values generated by non-terminals nt1..nti. + * Since the actions are executed by substituting an environment, + * the make_*_action family build the following closure: + * + * ((fun env -> + * (fun vi -> + * (fun env -> ... + * + * (fun v1 -> + * (fun env -> gram_action .. env act) + * ((x1,v1)::env)) + * ...) + * ((xi,vi)::env))) + * []) + *) + +(**********************************************************************) +(** Declare Notations grammar rules *) + +(**********************************************************************) +(* Binding constr entry keys to entries *) + +(* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *) +let camlp5_assoc = function + | Some NonA | Some RightA -> RightA + | None | Some LeftA -> LeftA + +let assoc_eq al ar = match al, ar with +| NonA, NonA +| RightA, RightA +| LeftA, LeftA -> true +| _, _ -> false + +(* [adjust_level assoc from prod] where [assoc] and [from] are the name + and associativity of the level where to add the rule; the meaning of + the result is + + None = SELF + Some None = NEXT + Some (Some (n,cur)) = constr LEVEL n + s.t. if [cur] is set then [n] is the same as the [from] level *) +let adjust_level assoc from = function +(* Associativity is None means force the level *) + | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) +(* Compute production name on the right side *) + (* If NonA or LeftA on the right-hand side, set to NEXT *) + | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) -> + Some None + (* If RightA on the right-hand side, set to the explicit (current) level *) + | (NumLevel n,BorderProd (Right,Some RightA)) -> + Some (Some (n,true)) +(* Compute production name on the left side *) + (* If NonA on the left-hand side, adopt the current assoc ?? *) + | (NumLevel n,BorderProd (Left,Some NonA)) -> None + (* If the expected assoc is the current one, set to SELF *) + | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) -> + None + (* Otherwise, force the level, n or n-1, according to expected assoc *) + | (NumLevel n,BorderProd (Left,Some a)) -> + begin match a with + | LeftA -> Some (Some (n, true)) + | _ -> Some None + end + (* None means NEXT *) + | (NextLevel,_) -> Some None +(* Compute production name elsewhere *) + | (NumLevel n,InternalProd) -> + if from = n + 1 then Some None else Some (Some (n, Int.equal n from)) + +type _ target = +| ForConstr : constr_expr target +| ForPattern : cases_pattern_expr target + +type prod_info = production_level * production_position + +type (_, _) entry = +| TTName : ('self, Misctypes.lname) entry +| TTReference : ('self, reference) entry +| TTBigint : ('self, Constrexpr.raw_natural_number) entry +| TTConstr : prod_info * 'r target -> ('r, 'r) entry +| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry +| TTPattern : int -> ('self, cases_pattern_expr) entry +| TTOpenBinderList : ('self, local_binder_expr list) entry +| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry + +type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry + +(* This computes the name of the level where to add a new rule *) +let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option = + fun forpat level -> match forpat with + | ForConstr -> + if level = 200 then Constr.binder_constr, None + else Constr.operconstr, Some level + | ForPattern -> Constr.pattern, Some level + +let target_entry : type s. s target -> s Gram.entry = function +| ForConstr -> Constr.operconstr +| ForPattern -> Constr.pattern + +let is_self from e = match e with +| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false +| (NumLevel n, BorderProd (Left, _)) -> Int.equal from n +| _ -> false + +let is_binder_level from e = match e with +| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200 +| _ -> false + +let make_sep_rules = function + | [tk] -> Atoken tk + | tkl -> + let rec mkrule : Tok.t list -> string rules = function + | [] -> Rules ({ norec_rule = Stop }, fun _ -> (* dropped anyway: *) "") + | tkn :: rem -> + let Rules ({ norec_rule = r }, f) = mkrule rem in + let r = { norec_rule = Next (r, Atoken tkn) } in + Rules (r, fun _ -> f) + in + let r = mkrule (List.rev tkl) in + Arules [r] + +let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat -> + if is_binder_level from p then Aentryl (target_entry forpat, 200) + else if is_self from p then Aself + else + let g = target_entry forpat in + let lev = adjust_level assoc from p in + begin match lev with + | None -> Aentry g + | Some None -> Anext + | Some (Some (lev, cur)) -> Aentryl (g, lev) + end + +let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with +| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat +| TTConstrList (typ', [], forpat) -> + Alist1 (symbol_of_target typ' assoc from forpat) +| TTConstrList (typ', tkl, forpat) -> + Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl) +| TTPattern p -> Aentryl (Constr.pattern, p) +| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder) +| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) +| TTName -> Aentry Prim.name +| TTOpenBinderList -> Aentry Constr.open_binders +| TTBigint -> Aentry Prim.bigint +| TTReference -> Aentry Constr.global + +let interp_entry forpat e = match e with +| ETProdName -> TTAny TTName +| ETProdReference -> TTAny TTReference +| ETProdBigint -> TTAny TTBigint +| ETProdConstr p -> TTAny (TTConstr (p, forpat)) +| ETProdPattern p -> TTAny (TTPattern p) +| ETProdOther _ -> assert false (** not used *) +| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) +| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList +| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) + +let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with + | Anonymous -> CPatAtom None + | Name id -> CPatAtom (Some (CAst.make ?loc @@ Ident id)) + +type 'r env = { + constrs : 'r list; + constrlists : 'r list list; + binders : cases_pattern_expr list; + binderlists : local_binder_expr list list; +} + +let push_constr subst v = { subst with constrs = v :: subst.constrs } + +let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v -> +match e with +| TTConstr _ -> push_constr subst v +| TTName -> + begin match forpat with + | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders } + | ForPattern -> push_constr subst (cases_pattern_expr_of_name v) + end +| TTPattern _ -> + begin match forpat with + | ForConstr -> { subst with binders = v :: subst.binders } + | ForPattern -> push_constr subst v + end +| TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists } +| TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } +| TTBigint -> + begin match forpat with + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (v,true))) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (v,true))) + end +| TTReference -> + begin match forpat with + | ForConstr -> push_constr subst (CAst.make @@ CRef (v, None)) + | ForPattern -> push_constr subst (CAst.make @@ CPatAtom (Some v)) + end +| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists } + +type (_, _) ty_symbol = +| TyTerm : Tok.t -> ('s, string) ty_symbol +| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol + +type ('self, _, 'r) ty_rule = +| TyStop : ('self, 'r, 'r) ty_rule +| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule +| TyMark : int * bool * int * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule + +type 'r gen_eval = Loc.t -> 'r env -> 'r + +let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> a = function +| TyStop -> + fun f env loc -> f loc env +| TyNext (rem, TyTerm _) -> + fun f env _ -> ty_eval rem f env +| TyNext (rem, TyNonTerm (_, _, _, false)) -> + fun f env _ -> ty_eval rem f env +| TyNext (rem, TyNonTerm (forpat, e, _, true)) -> + fun f env v -> + ty_eval rem f (push_item forpat e env v) +| TyMark (n, b, p, rem) -> + fun f env -> + let heads, constrs = List.chop n env.constrs in + let constrlists, constrs = + if b then + (* We rearrange constrs = c1..cn rem and constrlists = [d1..dr e1..ep] rem' into + constrs = e1..ep rem and constrlists [c1..cn d1..dr] rem' *) + let constrlist = List.hd env.constrlists in + let constrlist, tail = List.chop (List.length constrlist - p) constrlist in + (heads @ constrlist) :: List.tl env.constrlists, tail @ constrs + else + (* We rearrange constrs = c1..cn e1..ep rem into + constrs = e1..ep rem and add a constr list [c1..cn] *) + let constrlist, tail = List.chop (n - p) heads in + constrlist :: env.constrlists, tail @ constrs + in + ty_eval rem f { env with constrs; constrlists; } + +let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function +| TyStop -> Stop +| TyMark (_, _, _, r) -> ty_erase r +| TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok) +| TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s) + +type ('self, 'r) any_ty_rule = +| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule + +let make_ty_rule assoc from forpat prods = + let rec make_ty_rule = function + | [] -> AnyTyRule TyStop + | GramConstrTerminal tok :: rem -> + let AnyTyRule r = make_ty_rule rem in + AnyTyRule (TyNext (r, TyTerm tok)) + | GramConstrNonTerminal (e, var) :: rem -> + let AnyTyRule r = make_ty_rule rem in + let TTAny e = interp_entry forpat e in + let s = symbol_of_entry assoc from e in + let bind = match var with None -> false | Some _ -> true in + AnyTyRule (TyNext (r, TyNonTerm (forpat, e, s, bind))) + | GramConstrListMark (n, b, p) :: rem -> + let AnyTyRule r = make_ty_rule rem in + AnyTyRule (TyMark (n, b, p, r)) + in + make_ty_rule (List.rev prods) + +let target_to_bool : type r. r target -> bool = function +| ForConstr -> false +| ForPattern -> true + +let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = + let empty = (pos, [(name, p4assoc, [])]) in + if forpat then ExtendRule (Constr.pattern, reinit, empty) + else ExtendRule (Constr.operconstr, reinit, empty) + +let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with +| Stop -> [] +| Next (rem, Aentryl (_, i)) -> + let rem = pure_sublevels level rem in + begin match level with + | Some j when Int.equal i j -> rem + | _ -> i :: rem + end +| Next (rem, _) -> pure_sublevels level rem + +let make_act : type r. r target -> _ -> r gen_eval = function +| ForConstr -> fun notation loc env -> + let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in + CAst.make ~loc @@ CNotation (notation, env) +| ForPattern -> fun notation loc env -> + let env = (env.constrs, env.constrlists) in + CAst.make ~loc @@ CPatNotation (notation, env, []) + +let extend_constr state forpat ng = + let n,_,_ = ng.notgram_level in + let assoc = ng.notgram_assoc in + let (entry, level) = interp_constr_entry_key forpat n in + let fold (accu, state) pt = + let AnyTyRule r = make_ty_rule assoc n forpat pt in + let symbs = ty_erase r in + let pure_sublevels = pure_sublevels level symbs in + let isforpat = target_to_bool forpat in + let needed_levels, state = register_empty_levels state isforpat pure_sublevels in + let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in + let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in + let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in + let act = ty_eval r (make_act forpat ng.notgram_notation) empty in + let rule = (name, p4assoc, [Rule (symbs, act)]) in + let r = ExtendRule (entry, reinit, (pos, [rule])) in + (accu @ empty_rules @ [r], state) + in + List.fold_left fold ([], state) ng.notgram_prods + +let constr_levels = GramState.field () + +let extend_constr_notation ng state = + let levels = match GramState.get state constr_levels with + | None -> default_constr_levels + | Some lev -> lev + in + (* Add the notation in constr *) + let (r, levels) = extend_constr levels ForConstr ng in + (* Add the notation in cases_pattern *) + let (r', levels) = extend_constr levels ForPattern ng in + let state = GramState.set state constr_levels levels in + (r @ r', state) + +let constr_grammar : one_notation_grammar grammar_command = + create_grammar_command "Notation" extend_constr_notation + +let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli new file mode 100644 index 000000000..e15add10f --- /dev/null +++ b/vernac/egramcoq.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Mapping of grammar productions to camlp5 actions *) + +(** This is the part specific to Coq-level Notation and Tactic Notation. + For the ML-level tactic and vernac extensions, see Egramml. *) + +(** {5 Adding notations} *) + +val extend_constr_grammar : Notation_term.one_notation_grammar -> unit +(** Add a term notation rule to the parsing system. *) diff --git a/vernac/egramml.ml b/vernac/egramml.ml new file mode 100644 index 000000000..90cd7d10b --- /dev/null +++ b/vernac/egramml.ml @@ -0,0 +1,84 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +open Extend +open Pcoq +open Genarg +open Vernacexpr + +(** Grammar extensions declared at ML level *) + +type 's grammar_prod_item = + | GramTerminal of string + | GramNonTerminal : + ('a raw_abstract_argument_type option * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item + +type 'a ty_arg = ('a -> raw_generic_argument) + +type ('self, _, 'r) ty_rule = +| TyStop : ('self, 'r, 'r) ty_rule +| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) Extend.symbol * 'b ty_arg option -> + ('self, 'b -> 'a, 'r) ty_rule + +type ('self, 'r) any_ty_rule = +| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule + +let rec ty_rule_of_gram = function +| [] -> AnyTyRule TyStop +| GramTerminal s :: rem -> + let AnyTyRule rem = ty_rule_of_gram rem in + let tok = Atoken (CLexer.terminal s) in + let r = TyNext (rem, tok, None) in + AnyTyRule r +| GramNonTerminal (_, (t, tok)) :: rem -> + let AnyTyRule rem = ty_rule_of_gram rem in + let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in + let r = TyNext (rem, tok, inj) in + AnyTyRule r + +let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function +| TyStop -> Extend.Stop +| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok) + +type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r + +let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function +| TyStop -> fun f loc -> f loc [] +| TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f +| TyNext (rem, tok, Some inj) -> fun f x -> + let f loc args = f loc (inj x :: args) in + ty_eval rem f + +let make_rule f prod = + let AnyTyRule ty_rule = ty_rule_of_gram (List.rev prod) in + let symb = ty_erase ty_rule in + let f loc l = f loc (List.rev l) in + let act = ty_eval ty_rule f in + Extend.Rule (symb, act) + +(** Vernac grammar extensions *) + +let vernac_exts = ref [] + +let get_extend_vernac_rule (s, i) = + try + let find ((name, j), _) = String.equal name s && Int.equal i j in + let (_, rules) = List.find find !vernac_exts in + rules + with + | Failure _ -> raise Not_found + +let extend_vernac_command_grammar s nt gl = + let nt = Option.default Vernac_.command nt in + vernac_exts := (s,gl) :: !vernac_exts; + let mkact loc l = VernacExtend (s, l) in + let rules = [make_rule mkact gl] in + grammar_extend nt None (None, [None, None, rules]) diff --git a/vernac/egramml.mli b/vernac/egramml.mli new file mode 100644 index 000000000..31aa1a989 --- /dev/null +++ b/vernac/egramml.mli @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Vernacexpr + +(** Mapping of grammar productions to camlp5 actions. *) + +(** This is the part specific to vernac extensions. + For the Coq-level Notation and Tactic Notation, see Egramcoq. *) + +type 's grammar_prod_item = + | GramTerminal of string + | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option * + ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item + +val extend_vernac_command_grammar : + Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option -> + vernac_expr grammar_prod_item list -> unit + +val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list + +(** Utility function reused in Egramcoq : *) + +val make_rule : + (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> + 'a grammar_prod_item list -> 'a Extend.production_rule diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml new file mode 100644 index 000000000..7a34e8027 --- /dev/null +++ b/vernac/ppvernac.ml @@ -0,0 +1,1219 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open Names + +open CErrors +open Util +open CAst + +open Extend +open Libnames +open Decl_kinds +open Constrexpr +open Constrexpr_ops +open Vernacexpr +open Declaremods +open Pputils + + open Ppconstr + + let do_not_tag _ x = x + let tag_keyword = do_not_tag () + let tag_vernac = do_not_tag + + let keyword s = tag_keyword (str s) + + let pr_constr = pr_constr_expr + let pr_lconstr = pr_lconstr_expr + let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr + + let pr_uconstraint (l, d, r) = + pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ + pr_glob_level r + + let pr_univ_name_list = function + | None -> mt () + | Some l -> + str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}" + + let pr_univdecl_instance l extensible = + prlist_with_sep spc pr_lident l ++ + (if extensible then str"+" else mt ()) + + let pr_univdecl_constraints l extensible = + if List.is_empty l && extensible then mt () + else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++ + (if extensible then str"+" else mt()) + + let pr_universe_decl l = + let open Misctypes in + match l with + | None -> mt () + | Some l -> + str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++ + pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}" + + let pr_ident_decl (lid, l) = + pr_lident lid ++ pr_universe_decl l + + let string_of_fqid fqid = + String.concat "." (List.map Id.to_string fqid) + + let pr_fqid fqid = str (string_of_fqid fqid) + + let pr_lfqid {CAst.loc;v=fqid} = + match loc with + | None -> pr_fqid fqid + | Some loc -> let (b,_) = Loc.unloc loc in + pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid + + let pr_lname_decl (n, u) = + pr_lname n ++ pr_universe_decl u + + let pr_smart_global = Pputils.pr_or_by_notation pr_reference + + let pr_ltac_ref = Libnames.pr_reference + + let pr_module = Libnames.pr_reference + + let pr_import_module = Libnames.pr_reference + + let sep_end = function + | VernacBullet _ + | VernacSubproof _ + | VernacEndSubproof -> str"" + | _ -> str"." + + let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t + + let sep = fun _ -> spc() + let sep_v2 = fun _ -> str"," ++ spc() + + let pr_at_level = function + | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n + | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" + + let pr_constr_as_binder_kind = function + | AsIdent -> keyword "as ident" + | AsIdentOrPattern -> keyword "as pattern" + | AsStrictPattern -> keyword "as strict pattern" + + let pr_strict b = if b then str "strict " else mt () + + let pr_set_entry_type pr = function + | ETName -> str"ident" + | ETReference -> str"global" + | ETPattern (b,None) -> pr_strict b ++ str"pattern" + | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n) + | ETConstr lev -> str"constr" ++ pr lev + | ETOther (_,e) -> str e + | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk + | ETBigint -> str "bigint" + | ETBinder true -> str "binder" + | ETBinder false -> str "closed binder" + + let pr_at_level_opt = function + | None -> mt () + | Some n -> spc () ++ pr_at_level n + + let pr_set_simple_entry_type = + pr_set_entry_type pr_at_level_opt + + let pr_comment pr_c = function + | CommentConstr c -> pr_c c + | CommentString s -> qs s + | CommentInt n -> int n + + let pr_in_out_modules = function + | SearchInside l -> spc() ++ keyword "inside" ++ spc() ++ prlist_with_sep sep pr_module l + | SearchOutside [] -> mt() + | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l + + let pr_search_about (b,c) = + (if b then str "-" else mt()) ++ + match c with + | SearchSubPattern p -> pr_constr_pattern_expr p + | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + + let pr_search a gopt b pr_p = + pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt + ++ + match a with + | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b + | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b + | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b + | SearchAbout sl -> + keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + + let pr_locality local = if local then keyword "Local" else keyword "Global" + + let pr_option_ref_value = function + | QualidRefValue id -> pr_reference id + | StringRefValue s -> qs s + + let pr_printoption table b = + prlist_with_sep spc str table ++ + pr_opt (prlist_with_sep sep pr_option_ref_value) b + + let pr_set_option a b = + let pr_opt_value = function + | IntValue None -> assert false + (* This should not happen because of the grammar *) + | IntValue (Some n) -> spc() ++ int n + | StringValue s -> spc() ++ str s + | StringOptValue None -> mt() + | StringOptValue (Some s) -> spc() ++ str s + | BoolValue b -> mt() + in pr_printoption a None ++ pr_opt_value b + + let pr_opt_hintbases l = match l with + | [] -> mt() + | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z + + let pr_reference_or_constr pr_c = function + | HintsReference r -> pr_reference r + | HintsConstr c -> pr_c c + + let pr_hint_mode = function + | ModeInput -> str"+" + | ModeNoHeadEvar -> str"!" + | ModeOutput -> str"-" + + let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } = + pr_opt (fun x -> str"|" ++ int x) pri ++ + pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat + + let pr_hints db h pr_c pr_pat = + let opth = pr_opt_hintbases db in + let pph = + match h with + | HintsResolve l -> + keyword "Resolve " ++ prlist_with_sep sep + (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info) + l + | HintsImmediate l -> + keyword "Immediate" ++ spc() ++ + prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l + | HintsUnfold l -> + keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l + | HintsTransparency (l, b) -> + keyword (if b then "Transparent" else "Opaque") + ++ spc () + ++ prlist_with_sep sep pr_reference l + | HintsMode (m, l) -> + keyword "Mode" + ++ spc () + ++ pr_reference m ++ spc() ++ + prlist_with_sep spc pr_hint_mode l + | HintsConstructors c -> + keyword "Constructors" + ++ spc() ++ prlist_with_sep spc pr_reference c + | HintsExtern (n,c,tac) -> + let pat = match c with None -> mt () | Some pat -> pr_pat pat in + keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ + spc() ++ Pputils.pr_raw_generic (Global.env ()) tac + in + hov 2 (keyword "Hint "++ pph ++ opth) + + let pr_with_declaration pr_c = function + | CWith_Definition (id,udecl,c) -> + let p = pr_c c in + keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p + | CWith_Module (id,qid) -> + keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ + pr_ast pr_qualid qid + + let rec pr_module_ast leading_space pr_c = function + | { loc ; v = CMident qid } -> + if leading_space then + spc () ++ pr_located pr_qualid (loc, qid) + else + pr_located pr_qualid (loc,qid) + | { v = CMwith (mty,decl) } -> + let m = pr_module_ast leading_space pr_c mty in + let p = pr_with_declaration pr_c decl in + m ++ spc() ++ keyword "with" ++ spc() ++ p + | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } -> + pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2 + | { v = CMapply (me1,me2) } -> + pr_module_ast leading_space pr_c me1 ++ spc() ++ + hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")") + + let pr_inline = function + | DefaultInline -> mt () + | NoInline -> str "[no inline]" + | InlineAt i -> str "[inline at level " ++ int i ++ str "]" + + let pr_assumption_inline = function + | DefaultInline -> str "Inline" + | NoInline -> mt () + | InlineAt i -> str "Inline(" ++ int i ++ str ")" + + let pr_module_ast_inl leading_space pr_c (mast,inl) = + pr_module_ast leading_space pr_c mast ++ pr_inline inl + + let pr_of_module_type prc = function + | Enforce mty -> str ":" ++ pr_module_ast_inl true prc mty + | Check mtys -> + prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl true prc m) mtys + + let pr_require_token = function + | Some true -> + keyword "Export" ++ spc () + | Some false -> + keyword "Import" ++ spc () + | None -> mt() + + let pr_module_vardecls pr_c (export,idl,(mty,inl)) = + let m = pr_module_ast true pr_c mty in + spc() ++ + hov 1 (str"(" ++ pr_require_token export ++ + prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")") + + let pr_module_binders l pr_c = + prlist_strict (pr_module_vardecls pr_c) l + + let pr_type_option pr_c = function + | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() + | _ as c -> brk(0,2) ++ str" :" ++ pr_c c + + let pr_decl_notation prc ({loc; v=ntn},c,scopt) = + fnl () ++ keyword "where " ++ qs ntn ++ str " := " + ++ Flags.without_option Flags.beautify prc c ++ + pr_opt (fun sc -> str ": " ++ str sc) scopt + + let pr_binders_arg = + pr_non_empty_arg pr_binders + + let pr_and_type_binders_arg bl = + pr_binders_arg bl + + let pr_onescheme (idop,schem) = + match schem with + | InductionScheme (dep,ind,s) -> + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc () + ) ++ + hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for") + ++ spc() ++ pr_smart_global ind) ++ spc() ++ + hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s) + | CaseScheme (dep,ind,s) -> + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc () + ) ++ + hov 0 ((if dep then keyword "Elimination for" else keyword "Case for") + ++ spc() ++ pr_smart_global ind) ++ spc() ++ + hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s) + | EqualityScheme ind -> + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc() + ) ++ + hov 0 (keyword "Equality for") + ++ spc() ++ pr_smart_global ind + + let begin_of_inductive = function + | [] -> 0 + | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc + + let pr_class_rawexpr = function + | FunClass -> keyword "Funclass" + | SortClass -> keyword "Sortclass" + | RefClass qid -> pr_smart_global qid + + let pr_assumption_token many discharge kind = + match discharge, kind with + | (NoDischarge,Logical) -> + keyword (if many then "Axioms" else "Axiom") + | (NoDischarge,Definitional) -> + keyword (if many then "Parameters" else "Parameter") + | (NoDischarge,Conjectural) -> str"Conjecture" + | (DoDischarge,Logical) -> + keyword (if many then "Hypotheses" else "Hypothesis") + | (DoDischarge,Definitional) -> + keyword (if many then "Variables" else "Variable") + | (DoDischarge,Conjectural) -> + anomaly (Pp.str "Don't know how to beautify a local conjecture.") + + let pr_params pr_c (xl,(c,t)) = + hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ + (if c then str":>" else str":" ++ + spc() ++ pr_c t)) + + let rec factorize = function + | [] -> [] + | (c,(idl,t))::l -> + match factorize l with + | (xl,((c', t') as r))::l' + when (c : bool) == c' && Pervasives.(=) t t' -> + (** FIXME: we need equality on constr_expr *) + (idl@xl,r)::l' + | l' -> (idl,(c,t))::l' + + let pr_ne_params_list pr_c l = + match factorize l with + | [p] -> pr_params pr_c p + | l -> + prlist_with_sep spc + (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l + +(* + prlist_with_sep pr_semicolon (pr_params pr_c) +*) + + let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) + + let pr_syntax_modifier = function + | SetItemLevel (l,n) -> + prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n + | SetItemLevelAsBinder (l,bk,n) -> + prlist_with_sep sep_v2 str l ++ + spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk + | SetLevel n -> pr_at_level (NumLevel n) + | SetAssoc LeftA -> keyword "left associativity" + | SetAssoc RightA -> keyword "right associativity" + | SetAssoc NonA -> keyword "no associativity" + | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ + | SetOnlyPrinting -> keyword "only printing" + | SetOnlyParsing -> keyword "only parsing" + | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") + | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s + | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s + + let pr_syntax_modifiers = function + | [] -> mt() + | l -> spc() ++ + hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") + + let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) = + let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in + let annot = pr_guard_annot pr_lconstr_expr bl ro in + pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot + ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ + ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def + ++ prlist (pr_decl_notation pr_constr) ntn + + let pr_statement head (idpl,(bl,c)) = + hov 2 + (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++ + (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ + str":" ++ pr_spc_lconstr c) + +(**************************************) +(* Pretty printer for vernac commands *) +(**************************************) + + let pr_constrarg c = spc () ++ pr_constr c + let pr_lconstrarg c = spc () ++ pr_lconstr c + let pr_intarg n = spc () ++ int n + + let pr_oc = function + | None -> str" :" + | Some true -> str" :>" + | Some false -> str" :>>" + + let pr_record_field ((x, pri), ntn) = + let prx = match x with + | (oc,AssumExpr (id,t)) -> + hov 1 (pr_lname id ++ + pr_oc oc ++ spc() ++ + pr_lconstr_expr t) + | (oc,DefExpr(id,b,opt)) -> (match opt with + | Some t -> + hov 1 (pr_lname id ++ + pr_oc oc ++ spc() ++ + pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) + | None -> + hov 1 (pr_lname id ++ str" :=" ++ spc() ++ + pr_lconstr b)) in + let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in + prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn + + let pr_record_decl b c fs = + pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ + hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") + + let pr_printable = function + | PrintFullContext -> + keyword "Print All" + | PrintSectionContext s -> + keyword "Print Section" ++ spc() ++ Libnames.pr_reference s + | PrintGrammar ent -> + keyword "Print Grammar" ++ spc() ++ str ent + | PrintLoadPath dir -> + keyword "Print LoadPath" ++ pr_opt DirPath.print dir + | PrintModules -> + keyword "Print Modules" + | PrintMLLoadPath -> + keyword "Print ML Path" + | PrintMLModules -> + keyword "Print ML Modules" + | PrintDebugGC -> + keyword "Print ML GC" + | PrintGraph -> + keyword "Print Graph" + | PrintClasses -> + keyword "Print Classes" + | PrintTypeClasses -> + keyword "Print TypeClasses" + | PrintInstances qid -> + keyword "Print Instances" ++ spc () ++ pr_smart_global qid + | PrintCoercions -> + keyword "Print Coercions" + | PrintCoercionPaths (s,t) -> + keyword "Print Coercion Paths" ++ spc() + ++ pr_class_rawexpr s ++ spc() + ++ pr_class_rawexpr t + | PrintCanonicalConversions -> + keyword "Print Canonical Structures" + | PrintTables -> + keyword "Print Tables" + | PrintHintGoal -> + keyword "Print Hint" + | PrintHint qid -> + keyword "Print Hint" ++ spc () ++ pr_smart_global qid + | PrintHintDb -> + keyword "Print Hint *" + | PrintHintDbName s -> + keyword "Print HintDb" ++ spc () ++ str s + | PrintUniverses (b, fopt) -> + let cmd = + if b then "Print Sorted Universes" + else "Print Universes" + in + keyword cmd ++ pr_opt str fopt + | PrintName (qid,udecl) -> + keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl + | PrintModuleType qid -> + keyword "Print Module Type" ++ spc() ++ pr_reference qid + | PrintModule qid -> + keyword "Print Module" ++ spc() ++ pr_reference qid + | PrintInspect n -> + keyword "Inspect" ++ spc() ++ int n + | PrintScopes -> + keyword "Print Scopes" + | PrintScope s -> + keyword "Print Scope" ++ spc() ++ str s + | PrintVisibility s -> + keyword "Print Visibility" ++ pr_opt str s + | PrintAbout (qid,l,gopt) -> + pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt + ++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l + | PrintImplicit qid -> + keyword "Print Implicit" ++ spc() ++ pr_smart_global qid + (* spiwack: command printing all the axioms and section variables used in a + term *) + | PrintAssumptions (b, t, qid) -> + let cmd = match b, t with + | true, true -> "Print All Dependencies" + | true, false -> "Print Opaque Dependencies" + | false, true -> "Print Transparent Dependencies" + | false, false -> "Print Assumptions" + in + keyword cmd ++ spc() ++ pr_smart_global qid + | PrintNamespace dp -> + keyword "Print Namespace" ++ DirPath.print dp + | PrintStrategy None -> + keyword "Print Strategies" + | PrintStrategy (Some qid) -> + keyword "Print Strategy" ++ pr_smart_global qid + + let pr_using e = + let rec aux = function + | SsEmpty -> "()" + | SsType -> "(Type)" + | SsSingl { v=id } -> "("^Id.to_string id^")" + | SsCompl e -> "-" ^ aux e^"" + | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" + | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" + | SsFwdClose e -> "("^aux e^")*" + in Pp.str (aux e) + + let pr_extend s cl = + let pr_arg a = + try pr_gen a + with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in + try + let rl = Egramml.get_extend_vernac_rule s in + let rec aux rl cl = + match rl, cl with + | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl + | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl + | [], [] -> [] + | _ -> assert false in + hov 1 (pr_sequence identity (aux rl cl)) + with Not_found -> + hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") + + let pr_vernac_expr v = + let return = tag_vernac v in + match v with + | VernacLoad (f,s) -> + return ( + keyword "Load" + ++ if f then + (spc() ++ keyword "Verbose" ++ spc()) + else + spc() ++ qs s + ) + + (* Proof management *) + | VernacAbortAll -> + return (keyword "Abort All") + | VernacRestart -> + return (keyword "Restart") + | VernacUnfocus -> + return (keyword "Unfocus") + | VernacUnfocused -> + return (keyword "Unfocused") + | VernacAbort id -> + return (keyword "Abort" ++ pr_opt pr_lident id) + | VernacUndo i -> + return ( + if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i + ) + | VernacUndoTo i -> + return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i) + | VernacFocus i -> + return (keyword "Focus" ++ pr_opt int i) + | VernacShow s -> + let pr_goal_reference = function + | OpenSubgoals -> mt () + | NthGoal n -> spc () ++ int n + | GoalId id -> spc () ++ pr_id id + in + let pr_showable = function + | ShowGoal n -> keyword "Show" ++ pr_goal_reference n + | ShowProof -> keyword "Show Proof" + | ShowScript -> keyword "Show Script" + | ShowExistentials -> keyword "Show Existentials" + | ShowUniverses -> keyword "Show Universes" + | ShowProofNames -> keyword "Show Conjectures" + | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") + | ShowMatch id -> keyword "Show Match " ++ pr_reference id + in + return (pr_showable s) + | VernacCheckGuard -> + return (keyword "Guarded") + + (* Resetting *) + | VernacResetName id -> + return (keyword "Reset" ++ spc() ++ pr_lident id) + | VernacResetInitial -> + return (keyword "Reset Initial") + | VernacBack i -> + return ( + if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i + ) + | VernacBackTo i -> + return (keyword "BackTo" ++ pr_intarg i) + + (* State management *) + | VernacWriteState s -> + return (keyword "Write State" ++ spc () ++ qs s) + | VernacRestoreState s -> + return (keyword "Restore State" ++ spc() ++ qs s) + + (* Syntax *) + | VernacOpenCloseScope (opening,sc) -> + return ( + keyword (if opening then "Open " else "Close ") ++ + keyword "Scope" ++ spc() ++ str sc + ) + | VernacDelimiters (sc,Some key) -> + return ( + keyword "Delimit Scope" ++ spc () ++ str sc ++ + spc() ++ keyword "with" ++ spc () ++ str key + ) + | VernacDelimiters (sc, None) -> + return ( + keyword "Undelimit Scope" ++ spc () ++ str sc + ) + | VernacBindScope (sc,cll) -> + return ( + keyword "Bind Scope" ++ spc () ++ str sc ++ + spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll + ) + | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) + return ( + hov 0 (hov 0 (keyword "Infix " + ++ qs s ++ str " :=" ++ pr_constrarg q) ++ + pr_syntax_modifiers mv ++ + (match sn with + | None -> mt() + | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) + ) + | VernacNotation (c,({v=s},l),opt) -> + return ( + hov 2 (keyword "Notation" ++ spc() ++ qs s ++ + str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++ + (match opt with + | None -> mt() + | Some sc -> str" :" ++ spc() ++ str sc)) + ) + | VernacSyntaxExtension (_, (s, l)) -> + return ( + keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++ + pr_syntax_modifiers l + ) + | VernacNotationAddFormat(s,k,v) -> + return ( + keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v + ) + + (* Gallina *) + | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *) + let pr_def_token dk = + keyword ( + if Name.is_anonymous (fst id).v + then "Goal" + else Kindops.string_of_definition_object_kind dk) + in + let pr_reduce = function + | None -> mt() + | Some r -> + keyword "Eval" ++ spc() ++ + pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ + keyword " in" ++ spc() + in + let pr_def_body = function + | DefineBody (bl,red,body,d) -> + let ty = match d with + | None -> mt() + | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty + in + (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) + | ProveBody (bl,t) -> + let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in + (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in + let (binds,typ,c) = pr_def_body b in + return ( + hov 2 ( + pr_def_token kind ++ spc() + ++ pr_lname_decl id ++ binds ++ typ + ++ (match c with + | None -> mt() + | Some cc -> str" :=" ++ spc() ++ cc)) + ) + + | VernacStartTheoremProof (ki,l) -> + return ( + hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ + prlist (pr_statement (spc () ++ keyword "with")) (List.tl l)) + ) + + | VernacEndProof Admitted -> + return (keyword "Admitted") + + | VernacEndProof (Proved (opac,o)) -> return ( + let open Proof_global in + match o with + | None -> (match opac with + | Transparent -> keyword "Defined" + | Opaque -> keyword "Qed") + | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id + ) + | VernacExactProof c -> + return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) + | VernacAssumption ((discharge,kind),t,l) -> + let n = List.length (List.flatten (List.map fst (List.map snd l))) in + let pr_params (c, (xl, t)) = + hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++ + (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in + let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in + return (hov 2 (pr_assumption_token (n > 1) discharge kind ++ + pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) + | VernacInductive (cum, p,f,l) -> + let pr_constructor (coe,(id,c)) = + hov 2 (pr_lident id ++ str" " ++ + (if coe then str":>" else str":") ++ + Flags.without_option Flags.beautify pr_spc_lconstr c) + in + let pr_constructor_list b l = match l with + | Constructors [] -> mt() + | Constructors l -> + let fst_sep = match l with [_] -> " " | _ -> " | " in + pr_com_at (begin_of_inductive l) ++ + fnl() ++ str fst_sep ++ + prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l + | RecordDecl (c,fs) -> + pr_record_decl b c fs + in + let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) = + hov 0 ( + str key ++ spc() ++ + (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++ + pr_and_type_binders_arg indpar ++ + pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++ + str" :=") ++ pr_constructor_list k lc ++ + prlist (pr_decl_notation pr_constr) ntn + in + let key = + let (_,_,_,k,_),_ = List.hd l in + let kind = + match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class _ -> "Class" | Variant -> "Variant" + in + if p then + let cm = + match cum with + | Some VernacCumulative -> "Cumulative" + | Some VernacNonCumulative -> "NonCumulative" + | None -> "" + in + cm ^ " " ^ kind + else kind + in + return ( + hov 1 (pr_oneind key (List.hd l)) ++ + (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) + ) + + | VernacFixpoint (local, recs) -> + let local = match local with + | DoDischarge -> "Let " + | NoDischarge -> "" + in + return ( + hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ + prlist_with_sep (fun _ -> fnl () ++ keyword "with" + ++ spc ()) pr_rec_definition recs) + ) + + | VernacCoFixpoint (local, corecs) -> + let local = match local with + | DoDischarge -> keyword "Let" ++ spc () + | NoDischarge -> str "" + in + let pr_onecorec ((iddecl,bl,c,def),ntn) = + pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ + spc() ++ pr_lconstr_expr c ++ + pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++ + prlist (pr_decl_notation pr_constr) ntn + in + return ( + hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) + ) + | VernacScheme l -> + return ( + hov 2 (keyword "Scheme" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l) + ) + | VernacCombinedScheme (id, l) -> + return ( + hov 2 (keyword "Combined Scheme" ++ spc() ++ + pr_lident id ++ spc() ++ keyword "from" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) + ) + | VernacUniverse v -> + return ( + hov 2 (keyword "Universe" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_lident v) + ) + | VernacConstraint v -> + return ( + hov 2 (keyword "Constraint" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_uconstraint v) + ) + + (* Gallina extensions *) + | VernacBeginSection id -> + return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id)) + | VernacEndSegment id -> + return (hov 2 (keyword "End" ++ spc() ++ pr_lident id)) + | VernacNameSectionHypSet (id,set) -> + return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++ + str ":="++spc()++pr_using set)) + | VernacRequire (from, exp, l) -> + let from = match from with + | None -> mt () + | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc () + in + return ( + hov 2 + (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++ + prlist_with_sep sep pr_module l) + ) + | VernacImport (f,l) -> + return ( + (if f then keyword "Export" else keyword "Import") ++ spc() ++ + prlist_with_sep sep pr_import_module l + ) + | VernacCanonical q -> + return ( + keyword "Canonical Structure" ++ spc() ++ pr_smart_global q + ) + | VernacCoercion (id,c1,c2) -> + return ( + hov 1 ( + keyword "Coercion" ++ spc() ++ + pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ + spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) + ) + | VernacIdentityCoercion (id,c1,c2) -> + return ( + hov 1 ( + keyword "Identity Coercion" ++ spc() ++ pr_lident id ++ + spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ + spc() ++ pr_class_rawexpr c2) + ) + + | VernacInstance (abst, sup, (instid, bk, cl), props, info) -> + return ( + hov 1 ( + (if abst then keyword "Declare" ++ spc () else mt ()) ++ + keyword "Instance" ++ + (match instid with + | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc () + | { v = Anonymous }, _ -> mt ()) ++ + pr_and_type_binders_arg sup ++ + str":" ++ spc () ++ + (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ + pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ + (match props with + | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true,_) -> assert false + | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p + | None -> mt())) + ) + + | VernacContext l -> + return ( + hov 1 ( + keyword "Context" ++ pr_and_type_binders_arg l) + ) + + | VernacDeclareInstances insts -> + let pr_inst (id, info) = + pr_reference id ++ pr_hint_info pr_constr_pattern_expr info + in + return ( + hov 1 (keyword "Existing" ++ spc () ++ + keyword(String.plural (List.length insts) "Instance") ++ + spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts) + ) + + | VernacDeclareClass id -> + return ( + hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id) + ) + + (* Modules and Module Types *) + | VernacDefineModule (export,m,bl,tys,bd) -> + let b = pr_module_binders bl pr_lconstr in + return ( + hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++ + pr_lident m ++ b ++ + pr_of_module_type pr_lconstr tys ++ + (if List.is_empty bd then mt () else str ":= ") ++ + prlist_with_sep (fun () -> str " <+") + (pr_module_ast_inl true pr_lconstr) bd) + ) + | VernacDeclareModule (export,id,bl,m1) -> + let b = pr_module_binders bl pr_lconstr in + return ( + hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++ + pr_lident id ++ b ++ str " :" ++ + pr_module_ast_inl true pr_lconstr m1) + ) + | VernacDeclareModuleType (id,bl,tyl,m) -> + let b = pr_module_binders bl pr_lconstr in + let pr_mt = pr_module_ast_inl true pr_lconstr in + return ( + hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++ + prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++ + (if List.is_empty m then mt () else str ":= ") ++ + prlist_with_sep (fun () -> str " <+ ") pr_mt m) + ) + | VernacInclude (mexprs) -> + let pr_m = pr_module_ast_inl false pr_lconstr in + return ( + hov 2 (keyword "Include" ++ spc() ++ + prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) + ) + (* Solving *) + | VernacSolveExistential (i,c) -> + return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) + + (* Auxiliary file and library management *) + | VernacAddLoadPath (fl,s,d) -> + return ( + hov 2 + (keyword "Add" ++ + (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ + keyword "LoadPath" ++ spc() ++ qs s ++ + (match d with + | None -> mt() + | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) + ) + | VernacRemoveLoadPath s -> + return (keyword "Remove LoadPath" ++ qs s) + | VernacAddMLPath (fl,s) -> + return ( + keyword "Add" + ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) + ++ keyword "ML Path" + ++ qs s + ) + | VernacDeclareMLModule (l) -> + return ( + hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l) + ) + | VernacChdir s -> + return (keyword "Cd" ++ pr_opt qs s) + + (* Commands *) + | VernacCreateHintDb (dbname,b) -> + return ( + hov 1 (keyword "Create HintDb" ++ spc () ++ + str dbname ++ (if b then str" discriminated" else mt ())) + ) + | VernacRemoveHints (dbnames, ids) -> + return ( + hov 1 (keyword "Remove Hints" ++ spc () ++ + prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ + pr_opt_hintbases dbnames) + ) + | VernacHints (dbnames,h) -> + return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) + | VernacSyntacticDefinition (id,(ids,c),compat) -> + return ( + hov 2 + (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ + prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ + pr_syntax_modifiers + (match compat with + | None -> [] + | Some Flags.Current -> [SetOnlyParsing] + | Some v -> [SetCompatVersion v])) + ) + | VernacArguments (q, args, more_implicits, nargs, mods) -> + return ( + hov 2 ( + keyword "Arguments" ++ spc() ++ + pr_smart_global q ++ + let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in + let pr_if b x = if b then x else str "" in + let pr_br imp x = match imp with + | Vernacexpr.Implicit -> str "[" ++ x ++ str "]" + | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}" + | Vernacexpr.NotImplicit -> x in + let rec print_arguments n l = + match n, l with + | Some 0, l -> spc () ++ str"/" ++ print_arguments None l + | _, [] -> mt() + | n, { name = id; recarg_like = k; + notation_scope = s; + implicit_status = imp } :: tl -> + spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++ + print_arguments (Option.map pred n) tl + in + let rec print_implicits = function + | [] -> mt () + | (name, impl) :: rest -> + spc() ++ pr_br impl (Name.print name) ++ print_implicits rest + in + print_arguments nargs args ++ + if not (List.is_empty more_implicits) then + prlist (fun l -> str"," ++ print_implicits l) more_implicits + else (mt ()) ++ + (if not (List.is_empty mods) then str" : " else str"") ++ + prlist_with_sep (fun () -> str", " ++ spc()) (function + | `ReductionDontExposeCase -> keyword "simpl nomatch" + | `ReductionNeverUnfold -> keyword "simpl never" + | `DefaultImplicits -> keyword "default implicits" + | `Rename -> keyword "rename" + | `Assert -> keyword "assert" + | `ExtraScopes -> keyword "extra scopes" + | `ClearImplicits -> keyword "clear implicits" + | `ClearScopes -> keyword "clear scopes") + mods) + ) + | VernacReserve bl -> + let n = List.length (List.flatten (List.map fst bl)) in + return ( + hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " ")) + ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl)) + ) + | VernacGeneralizable g -> + return ( + hov 1 (tag_keyword ( + str"Generalizable Variable" ++ + match g with + | None -> str "s none" + | Some [] -> str "s all" + | Some idl -> + str (if List.length idl > 1 then "s " else " ") ++ + prlist_with_sep spc pr_lident idl) + )) + | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k -> + return ( + hov 1 (keyword "Transparent" ++ + spc() ++ prlist_with_sep sep pr_smart_global l) + ) + | VernacSetOpacity(Conv_oracle.Opaque,l) -> + return ( + hov 1 (keyword "Opaque" ++ + spc() ++ prlist_with_sep sep pr_smart_global l) + ) + | VernacSetOpacity _ -> + return ( + CErrors.anomaly (keyword "VernacSetOpacity used to set something else.") + ) + | VernacSetStrategy l -> + let pr_lev = function + | Conv_oracle.Opaque -> keyword "opaque" + | Conv_oracle.Expand -> keyword "expand" + | l when Conv_oracle.is_transparent l -> keyword "transparent" + | Conv_oracle.Level n -> int n + in + let pr_line (l,q) = + hov 2 (pr_lev l ++ spc() ++ + str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") + in + return ( + hov 1 (keyword "Strategy" ++ spc() ++ + hv 0 (prlist_with_sep sep pr_line l)) + ) + | VernacUnsetOption (export, na) -> + let export = if export then keyword "Export" ++ spc () else mt () in + return ( + hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None) + ) + | VernacSetOption (export, na,v) -> + let export = if export then keyword "Export" ++ spc () else mt () in + return ( + hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v) + ) + | VernacAddOption (na,l) -> + return ( + hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacRemoveOption (na,l) -> + return ( + hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacMemOption (na,l) -> + return ( + hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacPrintOption na -> + return ( + hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None) + ) + | VernacCheckMayEval (r,io,c) -> + let pr_mayeval r c = match r with + | Some r0 -> + hov 2 (keyword "Eval" ++ spc() ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ + spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) + | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) + in + let pr_i = match io with None -> mt () + | Some i -> Goal_select.pr_goal_selector i ++ str ": " in + return (pr_i ++ pr_mayeval r c) + | VernacGlobalCheck c -> + return (hov 2 (keyword "Type" ++ pr_constrarg c)) + | VernacDeclareReduction (s,r) -> + return ( + keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r + ) + | VernacPrint p -> + return (pr_printable p) + | VernacSearch (sea,g,sea_r) -> + return (pr_search sea g sea_r pr_constr_pattern_expr) + | VernacLocate loc -> + let pr_locate =function + | LocateAny qid -> pr_smart_global qid + | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid + | LocateFile f -> keyword "File" ++ spc() ++ qs f + | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid + | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid + | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid + in + return (keyword "Locate" ++ spc() ++ pr_locate loc) + | VernacRegister (id, RegisterInline) -> + return ( + hov 2 + (keyword "Register Inline" ++ spc() ++ pr_lident id) + ) + | VernacComments l -> + return ( + hov 2 + (keyword "Comments" ++ spc() + ++ prlist_with_sep sep (pr_comment pr_constr) l) + ) + + (* For extension *) + | VernacExtend (s,c) -> + return (pr_extend s c) + | VernacProof (None, None) -> + return (keyword "Proof") + | VernacProof (None, Some e) -> + return (keyword "Proof " ++ spc () ++ + keyword "using" ++ spc() ++ pr_using e) + | VernacProof (Some te, None) -> + return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te) + | VernacProof (Some te, Some e) -> + return ( + keyword "Proof" ++ spc () ++ + keyword "using" ++ spc() ++ pr_using e ++ spc() ++ + keyword "with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te + ) + | VernacProofMode s -> + return (keyword "Proof Mode" ++ str s) + | VernacBullet b -> + (* XXX: Redundant with Proof_bullet.print *) + return (let open Proof_bullet in begin match b with + | Dash n -> str (String.make n '-') + | Star n -> str (String.make n '*') + | Plus n -> str (String.make n '+') + end) + | VernacSubproof None -> + return (str "{") + | VernacSubproof (Some i) -> + return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") + | VernacEndSubproof -> + return (str "}") + +let pr_vernac_flag = + function + | VernacPolymorphic true -> keyword "Polymorphic" + | VernacPolymorphic false -> keyword "Monomorphic" + | VernacProgram -> keyword "Program" + | VernacLocal local -> pr_locality local + + let rec pr_vernac_control v = + let return = tag_vernac v in + match v with + | VernacExpr (f, v') -> + List.fold_right + (fun f a -> pr_vernac_flag f ++ spc() ++ a) + f + (pr_vernac_expr v' ++ sep_end v') + | VernacTime (_,{v}) -> + return (keyword "Time" ++ spc() ++ pr_vernac_control v) + | VernacRedirect (s, {v}) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) + | VernacTimeout(n,v) -> + return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v) + | VernacFail v -> + return (keyword "Fail" ++ spc() ++ pr_vernac_control v) + + let pr_vernac v = + try pr_vernac_control v + with e -> CErrors.print e diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli new file mode 100644 index 000000000..4aa24bf5d --- /dev/null +++ b/vernac/ppvernac.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module implements pretty-printers for vernac_expr syntactic + objects and their subcomponents. *) + +val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t + +(** Prints a fixpoint body *) +val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t + +(** Prints a vernac expression without dot *) +val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t + +(** Prints a "proof using X" clause. *) +val pr_using : Vernacexpr.section_subset_expr -> Pp.t + +(** Prints a vernac expression and closes it with a dot. *) +val pr_vernac : Vernacexpr.vernac_control -> Pp.t diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index f001b572a..6fceda56d 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,10 +1,14 @@ Vernacprop -Proof_using -Lemmas Himsg ExplainErr -Class Locality +Egramml +Vernacinterp +Ppvernac +Proof_using +Lemmas +Class +Egramcoq Metasyntax Auto_ind_decl Search @@ -20,7 +24,6 @@ Classes Record Assumptions Vernacstate -Vernacinterp Mltop Topfmt Vernacentries |