diff options
author | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-10-30 23:13:18 +0100 |
---|---|---|
committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:35 +0100 |
commit | 903f0d09c3be90a09303b549a711caef747fc11a (patch) | |
tree | 15b70fe7616d3857f61e9624d57ae503adefea82 | |
parent | 846dad24f483bd5d5221a2b6fe663bbd5ba86455 (diff) |
Ppannotation.t: New constructor AVernac.
Ppvernac.RichPp: New rich pretty-printer.
-rw-r--r-- | printing/ppannotation.ml | 4 | ||||
-rw-r--r-- | printing/ppannotation.mli | 4 | ||||
-rw-r--r-- | printing/ppvernac.ml | 1202 |
3 files changed, 716 insertions, 494 deletions
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml index 549a0dab8..3274a7bdc 100644 --- a/printing/ppannotation.ml +++ b/printing/ppannotation.ml @@ -6,9 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Constrexpr open Ppextend +open Constrexpr +open Vernacexpr type t = | AUnparsing of unparsing | AConstrExpr of constr_expr + | AVernac of vernac_expr diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli index 54f70aeda..a462c9f33 100644 --- a/printing/ppannotation.mli +++ b/printing/ppannotation.mli @@ -9,9 +9,11 @@ (** This module defines the annotations that are attached to semi-structured pretty-printing of Coq syntactic objects. *) -open Constrexpr open Ppextend +open Constrexpr +open Vernacexpr type t = | AUnparsing of unparsing | AConstrExpr of constr_expr + | AVernac of vernac_expr diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 67e11bb09..ecbc4a20e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -20,7 +20,12 @@ open Constrexpr open Constrexpr_ops open Decl_kinds -module Make (Ppconstr : Ppconstrsig.Pp) = struct +module Make + (Ppconstr : Ppconstrsig.Pp) + (Tagger : sig + val tag_vernac : vernac_expr -> std_ppcmds -> std_ppcmds + end) += struct open Ppconstr @@ -449,8 +454,8 @@ module Make (Ppconstr : Ppconstrsig.Pp) = struct | PrintVisibility s -> str "Print Visibility" ++ pr_opt str s | PrintAbout qid -> str "About" ++ spc() ++ pr_smart_global qid | PrintImplicit qid -> str "Print Implicit" ++ spc() ++ pr_smart_global qid -(* spiwack: command printing all the axioms and section variables used in a - term *) + (* 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" @@ -466,315 +471,431 @@ module Make (Ppconstr : Ppconstrsig.Pp) = struct let pr_using e = str (Proof_using.to_string e) in - let rec pr_vernac = function - | VernacPolymorphic (poly, v) -> - let s = if poly then str"Polymorphic" else str"Monomorphic" in - s ++ pr_vernac v - | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v - | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v - - (* Stm *) - | VernacStm JoinDocument -> str"Stm JoinDocument" - | VernacStm PrintDag -> str"Stm PrintDag" - | VernacStm Finish -> str"Stm Finish" - | VernacStm Wait -> str"Stm Wait" - | VernacStm (Observe id) -> - str"Stm Observe " ++ str(Stateid.to_string id) - | VernacStm (Command v) -> str"Stm Command " ++ pr_vernac v - | VernacStm (PGLast v) -> str"Stm PGLast " ++ pr_vernac v - - (* Proof management *) - | VernacAbortAll -> str "Abort All" - | VernacRestart -> str"Restart" - | VernacUnfocus -> str"Unfocus" - | VernacUnfocused -> str"Unfocused" - | VernacGoal c -> str"Goal" ++ pr_lconstrarg c - | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id - | VernacUndo i -> if Int.equal i 1 then str"Undo" else str"Undo" ++ pr_intarg i - | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i - | VernacBacktrack (i,j,k) -> - str "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k] - | VernacFocus i -> str"Focus" ++ pr_opt int i - | VernacShow s -> - let pr_goal_reference = function - | OpenSubgoals -> mt () - | NthGoal n -> spc () ++ int n - | GoalId n -> spc () ++ str n in - let pr_showable = function - | ShowGoal n -> str"Show" ++ pr_goal_reference n - | ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n - | ShowProof -> str"Show Proof" - | ShowNode -> str"Show Node" - | ShowScript -> str"Show Script" - | ShowExistentials -> str"Show Existentials" - | ShowUniverses -> str"Show Universes" - | ShowTree -> str"Show Tree" - | ShowProofNames -> str"Show Conjectures" - | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro") - | ShowMatch id -> str"Show Match " ++ pr_lident id - | ShowThesis -> str "Show Thesis" - in pr_showable s - | VernacCheckGuard -> str"Guarded" - - (* Resetting *) - | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id - | VernacResetInitial -> str"Reset Initial" - | VernacBack i -> if Int.equal i 1 then str"Back" else str"Back" ++ pr_intarg i - | VernacBackTo i -> str"BackTo" ++ pr_intarg i - - (* State management *) - | VernacWriteState s -> str"Write State" ++ spc () ++ qs s - | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s - - (* Control *) - | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" - ++ spc()) else spc() ++ qs s - | VernacTime v -> str"Time" ++ spc() ++ pr_vernac_list v - | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v - | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v - | VernacError _ -> str"No-parsing-rule for VernacError" - - (* Syntax *) - | VernacTacticNotation (n,r,e) -> - pr_grammar_tactic_rule n ("",r,e) - | VernacOpenCloseScope (_,(opening,sc)) -> - str (if opening then "Open " else "Close ") ++ - str "Scope" ++ spc() ++ str sc - | VernacDelimiters (sc,key) -> - str"Delimit Scope" ++ spc () ++ str sc ++ - spc() ++ str "with " ++ str key - | VernacBindScope (sc,cll) -> - str"Bind Scope" ++ spc () ++ str sc ++ - spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll - | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function - | None -> str"_" - | Some sc -> str sc in - str"Arguments Scope" ++ spc() ++ - pr_smart_global q - ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *) - hov 0 (hov 0 (str"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,((_,s),l),opt) -> - let ps = - let n = String.length s in - if n > 2 && s.[0] == '\'' && s.[n-1] == '\'' - then - let s' = String.sub s 1 (n-2) in - if String.contains s' '\'' then qs s else str s' - else qs s in - hov 2 (str"Notation" ++ spc() ++ ps ++ - str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++ - (match opt with - | None -> mt() - | Some sc -> str" :" ++ spc() ++ str sc)) - | VernacSyntaxExtension (_,(s,l)) -> - str"Reserved Notation" ++ spc() ++ pr_located qs s ++ - pr_syntax_modifiers l - | VernacNotationAddFormat(s,k,v) -> - str"Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v - - (* 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 - str (Kindops.string_of_definition_kind (l,false,dk)) in - let pr_reduce = function - | None -> mt() - | Some r -> - str"Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++ - str" 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) -> - (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in - let (binds,typ,c) = pr_def_body b in - hov 2 (pr_def_token d ++ spc() ++ pr_lident id ++ binds ++ typ ++ - (match c with - | None -> mt() - | Some cc -> str" :=" ++ spc() ++ cc)) - - | VernacStartTheoremProof (ki,l,_) -> - hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ - prlist (pr_statement (spc () ++ str "with")) (List.tl l)) - - | VernacEndProof Admitted -> str"Admitted" - | VernacEndProof (Proved (opac,o)) -> (match o with - | None -> if opac then str"Qed" else str"Defined" - | Some (id,th) -> (match th with - | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_lident id - | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)) - | VernacExactProof c -> - hov 2 (str"Proof" ++ pr_lconstrarg c) - | VernacAssumption (stre,_,l) -> - let n = List.length (List.flatten (List.map fst (List.map snd l))) in - hov 2 - (pr_assumption_token (n > 1) stre ++ spc() ++ - pr_ne_params_list pr_lconstr_expr l) - | VernacInductive (p,f,l) -> - let pr_constructor (coe,(id,c)) = - hov 2 (pr_lident id ++ str" " ++ - (if coe then str":>" else str":") ++ - 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,id),indpar,s,k,lc),ntn) = - hov 0 ( - str key ++ spc() ++ - (if coe then str"> " else str"") ++ pr_lident id ++ - pr_and_type_binders_arg indpar ++ spc() ++ - Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ - str" :=") ++ pr_constructor_list k lc ++ - prlist (pr_decl_notation pr_constr) ntn - 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" in - 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 - | Some Discharge -> "Let " - | Some Local -> "Local " - | None | Some Global -> "" - in - let pr_onerec = function - | ((loc,id),ro,bl,type_,def),ntn -> - let annot = pr_guard_annot pr_lconstr_expr bl ro in - pr_id id ++ 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_lconstr def) def ++ + let rec pr_vernac v = + let return = Tagger.tag_vernac v in + match v with + | VernacPolymorphic (poly, v) -> + let s = if poly then str"Polymorphic" else str"Monomorphic" in + return (s ++ pr_vernac v) + | VernacProgram v -> + return (str"Program" ++ spc() ++ pr_vernac v) + | VernacLocal (local, v) -> + return (pr_locality local ++ spc() ++ pr_vernac v) + + (* Stm *) + | VernacStm JoinDocument -> + return (str"Stm JoinDocument") + | VernacStm PrintDag -> + return (str"Stm PrintDag") + | VernacStm Finish -> + return (str"Stm Finish") + | VernacStm Wait -> + return (str"Stm Wait") + | VernacStm (Observe id) -> + return (str"Stm Observe " ++ str(Stateid.to_string id)) + | VernacStm (Command v) -> + return (str"Stm Command " ++ pr_vernac v) + | VernacStm (PGLast v) -> + return (str"Stm PGLast " ++ pr_vernac v) + + (* Proof management *) + | VernacAbortAll -> + return (str "Abort All") + | VernacRestart -> + return (str"Restart") + | VernacUnfocus -> + return (str"Unfocus") + | VernacUnfocused -> + return (str"Unfocused") + | VernacGoal c -> + return (str"Goal" ++ pr_lconstrarg c) + | VernacAbort id -> + return (str"Abort" ++ pr_opt pr_lident id) + | VernacUndo i -> + return ( + if Int.equal i 1 then str"Undo" else str"Undo" ++ pr_intarg i + ) + | VernacUndoTo i -> + return (str"Undo" ++ spc() ++ str"To" ++ pr_intarg i) + | VernacBacktrack (i,j,k) -> + return (str "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k]) + | VernacFocus i -> + return (str"Focus" ++ pr_opt int i) + | VernacShow s -> + let pr_goal_reference = function + | OpenSubgoals -> mt () + | NthGoal n -> spc () ++ int n + | GoalId n -> spc () ++ str n in + let pr_showable = function + | ShowGoal n -> str"Show" ++ pr_goal_reference n + | ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n + | ShowProof -> str"Show Proof" + | ShowNode -> str"Show Node" + | ShowScript -> str"Show Script" + | ShowExistentials -> str"Show Existentials" + | ShowUniverses -> str"Show Universes" + | ShowTree -> str"Show Tree" + | ShowProofNames -> str"Show Conjectures" + | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro") + | ShowMatch id -> str"Show Match " ++ pr_lident id + | ShowThesis -> str "Show Thesis" + in + return (pr_showable s) + | VernacCheckGuard -> + return (str"Guarded") + + (* Resetting *) + | VernacResetName id -> + return (str"Reset" ++ spc() ++ pr_lident id) + | VernacResetInitial -> + return (str"Reset Initial") + | VernacBack i -> + return ( + if Int.equal i 1 then str"Back" else str"Back" ++ pr_intarg i + ) + | VernacBackTo i -> + return (str"BackTo" ++ pr_intarg i) + + (* State management *) + | VernacWriteState s -> + return (str"Write State" ++ spc () ++ qs s) + | VernacRestoreState s -> + return (str"Restore State" ++ spc() ++ qs s) + + (* Control *) + | VernacLoad (f,s) -> + return ( + str"Load" + ++ if f then + (spc() ++ str"Verbose" ++ spc()) + else + spc() ++ qs s + ) + | VernacTime v -> + return (str"Time" ++ spc() ++ pr_vernac_list v) + | VernacTimeout(n,v) -> + return (str"Timeout " ++ int n ++ spc() ++ pr_vernac v) + | VernacFail v -> + return (str"Fail" ++ spc() ++ pr_vernac v) + | VernacError _ -> + return (str"No-parsing-rule for VernacError") + + (* Syntax *) + | VernacTacticNotation (n,r,e) -> + return (pr_grammar_tactic_rule n ("",r,e)) + | VernacOpenCloseScope (_,(opening,sc)) -> + return ( + str (if opening then "Open " else "Close ") ++ + str "Scope" ++ spc() ++ str sc + ) + | VernacDelimiters (sc,key) -> + return ( + str"Delimit Scope" ++ spc () ++ str sc ++ + spc() ++ str "with " ++ str key + ) + | VernacBindScope (sc,cll) -> + return ( + str"Bind Scope" ++ spc () ++ str sc ++ + spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll + ) + | VernacArgumentsScope (q,scl) -> + let pr_opt_scope = function + | None -> str"_" + | Some sc -> str sc + in + return ( + str"Arguments Scope" + ++ spc() ++ pr_smart_global q + ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" + ) + | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *) + return ( + hov 0 (hov 0 (str"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,((_,s),l),opt) -> + let ps = + let n = String.length s in + if n > 2 && s.[0] == '\'' && s.[n-1] == '\'' + then + let s' = String.sub s 1 (n-2) in + if String.contains s' '\'' then qs s else str s' + else qs s + in + return ( + hov 2 (str"Notation" ++ spc() ++ ps ++ + str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++ + (match opt with + | None -> mt() + | Some sc -> str" :" ++ spc() ++ str sc)) + ) + | VernacSyntaxExtension (_,(s,l)) -> + return ( + str"Reserved Notation" ++ spc() ++ pr_located qs s ++ + pr_syntax_modifiers l + ) + | VernacNotationAddFormat(s,k,v) -> + return ( + str"Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v + ) + + (* 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 + str (Kindops.string_of_definition_kind (l,false,dk)) + in + let pr_reduce = function + | None -> mt() + | Some r -> + str"Eval" ++ spc() ++ + pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++ + str" 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) -> + (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in + let (binds,typ,c) = pr_def_body b in + return ( + hov 2 (pr_def_token d ++ spc() ++ pr_lident 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 () ++ str "with")) (List.tl l)) + ) + + | VernacEndProof Admitted -> + return (str"Admitted") + + | VernacEndProof (Proved (opac,o)) -> return ( + match o with + | None -> if opac then str"Qed" else str"Defined" + | Some (id,th) -> (match th with + | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_lident id + | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id) + ) + | VernacExactProof c -> + return (hov 2 (str"Proof" ++ pr_lconstrarg c)) + | VernacAssumption (stre,_,l) -> + let n = List.length (List.flatten (List.map fst (List.map snd l))) in + return ( + hov 2 + (pr_assumption_token (n > 1) stre ++ spc() ++ + pr_ne_params_list pr_lconstr_expr l) + ) + | VernacInductive (p,f,l) -> + let pr_constructor (coe,(id,c)) = + hov 2 (pr_lident id ++ str" " ++ + (if coe then str":>" else str":") ++ + 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,id),indpar,s,k,lc),ntn) = + hov 0 ( + str key ++ spc() ++ + (if coe then str"> " else str"") ++ pr_lident id ++ + pr_and_type_binders_arg indpar ++ spc() ++ + Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ + str" :=") ++ pr_constructor_list k lc ++ prlist (pr_decl_notation pr_constr) ntn - in - hov 0 (str local ++ str "Fixpoint" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs) - - | VernacCoFixpoint (local, corecs) -> - let local = match local with - | Some Discharge -> "Let " - | Some Local -> "Local " - | None | Some Global -> "" - in - let pr_onecorec (((loc,id),bl,c,def),ntn) = - pr_id id ++ 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 - hov 0 (str local ++ str "CoFixpoint" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs) - | VernacScheme l -> - hov 2 (str"Scheme" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l) - | VernacCombinedScheme (id, l) -> - hov 2 (str"Combined Scheme" ++ spc() ++ - pr_lident id ++ spc() ++ str"from" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) - | VernacUniverse v -> - hov 2 (str"Universe" ++ spc () ++ - prlist_with_sep (fun _ -> str",") pr_lident v) - | VernacConstraint v -> - let pr_uconstraint (l, d, r) = - pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r - in - hov 2 (str"Constraint" ++ spc () ++ - prlist_with_sep (fun _ -> str",") pr_uconstraint v) - - (* Gallina extensions *) - | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id) - | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id) - | VernacRequire (exp, l) -> hov 2 - (str "Require" ++ spc() ++ pr_require_token exp ++ - prlist_with_sep sep pr_module l) - | VernacImport (f,l) -> - (if f then str"Export" else str"Import") ++ spc() ++ - prlist_with_sep sep pr_import_module l - | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q - | VernacCoercion (_,id,c1,c2) -> - hov 1 ( - str"Coercion" ++ spc() ++ - pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ - spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) - | VernacIdentityCoercion (_,id,c1,c2) -> - hov 1 ( - str"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, pri) -> - hov 1 ( - (if abst then str"Declare " else mt ()) ++ - str"Instance" ++ - (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | - Anonymous -> mt ()) ++ - pr_and_type_binders_arg sup ++ - str":" ++ spc () ++ - pr_constr cl ++ pr_priority pri ++ - (match props with - | Some (_,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p - | None -> mt())) - - | VernacContext l -> - hov 1 ( - str"Context" ++ spc () ++ pr_and_type_binders_arg l) - - - | VernacDeclareInstances (ids, pri) -> - hov 1 ( str"Existing" ++ spc () ++ - str(String.plural (List.length ids) "Instance") ++ - spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri) - - | VernacDeclareClass id -> - hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id) - - (* Modules and Module Types *) - | VernacDefineModule (export,m,bl,tys,bd) -> - let b = pr_module_binders bl pr_lconstr in - hov 2 (str"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 - hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++ - pr_lident id ++ b ++ - 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 - hov 2 (str"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 - hov 2 (str"Include" ++ spc() ++ - prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) - - (* Solving *) + 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" + 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 + | Some Discharge -> "Let " + | Some Local -> "Local " + | None | Some Global -> "" + in + let pr_onerec = function + | ((loc,id),ro,bl,type_,def),ntn -> + let annot = pr_guard_annot pr_lconstr_expr bl ro in + pr_id id ++ 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_lconstr def) def ++ + prlist (pr_decl_notation pr_constr) ntn + in + return ( + hov 0 (str local ++ str "Fixpoint" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs) + ) + + | VernacCoFixpoint (local, corecs) -> + let local = match local with + | Some Discharge -> "Let " + | Some Local -> "Local " + | None | Some Global -> "" + in + let pr_onecorec (((loc,id),bl,c,def),ntn) = + pr_id id ++ 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 (str local ++ str "CoFixpoint" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs) + ) + | VernacScheme l -> + return ( + hov 2 (str"Scheme" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l) + ) + | VernacCombinedScheme (id, l) -> + return ( + hov 2 (str"Combined Scheme" ++ spc() ++ + pr_lident id ++ spc() ++ str"from" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) + ) + | VernacUniverse v -> + return ( + hov 2 (str"Universe" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_lident v) + ) + | VernacConstraint v -> + let pr_uconstraint (l, d, r) = + pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r + in + return ( + hov 2 (str"Constraint" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_uconstraint v) + ) + + (* Gallina extensions *) + | VernacBeginSection id -> + return (hov 2 (str"Section" ++ spc () ++ pr_lident id)) + | VernacEndSegment id -> + return (hov 2 (str"End" ++ spc() ++ pr_lident id)) + | VernacRequire (exp, l) -> + return ( + hov 2 + (str "Require" ++ spc() ++ pr_require_token exp ++ + prlist_with_sep sep pr_module l) + ) + | VernacImport (f,l) -> + return ( + (if f then str"Export" else str"Import") ++ spc() ++ + prlist_with_sep sep pr_import_module l + ) + | VernacCanonical q -> + return ( + str"Canonical Structure" ++ spc() ++ pr_smart_global q + ) + | VernacCoercion (_,id,c1,c2) -> + return ( + hov 1 ( + str"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 ( + str"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, pri) -> + return ( + hov 1 ( + (if abst then str"Declare " else mt ()) ++ + str"Instance" ++ + (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | + Anonymous -> mt ()) ++ + pr_and_type_binders_arg sup ++ + str":" ++ spc () ++ + pr_constr cl ++ pr_priority pri ++ + (match props with + | Some (_,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p + | None -> mt())) + ) + + | VernacContext l -> + return ( + hov 1 ( + str"Context" ++ spc () ++ pr_and_type_binders_arg l) + ) + + | VernacDeclareInstances (ids, pri) -> + return ( + hov 1 (str"Existing" ++ spc () ++ + str(String.plural (List.length ids) "Instance") ++ + spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri) + ) + + | VernacDeclareClass id -> + return ( + hov 1 (str"Existing" ++ spc () ++ str"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 (str"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 (str"Declare Module" ++ spc() ++ pr_require_token export ++ + pr_lident id ++ b ++ + 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 (str"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 (str"Include" ++ spc() ++ + prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) + ) + (* Solving *) | VernacSolve (i,info,tac,deftac) -> let pr_goal_selector = function | SelectNth i -> int i ++ str":" @@ -787,188 +908,268 @@ module Make (Ppconstr : Ppconstrsig.Pp) = struct | None -> mt () | Some i -> str"Info"++spc()++int i++spc() in - (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++ + return ( + (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++ pr_info ++ pr_raw_tactic tac - ++ (if deftac then str ".." else mt ()) - | VernacSolveExistential (i,c) -> - str"Existential " ++ int i ++ pr_lconstrarg c - - (* Auxiliary file and library management *) - | VernacAddLoadPath (fl,s,d) -> hov 2 - (str"Add" ++ - (if fl then str" Rec " else spc()) ++ - str"LoadPath" ++ spc() ++ qs s ++ - (match d with - | None -> mt() - | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) - | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s - | VernacAddMLPath (fl,s) -> - str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s - | VernacDeclareMLModule (l) -> - hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l) - | VernacChdir s -> str"Cd" ++ pr_opt qs s - - (* Commands *) - | VernacDeclareTacticDefinition (rc,l) -> - let pr_tac_body (id, redef, body) = - let idl, body = - match body with - | Tacexpr.TacFun (idl,b) -> idl,b - | _ -> [], body in - pr_ltac_ref id ++ - prlist (function None -> str " _" - | Some id -> spc () ++ pr_id id) idl - ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ - pr_raw_tactic body - in - hov 1 - (str "Ltac " ++ - prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) - | VernacCreateHintDb (dbname,b) -> - hov 1 (str "Create HintDb " ++ - str dbname ++ (if b then str" discriminated" else mt ())) - | VernacRemoveHints (dbnames, ids) -> - hov 1 (str "Remove Hints " ++ - prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ - pr_opt_hintbases dbnames) - | VernacHints (_, dbnames,h) -> - pr_hints dbnames h pr_constr pr_constr_pattern_expr - | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> - hov 2 - (str"Notation " ++ pr_lident id ++ spc () ++ - prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++ - pr_syntax_modifiers - (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) - | VernacDeclareImplicits (q,[]) -> - hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q) - | VernacDeclareImplicits (q,impls) -> - hov 1 (str"Implicit Arguments " ++ - spc() ++ pr_smart_global q ++ spc() ++ - prlist_with_sep spc (fun imps -> - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") - impls) - | VernacArguments (q, impl, nargs, mods) -> - hov 2 (str"Arguments" ++ spc() ++ - pr_smart_global q ++ - let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in - let pr_if b x = if b then x else str "" in - let pr_br imp max x = match imp, max with - | true, false -> str "[" ++ x ++ str "]" - | true, true -> str "{" ++ x ++ str "}" - | _ -> x in - let rec aux n l = - match n, l with - | 0, l -> spc () ++ str"/" ++ aux ~-1 l - | _, [] -> mt() - | n, (id,k,s,imp,max) :: tl -> - spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ - aux (n-1) tl in - prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ - if not (List.is_empty mods) then str" : " else str"" ++ - prlist_with_sep (fun () -> str", " ++ spc()) (function - | `ReductionDontExposeCase -> str "simpl nomatch" - | `ReductionNeverUnfold -> str "simpl never" - | `DefaultImplicits -> str "default implicits" - | `Rename -> str "rename" - | `Assert -> str "assert" - | `ExtraScopes -> str "extra scopes" - | `ClearImplicits -> str "clear implicits" - | `ClearScopes -> str "clear scopes") - mods) - | VernacReserve bl -> - let n = List.length (List.flatten (List.map fst bl)) in - hov 2 (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 -> - hov 1 (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 -> - hov 1 (str "Transparent" ++ - spc() ++ prlist_with_sep sep pr_smart_global l) - | VernacSetOpacity(Conv_oracle.Opaque,l) -> - hov 1 (str "Opaque" ++ - spc() ++ prlist_with_sep sep pr_smart_global l) - | VernacSetOpacity _ -> - Errors.anomaly (str "VernacSetOpacity used to set something else") - | VernacSetStrategy l -> - let pr_lev = function - Conv_oracle.Opaque -> str"opaque" - | Conv_oracle.Expand -> str"expand" - | l when Conv_oracle.is_transparent l -> str"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 - hov 1 (str "Strategy" ++ spc() ++ - hv 0 (prlist_with_sep sep pr_line l)) - | VernacUnsetOption (na) -> - hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) - | VernacSetOption (na,v) -> - hov 2 (str"Set" ++ spc() ++ pr_set_option na v) - | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l)) - | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l)) - | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l)) - | VernacPrintOption na -> hov 2 (str"Test" ++ spc() ++ pr_printoption na None) - | VernacCheckMayEval (r,io,c) -> - let pr_mayeval r c = match r with - | Some r0 -> - hov 2 (str"Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++ - spc() ++ str"in" ++ spc () ++ pr_lconstr c) - | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c) - in - let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in - pr_i ++ pr_mayeval r c - | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c) - | VernacDeclareReduction (s,r) -> - str "Declare Reduction " ++ str s ++ str " := " ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r - | VernacPrint p -> pr_printable p - | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr - | VernacLocate loc -> - let pr_locate =function - | LocateAny qid -> pr_smart_global qid - | LocateTerm qid -> str "Term" ++ spc() ++ pr_smart_global qid - | LocateFile f -> str"File" ++ spc() ++ qs f - | LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid - | LocateModule qid -> str"Module" ++ spc () ++ pr_module qid - | LocateTactic qid -> str"Ltac" ++ spc () ++ pr_ltac_ref qid - in str"Locate" ++ spc() ++ pr_locate loc - | VernacRegister (id, RegisterInline) -> - hov 2 - (str "Register Inline" ++ spc() ++ pr_lident id) - | VernacComments l -> - hov 2 - (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) - | VernacNop -> mt() - - (* Toplevel control *) - | VernacToplevelControl exn -> pr_topcmd exn - - (* For extension *) - | VernacExtend (s,c) -> pr_extend s c - | VernacProof (None, None) -> str "Proof" - | VernacProof (None, Some e) -> str "Proof " ++ pr_using e - | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te - | VernacProof (Some te, Some e) -> - str "Proof " ++ pr_using e ++ spc() ++ - str "with" ++ spc() ++pr_raw_tactic te - | VernacProofMode s -> str ("Proof Mode "^s) - | VernacBullet b -> begin match b with - | Dash n -> str (String.make n '-') - | Star n -> str (String.make n '*') - | Plus n -> str (String.make n '+') - end ++ spc() - | VernacSubproof None -> str "{" - | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i - | VernacEndSubproof -> str "}" + ++ (if deftac then str ".." else mt ()) + ) + | VernacSolveExistential (i,c) -> + return (str"Existential " ++ int i ++ pr_lconstrarg c) + + (* Auxiliary file and library management *) + | VernacAddLoadPath (fl,s,d) -> + return ( + hov 2 + (str"Add" ++ + (if fl then str" Rec " else spc()) ++ + str"LoadPath" ++ spc() ++ qs s ++ + (match d with + | None -> mt() + | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) + ) + | VernacRemoveLoadPath s -> + return (str"Remove LoadPath" ++ qs s) + | VernacAddMLPath (fl,s) -> + return ( + str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s + ) + | VernacDeclareMLModule (l) -> + return ( + hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l) + ) + | VernacChdir s -> + return (str"Cd" ++ pr_opt qs s) + + (* Commands *) + | VernacDeclareTacticDefinition (rc,l) -> + let pr_tac_body (id, redef, body) = + let idl, body = + match body with + | Tacexpr.TacFun (idl,b) -> idl,b + | _ -> [], body in + pr_ltac_ref id ++ + prlist (function None -> str " _" + | Some id -> spc () ++ pr_id id) idl + ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ + pr_raw_tactic body + in + return ( + hov 1 + (str "Ltac " ++ + prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) + ) + | VernacCreateHintDb (dbname,b) -> + return ( + hov 1 (str "Create HintDb " ++ + str dbname ++ (if b then str" discriminated" else mt ())) + ) + | VernacRemoveHints (dbnames, ids) -> + return ( + hov 1 (str "Remove Hints " ++ + 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),_,onlyparsing) -> + return ( + hov 2 + (str"Notation " ++ pr_lident id ++ spc () ++ + prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++ + pr_syntax_modifiers + (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) + ) + | VernacDeclareImplicits (q,[]) -> + return ( + hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q) + ) + | VernacDeclareImplicits (q,impls) -> + return ( + hov 1 (str"Implicit Arguments " ++ + spc() ++ pr_smart_global q ++ spc() ++ + prlist_with_sep spc (fun imps -> + str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") + impls) + ) + | VernacArguments (q, impl, nargs, mods) -> + return ( + hov 2 ( + str"Arguments" ++ spc() ++ + pr_smart_global q ++ + let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in + let pr_if b x = if b then x else str "" in + let pr_br imp max x = match imp, max with + | true, false -> str "[" ++ x ++ str "]" + | true, true -> str "{" ++ x ++ str "}" + | _ -> x in + let rec aux n l = + match n, l with + | 0, l -> spc () ++ str"/" ++ aux ~-1 l + | _, [] -> mt() + | n, (id,k,s,imp,max) :: tl -> + spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ + aux (n-1) tl in + prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ + if not (List.is_empty mods) then str" : " else str"" ++ + prlist_with_sep (fun () -> str", " ++ spc()) (function + | `ReductionDontExposeCase -> str "simpl nomatch" + | `ReductionNeverUnfold -> str "simpl never" + | `DefaultImplicits -> str "default implicits" + | `Rename -> str "rename" + | `Assert -> str "assert" + | `ExtraScopes -> str "extra scopes" + | `ClearImplicits -> str "clear implicits" + | `ClearScopes -> str "clear scopes") + mods) + ) + | VernacReserve bl -> + let n = List.length (List.flatten (List.map fst bl)) in + return ( + hov 2 (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 (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 (str "Transparent" ++ + spc() ++ prlist_with_sep sep pr_smart_global l) + ) + | VernacSetOpacity(Conv_oracle.Opaque,l) -> + return ( + hov 1 (str "Opaque" ++ + spc() ++ prlist_with_sep sep pr_smart_global l) + ) + | VernacSetOpacity _ -> + return ( + Errors.anomaly (str "VernacSetOpacity used to set something else") + ) + | VernacSetStrategy l -> + let pr_lev = function + | Conv_oracle.Opaque -> str"opaque" + | Conv_oracle.Expand -> str"expand" + | l when Conv_oracle.is_transparent l -> str"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 (str "Strategy" ++ spc() ++ + hv 0 (prlist_with_sep sep pr_line l)) + ) + | VernacUnsetOption (na) -> + return ( + hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) + ) + | VernacSetOption (na,v) -> + return ( + hov 2 (str"Set" ++ spc() ++ pr_set_option na v) + ) + | VernacAddOption (na,l) -> + return ( + hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacRemoveOption (na,l) -> + return ( + hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacMemOption (na,l) -> + return ( + hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacPrintOption na -> + return ( + hov 2 (str"Test" ++ spc() ++ pr_printoption na None) + ) + | VernacCheckMayEval (r,io,c) -> + let pr_mayeval r c = match r with + | Some r0 -> + hov 2 (str"Eval" ++ spc() ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++ + spc() ++ str"in" ++ spc () ++ pr_lconstr c) + | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c) + in + let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in + return (pr_i ++ pr_mayeval r c) + | VernacGlobalCheck c -> + return (hov 2 (str"Type" ++ pr_constrarg c)) + | VernacDeclareReduction (s,r) -> + return ( + str "Declare Reduction " ++ str s ++ str " := " ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r + ) + | VernacPrint p -> + return (pr_printable p) + | VernacSearch (sea,sea_r) -> + return (pr_search sea sea_r pr_constr_pattern_expr) + | VernacLocate loc -> + let pr_locate =function + | LocateAny qid -> pr_smart_global qid + | LocateTerm qid -> str "Term" ++ spc() ++ pr_smart_global qid + | LocateFile f -> str"File" ++ spc() ++ qs f + | LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid + | LocateModule qid -> str"Module" ++ spc () ++ pr_module qid + | LocateTactic qid -> str"Ltac" ++ spc () ++ pr_ltac_ref qid + in + return (str"Locate" ++ spc() ++ pr_locate loc) + | VernacRegister (id, RegisterInline) -> + return ( + hov 2 + (str "Register Inline" ++ spc() ++ pr_lident id) + ) + | VernacComments l -> + return ( + hov 2 + (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) + ) + | VernacNop -> + mt() + + (* Toplevel control *) + | VernacToplevelControl exn -> + return (pr_topcmd exn) + + (* For extension *) + | VernacExtend (s,c) -> + return (pr_extend s c) + | VernacProof (None, None) -> + return (str "Proof") + | VernacProof (None, Some e) -> + return (str "Proof " ++ pr_using e) + | VernacProof (Some te, None) -> + return (str "Proof with" ++ spc() ++ pr_raw_tactic te) + | VernacProof (Some te, Some e) -> + return ( + str "Proof " ++ pr_using e ++ spc() ++ + str "with" ++ spc() ++pr_raw_tactic te + ) + | VernacProofMode s -> + return (str ("Proof Mode "^s)) + | VernacBullet b -> + return (begin match b with + | Dash n -> str (String.make n '-') + | Star n -> str (String.make n '*') + | Plus n -> str (String.make n '+') + end ++ spc()) + | VernacSubproof None -> + return (str "{") + | VernacSubproof (Some i) -> + return (str "BeginSubproof " ++ int i) + | VernacEndSubproof -> + return (str "}") +>>>>>>> Ppannotation.t: New constructor AVernac. and pr_vernac_list l = hov 2 (str"[" ++ spc() ++ @@ -1010,4 +1211,21 @@ module Make (Ppconstr : Ppconstrsig.Pp) = struct end -include Make (Ppconstr) +include Make (Ppconstr) (struct + let do_not_tag _ x = x + let tag_vernac = do_not_tag +end) + +module RichPp (Indexer : sig + val index : Ppannotation.t -> string +end) = struct + + include Make (Ppconstr.RichPp (Indexer)) (struct + open Ppannotation + + let tag_vernac v t = + Pp.open_tag (Indexer.index (AVernac v)) ++ t ++ Pp.close_tag () + + end) + +end |