Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ppvernac.ml Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open Names

open CErrors
open Util
open CAst

open Extend
open Decl_kinds
open Constrexpr
open Constrexpr_ops
open Vernacexpr
open Declaremods
open Pputils

  open Ppconstr

  let do_not_tag _ x = x
  let tag_keyword = do_not_tag ()
  let tag_vernac  = do_not_tag

  let keyword s = tag_keyword (str s)

  let pr_constr = pr_constr_expr
  let pr_lconstr = pr_lconstr_expr
  let pr_spc_lconstr =
    let env = Global.env () in
    let sigma = Evd.from_env env in
    pr_sep_com spc @@ pr_lconstr_expr env sigma

  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 UState 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_qualid

  let pr_ltac_ref = Libnames.pr_qualid

  let pr_module = Libnames.pr_qualid

  let pr_import_module = Libnames.pr_qualid

  let sep_end = function
    | VernacBullet _
    | VernacSubproof _
    | VernacEndSubproof -> str""
    | _ -> str"."

  let pr_gen t =
    let env = Global.env () in
    let sigma = Evd.from_env env in
    Pputils.pr_raw_generic env sigma t

  let sep = fun _ -> spc()
  let sep_v2 = fun _ -> str"," ++ spc()

  let pr_notation_entry = function
    | InConstrEntry -> keyword "constr"
    | InCustomEntry s -> keyword "custom" ++ spc () ++ str s

  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 = let open Notation_term in function
    | AsIdent -> spc () ++ keyword "as ident"
    | AsIdentOrPattern -> spc () ++ keyword "as pattern"
    | AsStrictPattern -> spc () ++ keyword "as strict pattern"

  let pr_strict b = if b then str "strict " else mt ()

  let pr_set_entry_type pr = function
    | ETIdent -> str"ident"
    | ETGlobal -> 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 (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
    | 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 ->
          let env = Global.env () in
          let sigma = Evd.from_env env in
          pr_constr_pattern_expr env sigma 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_option_ref_value = function
    | QualidRefValue id -> pr_qualid 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 =
    pr_printoption a None ++ (match b with
        | OptionUnset | OptionSetTrue -> mt()
        | OptionSetInt n -> spc() ++ int n
        | OptionSetString s -> spc() ++ quote (str s))

  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 = let open Hints in function
    | HintsReference r -> pr_qualid r
    | HintsConstr c -> pr_c c

  let pr_hint_mode = let open Hints in 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 =
      let open Hints in
      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
        | HintsResolveIFF (l2r, l, n) ->
          keyword "Resolve " ++ str (if l2r then "->" else "<-")
          ++ prlist_with_sep sep pr_qualid 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_qualid l
        | HintsTransparency (l, b) ->
          keyword (if b then "Transparent" else "Opaque")
          ++ spc ()
          ++ (match l with
              | HintsVariables -> keyword "Variables"
              | HintsConstants -> keyword "Constants"
              | HintsReferences l -> prlist_with_sep sep pr_qualid l)
        | HintsMode (m, l) ->
          keyword "Mode"
          ++ spc ()
          ++ pr_qualid m ++ spc() ++
            prlist_with_sep spc pr_hint_mode l
        | HintsConstructors c ->
          keyword "Constructors"
          ++ spc() ++ prlist_with_sep spc pr_qualid c
        | HintsExtern (n,c,tac) ->
          let pat = match c with None -> mt () | Some pat -> pr_pat pat in
          let env = Global.env () in
          let sigma = Evd.from_env env in
          keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
            spc() ++ Pputils.pr_raw_generic env sigma 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_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, Namegen.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 =
    let env = Global.env () in
    let sigma = Evd.from_env env in
    pr_non_empty_arg @@ pr_binders env sigma

  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() ++ Sorts.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() ++ Sorts.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 = let open Gramlib.Gramext in function
    | SetItemLevel (l,bko,n) ->
      prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++
      pr_opt pr_constr_as_binder_kind bko
    | SetLevel n -> pr_at_level (NumLevel n)
    | SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some 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 env = Global.env () in
    let sigma = Evd.from_env env in
    let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
    let annot = pr_guard_annot (pr_lconstr_expr env sigma) bl ro in
    pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot
    ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) type_
    ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) def
    ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn

  let pr_statement head (idpl,(bl,c)) =
    let env = Global.env () in
    let sigma = Evd.from_env env in
    hov 2
      (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
         (match bl with [] -> mt() | _ -> pr_binders env sigma bl ++ spc()) ++
         str":" ++ pr_spc_lconstr c)

(**************************************)
(* Pretty printer for vernac commands *)
(**************************************)

  let pr_constrarg c =
    let env = Global.env () in
    let sigma = Evd.from_env env in
    spc () ++ pr_constr env sigma c
  let pr_lconstrarg c =
    let env = Global.env () in
    let sigma = Evd.from_env env in
    spc () ++ pr_lconstr env sigma 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 env = Global.env () in
    let sigma = Evd.from_env env in
    let prx = match x with
      | (oc,AssumExpr (id,t)) ->
        hov 1 (pr_lname id ++
                 pr_oc oc ++ spc() ++
                 pr_lconstr_expr env sigma t)
      | (oc,DefExpr(id,b,opt)) -> (match opt with
          | Some t ->
            hov 1 (pr_lname id ++
                     pr_oc oc ++ spc() ++
                     pr_lconstr_expr env sigma t ++ str" :=" ++ pr_lconstr env sigma b)
          | None ->
            hov 1 (pr_lname id ++ str" :=" ++ spc() ++
                     pr_lconstr env sigma b)) in
    let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
    prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) 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_qualid s
    | PrintGrammar ent ->
      keyword "Print Grammar" ++ spc() ++ str ent
    | PrintCustomGrammar ent ->
      keyword "Print Custom 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, g, fopt) ->
      let cmd =
        if b then "Print Sorted Universes"
        else "Print Universes"
      in
      let pr_subgraph = prlist_with_sep spc pr_qualid in
      keyword cmd ++ pr_opt pr_subgraph g ++ 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_qualid qid
    | PrintModule qid ->
      keyword "Print Module" ++ spc() ++ pr_qualid 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
    | PrintRegistered ->
      keyword "Print Registered"

  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 " ++ str (fst s) ++ str ">" in
    try
      let rl = Egramml.get_extend_vernac_rule s in
      let rec aux rl cl =
        match rl, cl with
        | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
        | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
        | [], [] -> []
        | _ -> assert false in
      hov 1 (pr_sequence identity (aux rl cl))
    with Not_found ->
      hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")

  let pr_vernac_expr v =
    let return = tag_vernac v in
    let env = Global.env () in
    let sigma = Evd.from_env env 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_qualid 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
        )
      | VernacDeclareScope sc ->
        return (
          keyword "Declare 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
        )
      | VernacDeclareCustomEntry s ->
        return (
          keyword "Declare Custom Entry " ++ str s
        )

      (* 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() ++
              Ppred.pr_red_expr_env env sigma (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 env sigma 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 env sigma 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 env sigma s) s ++
              str" :=") ++ pr_constructor_list k lc ++
            prlist (pr_decl_notation @@ pr_constr env sigma) 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 env sigma bl ++ spc() ++ str":" ++
            spc() ++ pr_lconstr_expr env sigma c ++
            pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) def ++
            prlist (pr_decl_notation @@ pr_constr env sigma) 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 (sup, (instid, bk, cl), props, info) ->
        return (
          hov 1 (
            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 env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) 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 env sigma p
                | None -> mt()))
        )

      | VernacDeclareInstance (sup, (instid, bk, cl), info) ->
        return (
          hov 1 (
            keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++
            pr_and_type_binders_arg sup ++
              str":" ++ spc () ++
              (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
              pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info)
        )

      | VernacContext l ->
        return (
          hov 1 (
            keyword "Context" ++ pr_and_type_binders_arg l)
        )

      | VernacExistingInstance insts ->
        let pr_inst (id, info) =
           pr_qualid id ++ pr_hint_info (pr_constr_pattern_expr env sigma) info
         in
         return (
          hov 1 (keyword "Existing" ++ spc () ++
                   keyword(String.plural (List.length insts) "Instance") ++
                 spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
        )

      | VernacExistingClass id ->
        return (
          hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id)
        )

      (* Modules and Module Types *)
      | VernacDefineModule (export,m,bl,tys,bd) ->
        let b = pr_module_binders bl (pr_lconstr env sigma) in
        return (
          hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
                   pr_lident m ++ b ++
                   pr_of_module_type (pr_lconstr env sigma) tys ++
                   (if List.is_empty bd then mt () else str ":= ") ++
                   prlist_with_sep (fun () -> str " <+")
                   (pr_module_ast_inl true (pr_lconstr env sigma)) bd)
        )
      | VernacDeclareModule (export,id,bl,m1) ->
        let b = pr_module_binders bl (pr_lconstr env sigma) in
        return (
          hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
                   pr_lident id ++ b ++ str " :" ++
                   pr_module_ast_inl true (pr_lconstr env sigma) m1)
        )
      | VernacDeclareModuleType (id,bl,tyl,m) ->
        let b = pr_module_binders bl (pr_lconstr env sigma) in
        let pr_mt = pr_module_ast_inl true (pr_lconstr env sigma) 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 env sigma) 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 env sigma) (pr_constr_pattern_expr env sigma))
      | 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
                | Impargs.Implicit -> str "[" ++ x ++ str "]"
                | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
                | Impargs.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 env sigma) (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))
        )
      | VernacSetOption (export, na,v) ->
        let export = if export then keyword "Export" ++ spc () else mt () in
        let set = if v == OptionUnset then "Unset" else "Set" 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() ++
                     Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
                     spc() ++ keyword "in" ++ spc () ++ pr_lconstr env sigma c)
          | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr env sigma 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 " := " ++
            Ppred.pr_red_expr_env env sigma (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 env sigma)
      | 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 (qid, RegisterCoqlib name) ->
        return (
          hov 2
            (keyword "Register" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as"
             ++ spc () ++ pr_qualid name)
        )
      | VernacRegister (qid, RegisterInline) ->
        return (
          hov 2
            (keyword "Register Inline" ++ spc() ++ pr_qualid qid)
        )
      | VernacPrimitive(id,r,typopt) ->
         hov 2
             (keyword "Primitive" ++ spc() ++ pr_lident id ++
                (Option.cata (fun ty -> spc() ++ str":" ++ pr_spc_lconstr ty) (mt()) typopt) ++ spc() ++
                str ":=" ++ spc() ++
                str (CPrimitives.op_or_type_to_string r))
      | VernacComments l ->
        return (
          hov 2
            (keyword "Comments" ++ spc()
             ++ prlist_with_sep sep (pr_comment (pr_constr env sigma)) 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 env sigma te)
      | VernacProof (Some te, Some e) ->
        return (
          keyword "Proof" ++ spc () ++
            keyword "using" ++ spc() ++ pr_using e ++ spc() ++
            keyword "with" ++ spc() ++ Pputils.pr_raw_generic env sigma 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 rec pr_vernac_flag (k, v) =
  let k = keyword k in
  let open Attributes in
  match v with
  | VernacFlagEmpty -> k
  | VernacFlagLeaf v -> k ++ str " = " ++ qs v
  | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )"
and pr_vernac_flags m =
  prlist_with_sep (fun () -> str ", ") pr_vernac_flag m

let pr_vernac_attributes =
  function
  | [] -> mt ()
  | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()

  let rec pr_vernac_control v =
    let return = tag_vernac v in
    match v with
    | VernacExpr (f, v') -> pr_vernac_attributes 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

¤ Dauer der Verarbeitung: 0.91 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.