From 311e87f261b5e7f1dca61ac19d9b7b695b411ce0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 20 May 2018 22:23:02 +0200 Subject: [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. --- META.coq | 24 +- parsing/egramcoq.ml | 483 ------------------- parsing/egramcoq.mli | 19 - parsing/egramml.ml | 84 ---- parsing/egramml.mli | 33 -- parsing/parsing.mllib | 2 - printing/ppvernac.ml | 1219 ----------------------------------------------- printing/ppvernac.mli | 26 - printing/printing.mllib | 1 - vernac/egramcoq.ml | 483 +++++++++++++++++++ vernac/egramcoq.mli | 19 + vernac/egramml.ml | 84 ++++ vernac/egramml.mli | 33 ++ vernac/ppvernac.ml | 1219 +++++++++++++++++++++++++++++++++++++++++++++++ vernac/ppvernac.mli | 26 + vernac/vernac.mllib | 11 +- 16 files changed, 1883 insertions(+), 1883 deletions(-) delete mode 100644 parsing/egramcoq.ml delete mode 100644 parsing/egramcoq.mli delete mode 100644 parsing/egramml.ml delete mode 100644 parsing/egramml.mli delete mode 100644 printing/ppvernac.ml delete mode 100644 printing/ppvernac.mli create mode 100644 vernac/egramcoq.ml create mode 100644 vernac/egramcoq.mli create mode 100644 vernac/egramml.ml create mode 100644 vernac/egramml.mli create mode 100644 vernac/ppvernac.ml create mode 100644 vernac/ppvernac.mli diff --git a/META.coq b/META.coq index 8d4c3d5f00..cdc088e747 100644 --- a/META.coq +++ b/META.coq @@ -6,6 +6,18 @@ version = "8.8" directory = "" requires = "camlp5" +package "grammar" ( + + description = "Coq Camlp5 Grammar Extensions for Plugins" + version = "8.8" + + requires = "camlp5.gramlib" + directory = "grammar" + + archive(byte) = "grammar.cma" + archive(native) = "grammar.cmxa" +) + package "config" ( description = "Coq Configuration Variables" @@ -126,18 +138,6 @@ package "interp" ( ) -package "grammar" ( - - description = "Coq Camlp5 Grammar Extensions for Plugins" - version = "8.8" - - requires = "camlp5.gramlib" - directory = "grammar" - - archive(byte) = "grammar.cma" - archive(native) = "grammar.cmxa" -) - package "proofs" ( description = "Coq Proof Engine" diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml deleted file mode 100644 index 5f63d21c4d..0000000000 --- a/parsing/egramcoq.ml +++ /dev/null @@ -1,483 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 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/parsing/egramcoq.mli b/parsing/egramcoq.mli deleted file mode 100644 index e15add10f6..0000000000 --- a/parsing/egramcoq.mli +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* unit -(** Add a term notation rule to the parsing system. *) diff --git a/parsing/egramml.ml b/parsing/egramml.ml deleted file mode 100644 index 90cd7d10b7..0000000000 --- a/parsing/egramml.ml +++ /dev/null @@ -1,84 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* '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/parsing/egramml.mli b/parsing/egramml.mli deleted file mode 100644 index 31aa1a9891..0000000000 --- a/parsing/egramml.mli +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* '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/parsing/parsing.mllib b/parsing/parsing.mllib index 103e1188a9..e5a0a31cc3 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -3,8 +3,6 @@ CLexer Extend Vernacexpr Pcoq -Egramml -Egramcoq G_constr G_vernac G_prim diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml deleted file mode 100644 index 7a34e80274..0000000000 --- a/printing/ppvernac.ml +++ /dev/null @@ -1,1219 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 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 "" 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/printing/ppvernac.mli b/printing/ppvernac.mli deleted file mode 100644 index 4aa24bf5db..0000000000 --- a/printing/ppvernac.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 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/printing/printing.mllib b/printing/printing.mllib index 86b68d8fb0..b69d8a9ef8 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -4,4 +4,3 @@ Ppconstr Printer Printmod Prettyp -Ppvernac diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml new file mode 100644 index 0000000000..5f63d21c4d --- /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 *) +(* 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 0000000000..e15add10f6 --- /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 *) +(* 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 0000000000..90cd7d10b7 --- /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 *) +(* '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 0000000000..31aa1a9891 --- /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 *) +(* '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 0000000000..7a34e80274 --- /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 *) +(* 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 "" 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 0000000000..4aa24bf5db --- /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 *) +(* 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 f001b572a5..6fceda56da 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 -- cgit v1.2.3