diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/genprint.ml | 8 | ||||
| -rw-r--r-- | printing/genprint.mli | 8 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 51 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 13 | ||||
| -rw-r--r-- | printing/pputils.ml | 5 | ||||
| -rw-r--r-- | printing/pputils.mli | 3 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 1252 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 26 | ||||
| -rw-r--r-- | printing/prettyp.ml | 61 | ||||
| -rw-r--r-- | printing/prettyp.mli | 34 | ||||
| -rw-r--r-- | printing/printer.ml | 217 | ||||
| -rw-r--r-- | printing/printer.mli | 97 | ||||
| -rw-r--r-- | printing/printing.mllib | 2 | ||||
| -rw-r--r-- | printing/printmod.ml | 19 | ||||
| -rw-r--r-- | printing/printmod.mli | 2 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 635 | ||||
| -rw-r--r-- | printing/proof_diffs.mli | 84 |
17 files changed, 999 insertions, 1518 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml index 1bb7838a..fa53a879 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -19,15 +19,15 @@ open Geninterp (* Printing generic values *) type 'a with_level = - { default_already_surrounded : Notation_term.tolerability; - default_ensure_surrounded : Notation_term.tolerability; + { 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_term.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/genprint.mli b/printing/genprint.mli index fd5dd725..1a31025a 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -13,15 +13,15 @@ open Genarg type 'a with_level = - { default_already_surrounded : Notation_term.tolerability; - default_ensure_surrounded : Notation_term.tolerability; + { 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_term.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 4c5d955c..90d2b7ab 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -18,11 +18,12 @@ open Nameops open Libnames open Pputils open Ppextend -open Notation_term +open Glob_term open Constrexpr open Constrexpr_ops +open Notation_gram open Decl_kinds -open Misctypes +open Namegen (*i*) module Tag = @@ -87,8 +88,6 @@ let tag_var = tag Tag.variable | Numeral (_,b) -> if b then lposint else lnegint | String _ -> latom - open Notation - 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 @@ -160,7 +159,7 @@ let tag_var = tag Tag.variable let pr_univ_expr = function | Some (x,n) -> - pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) | None -> str"_" let pr_univ l = @@ -170,18 +169,18 @@ let tag_var = tag Tag.variable let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" - let pr_glob_sort = function + 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 = function + 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_reference u) + | GType (UNamed u) -> tag_type (pr_qualid u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -199,23 +198,23 @@ let tag_var = tag Tag.variable let pr_qualid = pr_qualid let pr_patvar = pr_id - let pr_glob_sort_instance = function + 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_reference u + | 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 = CAst.with_val (function - | Qualid qid -> pr_qualid qid - | Ident id -> tag_var (pr_id id)) + 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 @@ -229,7 +228,7 @@ let tag_var = tag Tag.variable str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type_spc pr = function - | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt () + | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t let pr_lident {loc; v=id} = @@ -243,8 +242,8 @@ let tag_var = tag Tag.variable | x -> pr_ast Name.print x let pr_or_var pr = function - | ArgArg x -> pr x - | ArgVar id -> pr_lident id + | Locus.ArgArg x -> pr x + | Locus.ArgVar id -> pr_lident id let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) @@ -296,7 +295,7 @@ let tag_var = tag Tag.variable | CPatOr pl -> hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator - | CPatNotation ("( _ )",([p],[]),[]) -> + | CPatNotation ((_,"( _ )"),([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom | CPatNotation (s,(l,ll),args) -> @@ -364,7 +363,7 @@ let tag_var = tag Tag.variable end | Default b -> match t with - | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> + | { CAst.v = CHole (_,IntroAnonymous,_) } -> let s = prlist_with_sep spc pr_lname nal in hov 1 (surround_implicit b s) | _ -> @@ -458,7 +457,7 @@ let tag_var = tag Tag.variable let pr_case_type pr po = match po with - | None | Some { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt() + | None | Some { CAst.v = CHole (_,IntroAnonymous,_) } -> mt() | Some p -> spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p) @@ -565,9 +564,9 @@ let tag_var = tag Tag.variable return (p ++ prlist (pr spc (lapp,L)) l2, lapp) else return (p, lproj) - | CAppExpl ((None,{v=Ident var},us),[t]) - | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None]) - when Id.equal var Notation_ops.ldots_var -> + | 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 @@ -593,7 +592,7 @@ let tag_var = tag Tag.variable hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> + | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ @@ -644,9 +643,9 @@ let tag_var = tag Tag.variable lif ) - | CHole (_,Misctypes.IntroIdentifier id,_) -> + | CHole (_,IntroIdentifier id,_) -> return (str "?[" ++ pr_id id ++ str "]", latom) - | CHole (_,Misctypes.IntroFresh id,_) -> + | CHole (_,IntroFresh id,_) -> return (str "?[?" ++ pr_id id ++ str "]", latom) | CHole (_,_,_) -> return (str "_", latom) @@ -666,7 +665,7 @@ let tag_var = tag Tag.variable | CastCoerce -> str ":>"), lcast ) - | CNotation ("( _ )",([t],[],[],[])) -> + | 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 diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 1f1308b0..bca419c9 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -15,14 +15,13 @@ open Libnames open Constrexpr open Names -open Misctypes -open Notation_term +open Notation_gram val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t -val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t +val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t val pr_lident : lident -> Pp.t val pr_lname : lname -> Pp.t @@ -39,16 +38,16 @@ val pr_name : Name.t -> Pp.t [@@ocaml.deprecated "alias of Names.Name.print"] val pr_qualid : qualid -> Pp.t -val pr_patvar : patvar -> Pp.t +val pr_patvar : Pattern.patvar -> Pp.t -val pr_glob_level : glob_level -> Pp.t -val pr_glob_sort : glob_sort -> 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 : (reference * constr_expr) list -> 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 diff --git a/printing/pputils.ml b/printing/pputils.ml index c14aa318..59e5f68f 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -11,7 +11,6 @@ open Util open Pp open Genarg -open Misctypes open Locus open Genredexpr @@ -69,7 +68,7 @@ let pr_short_red_flag pr r = let pr_red_flag pr r = try pr_short_red_flag pr r - with complexRedFlags -> + with ComplexRedFlag -> (if r.rBeta then pr_arg str "beta" else mt ()) ++ (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else (if r.rMatch then pr_arg str "match" else mt ()) ++ @@ -122,7 +121,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) -let pr_or_by_notation f = function +let pr_or_by_notation f = let open Constrexpr in function | {CAst.loc; v=AN v} -> f v | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc diff --git a/printing/pputils.mli b/printing/pputils.mli index 6039168f..5b1969e2 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -9,7 +9,6 @@ (************************************************************************) open Genarg -open Misctypes open Locus open Genredexpr @@ -18,7 +17,7 @@ val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t (** Prints an object surrounded by its commented location *) val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t -val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t +val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t val pr_with_occurrences : ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml deleted file mode 100644 index 5c5b7206..00000000 --- a/printing/ppvernac.ml +++ /dev/null @@ -1,1252 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Names - -open CErrors -open Util -open CAst - -open Extend -open Vernacexpr -open Pputils -open Libnames -open Constrexpr -open Constrexpr_ops -open Decl_kinds - - open Ppconstr - - let do_not_tag _ x = x - let tag_keyword = do_not_tag () - let tag_vernac = do_not_tag - - let keyword s = tag_keyword (str s) - - let pr_constr = pr_constr_expr - let pr_lconstr = pr_lconstr_expr - let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr - - let pr_uconstraint (l, d, r) = - pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ - pr_glob_level r - - let pr_univ_name_list = function - | None -> mt () - | Some l -> - str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}" - - let pr_univdecl_instance l extensible = - prlist_with_sep spc pr_lident l ++ - (if extensible then str"+" else mt ()) - - let pr_univdecl_constraints l extensible = - if List.is_empty l && extensible then mt () - else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++ - (if extensible then str"+" else mt()) - - let pr_universe_decl l = - let open Misctypes in - match l with - | None -> mt () - | Some l -> - str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++ - pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}" - - let pr_ident_decl (lid, l) = - pr_lident lid ++ pr_universe_decl l - - let string_of_fqid fqid = - String.concat "." (List.map Id.to_string fqid) - - let pr_fqid fqid = str (string_of_fqid fqid) - - let pr_lfqid {CAst.loc;v=fqid} = - match loc with - | None -> pr_fqid fqid - | Some loc -> let (b,_) = Loc.unloc loc in - pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid - - let pr_lname_decl (n, u) = - pr_lname n ++ pr_universe_decl u - - let pr_smart_global = Pputils.pr_or_by_notation pr_reference - - let pr_ltac_ref = Libnames.pr_reference - - let pr_module = Libnames.pr_reference - - let pr_import_module = Libnames.pr_reference - - let sep_end = function - | VernacBullet _ - | VernacSubproof _ - | VernacEndSubproof -> str"" - | _ -> str"." - - let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t - - let sep = fun _ -> spc() - let sep_v2 = fun _ -> str"," ++ spc() - - let pr_at_level = function - | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n - | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" - - let pr_constr_as_binder_kind = function - | AsIdent -> keyword "as ident" - | AsIdentOrPattern -> keyword "as pattern" - | AsStrictPattern -> keyword "as strict pattern" - - let pr_strict b = if b then str "strict " else mt () - - let pr_set_entry_type pr = function - | ETName -> str"ident" - | ETReference -> str"global" - | ETPattern (b,None) -> pr_strict b ++ str"pattern" - | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n) - | ETConstr lev -> str"constr" ++ pr lev - | ETOther (_,e) -> str e - | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk - | ETBigint -> str "bigint" - | ETBinder true -> str "binder" - | ETBinder false -> str "closed binder" - - let pr_at_level_opt = function - | None -> mt () - | Some n -> spc () ++ pr_at_level n - - let pr_set_simple_entry_type = - pr_set_entry_type pr_at_level_opt - - let pr_comment pr_c = function - | CommentConstr c -> pr_c c - | CommentString s -> qs s - | CommentInt n -> int n - - let pr_in_out_modules = function - | SearchInside l -> spc() ++ keyword "inside" ++ spc() ++ prlist_with_sep sep pr_module l - | SearchOutside [] -> mt() - | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l - - let pr_search_about (b,c) = - (if b then str "-" else mt()) ++ - match c with - | SearchSubPattern p -> pr_constr_pattern_expr p - | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc - - let pr_search a gopt b pr_p = - pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt - ++ - match a with - | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchAbout sl -> - keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b - - let pr_locality local = if local then keyword "Local" else keyword "Global" - - let pr_explanation (e,b,f) = - let a = match e with - | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.") - | ExplByName id -> pr_id id in - let a = if f then str"!" ++ a else a in - if b then str "[" ++ a ++ str "]" else a - - let pr_option_ref_value = function - | QualidRefValue id -> pr_reference id - | StringRefValue s -> qs s - - let pr_printoption table b = - prlist_with_sep spc str table ++ - pr_opt (prlist_with_sep sep pr_option_ref_value) b - - let pr_set_option a b = - let pr_opt_value = function - | IntValue None -> assert false - (* This should not happen because of the grammar *) - | IntValue (Some n) -> spc() ++ int n - | StringValue s -> spc() ++ str s - | StringOptValue None -> mt() - | StringOptValue (Some s) -> spc() ++ str s - | BoolValue b -> mt() - in pr_printoption a None ++ pr_opt_value b - - let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)" - - let pr_opt_hintbases l = match l with - | [] -> mt() - | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z - - let pr_reference_or_constr pr_c = function - | HintsReference r -> pr_reference r - | HintsConstr c -> pr_c c - - let pr_hint_mode = function - | ModeInput -> str"+" - | ModeNoHeadEvar -> str"!" - | ModeOutput -> str"-" - - let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } = - pr_opt (fun x -> str"|" ++ int x) pri ++ - pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat - - let pr_hints db h pr_c pr_pat = - let opth = pr_opt_hintbases db in - let pph = - match h with - | HintsResolve l -> - keyword "Resolve " ++ prlist_with_sep sep - (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info) - l - | HintsImmediate l -> - keyword "Immediate" ++ spc() ++ - prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l - | HintsUnfold l -> - keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l - | HintsTransparency (l, b) -> - keyword (if b then "Transparent" else "Opaque") - ++ spc () - ++ prlist_with_sep sep pr_reference l - | HintsMode (m, l) -> - keyword "Mode" - ++ spc () - ++ pr_reference m ++ spc() ++ - prlist_with_sep spc pr_hint_mode l - | HintsConstructors c -> - keyword "Constructors" - ++ spc() ++ prlist_with_sep spc pr_reference c - | HintsExtern (n,c,tac) -> - let pat = match c with None -> mt () | Some pat -> pr_pat pat in - keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ - spc() ++ Pputils.pr_raw_generic (Global.env ()) tac - in - hov 2 (keyword "Hint "++ pph ++ opth) - - let pr_with_declaration pr_c = function - | CWith_Definition (id,udecl,c) -> - let p = pr_c c in - keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p - | CWith_Module (id,qid) -> - keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ - pr_ast pr_qualid qid - - let rec pr_module_ast leading_space pr_c = function - | { loc ; v = CMident qid } -> - if leading_space then - spc () ++ pr_located pr_qualid (loc, qid) - else - pr_located pr_qualid (loc,qid) - | { v = CMwith (mty,decl) } -> - let m = pr_module_ast leading_space pr_c mty in - let p = pr_with_declaration pr_c decl in - m ++ spc() ++ keyword "with" ++ spc() ++ p - | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } -> - pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2 - | { v = CMapply (me1,me2) } -> - pr_module_ast leading_space pr_c me1 ++ spc() ++ - hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")") - - let pr_inline = function - | DefaultInline -> mt () - | NoInline -> str "[no inline]" - | InlineAt i -> str "[inline at level " ++ int i ++ str "]" - - let pr_assumption_inline = function - | DefaultInline -> str "Inline" - | NoInline -> mt () - | InlineAt i -> str "Inline(" ++ int i ++ str ")" - - let pr_module_ast_inl leading_space pr_c (mast,inl) = - pr_module_ast leading_space pr_c mast ++ pr_inline inl - - let pr_of_module_type prc = function - | Enforce mty -> str ":" ++ pr_module_ast_inl true prc mty - | Check mtys -> - prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl true prc m) mtys - - let pr_require_token = function - | Some true -> - keyword "Export" ++ spc () - | Some false -> - keyword "Import" ++ spc () - | None -> mt() - - let pr_module_vardecls pr_c (export,idl,(mty,inl)) = - let m = pr_module_ast true pr_c mty in - spc() ++ - hov 1 (str"(" ++ pr_require_token export ++ - prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")") - - let pr_module_binders l pr_c = - prlist_strict (pr_module_vardecls pr_c) l - - let pr_type_option pr_c = function - | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() - | _ as c -> brk(0,2) ++ str" :" ++ pr_c c - - let pr_decl_notation prc ({loc; v=ntn},c,scopt) = - fnl () ++ keyword "where " ++ qs ntn ++ str " := " - ++ Flags.without_option Flags.beautify prc c ++ - pr_opt (fun sc -> str ": " ++ str sc) scopt - - let pr_binders_arg = - pr_non_empty_arg pr_binders - - let pr_and_type_binders_arg bl = - pr_binders_arg bl - - let pr_onescheme (idop,schem) = - match schem with - | InductionScheme (dep,ind,s) -> - (match idop with - | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() - | None -> spc () - ) ++ - hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for") - ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s) - | CaseScheme (dep,ind,s) -> - (match idop with - | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() - | None -> spc () - ) ++ - hov 0 ((if dep then keyword "Elimination for" else keyword "Case for") - ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s) - | EqualityScheme ind -> - (match idop with - | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() - | None -> spc() - ) ++ - hov 0 (keyword "Equality for") - ++ spc() ++ pr_smart_global ind - - let begin_of_inductive = function - | [] -> 0 - | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc - - let pr_class_rawexpr = function - | FunClass -> keyword "Funclass" - | SortClass -> keyword "Sortclass" - | RefClass qid -> pr_smart_global qid - - let pr_assumption_token many discharge kind = - match discharge, kind with - | (NoDischarge,Logical) -> - keyword (if many then "Axioms" else "Axiom") - | (NoDischarge,Definitional) -> - keyword (if many then "Parameters" else "Parameter") - | (NoDischarge,Conjectural) -> str"Conjecture" - | (DoDischarge,Logical) -> - keyword (if many then "Hypotheses" else "Hypothesis") - | (DoDischarge,Definitional) -> - keyword (if many then "Variables" else "Variable") - | (DoDischarge,Conjectural) -> - anomaly (Pp.str "Don't know how to beautify a local conjecture.") - - let pr_params pr_c (xl,(c,t)) = - hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ - (if c then str":>" else str":" ++ - spc() ++ pr_c t)) - - let rec factorize = function - | [] -> [] - | (c,(idl,t))::l -> - match factorize l with - | (xl,((c', t') as r))::l' - when (c : bool) == c' && Pervasives.(=) t t' -> - (** FIXME: we need equality on constr_expr *) - (idl@xl,r)::l' - | l' -> (idl,(c,t))::l' - - let pr_ne_params_list pr_c l = - match factorize l with - | [p] -> pr_params pr_c p - | l -> - prlist_with_sep spc - (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l - -(* - prlist_with_sep pr_semicolon (pr_params pr_c) -*) - - let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) - - let pr_syntax_modifier = function - | SetItemLevel (l,n) -> - prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n - | SetItemLevelAsBinder (l,bk,n) -> - prlist_with_sep sep_v2 str l ++ - spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk - | SetLevel n -> pr_at_level (NumLevel n) - | SetAssoc LeftA -> keyword "left associativity" - | SetAssoc RightA -> keyword "right associativity" - | SetAssoc NonA -> keyword "no associativity" - | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ - | SetOnlyPrinting -> keyword "only printing" - | SetOnlyParsing -> keyword "only parsing" - | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") - | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s - | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s - - let pr_syntax_modifiers = function - | [] -> mt() - | l -> spc() ++ - hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - - let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) = - let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in - let annot = pr_guard_annot pr_lconstr_expr bl ro in - pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot - ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ - ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def - ++ prlist (pr_decl_notation pr_constr) ntn - - let pr_statement head (idpl,(bl,c)) = - hov 2 - (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++ - (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ - str":" ++ pr_spc_lconstr c) - -(**************************************) -(* Pretty printer for vernac commands *) -(**************************************) - - let pr_constrarg c = spc () ++ pr_constr c - let pr_lconstrarg c = spc () ++ pr_lconstr c - let pr_intarg n = spc () ++ int n - - let pr_oc = function - | None -> str" :" - | Some true -> str" :>" - | Some false -> str" :>>" - - let pr_record_field ((x, pri), ntn) = - let prx = match x with - | (oc,AssumExpr (id,t)) -> - hov 1 (pr_lname id ++ - pr_oc oc ++ spc() ++ - pr_lconstr_expr t) - | (oc,DefExpr(id,b,opt)) -> (match opt with - | Some t -> - hov 1 (pr_lname id ++ - pr_oc oc ++ spc() ++ - pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) - | None -> - hov 1 (pr_lname id ++ str" :=" ++ spc() ++ - pr_lconstr b)) in - let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in - prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn - - let pr_record_decl b c fs = - pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") - - let pr_printable = function - | PrintFullContext -> - keyword "Print All" - | PrintSectionContext s -> - keyword "Print Section" ++ spc() ++ Libnames.pr_reference s - | PrintGrammar ent -> - keyword "Print Grammar" ++ spc() ++ str ent - | PrintLoadPath dir -> - keyword "Print LoadPath" ++ pr_opt DirPath.print dir - | PrintModules -> - keyword "Print Modules" - | PrintMLLoadPath -> - keyword "Print ML Path" - | PrintMLModules -> - keyword "Print ML Modules" - | PrintDebugGC -> - keyword "Print ML GC" - | PrintGraph -> - keyword "Print Graph" - | PrintClasses -> - keyword "Print Classes" - | PrintTypeClasses -> - keyword "Print TypeClasses" - | PrintInstances qid -> - keyword "Print Instances" ++ spc () ++ pr_smart_global qid - | PrintCoercions -> - keyword "Print Coercions" - | PrintCoercionPaths (s,t) -> - keyword "Print Coercion Paths" ++ spc() - ++ pr_class_rawexpr s ++ spc() - ++ pr_class_rawexpr t - | PrintCanonicalConversions -> - keyword "Print Canonical Structures" - | PrintTables -> - keyword "Print Tables" - | PrintHintGoal -> - keyword "Print Hint" - | PrintHint qid -> - keyword "Print Hint" ++ spc () ++ pr_smart_global qid - | PrintHintDb -> - keyword "Print Hint *" - | PrintHintDbName s -> - keyword "Print HintDb" ++ spc () ++ str s - | PrintUniverses (b, fopt) -> - let cmd = - if b then "Print Sorted Universes" - else "Print Universes" - in - keyword cmd ++ pr_opt str fopt - | PrintName (qid,udecl) -> - keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl - | PrintModuleType qid -> - keyword "Print Module Type" ++ spc() ++ pr_reference qid - | PrintModule qid -> - keyword "Print Module" ++ spc() ++ pr_reference qid - | PrintInspect n -> - keyword "Inspect" ++ spc() ++ int n - | PrintScopes -> - keyword "Print Scopes" - | PrintScope s -> - keyword "Print Scope" ++ spc() ++ str s - | PrintVisibility s -> - keyword "Print Visibility" ++ pr_opt str s - | PrintAbout (qid,l,gopt) -> - pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt - ++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l - | PrintImplicit qid -> - keyword "Print Implicit" ++ spc() ++ pr_smart_global qid - (* spiwack: command printing all the axioms and section variables used in a - term *) - | PrintAssumptions (b, t, qid) -> - let cmd = match b, t with - | true, true -> "Print All Dependencies" - | true, false -> "Print Opaque Dependencies" - | false, true -> "Print Transparent Dependencies" - | false, false -> "Print Assumptions" - in - keyword cmd ++ spc() ++ pr_smart_global qid - | PrintNamespace dp -> - keyword "Print Namespace" ++ DirPath.print dp - | PrintStrategy None -> - keyword "Print Strategies" - | PrintStrategy (Some qid) -> - keyword "Print Strategy" ++ pr_smart_global qid - - let pr_using e = - let rec aux = function - | SsEmpty -> "()" - | SsType -> "(Type)" - | SsSingl { v=id } -> "("^Id.to_string id^")" - | SsCompl e -> "-" ^ aux e^"" - | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" - | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" - | SsFwdClose e -> "("^aux e^")*" - in Pp.str (aux e) - - let pr_extend s cl = - let pr_arg a = - try pr_gen a - with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in - try - let rl = Egramml.get_extend_vernac_rule s in - let rec aux rl cl = - match rl, cl with - | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl - | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl - | [], [] -> [] - | _ -> assert false in - hov 1 (pr_sequence identity (aux rl cl)) - with Not_found -> - hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") - - let pr_vernac_expr v = - let return = tag_vernac v in - match v with - | VernacLoad (f,s) -> - return ( - keyword "Load" - ++ if f then - (spc() ++ keyword "Verbose" ++ spc()) - else - spc() ++ qs s - ) - - (* Proof management *) - | VernacAbortAll -> - return (keyword "Abort All") - | VernacRestart -> - return (keyword "Restart") - | VernacUnfocus -> - return (keyword "Unfocus") - | VernacUnfocused -> - return (keyword "Unfocused") - | VernacAbort id -> - return (keyword "Abort" ++ pr_opt pr_lident id) - | VernacUndo i -> - return ( - if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i - ) - | VernacUndoTo i -> - return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i) - | VernacBacktrack (i,j,k) -> - return (keyword "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k]) - | VernacFocus i -> - return (keyword "Focus" ++ pr_opt int i) - | VernacShow s -> - let pr_goal_reference = function - | OpenSubgoals -> mt () - | NthGoal n -> spc () ++ int n - | GoalId id -> spc () ++ pr_id id - in - let pr_showable = function - | ShowGoal n -> keyword "Show" ++ pr_goal_reference n - | ShowProof -> keyword "Show Proof" - | ShowScript -> keyword "Show Script" - | ShowExistentials -> keyword "Show Existentials" - | ShowUniverses -> keyword "Show Universes" - | ShowProofNames -> keyword "Show Conjectures" - | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") - | ShowMatch id -> keyword "Show Match " ++ pr_reference id - in - return (pr_showable s) - | VernacCheckGuard -> - return (keyword "Guarded") - - (* Resetting *) - | VernacResetName id -> - return (keyword "Reset" ++ spc() ++ pr_lident id) - | VernacResetInitial -> - return (keyword "Reset Initial") - | VernacBack i -> - return ( - if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i - ) - | VernacBackTo i -> - return (keyword "BackTo" ++ pr_intarg i) - - (* State management *) - | VernacWriteState s -> - return (keyword "Write State" ++ spc () ++ qs s) - | VernacRestoreState s -> - return (keyword "Restore State" ++ spc() ++ qs s) - - (* Syntax *) - | VernacOpenCloseScope (opening,sc) -> - return ( - keyword (if opening then "Open " else "Close ") ++ - keyword "Scope" ++ spc() ++ str sc - ) - | VernacDelimiters (sc,Some key) -> - return ( - keyword "Delimit Scope" ++ spc () ++ str sc ++ - spc() ++ keyword "with" ++ spc () ++ str key - ) - | VernacDelimiters (sc, None) -> - return ( - keyword "Undelimit Scope" ++ spc () ++ str sc - ) - | VernacBindScope (sc,cll) -> - return ( - keyword "Bind Scope" ++ spc () ++ str sc ++ - spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll - ) - | VernacArgumentsScope (q,scl) -> - let pr_opt_scope = function - | None -> str"_" - | Some sc -> str sc - in - return ( - keyword "Arguments Scope" - ++ spc() ++ pr_smart_global q - ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - ) - | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) - return ( - hov 0 (hov 0 (keyword "Infix " - ++ qs s ++ str " :=" ++ pr_constrarg q) ++ - pr_syntax_modifiers mv ++ - (match sn with - | None -> mt() - | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) - ) - | VernacNotation (c,({v=s},l),opt) -> - return ( - hov 2 (keyword "Notation" ++ spc() ++ qs s ++ - str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++ - (match opt with - | None -> mt() - | Some sc -> str" :" ++ spc() ++ str sc)) - ) - | VernacSyntaxExtension (_, (s, l)) -> - return ( - keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++ - pr_syntax_modifiers l - ) - | VernacNotationAddFormat(s,k,v) -> - return ( - keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v - ) - - (* Gallina *) - | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *) - let pr_def_token dk = - keyword ( - if Name.is_anonymous (fst id).v - then "Goal" - else Kindops.string_of_definition_object_kind dk) - in - let pr_reduce = function - | None -> mt() - | Some r -> - keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ - keyword " in" ++ spc() - in - let pr_def_body = function - | DefineBody (bl,red,body,d) -> - let ty = match d with - | None -> mt() - | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty - in - (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) - | ProveBody (bl,t) -> - let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in - (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in - let (binds,typ,c) = pr_def_body b in - return ( - hov 2 ( - pr_def_token kind ++ spc() - ++ pr_lname_decl id ++ binds ++ typ - ++ (match c with - | None -> mt() - | Some cc -> str" :=" ++ spc() ++ cc)) - ) - - | VernacStartTheoremProof (ki,l) -> - return ( - hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ - prlist (pr_statement (spc () ++ keyword "with")) (List.tl l)) - ) - - | VernacEndProof Admitted -> - return (keyword "Admitted") - - | VernacEndProof (Proved (opac,o)) -> return ( - match o with - | None -> (match opac with - | Transparent -> keyword "Defined" - | Opaque -> keyword "Qed") - | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id - ) - | VernacExactProof c -> - return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) - | VernacAssumption ((discharge,kind),t,l) -> - let n = List.length (List.flatten (List.map fst (List.map snd l))) in - let pr_params (c, (xl, t)) = - hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++ - (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in - let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in - return (hov 2 (pr_assumption_token (n > 1) discharge kind ++ - pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) - | VernacInductive (cum, p,f,l) -> - let pr_constructor (coe,(id,c)) = - hov 2 (pr_lident id ++ str" " ++ - (if coe then str":>" else str":") ++ - Flags.without_option Flags.beautify pr_spc_lconstr c) - in - let pr_constructor_list b l = match l with - | Constructors [] -> mt() - | Constructors l -> - let fst_sep = match l with [_] -> " " | _ -> " | " in - pr_com_at (begin_of_inductive l) ++ - fnl() ++ str fst_sep ++ - prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l - | RecordDecl (c,fs) -> - pr_record_decl b c fs - in - let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) = - hov 0 ( - str key ++ spc() ++ - (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++ - pr_and_type_binders_arg indpar ++ - pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++ - str" :=") ++ pr_constructor_list k lc ++ - prlist (pr_decl_notation pr_constr) ntn - in - let key = - let (_,_,_,k,_),_ = List.hd l in - let kind = - match k with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" - in - if p then - let cm = - match cum with - | GlobalCumulativity | LocalCumulativity -> "Cumulative" - | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative" - in - cm ^ " " ^ kind - else kind - in - return ( - hov 1 (pr_oneind key (List.hd l)) ++ - (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) - ) - - | VernacFixpoint (local, recs) -> - let local = match local with - | DoDischarge -> "Let " - | NoDischarge -> "" - in - return ( - hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ - prlist_with_sep (fun _ -> fnl () ++ keyword "with" - ++ spc ()) pr_rec_definition recs) - ) - - | VernacCoFixpoint (local, corecs) -> - let local = match local with - | DoDischarge -> keyword "Let" ++ spc () - | NoDischarge -> str "" - in - let pr_onecorec ((iddecl,bl,c,def),ntn) = - pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ - spc() ++ pr_lconstr_expr c ++ - pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++ - prlist (pr_decl_notation pr_constr) ntn - in - return ( - hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) - ) - | VernacScheme l -> - return ( - hov 2 (keyword "Scheme" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l) - ) - | VernacCombinedScheme (id, l) -> - return ( - hov 2 (keyword "Combined Scheme" ++ spc() ++ - pr_lident id ++ spc() ++ keyword "from" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) - ) - | VernacUniverse v -> - return ( - hov 2 (keyword "Universe" ++ spc () ++ - prlist_with_sep (fun _ -> str",") pr_lident v) - ) - | VernacConstraint v -> - return ( - hov 2 (keyword "Constraint" ++ spc () ++ - prlist_with_sep (fun _ -> str",") pr_uconstraint v) - ) - - (* Gallina extensions *) - | VernacBeginSection id -> - return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id)) - | VernacEndSegment id -> - return (hov 2 (keyword "End" ++ spc() ++ pr_lident id)) - | VernacNameSectionHypSet (id,set) -> - return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++ - str ":="++spc()++pr_using set)) - | VernacRequire (from, exp, l) -> - let from = match from with - | None -> mt () - | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc () - in - return ( - hov 2 - (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++ - prlist_with_sep sep pr_module l) - ) - | VernacImport (f,l) -> - return ( - (if f then keyword "Export" else keyword "Import") ++ spc() ++ - prlist_with_sep sep pr_import_module l - ) - | VernacCanonical q -> - return ( - keyword "Canonical Structure" ++ spc() ++ pr_smart_global q - ) - | VernacCoercion (id,c1,c2) -> - return ( - hov 1 ( - keyword "Coercion" ++ spc() ++ - pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ - spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) - ) - | VernacIdentityCoercion (id,c1,c2) -> - return ( - hov 1 ( - keyword "Identity Coercion" ++ spc() ++ pr_lident id ++ - spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ - spc() ++ pr_class_rawexpr c2) - ) - - | VernacInstance (abst, sup, (instid, bk, cl), props, info) -> - return ( - hov 1 ( - (if abst then keyword "Declare" ++ spc () else mt ()) ++ - keyword "Instance" ++ - (match instid with - | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc () - | { v = Anonymous }, _ -> mt ()) ++ - pr_and_type_binders_arg sup ++ - str":" ++ spc () ++ - (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ - pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ - (match props with - | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" - | Some (true,_) -> assert false - | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p - | None -> mt())) - ) - - | VernacContext l -> - return ( - hov 1 ( - keyword "Context" ++ pr_and_type_binders_arg l) - ) - - | VernacDeclareInstances insts -> - let pr_inst (id, info) = - pr_reference id ++ pr_hint_info pr_constr_pattern_expr info - in - return ( - hov 1 (keyword "Existing" ++ spc () ++ - keyword(String.plural (List.length insts) "Instance") ++ - spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts) - ) - - | VernacDeclareClass id -> - return ( - hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id) - ) - - (* Modules and Module Types *) - | VernacDefineModule (export,m,bl,tys,bd) -> - let b = pr_module_binders bl pr_lconstr in - return ( - hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++ - pr_lident m ++ b ++ - pr_of_module_type pr_lconstr tys ++ - (if List.is_empty bd then mt () else str ":= ") ++ - prlist_with_sep (fun () -> str " <+") - (pr_module_ast_inl true pr_lconstr) bd) - ) - | VernacDeclareModule (export,id,bl,m1) -> - let b = pr_module_binders bl pr_lconstr in - return ( - hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++ - pr_lident id ++ b ++ str " :" ++ - pr_module_ast_inl true pr_lconstr m1) - ) - | VernacDeclareModuleType (id,bl,tyl,m) -> - let b = pr_module_binders bl pr_lconstr in - let pr_mt = pr_module_ast_inl true pr_lconstr in - return ( - hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++ - prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++ - (if List.is_empty m then mt () else str ":= ") ++ - prlist_with_sep (fun () -> str " <+ ") pr_mt m) - ) - | VernacInclude (mexprs) -> - let pr_m = pr_module_ast_inl false pr_lconstr in - return ( - hov 2 (keyword "Include" ++ spc() ++ - prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) - ) - (* Solving *) - | VernacSolveExistential (i,c) -> - return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) - - (* Auxiliary file and library management *) - | VernacAddLoadPath (fl,s,d) -> - return ( - hov 2 - (keyword "Add" ++ - (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ - keyword "LoadPath" ++ spc() ++ qs s ++ - (match d with - | None -> mt() - | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) - ) - | VernacRemoveLoadPath s -> - return (keyword "Remove LoadPath" ++ qs s) - | VernacAddMLPath (fl,s) -> - return ( - keyword "Add" - ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) - ++ keyword "ML Path" - ++ qs s - ) - | VernacDeclareMLModule (l) -> - return ( - hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l) - ) - | VernacChdir s -> - return (keyword "Cd" ++ pr_opt qs s) - - (* Commands *) - | VernacCreateHintDb (dbname,b) -> - return ( - hov 1 (keyword "Create HintDb" ++ spc () ++ - str dbname ++ (if b then str" discriminated" else mt ())) - ) - | VernacRemoveHints (dbnames, ids) -> - return ( - hov 1 (keyword "Remove Hints" ++ spc () ++ - prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ - pr_opt_hintbases dbnames) - ) - | VernacHints (dbnames,h) -> - return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),compat) -> - return ( - hov 2 - (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ - prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ - pr_syntax_modifiers - (match compat with - | None -> [] - | Some Flags.Current -> [SetOnlyParsing] - | Some v -> [SetCompatVersion v])) - ) - | VernacDeclareImplicits (q,[]) -> - return ( - hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q) - ) - | VernacDeclareImplicits (q,impls) -> - return ( - hov 1 (keyword "Implicit Arguments" ++ spc () ++ - spc() ++ pr_smart_global q ++ spc() ++ - prlist_with_sep spc (fun imps -> - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") - impls) - ) - | VernacArguments (q, args, more_implicits, nargs, mods) -> - return ( - hov 2 ( - keyword "Arguments" ++ spc() ++ - pr_smart_global q ++ - let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in - let pr_if b x = if b then x else str "" in - let pr_br imp x = match imp with - | Vernacexpr.Implicit -> str "[" ++ x ++ str "]" - | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}" - | Vernacexpr.NotImplicit -> x in - let rec print_arguments n l = - match n, l with - | Some 0, l -> spc () ++ str"/" ++ print_arguments None l - | _, [] -> mt() - | n, { name = id; recarg_like = k; - notation_scope = s; - implicit_status = imp } :: tl -> - spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++ - print_arguments (Option.map pred n) tl - in - let rec print_implicits = function - | [] -> mt () - | (name, impl) :: rest -> - spc() ++ pr_br impl (Name.print name) ++ print_implicits rest - in - print_arguments nargs args ++ - if not (List.is_empty more_implicits) then - prlist (fun l -> str"," ++ print_implicits l) more_implicits - else (mt ()) ++ - (if not (List.is_empty mods) then str" : " else str"") ++ - prlist_with_sep (fun () -> str", " ++ spc()) (function - | `ReductionDontExposeCase -> keyword "simpl nomatch" - | `ReductionNeverUnfold -> keyword "simpl never" - | `DefaultImplicits -> keyword "default implicits" - | `Rename -> keyword "rename" - | `Assert -> keyword "assert" - | `ExtraScopes -> keyword "extra scopes" - | `ClearImplicits -> keyword "clear implicits" - | `ClearScopes -> keyword "clear scopes") - mods) - ) - | VernacReserve bl -> - let n = List.length (List.flatten (List.map fst bl)) in - return ( - hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " ")) - ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl)) - ) - | VernacGeneralizable g -> - return ( - hov 1 (tag_keyword ( - str"Generalizable Variable" ++ - match g with - | None -> str "s none" - | Some [] -> str "s all" - | Some idl -> - str (if List.length idl > 1 then "s " else " ") ++ - prlist_with_sep spc pr_lident idl) - )) - | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k -> - return ( - hov 1 (keyword "Transparent" ++ - spc() ++ prlist_with_sep sep pr_smart_global l) - ) - | VernacSetOpacity(Conv_oracle.Opaque,l) -> - return ( - hov 1 (keyword "Opaque" ++ - spc() ++ prlist_with_sep sep pr_smart_global l) - ) - | VernacSetOpacity _ -> - return ( - CErrors.anomaly (keyword "VernacSetOpacity used to set something else.") - ) - | VernacSetStrategy l -> - let pr_lev = function - | Conv_oracle.Opaque -> keyword "opaque" - | Conv_oracle.Expand -> keyword "expand" - | l when Conv_oracle.is_transparent l -> keyword "transparent" - | Conv_oracle.Level n -> int n - in - let pr_line (l,q) = - hov 2 (pr_lev l ++ spc() ++ - str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") - in - return ( - hov 1 (keyword "Strategy" ++ spc() ++ - hv 0 (prlist_with_sep sep pr_line l)) - ) - | VernacUnsetOption (export, na) -> - let export = if export then keyword "Export" ++ spc () else mt () in - return ( - hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None) - ) - | VernacSetOption (export, na,v) -> - let export = if export then keyword "Export" ++ spc () else mt () in - return ( - hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v) - ) - | VernacAddOption (na,l) -> - return ( - hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l)) - ) - | VernacRemoveOption (na,l) -> - return ( - hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l)) - ) - | VernacMemOption (na,l) -> - return ( - hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l)) - ) - | VernacPrintOption na -> - return ( - hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None) - ) - | VernacCheckMayEval (r,io,c) -> - let pr_mayeval r c = match r with - | Some r0 -> - hov 2 (keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ - spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) - | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) - in - let pr_i = match io with None -> mt () - | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in - return (pr_i ++ pr_mayeval r c) - | VernacGlobalCheck c -> - return (hov 2 (keyword "Type" ++ pr_constrarg c)) - | VernacDeclareReduction (s,r) -> - return ( - keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r - ) - | VernacPrint p -> - return (pr_printable p) - | VernacSearch (sea,g,sea_r) -> - return (pr_search sea g sea_r pr_constr_pattern_expr) - | VernacLocate loc -> - let pr_locate =function - | LocateAny qid -> pr_smart_global qid - | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid - | LocateFile f -> keyword "File" ++ spc() ++ qs f - | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid - | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid - | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid - in - return (keyword "Locate" ++ spc() ++ pr_locate loc) - | VernacRegister (id, RegisterInline) -> - return ( - hov 2 - (keyword "Register Inline" ++ spc() ++ pr_lident id) - ) - | VernacComments l -> - return ( - hov 2 - (keyword "Comments" ++ spc() - ++ prlist_with_sep sep (pr_comment pr_constr) l) - ) - - (* Toplevel control *) - | VernacToplevelControl exn -> - return (pr_topcmd exn) - - (* For extension *) - | VernacExtend (s,c) -> - return (pr_extend s c) - | VernacProof (None, None) -> - return (keyword "Proof") - | VernacProof (None, Some e) -> - return (keyword "Proof " ++ spc () ++ - keyword "using" ++ spc() ++ pr_using e) - | VernacProof (Some te, None) -> - return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te) - | VernacProof (Some te, Some e) -> - return ( - keyword "Proof" ++ spc () ++ - keyword "using" ++ spc() ++ pr_using e ++ spc() ++ - keyword "with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te - ) - | VernacProofMode s -> - return (keyword "Proof Mode" ++ str s) - | VernacBullet b -> - return (begin match b with - | Dash n -> str (String.make n '-') - | Star n -> str (String.make n '*') - | Plus n -> str (String.make n '+') - end) - | VernacSubproof None -> - return (str "{") - | VernacSubproof (Some i) -> - return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") - | VernacEndSubproof -> - return (str "}") - -let pr_vernac_flag = - function - | VernacPolymorphic true -> keyword "Polymorphic" - | VernacPolymorphic false -> keyword "Monomorphic" - | VernacProgram -> keyword "Program" - | VernacLocal local -> pr_locality local - - let rec pr_vernac_control v = - let return = tag_vernac v in - match v with - | VernacExpr (f, v') -> - List.fold_right - (fun f a -> pr_vernac_flag f ++ spc() ++ a) - f - (pr_vernac_expr v' ++ sep_end v') - | VernacTime (_,{v}) -> - return (keyword "Time" ++ spc() ++ pr_vernac_control v) - | VernacRedirect (s, {v}) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) - | VernacTimeout(n,v) -> - return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v) - | VernacFail v -> - return (keyword "Fail" ++ spc() ++ pr_vernac_control v) - - let pr_vernac v = - try pr_vernac_control v - with e -> CErrors.print e diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli deleted file mode 100644 index 4aa24bf5..00000000 --- a/printing/ppvernac.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* * 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 vernac_expr syntactic - objects and their subcomponents. *) - -val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t - -(** Prints a fixpoint body *) -val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t - -(** Prints a vernac expression without dot *) -val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t - -(** Prints a "proof using X" clause. *) -val pr_using : Vernacexpr.section_subset_expr -> Pp.t - -(** Prints a vernac expression and closes it with a dot. *) -val pr_vernac : Vernacexpr.vernac_control -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1f17d844..1810cc65 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -26,7 +26,6 @@ open Libobject open Libnames open Globnames open Recordops -open Misctypes open Printer open Printmod open Context.Rel.Declaration @@ -35,13 +34,13 @@ open Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type object_pr = { - print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t; - print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t; + 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 -> Context.Named.Declaration.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; @@ -77,7 +76,9 @@ let print_ref reduce ref udecl = let typ = EConstr.of_constr typ in let typ = if reduce then - let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ + let env = Global.env () in + let sigma = Evd.from_env env in + let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in @@ -93,11 +94,12 @@ let print_ref reduce ref udecl = let inst = Univ.AUContext.instance univs in let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in let env = Global.env () in - let bl = Universes.universe_binders_with_opt_names ref + let bl = UnivNames.universe_binders_with_opt_names ref (Array.to_list (Univ.Instance.to_array inst)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = - if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs + if Global.is_polymorphic ref + then Printer.pr_universe_instance sigma (Univ.UContext.instance univs) else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ @@ -245,13 +247,13 @@ let print_type_in_type ref = else [] let print_primitive_record recflag mipv = function - | Some (Some (_, ps,_)) -> + | 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 @@ -328,7 +330,7 @@ type 'a locatable_info = { type locatable = Locatable : 'a locatable_info -> locatable type logical_name = - | Term of global_reference + | Term of GlobRef.t | Dir of global_dir_reference | Syntactic of KerName.t | ModuleType of ModPath.t @@ -343,8 +345,7 @@ let register_locatable name f = exception ObjFound of logical_name -let locate_any_name ref = - let {v=qid} = qualid_of_reference ref in +let locate_any_name qid = try Term (Nametab.locate qid) with Not_found -> try Syntactic (Nametab.locate_syndef qid) @@ -376,7 +377,6 @@ let pr_located_qualid = function | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir | DirModule { obj_dir ; _ } -> "Module", obj_dir - | DirClosedSection dir -> "Closed Section", dir in str s ++ spc () ++ DirPath.print dir | ModuleType mp -> @@ -452,8 +452,7 @@ type locatable_kind = | LocOther of string | LocAny -let print_located_qualid name flags ref = - let {v=qid} = qualid_of_reference ref in +let print_located_qualid name flags qid = let located = match flags with | LocTerm -> locate_term qid | LocModule -> locate_modtype qid @ locate_module qid @@ -554,8 +553,7 @@ let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then let univs = Declareops.constant_polymorphic_context cb in let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in - pr_universe_instance sigma univs + pr_universe_instance sigma inst else mt() let print_constant with_values sep sp udecl = @@ -595,7 +593,7 @@ let print_constant with_values sep sp udecl = in let ctx = UState.of_binders - (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl) + (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in @@ -659,14 +657,10 @@ let gallina_print_library_entry env sigma with_values ent = gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> - Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { obj_dir; _ }) -> Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) - | (oname,Lib.ClosedModule _) -> - Some (str " >>>>>>> Closed Module " ++ pr_name oname) let gallina_print_context env sigma with_values = let rec prec n = function @@ -718,7 +712,10 @@ let print_eval x = !object_pr.print_eval x (**** Printing declarations and judgments *) (**** Abstract layer *****) -let print_typed_value x = print_typed_value_in_env (Global.env ()) Evd.empty x +let print_typed_value x = + let env = Global.env () in + let sigma = Evd.from_env env in + print_typed_value_in_env env sigma x let print_judgment env sigma {uj_val=trm;uj_type=typ} = print_typed_value_in_env env sigma (trm, typ) @@ -784,18 +781,14 @@ let print_full_pure_context env sigma = follows the definition of the inductive type *) (* This is designed to print the contents of an opened section *) -let read_sec_context r = - let qid = qualid_of_reference r in +let read_sec_context qid = let dir = - try Nametab.locate_section qid.v + 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 ({obj_dir;_},_) as hd)::rest -> if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | (_,Lib.ClosedSection _)::rest -> - user_err Pp.(str "Cannot print the contents of a closed section.") - (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in @@ -839,12 +832,12 @@ let print_any_name env sigma na udecl = let print_name env sigma na udecl = match na with - | {loc; v=ByNotation (ntn,sc)} -> + | {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=AN ref} -> + | {loc; v=Constrexpr.AN ref} -> print_any_name env sigma (locate_any_name ref) udecl let print_opaque_name env sigma qid = @@ -892,11 +885,11 @@ let print_about_any ?loc env sigma k udecl = let print_about env sigma na udecl = match na with - | {loc;v=ByNotation (ntn,sc)} -> + | {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=AN ref} -> + | {loc;v=Constrexpr.AN ref} -> print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) @@ -909,7 +902,7 @@ let inspect env sigma depth = open Classops -let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v) +let print_coercion_value env sigma v = Printer.pr_global v.coe_value let print_class i = let cl,_ = class_info_from_index i in diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 213f0aee..1668bce2 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,8 +12,6 @@ open Names open Environ open Reductionops open Libnames -open Globnames -open Misctypes open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -26,20 +24,20 @@ val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node 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 -> reference -> Pp.t -val print_sec_context_typ : env -> Evd.evar_map -> reference -> 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 -> reference or_by_notation -> - Universes.univ_name_list option -> Pp.t -val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t -val print_about : env -> Evd.evar_map -> reference or_by_notation -> - Universes.univ_name_list option -> Pp.t -val print_impargs : reference or_by_notation -> 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 : env -> evar_map -> Pp.t @@ -50,7 +48,7 @@ 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 : global_reference -> 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 @@ -79,19 +77,19 @@ val register_locatable : string -> 'a locatable_info -> unit name describing the kind of objects considered and that is added as a grammar command prefix for vernacular commands Locate. *) -val print_located_qualid : reference -> Pp.t -val print_located_term : reference -> Pp.t -val print_located_module : reference -> Pp.t -val print_located_other : string -> reference -> Pp.t +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 -> Universes.univ_name_list option -> Pp.t; - print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t; + 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 -> Context.Named.Declaration.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; diff --git a/printing/printer.ml b/printing/printer.ml index 199aa79c..b4038e0f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -82,24 +82,23 @@ 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 goal_concl_style env sigma t = - pr_lconstr_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 env sigma c = pr_leconstr_core false env sigma (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 _ = Hook.set Refine.pr_constr pr_constr_env 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_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c -let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c - 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 + (* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = let (sigma, env) = Pfedit.get_current_context () in @@ -108,12 +107,12 @@ let pr_constr t = let (sigma, env) = Pfedit.get_current_context () in pr_constr_env env sigma t -let pr_open_lconstr (_,c) = pr_lconstr c -let pr_open_constr (_,c) = pr_constr c - let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c) let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c) +let pr_open_lconstr (_,c) = pr_leconstr c +let pr_open_constr (_,c) = pr_econstr 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 *) @@ -133,8 +132,7 @@ let pr_lconstr_under_binders c = 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 goal_concl_style env sigma t = - pr_lconstr_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) @@ -194,7 +192,7 @@ let pr_constr_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) -let _ = Termops.set_print_constr +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 pr x = str "(* " ++ pr x ++ str " *)" @@ -229,15 +227,15 @@ let dirpath_of_global = function dirpath_of_mp (MutInd.modpath kn) | VarRef _ -> DirPath.empty -let qualid_of_global env r = - Libnames.make_qualid (dirpath_of_global r) (id_of_global env r) +let 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 -> - CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r) + qualid_of_global ?loc env r in Constrextern.set_extern_reference extern_ref; try @@ -290,17 +288,19 @@ let pr_cumulativity_info sigma cumi = let pr_global_env = pr_global_env let pr_global = pr_global_env Id.Set.empty -let pr_puniverses f env (c,u) = - f env c ++ - (if !Constrextern.print_universes then - str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" - else mt ()) +let pr_universe_instance evd inst = + str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" + +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.empty (mkInd ind) -let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr) +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 @@ -493,16 +493,23 @@ let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) -(* display complete goal *) -let default_pr_goal gs = - let g = sig_it gs in - let sigma = project gs in +(* 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 = - pr_context_of env sigma ++ cut () ++ - str "============================" ++ cut () ++ - pr_goal_concl_style_env env sigma concl in + 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 *) @@ -518,13 +525,18 @@ let pr_goal_name sigma g = 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 ()) + ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ()) (* display the conclusion of a goal *) -let pr_concl n sigma g = +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 = pr_goal_concl_style_env env sigma (Goal.V82.concl 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 @@ -541,12 +553,12 @@ let pr_evgl_sign sigma evi = if List.is_empty ids then mt () else (str " (" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") in - let pc = pr_lconstr_env env sigma evi.evar_concl in + 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_lconstr_env env sigma) l ++ str "}" + prlist_with_sep (fun () -> str "|") (pr_leconstr_env env sigma) l ++ str "}" | _ -> mt () in @@ -591,11 +603,11 @@ let pr_ne_evar_set hd tl sigma l = mt () let pr_selected_subgoal name sigma g = - let pg = default_pr_goal { sigma=sigma ; it=g; } in + 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 default_pr_subgoal n sigma = +let pr_subgoal n sigma = let rec prrec p = function | [] -> user_err Pp.(str "No such goal.") | g::rest -> @@ -622,8 +634,8 @@ let print_evar_constraints gl sigma = end in let pr_evconstr (pbty,env,t1,t2) = - let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1) - and t2 = Evarutil.nf_evar sigma (EConstr.of_constr t2) in + 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 @@ -691,12 +703,25 @@ let print_dependent_evars gl sigma seeds = 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. *) -let default_pr_subgoals ?(pr_first=true) +(* [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 + + let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *) + try GoalMap.find ng diff_goal_map with Not_found -> ng + in + (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a @@ -729,17 +754,24 @@ let default_pr_subgoals ?(pr_first=true) if needed then str" focused " else str" " (* non-breakable space *) in - (** Main function *) + + let get_ogs g = + match os_map with + | Some (osigma, _) -> Some { it = map_goal_for_diff g; sigma = osigma } + | None -> None + in let rec pr_rec n = function | [] -> (mt ()) | g::rest -> - let pc = pr_concl n sigma g in + 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 - default_pr_goal { it = g ; sigma = sigma; } + 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 @@ -751,6 +783,8 @@ let default_pr_subgoals ?(pr_first=true) | Some cmd -> Feedback.msg_info cmd | None -> () in + + (** Main function *) match goals with | [] -> begin @@ -780,34 +814,7 @@ let default_pr_subgoals ?(pr_first=true) ++ print_dependent_evars (Some g1) sigma seeds ) -(**********************************************************************) -(* Abstraction layer *) - - -type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; - pr_subgoal : int -> evar_map -> goal list -> Pp.t; - pr_goal : goal sigma -> Pp.t; -} - -let default_printer_pr = { - pr_subgoals = default_pr_subgoals; - pr_subgoal = default_pr_subgoal; - pr_goal = default_pr_goal; -} - -let printer_pr = ref default_printer_pr - -let set_printer_pr = (:=) printer_pr - -let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x -let pr_subgoal x = !printer_pr.pr_subgoal x -let pr_goal x = !printer_pr.pr_goal x - -(* End abstraction layer *) -(**********************************************************************) - -let pr_open_subgoals ~proof = +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 @@ -830,21 +837,33 @@ let pr_open_subgoals ~proof = fnl () ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf | _ , _, _ -> - let end_cmd = - 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 () + 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 (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals + 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 - pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused + let os_map = match oproof with + | Some op when diffs -> + let (_,_,_,_, osigma) = Proof.proof 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 gls,_,_,_,sigma = Proof.proof proof in pr_subgoal n sigma gls @@ -879,7 +898,7 @@ type axiom = type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Axiom of axiom * (Label.t * Constr.rel_context * types) list | Opaque of Constant.t (* An opaque constant. *) | Transparent of Constant.t @@ -925,11 +944,18 @@ let pr_assumptionset env sigma s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> + (* FIXME? *) let mp,_,lab = Constant.repr3 kn in str (ModPath.to_string mp) ++ str "." ++ Label.print lab in - let safe_pr_ltype typ = - try str " : " ++ pr_ltype typ + 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) = @@ -940,9 +966,9 @@ let pr_assumptionset env sigma s = let pr_axiom env ax typ = match ax with | Constant kn -> - safe_pr_constant env kn ++ safe_pr_ltype typ + safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> - hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + 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 @@ -950,7 +976,7 @@ let pr_assumptionset env sigma s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = pr_id id ++ str " : " ++ pr_ltype typ in + 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 @@ -964,10 +990,10 @@ let pr_assumptionset env sigma s = l in (v, ax :: a, o, tr) | Opaque kn -> - let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in + 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 typ in + 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) = @@ -1014,6 +1040,21 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () -let pr_universe_instance evd ctx = - let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" +(* 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 index 41843680..518c5b93 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Constr open Environ open Pattern @@ -37,7 +36,7 @@ val pr_constr : constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t -val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> 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 "??" @@ -58,7 +57,7 @@ val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr : EConstr.t -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> 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 @@ -88,7 +87,7 @@ val pr_type_env : env -> evar_map -> types -> Pp.t val pr_type : types -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> 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_closed_glob : closed_glob_constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] @@ -121,7 +120,7 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t -val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t @@ -130,8 +129,8 @@ val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) -val pr_global_env : Id.Set.t -> global_reference -> Pp.t -val pr_global : global_reference -> Pp.t +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 @@ -140,9 +139,9 @@ 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 -> pconstant -> Pp.t -val pr_pinductive : env -> pinductive -> Pp.t -val pr_pconstructor : env -> pconstructor -> 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 *) @@ -153,13 +152,13 @@ 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 -> Context.Named.Declaration.t -> Pp.t -val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t -val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> 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 -> Context.Named.t -> 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 -> Context.Rel.t -> 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 @@ -172,22 +171,46 @@ val pr_transparent_state : transparent_state -> Pp.t (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) -val pr_goal : goal sigma -> Pp.t - -(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals] - prints the goals of the list [goals] followed by the goals in - [unfocused], in a short way (typically only the conclusion) except - for the first goal if [pr_first] is true. This function can be - replaced by another one by calling [set_printer_pr] (see below), - typically by plugin writers. The default printer prints only the - focused goals unless the conrresponding option - [enable_unfocused_goal_printing] is set. [seeds] is for printing - dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t +(** [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 sigma) -> 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 * Evar.t Evar.Map.t) -> Pp.t option -> evar_map + -> seeds:goal list -> shelf:goal list -> stack:int list + -> unfocused: goal list -> goals:goal list -> Pp.t val pr_subgoal : int -> evar_map -> goal list -> Pp.t -val pr_concl : int -> evar_map -> goal -> 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 sigma) -> evar_map -> 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 @@ -197,11 +220,14 @@ val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t val pr_prim_rule : prim_rule -> Pp.t +[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"] + +val print_and_diff : Proof.t option -> Proof.t option -> unit (** Backwards compatibility *) val prterm : constr -> Pp.t (** = pr_lconstr *) - +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] (** Declarations for the "Print Assumption" command *) type axiom = @@ -211,7 +237,7 @@ type axiom = type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Axiom of axiom * (Label.t * Constr.rel_context * types) list | Opaque of Constant.t (* An opaque constant. *) | Transparent of Constant.t @@ -223,14 +249,3 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t -type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; - - pr_subgoal : int -> evar_map -> goal list -> Pp.t; - pr_goal : goal sigma -> Pp.t; -} - -val set_printer_pr : printer_pr -> unit - -val default_printer_pr : printer_pr - diff --git a/printing/printing.mllib b/printing/printing.mllib index 86b68d8f..deb52ad2 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,7 +1,7 @@ Genprint Pputils Ppconstr +Proof_diffs Printer Printmod Prettyp -Ppvernac diff --git a/printing/printmod.ml b/printing/printmod.ml index e076c10f..e2d9850b 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -103,9 +103,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let envpar = push_rel_context params env in let inst = if Declareops.inductive_is_polymorphic mib then - let ctx = Declareops.inductive_polymorphic_context mib in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in - Printer.pr_universe_instance sigma ctx + Printer.pr_universe_instance sigma u else mt () in hov 0 ( @@ -140,7 +138,7 @@ let print_mutual_inductive env mind mib udecl = (AUContext.instance (Declareops.inductive_polymorphic_context mib))) else [] in - let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative @@ -183,7 +181,7 @@ let print_record env mind mib udecl = 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 = Universes.universe_binders_with_opt_names (IndRef (mind,0)) + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) (Array.to_list (Univ.Instance.to_array u)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = @@ -217,7 +215,7 @@ let print_record env mind mib udecl = ) let pr_mutual_inductive_body env mind mib udecl = - if mib.mind_record <> None && not !Flags.raw_print then + if mib.mind_record != NotRecord && not !Flags.raw_print then print_record env mind mib udecl else print_mutual_inductive env mind mib udecl @@ -323,7 +321,6 @@ let print_body is_impl env mp (l,body) = else Univ.Instance.empty in let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in - let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -332,17 +329,17 @@ let print_body is_impl env mp (l,body) = | None -> mt () | Some env -> str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env sigma + hov 0 (Printer.pr_ltype_env env (Evd.from_env env) (Vars.subst_instance_constr u cb.const_type)) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env sigma + Printer.pr_lconstr_env env (Evd.from_env env) (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx sigma ctx) + Printer.pr_universe_ctx (Evd.from_env env) ctx) | SFBmind mib -> try let env = Option.get env in @@ -387,7 +384,7 @@ let rec print_typ_expr env mp locals mty = let s = String.concat "." (List.map Id.to_string idl) in (* XXX: What should env and sigma be here? *) let env = Global.env () in - let sigma = Evd.empty in + let sigma = Evd.from_env env in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() ++ Printer.pr_lconstr_env env sigma c) diff --git a/printing/printmod.mli b/printing/printmod.mli index b0b0b0a3..48ba866c 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -15,6 +15,6 @@ val printable_body : DirPath.t -> bool val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> - Universes.univ_name_list option -> Pp.t + 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 00000000..0b630b39 --- /dev/null +++ b/printing/proof_diffs.ml @@ -0,0 +1,635 @@ +(************************************************************************) +(* * 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 e) :: acc) str + in + let st = CLexer.get_lexer_state () in + try + let istr = Stream.of_string s in + let lex = CLexer.lexer.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 + let o_entry = StringMap.find (List.hd old_ids) o_map in + o_entry.done_ <- true; + rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv; + end; + if n_line <> "" then begin + let n_entry = StringMap.find (List.hd new_ids) n_map in + n_entry.done_ <- true; + 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 () && + 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, tm) + | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm);; + +(* XXX: Very unfortunately we cannot use the Proofview interface as + Proof is still using the "legacy" one. *) +let process_goal_concl sigma g : Constr.t * Environ.env = + let env = Goal.V82.env sigma g in + let ty = Goal.V82.concl sigma g in + let ty = EConstr.to_constr sigma ty in + (ty, env) + +let process_goal sigma g : Constr.t reified_goal = + let env = Goal.V82.env sigma g in + let hyps = Goal.V82.hyps sigma g in + let ty = Goal.V82.concl sigma g in + let name = Goal.uid g in + (* There is a Constr/Econstr mess here... *) + let ty = EConstr.to_constr sigma ty in + (* compaction is usually desired [eg for better display] *) + let hyps = Termops.compact_named_context (Environ.named_context_of_val hyps) 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 EConstr.(of_constr 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 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 env sigma c in + let pb = if Constr.isCast 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 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 betwen 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 betwen 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 betwen 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; + List.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 + List.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 + List.iter2 (constr_expr ogname) ce ce2; + List.iter2 (fun a a2 -> List.iter2 (constr_expr ogname) a a2) cel cel2; + List.iter2 (fun a a2 -> List.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) -> + List.iter2 (fix_expr ogname) fl fl2 + | CCoFix (id,cfl), CCoFix (id2,cfl2) -> + List.iter2 (cofix_expr ogname) cfl cfl2 + | CProdN (bl,c2), CProdN (bl2,c22) + | CLambdaN (bl,c2), CLambdaN (bl2,c22) -> + List.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) -> + List.iter2 (constr_expr ogname) args args2 + | CApp ((isproj,f),args), CApp ((isproj2,f2),args2) -> + constr_expr ogname f f2; + List.iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in + constr_expr ogname c c2) args args2 + | CRecord fs, CRecord fs2 -> + List.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; + List.iter2 (case_expr ogname) tms tms2; + List.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; + List.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 betwen 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 betwen 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) + +[@@@ocaml.warning "-32"] +let db_goal_map op np ng_to_og = + Printf.printf "New Goals: "; + let (ngoals,_,_,_,nsigma) = Proof.proof np in + List.iter (fun ng -> Printf.printf "%d -> %s " (Evar.repr ng) (goal_to_evar ng nsigma)) ngoals; + (match op with + | Some op -> + let (ogoals,_,_,_,osigma) = Proof.proof op in + Printf.printf "\nOld Goals: "; + List.iter (fun og -> Printf.printf "%d -> %s " (Evar.repr og) (goal_to_evar og osigma)) ogoals + | None -> ()); + Printf.printf "\nGoal map: "; + GoalMap.iter (fun og ng -> Printf.printf "%d -> %d " (Evar.repr og) (Evar.repr ng)) ng_to_og; + Printf.printf "\n" +[@@@ocaml.warning "+32"] + +(* Create a map from new goals to old goals for proof diff. The map only + has entries for new goals that are not the same as the corresponding old + goal; there are no entries for unchanged goals. + + 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 for the differing goals. +*) +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 + + 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 (_,_,_,_,osigma) = Proof.proof 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); + + try + let (_,_,_,_,nsigma) = Proof.proof 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 -> ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og) add_gs; + !ng_to_og + with Not_found -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (6)") + 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 00000000..832393e1 --- /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 Proof_type +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 sigma option -> 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 sigma) -> 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 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 -> Evar.t 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 |