diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 533 |
1 files changed, 258 insertions, 275 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5d6d36d5..5c5b7206 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -11,6 +13,8 @@ open Names open CErrors open Util +open CAst + open Extend open Vernacexpr open Pputils @@ -19,18 +23,11 @@ open Constrexpr open Constrexpr_ops open Decl_kinds -module Make - (Ppconstr : Ppconstrsig.Pp) - (Pptactic : Pptacticsig.Pp) - (Taggers : sig - val tag_keyword : std_ppcmds -> std_ppcmds - val tag_vernac : vernac_expr -> std_ppcmds -> std_ppcmds - end) -= struct - - open Taggers open Ppconstr - open Pptactic + + let do_not_tag _ x = x + let tag_keyword = do_not_tag () + let tag_vernac = do_not_tag let keyword s = tag_keyword (str s) @@ -38,36 +35,50 @@ module Make let pr_lconstr = pr_lconstr_expr let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr - let pr_lident (loc,id) = - if Loc.is_ghost loc then - let (b,_) = Loc.unloc loc in - pr_located pr_id (Loc.make_loc (b,b + String.length(Id.to_string id)),id) - else - pr_id id - - let pr_plident (lid, l) = - pr_lident lid ++ - (match l with - | Some l -> prlist_with_sep spc pr_lident l - | None -> mt()) - + let pr_uconstraint (l, d, r) = + pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ + pr_glob_level r + + let pr_univ_name_list = function + | None -> mt () + | Some l -> + str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}" + + let pr_univdecl_instance l extensible = + prlist_with_sep spc pr_lident l ++ + (if extensible then str"+" else mt ()) + + let pr_univdecl_constraints l extensible = + if List.is_empty l && extensible then mt () + else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++ + (if extensible then str"+" else mt()) + + let pr_universe_decl l = + let open Misctypes in + match l with + | None -> mt () + | Some l -> + str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++ + pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}" + + let pr_ident_decl (lid, l) = + pr_lident lid ++ pr_universe_decl l + let string_of_fqid fqid = String.concat "." (List.map Id.to_string fqid) let pr_fqid fqid = str (string_of_fqid fqid) - let pr_lfqid (loc,fqid) = - if Loc.is_ghost loc then - let (b,_) = Loc.unloc loc in - pr_located pr_fqid (Loc.make_loc (b,b + String.length(string_of_fqid fqid)),fqid) - else - pr_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 = function - | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located pr_name lna + let pr_lname_decl (n, u) = + pr_lname n ++ pr_universe_decl u - let pr_smart_global = pr_or_by_notation pr_reference + let pr_smart_global = Pputils.pr_or_by_notation pr_reference let pr_ltac_ref = Libnames.pr_reference @@ -77,25 +88,44 @@ module Make let sep_end = function | VernacBullet _ - | VernacSubproof None + | VernacSubproof _ | VernacEndSubproof -> str"" | _ -> str"." - let pr_gen t = pr_raw_generic (Global.env ()) t + let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() - let pr_set_entry_type = function + 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 -> str"pattern" - | ETConstr _ -> str"constr" + | 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" - | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" + + 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 @@ -114,7 +144,7 @@ module Make | 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 -> int g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -127,7 +157,7 @@ module Make let pr_explanation (e,b,f) = let a = match e with - | ExplByPos (n,_) -> anomaly (Pp.str "No more supported") + | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.") | ExplByName id -> pr_id id in let a = if f then str"!" ++ a else a in if b then str "[" ++ a ++ str "]" else a @@ -198,31 +228,31 @@ module Make | 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() ++ pr_raw_tactic tac + 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,c) -> + | CWith_Definition (id,udecl,c) -> let p = pr_c c in - keyword "Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p + keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p | CWith_Module (id,qid) -> keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ - pr_located pr_qualid qid + pr_ast pr_qualid qid let rec pr_module_ast leading_space pr_c = function - | CMident qid -> + | { loc ; v = CMident qid } -> if leading_space then - spc () ++ pr_located pr_qualid qid + spc () ++ pr_located pr_qualid (loc, qid) else - pr_located pr_qualid qid - | CMwith (_,mty,decl) -> + 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 - | CMapply (_,me1,(CMident _ as me2)) -> + | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } -> pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2 - | CMapply (_,me1,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")") @@ -261,10 +291,10 @@ module Make prlist_strict (pr_module_vardecls pr_c) l let pr_type_option pr_c = function - | CHole (loc, k, Misctypes.IntroAnonymous, _) -> mt() + | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c - let pr_decl_notation prc ((loc,ntn),c,scopt) = + 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 @@ -284,7 +314,7 @@ module Make ) ++ hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (keyword "Sort" ++ spc() ++ pr_glob_sort s) + 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() @@ -292,7 +322,7 @@ module Make ) ++ hov 0 ((if dep then keyword "Elimination for" else keyword "Case for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (keyword "Sort" ++ spc() ++ pr_glob_sort s) + hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s) | EqualityScheme ind -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() @@ -303,31 +333,26 @@ module Make let begin_of_inductive = function | [] -> 0 - | (_,((loc,_),_))::_ -> fst (Loc.unloc loc) + | (_,({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 (l,a) = - let l = match l with Some x -> x | None -> Decl_kinds.Global in - match l, a with - | (Discharge,Logical) -> - keyword (if many then "Hypotheses" else "Hypothesis") - | (Discharge,Definitional) -> - keyword (if many then "Variables" else "Variable") - | (Global,Logical) -> + let pr_assumption_token many discharge kind = + match discharge, kind with + | (NoDischarge,Logical) -> keyword (if many then "Axioms" else "Axiom") - | (Global,Definitional) -> + | (NoDischarge,Definitional) -> keyword (if many then "Parameters" else "Parameter") - | (Local, Logical) -> - keyword (if many then "Local Axioms" else "Local Axiom") - | (Local,Definitional) -> - keyword (if many then "Local Parameters" else "Local Parameter") - | (Global,Conjectural) -> str"Conjecture" - | ((Discharge | Local),Conjectural) -> - anomaly (Pp.str "Don't know how to beautify a local conjecture") + | (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() ++ @@ -358,54 +383,41 @@ module Make let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) let pr_syntax_modifier = function - | SetItemLevel (l,NextLevel) -> - prlist_with_sep sep_v2 str l ++ - spc() ++ keyword "at next level" - | SetItemLevel (l,NumLevel n) -> + | 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() ++ keyword "at level" ++ spc() ++ int n - | SetLevel n -> keyword "at level" ++ spc() ++ int n + 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_entry_type typ + | 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_located qs s - | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s + | 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_univs pl = - match pl with - | None -> mt () - | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}" - - let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) = + 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_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot + 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,guard)) = - assert (not (Option.is_empty idpl)); - let id, pl = Option.get idpl in + let pr_statement head (idpl,(bl,c)) = hov 2 - (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++ + (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ - pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ str":" ++ pr_spc_lconstr c) - let pr_priority = function - | None -> mt () - | Some i -> spc () ++ str "|" ++ spc () ++ int i - (**************************************) (* Pretty printer for vernac commands *) (**************************************) @@ -448,7 +460,7 @@ module Make | PrintGrammar ent -> keyword "Print Grammar" ++ spc() ++ str ent | PrintLoadPath dir -> - keyword "Print LoadPath" ++ pr_opt pr_dirpath dir + keyword "Print LoadPath" ++ pr_opt DirPath.print dir | PrintModules -> keyword "Print Modules" | PrintMLLoadPath -> @@ -489,8 +501,8 @@ module Make else "Print Universes" in keyword cmd ++ pr_opt str fopt - | PrintName qid -> - keyword "Print" ++ spc() ++ pr_smart_global qid + | 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 -> @@ -503,9 +515,9 @@ module Make keyword "Print Scope" ++ spc() ++ str s | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s - | PrintAbout (qid,gopt) -> - pr_opt (fun g -> int g ++ str ":"++ spc()) gopt - ++ keyword "About" ++ spc() ++ pr_smart_global qid + | PrintAbout (qid,l,gopt) -> + pr_opt (fun g -> Proof_bullet.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 @@ -519,40 +531,50 @@ module Make in keyword cmd ++ spc() ++ pr_smart_global qid | PrintNamespace dp -> - keyword "Print Namespace" ++ pr_dirpath 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 = str (Proof_using.to_string e) + let pr_using e = + let rec aux = function + | SsEmpty -> "()" + | SsType -> "(Type)" + | SsSingl { v=id } -> "("^Id.to_string id^")" + | SsCompl e -> "-" ^ aux e^"" + | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" + | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" + | SsFwdClose e -> "("^aux e^")*" + in Pp.str (aux e) + + let pr_extend s cl = + let pr_arg a = + try pr_gen a + with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in + try + let rl = Egramml.get_extend_vernac_rule s in + let rec aux rl cl = + match rl, cl with + | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl + | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl + | [], [] -> [] + | _ -> assert false in + hov 1 (pr_sequence identity (aux rl cl)) + with Not_found -> + hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") - let rec pr_vernac_body v = - let return = Taggers.tag_vernac v in + let pr_vernac_expr v = + let return = tag_vernac v in match v with - | VernacPolymorphic (poly, v) -> - let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in - return (s ++ spc () ++ pr_vernac_body v) - | VernacProgram v -> - return (keyword "Program" ++ spc() ++ pr_vernac_body v) - | VernacLocal (local, v) -> - return (pr_locality local ++ spc() ++ pr_vernac_body v) - - (* Stm *) - | VernacStm JoinDocument -> - return (keyword "Stm JoinDocument") - | VernacStm PrintDag -> - return (keyword "Stm PrintDag") - | VernacStm Finish -> - return (keyword "Stm Finish") - | VernacStm Wait -> - return (keyword "Stm Wait") - | VernacStm (Observe id) -> - return (keyword "Stm Observe " ++ str(Stateid.to_string id)) - | VernacStm (Command v) -> - return (keyword "Stm Command " ++ pr_vernac_body v) - | VernacStm (PGLast v) -> - return (keyword "Stm PGLast " ++ pr_vernac_body v) + | VernacLoad (f,s) -> + return ( + keyword "Load" + ++ if f then + (spc() ++ keyword "Verbose" ++ spc()) + else + spc() ++ qs s + ) (* Proof management *) | VernacAbortAll -> @@ -563,8 +585,6 @@ module Make return (keyword "Unfocus") | VernacUnfocused -> return (keyword "Unfocused") - | VernacGoal c -> - return (keyword "Goal" ++ pr_lconstrarg c) | VernacAbort id -> return (keyword "Abort" ++ pr_opt pr_lident id) | VernacUndo i -> @@ -582,20 +602,16 @@ module Make | OpenSubgoals -> mt () | NthGoal n -> spc () ++ int n | GoalId id -> spc () ++ pr_id id - | GoalUid n -> spc () ++ str n in + in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n - | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n | ShowProof -> keyword "Show Proof" - | ShowNode -> keyword "Show Node" | ShowScript -> keyword "Show Script" | ShowExistentials -> keyword "Show Existentials" | ShowUniverses -> keyword "Show Universes" - | ShowTree -> keyword "Show Tree" | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") | ShowMatch id -> keyword "Show Match " ++ pr_reference id - | ShowThesis -> keyword "Show Thesis" in return (pr_showable s) | VernacCheckGuard -> @@ -619,28 +635,8 @@ module Make | VernacRestoreState s -> return (keyword "Restore State" ++ spc() ++ qs s) - (* Control *) - | VernacLoad (f,s) -> - return ( - keyword "Load" - ++ if f then - (spc() ++ keyword "Verbose" ++ spc()) - else - spc() ++ qs s - ) - | VernacTime (_,v) -> - return (keyword "Time" ++ spc() ++ pr_vernac_body v) - | VernacRedirect (s, (_,v)) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_body v) - | VernacTimeout(n,v) -> - return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v) - | VernacFail v -> - return (keyword "Fail" ++ spc() ++ pr_vernac_body v) - | VernacError _ -> - return (keyword "No-parsing-rule for VernacError") - (* Syntax *) - | VernacOpenCloseScope (_,(opening,sc)) -> + | VernacOpenCloseScope (opening,sc) -> return ( keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc @@ -669,7 +665,7 @@ module Make ++ spc() ++ pr_smart_global q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" ) - | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *) + | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " ++ qs s ++ str " :=" ++ pr_constrarg q) ++ @@ -678,7 +674,7 @@ module Make | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) ) - | VernacNotation (_,c,((_,s),l),opt) -> + | 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 ++ @@ -686,9 +682,9 @@ module Make | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) ) - | VernacSyntaxExtension (_,(s,l)) -> + | VernacSyntaxExtension (_, (s, l)) -> return ( - keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ + keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++ pr_syntax_modifiers l ) | VernacNotationAddFormat(s,k,v) -> @@ -697,16 +693,18 @@ module Make ) (* Gallina *) - | VernacDefinition (d,id,b) -> (* A verifier... *) - let pr_def_token (l,dk) = - let l = match l with Some x -> x | None -> Decl_kinds.Global in - keyword (Kindops.string_of_definition_kind (l,false,dk)) + | 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) r ++ + pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ keyword " in" ++ spc() in let pr_def_body = function @@ -717,18 +715,19 @@ module Make in (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) | ProveBody (bl,t) -> - (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in + 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 d ++ spc() - ++ pr_plident id ++ binds ++ typ + pr_def_token kind ++ spc() + ++ pr_lname_decl id ++ binds ++ typ ++ (match c with | None -> mt() | Some cc -> str" :=" ++ spc() ++ cc)) ) - | VernacStartTheoremProof (ki,l,_) -> + | VernacStartTheoremProof (ki,l) -> return ( hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ prlist (pr_statement (spc () ++ keyword "with")) (List.tl l)) @@ -741,25 +740,20 @@ module Make match o with | None -> (match opac with | Transparent -> keyword "Defined" - | Opaque None -> keyword "Qed" - | Opaque (Some l) -> - keyword "Qed" ++ spc() ++ str"export" ++ - prlist_with_sep (fun () -> str", ") pr_lident l) - | Some (id,th) -> (match th with - | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id - | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id) + | 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 (stre,t,l) -> + | 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_plident xl ++ spc() ++ + 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) stre ++ + return (hov 2 (pr_assumption_token (n > 1) discharge kind ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) - | VernacInductive (p,f,l) -> + | VernacInductive (cum, p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -775,10 +769,10 @@ module Make | RecordDecl (c,fs) -> pr_record_decl b c fs in - let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) = + let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) = hov 0 ( str key ++ spc() ++ - (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++ + (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 ++ @@ -786,20 +780,29 @@ module Make in let key = let (_,_,_,k,_),_ = List.hd l in - match k with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" + 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 + | GlobalCumulativity | LocalCumulativity -> "Cumulative" + | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative" + 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)) + (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) | VernacFixpoint (local, recs) -> let local = match local with - | Some Discharge -> "Let " - | Some Local -> "Local " - | None | Some Global -> "" + | DoDischarge -> "Let " + | NoDischarge -> "" in return ( hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ @@ -809,12 +812,11 @@ module Make | VernacCoFixpoint (local, corecs) -> let local = match local with - | Some Discharge -> keyword "Let" ++ spc () - | Some Local -> keyword "Local" ++ spc () - | None | Some Global -> str "" + | DoDischarge -> keyword "Let" ++ spc () + | NoDischarge -> str "" in - let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) = - pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ + 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 @@ -840,10 +842,6 @@ module Make prlist_with_sep (fun _ -> str",") pr_lident v) ) | VernacConstraint v -> - let pr_uconstraint (l, d, r) = - pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ - pr_glob_level r - in return ( hov 2 (keyword "Constraint" ++ spc () ++ prlist_with_sep (fun _ -> str",") pr_uconstraint v) @@ -876,14 +874,14 @@ module Make return ( keyword "Canonical Structure" ++ spc() ++ pr_smart_global q ) - | VernacCoercion (_,id,c1,c2) -> + | 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) -> + | VernacIdentityCoercion (id,c1,c2) -> return ( hov 1 ( keyword "Identity Coercion" ++ spc() ++ pr_lident id ++ @@ -895,16 +893,16 @@ module Make return ( hov 1 ( (if abst then keyword "Declare" ++ spc () else mt ()) ++ - keyword "Instance" ++ - (match instid with - | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc () - | (_, Anonymous), _ -> mt ()) ++ - pr_and_type_binders_arg sup ++ + 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,CRecord (_,l)) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | 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())) @@ -977,7 +975,7 @@ module Make keyword "LoadPath" ++ spc() ++ qs s ++ (match d with | None -> mt() - | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir)) + | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) ) | VernacRemoveLoadPath s -> return (keyword "Remove LoadPath" ++ qs s) @@ -1007,9 +1005,9 @@ module Make prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ pr_opt_hintbases dbnames) ) - | VernacHints (_, dbnames,h) -> + | VernacHints (dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),_,compat) -> + | VernacSyntacticDefinition (id,(ids,c),compat) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ @@ -1037,7 +1035,7 @@ module Make hov 2 ( keyword "Arguments" ++ spc() ++ pr_smart_global q ++ - let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in + 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 "]" @@ -1050,13 +1048,13 @@ module Make | n, { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> - spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ + 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 (pr_name name) ++ print_implicits rest + spc() ++ pr_br impl (Name.print name) ++ print_implicits rest in print_arguments nargs args ++ if not (List.is_empty more_implicits) then @@ -1103,7 +1101,7 @@ module Make ) | VernacSetOpacity _ -> return ( - CErrors.anomaly (keyword "VernacSetOpacity used to set something else") + CErrors.anomaly (keyword "VernacSetOpacity used to set something else.") ) | VernacSetStrategy l -> let pr_lev = function @@ -1120,18 +1118,15 @@ module Make hov 1 (keyword "Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) ) - | VernacUnsetOption (na) -> + | VernacUnsetOption (export, na) -> + let export = if export then keyword "Export" ++ spc () else mt () in return ( - hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None) + hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None) ) - | VernacSetOption (na,v) -> + | VernacSetOption (export, na,v) -> + let export = if export then keyword "Export" ++ spc () else mt () in return ( - hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v) - ) - | VernacSetAppendOption (na,v) -> - return ( - hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ - spc() ++ keyword "Append" ++ spc() ++ qs v) + hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v) ) | VernacAddOption (na,l) -> return ( @@ -1153,18 +1148,19 @@ module Make 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) r0 ++ + 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 -> int i ++ str ": " in + let pr_i = match io with None -> mt () + | Some i -> Proof_bullet.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) r + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r ) | VernacPrint p -> return (pr_printable p) @@ -1177,7 +1173,7 @@ module Make | LocateFile f -> keyword "File" ++ spc() ++ qs f | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid - | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid + | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid in return (keyword "Locate" ++ spc() ++ pr_locate loc) | VernacRegister (id, RegisterInline) -> @@ -1205,12 +1201,12 @@ module Make return (keyword "Proof " ++ spc () ++ keyword "using" ++ spc() ++ pr_using e) | VernacProof (Some te, None) -> - return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te) + 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() ++pr_raw_tactic te + keyword "with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te ) | VernacProofMode s -> return (keyword "Proof Mode" ++ str s) @@ -1223,47 +1219,34 @@ module Make | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (keyword "BeginSubproof" ++ spc () ++ int i) + return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") - and pr_extend s cl = - let pr_arg a = - try pr_gen a - with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in - try - let rl = Egramml.get_extend_vernac_rule s in - let rec aux rl cl = - match rl, cl with - | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl - | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl - | [], [] -> [] - | _ -> assert false in - hov 1 (pr_sequence (fun x -> x) (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 v = - try pr_vernac_body v ++ sep_end v - with e -> CErrors.print e - -end - -include Make (Ppconstr) (Pptactic) (struct - let do_not_tag _ x = x - let tag_keyword = do_not_tag () - let tag_vernac = do_not_tag -end) - -module Richpp = struct +let pr_vernac_flag = + function + | VernacPolymorphic true -> keyword "Polymorphic" + | VernacPolymorphic false -> keyword "Monomorphic" + | VernacProgram -> keyword "Program" + | VernacLocal local -> pr_locality local - include Make - (Ppconstr.Richpp) - (Pptactic.Richpp) - (struct - open Ppannotation - let tag_keyword s = Pp.tag (Pp.Tag.inj AKeyword tag) s - let tag_vernac v s = Pp.tag (Pp.Tag.inj (AVernac v) tag) s - end) - -end + 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 |