From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- printing/genprint.ml | 45 ++ printing/genprint.mli | 28 + printing/miscprint.ml | 49 ++ printing/miscprint.mli | 24 + printing/ppannotation.ml | 41 ++ printing/ppannotation.mli | 33 + printing/ppconstr.ml | 812 ++++++++++++++++++++++++ printing/ppconstr.mli | 21 + printing/ppconstrsig.mli | 95 +++ printing/ppstyle.ml | 149 +++++ printing/ppstyle.mli | 70 +++ printing/pptactic.ml | 1499 +++++++++++++++++++++++++++++++++++++++++++++ printing/pptactic.mli | 65 ++ printing/pptacticsig.mli | 95 +++ printing/pputils.ml | 15 + printing/pputils.mli | 13 + printing/ppvernac.ml | 1296 +++++++++++++++++++++++++++++++++++++++ printing/ppvernac.mli | 20 + printing/ppvernacsig.mli | 17 + printing/prettyp.ml | 852 ++++++++++++++++++++++++++ printing/prettyp.mli | 77 +++ printing/printer.ml | 760 +++++++++++++++++++++++ printing/printer.mli | 177 ++++++ printing/printing.mllib | 14 + printing/printmod.ml | 438 +++++++++++++ printing/printmod.mli | 14 + printing/printmodsig.mli | 17 + printing/richprinter.ml | 26 + printing/richprinter.mli | 41 ++ 29 files changed, 6803 insertions(+) create mode 100644 printing/genprint.ml create mode 100644 printing/genprint.mli create mode 100644 printing/miscprint.ml create mode 100644 printing/miscprint.mli create mode 100644 printing/ppannotation.ml create mode 100644 printing/ppannotation.mli create mode 100644 printing/ppconstr.ml create mode 100644 printing/ppconstr.mli create mode 100644 printing/ppconstrsig.mli create mode 100644 printing/ppstyle.ml create mode 100644 printing/ppstyle.mli create mode 100644 printing/pptactic.ml create mode 100644 printing/pptactic.mli create mode 100644 printing/pptacticsig.mli create mode 100644 printing/pputils.ml create mode 100644 printing/pputils.mli create mode 100644 printing/ppvernac.ml create mode 100644 printing/ppvernac.mli create mode 100644 printing/ppvernacsig.mli create mode 100644 printing/prettyp.ml create mode 100644 printing/prettyp.mli create mode 100644 printing/printer.ml create mode 100644 printing/printer.mli create mode 100644 printing/printing.mllib create mode 100644 printing/printmod.ml create mode 100644 printing/printmod.mli create mode 100644 printing/printmodsig.mli create mode 100644 printing/richprinter.ml create mode 100644 printing/richprinter.mli (limited to 'printing') diff --git a/printing/genprint.ml b/printing/genprint.ml new file mode 100644 index 00000000..ade69ef8 --- /dev/null +++ b/printing/genprint.ml @@ -0,0 +1,45 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds; + glb : 'glb -> std_ppcmds; + top : 'top -> std_ppcmds; +} + +module PrintObj = +struct + type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer + let name = "printer" + let default wit = match unquote (rawwit wit) with + | ExtraArgType name -> + let printer = { + raw = (fun _ -> str ""); + glb = (fun _ -> str ""); + top = (fun _ -> str ""); + } in + Some printer + | _ -> assert false +end + +module Print = Register (PrintObj) + +let register_print0 wit raw glb top = + let printer = { raw; glb; top; } in + Print.register0 wit printer + +let raw_print wit v = (Print.obj wit).raw v +let glb_print wit v = (Print.obj wit).glb v +let top_print wit v = (Print.obj wit).top v + +let generic_raw_print v = unpack { unpacker = fun w v -> raw_print w (raw v); } v +let generic_glb_print v = unpack { unpacker = fun w v -> glb_print w (glb v); } v +let generic_top_print v = unpack { unpacker = fun w v -> top_print w (top v); } v diff --git a/printing/genprint.mli b/printing/genprint.mli new file mode 100644 index 00000000..5b91d6d2 --- /dev/null +++ b/printing/genprint.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'raw -> std_ppcmds +(** Printer for raw level generic arguments. *) + +val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds +(** Printer for glob level generic arguments. *) + +val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds +(** Printer for top level generic arguments. *) + +val generic_raw_print : rlevel generic_argument -> std_ppcmds +val generic_glb_print : glevel generic_argument -> std_ppcmds +val generic_top_print : tlevel generic_argument -> std_ppcmds + +val register_print0 : ('raw, 'glb, 'top) genarg_type -> + ('raw -> std_ppcmds) -> ('glb -> std_ppcmds) -> ('top -> std_ppcmds) -> unit diff --git a/printing/miscprint.ml b/printing/miscprint.ml new file mode 100644 index 00000000..d09af6d2 --- /dev/null +++ b/printing/miscprint.ml @@ -0,0 +1,49 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* str "*" + | IntroForthcoming false -> str "**" + | IntroNaming p -> pr_intro_pattern_naming p + | IntroAction p -> pr_intro_pattern_action prc p + +and pr_intro_pattern_naming = function + | IntroIdentifier id -> Nameops.pr_id id + | IntroFresh id -> str "?" ++ Nameops.pr_id id + | IntroAnonymous -> str "?" + +and pr_intro_pattern_action prc = function + | IntroWildcard -> str "_" + | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll + | IntroInjection pl -> + str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ + str "]" + | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "/" ++ prc c + | IntroRewrite true -> str "->" + | IntroRewrite false -> str "<-" + +and pr_or_and_intro_pattern prc = function + | [pl] -> + str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")" + | pll -> + str "[" ++ + hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) + ++ str "]" + +(** Printing of [move_location] *) + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveFirst -> str " at top" + | MoveLast -> str " at bottom" diff --git a/printing/miscprint.mli b/printing/miscprint.mli new file mode 100644 index 00000000..1d915ef8 --- /dev/null +++ b/printing/miscprint.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds + +val pr_or_and_intro_pattern : + ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds + +val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds + +(** Printing of [move_location] *) + +val pr_move_location : + ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml new file mode 100644 index 00000000..4f26b824 --- /dev/null +++ b/printing/ppannotation.ml @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* "keyword" + | AUnparsing _ -> "unparsing" + | AConstrExpr _ -> "constr_expr" + | AVernac _ -> "vernac_expr" + | AGlobTacticExpr _ -> "glob_tactic_expr" + | AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr" + | ARawTacticExpr _ -> "raw_tactic_expr" + | ARawAtomicTacticExpr _ -> "raw_atomic_tactic_expr" + | ATacticExpr _ -> "tactic_expr" + | AAtomicTacticExpr _ -> "atomic_tactic_expr" + +let attributes_of_annotation a = + [] + +let tag = Pp.Tag.create "ppannotation" diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli new file mode 100644 index 00000000..bc345c34 --- /dev/null +++ b/printing/ppannotation.mli @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string + +val attributes_of_annotation : t -> (string * string) list + +val tag : t Pp.Tag.key diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml new file mode 100644 index 00000000..d9d8af66 --- /dev/null +++ b/printing/ppconstr.ml @@ -0,0 +1,812 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds + val tag_evar : std_ppcmds -> std_ppcmds + val tag_type : std_ppcmds -> std_ppcmds + val tag_path : std_ppcmds -> std_ppcmds + val tag_ref : std_ppcmds -> std_ppcmds + val tag_var : std_ppcmds -> std_ppcmds + val tag_constr_expr : constr_expr -> std_ppcmds -> std_ppcmds + val tag_unparsing : unparsing -> std_ppcmds -> std_ppcmds +end) = struct + + open Taggers + + let keyword s = tag_keyword (str s) + let sep_v = fun _ -> str"," ++ spc() + let pr_tight_coma () = str "," ++ cut () + + let latom = 0 + let lprod = 200 + let llambda = 200 + let lif = 200 + let lletin = 200 + let lletpattern = 200 + let lfix = 200 + let lcast = 100 + let larg = 9 + let lapp = 10 + let lposint = 0 + let lnegint = 35 (* must be consistent with Notation "- x" *) + let ltop = (200,E) + let lproj = 1 + let ldelim = 1 + let lsimpleconstr = (8,E) + let lsimplepatt = (1,E) + + let prec_less child (parent,assoc) = + if parent < 0 && Int.equal child lprod then true + else + let parent = abs parent in + match assoc with + | E -> (<=) child parent + | L -> (<) child parent + | Prec n -> child<=n + | Any -> true + + let prec_of_prim_token = function + | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint + | String _ -> latom + + open Notation + + let print_hunks n pr pr_binders (terms, termlists, binders) unps = + let env = ref terms and envlist = ref termlists and bll = ref binders in + let pop r = let a = List.hd !r in r := List.tl !r; a in + let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in + (* Warning: + The following function enforces a very precise order of + evaluation of sub-components. + Do not modify it unless you know what you are doing! *) + let rec aux = function + | [] -> + mt () + | UnpMetaVar (_, prec) as unp :: l -> + let c = pop env in + let pp2 = aux l in + let pp1 = pr (n, prec) c in + return unp pp1 pp2 + | UnpListMetaVar (_, prec, sl) as unp :: l -> + let cl = pop envlist in + let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in + let pp2 = aux l in + return unp pp1 pp2 + | UnpBinderListMetaVar (_, isopen, sl) as unp :: l -> + let cl = pop bll in + let pp2 = aux l in + let pp1 = pr_binders (fun () -> aux sl) isopen cl in + return unp pp1 pp2 + | UnpTerminal s as unp :: l -> + let pp2 = aux l in + let pp1 = str s in + return unp pp1 pp2 + | UnpBox (b,sub) as unp :: l -> + let pp1 = ppcmd_of_box b (aux sub) in + let pp2 = aux l in + return unp pp1 pp2 + | UnpCut cut as unp :: l -> + let pp2 = aux l in + let pp1 = ppcmd_of_cut cut in + return unp pp1 pp2 + in + aux unps + + let pr_notation pr pr_binders s env = + let unpl, level = find_notation_printing_rule s in + print_hunks level pr pr_binders env unpl, level + + let pr_delimiters key strm = + strm ++ str ("%"^key) + + let pr_generalization bk ak c = + let hd, tl = + match bk with + | Implicit -> "{", "}" + | Explicit -> "(", ")" + in (* TODO: syntax Abstraction Kind *) + str "`" ++ str hd ++ c ++ str tl + + let pr_com_at n = + if Flags.do_beautify() && not (Int.equal n 0) then comment n + else mt() + + let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) + + let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) + + let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" + + let pr_univ l = + match l with + | [x] -> str x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")" + + let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" + + let pr_glob_sort = function + | GProp -> tag_type (str "Prop") + | GSet -> tag_type (str "Set") + | GType [] -> tag_type (str "Type") + | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) + + let pr_qualid sp = + let (sl, id) = repr_qualid sp in + let id = tag_ref (str (Id.to_string id)) in + let sl = match List.rev (DirPath.repr sl) with + | [] -> mt () + | sl -> + let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in + prlist pr sl + in + sl ++ id + + let pr_id = pr_id + let pr_name = pr_name + let pr_qualid = pr_qualid + let pr_patvar = pr_id + + let pr_glob_sort_instance = function + | GProp -> + tag_type (str "Prop") + | GSet -> + tag_type (str "Set") + | GType u -> + (match u with + | Some u -> str u + | None -> tag_type (str "Type")) + + let pr_universe_instance l = + pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l + + let pr_reference = function + | Qualid (_, qid) -> pr_qualid qid + | Ident (_, id) -> tag_var (str (Id.to_string id)) + + let pr_cref ref us = + pr_reference ref ++ pr_universe_instance us + + let pr_expl_args pr (a,expl) = + match expl with + | None -> pr (lapp,L) a + | Some (_,ExplByPos (n,_id)) -> + anomaly (Pp.str "Explicitation by position not implemented") + | Some (_,ExplByName id) -> + str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" + + let pr_opt_type pr = function + | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () + | t -> cut () ++ str ":" ++ pr t + + let pr_opt_type_spc pr = function + | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () + | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t + + let pr_lident (loc,id) = + if not (Loc.is_ghost loc) then + let (b,_) = Loc.unloc loc in + pr_located pr_id (Loc.make_loc (b,b + String.length (Id.to_string id)), id) + else + pr_id id + + let pr_lname = function + | (loc,Name id) -> pr_lident (loc,id) + | lna -> pr_located pr_name lna + + let pr_or_var pr = function + | ArgArg x -> pr x + | ArgVar (loc,s) -> pr_lident (loc,s) + + let pr_prim_token = function + | Numeral n -> str (Bigint.to_string n) + | String s -> qs s + + let pr_evar pr id l = + hov 0 ( + tag_evar (str "?" ++ pr_id id) ++ + (match l with + | [] -> mt() + | l -> + let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in + str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) + + let las = lapp + let lpator = 100 + let lpatrec = 0 + + let rec pr_patt sep inh p = + let (strm,prec) = match p with + | CPatRecord (_, l) -> + let pp (c, p) = + pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p + in + str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec + + | CPatAlias (_, p, id) -> + pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las + + | CPatCstr (_,c, [], []) -> + pr_reference c, latom + + | CPatCstr (_, c, [], args) -> + pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + + | CPatCstr (_, c, args, []) -> + str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + + | CPatCstr (_, c, expl_args, extra_args) -> + surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args) + ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp + + | CPatAtom (_, None) -> + str "_", latom + + | CPatAtom (_,Some r) -> + pr_reference r, latom + + | CPatOr (_,pl) -> + hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator + + | CPatNotation (_,"( _ )",([p],[]),[]) -> + pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom + + | CPatNotation (_,s,(l,ll),args) -> + let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in + (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not) + ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not + + | CPatPrim (_,p) -> + pr_prim_token p, latom + + | CPatDelimiters (_,k,p) -> + pr_delimiters k (pr_patt mt lsimplepatt p), 1 + in + let loc = cases_pattern_expr_loc p in + pr_with_comments loc + (sep() ++ if prec_less prec inh then strm else surround strm) + + let pr_patt = pr_patt mt + + let pr_eqn pr (loc,pl,rhs) = + let pl = List.map snd pl in + spc() ++ hov 4 + (pr_with_comments loc + (str "| " ++ + hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl + ++ str " =>") ++ + pr_sep_com spc (pr ltop) rhs)) + + let begin_of_binder = function + LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) + | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) + | _ -> assert false + + let begin_of_binders = function + | b::_ -> begin_of_binder b + | _ -> 0 + + let surround_impl k p = + match k with + | Explicit -> str"(" ++ p ++ str")" + | Implicit -> str"{" ++ p ++ str"}" + + let surround_implicit k p = + match k with + | Explicit -> p + | Implicit -> (str"{" ++ p ++ str"}") + + let pr_binder many pr (nal,k,t) = + match k with + | Generalized (b, b', t') -> + assert (match b with Implicit -> true | _ -> false); + begin match nal with + |[loc,Anonymous] -> + hov 1 (str"`" ++ (surround_impl b' + ((if t' then str "!" else mt ()) ++ pr t))) + |[loc,Name id] -> + hov 1 (str "`" ++ (surround_impl b' + (pr_lident (loc,id) ++ str " : " ++ + (if t' then str "!" else mt()) ++ pr t))) + |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") + end + | Default b -> + match t with + | CHole (_,_,Misctypes.IntroAnonymous,_) -> + let s = prlist_with_sep spc pr_lname nal in + hov 1 (surround_implicit b s) + | _ -> + let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ pr t in + hov 1 (if many then surround_impl b s else surround_implicit b s) + + let pr_binder_among_many pr_c = function + | LocalRawAssum (nal,k,t) -> + pr_binder true pr_c (nal,k,t) + | LocalRawDef (na,c) -> + let c,topt = match c with + | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t + | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in + surround (pr_lname na ++ pr_opt_type pr_c topt ++ + str":=" ++ cut() ++ pr_c c) + + let pr_undelimited_binders sep pr_c = + prlist_with_sep sep (pr_binder_among_many pr_c) + + let pr_delimited_binders kw sep pr_c bl = + let n = begin_of_binders bl in + match bl with + | [LocalRawAssum (nal,k,t)] -> + pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) + | LocalRawAssum _ :: _ as bdl -> + pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl + | _ -> assert false + + let pr_binders_gen pr_c sep is_open = + if is_open then pr_delimited_binders mt sep pr_c + else pr_undelimited_binders sep pr_c + + let rec extract_prod_binders = function + (* | CLetIn (loc,na,b,c) as x -> + let bl,c = extract_prod_binders c in + if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + | CProdN (loc,[],c) -> + extract_prod_binders c + | CProdN (loc,(nal,bk,t)::bl,c) -> + let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in + LocalRawAssum (nal,bk,t) :: bl, c + | c -> [], c + + let rec extract_lam_binders = function + (* | CLetIn (loc,na,b,c) as x -> + let bl,c = extract_lam_binders c in + if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + | CLambdaN (loc,[],c) -> + extract_lam_binders c + | CLambdaN (loc,(nal,bk,t)::bl,c) -> + let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in + LocalRawAssum (nal,bk,t) :: bl, c + | c -> [], c + + let split_lambda = function + | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c) + | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c)) + | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c)) + | _ -> anomaly (Pp.str "ill-formed fixpoint body") + + let rename na na' t c = + match (na,na') with + | (_,Name id), (_,Name id') -> + (na',t,Topconstr.replace_vars_constr_expr (Id.Map.singleton id id') c) + | (_,Name id), (_,Anonymous) -> (na,t,c) + | _ -> (na',t,c) + + let split_product na' = function + | CProdN (loc,[[na],bk,t],c) -> rename na na' t c + | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c)) + | CProdN (loc,(na::nal,bk,t)::bl,c) -> + rename na na' t (CProdN(loc,(nal,bk,t)::bl,c)) + | _ -> anomaly (Pp.str "ill-formed fixpoint body") + + let rec split_fix n typ def = + if Int.equal n 0 then ([],typ,def) + else + let (na,_,def) = split_lambda def in + let (na,t,typ) = split_product na typ in + let (bl,typ,def) = split_fix (n-1) typ def in + (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def) + + let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = + let pr_body = + if dangling_with_for then pr_dangling else pr in + pr_id id ++ str" " ++ + hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++ + pr_opt_type_spc pr t ++ str " :=" ++ + pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c + + let pr_guard_annot pr_aux bl (n,ro) = + match n with + | None -> mt () + | Some (loc, id) -> + match (ro : Constrexpr.recursion_order_expr) with + | CStructRec -> + let names_of_binder = function + | LocalRawAssum (nal,_,_) -> nal + | LocalRawDef (_,_) -> [] + in let ids = List.flatten (List.map names_of_binder bl) in + if List.length ids > 1 then + spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" + else mt() + | CWfRec c -> + spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_id id ++ str"}" + | CMeasureRec (m,r) -> + spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++ + (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" + + let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) = + let annot = pr_guard_annot (pr lsimpleconstr) bl ro in + pr_recursive_decl pr prd dangling_with_for id bl annot t c + + let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) = + pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c + + let pr_recursive pr_decl id = function + | [] -> anomaly (Pp.str "(co)fixpoint with no definition") + | [d1] -> pr_decl false d1 + | dl -> + prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ()) + (pr_decl true) dl ++ + fnl() ++ keyword "for" ++ spc () ++ pr_id id + + let pr_asin pr (na,indnalopt) = + (match na with (* Decision of printing "_" or not moved to constrextern.ml *) + | Some na -> spc () ++ keyword "as" ++ spc () ++ pr_lname na + | None -> mt ()) ++ + (match indnalopt with + | None -> mt () + | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t) + + let pr_case_item pr (tm,asin) = + hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) + + let pr_case_type pr po = + match po with + | None | Some (CHole (_,_,Misctypes.IntroAnonymous,_)) -> mt() + | Some p -> + spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p) + + let pr_simple_return_type pr na po = + (match na with + | Some (_,Name id) -> + spc () ++ keyword "as" ++ spc () ++ pr_id id + | _ -> mt ()) ++ + pr_case_type pr po + + let pr_proj pr pr_app a f l = + hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") + + let pr_appexpl pr (f,us) l = + hov 2 ( + str "@" ++ pr_reference f ++ + pr_universe_instance us ++ + prlist (pr_sep_com spc (pr (lapp,L))) l) + + let pr_app pr a l = + hov 2 ( + pr (lapp,L) a ++ + prlist (fun a -> spc () ++ pr_expl_args pr a) l) + + let pr_forall () = keyword "forall" ++ spc () + + let pr_fun () = keyword "fun" ++ spc () + + let pr_fun_sep = spc () ++ str "=>" + + let pr_dangling_with_for sep pr inherited a = + match a with + | (CFix (_,_,[_])|CCoFix(_,_,[_])) -> + pr sep (latom,E) a + | _ -> + pr sep inherited a + + let pr pr sep inherited a = + let return (cmds, prec) = (tag_constr_expr a cmds, prec) in + let (strm, prec) = match a with + | CRef (r, us) -> + return (pr_cref r us, latom) + | CFix (_,id,fix) -> + return ( + hov 0 (keyword "fix" ++ spc () ++ + pr_recursive + (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix), + lfix + ) + | CCoFix (_,id,cofix) -> + return ( + hov 0 (keyword "cofix" ++ spc () ++ + pr_recursive + (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), + lfix + ) + | CProdN _ -> + let (bl,a) = extract_prod_binders a in + return ( + hov 0 ( + hov 2 (pr_delimited_binders pr_forall spc + (pr mt ltop) bl) ++ + str "," ++ pr spc ltop a), + lprod + ) + | CLambdaN _ -> + let (bl,a) = extract_lam_binders a in + return ( + hov 0 ( + hov 2 (pr_delimited_binders pr_fun spc + (pr mt ltop) bl) ++ + pr_fun_sep ++ pr spc ltop a), + llambda + ) + | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) + when Id.equal x x' -> + return ( + hv 0 ( + hov 2 (keyword "let" ++ spc () ++ pr mt ltop fx + ++ spc () + ++ keyword "in") ++ + pr spc ltop b), + lletin + ) + | CLetIn (_,x,a,b) -> + return ( + hv 0 ( + hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :=" + ++ pr spc ltop a ++ spc () + ++ keyword "in") ++ + pr spc ltop b), + lletin + ) + | CAppExpl (_,(Some i,f,us),l) -> + let l1,l2 = List.chop i l in + let c,l1 = List.sep_last l1 in + let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in + if not (List.is_empty l2) then + return (p ++ prlist (pr spc (lapp,L)) l2, lapp) + else + return (p, lproj) + | CAppExpl (_,(None,Ident (_,var),us),[t]) + | CApp (_,(_,CRef(Ident(_,var),us)),[t,None]) + when Id.equal var Notation_ops.ldots_var -> + return ( + hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), + larg + ) + | CAppExpl (_,(None,f,us),l) -> + return (pr_appexpl (pr mt) (f,us) l, lapp) + | CApp (_,(Some i,f),l) -> + let l1,l2 = List.chop i l in + let c,l1 = List.sep_last l1 in + assert (Option.is_empty (snd c)); + let p = pr_proj (pr mt) pr_app (fst c) f l1 in + if not (List.is_empty l2) then + return ( + p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, + lapp + ) + else + return (p, lproj) + | CApp (_,(None,a),l) -> + return (pr_app (pr mt) a l, lapp) + | CRecord (_,w,l) -> + let beg = + match w with + | None -> + spc () + | Some t -> + spc () ++ pr spc ltop t ++ spc () + ++ keyword "with" ++ spc () + in + return ( + hv 0 (str"{|" ++ beg ++ + prlist_with_sep pr_semicolon + (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l + ++ str" |}"), + latom + ) + | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) -> + return ( + hv 0 ( + keyword "let" ++ spc () ++ str"'" ++ + hov 0 (pr_patt ltop p ++ + pr_asin (pr_dangling_with_for mt pr) asin ++ + str " :=" ++ pr spc ltop c ++ + pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++ + spc () ++ keyword "in" ++ pr spc ltop b)), + lletpattern + ) + | CCases(_,_,rtntypopt,c,eqns) -> + return ( + v 0 + (hv 0 (keyword "match" ++ brk (1,2) ++ + hov 0 ( + prlist_with_sep sep_v + (pr_case_item (pr_dangling_with_for mt pr)) c + ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt) ++ + spc () ++ keyword "with") ++ + prlist (pr_eqn (pr mt)) eqns ++ spc() + ++ keyword "end"), + latom + ) + | CLetTuple (_,nal,(na,po),c,b) -> + return ( + hv 0 ( + keyword "let" ++ spc () ++ + hov 0 (str "(" ++ + prlist_with_sep sep_v pr_lname nal ++ + str ")" ++ + pr_simple_return_type (pr mt) na po ++ str " :=" ++ + pr spc ltop c ++ spc () + ++ keyword "in") ++ + pr spc ltop b), + lletin + ) + | CIf (_,c,(na,po),b1,b2) -> + (* On force les parenthèses autour d'un "if" sous-terme (même si le + parsing est lui plus tolérant) *) + return ( + hv 0 ( + hov 1 (keyword "if" ++ spc () ++ pr mt ltop c + ++ pr_simple_return_type (pr mt) na po) ++ + spc () ++ + hov 0 (keyword "then" + ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++ + hov 0 (keyword "else" ++ pr (fun () -> brk (1,1)) ltop b2)), + lif + ) + + | CHole (_,_,Misctypes.IntroIdentifier id,_) -> + return (str "?[" ++ pr_id id ++ str "]", latom) + | CHole (_,_,Misctypes.IntroFresh id,_) -> + return (str "?[?" ++ pr_id id ++ str "]", latom) + | CHole (_,_,_,_) -> + return (str "_", latom) + | CEvar (_,n,l) -> + return (pr_evar (pr mt) n l, latom) + | CPatVar (_,p) -> + return (str "?" ++ pr_patvar p, latom) + | CSort (_,s) -> + return (pr_glob_sort s, latom) + | CCast (_,a,b) -> + return ( + hv 0 (pr mt (lcast,L) a ++ cut () ++ + match b with + | CastConv b -> str ":" ++ pr mt (-lcast,E) b + | CastVM b -> str "<:" ++ pr mt (-lcast,E) b + | CastNative b -> str "<<:" ++ pr mt (-lcast,E) b + | CastCoerce -> str ":>"), + lcast + ) + | CNotation (_,"( _ )",([t],[],[])) -> + return (pr (fun()->str"(") (max_int,L) t ++ str")", latom) + | CNotation (_,s,env) -> + pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env + | CGeneralization (_,bk,ak,c) -> + return (pr_generalization bk ak (pr mt ltop c), latom) + | CPrim (_,p) -> + return (pr_prim_token p, prec_of_prim_token p) + | CDelimiters (_,sc,a) -> + return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) + in + let loc = constr_loc a in + pr_with_comments loc + (sep() ++ if prec_less prec inherited then strm else surround strm) + + type term_pr = { + pr_constr_expr : constr_expr -> std_ppcmds; + pr_lconstr_expr : constr_expr -> std_ppcmds; + pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; + pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds + } + + type precedence = Ppextend.precedence * Ppextend.parenRelation + let modular_constr_pr = pr + let rec fix rf x = rf (fix rf) x + let pr = fix modular_constr_pr mt + + let transf env c = + if !Flags.beautify_file then + let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in + Constrextern.extern_glob_constr (Termops.vars_of_env env) r + else c + + let pr prec c = pr prec (transf (Global.env()) c) + + let pr_simpleconstr = function + | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us + | c -> pr lsimpleconstr c + + let default_term_pr = { + pr_constr_expr = pr_simpleconstr; + pr_lconstr_expr = pr ltop; + pr_constr_pattern_expr = pr_simpleconstr; + pr_lconstr_pattern_expr = pr ltop + } + + let term_pr = ref default_term_pr + + let set_term_pr = (:=) term_pr + + let pr_constr_expr c = !term_pr.pr_constr_expr c + let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c + let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c + let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c + + let pr_cases_pattern_expr = pr_patt ltop + + let pr_binders = pr_undelimited_binders spc (pr ltop) + +end + +module Tag = +struct + let keyword = + let style = Terminal.make ~bold:true () in + Ppstyle.make ~style ["constr"; "keyword"] + + let evar = + let style = Terminal.make ~fg_color:`LIGHT_BLUE () in + Ppstyle.make ~style ["constr"; "evar"] + + let univ = + let style = Terminal.make ~bold:true ~fg_color:`YELLOW () in + Ppstyle.make ~style ["constr"; "type"] + + let notation = + let style = Terminal.make ~fg_color:`WHITE () in + Ppstyle.make ~style ["constr"; "notation"] + + let variable = + Ppstyle.make ["constr"; "variable"] + + let reference = + let style = Terminal.make ~fg_color:`LIGHT_GREEN () in + Ppstyle.make ~style ["constr"; "reference"] + + let path = + let style = Terminal.make ~fg_color:`LIGHT_MAGENTA () in + Ppstyle.make ~style ["constr"; "path"] + +end + +let do_not_tag _ x = x + +(** Instantiating Make with tagging functions that only add style + information. *) +include Make (struct + let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s + let tag_keyword = tag Tag.keyword + let tag_evar = tag Tag.evar + let tag_type = tag Tag.univ + let tag_unparsing = function + | UnpTerminal s -> tag Tag.notation + | _ -> do_not_tag () + let tag_constr_expr = do_not_tag + let tag_path = tag Tag.path + let tag_ref = tag Tag.reference + let tag_var = tag Tag.variable +end) + +module Richpp = struct + + include Make (struct + open Ppannotation + let tag_keyword = Pp.tag (Pp.Tag.inj AKeyword tag) + let tag_type = Pp.tag (Pp.Tag.inj AKeyword tag) + let tag_evar = do_not_tag () + let tag_unparsing unp = Pp.tag (Pp.Tag.inj (AUnparsing unp) tag) + let tag_constr_expr e = Pp.tag (Pp.Tag.inj (AConstrExpr e) tag) + let tag_path = do_not_tag () + let tag_ref = do_not_tag () + let tag_var = do_not_tag () + end) + +end + diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli new file mode 100644 index 00000000..6e8d3b04 --- /dev/null +++ b/printing/ppconstr.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* local_binder list * constr_expr + val extract_prod_binders : + constr_expr -> local_binder list * constr_expr + val split_fix : + int -> constr_expr -> constr_expr -> + local_binder list * constr_expr * constr_expr + + val prec_less : int -> int * Ppextend.parenRelation -> bool + + val pr_tight_coma : unit -> std_ppcmds + + val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds + + val pr_lident : Id.t located -> std_ppcmds + val pr_lname : Name.t located -> std_ppcmds + + val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds + val pr_com_at : int -> std_ppcmds + val pr_sep_com : + (unit -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + constr_expr -> std_ppcmds + + val pr_id : Id.t -> std_ppcmds + val pr_name : Name.t -> std_ppcmds + val pr_qualid : qualid -> std_ppcmds + val pr_patvar : patvar -> std_ppcmds + + val pr_glob_sort : glob_sort -> std_ppcmds + val pr_guard_annot : (constr_expr -> std_ppcmds) -> + local_binder list -> + ('a * Names.Id.t) option * recursion_order_expr -> + std_ppcmds + + val pr_binders : local_binder list -> std_ppcmds + val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds + val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds + val pr_constr_expr : constr_expr -> std_ppcmds + val pr_lconstr_expr : constr_expr -> std_ppcmds + val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds + + type term_pr = { + pr_constr_expr : constr_expr -> std_ppcmds; + pr_lconstr_expr : constr_expr -> std_ppcmds; + pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; + pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds + } + + val set_term_pr : term_pr -> unit + val default_term_pr : term_pr + +(** The modular constr printer. + [modular_constr_pr pr s p t] prints the head of the term [t] and calls + [pr] on its subterms. + [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers + and [ltop] for "lconstr" printers (spiwack: we might need more + specification here). + We can make a new modular constr printer by overriding certain branches, + for instance if we want to build a printer which prints "Prop" as "Omega" + instead we can proceed as follows: + let my_modular_constr_pr pr s p = function + | CSort (_,GProp Null) -> str "Omega" + | t -> modular_constr_pr pr s p t + Which has the same type. We can turn a modular printer into a printer by + taking its fixpoint. *) + + type precedence + val lsimpleconstr : precedence + val ltop : precedence + val modular_constr_pr : + ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) -> + (unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds + +end + diff --git a/printing/ppstyle.ml b/printing/ppstyle.ml new file mode 100644 index 00000000..fb334c70 --- /dev/null +++ b/printing/ppstyle.ml @@ -0,0 +1,149 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* assert false + +let set_style tag st = + try tags := String.Map.update tag st !tags with Not_found -> assert false + +let clear_styles () = + tags := String.Map.map (fun _ -> None) !tags + +let dump () = String.Map.bindings !tags + +let parse_config s = + let styles = Terminal.parse s in + let set accu (name, st) = + try String.Map.update name (Some st) accu with Not_found -> accu + in + tags := List.fold_left set !tags styles + +let tag = Pp.Tag.create "ppstyle" + +(** Default tag is to reset everything *) +let default = Terminal.({ + fg_color = Some `DEFAULT; + bg_color = Some `DEFAULT; + bold = Some false; + italic = Some false; + underline = Some false; + negative = Some false; +}) + +let empty = Terminal.make () + +let make_style_stack style_tags = + (** Not thread-safe. We should put a lock somewhere if we print from + different threads. Do we? *) + let style_stack = ref [] in + let peek () = match !style_stack with + | [] -> default (** Anomalous case, but for robustness *) + | st :: _ -> st + in + let push tag = + let style = + try + begin match String.Map.find tag style_tags with + | None -> empty + | Some st -> st + end + with Not_found -> empty + in + (** Use the merging of the latest tag and the one being currently pushed. + This may be useful if for instance the latest tag changes the background and + the current one the foreground, so that the two effects are additioned. *) + let style = Terminal.merge (peek ()) style in + let () = style_stack := style :: !style_stack in + Terminal.eval style + in + let pop _ = match !style_stack with + | [] -> + (** Something went wrong, we fallback *) + Terminal.eval default + | _ :: rem -> + let () = style_stack := rem in + Terminal.eval (peek ()) + in + let clear () = style_stack := [] in + push, pop, clear + +let error_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in + make ~style ["message"; "error"] + +let warning_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in + make ~style ["message"; "warning"] + +let debug_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in + make ~style ["message"; "debug"] + +let pp_tag t = match Pp.Tag.prj t tag with +| None -> "" +| Some key -> key + +let init_color_output () = + let push_tag, pop_tag, clear_tag = make_style_stack !tags in + let tag_handler = { + Format.mark_open_tag = push_tag; + Format.mark_close_tag = pop_tag; + Format.print_open_tag = ignore; + Format.print_close_tag = ignore; + } in + let open Pp_control in + let () = Format.pp_set_mark_tags !std_ft true in + let () = Format.pp_set_mark_tags !err_ft true in + let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in + let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in + let pptag = tag in + let open Pp in + let msg ?header ft strm = + let strm = match header with + | None -> hov 0 strm + | Some (h, t) -> + let tag = Pp.Tag.inj t pptag in + let h = Pp.tag tag (str h ++ str ":") in + hov 0 (h ++ spc () ++ strm) + in + pp_with ~pp_tag ft strm; + Format.pp_print_newline ft (); + Format.pp_print_flush ft (); + (** In case something went wrong, we reset the stack *) + clear_tag (); + in + let logger level strm = match level with + | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm + | Info -> msg !std_ft strm + | Notice -> msg !std_ft strm + | Warning -> + let header = ("Warning", warning_tag) in + Flags.if_warn (fun () -> msg ~header !err_ft strm) () + | Error -> msg ~header:("Error", error_tag) !err_ft strm + in + let () = set_logger logger in + () diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli new file mode 100644 index 00000000..f5d6184c --- /dev/null +++ b/printing/ppstyle.mli @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string list -> t +(** Create a new tag with the given name. Each name must be unique. The optional + style is taken as the default one. *) + +val repr : t -> string list +(** Gives back the original name of the style tag where each string has been + concatenated and separated with a dot. *) + +val tag : t Pp.Tag.key +(** An annotation for styles *) + +(** {5 Manipulating global styles} *) + +val get_style : t -> Terminal.style option +(** Get the style associated to a tag. *) + +val set_style : t -> Terminal.style option -> unit +(** Set a style associated to a tag. *) + +val clear_styles : unit -> unit +(** Clear all styles. *) + +val parse_config : string -> unit +(** Add all styles from the given string as parsed by {!Terminal.parse}. + Unregistered tags are ignored. *) + +val dump : unit -> (t * Terminal.style option) list +(** Recover the list of known tags together with their current style. *) + +(** {5 Setting color output} *) + +val init_color_output : unit -> unit +(** Once called, all tags defined here will use their current style when + printed. To this end, this function redefines the loggers used when sending + messages to the user. The program will in particular use the formatters + {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages, + with additional syle information provided by this module. Be careful this is + not compatible with the Emacs mode! *) + +val pp_tag : Pp.tag_handler +(** Returns the name of a style tag that is understandable by the formatters + that have been inititialized through {!init_color_output}. To be used with + {!Pp.pp_with}. *) + +(** {5 Tags} *) + +val error_tag : t +(** Tag used by the {!Pp.msg_error} function. *) + +val warning_tag : t +(** Tag used by the {!Pp.msg_warning} function. *) + +val debug_tag : t +(** Tag used by the {!Pp.msg_debug} function. *) diff --git a/printing/pptactic.ml b/printing/pptactic.ml new file mode 100644 index 00000000..f8264e5a --- /dev/null +++ b/printing/pptactic.ml @@ -0,0 +1,1499 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + (tolerability -> raw_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +type 'a glob_extra_genarg_printer = + (glob_constr_and_expr -> std_ppcmds) -> + (glob_constr_and_expr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +type 'a extra_genarg_printer = + (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +let genarg_pprule = ref String.Map.empty + +let declare_extra_genarg_pprule wit f g h = + let s = match unquote (topwit wit) with + | ExtraArgType s -> s + | _ -> error + "Can declare a pretty-printing rule only for extra argument types." + in + let f prc prlc prtac x = f prc prlc prtac (out_gen (rawwit wit) x) in + let g prc prlc prtac x = g prc prlc prtac (out_gen (glbwit wit) x) in + let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in + genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule + +module Make + (Ppconstr : Ppconstrsig.Pp) + (Taggers : sig + val tag_keyword + : std_ppcmds -> std_ppcmds + val tag_primitive + : std_ppcmds -> std_ppcmds + val tag_string + : std_ppcmds -> std_ppcmds + val tag_glob_tactic_expr + : glob_tactic_expr -> std_ppcmds -> std_ppcmds + val tag_glob_atomic_tactic_expr + : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds + val tag_raw_tactic_expr + : raw_tactic_expr -> std_ppcmds -> std_ppcmds + val tag_raw_atomic_tactic_expr + : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds + val tag_tactic_expr + : tactic_expr -> std_ppcmds -> std_ppcmds + val tag_atomic_tactic_expr + : atomic_tactic_expr -> std_ppcmds -> std_ppcmds + end) += struct + + open Taggers + + let keyword x = tag_keyword (str x) + let primitive x = tag_primitive (str x) + + let pr_with_occurrences pr (occs,c) = + match occs with + | AllOccurrences -> + pr c + | NoOccurrences -> + failwith "pr_with_occurrences: no occurrences" + | OnlyOccurrences nl -> + hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + | AllOccurrencesBut nl -> + hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + + exception ComplexRedFlag + + let pr_short_red_flag pr r = + if not r.rBeta || not r.rIota || not r.rZeta then raise ComplexRedFlag + else if List.is_empty r.rConst then + if r.rDelta then mt () else raise ComplexRedFlag + else (if r.rDelta then str "-" else mt ()) ++ + hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]") + + let pr_red_flag pr r = + try pr_short_red_flag pr r + with complexRedFlags -> + (if r.rBeta then pr_arg str "beta" else mt ()) ++ + (if r.rIota then pr_arg str "iota" else mt ()) ++ + (if r.rZeta then pr_arg str "zeta" else mt ()) ++ + (if List.is_empty r.rConst then + if r.rDelta then pr_arg str "delta" + else mt () + else + pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ + hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) + + let pr_union pr1 pr2 = function + | Inl a -> pr1 a + | Inr b -> pr2 b + + let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function + | Red false -> keyword "red" + | Hnf -> keyword "hnf" + | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) + ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o + | Cbv f -> + if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then + keyword "compute" + else + hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) + | Lazy f -> + hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f) + | Cbn f -> + hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f) + | Unfold l -> + hov 1 (keyword "unfold" ++ spc() ++ + prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l) + | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l) + | Pattern l -> + hov 1 (keyword "pattern" ++ + pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l) + + | Red true -> + error "Shouldn't be accessible from user." + | ExtraRedExpr s -> + str s + | CbvVm o -> + keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o + | CbvNative o -> + keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o + + let pr_may_eval test prc prlc pr2 pr3 = function + | ConstrEval (r,c) -> + hov 0 + (keyword "eval" ++ brk (1,1) ++ + pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++ + keyword "in" ++ spc() ++ prc c) + | ConstrContext ((_,id),c) -> + hov 0 + (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ + str "[" ++ prlc c ++ str "]") + | ConstrTypeOf c -> + hov 1 (keyword "type of" ++ spc() ++ prc c) + | ConstrTerm c when test c -> + h 0 (str "(" ++ prc c ++ str ")") + | ConstrTerm c -> + prc c + + let pr_may_eval a = + pr_may_eval (fun _ -> false) a + + let pr_arg pr x = spc () ++ pr x + + let pr_or_var pr = function + | ArgArg x -> pr x + | ArgVar (_,s) -> pr_id s + + let pr_and_short_name pr (c,_) = pr c + + let pr_or_by_notation f = function + | AN v -> f v + | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + + let pr_located pr (loc,x) = pr x + + let pr_evaluable_reference = function + | EvalVarRef id -> pr_id id + | EvalConstRef sp -> pr_global (Globnames.ConstRef sp) + + let pr_quantified_hypothesis = function + | AnonHyp n -> int n + | NamedHyp id -> pr_id id + + let pr_binding prc = function + | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + + let pr_bindings prc prlc = function + | ImplicitBindings l -> + brk (1,1) ++ keyword "with" ++ brk (1,1) ++ + hv 0 (prlist_with_sep spc prc l) + | ExplicitBindings l -> + brk (1,1) ++ keyword "with" ++ brk (1,1) ++ + hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l) + | NoBindings -> mt () + + let pr_bindings_no_with prc prlc = function + | ImplicitBindings l -> + brk (0,1) ++ + prlist_with_sep spc prc l + | ExplicitBindings l -> + brk (0,1) ++ + prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + | NoBindings -> mt () + + let pr_clear_flag clear_flag pp x = + (match clear_flag with Some false -> str "!" | Some true -> str ">" | None -> mt()) + ++ pp x + + let pr_with_bindings prc prlc (c,bl) = + prc c ++ pr_bindings prc prlc bl + + let pr_with_bindings_arg prc prlc (clear_flag,c) = + pr_clear_flag clear_flag (pr_with_bindings prc prlc) c + + let pr_with_constr prc = function + | None -> mt () + | Some c -> spc () ++ hov 1 (keyword "with" ++ spc () ++ prc c) + + let pr_message_token prid = function + | MsgString s -> tag_string (qs s) + | MsgInt n -> int n + | MsgIdent id -> prid id + + let pr_fresh_ids = + prlist (fun s -> spc() ++ pr_or_var (fun s -> tag_string (qs s)) s) + + let with_evars ev s = if ev then "e" ^ s else s + + + let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = + match Genarg.genarg_tag x with + | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x) + | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x) + | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) + | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x) + | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) + | ConstrMayEvalArgType -> + pr_may_eval prc prlc (pr_or_by_notation prref) prpat + (out_gen (rawwit wit_constr_may_eval) x) + | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x) + | RedExprArgType -> + pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat) + (out_gen (rawwit wit_red_expr) x) + | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) + | ConstrWithBindingsArgType -> + pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x) + | BindingsArgType -> + pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x) + | ListArgType _ -> + let list_unpacker wit l = + let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in + pr_sequence map (raw l) + in + hov 0 (list_unpack { list_unpacker } x) + | OptArgType _ -> + let opt_unpacker wit o = match raw o with + | None -> mt () + | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) + in + hov 0 (opt_unpack { opt_unpacker } x) + | PairArgType _ -> + let pair_unpacker wit1 wit2 o = + let p, q = raw o in + let p = in_gen (rawwit wit1) p in + let q = in_gen (rawwit wit2) q in + pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q] + in + hov 0 (pair_unpack { pair_unpacker } x) + | ExtraArgType s -> + try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x + with Not_found -> Genprint.generic_raw_print x + + + let rec pr_glb_generic prc prlc prtac prpat x = + match Genarg.genarg_tag x with + | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x) + | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x) + | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) + | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x) + | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) + | ConstrMayEvalArgType -> + pr_may_eval prc prlc + (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat + (out_gen (glbwit wit_constr_may_eval) x) + | QuantHypArgType -> + pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x) + | RedExprArgType -> + pr_red_expr + (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat) + (out_gen (glbwit wit_red_expr) x) + | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) + | ConstrWithBindingsArgType -> + pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x) + | BindingsArgType -> + pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x) + | ListArgType _ -> + let list_unpacker wit l = + let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in + pr_sequence map (glb l) + in + hov 0 (list_unpack { list_unpacker } x) + | OptArgType _ -> + let opt_unpacker wit o = match glb o with + | None -> mt () + | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) + in + hov 0 (opt_unpack { opt_unpacker } x) + | PairArgType _ -> + let pair_unpacker wit1 wit2 o = + let p, q = glb o in + let p = in_gen (glbwit wit1) p in + let q = in_gen (glbwit wit2) q in + pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q] + in + hov 0 (pair_unpack { pair_unpacker } x) + | ExtraArgType s -> + try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x + with Not_found -> Genprint.generic_glb_print x + + let rec pr_top_generic prc prlc prtac prpat x = + match Genarg.genarg_tag x with + | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x) + | IdentArgType -> pr_id (out_gen (topwit wit_ident) x) + | VarArgType -> pr_id (out_gen (topwit wit_var) x) + | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x) + | ConstrArgType -> prc (out_gen (topwit wit_constr) x) + | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x) + | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x) + | RedExprArgType -> + pr_red_expr (prc,prlc,pr_evaluable_reference,prpat) + (out_gen (topwit wit_red_expr) x) + | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) + | ConstrWithBindingsArgType -> + let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in + pr_with_bindings prc prlc (c,b) + | BindingsArgType -> + pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it + | ListArgType _ -> + let list_unpacker wit l = + let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in + pr_sequence map (top l) + in + hov 0 (list_unpack { list_unpacker } x) + | OptArgType _ -> + let opt_unpacker wit o = match top o with + | None -> mt () + | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) + in + hov 0 (opt_unpack { opt_unpacker } x) + | PairArgType _ -> + let pair_unpacker wit1 wit2 o = + let p, q = top o in + let p = in_gen (topwit wit1) p in + let q = in_gen (topwit wit2) q in + pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q] + in + hov 0 (pair_unpack { pair_unpacker } x) + | ExtraArgType s -> + try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x + with Not_found -> Genprint.generic_top_print x + + let rec tacarg_using_rule_token pr_gen = function + | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) + | None :: l, a :: al -> + let r = tacarg_using_rule_token pr_gen (l,al) in + pr_gen a :: r + | [], [] -> [] + | _ -> failwith "Inconsistent arguments of extended tactic" + + let pr_tacarg_using_rule pr_gen l = + let l = match l with + | (Some s :: l, al) -> + (** First terminal token should be considered as the name of the tactic, + so we tag it differently than the other terminal tokens. *) + primitive s :: (tacarg_using_rule_token pr_gen (l, al)) + | _ -> tacarg_using_rule_token pr_gen l + in + pr_sequence (fun x -> x) l + + let pr_extend_gen pr_gen lev s l = + try + let tags = List.map genarg_tag l in + let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in + let p = pr_tacarg_using_rule pr_gen (pl,l) in + if lev' > lev then surround p else p + with Not_found -> + let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in + let args = match l with + | [] -> mt () + | _ -> spc() ++ pr_sequence pr_gen l + in + str "<" ++ name ++ str ">" ++ args + + let pr_alias_gen pr_gen lev key l = + try + let pp = KNmap.find key !prnotation_tab in + let (lev', pl) = pp.pptac_prods in + let p = pr_tacarg_using_rule pr_gen (pl, l) in + if lev' > lev then surround p else p + with Not_found -> + KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" + + let pr_raw_extend prc prlc prtac prpat = + pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference) + let pr_glob_extend prc prlc prtac prpat = + pr_extend_gen (pr_glb_generic prc prlc prtac prpat) + let pr_extend prc prlc prtac prpat = + pr_extend_gen (pr_top_generic prc prlc prtac prpat) + + let pr_raw_alias prc prlc prtac prpat = + pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference) + let pr_glob_alias prc prlc prtac prpat = + pr_alias_gen (pr_glb_generic prc prlc prtac prpat) + let pr_alias prc prlc prtac prpat = + pr_alias_gen (pr_top_generic prc prlc prtac prpat) + + (**********************************************************************) + (* The tactic printer *) + + let strip_prod_binders_expr n ty = + let rec strip_ty acc n ty = + match ty with + Constrexpr.CProdN(_,bll,a) -> + let nb = + List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in + let bll = List.map (fun (x, _, y) -> x, y) bll in + if nb >= n then (List.rev (bll@acc)), a + else strip_ty (bll@acc) (n-nb) a + | _ -> error "Cannot translate fix tactic: not enough products" in + strip_ty [] n ty + + let pr_ltac_or_var pr = function + | ArgArg x -> pr x + | ArgVar (loc,id) -> pr_with_comments loc (pr_id id) + + let pr_ltac_constant kn = + if !Flags.in_debugger then pr_kn kn + else try + pr_qualid (Nametab.shortest_qualid_of_tactic kn) + with Not_found -> (* local tactic not accessible anymore *) + str "<" ++ pr_kn kn ++ str ">" + + let pr_evaluable_reference_env env = function + | EvalVarRef id -> pr_id id + | EvalConstRef sp -> + Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp) + + let pr_esubst prc l = + let pr_qhyp = function + (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" + | (_,NamedHyp id,c) -> + str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" + in + prlist_with_sep spc pr_qhyp l + + let pr_bindings_gen for_ex prc prlc = function + | ImplicitBindings l -> + spc () ++ + hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ + prlist_with_sep spc prc l) + | ExplicitBindings l -> + spc () ++ + hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ + pr_esubst prlc l) + | NoBindings -> mt () + + let pr_bindings prc prlc = pr_bindings_gen false prc prlc + + let pr_with_bindings prc prlc (c,bl) = + hov 1 (prc c ++ pr_bindings prc prlc bl) + + let pr_as_disjunctive_ipat prc ipatl = + keyword "as" ++ spc () ++ + pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl + + let pr_eqn_ipat (_,ipat) = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat + + let pr_with_induction_names prc = function + | None, None -> mt () + | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat) + | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat) + | Some eqpat, Some ipat -> + spc () ++ + hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat) + + let pr_as_intro_pattern prc ipat = + spc () ++ hov 1 (keyword "as" ++ spc () ++ Miscprint.pr_intro_pattern prc ipat) + + let pr_with_inversion_names prc = function + | None -> mt () + | Some ipat -> pr_as_disjunctive_ipat prc ipat + + let pr_as_ipat prc = function + | None -> mt () + | Some ipat -> pr_as_intro_pattern prc ipat + + let pr_as_name = function + | Anonymous -> mt () + | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.ghost,id) + + let pr_pose_as_style prc na c = + spc() ++ prc c ++ pr_as_name na + + let pr_pose prc prlc na c = match na with + | Anonymous -> spc() ++ prc c + | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c) + + let pr_assertion prc prdc _prlc ipat c = match ipat with + (* Use this "optimisation" or use only the general case ? + | IntroIdentifier id -> + spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c) + *) + | ipat -> + spc() ++ prc c ++ pr_as_ipat prdc ipat + + let pr_assumption prc prdc prlc ipat c = match ipat with + (* Use this "optimisation" or use only the general case ?*) + (* it seems that this "optimisation" is somehow more natural *) + | Some (_,IntroNaming (IntroIdentifier id)) -> + spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c) + | ipat -> + spc() ++ prc c ++ pr_as_ipat prdc ipat + + let pr_by_tactic prt = function + | TacId [] -> mt () + | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac + + let pr_hyp_location pr_id = function + | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs + | occs, InHypTypeOnly -> + spc () ++ pr_with_occurrences (fun id -> + str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")" + ) occs + | occs, InHypValueOnly -> + spc () ++ pr_with_occurrences (fun id -> + str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")" + ) occs + + let pr_in pp = spc () ++ hov 0 (keyword "in" ++ pp) + + let pr_simple_hyp_clause pr_id = function + | [] -> mt () + | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l) + + let pr_in_hyp_as prc pr_id = function + | None -> mt () + | Some (clear,id,ipat) -> + pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat + + let pr_clauses default_is_concl pr_id = function + | { onhyps=Some []; concl_occs=occs } + when (match default_is_concl with Some true -> true | _ -> false) -> + pr_with_occurrences mt (occs,()) + | { onhyps=None; concl_occs=AllOccurrences } + when (match default_is_concl with Some false -> true | _ -> false) -> mt () + | { onhyps=None; concl_occs=NoOccurrences } -> + pr_in (str " * |-") + | { onhyps=None; concl_occs=occs } -> + pr_in (pr_with_occurrences (fun () -> str " *") (occs,())) + | { onhyps=Some l; concl_occs=occs } -> + let pr_occs = match occs with + | NoOccurrences -> mt () + | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,()) + in + pr_in + (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ pr_occs) + + let pr_orient b = if b then mt () else str "<- " + + let pr_multi = function + | Precisely 1 -> mt () + | Precisely n -> int n ++ str "!" + | UpTo n -> int n ++ str "?" + | RepeatStar -> str "?" + | RepeatPlus -> str "!" + + let pr_induction_arg prc prlc = function + | ElimOnConstr c -> pr_with_bindings prc prlc c + | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) + | ElimOnAnonHyp n -> int n + + let pr_induction_kind = function + | SimpleInversion -> primitive "simple inversion" + | FullInversion -> primitive "inversion" + | FullInversionClear -> primitive "inversion_clear" + + let pr_lazy = function + | General -> keyword "multi" + | Select -> keyword "lazy" + | Once -> mt () + + let pr_match_pattern pr_pat = function + | Term a -> pr_pat a + | Subterm (b,None,a) -> + (** ppedrot: we don't make difference between [appcontext] and [context] + anymore, and the interpretation is governed by a flag instead. *) + keyword "context" ++ str" [" ++ pr_pat a ++ str "]" + | Subterm (b,Some id,a) -> + keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]" + + let pr_match_hyps pr_pat = function + | Hyp (nal,mp) -> + pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp + | Def (nal,mv,mp) -> + pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv + ++ str ":" ++ pr_match_pattern pr_pat mp + + let pr_match_rule m pr pr_pat = function + | Pat ([],mp,t) when m -> + pr_match_pattern pr_pat mp ++ + spc () ++ str "=>" ++ brk (1,4) ++ pr t + (* + | Pat (rl,mp,t) -> + hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl ++ + (if rl <> [] then spc () else mt ()) ++ + hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ + str "=>" ++ brk (1,4) ++ pr t)) + *) + | Pat (rl,mp,t) -> + hov 0 ( + hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++ + (if not (List.is_empty rl) then spc () else mt ()) ++ + hov 0 ( + str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ + str "=>" ++ brk (1,4) ++ pr t)) + | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t + + let pr_funvar = function + | None -> spc () ++ str "_" + | Some id -> spc () ++ pr_id id + + let pr_let_clause k pr (id,(bl,t)) = + hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ + str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t))) + + let pr_let_clauses recflag pr = function + | hd::tl -> + hv 0 + (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ + prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) + | [] -> anomaly (Pp.str "LetIn must declare at least one binding") + + let pr_seq_body pr tl = + hv 0 (str "[ " ++ + prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++ + str " ]") + + let pr_dispatch pr tl = + hv 0 (str "[>" ++ + prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++ + str " ]") + + let pr_opt_tactic pr = function + | TacId [] -> mt () + | t -> pr t + + let pr_tac_extend_gen pr tf tm tl = + prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++ + pr_opt_tactic pr tm ++ str ".." ++ + prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl + + let pr_then_gen pr tf tm tl = + hv 0 (str "[ " ++ + pr_tac_extend_gen pr tf tm tl ++ + str " ]") + + let pr_tac_extend pr tf tm tl = + hv 0 (str "[>" ++ + pr_tac_extend_gen pr tf tm tl ++ + str " ]") + + let pr_hintbases = function + | None -> spc () ++ keyword "with" ++ str" *" + | Some [] -> mt () + | Some l -> + spc () ++ hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l) + + let pr_auto_using prc = function + | [] -> mt () + | l -> spc () ++ + hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l) + + let string_of_debug = function + | Off -> "" + | Debug -> "debug " + | Info -> "info_" + + let pr_then () = str ";" + + let ltop = (5,E) + let lseq = 4 + let ltactical = 3 + let lorelse = 2 + let llet = 5 + let lfun = 5 + let lcomplete = 1 + let labstract = 3 + let lmatch = 1 + let latom = 0 + let lcall = 1 + let leval = 1 + let ltatom = 1 + let linfo = 5 + + let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq + + (** A printer for tactics that polymorphically works on the three + "raw", "glob" and "typed" levels *) + + type 'a printer = { + pr_tactic : tolerability -> 'tacexpr -> std_ppcmds; + pr_constr : 'trm -> std_ppcmds; + pr_uconstr : 'utrm -> std_ppcmds; + pr_lconstr : 'trm -> std_ppcmds; + pr_dconstr : 'dtrm -> std_ppcmds; + pr_pattern : 'pat -> std_ppcmds; + pr_lpattern : 'pat -> std_ppcmds; + pr_constant : 'cst -> std_ppcmds; + pr_reference : 'ref -> std_ppcmds; + pr_name : 'nam -> std_ppcmds; + pr_generic : 'lev generic_argument -> std_ppcmds; + pr_extend : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds; + pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds; + } + + constraint 'a = < + term :'trm; + utrm :'utrm; + dterm :'dtrm; + pattern :'pat; + constant :'cst; + reference :'ref; + name :'nam; + tacexpr :'tacexpr; + level :'lev + > + + let make_pr_tac pr strip_prod_binders tag_atom tag = + + (* some shortcuts *) + let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in + let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in + let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in + let pr_with_bindings_arg_full = pr_with_bindings_arg in + let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in + let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in + + let pr_constrarg c = spc () ++ pr.pr_constr c in + let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in + let pr_intarg n = spc () ++ int n in + + (* Some printing combinators *) + let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in + + let extract_binders = function + | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body) + | body -> ([],body) in + + let pr_binder_fix (nal,t) = + (* match t with + | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal + | _ ->*) + let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + spc() ++ hov 1 (str"(" ++ s ++ str")") in + + let pr_fix_tac (id,n,c) = + let rec set_nth_name avoid n = function + (nal,ty)::bll -> + if n <= List.length nal then + match List.chop (n-1) nal with + _, (_,Name id) :: _ -> id, (nal,ty)::bll + | bef, (loc,Anonymous) :: aft -> + let id = next_ident_away (Id.of_string"y") avoid in + id, ((bef@(loc,Name id)::aft, ty)::bll) + | _ -> assert false + else + let (id,bll') = set_nth_name avoid (n-List.length nal) bll in + (id,(nal,ty)::bll') + | [] -> assert false in + let (bll,ty) = strip_prod_binders n c in + let names = + List.fold_left + (fun ln (nal,_) -> List.fold_left + (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) + ln nal) + [] bll in + let idarg,bll = set_nth_name names n bll in + let annot = match names with + | [_] -> + mt () + | _ -> + spc() ++ str"{" + ++ keyword "struct" ++ spc () + ++ pr_id idarg ++ str"}" + in + hov 1 (str"(" ++ pr_id id ++ + prlist pr_binder_fix bll ++ annot ++ str" :" ++ + pr_lconstrarg ty ++ str")") in + (* spc() ++ + hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg + c) + *) + let pr_cofix_tac (id,c) = + hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in + + (* Printing tactics as arguments *) + let rec pr_atom0 a = tag_atom a (match a with + | TacIntroPattern [] -> primitive "intros" + | TacIntroMove (None,MoveLast) -> primitive "intro" + | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial" + | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto" + | TacClear (true,[]) -> primitive "clear" + | t -> str "(" ++ pr_atom1 t ++ str ")" + ) + + (* Main tactic printer *) + and pr_atom1 a = tag_atom a (match a with + (* Basic tactics *) + | TacIntroPattern [] as t -> + pr_atom0 t + | TacIntroPattern (_::_ as p) -> + hov 1 (primitive "intros" ++ spc () ++ + prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) + | TacIntroMove (None,MoveLast) as t -> + pr_atom0 t + | TacIntroMove (Some id,MoveLast) -> + primitive "intro" ++ spc () ++ pr_id id + | TacIntroMove (ido,hto) -> + hov 1 (primitive "intro" ++ pr_opt pr_id ido ++ + Miscprint.pr_move_location pr.pr_name hto) + | TacExact c -> + hov 1 (primitive "exact" ++ pr_constrarg c) + | TacApply (a,ev,cb,inhyp) -> + hov 1 ( + (if a then mt() else primitive "simple ") ++ + primitive (with_evars ev "apply") ++ spc () ++ + prlist_with_sep pr_comma pr_with_bindings_arg cb ++ + pr_in_hyp_as pr.pr_dconstr pr.pr_name inhyp + ) + | TacElim (ev,cb,cbo) -> + hov 1 ( + primitive (with_evars ev "elim") + ++ pr_arg pr_with_bindings_arg cb + ++ pr_opt pr_eliminator cbo) + | TacCase (ev,cb) -> + hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb) + | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n) + | TacMutualFix (id,n,l) -> + hov 1 ( + primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() + ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l) + | TacCofix ido -> + hov 1 (primitive "cofix" ++ pr_opt pr_id ido) + | TacMutualCofix (id,l) -> + hov 1 ( + primitive "cofix" ++ spc () ++ pr_id id ++ spc() + ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l + ) + | TacAssert (b,Some tac,ipat,c) -> + hov 1 ( + primitive (if b then "assert" else "enough") ++ + pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ + pr_by_tactic (pr.pr_tactic ltop) tac + ) + | TacAssert (_,None,ipat,c) -> + hov 1 ( + primitive "pose proof" + ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c + ) + | TacGeneralize l -> + hov 1 ( + primitive "generalize" ++ spc () + ++ prlist_with_sep pr_comma (fun (cl,na) -> + pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) + l + ) + | TacGeneralizeDep c -> + hov 1 ( + primitive "generalize" ++ spc () ++ str "dependent" + ++ pr_constrarg c + ) + | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> + hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) + | TacLetTac (na,c,cl,b,e) -> + hov 1 ( + (if b then primitive "set" else primitive "remember") ++ + (if b then pr_pose pr.pr_constr pr.pr_lconstr na c + else pr_pose_as_style pr.pr_constr na c) ++ + pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ + pr_clauses (Some b) pr.pr_name cl) + (* | TacInstantiate (n,c,ConclLocation ()) -> + hov 1 (str "instantiate" ++ spc() ++ + hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ + pr_lconstrarg c ++ str ")" )) + | TacInstantiate (n,c,HypLocation (id,hloc)) -> + hov 1 (str "instantiate" ++ spc() ++ + hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ + pr_lconstrarg c ++ str ")" ) + ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None))) + *) + + (* Derived basic tactics *) + | TacInductionDestruct (isrec,ev,(l,el)) -> + hov 1 ( + primitive (with_evars ev (if isrec then "induction" else "destruct")) + ++ spc () + ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) -> + pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++ + pr_with_induction_names pr.pr_dconstr ids ++ + pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++ + pr_opt pr_eliminator el + ) + | TacDoubleInduction (h1,h2) -> + hov 1 ( + primitive "double induction" + ++ pr_arg pr_quantified_hypothesis h1 + ++ pr_arg pr_quantified_hypothesis h2 + ) + + (* Automation tactics *) + | TacTrivial (_,[],Some []) as x -> + pr_atom0 x + | TacTrivial (d,lems,db) -> + hov 0 ( + str (string_of_debug d) ++ primitive "trivial" + ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db + ) + | TacAuto (_,None,[],Some []) as x -> + pr_atom0 x + | TacAuto (d,n,lems,db) -> + hov 0 ( + str (string_of_debug d) ++ primitive "auto" + ++ pr_opt (pr_or_var int) n + ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db + ) + + (* Context management *) + | TacClear (true,[]) as t -> + pr_atom0 t + | TacClear (keep,l) -> + hov 1 ( + primitive "clear" ++ spc () + ++ (if keep then str "- " else mt ()) + ++ prlist_with_sep spc pr.pr_name l + ) + | TacClearBody l -> + hov 1 ( + primitive "clearbody" ++ spc () + ++ prlist_with_sep spc pr.pr_name l + ) + | TacMove (id1,id2) -> + hov 1 ( + primitive "move" + ++ brk (1,1) ++ pr.pr_name id1 + ++ Miscprint.pr_move_location pr.pr_name id2 + ) + | TacRename l -> + hov 1 ( + primitive "rename" ++ brk (1,1) + ++ prlist_with_sep + (fun () -> str "," ++ brk (1,1)) + (fun (i1,i2) -> + pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2) + l + ) + + (* Constructors *) + | TacSplit (ev,l) -> + hov 1 ( + primitive (with_evars ev "exists") + ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l + ) + + (* Conversion *) + | TacReduce (r,h) -> + hov 1 ( + pr_red_expr r + ++ pr_clauses (Some true) pr.pr_name h + ) + | TacChange (op,c,h) -> + hov 1 ( + primitive "change" ++ brk (1,1) + ++ ( + match op with + None -> + mt () + | Some p -> + pr.pr_pattern p ++ spc () + ++ keyword "with" ++ spc () + ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h + ) + + (* Equivalence relations *) + | TacSymmetry cls -> + primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls + + (* Equality and inversion *) + | TacRewrite (ev,l,cl,by) -> + hov 1 ( + primitive (with_evars ev "rewrite") ++ spc () + ++ prlist_with_sep + (fun () -> str ","++spc()) + (fun (b,m,c) -> + pr_orient b ++ pr_multi m ++ + pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c) + l + ++ pr_clauses (Some true) pr.pr_name cl + ++ ( + match by with + | Some by -> pr_by_tactic (pr.pr_tactic ltop) by + | None -> mt() + ) + ) + | TacInversion (DepInversion (k,c,ids),hyp) -> + hov 1 ( + primitive "dependent " ++ pr_induction_kind k ++ spc () + ++ pr_quantified_hypothesis hyp + ++ pr_with_inversion_names pr.pr_dconstr ids + ++ pr_with_constr pr.pr_constr c + ) + | TacInversion (NonDepInversion (k,cl,ids),hyp) -> + hov 1 ( + pr_induction_kind k ++ spc () + ++ pr_quantified_hypothesis hyp + ++ pr_with_inversion_names pr.pr_dconstr ids + ++ pr_simple_hyp_clause pr.pr_name cl + ) + | TacInversion (InversionUsing (c,cl),hyp) -> + hov 1 ( + primitive "inversion" ++ spc() + ++ pr_quantified_hypothesis hyp ++ spc () + ++ keyword "using" ++ spc () ++ pr.pr_constr c + ++ pr_simple_hyp_clause pr.pr_name cl + ) + ) + in + + let rec pr_tac inherited tac = + let return (doc, l) = (tag tac doc, l) in + let (strm, prec) = return (match tac with + | TacAbstract (t,None) -> + keyword "abstract " ++ pr_tac (labstract,L) t, labstract + | TacAbstract (t,Some s) -> + hov 0 ( + keyword "abstract" + ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () + ++ keyword "using" ++ spc () ++ pr_id s), + labstract + | TacLetIn (recflag,llc,u) -> + let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in + v 0 + (hv 0 ( + pr_let_clauses recflag (pr_tac ltop) llc + ++ spc () ++ keyword "in" + ) ++ fnl () ++ pr_tac (llet,E) u), + llet + | TacMatch (lz,t,lrul) -> + hov 0 ( + pr_lazy lz ++ keyword "match" ++ spc () + ++ pr_tac ltop t ++ spc () ++ keyword "with" + ++ prlist (fun r -> + fnl () ++ str "| " + ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r + ) lrul + ++ fnl() ++ keyword "end"), + lmatch + | TacMatchGoal (lz,lr,lrul) -> + hov 0 ( + pr_lazy lz + ++ keyword (if lr then "match reverse goal with" else "match goal with") + ++ prlist (fun r -> + fnl () ++ str "| " + ++ pr_match_rule false (pr_tac ltop) pr.pr_lpattern r + ) lrul ++ fnl() ++ keyword "end"), + lmatch + | TacFun (lvar,body) -> + hov 2 ( + keyword "fun" + ++ prlist pr_funvar lvar ++ str " =>" ++ spc () + ++ pr_tac (lfun,E) body), + lfun + | TacThens (t,tl) -> + hov 1 ( + pr_tac (lseq,E) t ++ pr_then () ++ spc () + ++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl), + lseq + | TacThen (t1,t2) -> + hov 1 ( + pr_tac (lseq,E) t1 ++ pr_then () ++ spc () + ++ pr_tac (lseq,L) t2), + lseq + | TacDispatch tl -> + pr_dispatch (pr_tac ltop) tl, lseq + | TacExtendTac (tf,t,tr) -> + pr_tac_extend (pr_tac ltop) tf t tr , lseq + | TacThens3parts (t1,tf,t2,tl) -> + hov 1 ( + pr_tac (lseq,E) t1 ++ pr_then () ++ spc () + ++ pr_then_gen (pr_tac ltop) tf t2 tl), + lseq + | TacTry t -> + hov 1 ( + keyword "try" ++ spc () ++ pr_tac (ltactical,E) t), + ltactical + | TacDo (n,t) -> + hov 1 ( + str "do" ++ spc () + ++ pr_or_var int n ++ spc () + ++ pr_tac (ltactical,E) t), + ltactical + | TacTimeout (n,t) -> + hov 1 ( + keyword "timeout " + ++ pr_or_var int n ++ spc () + ++ pr_tac (ltactical,E) t), + ltactical + | TacTime (s,t) -> + hov 1 ( + keyword "time" + ++ pr_opt str s ++ spc () + ++ pr_tac (ltactical,E) t), + ltactical + | TacRepeat t -> + hov 1 ( + keyword "repeat" ++ spc () + ++ pr_tac (ltactical,E) t), + ltactical + | TacProgress t -> + hov 1 ( + keyword "progress" ++ spc () + ++ pr_tac (ltactical,E) t), + ltactical + | TacShowHyps t -> + hov 1 ( + keyword "infoH" ++ spc () + ++ pr_tac (ltactical,E) t), + ltactical + | TacInfo t -> + hov 1 ( + keyword "info" ++ spc () + ++ pr_tac (ltactical,E) t), + linfo + | TacOr (t1,t2) -> + hov 1 ( + pr_tac (lorelse,L) t1 ++ spc () + ++ str "+" ++ brk (1,1) + ++ pr_tac (lorelse,E) t2), + lorelse + | TacOnce t -> + hov 1 ( + keyword "once" ++ spc () + ++ pr_tac (ltactical,E) t), + ltactical + | TacExactlyOnce t -> + hov 1 ( + keyword "exactly_once" ++ spc () + ++ pr_tac (ltactical,E) t), + ltactical + | TacIfThenCatch (t,tt,te) -> + hov 1 ( + str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++ + str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++ + str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)), + ltactical + | TacOrelse (t1,t2) -> + hov 1 ( + pr_tac (lorelse,L) t1 ++ spc () + ++ str "||" ++ brk (1,1) + ++ pr_tac (lorelse,E) t2), + lorelse + | TacFail (g,n,l) -> + let arg = + match n with + | ArgArg 0 -> mt () + | _ -> pr_arg (pr_or_var int) n + in + let name = + match g with + | TacGlobal -> keyword "gfail" + | TacLocal -> keyword "fail" + in + hov 1 ( + name ++ arg + ++ prlist (pr_arg (pr_message_token pr.pr_name)) l), + latom + | TacFirst tl -> + keyword "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet + | TacSolve tl -> + keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet + | TacComplete t -> + pr_tac (lcomplete,E) t, lcomplete + | TacId l -> + keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom + | TacAtom (loc,t) -> + pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom + | TacArg(_,Tacexp e) -> + pr.pr_tactic (latom,E) e, latom + | TacArg(_,ConstrMayEval (ConstrTerm c)) -> + keyword "constr:" ++ pr.pr_constr c, latom + | TacArg(_,ConstrMayEval c) -> + pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval + | TacArg(_,TacFreshId l) -> + primitive "fresh" ++ pr_fresh_ids l, latom + | TacArg(_,TacGeneric arg) -> + pr.pr_generic arg, latom + | TacArg(_,TacCall(loc,f,[])) -> + pr.pr_reference f, latom + | TacArg(_,TacCall(loc,f,l)) -> + pr_with_comments loc (hov 1 ( + pr.pr_reference f ++ spc () + ++ prlist_with_sep spc pr_tacarg l)), + lcall + | TacArg (_,a) -> + pr_tacarg a, latom + | TacML (loc,s,l) -> + pr_with_comments loc (pr.pr_extend 1 s l), lcall + | TacAlias (loc,kn,l) -> + pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom + ) + in + if prec_less prec inherited then strm + else str"(" ++ strm ++ str")" + + and pr_tacarg = function + | TacDynamic (loc,t) -> + pr_with_comments loc ( + str "<" ++ keyword "dynamic" ++ str (" [" ^ (Dyn.tag t)^"]>") + ) + | MetaIdArg (loc,true,s) -> + pr_with_comments loc (str ("$" ^ s)) + | MetaIdArg (loc,false,s) -> + pr_with_comments loc (keyword "constr:" ++ str(" $" ^ s)) + | Reference r -> + pr.pr_reference r + | ConstrMayEval c -> + pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c + | UConstr c -> + keyword "uconstr:" ++ pr.pr_uconstr c + | TacFreshId l -> + keyword "fresh" ++ pr_fresh_ids l + | TacPretype c -> + keyword "type_term" ++ pr.pr_constr c + | TacNumgoals -> + keyword "numgoals" + | (TacCall _|Tacexp _ | TacGeneric _) as a -> + keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a)) + + in pr_tac + + let strip_prod_binders_glob_constr n (ty,_) = + let rec strip_ty acc n ty = + if Int.equal n 0 then (List.rev acc, (ty,None)) else + match ty with + Glob_term.GProd(loc,na,Explicit,a,b) -> + strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b + | _ -> error "Cannot translate fix tactic: not enough products" in + strip_ty [] n ty + + let raw_printers = + (strip_prod_binders_expr) + + let rec pr_raw_tactic_level n (t:raw_tactic_expr) = + let pr = { + pr_tactic = pr_raw_tactic_level; + pr_constr = pr_constr_expr; + pr_uconstr = pr_constr_expr; + pr_dconstr = pr_constr_expr; + pr_lconstr = pr_lconstr_expr; + pr_pattern = pr_constr_pattern_expr; + pr_lpattern = pr_lconstr_pattern_expr; + pr_constant = pr_or_by_notation pr_reference; + pr_reference = pr_reference; + pr_name = pr_lident; + pr_generic = Genprint.generic_raw_print; + pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; + pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; + } in + make_pr_tac + pr raw_printers + tag_raw_atomic_tactic_expr tag_raw_tactic_expr + n t + + let pr_raw_tactic = pr_raw_tactic_level ltop + + let pr_and_constr_expr pr (c,_) = pr c + + let pr_pat_and_constr_expr pr ((c,_),_) = pr c + + let rec pr_glob_tactic_level env n t = + let glob_printers = + (strip_prod_binders_glob_constr) + in + let rec prtac n (t:glob_tactic_expr) = + let pr = { + pr_tactic = prtac; + pr_constr = pr_and_constr_expr (pr_glob_constr_env env); + pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env); + pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); + pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env); + pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); + pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env); + pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env)); + pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); + pr_name = pr_lident; + pr_generic = Genprint.generic_glb_print; + pr_extend = pr_glob_extend + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); + pr_alias = pr_glob_alias + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); + } in + make_pr_tac + pr glob_printers + tag_glob_atomic_tactic_expr tag_glob_tactic_expr + n t + in + prtac n t + + let pr_glob_tactic env = pr_glob_tactic_level env ltop + + let strip_prod_binders_constr n ty = + let rec strip_ty acc n ty = + if n=0 then (List.rev acc, ty) else + match Term.kind_of_term ty with + Term.Prod(na,a,b) -> + strip_ty (([Loc.ghost,na],a)::acc) (n-1) b + | _ -> error "Cannot translate fix tactic: not enough products" in + strip_ty [] n ty + + let pr_tactic_level env n t = + let typed_printers = + (strip_prod_binders_constr) + in + let prtac n (t:tactic_expr) = + let pr = { + pr_tactic = pr_glob_tactic_level env; + pr_constr = pr_constr_env env Evd.empty; + pr_uconstr = pr_closed_glob_env env Evd.empty; + pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); + pr_lconstr = pr_lconstr_env env Evd.empty; + pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); + pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env); + pr_constant = pr_and_short_name (pr_evaluable_reference_env env); + pr_reference = pr_located pr_ltac_constant; + pr_name = pr_id; + pr_generic = Genprint.generic_top_print; + pr_extend = pr_extend + (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) + (pr_glob_tactic_level env) pr_constr_pattern; + pr_alias = pr_alias + (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) + (pr_glob_tactic_level env) pr_constr_pattern; + } + in + make_pr_tac + pr typed_printers + tag_atomic_tactic_expr tag_tactic_expr + n t + in + prtac n t + + let pr_tactic env = pr_tactic_level env ltop + +end + +module Tag = +struct + let keyword = + let style = Terminal.make ~bold:true () in + Ppstyle.make ~style ["tactic"; "keyword"] + + let primitive = + let style = Terminal.make ~fg_color:`LIGHT_GREEN () in + Ppstyle.make ~style ["tactic"; "primitive"] + + let string = + let style = Terminal.make ~fg_color:`LIGHT_RED () in + Ppstyle.make ~style ["tactic"; "string"] + +end + +include Make (Ppconstr) (struct + let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s + let do_not_tag _ x = x + let tag_keyword = tag Tag.keyword + let tag_primitive = tag Tag.primitive + let tag_string = tag Tag.string + let tag_glob_tactic_expr = do_not_tag + let tag_glob_atomic_tactic_expr = do_not_tag + let tag_raw_tactic_expr = do_not_tag + let tag_raw_atomic_tactic_expr = do_not_tag + let tag_tactic_expr = do_not_tag + let tag_atomic_tactic_expr = do_not_tag +end) + +(** Registering *) + +let () = + let pr_bool b = if b then str "true" else str "false" in + let pr_unit _ = str "()" in + let pr_string s = str "\"" ++ str s ++ str "\"" in + Genprint.register_print0 Constrarg.wit_ref + pr_reference (pr_or_var (pr_located pr_global)) pr_global; + Genprint.register_print0 + Constrarg.wit_intro_pattern + (Miscprint.pr_intro_pattern pr_constr_expr) + (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) + (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty)))); + Genprint.register_print0 + Constrarg.wit_clause_dft_concl + (pr_clauses (Some true) pr_lident) + (pr_clauses (Some true) pr_lident) + (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) + ; + Genprint.register_print0 Constrarg.wit_sort + pr_glob_sort pr_glob_sort (pr_sort Evd.empty); + Genprint.register_print0 + Constrarg.wit_uconstr + Ppconstr.pr_constr_expr + (fun (c,_) -> Printer.pr_glob_constr c) + Printer.pr_closed_glob + ; + Genprint.register_print0 Stdarg.wit_int int int int; + Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; + Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; + Genprint.register_print0 Stdarg.wit_pre_ident str str str; + Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string + +let () = + let printer _ _ prtac = prtac (0, E) in + declare_extra_genarg_pprule wit_tactic printer printer printer + +let _ = Hook.set Tactic_debug.tactic_printer + (fun x -> pr_glob_tactic (Global.env()) x) + +let _ = Hook.set Tactic_debug.match_pattern_printer + (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp) + +let _ = Hook.set Tactic_debug.match_rule_printer + (fun rl -> + pr_match_rule false (pr_glob_tactic (Global.env())) + (fun (_,p) -> pr_constr_pattern p) rl) + +module Richpp = struct + + include Make (Ppconstr.Richpp) (struct + open Ppannotation + let do_not_tag _ x = x + let tag e s = Pp.tag (Pp.Tag.inj e tag) s + let tag_keyword = tag AKeyword + let tag_primitive = tag AKeyword + let tag_string = do_not_tag () + let tag_glob_tactic_expr e = tag (AGlobTacticExpr e) + let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a) + let tag_raw_tactic_expr e = tag (ARawTacticExpr e) + let tag_raw_atomic_tactic_expr a = tag (ARawAtomicTacticExpr a) + let tag_tactic_expr e = tag (ATacticExpr e) + let tag_atomic_tactic_expr a = tag (AAtomicTacticExpr a) + end) + +end diff --git a/printing/pptactic.mli b/printing/pptactic.mli new file mode 100644 index 00000000..284237f0 --- /dev/null +++ b/printing/pptactic.mli @@ -0,0 +1,65 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + (tolerability -> raw_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +type 'a glob_extra_genarg_printer = + (glob_constr_and_expr -> std_ppcmds) -> + (glob_constr_and_expr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +type 'a extra_genarg_printer = + (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +val declare_extra_genarg_pprule : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer -> + 'b glob_extra_genarg_printer -> + 'c extra_genarg_printer -> unit + +type grammar_terminals = string option list + +type pp_tactic = { + pptac_args : argument_type list; + pptac_prods : int * grammar_terminals; +} + +val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit +val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit + +(** The default pretty-printers produce {!Pp.std_ppcmds} that are + interpreted as raw strings. *) +include Pptacticsig.Pp + +(** The rich pretty-printers produce {!Pp.std_ppcmds} that are + interpreted as annotated strings. The annotations can be + retrieved using {!RichPp.rich_pp}. Their definitions are + located in {!Ppannotation.t}. *) +module Richpp : Pptacticsig.Pp + diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli new file mode 100644 index 00000000..98b5757d --- /dev/null +++ b/printing/pptacticsig.mli @@ -0,0 +1,95 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds + val pr_red_expr : + ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> + ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds + val pr_may_eval : + ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds + + val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds + val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds + val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds + + val pr_clauses : bool option -> + ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds + val pr_raw_generic : + (constr_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + (tolerability -> raw_tactic_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + (Libnames.reference -> std_ppcmds) -> rlevel generic_argument -> + std_ppcmds + + val pr_glb_generic : + (glob_constr_and_expr -> Pp.std_ppcmds) -> + (glob_constr_and_expr -> Pp.std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (glob_constr_pattern_and_expr -> std_ppcmds) -> + glevel generic_argument -> std_ppcmds + + val pr_top_generic : + (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (Pattern.constr_pattern -> std_ppcmds) -> + tlevel generic_argument -> + std_ppcmds + + val pr_raw_extend: + (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> + (tolerability -> raw_tactic_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> int -> + ml_tactic_name -> raw_generic_argument list -> std_ppcmds + + val pr_glob_extend: + (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (glob_constr_pattern_and_expr -> std_ppcmds) -> int -> + ml_tactic_name -> glob_generic_argument list -> std_ppcmds + + val pr_extend : + (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (constr_pattern -> std_ppcmds) -> int -> + ml_tactic_name -> typed_generic_argument list -> std_ppcmds + + val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds + + val pr_raw_tactic : raw_tactic_expr -> std_ppcmds + + val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds + + val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds + + val pr_tactic : env -> tactic_expr -> std_ppcmds + + val pr_hintbases : string list option -> std_ppcmds + + val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds + + val pr_bindings : + ('constr -> std_ppcmds) -> + ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds + +end diff --git a/printing/pputils.ml b/printing/pputils.ml new file mode 100644 index 00000000..ee1a39ef --- /dev/null +++ b/printing/pputils.ml @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Loc.ghost then + let (b, e) = Loc.unloc loc in + Pp.comment b ++ pr x ++ Pp.comment e + else pr x diff --git a/printing/pputils.mli b/printing/pputils.mli new file mode 100644 index 00000000..72877483 --- /dev/null +++ b/printing/pputils.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds) -> 'a Loc.located -> std_ppcmds +(** Prints an object surrounded by its commented location *) + diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml new file mode 100644 index 00000000..e9e335ec --- /dev/null +++ b/printing/ppvernac.ml @@ -0,0 +1,1296 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* std_ppcmds + val tag_vernac : vernac_expr -> std_ppcmds -> std_ppcmds + end) += struct + + open Taggers + open Ppconstr + open Pptactic + + let keyword s = tag_keyword (str s) + + let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr + + let pr_lident (loc,id) = + if Loc.is_ghost loc then + let (b,_) = Loc.unloc loc in + pr_located pr_id (Loc.make_loc (b,b + String.length(Id.to_string id)),id) + else + pr_id id + + let string_of_fqid fqid = + String.concat "." (List.map Id.to_string fqid) + + let pr_fqid fqid = str (string_of_fqid fqid) + + let pr_lfqid (loc,fqid) = + if Loc.is_ghost loc then + let (b,_) = Loc.unloc loc in + pr_located pr_fqid (Loc.make_loc (b,b + String.length(string_of_fqid fqid)),fqid) + else + pr_fqid fqid + + let pr_lname = function + | (loc,Name id) -> pr_lident (loc,id) + | lna -> pr_located pr_name lna + + let pr_smart_global = pr_or_by_notation pr_reference + + let pr_ltac_ref = Libnames.pr_reference + + let pr_module = Libnames.pr_reference + + let pr_import_module = Libnames.pr_reference + + let sep_end = function + | VernacBullet _ + | VernacSubproof None + | VernacEndSubproof -> str"" + | _ -> str"." + + let pr_gen t = + pr_raw_generic + pr_constr_expr + pr_lconstr_expr + pr_raw_tactic_level + pr_constr_expr + pr_reference t + + let sep = fun _ -> spc() + let sep_v2 = fun _ -> str"," ++ spc() + + let pr_ne_sep sep pr = function + [] -> mt() + | l -> sep() ++ pr l + + let pr_set_entry_type = function + | ETName -> str"ident" + | ETReference -> str"global" + | ETPattern -> str"pattern" + | ETConstr _ -> str"constr" + | ETOther (_,e) -> str e + | ETBigint -> str "bigint" + | ETBinder true -> str "binder" + | ETBinder false -> str "closed binder" + | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" + + let strip_meta id = + let s = Id.to_string id in + if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1)) + else id + + let pr_production_item = function + | TacNonTerm (loc,nt,Some (p,sep)) -> + let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in + str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")" + | TacNonTerm (loc,nt,None) -> str nt + | TacTerm s -> qs s + + let pr_comment pr_c = function + | CommentConstr c -> pr_c c + | CommentString s -> qs s + | CommentInt n -> int n + + let pr_in_out_modules = function + | SearchInside l -> spc() ++ keyword "inside" ++ spc() ++ prlist_with_sep sep pr_module l + | SearchOutside [] -> mt() + | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l + + let pr_search_about (b,c) = + (if b then str "-" else mt()) ++ + match c with + | SearchSubPattern p -> pr_constr_pattern_expr p + | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + + let pr_search a gopt b pr_p = + pr_opt (fun g -> int g ++ str ":"++ spc()) gopt + ++ + match a with + | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b + | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b + | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b + | SearchAbout sl -> + keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + + let pr_locality local = if local then keyword "Local" else keyword "Global" + + let pr_explanation (e,b,f) = + let a = match e with + | ExplByPos (n,_) -> anomaly (Pp.str "No more supported") + | ExplByName id -> pr_id id in + let a = if f then str"!" ++ a else a in + if b then str "[" ++ a ++ str "]" else a + + let pr_option_ref_value = function + | QualidRefValue id -> pr_reference id + | StringRefValue s -> qs s + + let pr_printoption table b = + prlist_with_sep spc str table ++ + pr_opt (prlist_with_sep sep pr_option_ref_value) b + + let pr_set_option a b = + let pr_opt_value = function + | IntValue None -> assert false + (* This should not happen because of the grammar *) + | IntValue (Some n) -> spc() ++ int n + | StringValue s -> spc() ++ str s + | BoolValue b -> mt() + in pr_printoption a None ++ pr_opt_value b + + let pr_topcmd _ = str"(* : No printer for toplevel commands *)" + + let pr_opt_hintbases l = match l with + | [] -> mt() + | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z + + let pr_reference_or_constr pr_c = function + | HintsReference r -> pr_reference r + | HintsConstr c -> pr_c c + + let pr_hints db h pr_c pr_pat = + let opth = pr_opt_hintbases db in + let pph = + match h with + | HintsResolve l -> + keyword "Resolve " ++ prlist_with_sep sep + (fun (pri, _, c) -> pr_reference_or_constr pr_c c ++ + match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ()) + l + | HintsImmediate l -> + keyword "Immediate" ++ spc() ++ + prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l + | HintsUnfold l -> + keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l + | HintsTransparency (l, b) -> + keyword (if b then "Transparent" else "Opaque") + ++ spc () + ++ prlist_with_sep sep pr_reference l + | HintsMode (m, l) -> + keyword "Mode" + ++ spc () + ++ pr_reference m ++ spc() ++ prlist_with_sep spc + (fun b -> if b then str"+" else str"-") l + | HintsConstructors c -> + keyword "Constructors" + ++ spc() ++ prlist_with_sep spc pr_reference c + | HintsExtern (n,c,tac) -> + let pat = match c with None -> mt () | Some pat -> pr_pat pat in + keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ + spc() ++ pr_raw_tactic tac + in + hov 2 (keyword "Hint "++ pph ++ opth) + + let pr_with_declaration pr_c = function + | CWith_Definition (id,c) -> + let p = pr_c c in + keyword "Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p + | CWith_Module (id,qid) -> + keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ + pr_located pr_qualid qid + + let rec pr_module_ast leading_space pr_c = function + | CMident qid -> + if leading_space then + spc () ++ pr_located pr_qualid qid + else + pr_located pr_qualid qid + | CMwith (_,mty,decl) -> + let m = pr_module_ast leading_space pr_c mty in + let p = pr_with_declaration pr_c decl in + m ++ spc() ++ keyword "with" ++ spc() ++ p + | CMapply (_,me1,(CMident _ as me2)) -> + pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2 + | 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_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 + | CHole (loc, k, Misctypes.IntroAnonymous, _) -> mt() + | _ as c -> brk(0,2) ++ str" :" ++ pr_c c + + let pr_decl_notation prc ((loc,ntn),c,scopt) = + fnl () ++ keyword "where " ++ qs ntn ++ str " := " ++ prc c ++ + pr_opt (fun sc -> str ": " ++ str sc) scopt + + let pr_binders_arg = + pr_ne_sep spc pr_binders + + let pr_and_type_binders_arg bl = + pr_binders_arg bl + + let pr_onescheme (idop,schem) = + match schem with + | InductionScheme (dep,ind,s) -> + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc () + ) ++ + hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for") + ++ spc() ++ pr_smart_global ind) ++ spc() ++ + hov 0 (keyword "Sort" ++ spc() ++ pr_glob_sort 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() ++ pr_glob_sort 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,_),_))::_ -> fst (Loc.unloc loc) + + let pr_class_rawexpr = function + | FunClass -> keyword "Funclass" + | SortClass -> keyword "Sortclass" + | RefClass qid -> pr_smart_global qid + + let pr_assumption_token many (l,a) = + let l = match l with Some x -> x | None -> Decl_kinds.Global in + match l, a with + | (Discharge,Logical) -> + keyword (if many then "Hypotheses" else "Hypothesis") + | (Discharge,Definitional) -> + keyword (if many then "Variables" else "Variable") + | (Global,Logical) -> + keyword (if many then "Axioms" else "Axiom") + | (Global,Definitional) -> + keyword (if many then "Parameters" else "Parameter") + | (Local, Logical) -> + keyword (if many then "Local Axioms" else "Local Axiom") + | (Local,Definitional) -> + keyword (if many then "Local Parameters" else "Local Parameter") + | (Global,Conjectural) -> str"Conjecture" + | ((Discharge | Local),Conjectural) -> + anomaly (Pp.str "Don't know how to beautify a local conjecture") + + let pr_params pr_c (xl,(c,t)) = + hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ + (if c then str":>" else str":" ++ + spc() ++ pr_c t)) + + let rec factorize = function + | [] -> [] + | (c,(idl,t))::l -> + match factorize l with + | (xl,((c', t') as r))::l' + when (c : bool) == c' && Pervasives.(=) t t' -> + (** FIXME: we need equality on constr_expr *) + (idl@xl,r)::l' + | l' -> (idl,(c,t))::l' + + let pr_ne_params_list pr_c l = + match factorize l with + | [p] -> pr_params pr_c p + | l -> + prlist_with_sep spc + (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l +(* + prlist_with_sep pr_semicolon (pr_params pr_c) +*) + + let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) + + let pr_syntax_modifier = function + | SetItemLevel (l,NextLevel) -> + prlist_with_sep sep_v2 str l ++ + spc() ++ keyword "at next level" + | SetItemLevel (l,NumLevel n) -> + prlist_with_sep sep_v2 str l ++ + spc() ++ keyword "at level" ++ spc() ++ int n + | SetLevel n -> keyword "at level" ++ spc() ++ int n + | SetAssoc LeftA -> keyword "left associativity" + | SetAssoc RightA -> keyword "right associativity" + | SetAssoc NonA -> keyword "no associativity" + | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ + | SetOnlyParsing Flags.Current -> keyword "only parsing" + | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") + | SetFormat("text",s) -> keyword "format " ++ pr_located qs s + | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s + + let pr_syntax_modifiers = function + | [] -> mt() + | l -> spc() ++ + hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") + + let print_level n = + if not (Int.equal n 0) then + spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")") + else + mt () + + let pr_grammar_tactic_rule n (_,pil,t) = + hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++ + hov 0 (prlist_with_sep sep pr_production_item pil ++ + spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) + + let pr_statement head (id,(bl,c,guard)) = + assert (not (Option.is_empty id)); + hov 2 + (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++ + (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ + pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ + str":" ++ pr_spc_lconstr c) + + let pr_priority = function + | None -> mt () + | Some i -> spc () ++ str "|" ++ spc () ++ int i + +(**************************************) +(* Pretty printer for vernac commands *) +(**************************************) + let make_pr_vernac pr_constr pr_lconstr = + let pr_constrarg c = spc () ++ pr_constr c in + let pr_lconstrarg c = spc () ++ pr_lconstr c in + let pr_intarg n = spc () ++ int n in + let pr_oc = function + None -> str" :" + | Some true -> str" :>" + | Some false -> str" :>>" + in + let pr_record_field ((x, pri), ntn) = + let prx = match x with + | (oc,AssumExpr (id,t)) -> + hov 1 (pr_lname id ++ + pr_oc oc ++ spc() ++ + pr_lconstr_expr t) + | (oc,DefExpr(id,b,opt)) -> (match opt with + | Some t -> + hov 1 (pr_lname id ++ + pr_oc oc ++ spc() ++ + pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) + | None -> + hov 1 (pr_lname id ++ str" :=" ++ spc() ++ + pr_lconstr b)) in + let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in + prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn + in + 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"}") + in + + let pr_printable = function + | PrintFullContext -> + keyword "Print All" + | PrintSectionContext s -> + keyword "Print Section" ++ spc() ++ Libnames.pr_reference s + | PrintGrammar ent -> + keyword "Print Grammar" ++ spc() ++ str ent + | PrintLoadPath dir -> + keyword "Print LoadPath" ++ pr_opt pr_dirpath 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 + | PrintLtac qid -> + keyword "Print Ltac" ++ spc() ++ pr_ltac_ref 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 + | PrintRewriteHintDbName s -> + keyword "Print Rewrite HintDb" ++ spc() ++ str s + | PrintUniverses (b, fopt) -> + let cmd = + if b then "Print Sorted Universes" + else "Print Universes" + in + keyword cmd ++ pr_opt str fopt + | PrintName qid -> + keyword "Print" ++ spc() ++ pr_smart_global qid + | PrintModuleType qid -> + keyword "Print Module Type" ++ spc() ++ pr_reference qid + | PrintModule qid -> + keyword "Print Module" ++ spc() ++ pr_reference qid + | PrintInspect n -> + keyword "Inspect" ++ spc() ++ int n + | PrintScopes -> + keyword "Print Scopes" + | PrintScope s -> + keyword "Print Scope" ++ spc() ++ str s + | PrintVisibility s -> + keyword "Print Visibility" ++ pr_opt str s + | PrintAbout (qid,gopt) -> + pr_opt (fun g -> int g ++ str ":"++ spc()) gopt + ++ keyword "About" ++ spc() ++ pr_smart_global qid + | 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" ++ pr_dirpath dp + | PrintStrategy None -> + keyword "Print Strategies" + | PrintStrategy (Some qid) -> + keyword "Print Strategy" ++ pr_smart_global qid + in + + let pr_using e = str (Proof_using.to_string e) in + + let rec pr_vernac v = + let return = Taggers.tag_vernac v in + match v with + | VernacPolymorphic (poly, v) -> + let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in + return (s ++ pr_vernac v) + | VernacProgram v -> + return (keyword "Program" ++ spc() ++ pr_vernac v) + | VernacLocal (local, v) -> + return (pr_locality local ++ spc() ++ pr_vernac v) + + (* Stm *) + | VernacStm JoinDocument -> + return (keyword "Stm JoinDocument") + | VernacStm PrintDag -> + return (keyword "Stm PrintDag") + | VernacStm Finish -> + return (keyword "Stm Finish") + | VernacStm Wait -> + return (keyword "Stm Wait") + | VernacStm (Observe id) -> + return (keyword "Stm Observe " ++ str(Stateid.to_string id)) + | VernacStm (Command v) -> + return (keyword "Stm Command " ++ pr_vernac v) + | VernacStm (PGLast v) -> + return (keyword "Stm PGLast " ++ pr_vernac v) + + (* Proof management *) + | VernacAbortAll -> + return (keyword "Abort All") + | VernacRestart -> + return (keyword "Restart") + | VernacUnfocus -> + return (keyword "Unfocus") + | VernacUnfocused -> + return (keyword "Unfocused") + | VernacGoal c -> + return (keyword "Goal" ++ pr_lconstrarg c) + | VernacAbort id -> + return (keyword "Abort" ++ pr_opt pr_lident id) + | VernacUndo i -> + 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) + | VernacBacktrack (i,j,k) -> + return (keyword "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k]) + | VernacFocus i -> + return (keyword "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 -> keyword "Show" ++ pr_goal_reference n + | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n + | ShowProof -> keyword "Show Proof" + | ShowNode -> keyword "Show Node" + | ShowScript -> keyword "Show Script" + | ShowExistentials -> keyword "Show Existentials" + | ShowUniverses -> keyword "Show Universes" + | ShowTree -> keyword "Show Tree" + | ShowProofNames -> keyword "Show Conjectures" + | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") + | ShowMatch id -> keyword "Show Match " ++ pr_lident id + | ShowThesis -> keyword "Show Thesis" + 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) + + (* Control *) + | VernacLoad (f,s) -> + return ( + keyword "Load" + ++ if f then + (spc() ++ keyword "Verbose" ++ spc()) + else + spc() ++ qs s + ) + | VernacTime v -> + return (keyword "Time" ++ spc() ++ pr_vernac_list v) + | VernacTimeout(n,v) -> + return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v) + | VernacFail v -> + return (keyword "Fail" ++ spc() ++ pr_vernac v) + | VernacError _ -> + return (keyword "No-parsing-rule for VernacError") + + (* Syntax *) + | VernacTacticNotation (n,r,e) -> + return (pr_grammar_tactic_rule n ("",r,e)) + | VernacOpenCloseScope (_,(opening,sc)) -> + return ( + keyword (if opening then "Open " else "Close ") ++ + keyword "Scope" ++ spc() ++ str sc + ) + | VernacDelimiters (sc,key) -> + return ( + keyword "Delimit Scope" ++ spc () ++ str sc ++ + spc() ++ keyword "with" ++ spc () ++ str key + ) + | VernacBindScope (sc,cll) -> + return ( + keyword "Bind Scope" ++ spc () ++ str sc ++ + spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_smart_global cll + ) + | VernacArgumentsScope (q,scl) -> + let pr_opt_scope = function + | None -> str"_" + | Some sc -> str sc + in + return ( + keyword "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 (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,((_,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 (keyword "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 ( + keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ + pr_syntax_modifiers l + ) + | VernacNotationAddFormat(s,k,v) -> + return ( + keyword "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 + keyword (Kindops.string_of_definition_kind (l,false,dk)) + in + let pr_reduce = function + | None -> mt() + | Some r -> + keyword "Eval" ++ spc() ++ + pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++ + keyword " in" ++ spc() + in + let pr_def_body = function + | DefineBody (bl,red,body,d) -> + let ty = match d with + | None -> mt() + | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty + in + (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) + | ProveBody (bl,t) -> + (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 () ++ keyword "with")) (List.tl l)) + ) + + | VernacEndProof Admitted -> + return (keyword "Admitted") + + | VernacEndProof (Proved (opac,o)) -> return ( + match o with + | None -> if opac then keyword "Qed" else keyword "Defined" + | Some (id,th) -> (match th with + | None -> (if opac then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id + | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id) + ) + | VernacExactProof c -> + return (hov 2 (keyword "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 + 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 ++ keyword "Fixpoint" ++ spc () ++ + prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs) + ) + + | VernacCoFixpoint (local, corecs) -> + let local = match local with + | Some Discharge -> keyword "Let" ++ spc () + | Some Local -> keyword "Local" ++ spc () + | None | Some Global -> str "" + 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 (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 -> + let pr_uconstraint (l, d, r) = + pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r + in + 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 (exp, l) -> + return ( + hov 2 + (keyword "Require" ++ spc() ++ pr_require_token exp ++ + prlist_with_sep sep pr_module l) + ) + | VernacImport (f,l) -> + return ( + (if f then keyword "Export" else keyword "Import") ++ spc() ++ + prlist_with_sep sep pr_import_module l + ) + | VernacCanonical q -> + return ( + keyword "Canonical Structure" ++ spc() ++ pr_smart_global q + ) + | VernacCoercion (_,id,c1,c2) -> + return ( + hov 1 ( + keyword "Coercion" ++ spc() ++ + pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ + spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) + ) + | VernacIdentityCoercion (_,id,c1,c2) -> + return ( + hov 1 ( + keyword "Identity Coercion" ++ spc() ++ pr_lident id ++ + spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ + spc() ++ pr_class_rawexpr c2) + ) + + | VernacInstance (abst, sup, (instid, bk, cl), props, pri) -> + return ( + hov 1 ( + (if abst then keyword "Declare" ++ spc () else mt ()) ++ + keyword "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 ( + keyword "Context" ++ spc () ++ pr_and_type_binders_arg l) + ) + + | VernacDeclareInstances (ids, pri) -> + return ( + hov 1 (keyword "Existing" ++ spc () ++ + keyword(String.plural (List.length ids) "Instance") ++ + spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri) + ) + + | VernacDeclareClass id -> + return ( + hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id) + ) + + (* Modules and Module Types *) + | VernacDefineModule (export,m,bl,tys,bd) -> + let b = pr_module_binders bl pr_lconstr in + return ( + hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++ + pr_lident m ++ b ++ + pr_of_module_type pr_lconstr tys ++ + (if List.is_empty bd then mt () else str ":= ") ++ + prlist_with_sep (fun () -> str " <+ ") + (pr_module_ast_inl true pr_lconstr) bd) + ) + | VernacDeclareModule (export,id,bl,m1) -> + let b = pr_module_binders bl pr_lconstr in + return ( + hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++ + pr_lident id ++ b ++ + pr_module_ast_inl true pr_lconstr m1) + ) + | VernacDeclareModuleType (id,bl,tyl,m) -> + let b = pr_module_binders bl pr_lconstr in + let pr_mt = pr_module_ast_inl true pr_lconstr in + return ( + hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++ + prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++ + (if List.is_empty m then mt () else str ":= ") ++ + prlist_with_sep (fun () -> str " <+ ") pr_mt m) + ) + | VernacInclude (mexprs) -> + let pr_m = pr_module_ast_inl false pr_lconstr in + return ( + hov 2 (keyword "Include" ++ spc() ++ + prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) + ) + (* Solving *) + | VernacSolve (i,info,tac,deftac) -> + let pr_goal_selector = function + | SelectNth i -> int i ++ str":" + | SelectId id -> pr_id id ++ str":" + | SelectAll -> str"all" ++ str":" + | SelectAllParallel -> str"par" + in + let pr_info = + match info with + | None -> mt () + | Some i -> str"Info"++spc()++int i++spc() + in + 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) -> + 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() ++ pr_dirpath 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 *) + | 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 + (keyword "Ltac" ++ spc () ++ + prlist_with_sep (fun () -> + fnl() ++ keyword "with" ++ spc ()) pr_tac_body l) + ) + | VernacCreateHintDb (dbname,b) -> + return ( + hov 1 (keyword "Create HintDb" ++ spc () ++ + str dbname ++ (if b then str" discriminated" else mt ())) + ) + | VernacRemoveHints (dbnames, ids) -> + return ( + hov 1 (keyword "Remove Hints" ++ spc () ++ + prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ + pr_opt_hintbases dbnames) + ) + | VernacHints (_, dbnames,h) -> + return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) + | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> + return ( + hov 2 + (keyword "Notation" ++ spc () ++ 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 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q) + ) + | VernacDeclareImplicits (q,impls) -> + return ( + hov 1 (keyword "Implicit Arguments" ++ spc () ++ + 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 ( + keyword "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 -> keyword "simpl nomatch" + | `ReductionNeverUnfold -> keyword "simpl never" + | `DefaultImplicits -> keyword "default implicits" + | `Rename -> keyword "rename" + | `Assert -> keyword "assert" + | `ExtraScopes -> keyword "extra scopes" + | `ClearImplicits -> keyword "clear implicits" + | `ClearScopes -> keyword "clear scopes") + mods) + ) + | VernacReserve bl -> + let n = List.length (List.flatten (List.map fst bl)) in + return ( + hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " ")) + ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl)) + ) + | VernacGeneralizable g -> + return ( + hov 1 (tag_keyword ( + str"Generalizable Variable" ++ + match g with + | None -> str "s none" + | Some [] -> str "s all" + | Some idl -> + str (if List.length idl > 1 then "s " else " ") ++ + prlist_with_sep spc pr_lident idl) + )) + | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k -> + return ( + hov 1 (keyword "Transparent" ++ + spc() ++ prlist_with_sep sep pr_smart_global l) + ) + | VernacSetOpacity(Conv_oracle.Opaque,l) -> + return ( + hov 1 (keyword "Opaque" ++ + spc() ++ prlist_with_sep sep pr_smart_global l) + ) + | VernacSetOpacity _ -> + return ( + Errors.anomaly (keyword "VernacSetOpacity used to set something else") + ) + | VernacSetStrategy l -> + let pr_lev = function + | Conv_oracle.Opaque -> keyword "opaque" + | Conv_oracle.Expand -> keyword "expand" + | l when Conv_oracle.is_transparent l -> keyword "transparent" + | Conv_oracle.Level n -> int n + in + let pr_line (l,q) = + hov 2 (pr_lev l ++ spc() ++ + str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") + in + return ( + hov 1 (keyword "Strategy" ++ spc() ++ + hv 0 (prlist_with_sep sep pr_line l)) + ) + | VernacUnsetOption (na) -> + return ( + hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None) + ) + | VernacSetOption (na,v) -> + return ( + hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v) + ) + | VernacAddOption (na,l) -> + return ( + hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacRemoveOption (na,l) -> + return ( + hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacMemOption (na,l) -> + return ( + hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacPrintOption na -> + return ( + hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None) + ) + | VernacCheckMayEval (r,io,c) -> + let pr_mayeval r c = match r with + | Some r0 -> + hov 2 (keyword "Eval" ++ spc() ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++ + spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) + | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) + in + let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in + return (pr_i ++ pr_mayeval r c) + | VernacGlobalCheck c -> + return (hov 2 (keyword "Type" ++ pr_constrarg c)) + | VernacDeclareReduction (s,r) -> + return ( + keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r + ) + | VernacPrint p -> + return (pr_printable p) + | VernacSearch (sea,g,sea_r) -> + return (pr_search sea g sea_r pr_constr_pattern_expr) + | VernacLocate loc -> + let pr_locate =function + | LocateAny qid -> pr_smart_global qid + | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid + | LocateFile f -> keyword "File" ++ spc() ++ qs f + | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid + | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid + | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid + in + return (keyword "Locate" ++ spc() ++ pr_locate loc) + | VernacRegister (id, RegisterInline) -> + return ( + hov 2 + (keyword "Register Inline" ++ spc() ++ pr_lident id) + ) + | VernacComments l -> + return ( + hov 2 + (keyword "Comments" ++ spc() + ++ prlist_with_sep sep (pr_comment pr_constr) l) + ) + | VernacNop -> + mt() + + (* Toplevel control *) + | VernacToplevelControl exn -> + return (pr_topcmd exn) + + (* 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() ++ pr_raw_tactic te) + | VernacProof (Some te, Some e) -> + return ( + keyword "Proof" ++ spc () ++ + keyword "using" ++ spc() ++ pr_using e ++ spc() ++ + keyword "with" ++ spc() ++pr_raw_tactic te + ) + | VernacProofMode s -> + return (keyword "Proof Mode" ++ str 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 (keyword "BeginSubproof" ++ spc () ++ int i) + | VernacEndSubproof -> + return (str "}") + + and pr_vernac_list l = + hov 2 (str"[" ++ spc() ++ + prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l + ++ spc() ++ str"]") + + and pr_extend s cl = + let pr_arg a = + try pr_gen a + with Failure _ -> str ("") in + try + let rl = Egramml.get_extend_vernac_rule s in + let start,rl,cl = + match rl with + | Egramml.GramTerminal s :: rl -> str s, rl, cl + | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl + | [] -> anomaly (Pp.str "Empty entry") in + let (pp,_) = + List.fold_left + (fun (strm,args) pi -> + let pp,args = match pi with + | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args) + | Egramml.GramTerminal s -> (str s, args) in + (strm ++ spc() ++ pp), args) + (start,cl) rl in + hov 1 pp + with Not_found -> + hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") + + in pr_vernac + + let pr_vernac_body v = make_pr_vernac pr_constr_expr pr_lconstr_expr v + + let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end v + + let pr_vernac x = + try pr_vernac x + with e -> Errors.print e + +end + +include Make (Ppconstr) (Pptactic) (struct + let do_not_tag _ x = x + let tag_keyword = do_not_tag () + let tag_vernac = do_not_tag +end) + +module Richpp = struct + + include Make + (Ppconstr.Richpp) + (Pptactic.Richpp) + (struct + open Ppannotation + let tag_keyword s = Pp.tag (Pp.Tag.inj AKeyword tag) s + let tag_vernac v s = Pp.tag (Pp.Tag.inj (AVernac v) tag) s + end) + +end diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli new file mode 100644 index 00000000..f38848cd --- /dev/null +++ b/printing/ppvernac.mli @@ -0,0 +1,20 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Pp.std_ppcmds + + (** Prints a vernac expression and closes it with a dot. *) + val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds + +end diff --git a/printing/prettyp.ml b/printing/prettyp.ml new file mode 100644 index 00000000..223377c2 --- /dev/null +++ b/printing/prettyp.ml @@ -0,0 +1,852 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + * on May-June 2006 for implementation of abstraction of pretty-printing of objects. + *) + +open Pp +open Errors +open Util +open Names +open Nameops +open Term +open Termops +open Declarations +open Environ +open Impargs +open Libobject +open Libnames +open Globnames +open Recordops +open Misctypes +open Printer +open Printmod + +type object_pr = { + print_inductive : mutual_inductive -> std_ppcmds; + print_constant_with_infos : constant -> std_ppcmds; + print_section_variable : variable -> std_ppcmds; + print_syntactic_def : kernel_name -> std_ppcmds; + print_module : bool -> Names.module_path -> std_ppcmds; + print_modtype : module_path -> std_ppcmds; + print_named_decl : Id.t * constr option * types -> std_ppcmds; + print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; + print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds; +} + +let gallina_print_module = print_module +let gallina_print_modtype = print_modtype + +(**************) +(** Utilities *) + +let print_closed_sections = ref false + +let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) + +let with_line_skip l = if List.is_empty l then mt() else fnl() ++ fnl () ++ pr_infos_list l + +let blankline = mt() (* add a blank sentence in the list of infos *) + +let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": " + +let int_or_no n = if Int.equal n 0 then str "no" else int n + +(*******************) +(** Basic printing *) + +let print_basename sp = pr_global (ConstRef sp) + +let print_ref reduce ref = + let typ = Global.type_of_global_unsafe ref in + let typ = + if reduce then + let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ + in it_mkProd_or_LetIn ccl ctx + else typ in + let univs = Global.universes_of_global ref in + hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ + Printer.pr_universe_ctx univs) + +(********************************) +(** Printing implicit arguments *) + +let pr_impl_name imp = pr_id (name_of_implicit imp) + +let print_impargs_by_name max = function + | [] -> [] + | impls -> + let n = List.length impls in + [hov 0 (str (String.plural n "Argument") ++ spc() ++ + prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++ + str (String.conjugate_verb_to_be n) ++ str" implicit" ++ + (if max then strbrk " and maximally inserted" else mt()))] + +let print_one_impargs_list l = + let imps = List.filter is_status_implicit l in + let maximps = List.filter Impargs.maximal_insertion_of imps in + let nonmaximps = List.subtract Pervasives.(=) imps maximps in (* FIXME *) + print_impargs_by_name false nonmaximps @ + print_impargs_by_name true maximps + +let print_impargs_list prefix l = + let l = extract_impargs_data l in + List.flatten (List.map (fun (cond,imps) -> + match cond with + | None -> + List.map (fun pp -> add_colon prefix ++ pp) + (print_one_impargs_list imps) + | Some (n1,n2) -> + [v 2 (prlist_with_sep cut (fun x -> x) + [(if ismt prefix then str "When" else prefix ++ str ", when") ++ + str " applied to " ++ + (if Int.equal n1 n2 then int_or_no n2 else + if Int.equal n1 0 then str "less than " ++ int n2 + else int n1 ++ str " to " ++ int_or_no n2) ++ + str (String.plural n2 " argument") ++ str ":"; + v 0 (prlist_with_sep cut (fun x -> x) + (if List.exists is_status_implicit imps + then print_one_impargs_list imps + else [str "No implicit arguments"]))])]) l) + +let print_renames_list prefix l = + if List.is_empty l then [] else + [add_colon prefix ++ str "Arguments are renamed to " ++ + hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))] + +let need_expansion impl ref = + let typ = Global.type_of_global_unsafe ref in + let ctx = prod_assum typ in + let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in + not (List.is_empty impl) && List.length impl >= nprods && + let _,lastimpl = List.chop nprods impl in + List.exists is_status_implicit lastimpl + +let print_impargs ref = + let ref = Smartlocate.smart_global ref in + let impl = implicits_of_global ref in + let has_impl = not (List.is_empty impl) in + (* Need to reduce since implicits are computed with products flattened *) + pr_infos_list + ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref; + blankline ] @ + (if has_impl then print_impargs_list (mt()) impl + else [str "No implicit arguments"])) + +(*********************) +(** Printing Scopes *) + +let print_argument_scopes prefix = function + | [Some sc] -> + [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"] + | l when not (List.for_all Option.is_empty l) -> + [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++ + str "[" ++ + pr_sequence (function Some sc -> str sc | None -> str "_") l ++ + str "]")] + | _ -> [] + +(*********************) +(** Printing Opacity *) + +type opacity = + | FullyOpaque + | TransparentMaybeOpacified of Conv_oracle.level + +let opacity env = function + | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) -> + Some(TransparentMaybeOpacified + (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) + | ConstRef cst -> + let cb = Environ.lookup_constant cst env in + (match cb.const_body with + | Undef _ -> None + | OpaqueDef _ -> Some FullyOpaque + | Def _ -> Some + (TransparentMaybeOpacified + (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst)))) + | _ -> None + +let print_opacity ref = + match opacity (Global.env()) ref with + | None -> [] + | Some s -> + [pr_global ref ++ str " is " ++ + str (match s with + | FullyOpaque -> "opaque" + | TransparentMaybeOpacified Conv_oracle.Opaque -> + "basically transparent but considered opaque for reduction" + | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev -> + "transparent" + | TransparentMaybeOpacified (Conv_oracle.Level n) -> + "transparent (with expansion weight "^string_of_int n^")" + | TransparentMaybeOpacified Conv_oracle.Expand -> + "transparent (with minimal expansion weight)")] + +(*******************) +(* *) + +let print_polymorphism ref = + let poly = Global.is_polymorphic ref in + let template_poly = Global.is_template_polymorphic ref in + pr_global ref ++ str " is " ++ str + (if poly then "universe polymorphic" + else if template_poly then + "template universe polymorphic" + else "not universe polymorphic") + +let print_primitive_record mipv = function + | Some (Some (_, ps,_)) -> + [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."] + | _ -> [] + +let print_primitive ref = + match ref with + | IndRef ind -> + let mib,_ = Global.lookup_inductive ind in + print_primitive_record mib.mind_packets mib.mind_record + | _ -> [] + +let print_name_infos ref = + let poly = print_polymorphism ref in + let impls = implicits_of_global ref in + let scopes = Notation.find_arguments_scope ref in + let renames = + try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in + let type_info_for_implicit = + if need_expansion (select_impargs_size 0 impls) ref then + (* Need to reduce since implicits are computed with products flattened *) + [str "Expanded type for implicit arguments"; + print_ref true ref; blankline] + else + [] in + poly :: print_primitive ref @ + type_info_for_implicit @ + print_renames_list (mt()) renames @ + print_impargs_list (mt()) impls @ + print_argument_scopes (mt()) scopes + +let print_id_args_data test pr id l = + if List.exists test l then + pr (str "For " ++ pr_id id) l + else + [] + +let print_args_data_of_inductive_ids get test pr sp mipv = + List.flatten (Array.to_list (Array.mapi + (fun i mip -> + print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) @ + List.flatten (Array.to_list (Array.mapi + (fun j idc -> + print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1)))) + mip.mind_consnames))) + mipv)) + +let print_inductive_implicit_args = + print_args_data_of_inductive_ids + implicits_of_global (fun l -> not (List.is_empty (positions_of_implicits l))) + print_impargs_list + +let print_inductive_renames = + print_args_data_of_inductive_ids + (fun r -> + try List.hd (Arguments_renaming.arguments_names r) with Not_found -> []) + ((!=) Anonymous) + print_renames_list + +let print_inductive_argument_scopes = + print_args_data_of_inductive_ids + Notation.find_arguments_scope (Option.has_some) print_argument_scopes + +(*********************) +(* "Locate" commands *) + +type logical_name = + | Term of global_reference + | Dir of global_dir_reference + | Syntactic of kernel_name + | ModuleType of module_path + | Tactic of Nametab.ltac_constant + | Undefined of qualid + +let locate_any_name ref = + let (loc,qid) = qualid_of_reference ref in + try Term (Nametab.locate qid) + with Not_found -> + try Syntactic (Nametab.locate_syndef qid) + with Not_found -> + try Dir (Nametab.locate_dir qid) + with Not_found -> + try ModuleType (Nametab.locate_modtype qid) + with Not_found -> Undefined qid + +let pr_located_qualid = function + | Term ref -> + let ref_str = match ref with + ConstRef _ -> "Constant" + | IndRef _ -> "Inductive" + | ConstructRef _ -> "Constructor" + | VarRef _ -> "Variable" in + str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) + | Syntactic kn -> + str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) + | Dir dir -> + let s,dir = match dir with + | DirOpenModule (dir,_) -> "Open Module", dir + | DirOpenModtype (dir,_) -> "Open Module Type", dir + | DirOpenSection (dir,_) -> "Open Section", dir + | DirModule (dir,_) -> "Module", dir + | DirClosedSection dir -> "Closed Section", dir + in + str s ++ spc () ++ pr_dirpath dir + | ModuleType mp -> + str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) + | Tactic kn -> + str "Ltac" ++ spc () ++ pr_path (Nametab.path_of_tactic kn) + | Undefined qid -> + pr_qualid qid ++ spc () ++ str "not a defined object." + +let canonize_ref = function + | ConstRef c -> + let kn = Constant.canonical c in + if KerName.equal (Constant.user c) kn then None + else Some (ConstRef (Constant.make1 kn)) + | IndRef (ind,i) -> + let kn = MutInd.canonical ind in + if KerName.equal (MutInd.user ind) kn then None + else Some (IndRef (MutInd.make1 kn, i)) + | ConstructRef ((ind,i),j) -> + let kn = MutInd.canonical ind in + if KerName.equal (MutInd.user ind) kn then None + else Some (ConstructRef ((MutInd.make1 kn, i),j)) + | VarRef _ -> None + +let display_alias = function + | Term r -> + begin match canonize_ref r with + | None -> mt () + | Some r' -> + let q' = Nametab.shortest_qualid_of_global Id.Set.empty r' in + spc () ++ str "(alias of " ++ pr_qualid q' ++ str ")" + end + | _ -> mt () + +let locate_term qid = + let expand = function + | TrueGlobal ref -> + Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref + | SynDef kn -> + Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn + in + List.map expand (Nametab.locate_extended_all qid) + +let locate_tactic qid = + let all = Nametab.locate_extended_all_tactic qid in + List.map (fun kn -> (Tactic kn, Nametab.shortest_qualid_of_tactic kn)) all + +let locate_module qid = + let all = Nametab.locate_extended_all_dir qid in + let map dir = match dir with + | DirModule (_, (mp, _)) -> Some (Dir dir, Nametab.shortest_qualid_of_module mp) + | DirOpenModule _ -> Some (Dir dir, qid) + | _ -> None + in + List.map_filter map all + +let locate_modtype qid = + let all = Nametab.locate_extended_all_modtype qid in + let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in + let modtypes = List.map map all in + (** Don't forget the opened module types: they are not part of the same name tab. *) + let all = Nametab.locate_extended_all_dir qid in + let map dir = match dir with + | DirOpenModtype _ -> Some (Dir dir, qid) + | _ -> None + in + modtypes @ List.map_filter map all + +let print_located_qualid name flags ref = + let (loc,qid) = qualid_of_reference ref in + let located = [] in + let located = if List.mem `LTAC flags then locate_tactic qid @ located else located in + let located = if List.mem `MODTYPE flags then locate_modtype qid @ located else located in + let located = if List.mem `MODULE flags then locate_module qid @ located else located in + let located = if List.mem `TERM flags then locate_term qid @ located else located in + match located with + | [] -> + let (dir,id) = repr_qualid qid in + if DirPath.is_empty dir then + str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id + else + str ("No " ^ name ^ " of suffix") ++ spc () ++ pr_qualid qid + | l -> + prlist_with_sep fnl + (fun (o,oqid) -> + hov 2 (pr_located_qualid o ++ + (if not (qualid_eq oqid qid) then + spc() ++ str "(shorter name to refer to it in current context is " + ++ pr_qualid oqid ++ str")" + else mt ()) ++ + display_alias o)) l + +let print_located_term ref = print_located_qualid "term" [`TERM] ref +let print_located_tactic ref = print_located_qualid "tactic" [`LTAC] ref +let print_located_module ref = print_located_qualid "module" [`MODULE; `MODTYPE] ref +let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE; `MODTYPE] ref + +(******************************************) +(**** Printing declarations and judgments *) +(**** Gallina layer *****) + +let gallina_print_typed_value_in_env env sigma (trm,typ) = + (pr_lconstr_env env sigma trm ++ fnl () ++ + str " : " ++ pr_ltype_env env sigma typ) + +(* To be improved; the type should be used to provide the types in the + abstractions. This should be done recursively inside pr_lconstr, so that + the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) + synthesizes the type nat of the abstraction on u *) + +let print_named_def name body typ = + let pbody = pr_lconstr body in + let ptyp = pr_ltype typ in + let pbody = if isCast body then surround pbody else pbody in + (str "*** [" ++ str name ++ str " " ++ + hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ + str ":" ++ brk (1,2) ++ ptyp) ++ + str "]") + +let print_named_assum name typ = + str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" + +let gallina_print_named_decl (id,c,typ) = + let s = Id.to_string id in + match c with + | Some body -> print_named_def s body typ + | None -> print_named_assum s typ + +let assumptions_for_print lna = + List.fold_right (fun na env -> add_name na env) lna empty_names_context + +(*********************) +(* *) + +let gallina_print_inductive sp = + let env = Global.env() in + let mib = Environ.lookup_mind sp env in + let mipv = mib.mind_packets in + pr_mutual_inductive_body env sp mib ++ + with_line_skip + (print_primitive_record mipv mib.mind_record @ + print_inductive_renames sp mipv @ + print_inductive_implicit_args sp mipv @ + print_inductive_argument_scopes sp mipv) + +let print_named_decl id = + gallina_print_named_decl (Global.lookup_named id) ++ fnl () + +let gallina_print_section_variable id = + print_named_decl id ++ + with_line_skip (print_name_infos (VarRef id)) + +let print_body = function + | Some c -> pr_lconstr c + | None -> (str"") + +let print_typed_body (val_0,typ) = + (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ) + +let ungeneralized_type_of_constant_type t = + Typeops.type_of_constant_type (Global.env ()) t + +let print_constant with_values sep sp = + let cb = Global.lookup_constant sp in + let val_0 = Global.body_of_constant_body cb in + let typ = Declareops.type_of_constant cb in + let typ = ungeneralized_type_of_constant_type typ in + let univs = Univ.instantiate_univ_context + (Global.universes_of_constant_body cb) + in + hov 0 (pr_polymorphic cb.const_polymorphic ++ + match val_0 with + | None -> + str"*** [ " ++ + print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ + str" ]" ++ + Printer.pr_universe_ctx univs + | _ -> + print_basename sp ++ str sep ++ cut () ++ + (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ + Printer.pr_universe_ctx univs) + +let gallina_print_constant_with_infos sp = + print_constant true " = " sp ++ + with_line_skip (print_name_infos (ConstRef sp)) + +let gallina_print_syntactic_def kn = + let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn + and (vars,a) = Syntax_def.search_syntactic_definition kn in + let c = Notation_ops.glob_constr_of_notation_constr Loc.ghost a in + hov 2 + (hov 4 + (str "Notation " ++ pr_qualid qid ++ + prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ + spc () ++ str ":=") ++ + spc () ++ + Constrextern.without_specific_symbols + [Notation.SynDefRule kn] pr_glob_constr c) + +let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = + let sep = if with_values then " = " else " : " + and tag = object_tag lobj in + match (oname,tag) with + | (_,"VARIABLE") -> + (* Outside sections, VARIABLES still exist but only with universes + constraints *) + (try Some(print_named_decl (basename sp)) with Not_found -> None) + | (_,"CONSTANT") -> + Some (print_constant with_values sep (constant_of_kn kn)) + | (_,"INDUCTIVE") -> + Some (gallina_print_inductive (mind_of_kn kn)) + | (_,"MODULE") -> + let (mp,_,l) = repr_kn kn in + Some (print_module with_values (MPdot (mp,l))) + | (_,"MODULE TYPE") -> + let (mp,_,l) = repr_kn kn in + Some (print_modtype (MPdot (mp,l))) + | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| + "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None + (* To deal with forgotten cases... *) + | (_,s) -> None + +let gallina_print_library_entry with_values ent = + let pr_name (sp,_) = pr_id (basename sp) in + match ent with + | (oname,Lib.Leaf lobj) -> + gallina_print_leaf_entry with_values (oname,lobj) + | (oname,Lib.OpenedSection (dir,_)) -> + Some (str " >>>>>>> Section " ++ pr_name oname) + | (oname,Lib.ClosedSection _) -> + Some (str " >>>>>>> Closed Section " ++ pr_name oname) + | (_,Lib.CompilingLibrary (dir,_)) -> + Some (str " >>>>>>> Library " ++ pr_dirpath dir) + | (oname,Lib.OpenedModule _) -> + Some (str " >>>>>>> Module " ++ pr_name oname) + | (oname,Lib.ClosedModule _) -> + Some (str " >>>>>>> Closed Module " ++ pr_name oname) + | (_,Lib.FrozenState _) -> + None + +let gallina_print_context with_values = + let rec prec n = function + | h::rest when Option.is_empty n || Option.get n > 0 -> + (match gallina_print_library_entry with_values h with + | None -> prec n rest + | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) + | _ -> mt () + in + prec + +let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = + let ntrm = red_fun env sigma trm in + (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) + +(******************************************) +(**** Printing abstraction layer *) + +let default_object_pr = { + print_inductive = gallina_print_inductive; + print_constant_with_infos = gallina_print_constant_with_infos; + print_section_variable = gallina_print_section_variable; + print_syntactic_def = gallina_print_syntactic_def; + print_module = gallina_print_module; + print_modtype = gallina_print_modtype; + print_named_decl = gallina_print_named_decl; + print_library_entry = gallina_print_library_entry; + print_context = gallina_print_context; + print_typed_value_in_env = gallina_print_typed_value_in_env; + print_eval = gallina_print_eval; +} + +let object_pr = ref default_object_pr +let set_object_pr = (:=) object_pr + +let print_inductive x = !object_pr.print_inductive x +let print_constant_with_infos c = !object_pr.print_constant_with_infos c +let print_section_variable c = !object_pr.print_section_variable c +let print_syntactic_def x = !object_pr.print_syntactic_def x +let print_module x = !object_pr.print_module x +let print_modtype x = !object_pr.print_modtype x +let print_named_decl x = !object_pr.print_named_decl x +let print_library_entry x = !object_pr.print_library_entry x +let print_context x = !object_pr.print_context x +let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x +let print_eval x = !object_pr.print_eval x + +(******************************************) +(**** Printing declarations and judgments *) +(**** Abstract layer *****) + +let print_typed_value x = print_typed_value_in_env (Global.env ()) Evd.empty x + +let print_judgment env sigma {uj_val=trm;uj_type=typ} = + print_typed_value_in_env env sigma (trm, typ) + +let print_safe_judgment env sigma j = + let trm = Safe_typing.j_val j in + let typ = Safe_typing.j_type j in + print_typed_value_in_env env sigma (trm, typ) + +(*********************) +(* *) + +let print_full_context () = print_context true None (Lib.contents ()) +let print_full_context_typ () = print_context false None (Lib.contents ()) + +let print_full_pure_context () = + let rec prec = function + | ((_,kn),Lib.Leaf lobj)::rest -> + let pp = match object_tag lobj with + | "CONSTANT" -> + let con = Global.constant_of_delta_kn kn in + let cb = Global.lookup_constant con in + let typ = ungeneralized_type_of_constant_type cb.const_type in + hov 0 ( + match cb.const_body with + | Undef _ -> + str "Parameter " ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype typ + | OpaqueDef lc -> + str "Theorem " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ + str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc) + | Def c -> + str "Definition " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ + pr_lconstr (Mod_subst.force_constr c)) + ++ str "." ++ fnl () ++ fnl () + | "INDUCTIVE" -> + let mind = Global.mind_of_delta_kn kn in + let mib = Global.lookup_mind mind in + pr_mutual_inductive_body (Global.env()) mind mib ++ + str "." ++ fnl () ++ fnl () + | "MODULE" -> + (* TODO: make it reparsable *) + let (mp,_,l) = repr_kn kn in + print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + | "MODULE TYPE" -> + (* TODO: make it reparsable *) + (* TODO: make it reparsable *) + let (mp,_,l) = repr_kn kn in + print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + | _ -> mt () in + prec rest ++ pp + | _::rest -> prec rest + | _ -> mt () in + prec (Lib.contents ()) + +(* For printing an inductive definition with + its constructors and elimination, + assume that the declaration of constructors and eliminations + follows the definition of the inductive type *) + +(* This is designed to print the contents of an opened section *) +let read_sec_context r = + let loc,qid = qualid_of_reference r in + let dir = + try Nametab.locate_section qid + with Not_found -> + user_err_loc (loc,"read_sec_context", str "Unknown section.") in + let rec get_cxt in_cxt = function + | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> + if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest + | (_,Lib.ClosedSection _)::rest -> + error "Cannot print the contents of a closed section." + (* LEM: Actually, we could if we wanted to. *) + | [] -> [] + | hd::rest -> get_cxt (hd::in_cxt) rest + in + let cxt = Lib.contents () in + List.rev (get_cxt [] cxt) + +let print_sec_context sec = + print_context true None (read_sec_context sec) + +let print_sec_context_typ sec = + print_context false None (read_sec_context sec) + +let print_any_name = function + | Term (ConstRef sp) -> print_constant_with_infos sp + | Term (IndRef (sp,_)) -> print_inductive sp + | Term (ConstructRef ((sp,_),_)) -> print_inductive sp + | Term (VarRef sp) -> print_section_variable sp + | Syntactic kn -> print_syntactic_def kn + | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp + | Dir _ -> mt () + | ModuleType mp -> print_modtype mp + | Tactic kn -> mt () (** TODO *) + | Undefined qid -> + try (* Var locale de but, pas var de section... donc pas d'implicits *) + let dir,str = repr_qualid qid in + if not (DirPath.is_empty dir) then raise Not_found; + let (_,c,typ) = Global.lookup_named str in + (print_named_decl (str,c,typ)) + with Not_found -> + errorlabstrm + "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") + +let print_name = function + | ByNotation (loc,ntn,sc) -> + print_any_name + (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + ntn sc)) + | AN ref -> + print_any_name (locate_any_name ref) + +let print_opaque_name qid = + let env = Global.env () in + match Nametab.global qid with + | ConstRef cst -> + let cb = Global.lookup_constant cst in + if Declareops.constant_has_body cb then + print_constant_with_infos cst + else + error "Not a defined constant." + | IndRef (sp,_) -> + print_inductive sp + | ConstructRef cstr as gr -> + let ty = Universes.unsafe_type_of_global gr in + print_typed_value (mkConstruct cstr, ty) + | VarRef id -> + let (_,c,ty) = lookup_named id env in + print_named_decl (id,c,ty) + +let print_about_any loc k = + match k with + | Term ref -> + let rb = Reductionops.ReductionBehaviour.print ref in + Dumpglob.add_glob loc ref; + pr_infos_list + (print_ref false ref :: blankline :: + print_name_infos ref @ + (if Pp.ismt rb then [] else [rb]) @ + print_opacity ref @ + [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) + | Syntactic kn -> + let () = match Syntax_def.search_syntactic_definition kn with + | [],Notation_term.NRef ref -> Dumpglob.add_glob loc ref + | _ -> () in + v 0 ( + print_syntactic_def kn ++ fnl () ++ + hov 0 (str "Expands to: " ++ pr_located_qualid k)) + | Dir _ | ModuleType _ | Tactic _ | Undefined _ -> + hov 0 (pr_located_qualid k) + +let print_about = function + | ByNotation (loc,ntn,sc) -> + print_about_any loc + (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + ntn sc)) + | AN ref -> + print_about_any (loc_of_reference ref) (locate_any_name ref) + +(* for debug *) +let inspect depth = + print_context false (Some depth) (Lib.contents ()) + + +(*************************************************************************) +(* Pretty-printing functions coming from classops.ml *) + +open Classops + +let print_coercion_value v = pr_lconstr (get_coercion_value v) + +let print_class i = + let cl,_ = class_info_from_index i in + pr_class cl + +let print_path ((i,j),p) = + hov 2 ( + str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ + str"] : ") ++ + print_class i ++ str" >-> " ++ print_class j + +let _ = Classops.install_path_printer print_path + +let print_graph () = + prlist_with_sep fnl print_path (inheritance_graph()) + +let print_classes () = + pr_sequence pr_class (classes()) + +let print_coercions () = + pr_sequence print_coercion_value (coercions()) + +let index_of_class cl = + try + fst (class_info cl) + with Not_found -> + errorlabstrm "index_of_class" + (pr_class cl ++ spc() ++ str "not a defined class.") + +let print_path_between cls clt = + let i = index_of_class cls in + let j = index_of_class clt in + let p = + try + lookup_path_between_class (i,j) + with Not_found -> + errorlabstrm "index_cl_of_id" + (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt + ++ str ".") + in + print_path ((i,j),p) + +let print_canonical_projections () = + prlist_with_sep fnl + (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ + str " <- " ++ + pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") + (canonical_projections ()) + +(*************************************************************************) + +(*************************************************************************) +(* Pretty-printing functions for type classes *) + +open Typeclasses + +let pr_typeclass env t = + print_ref false t.cl_impl + +let print_typeclasses () = + let env = Global.env () in + prlist_with_sep fnl (pr_typeclass env) (typeclasses ()) + +let pr_instance env i = + (* gallina_print_constant_with_infos i.is_impl *) + (* lighter *) + print_ref false (instance_impl i) ++ + begin match instance_priority i with + | None -> mt () + | Some i -> spc () ++ str "|" ++ spc () ++ int i + end + +let print_all_instances () = + let env = Global.env () in + let inst = all_instances () in + prlist_with_sep fnl (pr_instance env) inst + +let print_instances r = + let env = Global.env () in + let inst = instances r in + prlist_with_sep fnl (pr_instance env) inst diff --git a/printing/prettyp.mli b/printing/prettyp.mli new file mode 100644 index 00000000..6216d4d5 --- /dev/null +++ b/printing/prettyp.mli @@ -0,0 +1,77 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Termops.names_context + +val print_closed_sections : bool ref +val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds +val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option +val print_full_context : unit -> std_ppcmds +val print_full_context_typ : unit -> std_ppcmds +val print_full_pure_context : unit -> std_ppcmds +val print_sec_context : reference -> std_ppcmds +val print_sec_context_typ : reference -> std_ppcmds +val print_judgment : env -> Evd.evar_map -> unsafe_judgment -> std_ppcmds +val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds +val print_eval : + reduction_function -> env -> Evd.evar_map -> + Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds + +val print_name : reference or_by_notation -> std_ppcmds +val print_opaque_name : reference -> std_ppcmds +val print_about : reference or_by_notation -> std_ppcmds +val print_impargs : reference or_by_notation -> std_ppcmds + +(** Pretty-printing functions for classes and coercions *) +val print_graph : unit -> std_ppcmds +val print_classes : unit -> std_ppcmds +val print_coercions : unit -> std_ppcmds +val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds +val print_canonical_projections : unit -> std_ppcmds + +(** Pretty-printing functions for type classes and instances *) +val print_typeclasses : unit -> std_ppcmds +val print_instances : global_reference -> std_ppcmds +val print_all_instances : unit -> std_ppcmds + +val inspect : int -> std_ppcmds + +(** Locate *) + +val print_located_qualid : reference -> std_ppcmds +val print_located_term : reference -> std_ppcmds +val print_located_tactic : reference -> std_ppcmds +val print_located_module : reference -> std_ppcmds + +type object_pr = { + print_inductive : mutual_inductive -> std_ppcmds; + print_constant_with_infos : constant -> std_ppcmds; + print_section_variable : variable -> std_ppcmds; + print_syntactic_def : kernel_name -> std_ppcmds; + print_module : bool -> Names.module_path -> std_ppcmds; + print_modtype : module_path -> std_ppcmds; + print_named_decl : Id.t * constr option * types -> std_ppcmds; + print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; + print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; + print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds +} + +val set_object_pr : object_pr -> unit +val default_object_pr : object_pr diff --git a/printing/printer.ml b/printing/printer.ml new file mode 100644 index 00000000..3403fb9c --- /dev/null +++ b/printing/printer.ml @@ -0,0 +1,760 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (Evd.empty, Global.env()) + +(**********************************************************************) +(** Terms *) + +(* [goal_concl_style] means that all names of goal/section variables + and all names of rel variables (if any) in the given env and all short + names of global definitions of the current module must be avoided while + printing bound variables. + Otherwise, short names of global definitions are printed qualified + and only names of goal/section variables and rel names that do + _not_ occur in the scope of the binder to be printed are avoided. *) + +let pr_constr_core goal_concl_style env sigma t = + pr_constr_expr (extern_constr goal_concl_style env sigma t) +let pr_lconstr_core goal_concl_style env sigma t = + pr_lconstr_expr (extern_constr goal_concl_style env sigma t) + +let pr_lconstr_env env = pr_lconstr_core false env +let pr_constr_env env = pr_constr_core false env +let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env + +let pr_lconstr_goal_style_env env = pr_lconstr_core true env +let pr_constr_goal_style_env env = pr_constr_core true env + +let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c +let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c + + (* NB do not remove the eta-redexes! Global.env() has side-effects... *) +let pr_lconstr t = + let (sigma, env) = get_current_context () in + pr_lconstr_env env sigma t +let pr_constr t = + let (sigma, env) = get_current_context () in + pr_constr_env env sigma t + +let pr_open_lconstr (_,c) = pr_lconstr c +let pr_open_constr (_,c) = pr_constr c + +let pr_constr_under_binders_env_gen pr env sigma (ids,c) = + (* Warning: clashes can occur with variables of same name in env but *) + (* we also need to preserve the actual names of the patterns *) + (* So what to do? *) + let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in + pr (Termops.push_rels_assum assums env) sigma c + +let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env +let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env + +let pr_constr_under_binders c = + let (sigma, env) = get_current_context () in + pr_constr_under_binders_env env sigma c +let pr_lconstr_under_binders c = + let (sigma, env) = get_current_context () in + pr_lconstr_under_binders_env env sigma c + +let pr_type_core goal_concl_style env sigma t = + pr_constr_expr (extern_type goal_concl_style env sigma t) +let pr_ltype_core goal_concl_style env sigma t = + pr_lconstr_expr (extern_type goal_concl_style env sigma t) + +let pr_goal_concl_style_env env = pr_ltype_core true env +let pr_ltype_env env = pr_ltype_core false env +let pr_type_env env = pr_type_core false env + +let pr_ltype t = + let (sigma, env) = get_current_context () in + pr_ltype_env env sigma t +let pr_type t = + let (sigma, env) = get_current_context () in + pr_type_env env sigma t + +let pr_ljudge_env env sigma j = + (pr_lconstr_env env sigma j.uj_val, pr_lconstr_env env sigma j.uj_type) + +let pr_ljudge j = + let (sigma, env) = get_current_context () in + pr_ljudge_env env sigma j + +let pr_lglob_constr_env env c = + pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c) +let pr_glob_constr_env env c = + pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c) + +let pr_lglob_constr c = + let (sigma, env) = get_current_context () in + pr_lglob_constr_env env c +let pr_glob_constr c = + let (sigma, env) = get_current_context () in + pr_glob_constr_env env c + +let pr_closed_glob_env env sigma c = + pr_constr_expr (extern_closed_glob false env sigma c) +let pr_closed_glob c = + let (sigma, env) = get_current_context () in + pr_closed_glob_env env sigma c + +let pr_lconstr_pattern_env env sigma c = + pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c) +let pr_constr_pattern_env env sigma c = + pr_constr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c) + +let pr_cases_pattern t = + pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t) + +let pr_lconstr_pattern t = + let (sigma, env) = get_current_context () in + pr_lconstr_pattern_env env sigma t +let pr_constr_pattern t = + let (sigma, env) = get_current_context () in + pr_constr_pattern_env env sigma t + +let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) + +let _ = Termops.set_print_constr + (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t)) + +let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" + +(** Term printers resilient to [Nametab] errors *) + +(** When the nametab isn't up-to-date, the term printers above + could raise [Not_found] during [Nametab.shortest_qualid_of_global]. + In this case, we build here a fully-qualified name based upon + the kernel modpath and label of constants, and the idents in + the [mutual_inductive_body] for the inductives and constructors + (needs an environment for this). *) + +let id_of_global env = function + | ConstRef kn -> Label.to_id (Constant.label kn) + | IndRef (kn,0) -> Label.to_id (MutInd.label kn) + | IndRef (kn,i) -> + (Environ.lookup_mind kn env).mind_packets.(i).mind_typename + | ConstructRef ((kn,i),j) -> + (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1) + | VarRef v -> v + +let rec dirpath_of_mp = function + | MPfile sl -> sl + | MPbound uid -> DirPath.make [MBId.to_id uid] + | MPdot (mp,l) -> + Libnames.add_dirpath_suffix (dirpath_of_mp mp) (Label.to_id l) + +let dirpath_of_global = function + | ConstRef kn -> dirpath_of_mp (Constant.modpath kn) + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + dirpath_of_mp (MutInd.modpath kn) + | VarRef _ -> DirPath.empty + +let qualid_of_global env r = + Libnames.make_qualid (dirpath_of_global r) (id_of_global env r) + +let safe_gen f env sigma c = + let orig_extern_ref = Constrextern.get_extern_reference () in + let extern_ref loc vars r = + try orig_extern_ref loc vars r + with e when Errors.noncritical e -> + Libnames.Qualid (loc, qualid_of_global env r) + in + Constrextern.set_extern_reference extern_ref; + try + let p = f env sigma c in + Constrextern.set_extern_reference orig_extern_ref; + p + with e when Errors.noncritical e -> + Constrextern.set_extern_reference orig_extern_ref; + str "??" + +let safe_pr_lconstr_env = safe_gen pr_lconstr_env +let safe_pr_constr_env = safe_gen pr_constr_env +let safe_pr_lconstr t = + let (sigma, env) = get_current_context () in + safe_pr_lconstr_env env sigma t + +let safe_pr_constr t = + let (sigma, env) = get_current_context () in + safe_pr_constr_env env sigma t + +let pr_universe_ctx c = + if !Detyping.print_universes && not (Univ.UContext.is_empty c) then + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_universe_context Universes.pr_with_global_universes c)) c + else + mt() + +(**********************************************************************) +(* Global references *) + +let pr_global_env = pr_global_env +let pr_global = pr_global_env Id.Set.empty + +let pr_puniverses f env (c,u) = + f env c ++ + (if !Constrextern.print_universes then + str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" + else mt ()) + +let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) +let pr_existential_key = Evd.pr_existential_key +let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) +let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind) +let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr) + +let pr_pconstant = pr_puniverses pr_constant +let pr_pinductive = pr_puniverses pr_inductive +let pr_pconstructor = pr_puniverses pr_constructor + +let pr_evaluable_reference ref = + pr_global (Tacred.global_of_evaluable_reference ref) + +(*let pr_glob_constr t = + pr_lconstr (Constrextern.extern_glob_constr Id.Set.empty t)*) + +(*open Pattern + +let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) + +(**********************************************************************) +(* Contexts and declarations *) + +let pr_var_decl_skel pr_id env sigma (id,c,typ) = + let pbody = match c with + | None -> (mt ()) + | Some c -> + (* Force evaluation *) + let pb = pr_lconstr_env env sigma c in + let pb = if isCast c then surround pb else pb in + (str" := " ++ pb ++ cut () ) in + let pt = pr_ltype_env env sigma typ in + let ptyp = (str" : " ++ pt) in + (pr_id id ++ hov 0 (pbody ++ ptyp)) + +let pr_var_decl env sigma (id,c,typ) = + pr_var_decl_skel pr_id env sigma (id,c,typ) + +let pr_var_list_decl env sigma (l,c,typ) = + hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) + +let pr_rel_decl env sigma (na,c,typ) = + let pbody = match c with + | None -> mt () + | Some c -> + (* Force evaluation *) + let pb = pr_lconstr_env env sigma c in + let pb = if isCast c then surround pb else pb in + (str":=" ++ spc () ++ pb ++ spc ()) in + let ptyp = pr_ltype_env env sigma typ in + match na with + | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + + +(* Prints out an "env" in a nice format. We print out the + * signature,then a horizontal bar, then the debruijn environment. + * It's printed out from outermost to innermost, so it's readable. *) + +(* Prints a signature, all declarations on the same line if possible *) +let pr_named_context_of env sigma = + let make_decl_list env d pps = pr_var_decl env sigma d :: pps in + let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in + hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) + +let pr_named_context env sigma ne_context = + hv 0 (Context.fold_named_context + (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) + ne_context ~init:(mt ())) + +let pr_rel_context env sigma rel_context = + pr_binders (extern_rel_context None env sigma rel_context) + +let pr_rel_context_of env sigma = + pr_rel_context env sigma (rel_context env) + +(* Prints an env (variables and de Bruijn). Separator: newline *) +let pr_context_unlimited env sigma = + let sign_env = + Context.fold_named_list_context + (fun d pps -> + let pidt = pr_var_list_decl env sigma d in + (pps ++ fnl () ++ pidt)) + (Termops.compact_named_context (named_context env)) ~init:(mt ()) + in + let db_env = + fold_rel_context + (fun env d pps -> + let pnat = pr_rel_decl env sigma d in (pps ++ fnl () ++ pnat)) + env ~init:(mt ()) + in + (sign_env ++ db_env) + +let pr_ne_context_of header env sigma = + if List.is_empty (Environ.rel_context env) && + List.is_empty (Environ.named_context env) then (mt ()) + else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ()) + +let pr_context_limit n env sigma = + let named_context = Environ.named_context env in + let lgsign = List.length named_context in + if n >= lgsign then + pr_context_unlimited env sigma + else + let k = lgsign-n in + let _,sign_env = + Context.fold_named_list_context + (fun d (i,pps) -> + if i < k then + (i+1, (pps ++str ".")) + else + let pidt = pr_var_list_decl env sigma d in + (i+1, (pps ++ fnl () ++ + str (emacs_str "") ++ + pidt))) + (Termops.compact_named_context (Environ.named_context env)) ~init:(0,(mt ())) + in + let db_env = + fold_rel_context + (fun env d pps -> + let pnat = pr_rel_decl env sigma d in + (pps ++ fnl () ++ + str (emacs_str "") ++ + pnat)) + env ~init:(mt ()) + in + (sign_env ++ db_env) + +let pr_context_of env sigma = match Flags.print_hyps_limit () with + | None -> hv 0 (pr_context_unlimited env sigma) + | Some n -> hv 0 (pr_context_limit n env sigma) + +(* display goal parts (Proof mode) *) + +let pr_predicate pr_elt (b, elts) = + let pr_elts = prlist_with_sep spc pr_elt elts in + if b then + str"all" ++ + (if List.is_empty elts then mt () else str" except: " ++ pr_elts) + else + if List.is_empty elts then str"none" else pr_elts + +let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) +let pr_idpred p = pr_predicate Nameops.pr_id (Id.Pred.elements p) + +let pr_transparent_state (ids, csts) = + hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ + str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) + +(* display complete goal *) +let default_pr_goal gs = + let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in + let env = Goal.V82.env sigma g in + let preamb,thesis,penv,pc = + mt (), mt (), + pr_context_of env sigma, + pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) + in + preamb ++ + str" " ++ hv 0 (penv ++ fnl () ++ + str (emacs_str "") ++ + str "============================" ++ fnl () ++ + thesis ++ str " " ++ pc) + +(* display a goal tag *) +let pr_goal_tag g = + let s = " (ID " ^ Goal.uid g ^ ")" in + str (emacs_str s) + +let display_name = false + +(* display a goal name *) +let pr_goal_name sigma g = + if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma)) + else mt () + +(* display the conclusion of a goal *) +let pr_concl n sigma g = + let (g,sigma) = Goal.V82.nf_evar sigma g in + let env = Goal.V82.env sigma g in + let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in + str (emacs_str "") ++ + str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++ + str " is:" ++ cut () ++ str" " ++ pc + +(* display evar type: a context and a type *) +let pr_evgl_sign sigma evi = + let env = evar_env evi in + let ps = pr_named_context_of env sigma in + let _, l = match Filter.repr (evar_filter evi) with + | None -> [], [] + | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) + in + let ids = List.rev_map pi1 l in + let warn = + if List.is_empty ids then mt () else + (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") + in + let pc = pr_lconstr_env env sigma evi.evar_concl in + hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ spc () ++ warn) + +(* Print an existential variable *) + +let pr_evar sigma (evk, evi) = + let pegl = pr_evgl_sign sigma evi in + hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl) + +(* Print an enumerated list of existential variables *) +let rec pr_evars_int_hd head sigma i = function + | [] -> mt () + | (evk,evi)::rest -> + (hov 0 (head i ++ pr_evar sigma (evk,evi))) ++ + (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd head sigma (i+1) rest) + +let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ int i ++ str " =" ++ spc ()) sigma i (Evar.Map.bindings evs) + +let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs) + +let default_pr_subgoal n sigma = + let rec prrec p = function + | [] -> error "No such goal." + | g::rest -> + if Int.equal p 1 then + let pg = default_pr_goal { sigma=sigma ; it=g; } in + v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g + ++ str " is:" ++ cut () ++ pg) + else + prrec (p-1) rest + in + prrec n + +let pr_internal_existential_key ev = str (string_of_existential ev) + +let emacs_print_dependent_evars sigma seeds = + let evars () = + let evars = Evarutil.gather_dependent_evars sigma seeds in + let evars = + Evar.Map.fold begin fun e i s -> + let e' = pr_internal_existential_key e in + match i with + | None -> s ++ str" " ++ e' ++ str " open," + | Some i -> + s ++ str " " ++ e' ++ str " using " ++ + Evar.Set.fold begin fun d s -> + pr_internal_existential_key d ++ str " " ++ s + end i (str ",") + end evars (str "") + in + fnl () ++ + str "(dependent evars:" ++ evars ++ str ")" ++ fnl () + in + delayed_emacs_cmd evars + +(* Print open subgoals. Checks for uninstantiated existential variables *) +(* spiwack: [seeds] is for printing dependent evars in emacs mode. *) +(* spiwack: [pr_first] is true when the first goal must be singled out + and printed in its entirety. *) +(* courtieu: in emacs mode, even less cases where the first goal is printed + in its entirety *) +let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals = + (** Printing functions for the extra informations. *) + let rec print_stack a = function + | [] -> Pp.int a + | b::l -> Pp.int a ++ str"-" ++ print_stack b l + in + let print_unfocused l = + match l with + | [] -> None + | a::l -> Some (str"unfocused: " ++ print_stack a l) + in + let print_shelf l = + match l with + | [] -> None + | _ -> Some (str"shelved: " ++ Pp.int (List.length l)) + in + let rec print_comma_separated_list a l = + match l with + | [] -> a + | b::l -> print_comma_separated_list (a++str", "++b) l + in + let print_extra_list l = + match l with + | [] -> Pp.mt () + | a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")" + in + let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in + let print_extra = print_extra_list extra in + let focused_if_needed = + let needed = not (CList.is_empty extra) && pr_first in + if needed then str" focused " + else str" " (* non-breakable space *) + in + (** Main function *) + let rec pr_rec n = function + | [] -> (mt ()) + | g::rest -> + let pc = pr_concl n sigma g in + let prest = pr_rec (n+1) rest in + (cut () ++ pc ++ prest) + in + let print_multiple_goals g l = + if pr_first then + default_pr_goal { it = g ; sigma = sigma; } ++ fnl () ++ + pr_rec 2 l + else + pr_rec 1 (g::l) + in + match goals with + | [] -> + begin + match close_cmd with + Some cmd -> + (str "Subproof completed, now type " ++ str cmd ++ + str ".") + | None -> + let exl = Evarutil.non_instantiated sigma in + if Evar.Map.is_empty exl then + (str"No more subgoals." + ++ emacs_print_dependent_evars sigma seeds) + else + let pei = pr_evars_int sigma 1 exl in + (str "No more subgoals but non-instantiated existential " ++ + str "variables:" ++ fnl () ++ (hov 0 pei) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + str "You can use Grab Existential Variables.") + end + | [g] when not !Flags.print_emacs -> + let pg = default_pr_goal { it = g ; sigma = sigma; } in + v 0 ( + str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra + ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg + ++ emacs_print_dependent_evars sigma seeds + ) + | g1::rest -> + let goals = print_multiple_goals g1 rest in + v 0 ( + int(List.length rest+1) ++ focused_if_needed ++ str"subgoals" ++ + print_extra ++ + str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1") + ++ pr_goal_tag g1 + ++ pr_goal_name sigma g1 ++ cut () + ++ goals + ++ emacs_print_dependent_evars sigma seeds + ) + +(**********************************************************************) +(* Abstraction layer *) + + +type printer_pr = { + pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; + pr_goal : goal sigma -> std_ppcmds; +} + +let default_printer_pr = { + pr_subgoals = default_pr_subgoals; + pr_subgoal = default_pr_subgoal; + pr_goal = default_pr_goal; +} + +let printer_pr = ref default_printer_pr + +let set_printer_pr = (:=) printer_pr + +let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x +let pr_subgoal x = !printer_pr.pr_subgoal x +let pr_goal x = !printer_pr.pr_goal x + +(* End abstraction layer *) +(**********************************************************************) + +let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = + (* spiwack: it shouldn't be the job of the printer to look up stuff + in the [evar_map], I did stuff that way because it was more + straightforward, but seriously, [Proof.proof] should return + [evar_info]-s instead. *) + let p = proof in + let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in + let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in + let seeds = Proof.V82.top_evars p in + begin match goals with + | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in + begin match bgoals,shelf,given_up with + | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals + | [] , [] , _ -> + msg_info (str "No more goals, however there are goals you gave up. You need to go back and solve them."); + fnl () + ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up + | [] , _ , _ -> + msg_info (str "All the remaining goals are on the shelf."); + fnl () + ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf + | _ , _, _ -> + msg_info (str "This subproof is complete, but there are still unfocused goals." ++ + (match Proof_global.Bullet.suggest p + with None -> str"" | Some s -> fnl () ++ str s)); + fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals + end + | _ -> pr_subgoals None sigma seeds shelf stack goals + end + +let pr_nth_open_subgoal n = + let pf = get_pftreestate () in + let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in + pr_subgoal n sigma gls + +let pr_goal_by_id id = + let p = Proof_global.give_me_the_proof () in + let g = Goal.get_by_uid id in + let pr gs = + v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut () + ++ pr_goal gs) + in + try + Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;}) + with Not_found -> error "Invalid goal identifier." + +(* Elementary tactics *) + +let pr_prim_rule = function + | Cut (b,replace,id,t) -> + if b then + (* TODO: express "replace" *) + (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")") + else + let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in + (str"cut " ++ pr_constr t ++ + str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") + + | FixRule (f,n,[],_) -> + (str"fix " ++ pr_id f ++ str"/" ++ int n) + + | FixRule (f,n,others,j) -> + if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); + let rec print_mut = function + | (f,n,ar)::oth -> + pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth + | [] -> mt () in + (str"fix " ++ pr_id f ++ str"/" ++ int n ++ + str" with " ++ print_mut others) + + | Cofix (f,[],_) -> + (str"cofix " ++ pr_id f) + + | Cofix (f,others,j) -> + if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); + let rec print_mut = function + | (f,ar)::oth -> + (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) + | [] -> mt () in + (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) + | Refine c -> + str(if Termops.occur_meta c then "refine " else "exact ") ++ + Constrextern.with_meta_as_hole pr_constr c + + | Thin ids -> + (str"clear " ++ pr_sequence pr_id ids) + + | Move (id1,id2) -> + (str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) + +(* Backwards compatibility *) + +let prterm = pr_lconstr + + +(* Printer function for sets of Assumptions.assumptions. + It is used primarily by the Print Assumptions command. *) + +open Assumptions + +let pr_assumptionset env s = + if ContextObjectMap.is_empty s then + str "Closed under the global context" + else + let safe_pr_constant env kn = + try pr_constant env kn + with Not_found -> + let mp,_,lab = repr_con kn in + str (string_of_mp mp ^ "." ^ Label.to_string lab) + in + let safe_pr_ltype typ = + try str " : " ++ pr_ltype typ + with e when Errors.noncritical e -> mt () + in + let fold t typ accu = + let (v, a, o, tr) = accu in + match t with + | Variable id -> + let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in + (var :: v, a, o, tr) + | Axiom kn -> + let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in + (v, ax :: a, o, tr) + | Opaque kn -> + let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in + (v, a, opq :: o, tr) + | Transparent kn -> + let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in + (v, a, o, tran :: tr) + in + let (vars, axioms, opaque, trans) = + ContextObjectMap.fold fold s ([], [], [], []) + in + let opt_list title = function + | [] -> None + | l -> + let section = + title ++ fnl () ++ + v 0 (prlist_with_sep fnl (fun s -> s) l) in + Some section + in + let assums = [ + opt_list (str "Transparent constants:") trans; + opt_list (str "Section Variables:") vars; + opt_list (str "Axioms:") axioms; + opt_list (str "Opaque constants:") opaque; + ] in + prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums) + +let xor a b = + (a && not b) || (not a && b) + +let pr_polymorphic b = + let print = xor (Flags.is_universe_polymorphism ()) b in + if print then + if b then str"Polymorphic " else str"Monomorphic " + else mt () + diff --git a/printing/printer.mli b/printing/printer.mli new file mode 100644 index 00000000..6b9c7081 --- /dev/null +++ b/printing/printer.mli @@ -0,0 +1,177 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* evar_map -> constr -> std_ppcmds +val pr_lconstr : constr -> std_ppcmds +val pr_lconstr_goal_style_env : env -> evar_map -> constr -> std_ppcmds + +val pr_constr_env : env -> evar_map -> constr -> std_ppcmds +val pr_constr : constr -> std_ppcmds +val pr_constr_goal_style_env : env -> evar_map -> constr -> std_ppcmds + +(** Same, but resilient to [Nametab] errors. Prints fully-qualified + names when [shortest_qualid_of_global] has failed. Prints "??" + in case of remaining issues (such as reference not in env). *) + +val safe_pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds +val safe_pr_lconstr : constr -> std_ppcmds + +val safe_pr_constr_env : env -> evar_map -> constr -> std_ppcmds +val safe_pr_constr : constr -> std_ppcmds + + +val pr_open_constr_env : env -> evar_map -> open_constr -> std_ppcmds +val pr_open_constr : open_constr -> std_ppcmds + +val pr_open_lconstr_env : env -> evar_map -> open_constr -> std_ppcmds +val pr_open_lconstr : open_constr -> std_ppcmds + +val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds +val pr_constr_under_binders : constr_under_binders -> std_ppcmds + +val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds +val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds + +val pr_goal_concl_style_env : env -> evar_map -> types -> std_ppcmds +val pr_ltype_env : env -> evar_map -> types -> std_ppcmds +val pr_ltype : types -> std_ppcmds + +val pr_type_env : env -> evar_map -> types -> std_ppcmds +val pr_type : types -> std_ppcmds + +val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> std_ppcmds +val pr_closed_glob : closed_glob_constr -> std_ppcmds + +val pr_ljudge_env : env -> evar_map -> unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge : unsafe_judgment -> std_ppcmds * std_ppcmds + +val pr_lglob_constr_env : env -> glob_constr -> std_ppcmds +val pr_lglob_constr : glob_constr -> std_ppcmds + +val pr_glob_constr_env : env -> glob_constr -> std_ppcmds +val pr_glob_constr : glob_constr -> std_ppcmds + +val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds +val pr_lconstr_pattern : constr_pattern -> std_ppcmds + +val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds +val pr_constr_pattern : constr_pattern -> std_ppcmds + +val pr_cases_pattern : cases_pattern -> std_ppcmds + +val pr_sort : evar_map -> sorts -> std_ppcmds + +(** Universe constraints *) + +val pr_polymorphic : bool -> std_ppcmds +val pr_universe_ctx : Univ.universe_context -> std_ppcmds + +(** Printing global references using names as short as possible *) + +val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds +val pr_global : global_reference -> std_ppcmds + +val pr_constant : env -> constant -> std_ppcmds +val pr_existential_key : evar_map -> existential_key -> std_ppcmds +val pr_existential : env -> evar_map -> existential -> std_ppcmds +val pr_constructor : env -> constructor -> std_ppcmds +val pr_inductive : env -> inductive -> std_ppcmds +val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds + +val pr_pconstant : env -> pconstant -> std_ppcmds +val pr_pinductive : env -> pinductive -> std_ppcmds +val pr_pconstructor : env -> pconstructor -> std_ppcmds + + +(** Contexts *) + +val pr_context_unlimited : env -> evar_map -> std_ppcmds +val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds + +val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds +val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds +val pr_rel_decl : env -> evar_map -> rel_declaration -> std_ppcmds + +val pr_named_context : env -> evar_map -> named_context -> std_ppcmds +val pr_named_context_of : env -> evar_map -> std_ppcmds +val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds +val pr_rel_context_of : env -> evar_map -> std_ppcmds +val pr_context_of : env -> evar_map -> std_ppcmds + +(** Predicates *) + +val pr_predicate : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds +val pr_cpred : Cpred.t -> std_ppcmds +val pr_idpred : Id.Pred.t -> std_ppcmds +val pr_transparent_state : transparent_state -> std_ppcmds + +(** Proofs *) + +val pr_goal : goal sigma -> std_ppcmds +val pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds +val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds +val pr_concl : int -> evar_map -> goal -> std_ppcmds + +val pr_open_subgoals : ?proof:Proof.proof -> unit -> std_ppcmds +val pr_nth_open_subgoal : int -> std_ppcmds +val pr_evar : evar_map -> (evar * evar_info) -> std_ppcmds +val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds +val pr_evars : evar_map -> evar_info Evar.Map.t -> std_ppcmds + +val pr_prim_rule : prim_rule -> std_ppcmds + +(** Emacs/proof general support + (emacs_str s) outputs + - s if emacs mode, + - nothing otherwise. + This function was previously used to insert special chars like + [(String.make 1 (Char.chr 253))] to parenthesize sub-parts of the + proof context for proof by pointing. This part of the code is + removed for now because it interacted badly with utf8. We may put + it back some day using some xml-like tags instead of special + chars. See for example the tag in the prompt when in + emacs mode. *) +val emacs_str : string -> string + +(** Backwards compatibility *) + +val prterm : constr -> std_ppcmds (** = pr_lconstr *) + + +(** spiwack: printer function for sets of Environ.assumption. + It is used primarily by the Print Assumption command. *) +val pr_assumptionset : + env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds + +val pr_goal_by_id : string -> std_ppcmds + +type printer_pr = { + pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; + pr_goal : goal sigma -> std_ppcmds; +};; + +val set_printer_pr : printer_pr -> unit + +val default_printer_pr : printer_pr + diff --git a/printing/printing.mllib b/printing/printing.mllib new file mode 100644 index 00000000..7b4c71a8 --- /dev/null +++ b/printing/printing.mllib @@ -0,0 +1,14 @@ +Genprint +Pputils +Ppstyle +Ppannotation +Ppconstr +Ppconstrsig +Printer +Pptactic +Pptacticsig +Printmod +Prettyp +Ppvernac +Ppvernacsig +Richprinter diff --git a/printing/printmod.ml b/printing/printmod.ml new file mode 100644 index 00000000..295d8aaa --- /dev/null +++ b/printing/printmod.ml @@ -0,0 +1,438 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* !short) ; + optwrite = ((:=) short) } + +(** Each time we have to print a non-globally visible structure, + we place its elements in a fake fresh namespace. *) + +let mk_fake_top = + let r = ref 0 in + fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r)) + +module Make (Taggers : sig + val tag_definition : std_ppcmds -> std_ppcmds + val tag_keyword : std_ppcmds -> std_ppcmds +end) = +struct + +let def s = Taggers.tag_definition (str s) +let keyword s = Taggers.tag_keyword (str s) + +let get_new_id locals id = + let rec get_id l id = + let dir = DirPath.make [id] in + if not (Nametab.exists_module dir) then + id + else + get_id (id::l) (Namegen.next_ident_away id l) + in + get_id (List.map snd locals) id + +(** Inductive declarations *) + +open Termops +open Reduction + +let print_params env sigma params = + if List.is_empty params then mt () + else Printer.pr_rel_context env sigma params ++ brk(1,2) + +let print_constructors envpar names types = + let pc = + prlist_with_sep (fun () -> brk(1,0) ++ str "| ") + (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c) + (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) + in + hv 0 (str " " ++ pc) + +let build_ind_type env mip = + Inductive.type_of_inductive env mip + +let print_one_inductive env mib ((_,i) as ind) = + let u = if mib.mind_polymorphic then + Univ.UContext.instance mib.mind_universes + else Univ.Instance.empty in + let mip = mib.mind_packets.(i) in + let params = Inductive.inductive_paramdecls (mib,u) in + let args = extended_rel_list 0 params in + let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in + let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in + let envpar = push_rel_context params env in + hov 0 ( + pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++ + str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ + brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes + +let print_mutual_inductive env mind mib = + let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) + in + let keyword = + let open Decl_kinds in + match mib.mind_finite with + | Finite -> "Inductive" + | BiFinite -> "Variant" + | CoFinite -> "CoInductive" + in + hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ + def keyword ++ spc () ++ + prlist_with_sep (fun () -> fnl () ++ str" with ") + (print_one_inductive env mib) inds ++ + Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + +let get_fields = + let rec prodec_rec l subst c = + match kind_of_term c with + | Prod (na,t,c) -> + let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in + prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c + | LetIn (na,b,_,c) -> + let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in + prodec_rec ((id,false,Vars.substl subst b)::l) (mkVar id::subst) c + | _ -> List.rev l + in + prodec_rec [] [] + +let print_record env mind mib = + let u = + if mib.mind_polymorphic then + Univ.UContext.instance mib.mind_universes + else Univ.Instance.empty + in + let mip = mib.mind_packets.(0) in + let params = Inductive.inductive_paramdecls (mib,u) in + let args = extended_rel_list 0 params in + let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in + let cstrtype = hnf_prod_applist env cstrtypes.(0) args in + let fields = get_fields cstrtype in + let envpar = push_rel_context params env in + let keyword = + let open Decl_kinds in + match mib.mind_finite with + | BiFinite -> "Record" + | Finite -> "Inductive" + | CoFinite -> "CoInductive" + in + hov 0 ( + hov 0 ( + Printer.pr_polymorphic mib.mind_polymorphic ++ + def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ + print_params env Evd.empty params ++ + str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++ + str ":= " ++ pr_id mip.mind_consnames.(0)) ++ + brk(1,2) ++ + hv 2 (str "{ " ++ + prlist_with_sep (fun () -> str ";" ++ brk(2,0)) + (fun (id,b,c) -> + pr_id id ++ str (if b then " : " else " := ") ++ + Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++ + Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + +let pr_mutual_inductive_body env mind mib = + if mib.mind_record <> None && not !Flags.raw_print then + print_record env mind mib + else + print_mutual_inductive env mind mib + +(** Modpaths *) + +let rec print_local_modpath locals = function + | MPbound mbid -> pr_id (Util.List.assoc_f MBId.equal mbid locals) + | MPdot(mp,l) -> + print_local_modpath locals mp ++ str "." ++ pr_lab l + | MPfile _ -> raise Not_found + +let print_modpath locals mp = + try (* must be with let because streams are lazy! *) + let qid = Nametab.shortest_qualid_of_module mp in + pr_qualid qid + with + | Not_found -> print_local_modpath locals mp + +let print_kn locals kn = + try + let qid = Nametab.shortest_qualid_of_modtype kn in + pr_qualid qid + with + Not_found -> + try + print_local_modpath locals kn + with + Not_found -> print_modpath locals kn + +let nametab_register_dir mp = + let id = mk_fake_top () in + let dir = DirPath.make [id] in + Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty))) + +(** Nota: the [global_reference] we register in the nametab below + might differ from internal ones, since we cannot recreate here + the canonical part of constant and inductive names, but only + the user names. This works nonetheless since we search now + [Nametab.the_globrevtab] modulo user name. *) + +let nametab_register_body mp dir (l,body) = + let push id ref = + Nametab.push (Nametab.Until (1+List.length (DirPath.repr dir))) + (make_path dir id) ref + in + match body with + | SFBmodule _ -> () (* TODO *) + | SFBmodtype _ -> () (* TODO *) + | SFBconst _ -> + push (Label.to_id l) (ConstRef (Constant.make2 mp l)) + | SFBmind mib -> + let mind = MutInd.make2 mp l in + Array.iteri + (fun i mip -> + push mip.mind_typename (IndRef (mind,i)); + Array.iteri (fun j id -> push id (ConstructRef ((mind,i),j+1))) + mip.mind_consnames) + mib.mind_packets + +let nametab_register_module_body mp struc = + (* If [mp] is a globally visible module, we simply import it *) + try Declaremods.really_import_module mp + with Not_found -> + (* Otherwise we try to emulate an import by playing with nametab *) + nametab_register_dir mp; + List.iter (nametab_register_body mp DirPath.empty) struc + +let get_typ_expr_alg mtb = match mtb.mod_type_alg with + | Some (NoFunctor me) -> me + | _ -> raise Not_found + +let nametab_register_modparam mbid mtb = + match mtb.mod_type with + | MoreFunctor _ -> () (* functorial param : nothing to register *) + | NoFunctor struc -> + (* We first try to use the algebraic type expression if any, + via a Declaremods function that converts back to module entries *) + try + Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) + with e when Errors.noncritical e -> + (* Otherwise, we try to play with the nametab ourselves *) + let mp = MPbound mbid in + let dir = DirPath.make [MBId.to_id mbid] in + nametab_register_dir mp; + List.iter (nametab_register_body mp dir) struc + +let print_body is_impl env mp (l,body) = + let name = str (Label.to_string l) in + hov 2 (match body with + | SFBmodule _ -> keyword "Module" ++ spc () ++ name + | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name + | SFBconst cb -> + (match cb.const_body with + | Def _ -> def "Definition" ++ spc () + | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () + | _ -> def "Parameter" ++ spc ()) ++ name ++ + (match env with + | None -> mt () + | Some env -> + str " :" ++ spc () ++ + hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *) + (Typeops.type_of_constant_type env cb.const_type)) ++ + (match cb.const_body with + | Def l when is_impl -> + spc () ++ + hov 2 (str ":= " ++ + Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l)) + | _ -> mt ()) ++ str "." ++ + Printer.pr_universe_ctx cb.const_universes) + | SFBmind mib -> + try + let env = Option.get env in + pr_mutual_inductive_body env (MutInd.make2 mp l) mib + with e when Errors.noncritical e -> + let keyword = + let open Decl_kinds in + match mib.mind_finite with + | Finite -> def "Inductive" + | BiFinite -> def "Variant" + | CoFinite -> def "CoInductive" + in + keyword ++ spc () ++ name) + +let print_struct is_impl env mp struc = + prlist_with_sep spc (print_body is_impl env mp) struc + +let print_structure is_type env mp locals struc = + let env' = Option.map + (Modops.add_structure mp struc Mod_subst.empty_delta_resolver) env in + nametab_register_module_body mp struc; + let kwd = if is_type then "Sig" else "Struct" in + hv 2 (keyword kwd ++ spc () ++ print_struct false env' mp struc ++ + brk (1,-2) ++ keyword "End") + +let rec flatten_app mexpr l = match mexpr with + | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l) + | MEident mp -> mp::l + | MEwith _ -> assert false + +let rec print_typ_expr env mp locals mty = + match mty with + | MEident kn -> print_kn locals kn + | MEapply _ -> + let lapp = flatten_app mty [] in + let fapp = List.hd lapp in + let mapp = List.tl lapp in + hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++ + prlist_with_sep spc (print_modpath locals) mapp ++ str")") + | MEwith(me,WithDef(idl,c))-> + let env' = None in (* TODO: build a proper environment if env <> None *) + let s = String.concat "." (List.map Id.to_string idl) in + hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() + ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) + | MEwith(me,WithMod(idl,mp))-> + let s = String.concat "." (List.map Id.to_string idl) in + hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ + keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) + +let print_mod_expr env mp locals = function + | MEident mp -> print_modpath locals mp + | MEapply _ as me -> + let lapp = flatten_app me [] in + hov 3 + (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")") + | MEwith _ -> assert false (* No 'with' syntax for modules *) + +let rec print_functor fty fatom is_type env mp locals = function + |NoFunctor me -> fatom is_type env mp locals me + |MoreFunctor (mbid,mtb1,me2) -> + nametab_register_modparam mbid mtb1; + let mp1 = MPbound mbid in + let pr_mtb1 = fty env mp1 locals mtb1 in + let env' = Option.map (Modops.add_module_type mp1 mtb1) env in + let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in + let kwd = if is_type then "Funsig" else "Functor" in + hov 2 + (keyword kwd ++ spc () ++ + str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++ + spc() ++ print_functor fty fatom is_type env' mp locals' me2) + +let rec print_expression x = + print_functor + print_modtype + (function true -> print_typ_expr | false -> print_mod_expr) x + +and print_signature x = + print_functor print_modtype print_structure x + +and print_modtype env mp locals mtb = match mtb.mod_type_alg with + | Some me -> print_expression true env mp locals me + | None -> print_signature true env mp locals mtb.mod_type + +let rec printable_body dir = + let dir = pop_dirpath dir in + DirPath.is_empty dir || + try + match Nametab.locate_dir (qualid_of_dirpath dir) with + DirOpenModtype _ -> false + | DirModule _ | DirOpenModule _ -> printable_body dir + | _ -> true + with + Not_found -> true + +(** Since we might play with nametab above, we should reset to prior + state after the printing *) + +let print_expression' is_type env mp me = + States.with_state_protection + (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me + +let print_signature' is_type env mp me = + States.with_state_protection + (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me + +let unsafe_print_module env mp with_body mb = + let name = print_modpath [] mp in + let pr_equals = spc () ++ str ":= " in + let body = match with_body, mb.mod_expr with + | false, _ + | true, Abstract -> mt() + | _, Algebraic me -> pr_equals ++ print_expression' false env mp me + | _, Struct sign -> pr_equals ++ print_signature' false env mp sign + | _, FullStruct -> pr_equals ++ print_signature' false env mp mb.mod_type + in + let modtype = match mb.mod_expr, mb.mod_type_alg with + | FullStruct, _ -> mt () + | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true env mp ty + | _, _ -> brk (1,1) ++ str": " ++ print_signature' true env mp mb.mod_type + in + hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body) + +exception ShortPrinting + +let print_module with_body mp = + let me = Global.lookup_module mp in + try + if !short then raise ShortPrinting; + unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl () + with e when Errors.noncritical e -> + unsafe_print_module None mp with_body me ++ fnl () + +let print_modtype kn = + let mtb = Global.lookup_modtype kn in + let name = print_kn [] kn in + hv 1 + (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++ + (try + if !short then raise ShortPrinting; + print_signature' true (Some (Global.env ())) kn mtb.mod_type + with e when Errors.noncritical e -> + print_signature' true None kn mtb.mod_type)) + +end + +module Tag = +struct + let definition = + let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in + Ppstyle.make ~style ["module"; "definition"] + let keyword = + let style = Terminal.make ~bold:true () in + Ppstyle.make ~style ["module"; "keyword"] +end + +include Make(struct + let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s + let tag_definition s = tag Tag.definition s + let tag_keyword s = tag Tag.keyword s +end) diff --git a/printing/printmod.mli b/printing/printmod.mli new file mode 100644 index 00000000..bea47534 --- /dev/null +++ b/printing/printmod.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool + +include Printmodsig.Pp diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli new file mode 100644 index 00000000..5d0d4ab0 --- /dev/null +++ b/printing/printmodsig.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds + val print_module : bool -> module_path -> std_ppcmds + val print_modtype : module_path -> std_ppcmds +end diff --git a/printing/richprinter.ml b/printing/richprinter.ml new file mode 100644 index 00000000..d71dc82d --- /dev/null +++ b/printing/richprinter.ml @@ -0,0 +1,26 @@ +open Richpp + +module RichppConstr = Ppconstr.Richpp +module RichppVernac = Ppvernac.Richpp +module RichppTactic = Pptactic.Richpp + +type rich_pp = + string + * Ppannotation.t Richpp.located Xml_datatype.gxml + * Xml_datatype.xml + +let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag + +let make_richpp pr ast = + let raw_pp, rich_pp = + rich_pp get_annotations (pr ast) + in + let xml = Ppannotation.( + xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp + ) + in + (raw_pp, rich_pp, xml) + +let richpp_vernac = make_richpp RichppVernac.pr_vernac +let richpp_constr = make_richpp RichppConstr.pr_constr_expr +let richpp_tactic env = make_richpp (RichppTactic.pr_tactic env) diff --git a/printing/richprinter.mli b/printing/richprinter.mli new file mode 100644 index 00000000..c67d52c0 --- /dev/null +++ b/printing/richprinter.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* rich_pp + +(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *) +val richpp_constr : Constrexpr.constr_expr -> rich_pp + +(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *) +val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp -- cgit v1.2.3