aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/dune6
-rw-r--r--printing/genprint.ml155
-rw-r--r--printing/genprint.mli54
-rw-r--r--printing/ppconstr.ml721
-rw-r--r--printing/ppconstr.mli81
-rw-r--r--printing/pputils.ml109
-rw-r--r--printing/pputils.mli30
-rw-r--r--printing/prettyp.ml956
-rw-r--r--printing/prettyp.mli99
-rw-r--r--printing/printer.ml1002
-rw-r--r--printing/printer.mli209
-rw-r--r--printing/printing.mllib7
-rw-r--r--printing/printmod.ml460
-rw-r--r--printing/printmod.mli20
-rw-r--r--printing/proof_diffs.ml649
-rw-r--r--printing/proof_diffs.mli84
16 files changed, 4642 insertions, 0 deletions
diff --git a/printing/dune b/printing/dune
new file mode 100644
index 0000000000..3392342165
--- /dev/null
+++ b/printing/dune
@@ -0,0 +1,6 @@
+(library
+ (name printing)
+ (synopsis "Coq's Term Pretty Printing Library")
+ (public_name coq.printing)
+ (wrapped false)
+ (libraries parsing proofs))
diff --git a/printing/genprint.ml b/printing/genprint.ml
new file mode 100644
index 0000000000..fa53a87945
--- /dev/null
+++ b/printing/genprint.ml
@@ -0,0 +1,155 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open Genarg
+open Geninterp
+
+(* We register printers at two levels:
+ - generic arguments for general printers
+ - generic values for printing ltac values *)
+
+(* Printing generic values *)
+
+type 'a with_level =
+ { default_already_surrounded : Notation_gram.tolerability;
+ default_ensure_surrounded : Notation_gram.tolerability;
+ printer : 'a }
+
+type printer_result =
+| PrinterBasic of (unit -> Pp.t)
+| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
+
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
+
+type top_printer_result =
+| TopPrinterBasic of (unit -> Pp.t)
+| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
+
+type 'a printer = 'a -> printer_result
+
+type 'a top_printer = 'a -> top_printer_result
+
+module ValMap = ValTMap (struct type 'a t = 'a -> top_printer_result end)
+
+let print0_val_map = ref ValMap.empty
+
+let find_print_val_fun tag =
+ try ValMap.find tag !print0_val_map
+ with Not_found ->
+ let msg s = Pp.(str "print function not found for a value interpreted as " ++ str s ++ str ".") in
+ CErrors.anomaly (msg (Val.repr tag))
+
+let generic_val_print v =
+ let Val.Dyn (tag,v) = v in
+ find_print_val_fun tag v
+
+let register_val_print0 s pr =
+ print0_val_map := ValMap.add s pr !print0_val_map
+
+let combine_dont_needs pr_pair pr1 = function
+ | TopPrinterBasic pr2 ->
+ TopPrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ()))
+ | TopPrinterNeedsContext pr2 ->
+ TopPrinterNeedsContext (fun env sigma ->
+ pr_pair (pr1 ()) (pr2 env sigma))
+ | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+ TopPrinterNeedsContext (fun env sigma ->
+ pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded))
+
+let combine_needs pr_pair pr1 = function
+ | TopPrinterBasic pr2 ->
+ TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ()))
+ | TopPrinterNeedsContext pr2 ->
+ TopPrinterNeedsContext (fun env sigma ->
+ pr_pair (pr1 env sigma) (pr2 env sigma))
+ | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+ TopPrinterNeedsContext (fun env sigma ->
+ pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded))
+
+let combine pr_pair pr1 v2 =
+ match pr1 with
+ | TopPrinterBasic pr1 ->
+ combine_dont_needs pr_pair pr1 (generic_val_print v2)
+ | TopPrinterNeedsContext pr1 ->
+ combine_needs pr_pair pr1 (generic_val_print v2)
+ | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+ combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded)
+ (generic_val_print v2)
+
+let _ =
+ let pr_cons a b = Pp.(a ++ spc () ++ b) in
+ register_val_print0 Val.typ_list
+ (function
+ | [] -> TopPrinterBasic mt
+ | a::l ->
+ List.fold_left (combine pr_cons) (generic_val_print a) l)
+
+let _ =
+ register_val_print0 Val.typ_opt
+ (function
+ | None -> TopPrinterBasic Pp.mt
+ | Some v -> generic_val_print v)
+
+let _ =
+ let pr_pair a b = Pp.(a ++ spc () ++ b) in
+ register_val_print0 Val.typ_pair
+ (fun (v1,v2) -> combine pr_pair (generic_val_print v1) v2)
+
+(* Printing generic arguments *)
+
+type ('raw, 'glb, 'top) genprinter = {
+ raw : 'raw -> printer_result;
+ glb : 'glb -> printer_result;
+ top : 'top -> top_printer_result;
+}
+
+module PrintObj =
+struct
+ type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) genprinter
+ let name = "printer"
+ let default wit = match wit with
+ | ExtraArg tag ->
+ let name = ArgT.repr tag in
+ let printer = {
+ raw = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+ glb = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+ top = (fun _ -> TopPrinterBasic (fun () -> str "<genarg:" ++ str name ++ 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;
+ match val_tag (Topwit wit), wit with
+ | Val.Base t, ExtraArg t' when Geninterp.Val.repr t = ArgT.repr t' ->
+ register_val_print0 t top
+ | _ ->
+ (* An alias, thus no primitive printer attached *)
+ ()
+
+let register_vernac_print0 wit raw =
+ let glb _ = CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.") in
+ let top _ = CErrors.anomaly (Pp.str "vernac argument needs not wit printer.") in
+ 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 (GenArg (Rawwit w, v)) = raw_print w v
+let generic_glb_print (GenArg (Glbwit w, v)) = glb_print w v
+let generic_top_print (GenArg (Topwit w, v)) = top_print w v
diff --git a/printing/genprint.mli b/printing/genprint.mli
new file mode 100644
index 0000000000..1a31025a9a
--- /dev/null
+++ b/printing/genprint.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Entry point for generic printers *)
+
+open Genarg
+
+type 'a with_level =
+ { default_already_surrounded : Notation_gram.tolerability;
+ default_ensure_surrounded : Notation_gram.tolerability;
+ printer : 'a }
+
+type printer_result =
+| PrinterBasic of (unit -> Pp.t)
+| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
+
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
+
+type top_printer_result =
+| TopPrinterBasic of (unit -> Pp.t)
+| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
+
+type 'a printer = 'a -> printer_result
+
+type 'a top_printer = 'a -> top_printer_result
+
+val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer
+(** Printer for raw level generic arguments. *)
+
+val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb printer
+(** Printer for glob level generic arguments. *)
+
+val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer
+(** Printer for top level generic arguments. *)
+
+val register_print0 : ('raw, 'glb, 'top) genarg_type ->
+ 'raw printer -> 'glb printer -> 'top top_printer -> unit
+val register_val_print0 : 'top Geninterp.Val.typ ->
+ 'top top_printer -> unit
+val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type ->
+ 'raw printer -> unit
+
+val generic_raw_print : rlevel generic_argument printer
+val generic_glb_print : glevel generic_argument printer
+val generic_top_print : tlevel generic_argument top_printer
+val generic_val_print : Geninterp.Val.t top_printer
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
new file mode 100644
index 0000000000..26202ef4ca
--- /dev/null
+++ b/printing/ppconstr.ml
@@ -0,0 +1,721 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(*i*)
+open CErrors
+open Util
+open Pp
+open CAst
+open Names
+open Libnames
+open Pputils
+open Ppextend
+open Glob_term
+open Constrexpr
+open Constrexpr_ops
+open Notation_gram
+open Decl_kinds
+open Namegen
+(*i*)
+
+module Tag =
+struct
+ let keyword = "constr.keyword"
+ let evar = "constr.evar"
+ let univ = "constr.type"
+ let notation = "constr.notation"
+ let variable = "constr.variable"
+ let reference = "constr.reference"
+ let path = "constr.path"
+
+end
+
+let do_not_tag _ x = x
+let tag t s = Pp.tag t 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
+
+
+ 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 (_,b) -> if b then lposint else lnegint
+ | String _ -> latom
+
+ let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
+ let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists 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
+ | UnpBinderMetaVar (_, prec) as unp :: l ->
+ let c = pop bl in
+ let pp2 = aux l in
+ let pp1 = pr_patt (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 (List.map snd 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_patt pr_binders s env =
+ let unpl, level = find_notation_printing_rule s in
+ print_hunks level pr pr_patt 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.beautify && not (Int.equal n 0) then comment (Pputils.extract_comments 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 ?loc:(constr_loc c) (sep() ++ f c)
+
+ let pr_univ_expr = function
+ | Some (x,n) ->
+ pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+ | None -> str"_"
+
+ let pr_univ l =
+ match l with
+ | [x] -> pr_univ_expr x
+ | l -> str"max(" ++ prlist_with_sep (fun () -> str",") pr_univ_expr l ++ str")"
+
+ let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
+
+ let pr_glob_sort = let open Glob_term in 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_glob_level = let open Glob_term in function
+ | GProp -> tag_type (str "Prop")
+ | GSet -> tag_type (str "Set")
+ | GType UUnknown -> tag_type (str "Type")
+ | GType UAnonymous -> tag_type (str "_")
+ | GType (UNamed u) -> tag_type (pr_qualid u)
+
+ let pr_qualid sp =
+ let (sl, id) = repr_qualid sp in
+ let id = tag_ref (Id.print id) in
+ let sl = match List.rev (DirPath.repr sl) with
+ | [] -> mt ()
+ | sl ->
+ let pr dir = tag_path (Id.print dir) ++ str "." in
+ prlist pr sl
+ in
+ sl ++ id
+
+ let pr_id = Id.print
+ let pr_qualid = pr_qualid
+ let pr_patvar = pr_id
+
+ let pr_glob_sort_instance = let open Glob_term in function
+ | GProp ->
+ tag_type (str "Prop")
+ | GSet ->
+ tag_type (str "Set")
+ | GType u ->
+ (match u with
+ | UNamed u -> pr_qualid u
+ | UAnonymous -> tag_type (str "Type")
+ | UUnknown -> tag_type (str "_"))
+
+ let pr_universe_instance l =
+ pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
+
+ let pr_reference qid =
+ if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid)
+ else pr_qualid qid
+
+ 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 {v=ExplByPos (n,_id)} ->
+ anomaly (Pp.str "Explicitation by position not implemented.")
+ | Some {v=ExplByName id} ->
+ str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
+
+ let pr_opt_type_spc pr = function
+ | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt ()
+ | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
+
+ let pr_prim_token = function
+ | Numeral (n,s) -> str (if s then n else "-"^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 CAst.(p.v) 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, na) ->
+ pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las
+
+ | CPatCstr (c, None, []) ->
+ pr_reference c, latom
+
+ | CPatCstr (c, None, args) ->
+ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+
+ | CPatCstr (c, Some args, []) ->
+ str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+
+ | CPatCstr (c, Some 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_spcbar (pr_patt mt (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 ()) (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
+ | CPatCast _ ->
+ assert false
+ in
+ let loc = p.CAst.loc 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;v=(pl,rhs)} =
+ spc() ++ hov 4
+ (pr_with_comments ?loc
+ (str "| " ++
+ hov 0 (prlist_with_sep pr_spcbar (prlist_with_sep sep_v (pr_patt ltop)) pl
+ ++ str " =>") ++
+ pr_sep_com spc (pr ltop) rhs))
+
+ let begin_of_binder l_bi =
+ let b_loc l = fst (Option.cata Loc.unloc (0,0) l) in
+ match l_bi with
+ | CLocalDef({loc},_,_) -> b_loc loc
+ | CLocalAssum({loc}::_,_,_) -> b_loc loc
+ | CLocalPattern{loc} -> b_loc 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; v=Anonymous}] ->
+ hov 1 (str"`" ++ (surround_impl b'
+ ((if t' then str "!" else mt ()) ++ pr t)))
+ |[{loc; v=Name id}] ->
+ hov 1 (str "`" ++ (surround_impl b'
+ (pr_lident CAst.(make ?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
+ | { CAst.v = CHole (_,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
+ | CLocalAssum (nal,k,t) ->
+ pr_binder true pr_c (nal,k,t)
+ | CLocalDef (na,c,topt) ->
+ surround (pr_lname na ++
+ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++
+ str" :=" ++ spc() ++ pr_c c)
+ | CLocalPattern {CAst.loc; v = p,tyo} ->
+ let p = pr_patt lsimplepatt p in
+ match tyo with
+ | None ->
+ str "'" ++ p
+ | Some ty ->
+ str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty)
+
+ 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
+ | [CLocalAssum (nal,k,t)] ->
+ kw n ++ pr_binder false pr_c (nal,k,t)
+ | (CLocalAssum _ | CLocalPattern _ | CLocalDef _) :: _ as bdl ->
+ kw n ++ pr_undelimited_binders sep pr_c bdl
+ | [] -> anomaly (Pp.str "The ast is malformed, found lambda/prod without proper binders.")
+
+ let pr_binders_gen pr_c sep is_open =
+ if is_open then pr_delimited_binders pr_com_at sep pr_c
+ else pr_undelimited_binders sep pr_c
+
+ 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 ++ (if bl = [] then mt () else 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; v = id} ->
+ match (ro : Constrexpr.recursion_order_expr) with
+ | CStructRec ->
+ let names_of_binder = function
+ | CLocalAssum (nal,_,_) -> nal
+ | CLocalDef (_,_,_) -> []
+ | CLocalPattern _ -> assert false
+ 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 ({v=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 ({v=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,as_clause, in_clause) =
+ hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause)
+
+ let pr_case_type pr po =
+ match po with
+ | None | Some { CAst.v = CHole (_,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 {v=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_record_body_gen pr l =
+ spc () ++
+ prlist_with_sep pr_semicolon
+ (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l
+
+ let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc ()
+
+ let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc ()
+
+ let pr_fun_sep = spc () ++ str "=>"
+
+ let pr_dangling_with_for sep pr inherited a =
+ match a.v 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 CAst.(a.v) 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)) id.v fix),
+ lfix
+ )
+ | CCoFix (id,cofix) ->
+ return (
+ hov 0 (keyword "cofix" ++ spc () ++
+ pr_recursive
+ (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix),
+ lfix
+ )
+ | CProdN (bl,a) ->
+ return (
+ hov 0 (
+ hov 2 (pr_delimited_binders pr_forall spc
+ (pr mt ltop) bl) ++
+ str "," ++ pr spc ltop a),
+ lprod
+ )
+ | CLambdaN (bl,a) ->
+ return (
+ hov 0 (
+ hov 2 (pr_delimited_binders pr_fun spc
+ (pr mt ltop) bl) ++
+ pr_fun_sep ++ pr spc ltop a),
+ llambda
+ )
+ | CLetIn ({v=Name x}, ({ v = CFix({v=x'},[_])}
+ | { v = CCoFix({v=x'},[_]) } as fx), t, 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,t,b) ->
+ return (
+ hv 0 (
+ hov 2 (keyword "let" ++ spc () ++ pr_lname x
+ ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr mt ltop t) t
+ ++ 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,qid,us),[t])
+ | CApp ((_, {v = CRef(qid,us)}),[t,None])
+ when qualid_is_ident qid && Id.equal (qualid_basename qid) 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 l ->
+ return (
+ hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
+ latom
+ )
+ | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
+ return (
+ hv 0 (
+ keyword "let" ++ spc () ++ str"'" ++
+ hov 0 (pr_patt ltop p ++
+ pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++
+ 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 (
+ hov 2 (keyword "let" ++ spc () ++
+ hov 1 (str "(" ++
+ prlist_with_sep sep_v pr_lname nal ++
+ str ")" ++
+ pr_simple_return_type (pr mt) na po ++ str " :=") ++
+ pr spc ltop c
+ ++ 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 (_,IntroIdentifier id,_) ->
+ return (str "?[" ++ pr_id id ++ str "]", latom)
+ | CHole (_,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 ++ spc () ++
+ match b with
+ | CastConv b -> str ":" ++ ws 1 ++ pr mt (-lcast,E) b
+ | CastVM b -> str "<:" ++ ws 1 ++ pr mt (-lcast,E) b
+ | CastNative b -> str "<<:" ++ ws 1 ++ 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_patt (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 -> Pp.t;
+ pr_lconstr_expr : constr_expr -> Pp.t;
+ pr_constr_pattern_expr : constr_pattern_expr -> Pp.t;
+ pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
+ }
+
+ let modular_constr_pr = pr
+ let rec fix rf x = rf (fix rf) x
+ let pr = fix modular_constr_pr mt
+
+ let pr prec = function
+ (* A toplevel printer hack mimicking parsing, incidentally meaning
+ that we cannot use [pr] correctly anymore in a recursive loop
+ if the current expr is followed by other exprs which would be
+ interpreted as arguments *)
+ | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us
+ | c -> pr prec c
+
+ let transf env sigma c =
+ if !Flags.beautify_file then
+ let r = Constrintern.for_grammar (Constrintern.intern_constr env sigma) c in
+ Constrextern.extern_glob_constr (Termops.vars_of_env env) r
+ else c
+
+ let pr_expr prec c =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr prec (transf env sigma c)
+
+ let pr_simpleconstr = pr_expr lsimpleconstr
+
+ let default_term_pr = {
+ pr_constr_expr = pr_simpleconstr;
+ pr_lconstr_expr = pr_expr ltop;
+ pr_constr_pattern_expr = pr_simpleconstr;
+ pr_lconstr_pattern_expr = pr_expr ltop
+ }
+
+ let term_pr = ref default_term_pr
+
+ let set_term_pr = (:=) term_pr
+
+ let pr_constr_expr_n n c = pr_expr n c
+ 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_record_body = pr_record_body_gen pr
+
+ let pr_binders = pr_undelimited_binders spc (pr_expr ltop)
+
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
new file mode 100644
index 0000000000..1cb3aa6d7a
--- /dev/null
+++ b/printing/ppconstr.mli
@@ -0,0 +1,81 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** This module implements pretty-printers for constr_expr syntactic
+ objects and their subcomponents. *)
+
+(** The default pretty-printers produce pretty-printing commands ({!Pp.t}). *)
+open Libnames
+open Constrexpr
+open Names
+open Notation_gram
+
+val prec_less : precedence -> tolerability -> bool
+
+val pr_tight_coma : unit -> Pp.t
+
+val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
+val pr_com_at : int -> Pp.t
+val pr_sep_com :
+ (unit -> Pp.t) ->
+ (constr_expr -> Pp.t) ->
+ constr_expr -> Pp.t
+
+val pr_id : Id.t -> Pp.t
+
+val pr_qualid : qualid -> Pp.t
+val pr_patvar : Pattern.patvar -> Pp.t
+
+val pr_glob_level : Glob_term.glob_level -> Pp.t
+val pr_glob_sort : Glob_term.glob_sort -> Pp.t
+val pr_guard_annot : (constr_expr -> Pp.t) ->
+ local_binder_expr list ->
+ lident option * recursion_order_expr ->
+ Pp.t
+
+val pr_record_body : (qualid * constr_expr) list -> Pp.t
+val pr_binders : local_binder_expr list -> Pp.t
+val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t
+val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
+val pr_constr_expr : constr_expr -> Pp.t
+val pr_lconstr_expr : constr_expr -> Pp.t
+val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t
+val pr_constr_expr_n : tolerability -> constr_expr -> Pp.t
+
+type term_pr = {
+ pr_constr_expr : constr_expr -> Pp.t;
+ pr_lconstr_expr : constr_expr -> Pp.t;
+ pr_constr_pattern_expr : constr_pattern_expr -> Pp.t;
+ pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
+}
+
+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. *)
+
+val lsimpleconstr : tolerability
+val ltop : tolerability
+val modular_constr_pr :
+ ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) ->
+ (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t
diff --git a/printing/pputils.ml b/printing/pputils.ml
new file mode 100644
index 0000000000..e6daf9544c
--- /dev/null
+++ b/printing/pputils.ml
@@ -0,0 +1,109 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Util
+open Pp
+open Genarg
+open Locus
+
+let beautify_comments = ref []
+
+let rec split_comments comacc acc pos = function
+ | [] -> beautify_comments := List.rev acc; comacc
+ | ((b,e),c as com)::coms ->
+ (* Take all comments that terminates before pos, or begin exactly
+ at pos (used to print comments attached after an expression) *)
+ if e<=pos || pos=b then split_comments (c::comacc) acc pos coms
+ else split_comments comacc (com::acc) pos coms
+
+let extract_comments pos = split_comments [] [] pos !beautify_comments
+
+let pr_located pr (loc, x) =
+ match loc with
+ | Some loc when !Flags.beautify ->
+ let (b, e) = Loc.unloc loc in
+ (* Side-effect: order matters *)
+ let before = Pp.comment (extract_comments b) in
+ let x = pr x in
+ let after = Pp.comment (extract_comments e) in
+ before ++ x ++ after
+ | _ -> pr x
+
+let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v)
+
+let pr_lident { CAst.loc; v=id } =
+ let open Names.Id in
+ match loc with
+ | None -> print id
+ | Some loc -> let (b,_) = Loc.unloc loc in
+ pr_located print
+ (Some (Loc.make_loc (b,b + String.length (to_string id))), id)
+
+let pr_lname = let open Names in function
+ | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id)
+ | x -> pr_ast Name.print x
+
+let pr_or_var pr = function
+ | ArgArg x -> pr x
+ | ArgVar id -> pr_lident id
+
+let pr_or_by_notation f = let open Constrexpr in CAst.with_val (function
+ | AN v -> f v
+ | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
+
+let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
+
+let rec pr_raw_generic env (GenArg (Rawwit wit, x)) =
+ match wit with
+ | ListArg wit ->
+ let map x = pr_raw_generic env (in_gen (rawwit wit) x) in
+ let ans = pr_sequence map x in
+ hov_if_not_empty 0 ans
+ | OptArg wit ->
+ let ans = match x with
+ | None -> mt ()
+ | Some x -> pr_raw_generic env (in_gen (rawwit wit) x)
+ in
+ hov_if_not_empty 0 ans
+ | PairArg (wit1, wit2) ->
+ let p, q = x in
+ let p = in_gen (rawwit wit1) p in
+ let q = in_gen (rawwit wit2) q in
+ hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q])
+ | ExtraArg s ->
+ let open Genprint in
+ match generic_raw_print (in_gen (rawwit wit) x) with
+ | PrinterBasic pp -> pp ()
+ | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
+
+
+let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
+ match wit with
+ | ListArg wit ->
+ let map x = pr_glb_generic env (in_gen (glbwit wit) x) in
+ let ans = pr_sequence map x in
+ hov_if_not_empty 0 ans
+ | OptArg wit ->
+ let ans = match x with
+ | None -> mt ()
+ | Some x -> pr_glb_generic env (in_gen (glbwit wit) x)
+ in
+ hov_if_not_empty 0 ans
+ | PairArg (wit1, wit2) ->
+ let p, q = x in
+ let p = in_gen (glbwit wit1) p in
+ let q = in_gen (glbwit wit2) q in
+ let ans = pr_sequence (pr_glb_generic env) [p; q] in
+ hov_if_not_empty 0 ans
+ | ExtraArg s ->
+ let open Genprint in
+ match generic_glb_print (in_gen (glbwit wit) x) with
+ | PrinterBasic pp -> pp ()
+ | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
diff --git a/printing/pputils.mli b/printing/pputils.mli
new file mode 100644
index 0000000000..ea554355bc
--- /dev/null
+++ b/printing/pputils.mli
@@ -0,0 +1,30 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Genarg
+
+val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t
+val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t
+(** Prints an object surrounded by its commented location *)
+
+val pr_lident : lident -> Pp.t
+val pr_lname : lname -> Pp.t
+val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
+val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t
+
+val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t
+val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t
+
+(* The comments interface is imperative due to the printer not
+ threading it, this could be solved using a better data
+ structure. *)
+val beautify_comments : ((int * int) * string) list ref
+val extract_comments : int -> string list
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
new file mode 100644
index 0000000000..c417ef8a66
--- /dev/null
+++ b/printing/prettyp.ml
@@ -0,0 +1,956 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu>
+ * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
+ *)
+
+open Pp
+open CErrors
+open Util
+open CAst
+open Names
+open Nameops
+open Termops
+open Declarations
+open Environ
+open Impargs
+open Libobject
+open Libnames
+open Globnames
+open Recordops
+open Printer
+open Printmod
+open Context.Rel.Declaration
+
+(* module RelDecl = Context.Rel.Declaration *)
+module NamedDecl = Context.Named.Declaration
+
+type object_pr = {
+ print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
+ print_syntactic_def : env -> KerName.t -> Pp.t;
+ print_module : bool -> ModPath.t -> Pp.t;
+ print_modtype : ModPath.t -> Pp.t;
+ print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
+ print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
+ print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
+ print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
+ print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
+}
+
+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 udecl =
+ let env = Global.env () in
+ let typ, univs = Typeops.type_of_global_in_context env ref in
+ let inst = Univ.make_abstract_instance univs in
+ let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
+ let sigma = Evd.from_ctx (UState.of_binders bl) in
+ let typ = EConstr.of_constr typ in
+ let typ =
+ if reduce then
+ let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
+ in EConstr.it_mkProd_or_LetIn ccl ctx
+ else typ in
+ let variance = match ref with
+ | VarRef _ | ConstRef _ -> None
+ | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
+ let mind = Environ.lookup_mind ind env in
+ begin match mind.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None
+ | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi)
+ end
+ in
+ let inst =
+ if Global.is_polymorphic ref
+ then Printer.pr_universe_instance sigma inst
+ else mt ()
+ in
+ let priv = None in (* We deliberately don't print private univs in About. *)
+ hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++
+ Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv)
+
+(********************************)
+(** Printing implicit arguments *)
+
+let pr_impl_name imp = Id.print (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 "no more 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 Name.print l))]
+
+let need_expansion impl ref =
+ let typ, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
+ let ctx = Term.prod_assum typ in
+ let nprods = List.count is_local_assum 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 None;
+ 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 NamedDecl.is_local_def (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 " ++
+ match s with
+ | FullyOpaque -> str "opaque"
+ | TransparentMaybeOpacified Conv_oracle.Opaque ->
+ str "basically transparent but considered opaque for reduction"
+ | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
+ str "transparent"
+ | TransparentMaybeOpacified (Conv_oracle.Level n) ->
+ str "transparent (with expansion weight " ++ int n ++ str ")"
+ | TransparentMaybeOpacified Conv_oracle.Expand ->
+ str "transparent (with minimal expansion weight)"]
+
+(*******************)
+
+let print_if_is_coercion ref =
+ if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+
+(*******************)
+(* *)
+
+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_type_in_type ref =
+ let unsafe = Global.is_type_in_type ref in
+ if unsafe then
+ [ pr_global ref ++ str " relies on an unsafe universe hierarchy"]
+ else []
+
+let print_primitive_record recflag mipv = function
+ | PrimRecord _ ->
+ let eta = match recflag with
+ | CoFinite | Finite -> str" without eta conversion"
+ | BiFinite -> str " with eta conversion"
+ in
+ [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
+ | FakeRecord | NotRecord -> []
+
+let print_primitive ref =
+ match ref with
+ | IndRef ind ->
+ let mib,_ = Global.lookup_inductive ind in
+ print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record
+ | _ -> []
+
+let print_name_infos ref =
+ let impls = implicits_of_global ref in
+ let scopes = Notation.find_arguments_scope ref in
+ let renames =
+ try 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 None; blankline]
+ else
+ [] in
+ print_polymorphism ref @
+ print_type_in_type ref @
+ print_primitive ref @
+ type_info_for_implicit @
+ print_renames_list (mt()) renames @
+ print_impargs_list (mt()) impls @
+ print_argument_scopes (mt()) scopes @
+ print_if_is_coercion ref
+
+let print_id_args_data test pr id l =
+ if List.exists test l then
+ pr (str "For " ++ Id.print 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 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 'a locatable_info = {
+ locate : qualid -> 'a option;
+ locate_all : qualid -> 'a list;
+ shortest_qualid : 'a -> qualid;
+ name : 'a -> Pp.t;
+ print : 'a -> Pp.t;
+ about : 'a -> Pp.t;
+}
+
+type locatable = Locatable : 'a locatable_info -> locatable
+
+type logical_name =
+ | Term of GlobRef.t
+ | Dir of Nametab.GlobDirRef.t
+ | Syntactic of KerName.t
+ | ModuleType of ModPath.t
+ | Other : 'a * 'a locatable_info -> logical_name
+ | Undefined of qualid
+
+(** Generic table for objects that are accessible through a name. *)
+let locatable_map : locatable String.Map.t ref = ref String.Map.empty
+
+let register_locatable name f =
+ locatable_map := String.Map.add name (Locatable f) !locatable_map
+
+exception ObjFound of logical_name
+
+let locate_any_name qid =
+ 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 ->
+ let iter _ (Locatable info) = match info.locate qid with
+ | None -> ()
+ | Some ans -> raise (ObjFound (Other (ans, info)))
+ in
+ try String.Map.iter iter !locatable_map; Undefined qid
+ with ObjFound obj -> obj
+
+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 =
+ let open Nametab in
+ let open GlobDirRef in match dir with
+ | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir
+ | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir
+ | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir
+ | DirModule { obj_dir ; _ } -> "Module", obj_dir
+ in
+ str s ++ spc () ++ DirPath.print dir
+ | ModuleType mp ->
+ str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp)
+ | Other (obj, info) -> info.name obj
+ | 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_module qid =
+ let all = Nametab.locate_extended_all_dir qid in
+ let map dir = let open Nametab.GlobDirRef in match dir with
+ | DirModule { Nametab.obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_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 = let open Nametab.GlobDirRef in match dir with
+ | DirOpenModtype _ -> Some (Dir dir, qid)
+ | _ -> None
+ in
+ modtypes @ List.map_filter map all
+
+let locate_other s qid =
+ let Locatable info = String.Map.find s !locatable_map in
+ let ans = info.locate_all qid in
+ let map obj = (Other (obj, info), info.shortest_qualid obj) in
+ List.map map ans
+
+type locatable_kind =
+| LocTerm
+| LocModule
+| LocOther of string
+| LocAny
+
+let print_located_qualid name flags qid =
+ let located = match flags with
+ | LocTerm -> locate_term qid
+ | LocModule -> locate_modtype qid @ locate_module qid
+ | LocOther s -> locate_other s qid
+ | LocAny ->
+ locate_term qid @
+ locate_modtype qid @
+ locate_module qid @
+ String.Map.fold (fun s _ accu -> locate_other s qid @ accu) !locatable_map []
+ in
+ match located with
+ | [] ->
+ let (dir,id) = repr_qualid qid in
+ if DirPath.is_empty dir then
+ str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id
+ else
+ str "No " ++ str name ++ str " 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" LocTerm ref
+let print_located_other s ref = print_located_qualid s (LocOther s) ref
+let print_located_module ref = print_located_qualid "module" LocModule ref
+let print_located_qualid ref = print_located_qualid "object" LocAny ref
+
+(******************************************)
+(**** Printing declarations and judgments *)
+(**** Gallina layer *****)
+
+let gallina_print_typed_value_in_env env sigma (trm,typ) =
+ (pr_leconstr_env env sigma trm ++ fnl () ++
+ str " : " ++ pr_letype_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 env sigma name body typ =
+ let pbody = pr_lconstr_env env sigma body in
+ let ptyp = pr_ltype_env env sigma typ in
+ let pbody = if Constr.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 env sigma name typ =
+ str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]"
+
+let gallina_print_named_decl env sigma =
+ let open Context.Named.Declaration in
+ function
+ | LocalAssum (id, typ) ->
+ print_named_assum env sigma (Id.to_string id) typ
+ | LocalDef (id, body, typ) ->
+ print_named_def env sigma (Id.to_string id) body 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 udecl =
+ 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 udecl ++
+ with_line_skip
+ (print_primitive_record mib.mind_finite 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 env sigma id =
+ gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl ()
+
+let gallina_print_section_variable env sigma id =
+ print_named_decl env sigma id ++
+ with_line_skip (print_name_infos (VarRef id))
+
+let print_body env evd = function
+ | Some c -> pr_lconstr_env env evd c
+ | None -> (str"<no body>")
+
+let print_typed_body env evd (val_0,typ) =
+ (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ)
+
+let print_instance sigma cb =
+ if Declareops.constant_is_polymorphic cb then
+ let univs = Declareops.constant_polymorphic_context cb in
+ let inst = Univ.make_abstract_instance univs in
+ pr_universe_instance sigma inst
+ else mt()
+
+let print_constant with_values sep sp udecl =
+ let cb = Global.lookup_constant sp in
+ let val_0 = Global.body_of_constant_body cb in
+ let typ = cb.const_type in
+ let univs =
+ let open Univ in
+ let otab = Global.opaque_tables () in
+ match cb.const_body with
+ | Undef _ | Def _ -> cb.const_universes
+ | OpaqueDef o ->
+ let body_uctxs = Opaqueproof.force_constraints otab o in
+ match cb.const_universes with
+ | Monomorphic_const ctx ->
+ Monomorphic_const (ContextSet.union body_uctxs ctx)
+ | Polymorphic_const ctx ->
+ assert(ContextSet.is_empty body_uctxs);
+ Polymorphic_const ctx
+ in
+ let ctx =
+ UState.of_binders
+ (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl)
+ in
+ let env = Global.env () and sigma = Evd.from_ctx ctx in
+ let pr_ltype = pr_ltype_env env sigma in
+ hov 0 (
+ match val_0 with
+ | None ->
+ str"*** [ " ++
+ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
+ str" ]" ++
+ Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs
+ | Some (c, ctx) ->
+ print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
+ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
+ Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs)
+
+let gallina_print_constant_with_infos sp udecl =
+ print_constant true " = " sp udecl ++
+ with_line_skip (print_name_infos (ConstRef sp))
+
+let gallina_print_syntactic_def env 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 a in
+ hov 2
+ (hov 4
+ (str "Notation " ++ pr_qualid qid ++
+ prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++
+ spc () ++ str ":=") ++
+ spc () ++
+ Constrextern.without_specific_symbols
+ [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
+
+let gallina_print_leaf_entry env sigma 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 env sigma (basename sp)) with Not_found -> None)
+ | (_,"CONSTANT") ->
+ Some (print_constant with_values sep (Constant.make1 kn) None)
+ | (_,"INDUCTIVE") ->
+ Some (gallina_print_inductive (MutInd.make1 kn) None)
+ | (_,"MODULE") ->
+ let (mp,l) = KerName.repr kn in
+ Some (print_module with_values (MPdot (mp,l)))
+ | (_,"MODULE TYPE") ->
+ let (mp,l) = KerName.repr 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 env sigma with_values ent =
+ let pr_name (sp,_) = Id.print (basename sp) in
+ match ent with
+ | (oname,Lib.Leaf lobj) ->
+ gallina_print_leaf_entry env sigma with_values (oname,lobj)
+ | (oname,Lib.OpenedSection (dir,_)) ->
+ Some (str " >>>>>>> Section " ++ pr_name oname)
+ | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) ->
+ Some (str " >>>>>>> Library " ++ DirPath.print obj_dir)
+ | (oname,Lib.OpenedModule _) ->
+ Some (str " >>>>>>> Module " ++ pr_name oname)
+
+let gallina_print_context env sigma with_values =
+ let rec prec n = function
+ | h::rest when Option.is_empty n || Option.get n > 0 ->
+ (match gallina_print_library_entry env sigma 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_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
+ let trm = EConstr.of_constr trm in
+ let typ = EConstr.of_constr typ in
+ print_typed_value_in_env env sigma (trm, typ)
+
+(*********************)
+(* *)
+
+let print_full_context env sigma = print_context env sigma true None (Lib.contents ())
+let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ())
+
+let print_full_pure_context env sigma =
+ 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 = cb.const_type in
+ hov 0 (
+ match cb.const_body with
+ | Undef _ ->
+ str "Parameter " ++
+ print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ
+ | OpaqueDef lc ->
+ str "Theorem " ++ print_basename con ++ cut () ++
+ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
+ str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof (Global.opaque_tables ()) lc)
+ | Def c ->
+ str "Definition " ++ print_basename con ++ cut () ++
+ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
+ pr_lconstr_env env sigma (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 None ++
+ str "." ++ fnl () ++ fnl ()
+ | "MODULE" ->
+ (* TODO: make it reparsable *)
+ let (mp,l) = KerName.repr kn in
+ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+ | "MODULE TYPE" ->
+ (* TODO: make it reparsable *)
+ (* TODO: make it reparsable *)
+ let (mp,l) = KerName.repr 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 qid =
+ let dir =
+ try Nametab.locate_section qid
+ with Not_found ->
+ user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in
+ let rec get_cxt in_cxt = function
+ | (_,Lib.OpenedSection ({Nametab.obj_dir;_},_) as hd)::rest ->
+ if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+ | [] -> []
+ | hd::rest -> get_cxt (hd::in_cxt) rest
+ in
+ let cxt = Lib.contents () in
+ List.rev (get_cxt [] cxt)
+
+let print_sec_context env sigma sec =
+ print_context env sigma true None (read_sec_context sec)
+
+let print_sec_context_typ env sigma sec =
+ print_context env sigma false None (read_sec_context sec)
+
+let maybe_error_reject_univ_decl na udecl =
+ match na, udecl with
+ | _, None | Term (ConstRef _ | IndRef _ | ConstructRef _), Some _ -> ()
+ | (Term (VarRef _) | Syntactic _ | Dir _ | ModuleType _ | Other _ | Undefined _), Some udecl ->
+ (* TODO Print na somehow *)
+ user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.")
+
+let print_any_name env sigma na udecl =
+ maybe_error_reject_univ_decl na udecl;
+ match na with
+ | Term (ConstRef sp) -> print_constant_with_infos sp udecl
+ | Term (IndRef (sp,_)) -> print_inductive sp udecl
+ | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl
+ | Term (VarRef sp) -> print_section_variable env sigma sp
+ | Syntactic kn -> print_syntactic_def env kn
+ | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp
+ | Dir _ -> mt ()
+ | ModuleType mp -> print_modtype mp
+ | Other (obj, info) -> info.print obj
+ | 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;
+ str |> Global.lookup_named |> print_named_decl env sigma
+
+ with Not_found ->
+ user_err
+ ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
+
+let print_name env sigma na udecl =
+ match na with
+ | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
+ print_any_name env sigma
+ (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+ ntn sc))
+ udecl
+ | {loc; v=Constrexpr.AN ref} ->
+ print_any_name env sigma (locate_any_name ref) udecl
+
+let print_opaque_name env sigma qid =
+ 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 None
+ else
+ user_err Pp.(str "Not a defined constant.")
+ | IndRef (sp,_) ->
+ print_inductive sp None
+ | ConstructRef cstr as gr ->
+ let ty, ctx = Typeops.type_of_global_in_context env gr in
+ let ty = EConstr.of_constr ty in
+ let open EConstr in
+ print_typed_value_in_env env sigma (mkConstruct cstr, ty)
+ | VarRef id ->
+ env |> lookup_named id |> print_named_decl env sigma
+
+let print_about_any ?loc env sigma k udecl =
+ maybe_error_reject_univ_decl k udecl;
+ match k with
+ | Term ref ->
+ let rb = Reductionops.ReductionBehaviour.print ref in
+ Dumpglob.add_glob ?loc ref;
+ pr_infos_list
+ (print_ref false ref udecl :: 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 env kn ++ fnl () ++
+ hov 0 (str "Expands to: " ++ pr_located_qualid k))
+ | Dir _ | ModuleType _ | Undefined _ ->
+ hov 0 (pr_located_qualid k)
+ | Other (obj, info) -> hov 0 (info.about obj)
+
+let print_about env sigma na udecl =
+ match na with
+ | {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
+ print_about_any ?loc env sigma
+ (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+ ntn sc)) udecl
+ | {loc;v=Constrexpr.AN ref} ->
+ print_about_any ?loc env sigma (locate_any_name ref) udecl
+
+(* for debug *)
+let inspect env sigma depth =
+ print_context env sigma false (Some depth) (Lib.contents ())
+
+
+(*************************************************************************)
+(* Pretty-printing functions coming from classops.ml *)
+
+open Classops
+
+let print_coercion_value v = Printer.pr_global v.coe_value
+
+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 ->
+ user_err ~hdr:"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 ->
+ user_err ~hdr:"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 env sigma =
+ prlist_with_sep fnl
+ (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
+ str " <- " ++
+ pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma 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 None
+
+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) None ++
+ begin match hint_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 0000000000..9213bc8561
--- /dev/null
+++ b/printing/prettyp.mli
@@ -0,0 +1,99 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Environ
+open Reductionops
+open Libnames
+
+(** A Pretty-Printer for the Calculus of Inductive Constructions. *)
+
+val assumptions_for_print : Name.t list -> Termops.names_context
+
+val print_closed_sections : bool ref
+val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t
+val print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option
+val print_full_context : env -> Evd.evar_map -> Pp.t
+val print_full_context_typ : env -> Evd.evar_map -> Pp.t
+val print_full_pure_context : env -> Evd.evar_map -> Pp.t
+val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t
+val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t
+val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t
+val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
+val print_eval :
+ reduction_function -> env -> Evd.evar_map ->
+ Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
+
+val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
+ UnivNames.univ_name_list option -> Pp.t
+val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t
+val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
+ UnivNames.univ_name_list option -> Pp.t
+val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
+
+(** Pretty-printing functions for classes and coercions *)
+val print_graph : unit -> Pp.t
+val print_classes : unit -> Pp.t
+val print_coercions : unit -> Pp.t
+val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
+val print_canonical_projections : env -> Evd.evar_map -> Pp.t
+
+(** Pretty-printing functions for type classes and instances *)
+val print_typeclasses : unit -> Pp.t
+val print_instances : GlobRef.t -> Pp.t
+val print_all_instances : unit -> Pp.t
+
+val inspect : env -> Evd.evar_map -> int -> Pp.t
+
+(** {5 Locate} *)
+
+type 'a locatable_info = {
+ locate : qualid -> 'a option;
+ (** Locate the most precise object with the provided name if any. *)
+ locate_all : qualid -> 'a list;
+ (** Locate all objects whose name is a suffix of the provided name *)
+ shortest_qualid : 'a -> qualid;
+ (** Return the shortest name in the current context *)
+ name : 'a -> Pp.t;
+ (** Data as printed by the Locate command *)
+ print : 'a -> Pp.t;
+ (** Data as printed by the Print command *)
+ about : 'a -> Pp.t;
+ (** Data as printed by the About command *)
+}
+(** Generic data structure representing locatable objects. *)
+
+val register_locatable : string -> 'a locatable_info -> unit
+(** Define a new type of locatable objects that can be reached via the
+ corresponding generic vernacular commands. The string should be a unique
+ name describing the kind of objects considered and that is added as a
+ grammar command prefix for vernacular commands Locate. *)
+
+val print_located_qualid : qualid -> Pp.t
+val print_located_term : qualid -> Pp.t
+val print_located_module : qualid -> Pp.t
+val print_located_other : string -> qualid -> Pp.t
+
+type object_pr = {
+ print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
+ print_syntactic_def : env -> KerName.t -> Pp.t;
+ print_module : bool -> ModPath.t -> Pp.t;
+ print_modtype : ModPath.t -> Pp.t;
+ print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
+ print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option;
+ print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
+ print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
+ print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
+}
+
+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 0000000000..3f7837fd6e
--- /dev/null
+++ b/printing/printer.ml
@@ -0,0 +1,1002 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Constr
+open Environ
+open Globnames
+open Evd
+open Refiner
+open Constrextern
+open Ppconstr
+open Declarations
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+module CompactedDecl = Context.Compacted.Declaration
+
+let enable_unfocused_goal_printing = ref false
+let enable_goal_tags_printing = ref false
+let enable_goal_names_printing = ref false
+
+let should_tag() = !enable_goal_tags_printing
+let should_unfoc() = !enable_unfocused_goal_printing
+let should_gname() = !enable_goal_names_printing
+
+
+let () =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "printing of unfocused goal";
+ optkey = ["Printing";"Unfocused"];
+ optread = (fun () -> !enable_unfocused_goal_printing);
+ optwrite = (fun b -> enable_unfocused_goal_printing:=b) }
+
+(* This is set on by proofgeneral proof-tree mode. But may be used for
+ other purposes *)
+let () =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "printing of goal tags";
+ optkey = ["Printing";"Goal";"Tags"];
+ optread = (fun () -> !enable_goal_tags_printing);
+ optwrite = (fun b -> enable_goal_tags_printing:=b) }
+
+
+let () =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "printing of goal names";
+ optkey = ["Printing";"Goal";"Names"];
+ optread = (fun () -> !enable_goal_names_printing);
+ optwrite = (fun b -> enable_goal_names_printing:=b) }
+
+
+(**********************************************************************)
+(** 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_econstr_n_core goal_concl_style env sigma n t =
+ pr_constr_expr_n n (extern_constr goal_concl_style env sigma t)
+let pr_econstr_core goal_concl_style env sigma t =
+ pr_constr_expr (extern_constr goal_concl_style env sigma t)
+let pr_leconstr_core = Proof_diffs.pr_leconstr_core
+
+let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c)
+let pr_lconstr_env = Proof_diffs.pr_lconstr_env
+let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c)
+
+let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c)
+let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c)
+
+let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c
+let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c
+let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
+
+let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c
+let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma 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_econstr_env
+let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env
+
+let pr_etype_core goal_concl_style env sigma t =
+ pr_constr_expr (extern_type goal_concl_style env sigma t)
+let pr_letype_core = Proof_diffs.pr_letype_core
+
+let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c)
+let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c)
+
+let pr_etype_env env sigma c = pr_etype_core false env sigma c
+let pr_letype_env env sigma c = pr_letype_core false env sigma c
+let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c
+
+let pr_ljudge_env env sigma j =
+ (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
+
+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_closed_glob_n_env env sigma n c =
+ pr_constr_expr_n n (extern_closed_glob false env sigma c)
+let pr_closed_glob_env env sigma c =
+ pr_constr_expr (extern_closed_glob false 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_sort sigma s = pr_glob_sort (extern_sort sigma s)
+
+let () = Termops.Internal.set_print_constr
+ (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
+
+let pr_in_comment x = str "(* " ++ 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 ?loc env r =
+ Libnames.make_qualid ?loc (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 vars r
+ with e when CErrors.noncritical e ->
+ qualid_of_global ?loc 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 CErrors.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 pr_universe_ctx_set sigma c =
+ if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
+ fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c))
+ else
+ mt()
+
+let pr_universe_ctx sigma ?variance c =
+ if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
+ fnl()++pr_in_comment (v 0 (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c))
+ else
+ mt()
+
+let pr_abstract_universe_ctx sigma ?variance c ~priv =
+ let open Univ in
+ let priv = Option.default Univ.ContextSet.empty priv in
+ let has_priv = not (ContextSet.is_empty priv) in
+ if !Detyping.print_universes && (not (Univ.AUContext.is_empty c) || has_priv) then
+ let prlev u = Termops.pr_evd_level sigma u in
+ let pub = (if has_priv then str "Public universes:" ++ fnl() else mt()) ++ v 0 (Univ.pr_abstract_universe_context prlev ?variance c) in
+ let priv = if has_priv then fnl() ++ str "Private universes:" ++ fnl() ++ v 0 (Univ.pr_universe_context_set prlev priv) else mt() in
+ fnl()++pr_in_comment (pub ++ priv)
+ else
+ mt()
+
+let pr_constant_universes sigma ~priv = function
+ | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx
+ | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv
+
+let pr_cumulativity_info sigma cumi =
+ if !Detyping.print_universes
+ && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
+ fnl()++pr_in_comment (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi))
+ else
+ mt()
+
+let pr_abstract_cumulativity_info sigma cumi =
+ if !Detyping.print_universes
+ && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then
+ fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi))
+ else
+ mt()
+
+(**********************************************************************)
+(* Global references *)
+
+let pr_global_env = Nametab.pr_global_env
+let pr_global = pr_global_env Id.Set.empty
+
+let pr_universe_instance_constraints evd inst csts =
+ let open Univ in
+ let prlev = Termops.pr_evd_level evd in
+ let pcsts = if Constraint.is_empty csts then mt()
+ else str " |= " ++
+ prlist_with_sep (fun () -> str "," ++ spc())
+ (fun (u,d,v) -> hov 0 (prlev u ++ pr_constraint_type d ++ prlev v))
+ (Constraint.elements csts)
+ in
+ str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}"
+
+let pr_universe_instance evd inst =
+ pr_universe_instance_constraints evd inst Univ.Constraint.empty
+
+let pr_puniverses f env sigma (c,u) =
+ if !Constrextern.print_universes
+ then f env c ++ pr_universe_instance sigma u
+ else f env c
+
+let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
+let pr_existential_key = Termops.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.from_env env) (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (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 *)
+
+
+(* Flag for compact display of goals *)
+
+let get_compact_context,set_compact_context =
+ let compact_context = ref false in
+ (fun () -> !compact_context),(fun b -> compact_context := b)
+
+let pr_compacted_decl env sigma decl =
+ let ids, pbody, typ = match decl with
+ | CompactedDecl.LocalAssum (ids, typ) ->
+ ids, mt (), typ
+ | CompactedDecl.LocalDef (ids,c,typ) ->
+ (* Force evaluation *)
+ let pb = pr_lconstr_env env sigma c in
+ let pb = if isCast c then surround pb else pb in
+ ids, (str" := " ++ pb ++ cut ()), typ
+ in
+ let pids = prlist_with_sep pr_comma pr_id ids in
+ let pt = pr_ltype_env env sigma typ in
+ let ptyp = (str" : " ++ pt) in
+ hov 0 (pids ++ pbody ++ ptyp)
+
+let pr_named_decl env sigma decl =
+ decl |> CompactedDecl.of_named_decl |> pr_compacted_decl env sigma
+
+let pr_rel_decl env sigma decl =
+ let na = RelDecl.get_name decl in
+ let typ = RelDecl.get_type decl in
+ let pbody = match decl with
+ | RelDecl.LocalAssum _ -> mt ()
+ | RelDecl.LocalDef (_,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_named_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_var_list_decl env sigma decl =
+ hov 0 (pr_compacted_decl env sigma decl)
+
+let pr_named_context env sigma ne_context =
+ hv 0 (Context.Named.fold_outside
+ (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d)
+ ne_context ~init:(mt ()))
+
+let pr_rel_context env sigma rel_context =
+ let rel_context = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) rel_context in
+ 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.Compacted.fold
+ (fun d pps ->
+ let pidt = pr_compacted_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 ())
+
+(* Heuristic for horizontalizing hypothesis that the user probably
+ considers as "variables": An hypothesis H:T where T:S and S<>Prop. *)
+let should_compact env sigma typ =
+ get_compact_context() &&
+ let type_of_typ = Retyping.get_type_of env sigma (EConstr.of_constr typ) in
+ not (is_Prop (EConstr.to_constr sigma type_of_typ))
+
+
+(* If option Compact Contexts is set, we pack "simple" hypothesis in a
+ hov box (with three sapaces as a separator), the global box being a
+ v box *)
+let rec bld_sign_env env sigma ctxt pps =
+ match ctxt with
+ | [] -> pps
+ | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ ->
+ let pps',ctxt' = bld_sign_env_id env sigma ctxt (mt ()) true in
+ (* putting simple hyps in a more horizontal flavor *)
+ bld_sign_env env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps')
+ | d:: ctxt' ->
+ let pidt = pr_var_list_decl env sigma d in
+ let pps' = pps ++ brk (0,0) ++ pidt in
+ bld_sign_env env sigma ctxt' pps'
+and bld_sign_env_id env sigma ctxt pps is_start =
+ match ctxt with
+ | [] -> pps,ctxt
+ | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
+ let pidt = pr_var_list_decl env sigma d in
+ let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in
+ bld_sign_env_id env sigma ctxt' pps' false
+ | _ -> pps,ctxt
+
+
+(* compact printing an env (variables and de Bruijn). Separator: three
+ spaces between simple hyps, and newline otherwise *)
+let pr_context_limit_compact ?n env sigma =
+ let ctxt = Termops.compact_named_context (named_context env) in
+ let lgth = List.length ctxt in
+ let n_capped =
+ match n with
+ | None -> lgth
+ | Some n when n > lgth -> lgth
+ | Some n -> n in
+ let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in
+ (* a dot line hinting the number of hidden hyps. *)
+ let hidden_dots = String.make (List.length ctxt_hidden) '.' in
+ let sign_env = v 0 (str hidden_dots ++ (mt ())
+ ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in
+ let db_env =
+ fold_rel_context (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d)
+ env ~init:(mt ()) in
+ sign_env ++ db_env
+
+(* The number of printed hypothesis in a goal *)
+(* If [None], no limit *)
+let print_hyps_limit = ref (None : int option)
+
+let () =
+ let open Goptions in
+ declare_int_option
+ { optdepr = false;
+ optname = "the hypotheses limit";
+ optkey = ["Hyps";"Limit"];
+ optread = (fun () -> !print_hyps_limit);
+ optwrite = (fun x -> print_hyps_limit := x) }
+
+let pr_context_of env sigma = match !print_hyps_limit with
+ | None -> hv 0 (pr_context_limit_compact env sigma)
+ | Some n -> hv 0 (pr_context_limit_compact ~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 Id.print (Id.Pred.elements p)
+
+let pr_transparent_state ts =
+ hv 0 (str"VARIABLES: " ++ pr_idpred ts.TransparentState.tr_var ++ fnl () ++
+ str"CONSTANTS: " ++ pr_cpred ts.TransparentState.tr_cst ++ fnl ())
+
+(* display complete goal
+ og_s has goal+sigma on the previous proof step for diffs
+ g_s has goal+sigma on the current proof step
+ *)
+let pr_goal ?(diffs=false) ?og_s g_s =
+ let g = sig_it g_s in
+ let sigma = project g_s in
+ let env = Goal.V82.env sigma g in
+ let concl = Goal.V82.concl sigma g in
+ let goal =
+ if diffs then
+ Proof_diffs.diff_goal ?og_s g sigma
+ else
+ pr_context_of env sigma ++ cut () ++
+ str "============================" ++ cut () ++
+ pr_goal_concl_style_env env sigma concl
+ in
+ str " " ++ v 0 goal
+
+(* display a goal tag *)
+let pr_goal_tag g =
+ let s = " (ID " ^ Goal.uid g ^ ")" in
+ str s
+
+(* display a goal name *)
+let pr_goal_name sigma g =
+ if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g)
+ else mt ()
+
+let pr_goal_header nme sigma g =
+ let (g,sigma) = Goal.V82.nf_evar sigma g in
+ str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
+ ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
+
+(* display the conclusion of a goal *)
+let pr_concl n ?(diffs=false) ?og_s sigma g =
+ let (g,sigma) = Goal.V82.nf_evar sigma g in
+ let env = Goal.V82.env sigma g in
+ let pc =
+ if diffs then
+ Proof_diffs.diff_concl ?og_s sigma g
+ else
+ pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
+ in
+ let header = pr_goal_header (int n) sigma g in
+ header ++ 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 NamedDecl.get_id 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_leconstr_env env sigma evi.evar_concl in
+ let candidates =
+ match evi.evar_body, evi.evar_candidates with
+ | Evar_empty, Some l ->
+ spc () ++ str "= {" ++
+ prlist_with_sep (fun () -> str "|") (pr_leconstr_env env sigma) l ++ str "}"
+ | _ ->
+ mt ()
+ in
+ hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++
+ candidates ++ 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 pr sigma i = function
+ | [] -> mt ()
+ | (evk,evi)::rest ->
+ (hov 0 (pr i evk evi)) ++
+ (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest)
+
+let pr_evars_int sigma ~shelf ~given_up i evs =
+ let pr_status i =
+ if List.mem i shelf then str " (shelved)"
+ else if List.mem i given_up then str " (given up)"
+ else mt () in
+ pr_evars_int_hd
+ (fun i evk evi ->
+ str "Existential " ++ int i ++ str " =" ++
+ spc () ++ pr_evar sigma (evk,evi) ++ pr_status evk)
+ sigma i (Evar.Map.bindings evs)
+
+let pr_evars sigma evs =
+ pr_evars_int_hd (fun i evk evi -> pr_evar sigma (evk,evi)) sigma 1 (Evar.Map.bindings evs)
+
+(* Display a list of evars given by their name, with a prefix *)
+let pr_ne_evar_set hd tl sigma l =
+ if l != Evar.Set.empty then
+ let l = Evar.Set.fold (fun ev ->
+ Evar.Map.add ev (Evarutil.nf_evar_info sigma (Evd.find sigma ev)))
+ l Evar.Map.empty in
+ hd ++ pr_evars sigma l ++ tl
+ else
+ mt ()
+
+let pr_selected_subgoal name sigma g =
+ let pg = pr_goal { sigma=sigma ; it=g; } in
+ let header = pr_goal_header name sigma g in
+ v 0 (header ++ str " is:" ++ cut () ++ pg)
+
+let pr_subgoal n sigma =
+ let rec prrec p = function
+ | [] -> user_err Pp.(str "No such goal.")
+ | g::rest ->
+ if Int.equal p 1 then
+ pr_selected_subgoal (int n) sigma g
+ else
+ prrec (p-1) rest
+ in
+ prrec n
+
+let pr_internal_existential_key ev = Evar.print ev
+
+let print_evar_constraints gl sigma =
+ let pr_env =
+ match gl with
+ | None -> fun e' -> pr_context_of e' sigma
+ | Some g ->
+ let env = Goal.V82.env sigma g in fun e' ->
+ begin
+ if Context.Named.equal Constr.equal (named_context env) (named_context e') then
+ if Context.Rel.equal Constr.equal (rel_context env) (rel_context e') then mt ()
+ else pr_rel_context_of e' sigma ++ str " |-" ++ spc ()
+ else pr_context_of e' sigma ++ str " |-" ++ spc ()
+ end
+ in
+ let pr_evconstr (pbty,env,t1,t2) =
+ let t1 = Evarutil.nf_evar sigma t1
+ and t2 = Evarutil.nf_evar sigma t2 in
+ let env =
+ (* We currently allow evar instances to refer to anonymous de Bruijn
+ indices, so we protect the error printing code in this case by giving
+ names to every de Bruijn variable in the rel_context of the conversion
+ problem. MS: we should rather stop depending on anonymous variables, they
+ can be used to indicate independency. Also, this depends on a strategy for
+ naming/renaming *)
+ Namegen.make_all_name_different env sigma in
+ str" " ++
+ hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++
+ str (match pbty with
+ | Reduction.CONV -> "=="
+ | Reduction.CUMUL -> "<=") ++
+ spc () ++ pr_leconstr_env env sigma t2)
+ in
+ let pr_candidate ev evi (candidates,acc) =
+ if Option.has_some evi.evar_candidates then
+ (succ candidates, acc ++ pr_evar sigma (ev,evi) ++ fnl ())
+ else (candidates, acc)
+ in
+ let constraints =
+ let _, cstrs = Evd.extract_all_conv_pbs sigma in
+ if List.is_empty cstrs then mt ()
+ else fnl () ++ str (String.plural (List.length cstrs) "unification constraint")
+ ++ str":" ++ fnl () ++ hov 0 (prlist_with_sep fnl pr_evconstr cstrs)
+ in
+ let candidates, ppcandidates = Evd.fold_undefined pr_candidate sigma (0,mt ()) in
+ constraints ++
+ if candidates > 0 then
+ fnl () ++ str (String.plural candidates "existential") ++
+ str" with candidates:" ++ fnl () ++ hov 0 ppcandidates
+ else mt ()
+
+let should_print_dependent_evars = ref false
+
+let () =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "Printing Dependent Evars Line";
+ optkey = ["Printing";"Dependent";"Evars";"Line"];
+ optread = (fun () -> !should_print_dependent_evars);
+ optwrite = (fun v -> should_print_dependent_evars := v) }
+
+let print_dependent_evars gl sigma seeds =
+ let constraints = print_evar_constraints gl sigma in
+ let evars () =
+ if !should_print_dependent_evars then
+ 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
+ cut () ++ cut () ++
+ str "(dependent evars:" ++ evars ++ str ")"
+ else mt ()
+ in
+ constraints ++ evars ()
+
+module GoalMap = Evar.Map
+
+(* 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. *)
+(* [os_map] is derived from the previous proof step, used for diffs *)
+let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
+ close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals =
+ let diff_goal_map =
+ match os_map with
+ | Some (_, diff_goal_map) -> diff_goal_map
+ | None -> GoalMap.empty
+ in
+
+ (* 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_nums 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_nums 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
+
+ let get_ogs g =
+ match os_map with
+ | Some (osigma, _) ->
+ (* if Not_found, returning None treats the goal as new and it will be diff highlighted;
+ returning Some { it = g; sigma = sigma } will compare the new goal
+ to itself and it won't be highlighted *)
+ (try Some { it = GoalMap.find g diff_goal_map; sigma = osigma }
+ with Not_found -> None)
+ | None -> None
+ in
+ let rec pr_rec n = function
+ | [] -> (mt ())
+ | g::rest ->
+ let og_s = get_ogs g in
+ let pc = pr_concl n ~diffs ?og_s 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
+ let og_s = get_ogs g in
+ pr_goal ~diffs ?og_s { it = g ; sigma = sigma }
+ ++ (if l=[] then mt () else cut ())
+ ++ pr_rec 2 l
+ else
+ pr_rec 1 (g::l)
+ in
+ (* Side effect! This has to be made more robust *)
+ let () =
+ match close_cmd with
+ | Some cmd -> Feedback.msg_info cmd
+ | None -> ()
+ in
+
+ (* Main function *)
+ match goals with
+ | [] ->
+ begin
+ let exl = Evd.undefined_map sigma in
+ if Evar.Map.is_empty exl then
+ (str"No more subgoals." ++ print_dependent_evars None sigma seeds)
+ else
+ let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in
+ v 0 ((str "No more subgoals,"
+ ++ str " but there are non-instantiated existential variables:"
+ ++ cut () ++ (hov 0 pei)
+ ++ print_dependent_evars None sigma seeds
+ ++ cut () ++ str "You can use Grab Existential Variables."))
+ end
+ | g1::rest ->
+ let goals = print_multiple_goals g1 rest in
+ let ngoals = List.length rest+1 in
+ v 0 (
+ int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
+ ++ print_extra
+ ++ str (if (should_gname()) then ", subgoal 1" else "")
+ ++ (if should_tag() then pr_goal_tag g1 else str"")
+ ++ pr_goal_name sigma g1 ++ cut () ++ goals
+ ++ (if unfocused=[] then str ""
+ else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut()
+ ++ pr_rec (List.length rest + 2) unfocused))
+ ++ print_dependent_evars (Some g1) sigma seeds
+ )
+
+let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof 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 Proof.{goals; stack; shelf; given_up; sigma} = Proof.data 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 ~unfocused:[] ~goals
+ | [] , [] , _ ->
+ Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:");
+ fnl ()
+ ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:given_up
+ ++ fnl () ++ str "You need to go back and solve them."
+ | [] , _ , _ ->
+ Feedback.msg_info (str "All the remaining goals are on the shelf.");
+ fnl ()
+ ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf
+ | _ , _, _ ->
+ let cmd = if quiet then None else
+ Some
+ (str "This subproof is complete, but there are some unfocused goals." ++
+ (let s = Proof_bullet.suggest p in
+ if Pp.ismt s then s else fnl () ++ s) ++
+ fnl ())
+ in
+ pr_subgoals ~pr_first:false cmd bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals
+ end
+ | _ ->
+ let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
+ let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in
+ let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
+ let os_map = match oproof with
+ | Some op when diffs ->
+ let Proof.{sigma=osigma} = Proof.data op in
+ let diff_goal_map = Proof_diffs.make_goal_map oproof proof in
+ Some (osigma, diff_goal_map)
+ | _ -> None
+ in
+ pr_subgoals ~pr_first:true ~diffs ?os_map None bsigma ~seeds ~shelf ~stack:[]
+ ~unfocused:unfocused_if_needed ~goals:bgoals_focused
+ end
+
+let pr_open_subgoals ~proof =
+ pr_open_subgoals_diff proof
+
+let pr_nth_open_subgoal ~proof n =
+ let Proof.{goals;sigma} = Proof.data proof in
+ pr_subgoal n sigma goals
+
+let pr_goal_by_id ~proof id =
+ try
+ Proof.in_proof proof (fun sigma ->
+ let g = Evd.evar_key id sigma in
+ pr_selected_subgoal (pr_id id) sigma g)
+ with Not_found -> user_err Pp.(str "No such goal.")
+
+(* Printer function for sets of Assumptions.assumptions.
+ It is used primarily by the Print Assumptions command. *)
+
+type axiom =
+ | Constant of Constant.t (* An axiom or a constant. *)
+ | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
+ | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+
+type context_object =
+ | Variable of Id.t (* A section variable or a Let definition *)
+ | Axiom of axiom * (Label.t * Constr.rel_context * types) list
+ | Opaque of Constant.t (* An opaque constant. *)
+ | Transparent of Constant.t
+
+(* Defines a set of [assumption] *)
+module OrderedContextObject =
+struct
+ type t = context_object
+
+ let compare_axiom x y =
+ match x,y with
+ | Constant k1 , Constant k2 ->
+ Constant.CanOrd.compare k1 k2
+ | Positive m1 , Positive m2 ->
+ MutInd.CanOrd.compare m1 m2
+ | Guarded k1 , Guarded k2 ->
+ Constant.CanOrd.compare k1 k2
+ | _ , Constant _ -> 1
+ | _ , Positive _ -> 1
+ | _ -> -1
+
+ let compare x y =
+ match x , y with
+ | Variable i1 , Variable i2 -> Id.compare i1 i2
+ | Variable _ , _ -> -1
+ | _ , Variable _ -> 1
+ | Axiom (k1,_) , Axiom (k2, _) -> compare_axiom k1 k2
+ | Axiom _ , _ -> -1
+ | _ , Axiom _ -> 1
+ | Opaque k1 , Opaque k2 -> Constant.CanOrd.compare k1 k2
+ | Opaque _ , _ -> -1
+ | _ , Opaque _ -> 1
+ | Transparent k1 , Transparent k2 -> Constant.CanOrd.compare k1 k2
+end
+
+module ContextObjectSet = Set.Make (OrderedContextObject)
+module ContextObjectMap = Map.Make (OrderedContextObject)
+
+let pr_assumptionset env sigma s =
+ if ContextObjectMap.is_empty s &&
+ engagement env = PredicativeSet then
+ str "Closed under the global context"
+ else
+ let safe_pr_constant env kn =
+ try pr_constant env kn
+ with Not_found ->
+ (* FIXME? *)
+ let mp,lab = Constant.repr2 kn in
+ str (ModPath.to_string mp) ++ str "." ++ Label.print lab
+ in
+ let safe_pr_inductive env kn =
+ try pr_inductive env (kn,0)
+ with Not_found ->
+ (* FIXME? *)
+ MutInd.print kn
+ in
+ let safe_pr_ltype env sigma typ =
+ try str " : " ++ pr_ltype_env env sigma typ
+ with e when CErrors.noncritical e -> mt ()
+ in
+ let safe_pr_ltype_relctx (rctx, typ) =
+ let env = Environ.push_rel_context rctx env in
+ try str " " ++ pr_ltype_env env sigma typ
+ with e when CErrors.noncritical e -> mt ()
+ in
+ let pr_axiom env ax typ =
+ match ax with
+ | Constant kn ->
+ safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
+ | Positive m ->
+ hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.")
+ | Guarded kn ->
+ hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
+ in
+ let fold t typ accu =
+ let (v, a, o, tr) = accu in
+ match t with
+ | Variable id ->
+ let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in
+ (var :: v, a, o, tr)
+ | Axiom (axiom, []) ->
+ let ax = pr_axiom env axiom typ in
+ (v, ax :: a, o, tr)
+ | Axiom (axiom,l) ->
+ let ax = pr_axiom env axiom typ ++
+ cut() ++
+ prlist_with_sep cut (fun (lbl, ctx, ty) ->
+ str " used in " ++ Label.print lbl ++
+ str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty))
+ l in
+ (v, ax :: a, o, tr)
+ | Opaque kn ->
+ let opq = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
+ (v, a, opq :: o, tr)
+ | Transparent kn ->
+ let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
+ (v, a, o, tran :: tr)
+ in
+ let (vars, axioms, opaque, trans) =
+ ContextObjectMap.fold fold s ([], [], [], [])
+ in
+ let theory =
+ if is_impredicative_set env then
+ [str "Set is impredicative"]
+ else []
+ in
+ let theory =
+ if type_in_type env then
+ str "Type hierarchy is collapsed (logic is inconsistent)" :: theory
+ else theory
+ 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;
+ opt_list (str "Theory:") theory;
+ ] in
+ prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
+
+(* print the proof step, possibly with diffs highlighted, *)
+let print_and_diff oldp newp =
+ match newp with
+ | None -> ()
+ | Some proof ->
+ let output =
+ if Proof_diffs.show_diffs () then
+ try pr_open_subgoals_diff ~diffs:true ?oproof:oldp proof
+ with Pp_diff.Diff_Failure msg -> begin
+ (* todo: print the unparsable string (if we know it) *)
+ Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut()
+ ++ str "Showing results without diff highlighting" );
+ pr_open_subgoals ~proof
+ end
+ else
+ pr_open_subgoals ~proof
+ in
+ Feedback.msg_notice output;;
diff --git a/printing/printer.mli b/printing/printer.mli
new file mode 100644
index 0000000000..9a06d555e4
--- /dev/null
+++ b/printing/printer.mli
@@ -0,0 +1,209 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Constr
+open Environ
+open Pattern
+open Evd
+open Glob_term
+open Ltac_pretype
+
+(** These are the entry points for printing terms, context, tac, ... *)
+
+
+val enable_unfocused_goal_printing: bool ref
+val enable_goal_tags_printing : bool ref
+val enable_goal_names_printing : bool ref
+
+(** Terms *)
+
+val pr_lconstr_env : env -> evar_map -> constr -> Pp.t
+val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t
+
+val pr_constr_env : env -> evar_map -> constr -> Pp.t
+val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
+
+val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
+
+(** 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 -> Pp.t
+
+val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t
+
+val pr_econstr_env : env -> evar_map -> EConstr.t -> Pp.t
+val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t
+
+val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
+
+val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t
+val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t
+
+val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t
+
+val pr_open_lconstr_env : env -> evar_map -> open_constr -> Pp.t
+
+val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t
+
+val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t
+
+val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t
+val pr_ltype_env : env -> evar_map -> types -> Pp.t
+
+val pr_type_env : env -> evar_map -> types -> Pp.t
+
+val pr_closed_glob_n_env : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
+val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t
+
+val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
+
+val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t
+
+val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t
+
+val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
+
+val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
+
+val pr_cases_pattern : cases_pattern -> Pp.t
+
+val pr_sort : evar_map -> Sorts.t -> Pp.t
+
+(** Universe constraints *)
+
+val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t
+val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t
+val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
+ Univ.UContext.t -> Pp.t
+val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
+ Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t
+val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t
+val pr_constant_universes : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t
+val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t
+val pr_abstract_cumulativity_info : evar_map -> Univ.ACumulativityInfo.t -> Pp.t
+
+(** Printing global references using names as short as possible *)
+
+val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t
+val pr_global : GlobRef.t -> Pp.t
+
+val pr_constant : env -> Constant.t -> Pp.t
+val pr_existential_key : evar_map -> Evar.t -> Pp.t
+val pr_existential : env -> evar_map -> existential -> Pp.t
+val pr_constructor : env -> constructor -> Pp.t
+val pr_inductive : env -> inductive -> Pp.t
+val pr_evaluable_reference : evaluable_global_reference -> Pp.t
+
+val pr_pconstant : env -> evar_map -> pconstant -> Pp.t
+val pr_pinductive : env -> evar_map -> pinductive -> Pp.t
+val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t
+
+
+(** Contexts *)
+
+(** Display compact contexts of goals (simple hyps on the same line) *)
+val set_compact_context : bool -> unit
+val get_compact_context : unit -> bool
+
+val pr_context_unlimited : env -> evar_map -> Pp.t
+val pr_ne_context_of : Pp.t -> env -> evar_map -> Pp.t
+
+val pr_named_decl : env -> evar_map -> Constr.named_declaration -> Pp.t
+val pr_compacted_decl : env -> evar_map -> Constr.compacted_declaration -> Pp.t
+val pr_rel_decl : env -> evar_map -> Constr.rel_declaration -> Pp.t
+
+val pr_named_context : env -> evar_map -> Constr.named_context -> Pp.t
+val pr_named_context_of : env -> evar_map -> Pp.t
+val pr_rel_context : env -> evar_map -> Constr.rel_context -> Pp.t
+val pr_rel_context_of : env -> evar_map -> Pp.t
+val pr_context_of : env -> evar_map -> Pp.t
+
+(** Predicates *)
+
+val pr_predicate : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t
+val pr_cpred : Cpred.t -> Pp.t
+val pr_idpred : Id.Pred.t -> Pp.t
+val pr_transparent_state : TransparentState.t -> Pp.t
+
+(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
+
+(** [pr_goal ~diffs ~og_s g_s] prints the goal specified by [g_s]. If [diffs] is true,
+ highlight the differences between the old goal, [og_s], and [g_s]. [g_s] and [og_s] are
+ records containing the goal and sigma for, respectively, the new and old proof steps,
+ e.g. [{ it = g ; sigma = sigma }].
+*)
+val pr_goal : ?diffs:bool -> ?og_s:(Goal.goal sigma) -> Goal.goal sigma -> Pp.t
+
+(** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals]
+ prints the goals in [goals] followed by the goals in [unfocused] in a compact form
+ (typically only the conclusion). If [pr_first] is true, print the first goal in full.
+ [close_cmd] is printed afterwards verbatim.
+
+ If [diffs] is true, then highlight diffs relative to [os_map] in the output for first goal.
+ [os_map] contains sigma for the old proof step and the goal map created by
+ [Proof_diffs.make_goal_map].
+
+ This function prints only the focused goals unless the corresponding option [enable_unfocused_goal_printing] is set.
+ [seeds] is for printing dependent evars (mainly for emacs proof tree mode). [shelf] is from
+ Proof.proof and is used to identify shelved goals in a message if there are no more subgoals but
+ there are non-instantiated existential variables. [stack] is used to print summary info on unfocused
+ goals.
+*)
+val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Goal.goal Evar.Map.t) -> Pp.t option -> evar_map
+ -> seeds:Goal.goal list -> shelf:Goal.goal list -> stack:int list
+ -> unfocused:Goal.goal list -> goals:Goal.goal list -> Pp.t
+
+val pr_subgoal : int -> evar_map -> Goal.goal list -> Pp.t
+
+(** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma]. The output
+ is labelled "subgoal [n]". If [diffs] is true, highlight the differences between the old conclusion,
+ [og_s], and [g]+[sigma]. [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }].
+*)
+val pr_concl : int -> ?diffs:bool -> ?og_s:(Goal.goal sigma) -> evar_map -> Goal.goal -> Pp.t
+
+(** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop.
+ The first active goal is printed with all its antecedents and the conclusion. The other active goals only show their
+ conclusions. If [diffs] is true, highlight the differences between the old proof, [oproof], and [proof]. [quiet]
+ disables printing messages as Feedback.
+*)
+val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Proof.t -> Pp.t
+val pr_open_subgoals : proof:Proof.t -> Pp.t
+val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t
+val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t
+val pr_evars_int : evar_map -> shelf:Goal.goal list -> given_up:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t
+val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t
+val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map ->
+ Evar.Set.t -> Pp.t
+
+val print_and_diff : Proof.t option -> Proof.t option -> unit
+
+(** Declarations for the "Print Assumption" command *)
+type axiom =
+ | Constant of Constant.t (* An axiom or a constant. *)
+ | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
+ | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+
+type context_object =
+ | Variable of Id.t (* A section variable or a Let definition *)
+ | Axiom of axiom * (Label.t * Constr.rel_context * types) list
+ | Opaque of Constant.t (* An opaque constant. *)
+ | Transparent of Constant.t
+
+module ContextObjectSet : Set.S with type elt = context_object
+module ContextObjectMap : CMap.ExtS
+ with type key = context_object and module Set := ContextObjectSet
+
+val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
+
+val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
+
diff --git a/printing/printing.mllib b/printing/printing.mllib
new file mode 100644
index 0000000000..deb52ad270
--- /dev/null
+++ b/printing/printing.mllib
@@ -0,0 +1,7 @@
+Genprint
+Pputils
+Ppconstr
+Proof_diffs
+Printer
+Printmod
+Prettyp
diff --git a/printing/printmod.ml b/printing/printmod.ml
new file mode 100644
index 0000000000..898f231a8b
--- /dev/null
+++ b/printing/printmod.ml
@@ -0,0 +1,460 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Util
+open Constr
+open Pp
+open Names
+open Environ
+open Declarations
+open Globnames
+open Libnames
+open Goptions
+
+(** Note: there is currently two modes for printing modules.
+ - The "short" one, that just prints the names of the fields.
+ - The "rich" one, that also tries to print the types of the fields.
+ The short version used to be the default behavior, but now we print
+ types by default. The following option allows changing this.
+*)
+
+module Tag =
+struct
+
+ let definition = "module.definition"
+ let keyword = "module.keyword"
+
+end
+
+let tag t s = Pp.tag t s
+let tag_definition s = tag Tag.definition s
+let tag_keyword s = tag Tag.keyword s
+
+type short = OnlyNames | WithContents
+
+let short = ref false
+
+let () =
+ declare_bool_option
+ { optdepr = false;
+ optname = "short module printing";
+ optkey = ["Short";"Module";"Printing"];
+ optread = (fun () -> !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))
+
+let def s = tag_definition (str s)
+let keyword s = 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.Set.add id l) (Namegen.next_ident_away id l)
+ in
+ let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in
+ get_id avoid id
+
+(** Inductive declarations *)
+
+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 sigma names types =
+ let pc =
+ prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
+ (fun (id,c) -> Id.print id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma 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 sigma mib ((_,i) as ind) =
+ let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+ let mip = mib.mind_packets.(i) in
+ let params = Inductive.inductive_paramdecls (mib,u) in
+ let nparamdecls = Context.Rel.length params in
+ let args = Context.Rel.to_extended_list mkRel 0 params in
+ let arity = hnf_prod_applist_assum env nparamdecls (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_assum env nparamdecls c args) cstrtypes in
+ let envpar = push_rel_context params env in
+ let inst =
+ if Declareops.inductive_is_polymorphic mib then
+ Printer.pr_universe_instance sigma u
+ else mt ()
+ in
+ hov 0 (
+ Id.print mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++
+ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
+ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
+
+let print_mutual_inductive env mind mib udecl =
+ let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
+ in
+ let keyword =
+ let open Declarations in
+ match mib.mind_finite with
+ | Finite -> "Inductive"
+ | BiFinite -> "Variant"
+ | CoFinite -> "CoInductive"
+ in
+ let bl = UnivNames.universe_binders_with_opt_names
+ (Declareops.inductive_polymorphic_context mib) udecl
+ in
+ let sigma = Evd.from_ctx (UState.of_binders bl) in
+ hov 0 (def keyword ++ spc () ++
+ prlist_with_sep (fun () -> fnl () ++ str" with ")
+ (print_one_inductive env sigma mib) inds ++
+ match mib.mind_universes with
+ | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
+ | Cumulative_ind cumi ->
+ Printer.pr_abstract_cumulativity_info sigma cumi)
+
+let get_fields =
+ let rec prodec_rec l subst c =
+ match kind 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 udecl =
+ let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+ let mip = mib.mind_packets.(0) in
+ let params = Inductive.inductive_paramdecls (mib,u) in
+ let nparamdecls = Context.Rel.length params in
+ let args = Context.Rel.to_extended_list mkRel 0 params in
+ let arity = hnf_prod_applist_assum env nparamdecls (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_assum env nparamdecls cstrtypes.(0) args in
+ let fields = get_fields cstrtype in
+ let envpar = push_rel_context params env in
+ let bl = UnivNames.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib)
+ udecl
+ in
+ let sigma = Evd.from_ctx (UState.of_binders bl) in
+ let keyword =
+ let open Declarations in
+ match mib.mind_finite with
+ | BiFinite -> "Record"
+ | Finite -> "Inductive"
+ | CoFinite -> "CoInductive"
+ in
+ hov 0 (
+ hov 0 (
+ def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++
+ print_params env sigma params ++
+ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
+ str ":= " ++ Id.print mip.mind_consnames.(0)) ++
+ brk(1,2) ++
+ hv 2 (str "{ " ++
+ prlist_with_sep (fun () -> str ";" ++ brk(2,0))
+ (fun (id,b,c) ->
+ Id.print id ++ str (if b then " : " else " := ") ++
+ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
+ match mib.mind_universes with
+ | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
+ | Cumulative_ind cumi ->
+ Printer.pr_abstract_cumulativity_info sigma cumi
+ )
+
+let pr_mutual_inductive_body env mind mib udecl =
+ if mib.mind_record != NotRecord && not !Flags.raw_print then
+ print_record env mind mib udecl
+ else
+ print_mutual_inductive env mind mib udecl
+
+(** Modpaths *)
+
+let rec print_local_modpath locals = function
+ | MPbound mbid -> Id.print (Util.List.assoc_f MBId.equal mbid locals)
+ | MPdot(mp,l) ->
+ print_local_modpath locals mp ++ str "." ++ Label.print 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 obj_mp =
+ let id = mk_fake_top () in
+ let obj_dir = DirPath.make [id] in
+ Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; obj_sec = 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 =
+ let id = MBId.to_id mbid in
+ match mtb.mod_type with
+ | MoreFunctor _ -> id (* 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
+ let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in
+ id
+ with e when CErrors.noncritical e ->
+ (* Otherwise, we try to play with the nametab ourselves *)
+ let mp = MPbound mbid in
+ let check id = Nametab.exists_dir (DirPath.make [id]) in
+ let id = Namegen.next_ident_away_from id check in
+ let dir = DirPath.make [id] in
+ nametab_register_dir mp;
+ List.iter (nametab_register_body mp dir) struc;
+ id
+
+let print_body is_impl extent env mp (l,body) =
+ let name = Label.print l in
+ hov 2 (match body with
+ | SFBmodule _ -> keyword "Module" ++ spc () ++ name
+ | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
+ | SFBconst cb ->
+ let ctx = Declareops.constant_polymorphic_context cb in
+ (match cb.const_body with
+ | Def _ -> def "Definition" ++ spc ()
+ | OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
+ | _ -> def "Parameter" ++ spc ()) ++ name ++
+ (match extent with
+ | OnlyNames -> mt ()
+ | WithContents ->
+ let bl = UnivNames.universe_binders_with_opt_names ctx None in
+ let sigma = Evd.from_ctx (UState.of_binders bl) in
+ str " :" ++ spc () ++
+ hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++
+ (match cb.const_body with
+ | Def l when is_impl ->
+ spc () ++
+ hov 2 (str ":= " ++
+ Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
+ | _ -> mt ()) ++ str "." ++
+ Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs)
+ | SFBmind mib ->
+ match extent with
+ | WithContents ->
+ pr_mutual_inductive_body env (MutInd.make2 mp l) mib None
+ | OnlyNames ->
+ let keyword =
+ let open Declarations in
+ match mib.mind_finite with
+ | Finite -> def "Inductive"
+ | BiFinite -> def "Variant"
+ | CoFinite -> def "CoInductive"
+ in
+ keyword ++ spc () ++ name)
+
+let print_struct is_impl extent env mp struc =
+ prlist_with_sep spc (print_body is_impl extent env mp) struc
+
+let print_structure is_type extent env mp locals struc =
+ let env' = 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 extent 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 extent 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 s = String.concat "." (List.map Id.to_string idl) in
+ let body = match extent with
+ | WithContents ->
+ let sigma = Evd.from_env env in
+ spc() ++ str ":=" ++ spc() ++ Printer.pr_lconstr_env env sigma c
+ | OnlyNames ->
+ mt() in
+ hov 2 (print_typ_expr extent env mp locals me ++ spc() ++ str "with" ++ spc()
+ ++ def "Definition"++ spc() ++ str s ++ body)
+ | MEwith(me,WithMod(idl,mp'))->
+ let s = String.concat "." (List.map Id.to_string idl) in
+ let body = match extent with
+ | WithContents ->
+ spc() ++ str ":="++ spc() ++ print_modpath locals mp'
+ | OnlyNames -> mt () in
+ hov 2 (print_typ_expr extent env mp locals me ++ spc() ++ str "with" ++ spc() ++
+ keyword "Module"++ spc() ++ str s ++ body)
+
+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 extent env mp locals = function
+ | NoFunctor me -> fatom is_type extent env mp locals me
+ | MoreFunctor (mbid,mtb1,me2) ->
+ let id = nametab_register_modparam mbid mtb1 in
+ let mp1 = MPbound mbid in
+ let pr_mtb1 = fty extent env mp1 locals mtb1 in
+ let env' = 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 "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++
+ spc() ++ print_functor fty fatom is_type extent env' mp locals' me2)
+
+let rec print_expression x =
+ print_functor
+ print_modtype
+ (function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x
+
+and print_signature x =
+ print_functor print_modtype print_structure x
+
+and print_modtype extent env mp locals mtb = match mtb.mod_type_alg with
+ | Some me -> print_expression true extent env mp locals me
+ | None -> print_signature true extent env mp locals mtb.mod_type
+
+let rec printable_body dir =
+ let dir = pop_dirpath dir in
+ DirPath.is_empty dir ||
+ try
+ let open Nametab.GlobDirRef in
+ 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 extent env mp me =
+ States.with_state_protection
+ (fun e -> print_expression is_type extent env mp [] e) me
+
+let print_signature' is_type extent env mp me =
+ States.with_state_protection
+ (fun e -> print_signature is_type extent env mp [] e) me
+
+let unsafe_print_module extent 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 extent env mp me
+ | _, Struct sign -> pr_equals ++ print_signature' false extent env mp sign
+ | _, FullStruct -> pr_equals ++ print_signature' false extent 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 extent env mp ty
+ | _, _ -> brk (1,1) ++ str": " ++ print_signature' true extent 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 WithContents
+ (Global.env ()) mp with_body me ++ fnl ()
+ with e when CErrors.noncritical e ->
+ unsafe_print_module OnlyNames
+ (Global.env ()) 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 WithContents
+ (Global.env ()) kn mtb.mod_type
+ with e when CErrors.noncritical e ->
+ print_signature' true OnlyNames
+ (Global.env ()) kn mtb.mod_type)
diff --git a/printing/printmod.mli b/printing/printmod.mli
new file mode 100644
index 0000000000..48ba866cc0
--- /dev/null
+++ b/printing/printmod.mli
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+
+(** false iff the module is an element of an open module type *)
+val printable_body : DirPath.t -> bool
+
+val pr_mutual_inductive_body : Environ.env ->
+ MutInd.t -> Declarations.mutual_inductive_body ->
+ UnivNames.univ_name_list option -> Pp.t
+val print_module : bool -> ModPath.t -> Pp.t
+val print_modtype : ModPath.t -> Pp.t
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
new file mode 100644
index 0000000000..c1ea067567
--- /dev/null
+++ b/printing/proof_diffs.ml
@@ -0,0 +1,649 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(*
+Displays the differences between successive proof steps in coqtop and CoqIDE.
+Proof General requires minor changes to make the diffs visible, but this code
+shouldn't break the existing version of PG. See pp_diff.ml for details on how
+the diff works.
+
+Diffs are computed for the hypotheses and conclusion of each goal in the new
+proof with its matching goal in the old proof.
+
+Diffs can be enabled in coqtop with 'Set Diffs "on"|"off"|"removed"' or
+'-diffs on|off|removed' on the OS command line. In CoqIDE, they can be enabled
+from the View menu. The "on" option shows only the new item with added text,
+while "removed" shows each modified item twice--once with the old value showing
+removed text and once with the new value showing added text.
+
+In CoqIDE, colors and highlights can be set in the Edit/Preferences/Tags panel.
+For coqtop, these can be set through the COQ_COLORS environment variable.
+
+Limitations/Possible enhancements:
+
+- coqtop colors were chosen for white text on a black background. They're
+not the greatest. I didn't want to change the existing green highlight.
+Suggestions welcome.
+
+- coqtop underlines removed text because (per Wikipedia) the ANSI escape code
+for strikeout is not commonly supported (it didn't work on my system). CoqIDE
+uses strikeout on removed text.
+*)
+
+open Pp_diff
+
+let diff_option = ref `OFF
+
+let read_diffs_option () = match !diff_option with
+| `OFF -> "off"
+| `ON -> "on"
+| `REMOVED -> "removed"
+
+let write_diffs_option = function
+| "off" -> diff_option := `OFF
+| "on" -> diff_option := `ON
+| "removed" -> diff_option := `REMOVED
+| _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
+
+let () =
+ Goptions.(declare_string_option {
+ optdepr = false;
+ optname = "show diffs in proofs";
+ optkey = ["Diffs"];
+ optread = read_diffs_option;
+ optwrite = write_diffs_option
+ })
+
+let show_diffs () = !diff_option <> `OFF;;
+let show_removed () = !diff_option = `REMOVED;;
+
+
+(* DEBUG/UNIT TEST *)
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
+let log_out_ch = ref stdout
+[@@@ocaml.warning "-32"]
+let cprintf s = cfprintf !log_out_ch s
+[@@@ocaml.warning "+32"]
+
+module StringMap = Map.Make(String);;
+
+let tokenize_string s =
+ (* todo: cLexer changes buff as it proceeds. Seems like that should be saved, too.
+ But I don't understand how it's used--it looks like things get appended to it but
+ it never gets cleared. *)
+ let rec stream_tok acc str =
+ let e = Stream.next str in
+ if Tok.(equal e EOI) then
+ List.rev acc
+ else
+ stream_tok ((Tok.extract_string true e) :: acc) str
+ in
+ let st = CLexer.get_lexer_state () in
+ try
+ let istr = Stream.of_string s in
+ let lexer = CLexer.make_lexer ~diff_mode:true in
+ let lex = lexer.Gramlib.Plexing.tok_func istr in
+ let toks = stream_tok [] (fst lex) in
+ CLexer.set_lexer_state st;
+ toks
+ with exn ->
+ CLexer.set_lexer_state st;
+ raise (Diff_Failure "Input string is not lexable");;
+
+
+type hyp_info = {
+ idents: string list;
+ rhs_pp: Pp.t;
+ mutable done_: bool;
+}
+
+(* Generate the diffs between the old and new hyps.
+ This works by matching lines with the hypothesis name and diffing the right-hand side.
+ Lines that have multiple names such as "n, m : nat" are handled specially to account
+ for, say, the addition of m to a pre-existing "n : nat".
+ *)
+let diff_hyps o_line_idents o_map n_line_idents n_map =
+ let rv : Pp.t list ref = ref [] in
+
+ let is_done ident map = (StringMap.find ident map).done_ in
+ let exists ident map =
+ try let _ = StringMap.find ident map in true
+ with Not_found -> false in
+ let contains l ident = try [List.find (fun x -> x = ident) l] with Not_found -> [] in
+
+ let output old_ids_uo new_ids =
+ (* use the order from the old line in case it's changed in the new *)
+ let old_ids = if old_ids_uo = [] then [] else
+ let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in
+ List.concat (List.map (contains orig) old_ids_uo)
+ in
+
+ let setup ids map = if ids = [] then ("", Pp.mt ()) else
+ let open Pp in
+ let rhs_pp = (StringMap.find (List.hd ids) map).rhs_pp in
+ let pp_ids = List.map (fun x -> str x) ids in
+ let hyp_pp = List.fold_left (fun l1 l2 -> l1 ++ str ", " ++ l2) (List.hd pp_ids) (List.tl pp_ids) ++ rhs_pp in
+ (string_of_ppcmds hyp_pp, hyp_pp)
+ in
+
+ let (o_line, o_pp) = setup old_ids o_map in
+ let (n_line, n_pp) = setup new_ids n_map in
+
+ let hyp_diffs = diff_str ~tokenize_string o_line n_line in
+ let (has_added, has_removed) = has_changes hyp_diffs in
+ if show_removed () && has_removed then begin
+ List.iter (fun x -> (StringMap.find x o_map).done_ <- true) old_ids;
+ rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv;
+ end;
+ if n_line <> "" then begin
+ List.iter (fun x -> (StringMap.find x n_map).done_ <- true) new_ids;
+ rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv
+ end
+ in
+
+ (* process identifier level diff *)
+ let process_ident_diff diff =
+ let (dtype, ident) = get_dinfo diff in
+ match dtype with
+ | `Removed ->
+ if dtype = `Removed then begin
+ let o_idents = (StringMap.find ident o_map).idents in
+ (* only show lines that have all idents removed here; other removed idents appear later *)
+ if show_removed () && not (is_done ident o_map) &&
+ List.for_all (fun x -> not (exists x n_map)) o_idents then
+ output (List.rev o_idents) []
+ end
+ | _ -> begin (* Added or Common case *)
+ let n_idents = (StringMap.find ident n_map).idents in
+
+ (* Process a new hyp line, possibly splitting it. Duplicates some of
+ process_ident iteration, but easier to understand this way *)
+ let process_line ident2 =
+ if not (is_done ident2 n_map) then begin
+ let n_ids_list : string list ref = ref [] in
+ let o_ids_list : string list ref = ref [] in
+ let fst_omap_idents = ref None in
+ let add ids id map =
+ ids := id :: !ids;
+ (StringMap.find id map).done_ <- true in
+
+ (* get identifiers shared by one old and one new line, plus
+ other Added in new and other Removed in old *)
+ let process_split ident3 =
+ if not (is_done ident3 n_map) then begin
+ let this_omap_idents = try Some (StringMap.find ident3 o_map).idents
+ with Not_found -> None in
+ if !fst_omap_idents = None then
+ fst_omap_idents := this_omap_idents;
+ match (!fst_omap_idents, this_omap_idents) with
+ | (Some fst, Some this) when fst == this -> (* yes, == *)
+ add n_ids_list ident3 n_map;
+ (* include, in old order, all undone Removed idents in old *)
+ List.iter (fun x -> if x = ident3 || not (is_done x o_map) && not (exists x n_map) then
+ (add o_ids_list x o_map)) fst
+ | (_, None) ->
+ add n_ids_list ident3 n_map (* include all undone Added idents in new *)
+ | _ -> ()
+ end in
+ List.iter process_split n_idents;
+ output (List.rev !o_ids_list) (List.rev !n_ids_list)
+ end in
+ List.iter process_line n_idents (* O(n^2), so sue me *)
+ end in
+
+ let cvt s = Array.of_list (List.concat s) in
+ let ident_diffs = diff_strs (cvt o_line_idents) (cvt n_line_idents) in
+ List.iter process_ident_diff ident_diffs;
+ List.rev !rv;;
+
+
+type 'a hyp = (Names.Id.t list * 'a option * 'a)
+type 'a reified_goal = { name: string; ty: 'a; hyps: 'a hyp list; env : Environ.env; sigma: Evd.evar_map }
+
+(* XXX: Port to proofview, one day. *)
+(* open Proofview *)
+module CDC = Context.Compacted.Declaration
+
+let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * 'pc) =
+ let open CDC in function
+ | LocalAssum(idl, tm) -> (idl, None, EConstr.of_constr tm)
+ | LocalDef(idl,tdef,tm) -> (idl, Some (EConstr.of_constr tdef), EConstr.of_constr tm);;
+
+(* XXX: Very unfortunately we cannot use the Proofview interface as
+ Proof is still using the "legacy" one. *)
+let process_goal_concl sigma g : EConstr.t * Environ.env =
+ let env = Goal.V82.env sigma g in
+ let ty = Goal.V82.concl sigma g in
+ (ty, env)
+
+let process_goal sigma g : EConstr.t reified_goal =
+ let env = Goal.V82.env sigma g in
+ let ty = Goal.V82.concl sigma g in
+ let name = Goal.uid g in
+ (* compaction is usually desired [eg for better display] *)
+ let hyps = Termops.compact_named_context (Environ.named_context env) in
+ let hyps = List.map to_tuple hyps in
+ { name; ty; hyps; env; sigma };;
+
+let pr_letype_core goal_concl_style env sigma t =
+ Ppconstr.pr_lconstr_expr (Constrextern.extern_type goal_concl_style env sigma t)
+
+let pp_of_type env sigma ty =
+ pr_letype_core true env sigma ty
+
+let pr_leconstr_core goal_concl_style env sigma t =
+ Ppconstr.pr_lconstr_expr (Constrextern.extern_constr goal_concl_style env sigma t)
+
+let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
+
+let pr_lconstr_env_econstr env sigma c = pr_leconstr_core false env sigma c
+
+let diff_concl ?og_s nsigma ng =
+ let open Evd in
+ let o_concl_pp = match og_s with
+ | Some { it=og; sigma=osigma } ->
+ let (oty, oenv) = process_goal_concl osigma og in
+ pp_of_type oenv osigma oty
+ | None -> Pp.mt()
+ in
+ let (nty, nenv) = process_goal_concl nsigma ng in
+ let n_concl_pp = pp_of_type nenv nsigma nty in
+
+ let show_removed = Some (show_removed ()) in
+
+ diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp
+
+(* fetch info from a goal, returning (idents, map, concl_pp) where
+idents is a list with one entry for each hypothesis, in which each entry
+is the list of idents on the lhs of the hypothesis. map is a map from
+ident to hyp_info reoords. For example: for the hypotheses:
+ b : bool
+ n, m : nat
+
+idents will be [ ["b"]; ["n"; "m"] ]
+
+map will contain:
+ "b" -> { ["b"], Pp.t for ": bool"; false }
+ "n" -> { ["n"; "m"], Pp.t for ": nat"; false }
+ "m" -> { ["n"; "m"], Pp.t for ": nat"; false }
+ where the last two entries share the idents list.
+
+concl_pp is the conclusion as a Pp.t
+*)
+let goal_info goal sigma =
+ let map = ref StringMap.empty in
+ let line_idents = ref [] in
+ let build_hyp_info env sigma hyp =
+ let (names, body, ty) = hyp in
+ let open Pp in
+ let idents = List.map (fun x -> Names.Id.to_string x) names in
+
+ line_idents := idents :: !line_idents;
+ let mid = match body with
+ | Some c ->
+ let pb = pr_lconstr_env_econstr env sigma c in
+ let pb = if EConstr.isCast sigma c then surround pb else pb in
+ str " := " ++ pb
+ | None -> mt() in
+ let ts = pp_of_type env sigma ty in
+ let rhs_pp = mid ++ str " : " ++ ts in
+
+ let make_entry () = { idents; rhs_pp; done_ = false } in
+ List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents
+ in
+
+ try
+ let { ty=ty; hyps=hyps; env=env } = process_goal sigma goal in
+ List.iter (build_hyp_info env sigma) (List.rev hyps);
+ let concl_pp = pp_of_type env sigma ty in
+ ( List.rev !line_idents, !map, concl_pp )
+ with _ -> ([], !map, Pp.mt ());;
+
+let diff_goal_info o_info n_info =
+ let (o_line_idents, o_hyp_map, o_concl_pp) = o_info in
+ let (n_line_idents, n_hyp_map, n_concl_pp) = n_info in
+ let show_removed = Some (show_removed ()) in
+ let concl_pp = diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp in
+
+ let hyp_diffs_list = diff_hyps o_line_idents o_hyp_map n_line_idents n_hyp_map in
+ (hyp_diffs_list, concl_pp)
+
+let hyp_list_to_pp hyps =
+ let open Pp in
+ match hyps with
+ | h :: tl -> List.fold_left (fun x y -> x ++ cut () ++ y) h tl
+ | [] -> mt ();;
+
+let unwrap g_s =
+ match g_s with
+ | Some g_s ->
+ let goal = Evd.sig_it g_s in
+ let sigma = Refiner.project g_s in
+ goal_info goal sigma
+ | None -> ([], StringMap.empty, Pp.mt ())
+
+let diff_goal_ide og_s ng nsigma =
+ diff_goal_info (unwrap og_s) (goal_info ng nsigma)
+
+let diff_goal ?og_s ng ns =
+ let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap og_s) (goal_info ng ns) in
+ let open Pp in
+ v 0 (
+ (hyp_list_to_pp hyps_pp_list) ++ cut () ++
+ str "============================" ++ cut () ++
+ concl_pp);;
+
+
+(*** Code to determine which calls to compare between the old and new proofs ***)
+
+open Constrexpr
+open Glob_term
+open Names
+open CAst
+
+(* Compare the old and new proof trees to identify the correspondence between
+new and old goals. Returns a map from the new evar name to the old,
+e.g. "Goal2" -> "Goal1". Assumes that proof steps only rewrite CEvar nodes
+and that CEvar nodes cannot contain other CEvar nodes.
+
+The comparison works this way:
+1. Traverse the old and new trees together (ogname = "", ot != nt):
+- if the old and new trees both have CEvar nodes, add an entry to the map from
+ the new evar name to the old evar name. (Position of goals is preserved but
+ evar names may not be--see below.)
+- if the old tree has a CEvar node and the new tree has a different type of node,
+ we've found a changed goal. Set ogname to the evar name of the old goal and
+ go to step 2.
+- any other mismatch violates the assumptions, raise an exception
+2. Traverse the new tree from the point of the difference (ogname <> "", ot = nt).
+- if the node is a CEvar, generate a map entry from the new evar name to ogname.
+
+Goal ids for unchanged goals appear to be preserved across proof steps.
+However, the evar name associated with a goal id may change in a proof step
+even if that goal is not changed by the tactic. You can see this by enabling
+the call to db_goal_map and entering the following:
+
+ Parameter P : nat -> Prop.
+ Goal (P 1 /\ P 2 /\ P 3) /\ P 4.
+ split.
+ Show Proof.
+ split.
+ Show Proof.
+
+ Which gives you this summarized output:
+
+ > split.
+ New Goals: 3 -> Goal 4 -> Goal0 <--- goal 4 is "Goal0"
+ Old Goals: 1 -> Goal
+ Goal map: 3 -> 1 4 -> 1
+ > Show Proof.
+ (conj ?Goal ?Goal0) <--- goal 4 is the rightmost goal in the proof
+ > split.
+ New Goals: 6 -> Goal0 7 -> Goal1 4 -> Goal <--- goal 4 is now "Goal"
+ Old Goals: 3 -> Goal 4 -> Goal0
+ Goal map: 6 -> 3 7 -> 3
+ > Show Proof.
+ (conj (conj ?Goal0 ?Goal1) ?Goal) <--- goal 4 is still the rightmost goal in the proof
+ *)
+let match_goals ot nt =
+ let nevar_to_oevar = ref StringMap.empty in
+ (* ogname is "" when there is no difference on the current path.
+ It's set to the old goal's evar name once a rewitten goal is found,
+ at which point the code only searches for the replacing goals
+ (and ot is set to nt). *)
+ let iter2 f l1 l2 =
+ if List.length l1 = (List.length l2) then
+ List.iter2 f l1 l2
+ in
+ let rec match_goals_r ogname ot nt =
+ let constr_expr ogname exp exp2 =
+ match_goals_r ogname exp.v exp2.v
+ in
+ let constr_expr_opt ogname exp exp2 =
+ match exp, exp2 with
+ | Some expa, Some expb -> constr_expr ogname expa expb
+ | None, None -> ()
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (1)")
+ in
+ let local_binder_expr ogname exp exp2 =
+ match exp, exp2 with
+ | CLocalAssum (nal,bk,ty), CLocalAssum(nal2,bk2,ty2) ->
+ constr_expr ogname ty ty2
+ | CLocalDef (n,c,t), CLocalDef (n2,c2,t2) ->
+ constr_expr ogname c c2;
+ constr_expr_opt ogname t t2
+ | CLocalPattern p, CLocalPattern p2 ->
+ let (p,ty), (p2,ty2) = p.v,p2.v in
+ constr_expr_opt ogname ty ty2
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
+ in
+ let recursion_order_expr ogname exp exp2 =
+ match exp, exp2 with
+ | CStructRec, CStructRec -> ()
+ | CWfRec c, CWfRec c2 ->
+ constr_expr ogname c c2
+ | CMeasureRec (m,r), CMeasureRec (m2,r2) ->
+ constr_expr ogname m m2;
+ constr_expr_opt ogname r r2
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)")
+ in
+ let fix_expr ogname exp exp2 =
+ let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in
+ recursion_order_expr ogname ro ro2;
+ iter2 (local_binder_expr ogname) lb lb2;
+ constr_expr ogname ce1 ce12;
+ constr_expr ogname ce2 ce22
+ in
+ let cofix_expr ogname exp exp2 =
+ let (l,lb,ce1,ce2), (l2,lb2,ce12,ce22) = exp,exp2 in
+ iter2 (local_binder_expr ogname) lb lb2;
+ constr_expr ogname ce1 ce12;
+ constr_expr ogname ce2 ce22
+ in
+ let case_expr ogname exp exp2 =
+ let (ce,l,cp), (ce2,l2,cp2) = exp,exp2 in
+ constr_expr ogname ce ce2
+ in
+ let branch_expr ogname exp exp2 =
+ let (cpe,ce), (cpe2,ce2) = exp.v,exp2.v in
+ constr_expr ogname ce ce2
+ in
+ let constr_notation_substitution ogname exp exp2 =
+ let (ce, cel, cp, lb), (ce2, cel2, cp2, lb2) = exp, exp2 in
+ iter2 (constr_expr ogname) ce ce2;
+ iter2 (fun a a2 -> iter2 (constr_expr ogname) a a2) cel cel2;
+ iter2 (fun a a2 -> iter2 (local_binder_expr ogname) a a2) lb lb2
+ in
+ begin
+ match ot, nt with
+ | CRef (ref,us), CRef (ref2,us2) -> ()
+ | CFix (id,fl), CFix (id2,fl2) ->
+ iter2 (fix_expr ogname) fl fl2
+ | CCoFix (id,cfl), CCoFix (id2,cfl2) ->
+ iter2 (cofix_expr ogname) cfl cfl2
+ | CProdN (bl,c2), CProdN (bl2,c22)
+ | CLambdaN (bl,c2), CLambdaN (bl2,c22) ->
+ iter2 (local_binder_expr ogname) bl bl2;
+ constr_expr ogname c2 c22
+ | CLetIn (na,c1,t,c2), CLetIn (na2,c12,t2,c22) ->
+ constr_expr ogname c1 c12;
+ constr_expr_opt ogname t t2;
+ constr_expr ogname c2 c22
+ | CAppExpl ((isproj,ref,us),args), CAppExpl ((isproj2,ref2,us2),args2) ->
+ iter2 (constr_expr ogname) args args2
+ | CApp ((isproj,f),args), CApp ((isproj2,f2),args2) ->
+ constr_expr ogname f f2;
+ iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in
+ constr_expr ogname c c2) args args2
+ | CRecord fs, CRecord fs2 ->
+ iter2 (fun a a2 -> let (_, c) = a and (_, c2) = a2 in
+ constr_expr ogname c c2) fs fs2
+ | CCases (sty,rtnpo,tms,eqns), CCases (sty2,rtnpo2,tms2,eqns2) ->
+ constr_expr_opt ogname rtnpo rtnpo2;
+ iter2 (case_expr ogname) tms tms2;
+ iter2 (branch_expr ogname) eqns eqns2
+ | CLetTuple (nal,(na,po),b,c), CLetTuple (nal2,(na2,po2),b2,c2) ->
+ constr_expr_opt ogname po po2;
+ constr_expr ogname b b2;
+ constr_expr ogname c c2
+ | CIf (c,(na,po),b1,b2), CIf (c2,(na2,po2),b12,b22) ->
+ constr_expr ogname c c2;
+ constr_expr_opt ogname po po2;
+ constr_expr ogname b1 b12;
+ constr_expr ogname b2 b22
+ | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> ()
+ | CPatVar _, CPatVar _ -> ()
+ | CEvar (n,l), CEvar (n2,l2) ->
+ let oevar = if ogname = "" then Id.to_string n else ogname in
+ nevar_to_oevar := StringMap.add (Id.to_string n2) oevar !nevar_to_oevar;
+ iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2
+ | CEvar (n,l), nt' ->
+ (* pass down the old goal evar name *)
+ match_goals_r (Id.to_string n) nt' nt'
+ | CSort s, CSort s2 -> ()
+ | CCast (c,c'), CCast (c2,c'2) ->
+ constr_expr ogname c c2;
+ (match c', c'2 with
+ | CastConv a, CastConv a2
+ | CastVM a, CastVM a2
+ | CastNative a, CastNative a2 ->
+ constr_expr ogname a a2
+ | CastCoerce, CastCoerce -> ()
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)"))
+ | CNotation (ntn,args), CNotation (ntn2,args2) ->
+ constr_notation_substitution ogname args args2
+ | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) ->
+ constr_expr ogname c c2
+ | CPrim p, CPrim p2 -> ()
+ | CDelimiters (key,e), CDelimiters (key2,e2) ->
+ constr_expr ogname e e2
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (5)")
+ end
+ in
+
+ (match ot with
+ | Some ot -> match_goals_r "" ot nt
+ | None -> ());
+ !nevar_to_oevar
+
+
+let to_constr p =
+ let open CAst in
+ let pprf = Proof.partial_proof p in
+ (* pprf generally has only one element, but it may have more in the derive plugin *)
+ let t = List.hd pprf in
+ let sigma, env = Pfedit.get_current_context ~p () in
+ let x = Constrextern.extern_constr false env sigma t in (* todo: right options?? *)
+ x.v
+
+
+module GoalMap = Evar.Map
+
+let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma)
+
+open Goal.Set
+
+[@@@ocaml.warning "-32"]
+let db_goal_map op np ng_to_og =
+ let pr_goals title prf =
+ Printf.printf "%s: " title;
+ let Proof.{goals;sigma} = Proof.data prf in
+ List.iter (fun g -> Printf.printf "%d -> %s " (Evar.repr g) (goal_to_evar g sigma)) goals;
+ let gs = diff (Proof.all_goals prf) (List.fold_left (fun s g -> add g s) empty goals) in
+ List.iter (fun g -> Printf.printf "%d " (Evar.repr g)) (elements gs);
+ in
+
+ pr_goals "New Goals" np;
+ (match op with
+ | Some op ->
+ pr_goals "\nOld Goals" op
+ | None -> ());
+ Printf.printf "\nGoal map: ";
+ GoalMap.iter (fun ng og -> Printf.printf "%d -> %d " (Evar.repr ng) (Evar.repr og)) ng_to_og;
+ let unmapped = ref (Proof.all_goals np) in
+ GoalMap.iter (fun ng _ -> unmapped := Goal.Set.remove ng !unmapped) ng_to_og;
+ if Goal.Set.cardinal !unmapped > 0 then begin
+ Printf.printf "\nUnmapped goals: ";
+ Goal.Set.iter (fun ng -> Printf.printf "%d " (Evar.repr ng)) !unmapped
+ end;
+ Printf.printf "\n"
+[@@@ocaml.warning "+32"]
+
+(* Create a map from new goals to old goals for proof diff. New goals
+ that are evars not appearing in the proof will not have a mapping.
+
+ It proceeds as follows:
+ 1. Find the goal ids that were removed from the old proof and that were
+ added in the new proof. If the same goal id is present in both proofs
+ then conclude the goal is unchanged (assumption).
+
+ 2. The code assumes that proof changes only take the form of replacing
+ one or more goal symbols (CEvars) with new terms. Therefore:
+ - if there are no removals, the proofs are the same.
+ - if there are removals but no additions, then there are no new goals
+ that aren't the same as their associated old goals. For the both of
+ these cases, the map is empty because there are no new goals that differ
+ from their old goals
+ - if there is only one removal, then any added goals should be mapped to
+ the removed goal.
+ - if there are more than 2 removals and more than one addition, call
+ match_goals to get a map between old and new evar names, then use this
+ to create the map from new goal ids to old goal ids.
+*)
+let make_goal_map_i op np =
+ let ng_to_og = ref GoalMap.empty in
+ match op with
+ | None -> !ng_to_og
+ | Some op ->
+ let open Goal.Set in
+ let ogs = Proof.all_goals op in
+ let ngs = Proof.all_goals np in
+ let rem_gs = diff ogs ngs in
+ let num_rems = cardinal rem_gs in
+ let add_gs = diff ngs ogs in
+ let num_adds = cardinal add_gs in
+
+ (* add common goals *)
+ Goal.Set.iter (fun x -> ng_to_og := GoalMap.add x x !ng_to_og) (inter ogs ngs);
+
+ if num_rems = 0 then
+ !ng_to_og (* proofs are the same *)
+ else if num_adds = 0 then
+ !ng_to_og (* only removals *)
+ else if num_rems = 1 then begin
+ (* only 1 removal, some additions *)
+ let removed_g = List.hd (elements rem_gs) in
+ Goal.Set.iter (fun x -> ng_to_og := GoalMap.add x removed_g !ng_to_og) add_gs;
+ !ng_to_og
+ end else begin
+ (* >= 2 removals, >= 1 addition, need to match *)
+ let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in
+
+ let oevar_to_og = ref StringMap.empty in
+ let Proof.{sigma=osigma} = Proof.data op in
+ List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og)
+ (Goal.Set.elements rem_gs);
+
+ let Proof.{sigma=nsigma} = Proof.data np in
+ let get_og ng =
+ let nevar = goal_to_evar ng nsigma in
+ let oevar = StringMap.find nevar nevar_to_oevar in
+ let og = StringMap.find oevar !oevar_to_og in
+ og
+ in
+ Goal.Set.iter (fun ng ->
+ try ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og with Not_found -> ()) add_gs;
+ !ng_to_og
+ end
+
+let make_goal_map op np =
+ let ng_to_og = make_goal_map_i op np in
+ (*db_goal_map op np ng_to_og;*)
+ ng_to_og
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
new file mode 100644
index 0000000000..1ebde3d572
--- /dev/null
+++ b/printing/proof_diffs.mli
@@ -0,0 +1,84 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* diff options *)
+
+(** Controls whether to show diffs. Takes values "on", "off", "removed" *)
+val write_diffs_option : string -> unit
+
+(** Returns true if the diffs option is "on" or "removed" *)
+val show_diffs : unit -> bool
+
+open Evd
+open Environ
+open Constr
+
+(** Computes the diff between the goals of two Proofs and returns
+the highlighted lists of hypotheses and conclusions.
+
+If the strings used to display the goal are not lexable (this is believed
+unlikely), this routine will generate a Diff_Failure. This routine may also
+raise Diff_Failure under some "impossible" conditions.
+
+If you want to make your call especially bulletproof, catch these
+exceptions, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val diff_goal_ide : Goal.goal sigma option -> Goal.goal -> Evd.evar_map -> Pp.t list * Pp.t
+
+(** Computes the diff between two goals
+
+If the strings used to display the goal are not lexable (this is believed
+unlikely), this routine will generate a Diff_Failure. This routine may also
+raise Diff_Failure under some "impossible" conditions.
+
+If you want to make your call especially bulletproof, catch these
+exceptions, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t
+
+(** Convert a string to a list of token strings using the lexer *)
+val tokenize_string : string -> string list
+
+val pr_letype_core : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
+val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
+val pr_lconstr_env : env -> evar_map -> constr -> Pp.t
+
+(** Computes diffs for a single conclusion *)
+val diff_concl : ?og_s:Goal.goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t
+
+(** Generates a map from [np] to [op] that maps changed goals to their prior
+forms. The map doesn't include entries for unchanged goals; unchanged goals
+will have the same goal id in both versions.
+
+[op] and [np] must be from the same proof document and [op] must be for a state
+before [np]. *)
+val make_goal_map : Proof.t option -> Proof.t -> Goal.goal Evar.Map.t
+
+(* Exposed for unit test, don't use these otherwise *)
+(* output channel for the test log file *)
+val log_out_ch : out_channel ref
+
+
+type hyp_info = {
+ idents: string list;
+ rhs_pp: Pp.t;
+ mutable done_: bool;
+}
+
+module StringMap :
+sig
+ type +'a t
+ val empty: hyp_info t
+ val add : string -> hyp_info -> hyp_info t -> hyp_info t
+end
+
+val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 10:17:43 +0000