diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/genprint.ml | 13 | ||||
| -rw-r--r-- | printing/genprint.mli | 2 | ||||
| -rw-r--r-- | printing/miscprint.ml | 6 | ||||
| -rw-r--r-- | printing/miscprint.mli | 2 | ||||
| -rw-r--r-- | printing/ppannotation.ml | 2 | ||||
| -rw-r--r-- | printing/ppannotation.mli | 2 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 56 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 2 | ||||
| -rw-r--r-- | printing/ppconstrsig.mli | 2 | ||||
| -rw-r--r-- | printing/pptactic.ml | 441 | ||||
| -rw-r--r-- | printing/pptactic.mli | 10 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 63 | ||||
| -rw-r--r-- | printing/pputils.ml | 2 | ||||
| -rw-r--r-- | printing/pputils.mli | 2 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 133 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 2 | ||||
| -rw-r--r-- | printing/ppvernacsig.mli | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 77 | ||||
| -rw-r--r-- | printing/prettyp.mli | 4 | ||||
| -rw-r--r-- | printing/printer.ml | 86 | ||||
| -rw-r--r-- | printing/printer.mli | 21 | ||||
| -rw-r--r-- | printing/printmod.ml | 66 | ||||
| -rw-r--r-- | printing/printmod.mli | 2 | ||||
| -rw-r--r-- | printing/printmodsig.mli | 2 | ||||
| -rw-r--r-- | printing/richprinter.mli | 2 |
25 files changed, 468 insertions, 534 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml index ade69ef831..0ec35e07be 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,8 +19,9 @@ module PrintObj = struct type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer let name = "printer" - let default wit = match unquote (rawwit wit) with - | ExtraArgType name -> + let default wit = match wit with + | ExtraArg tag -> + let name = ArgT.repr tag in let printer = { raw = (fun _ -> str "<genarg:" ++ str name ++ str ">"); glb = (fun _ -> str "<genarg:" ++ str name ++ str ">"); @@ -40,6 +41,6 @@ let raw_print wit v = (Print.obj wit).raw v let glb_print wit v = (Print.obj wit).glb v let top_print wit v = (Print.obj wit).top v -let generic_raw_print v = unpack { unpacker = fun w v -> raw_print w (raw v); } v -let generic_glb_print v = unpack { unpacker = fun w v -> glb_print w (glb v); } v -let generic_top_print v = unpack { unpacker = fun w v -> top_print w (top v); } v +let generic_raw_print (GenArg (Rawwit w, v)) = raw_print w v +let generic_glb_print (GenArg (Glbwit w, v)) = glb_print w v +let generic_top_print (GenArg (Topwit w, v)) = top_print w v diff --git a/printing/genprint.mli b/printing/genprint.mli index 5b91d6d216..6e6626f2f6 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/miscprint.ml b/printing/miscprint.ml index d09af6d2ac..5e86c6bd76 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -33,9 +33,9 @@ and pr_intro_pattern_action prc = function | IntroRewrite false -> str "<-" and pr_or_and_intro_pattern prc = function - | [pl] -> + | IntroAndPattern pl -> str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")" - | pll -> + | IntroOrPattern pll -> str "[" ++ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) ++ str "]" diff --git a/printing/miscprint.mli b/printing/miscprint.mli index 1d915ef8c5..fe8c779ff4 100644 --- a/printing/miscprint.mli +++ b/printing/miscprint.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml index 4f26b82424..df7f925b73 100644 --- a/printing/ppannotation.ml +++ b/printing/ppannotation.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli index bc345c347b..84724053ed 100644 --- a/printing/ppannotation.mli +++ b/printing/ppannotation.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 650b8f7262..1866ca5042 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -136,12 +136,10 @@ end) = struct let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) - let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" - let pr_univ l = match l with - | [x] -> str x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")" + | [_,x] -> str x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")" let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" @@ -153,11 +151,11 @@ end) = struct let pr_qualid sp = let (sl, id) = repr_qualid sp in - let id = tag_ref (str (Id.to_string id)) in + let id = tag_ref (pr_id id) in let sl = match List.rev (DirPath.repr sl) with | [] -> mt () | sl -> - let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in + let pr dir = tag_path (pr_id dir) ++ str "." in prlist pr sl in sl ++ id @@ -174,7 +172,7 @@ end) = struct tag_type (str "Set") | GType u -> (match u with - | Some u -> str u + | Some (_,u) -> str u | None -> tag_type (str "Type")) let pr_universe_instance l = @@ -182,7 +180,7 @@ end) = struct let pr_reference = function | Qualid (_, qid) -> pr_qualid qid - | Ident (_, id) -> tag_var (str (Id.to_string id)) + | Ident (_, id) -> tag_var (pr_id id) let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -246,16 +244,16 @@ end) = struct | CPatAlias (_, p, id) -> pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las - | CPatCstr (_,c, [], []) -> + | CPatCstr (_,c, None, []) -> pr_reference c, latom - | CPatCstr (_, c, [], args) -> + | CPatCstr (_, c, None, args) -> pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatCstr (_, c, args, []) -> + | CPatCstr (_, c, Some args, []) -> str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatCstr (_, c, expl_args, extra_args) -> + | CPatCstr (_, c, Some expl_args, extra_args) -> surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args) ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp @@ -457,7 +455,7 @@ end) = struct (pr_decl true) dl ++ fnl() ++ keyword "for" ++ spc () ++ pr_id id - let pr_asin pr (na,indnalopt) = + let pr_asin pr na indnalopt = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) | Some na -> spc () ++ keyword "as" ++ spc () ++ pr_lname na | None -> mt ()) ++ @@ -465,8 +463,8 @@ end) = struct | None -> mt () | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t) - let pr_case_item pr (tm,asin) = - hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) + let pr_case_item pr (tm,as_clause, in_clause) = + hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause) let pr_case_type pr po = match po with @@ -595,28 +593,20 @@ end) = struct return (p, lproj) | CApp (_,(None,a),l) -> return (pr_app (pr mt) a l, lapp) - | CRecord (_,w,l) -> - let beg = - match w with - | None -> - spc () - | Some t -> - spc () ++ pr spc ltop t ++ spc () - ++ keyword "with" ++ spc () - in + | CRecord (_,l) -> return ( - hv 0 (str"{|" ++ beg ++ + hv 0 (str"{|" ++ spc () ++ prlist_with_sep pr_semicolon (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l ++ str" |}"), latom ) - | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) -> + | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ hov 0 (pr_patt ltop p ++ - pr_asin (pr_dangling_with_for mt pr) asin ++ + pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++ str " :=" ++ pr spc ltop c ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++ spc () ++ keyword "in" ++ pr spc ltop b)), @@ -638,13 +628,13 @@ end) = struct | CLetTuple (_,nal,(na,po),c,b) -> return ( hv 0 ( - keyword "let" ++ spc () ++ - hov 0 (str "(" ++ + hov 2 (keyword "let" ++ spc () ++ + hov 1 (str "(" ++ prlist_with_sep sep_v pr_lname nal ++ str ")" ++ - pr_simple_return_type (pr mt) na po ++ str " :=" ++ - pr spc ltop c ++ spc () - ++ keyword "in") ++ + pr_simple_return_type (pr mt) na po ++ str " :=") ++ + pr spc ltop c + ++ keyword " in") ++ pr spc ltop b), lletin ) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 6e8d3b04c4..0241633c61 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli index b7eb9b1fff..c711dd8f7f 100644 --- a/printing/ppconstrsig.mli +++ b/printing/ppconstrsig.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index e8ccd29c8a..982c18ec61 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,11 +26,11 @@ open Printer let pr_global x = Nametab.pr_global_env Id.Set.empty x -type grammar_terminals = string option list +type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list type pp_tactic = { - pptac_args : argument_type list; - pptac_prods : int * grammar_terminals; + pptac_level : int; + pptac_prods : grammar_terminals; } (* ML Extensions *) @@ -61,14 +61,14 @@ type 'a glob_extra_genarg_printer = type 'a extra_genarg_printer = (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds let genarg_pprule = ref String.Map.empty let declare_extra_genarg_pprule wit f g h = - let s = match unquote (topwit wit) with - | ExtraArgType s -> s + let s = match wit with + | ExtraArg s -> ArgT.repr s | _ -> error "Can declare a pretty-printing rule only for extra argument types." in @@ -106,6 +106,8 @@ module Make let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) + let pr_value _ _ = str "(* FIXME *)" + let pr_with_occurrences pr (occs,c) = match occs with | AllOccurrences -> @@ -265,149 +267,89 @@ module Make let with_evars ev s = if ev then "e" ^ s else s - let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) - | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) - | ConstrMayEvalArgType -> - pr_may_eval prc prlc (pr_or_by_notation prref) prpat - (out_gen (rawwit wit_constr_may_eval) x) - | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat) - (out_gen (rawwit wit_red_expr) x) - | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x) - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - pr_sequence map (raw l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match raw o with + let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () - | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) + | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = raw o in - let p = in_gen (rawwit wit1) p in - let q = in_gen (rawwit wit2) q in - pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q] - in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_raw_print x - - - let rec pr_glb_generic prc prlc prtac prpat x = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) - | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) - | ConstrMayEvalArgType -> - pr_may_eval prc prlc - (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat - (out_gen (glbwit wit_constr_may_eval) x) - | QuantHypArgType -> - pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr - (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat) - (out_gen (glbwit wit_red_expr) x) - | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x) - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in - pr_sequence map (glb l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match glb o with + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (rawwit wit1) p in + let q = in_gen (rawwit wit2) q in + hov 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q]) + | ExtraArg s -> + try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x) + with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x) + + + let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () - | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) - in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = glb o in - let p = in_gen (glbwit wit1) p in - let q = in_gen (glbwit wit2) q in - pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q] + | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_glb_print x - - let rec pr_top_generic prc prlc prtac prpat x = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (topwit wit_ident) x) - | VarArgType -> pr_id (out_gen (topwit wit_var) x) - | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (topwit wit_constr) x) - | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x) - | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr (prc,prlc,pr_evaluable_reference,prpat) - (out_gen (topwit wit_red_expr) x) - | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in - pr_with_bindings prc prlc (c,b) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in - pr_sequence map (top l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match top o with + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (glbwit wit1) p in + let q = in_gen (glbwit wit2) q in + let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in + hov 0 ans + | ExtraArg s -> + try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x) + with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x) + + let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () - | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) - in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = top o in - let p = in_gen (topwit wit1) p in - let q = in_gen (topwit wit2) q in - pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q] + | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_top_print x + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (topwit wit1) p in + let q = in_gen (topwit wit2) q in + let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in + hov 0 ans + | ExtraArg s -> + try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x) + with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x) let rec tacarg_using_rule_token pr_gen = function - | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) - | None :: l, a :: al -> + | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) + | Egramml.GramNonTerminal _ :: l, a :: al -> let r = tacarg_using_rule_token pr_gen (l,al) in pr_gen a :: r | [], [] -> [] | _ -> failwith "Inconsistent arguments of extended tactic" + type any_arg = AnyArg : 'a Genarg.raw_abstract_argument_type -> any_arg + + let filter_arg = function + | Egramml.GramTerminal _ -> None + | Egramml.GramNonTerminal (_, t, _) -> Some (AnyArg t) + let pr_tacarg_using_rule pr_gen l = let l = match l with - | (Some s :: l, al) -> + | (Egramml.GramTerminal s :: l, al) -> (** First terminal token should be considered as the name of the tactic, so we tag it differently than the other terminal tokens. *) primitive s :: (tacarg_using_rule_token pr_gen (l, al)) @@ -415,13 +357,14 @@ module Make in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = + let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l = try let pp_rules = Hashtbl.find prtac_tab s in let pp = pp_rules.(i) in - let (lev', pl) = pp.pptac_prods in - let p = pr_tacarg_using_rule pr_gen (pl,l) in - if lev' > lev then surround p else p + let args = List.map_filter filter_arg pp.pptac_prods in + let () = if not (List.for_all2eq check args l) then raise Not_found in + let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + if pp.pptac_level > lev then surround p else p with Not_found -> let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ @@ -433,28 +376,35 @@ module Make in str "<" ++ name ++ str ">" ++ args - let pr_alias_gen pr_gen lev key l = + let pr_alias_gen check pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in - let (lev', pl) = pp.pptac_prods in - let p = pr_tacarg_using_rule pr_gen (pl, l) in - if lev' > lev then surround p else p + let args = List.map_filter filter_arg pp.pptac_prods in + let () = if not (List.for_all2eq check args l) then raise Not_found in + let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + if pp.pptac_level > lev then surround p else p with Not_found -> KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" - let pr_raw_extend prc prlc prtac prpat = - pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference) - let pr_glob_extend prc prlc prtac prpat = - pr_extend_gen (pr_glb_generic prc prlc prtac prpat) - let pr_extend prc prlc prtac prpat = - pr_extend_gen (pr_top_generic prc prlc prtac prpat) + let check_type t arg = match t, arg with + | AnyArg t, TacGeneric arg -> argument_type_eq (unquote t) (genarg_tag arg) + | _ -> false + + let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false + + let pr_raw_extend_rec prc prlc prtac prpat = + pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) + let pr_glob_extend_rec prc prlc prtac prpat = + pr_extend_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) + let pr_extend_rec prc prlc prtac prpat = + pr_extend_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) let pr_raw_alias prc prlc prtac prpat = - pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference) + pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) let pr_glob_alias prc prlc prtac prpat = - pr_alias_gen (pr_glb_generic prc prlc prtac prpat) + pr_alias_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) let pr_alias prc prlc prtac prpat = - pr_alias_gen (pr_top_generic prc prlc prtac prpat) + pr_alias_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) (**********************************************************************) (* The tactic printer *) @@ -586,8 +536,7 @@ module Make let pr_in_hyp_as prc pr_id = function | None -> mt () - | Some (clear,id,ipat) -> - pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat + | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat let pr_clauses default_is_concl pr_id = function | { onhyps=Some []; concl_occs=occs } @@ -722,11 +671,6 @@ module Make | l -> spc () ++ hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l) - let string_of_debug = function - | Off -> "" - | Debug -> "debug " - | Info -> "info_" - let pr_then () = str ";" let ltop = (5,E) @@ -752,7 +696,6 @@ module Make type 'a printer = { pr_tactic : tolerability -> 'tacexpr -> std_ppcmds; pr_constr : 'trm -> std_ppcmds; - pr_uconstr : 'utrm -> std_ppcmds; pr_lconstr : 'trm -> std_ppcmds; pr_dconstr : 'dtrm -> std_ppcmds; pr_pattern : 'pat -> std_ppcmds; @@ -761,13 +704,12 @@ module Make pr_reference : 'ref -> std_ppcmds; pr_name : 'nam -> std_ppcmds; pr_generic : 'lev generic_argument -> std_ppcmds; - pr_extend : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds; - pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds; + pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds; + pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds; } constraint 'a = < term :'trm; - utrm :'utrm; dterm :'dtrm; pattern :'pat; constant :'cst; @@ -781,7 +723,6 @@ module Make (* some shortcuts *) let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in - let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in let pr_with_bindings_arg_full = pr_with_bindings_arg in let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in @@ -849,9 +790,6 @@ module Make let rec pr_atom0 a = tag_atom a (match a with | TacIntroPattern [] -> primitive "intros" | TacIntroMove (None,MoveLast) -> primitive "intro" - | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial" - | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto" - | TacClear (true,[]) -> primitive "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" ) @@ -886,13 +824,10 @@ module Make ++ pr_opt pr_eliminator cbo) | TacCase (ev,cb) -> hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb) - | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> hov 1 ( primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l) - | TacCofix ido -> - hov 1 (primitive "cofix" ++ pr_opt pr_id ido) | TacMutualCofix (id,l) -> hov 1 ( primitive "cofix" ++ spc () ++ pr_id id ++ spc() @@ -916,11 +851,6 @@ module Make pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacGeneralizeDep c -> - hov 1 ( - primitive "generalize" ++ spc () ++ str "dependent" - ++ pr_constrarg c - ) | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) | TacLetTac (na,c,cl,b,e) -> @@ -959,43 +889,7 @@ module Make ++ pr_arg pr_quantified_hypothesis h2 ) - (* Automation tactics *) - | TacTrivial (_,[],Some []) as x -> - pr_atom0 x - | TacTrivial (d,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "trivial" - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - | TacAuto (_,None,[],Some []) as x -> - pr_atom0 x - | TacAuto (d,n,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "auto" - ++ pr_opt (pr_or_var int) n - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - (* Context management *) - | TacClear (true,[]) as t -> - pr_atom0 t - | TacClear (keep,l) -> - hov 1 ( - primitive "clear" ++ spc () - ++ (if keep then str "- " else mt ()) - ++ prlist_with_sep spc pr.pr_name l - ) - | TacClearBody l -> - hov 1 ( - primitive "clearbody" ++ spc () - ++ prlist_with_sep spc pr.pr_name l - ) - | TacMove (id1,id2) -> - hov 1 ( - primitive "move" - ++ brk (1,1) ++ pr.pr_name id1 - ++ Miscprint.pr_move_location pr.pr_name id2 - ) | TacRename l -> hov 1 ( primitive "rename" ++ brk (1,1) @@ -1006,13 +900,6 @@ module Make l ) - (* Constructors *) - | TacSplit (ev,l) -> - hov 1 ( - primitive (with_evars ev "exists") - ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l - ) - (* Conversion *) | TacReduce (r,h) -> hov 1 ( @@ -1032,10 +919,6 @@ module Make ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h ) - (* Equivalence relations *) - | TacSymmetry cls -> - primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> hov 1 ( @@ -1257,26 +1140,17 @@ module Make | TacML (loc,s,l) -> pr_with_comments loc (pr.pr_extend 1 s l), lcall | TacAlias (loc,kn,l) -> - pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom + pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom ) in if prec_less prec inherited then strm else str"(" ++ strm ++ str")" and pr_tacarg = function - | TacDynamic (loc,t) -> - pr_with_comments loc - (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>") - | MetaIdArg (loc,true,s) -> - pr_with_comments loc (str "$" ++ str s) - | MetaIdArg (loc,false,s) -> - pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s) | Reference r -> pr.pr_reference r | ConstrMayEval c -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c - | UConstr c -> - keyword "uconstr:" ++ pr.pr_uconstr c | TacFreshId l -> keyword "fresh" ++ pr_fresh_ids l | TacPretype c -> @@ -1304,7 +1178,6 @@ module Make let pr = { pr_tactic = pr_raw_tactic_level; pr_constr = pr_constr_expr; - pr_uconstr = pr_constr_expr; pr_dconstr = pr_constr_expr; pr_lconstr = pr_lconstr_expr; pr_pattern = pr_constr_pattern_expr; @@ -1313,7 +1186,7 @@ module Make pr_reference = pr_reference; pr_name = pr_lident; pr_generic = Genprint.generic_raw_print; - pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; + pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; } in make_pr_tac @@ -1327,7 +1200,7 @@ module Make let pr_pat_and_constr_expr pr ((c,_),_) = pr c - let rec pr_glob_tactic_level env n t = + let pr_glob_tactic_level env n t = let glob_printers = (strip_prod_binders_glob_constr) in @@ -1335,7 +1208,6 @@ module Make let pr = { pr_tactic = prtac; pr_constr = pr_and_constr_expr (pr_glob_constr_env env); - pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env); pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); @@ -1344,7 +1216,7 @@ module Make pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; pr_generic = Genprint.generic_glb_print; - pr_extend = pr_glob_extend + pr_extend = pr_glob_extend_rec (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); pr_alias = pr_glob_alias @@ -1377,7 +1249,6 @@ module Make let pr = { pr_tactic = pr_glob_tactic_level env; pr_constr = pr_constr_env env Evd.empty; - pr_uconstr = pr_closed_glob_env env Evd.empty; pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_lconstr_env env Evd.empty; pr_pattern = pr_constr_pattern_env env Evd.empty; @@ -1386,12 +1257,12 @@ module Make pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; pr_generic = Genprint.generic_top_print; - pr_extend = pr_extend + pr_extend = pr_extend_rec (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern; + pr_value pr_constr_pattern; pr_alias = pr_alias (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern; + pr_value pr_constr_pattern; } in make_pr_tac @@ -1401,6 +1272,39 @@ module Make in prtac n t + let pr_raw_generic env = pr_raw_generic_rec + pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference + + let pr_glb_generic env = pr_glb_generic_rec + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + + let pr_top_generic env = pr_top_generic_rec + (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) + pr_value pr_constr_pattern + + let pr_raw_extend env = pr_raw_extend_rec + pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr + + let pr_glob_extend env = pr_glob_extend_rec + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + + let check_val_type t arg = + let AnyArg t = t in +(* let t = Genarg.val_tag (Obj.magic t) in *) +(* let Val.Dyn (t', _) = arg in *) +(* match Genarg.Val.eq t t' with *) +(* | None -> false *) +(* | Some _ -> true *) + true (** FIXME *) + + let pr_alias pr lev key args = + pr_alias_gen check_val_type pr lev key args + + let pr_extend pr lev ml args = + pr_extend_gen check_val_type pr lev ml args + let pr_tactic env = pr_tactic_level env ltop end @@ -1437,17 +1341,26 @@ end) (** Registering *) +let run_delayed c = + Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma } + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in let pr_string s = str "\"" ++ str s ++ str "\"" in + Genprint.register_print0 Constrarg.wit_int_or_var + (pr_or_var int) (pr_or_var int) int; Genprint.register_print0 Constrarg.wit_ref pr_reference (pr_or_var (pr_located pr_global)) pr_global; + Genprint.register_print0 Constrarg.wit_ident + pr_id pr_id pr_id; + Genprint.register_print0 Constrarg.wit_var + (pr_located pr_id) (pr_located pr_id) pr_id; Genprint.register_print0 Constrarg.wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty)))); + (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c)))); Genprint.register_print0 Constrarg.wit_clause_dft_concl (pr_clauses (Some true) pr_lident) @@ -1457,11 +1370,41 @@ let () = Genprint.register_print0 Constrarg.wit_sort pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 + Constrarg.wit_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; + Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr (fun (c,_) -> Printer.pr_glob_constr c) Printer.pr_closed_glob ; + Genprint.register_print0 + Constrarg.wit_open_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; + Genprint.register_print0 Constrarg.wit_red_expr + (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) + (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern)); + Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + Genprint.register_print0 Constrarg.wit_bindings + (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) + (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it))); + Genprint.register_print0 Constrarg.wit_constr_may_eval + (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr) + (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr) + (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr)) + pr_constr; + Genprint.register_print0 Constrarg.wit_constr_with_bindings + (pr_with_bindings pr_constr_expr pr_lconstr_expr) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it))); Genprint.register_print0 Stdarg.wit_int int int int; Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; @@ -1472,16 +1415,10 @@ let () = let printer _ _ prtac = prtac (0, E) in declare_extra_genarg_pprule wit_tactic printer printer printer -let _ = Hook.set Tactic_debug.tactic_printer - (fun x -> pr_glob_tactic (Global.env()) x) - -let _ = Hook.set Tactic_debug.match_pattern_printer - (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp) - -let _ = Hook.set Tactic_debug.match_rule_printer - (fun rl -> - pr_match_rule false (pr_glob_tactic (Global.env())) - (fun (_,p) -> pr_constr_pattern p) rl) +let () = + let pr_unit _ _ _ () = str "()" in + let printer _ _ prtac = prtac (0, E) in + declare_extra_genarg_pprule wit_ltac printer printer pr_unit module Richpp = struct diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 30b9483db7..31a5a5d4a8 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,7 +32,7 @@ type 'a glob_extra_genarg_printer = type 'a extra_genarg_printer = (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds val declare_extra_genarg_pprule : @@ -41,11 +41,11 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit -type grammar_terminals = string option list +type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list type pp_tactic = { - pptac_args : argument_type list; - pptac_prods : int * grammar_terminals; + pptac_level : int; + pptac_prods : grammar_terminals; } val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 1631bda377..b98b6c67e7 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,11 +8,9 @@ open Pp open Genarg -open Constrexpr open Tacexpr open Ppextend open Environ -open Pattern open Misctypes module type Pp = sig @@ -32,46 +30,24 @@ module type Pp = sig val pr_clauses : bool option -> ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds - val pr_raw_generic : - (constr_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - (tolerability -> raw_tactic_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - (Libnames.reference -> std_ppcmds) -> rlevel generic_argument -> - std_ppcmds - - val pr_glb_generic : - (glob_constr_and_expr -> Pp.std_ppcmds) -> - (glob_constr_and_expr -> Pp.std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (glob_constr_pattern_and_expr -> std_ppcmds) -> - glevel generic_argument -> std_ppcmds - - val pr_top_generic : - (Term.constr -> std_ppcmds) -> - (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (Pattern.constr_pattern -> std_ppcmds) -> - tlevel generic_argument -> - std_ppcmds - - val pr_raw_extend: - (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> - (tolerability -> raw_tactic_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> int -> - ml_tactic_entry -> raw_generic_argument list -> std_ppcmds - - val pr_glob_extend: - (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (glob_constr_pattern_and_expr -> std_ppcmds) -> int -> - ml_tactic_entry -> glob_generic_argument list -> std_ppcmds + + val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds + + val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds + + val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds + + val pr_raw_extend: env -> int -> + ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds + + val pr_glob_extend: env -> int -> + ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds val pr_extend : - (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (constr_pattern -> std_ppcmds) -> int -> - ml_tactic_entry -> typed_generic_argument list -> std_ppcmds + (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + + val pr_alias : (Val.t -> std_ppcmds) -> + int -> Names.KerName.t -> Val.t list -> std_ppcmds val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds @@ -91,4 +67,9 @@ module type Pp = sig ('constr -> std_ppcmds) -> ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds + val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds + + val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('b, 'a) match_rule -> std_ppcmds + end diff --git a/printing/pputils.ml b/printing/pputils.ml index ee1a39efd3..906b463a85 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/pputils.mli b/printing/pputils.mli index 7287748327..a0f2c77283 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4e889e55f0..c1f5e122bd 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -43,6 +43,12 @@ module Make else pr_id id + let pr_plident (lid, l) = + pr_lident lid ++ + (match l with + | Some l -> prlist_with_sep spc pr_lident l + | None -> mt()) + let string_of_fqid fqid = String.concat "." (List.map Id.to_string fqid) @@ -73,13 +79,7 @@ module Make | VernacEndSubproof -> str"" | _ -> str"." - let pr_gen t = - pr_raw_generic - pr_constr_expr - pr_lconstr_expr - pr_raw_tactic_level - pr_constr_expr - pr_reference t + let pr_gen t = pr_raw_generic (Global.env ()) t let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() @@ -105,10 +105,9 @@ module Make else id let pr_production_item = function - | TacNonTerm (loc,nt,Some (p,sep)) -> + | TacNonTerm (loc, nt, (p, sep)) -> let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")" - | TacNonTerm (loc,nt,None) -> str nt | TacTerm s -> qs s let pr_comment pr_c = function @@ -160,6 +159,8 @@ module Make (* 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 @@ -348,6 +349,7 @@ module Make | 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) *) @@ -376,21 +378,16 @@ module Make | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - let print_level n = - if not (Int.equal n 0) then - spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")") - else - mt () - - let pr_grammar_tactic_rule n (_,pil,t) = - hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++ - hov 0 (prlist_with_sep sep pr_production_item pil ++ - spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) + let pr_univs pl = + match pl with + | None -> mt () + | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}" - let pr_statement head (id,(bl,c,guard)) = - assert (not (Option.is_empty id)); + let pr_statement head (idpl,(bl,c,guard)) = + assert (not (Option.is_empty idpl)); + let id, pl = Option.get idpl in hov 2 - (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++ + (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ str":" ++ pr_spc_lconstr c) @@ -458,8 +455,6 @@ module Make keyword "Print TypeClasses" | PrintInstances qid -> keyword "Print Instances" ++ spc () ++ pr_smart_global qid - | PrintLtac qid -> - keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid | PrintCoercions -> keyword "Print Coercions" | PrintCoercionPaths (s,t) -> @@ -478,8 +473,6 @@ module Make keyword "Print Hint *" | PrintHintDbName s -> keyword "Print HintDb" ++ spc () ++ str s - | PrintRewriteHintDbName s -> - keyword "Print Rewrite HintDb" ++ spc() ++ str s | PrintUniverses (b, fopt) -> let cmd = if b then "Print Sorted Universes" @@ -579,7 +572,8 @@ module Make let pr_goal_reference = function | OpenSubgoals -> mt () | NthGoal n -> spc () ++ int n - | GoalId n -> spc () ++ str n in + | GoalId id -> spc () ++ pr_id id + | GoalUid n -> spc () ++ str n in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n @@ -625,10 +619,10 @@ module Make else spc() ++ qs s ) - | VernacTime v -> - return (keyword "Time" ++ spc() ++ pr_vernac_list v) - | VernacRedirect (s, v) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v) + | VernacTime (_,v) -> + return (keyword "Time" ++ spc() ++ pr_vernac v) + | VernacRedirect (s, (_,v)) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v) | VernacFail v -> @@ -637,8 +631,6 @@ module Make return (keyword "No-parsing-rule for VernacError") (* Syntax *) - | VernacTacticNotation (n,r,e) -> - return (pr_grammar_tactic_rule n ("",r,e)) | VernacOpenCloseScope (_,(opening,sc)) -> return ( keyword (if opening then "Open " else "Close ") ++ @@ -729,7 +721,7 @@ module Make return ( hov 2 ( pr_def_token d ++ spc() - ++ pr_lident id ++ binds ++ typ + ++ pr_plident id ++ binds ++ typ ++ (match c with | None -> mt() | Some cc -> str" :=" ++ spc() ++ cc)) @@ -760,11 +752,12 @@ module Make return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) | VernacAssumption (stre,_,l) -> let n = List.length (List.flatten (List.map fst (List.map snd l))) in - return ( - hov 2 - (pr_assumption_token (n > 1) stre ++ spc() ++ - pr_ne_params_list pr_lconstr_expr l) - ) + let pr_params (c, (xl, t)) = + hov 2 (prlist_with_sep sep pr_plident 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) stre ++ spc() ++ assumptions)) | VernacInductive (p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ @@ -781,10 +774,10 @@ module Make | RecordDecl (c,fs) -> pr_record_decl b c fs in - let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) = + let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) = hov 0 ( str key ++ spc() ++ - (if coe then str"> " else str"") ++ pr_lident id ++ + (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++ pr_and_type_binders_arg indpar ++ spc() ++ Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ str" :=") ++ pr_constructor_list k lc ++ @@ -808,9 +801,9 @@ module Make | None | Some Global -> "" in let pr_onerec = function - | ((loc,id),ro,bl,type_,def),ntn -> + | (((loc,id),pl),ro,bl,type_,def),ntn -> let annot = pr_guard_annot pr_lconstr_expr bl ro in - pr_id id ++ pr_binders_arg bl ++ annot + pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn @@ -826,8 +819,8 @@ module Make | Some Local -> keyword "Local" ++ spc () | None | Some Global -> str "" in - let pr_onecorec (((loc,id),bl,c,def),ntn) = - pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ + let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) = + pr_id id ++ pr_univs pl ++ 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 @@ -908,8 +901,9 @@ module Make hov 1 ( (if abst then keyword "Declare" ++ spc () else mt ()) ++ keyword "Instance" ++ - (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | - Anonymous -> mt ()) ++ + (match instid with + | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc () + | (_, Anonymous), _ -> mt ()) ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ pr_constr cl ++ pr_priority pri ++ @@ -970,24 +964,6 @@ module Make prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) ) (* Solving *) - | VernacSolve (i,info,tac,deftac) -> - let pr_goal_selector = function - | SelectNth i -> int i ++ str":" - | SelectId id -> pr_id id ++ str":" - | SelectAll -> str"all" ++ str":" - | SelectAllParallel -> str"par" - in - let pr_info = - match info with - | None -> mt () - | Some i -> str"Info"++spc()++int i++spc() - in - return ( - (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++ - pr_info ++ - pr_raw_tactic tac - ++ (if deftac then str ".." else mt ()) - ) | VernacSolveExistential (i,c) -> return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) @@ -1019,24 +995,6 @@ module Make return (keyword "Cd" ++ pr_opt qs s) (* Commands *) - | VernacDeclareTacticDefinition (rc,l) -> - let pr_tac_body (id, redef, body) = - let idl, body = - match body with - | Tacexpr.TacFun (idl,b) -> idl,b - | _ -> [], body in - pr_ltac_ref id ++ - prlist (function None -> str " _" - | Some id -> spc () ++ pr_id id) idl - ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ - pr_raw_tactic body - in - return ( - hov 1 - (keyword "Ltac" ++ spc () ++ - prlist_with_sep (fun () -> - fnl() ++ keyword "with" ++ spc ()) pr_tac_body l) - ) | VernacCreateHintDb (dbname,b) -> return ( hov 1 (keyword "Create HintDb" ++ spc () ++ @@ -1213,8 +1171,6 @@ module Make (keyword "Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) ) - | VernacNop -> - mt() (* Toplevel control *) | VernacToplevelControl exn -> @@ -1251,11 +1207,6 @@ module Make | VernacEndSubproof -> return (str "}") - and pr_vernac_list l = - hov 2 (str"[" ++ spc() ++ - prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l - ++ spc() ++ str"]") - and pr_extend s cl = let pr_arg a = try pr_gen a diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index f38848cdcf..d3d4a5ceb7 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli index cfcd49744e..5d1c89332c 100644 --- a/printing/ppvernacsig.mli +++ b/printing/ppvernacsig.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b8c5fd4cfc..9745a79250 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -35,7 +35,7 @@ type object_pr = { print_syntactic_def : kernel_name -> std_ppcmds; print_module : bool -> Names.module_path -> std_ppcmds; print_modtype : module_path -> std_ppcmds; - print_named_decl : Id.t * constr option * types -> std_ppcmds; + print_named_decl : Context.Named.Declaration.t -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; @@ -73,8 +73,15 @@ let print_ref reduce ref = in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in - hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ - Printer.pr_universe_ctx univs) + let env = Global.env () in + let bl = Universes.universe_binders_of_global ref in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let inst = + if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs + else mt () + in + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ + Printer.pr_universe_ctx sigma univs) (********************************) (** Printing implicit arguments *) @@ -125,7 +132,8 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in - let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in + let open Context.Rel.Declaration in + let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in List.exists is_status_implicit lastimpl @@ -161,8 +169,10 @@ type opacity = | FullyOpaque | TransparentMaybeOpacified of Conv_oracle.level -let opacity env = function - | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) -> +let opacity env = + let open Context.Named.Declaration in + function + | VarRef v when is_local_def (Environ.lookup_named v env) -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) | ConstRef cst -> @@ -208,8 +218,8 @@ let print_polymorphism ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite -> mt () - | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion" + | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt () + | Decl_kinds.BiFinite -> str " and has eta conversion" in [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] | _ -> [] @@ -433,11 +443,13 @@ let print_named_def name body typ = let print_named_assum name typ = str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" -let gallina_print_named_decl (id,c,typ) = - let s = Id.to_string id in - match c with - | Some body -> print_named_def s body typ - | None -> print_named_assum s typ +let gallina_print_named_decl = + let open Context.Named.Declaration in + function + | LocalAssum (id, typ) -> + print_named_assum (Id.to_string id) typ + | LocalDef (id, body, typ) -> + print_named_def (Id.to_string id) body typ let assumptions_for_print lna = List.fold_right (fun na env -> add_name na env) lna empty_names_context @@ -463,16 +475,21 @@ let gallina_print_section_variable id = print_named_decl id ++ with_line_skip (print_name_infos (VarRef id)) -let print_body = function - | Some c -> pr_lconstr c +let print_body env evd = function + | Some c -> pr_lconstr_env env evd c | None -> (str"<no body>") -let print_typed_body (val_0,typ) = - (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ) +let print_typed_body env evd (val_0,typ) = + (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) let ungeneralized_type_of_constant_type t = Typeops.type_of_constant_type (Global.env ()) t +let print_instance sigma cb = + if cb.const_polymorphic then + pr_universe_instance sigma cb.const_universes + else mt() + let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in @@ -481,17 +498,23 @@ let print_constant with_values sep sp = let univs = Univ.instantiate_univ_context (Global.universes_of_constant_body cb) in + let ctx = + Evd.evar_universe_context_of_binders + (Universes.universe_binders_of_global (ConstRef sp)) + in + let env = Global.env () and sigma = Evd.from_ctx ctx in + let pr_ltype = pr_ltype_env env sigma in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> str"*** [ " ++ - print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ + print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_universe_ctx univs + Printer.pr_universe_ctx sigma univs | _ -> - print_basename sp ++ str sep ++ cut () ++ - (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ - Printer.pr_universe_ctx univs) + print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ + (if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++ + Printer.pr_universe_ctx sigma univs) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ @@ -703,8 +726,8 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - let (_,c,typ) = Global.lookup_named str in - (print_named_decl (str,c,typ)) + let open Context.Named.Declaration in + str |> Global.lookup_named |> set_id str |> print_named_decl with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") @@ -732,8 +755,8 @@ let print_opaque_name qid = let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let (_,c,ty) = lookup_named id env in - print_named_decl (id,c,ty) + let open Context.Named.Declaration in + lookup_named id env |> set_id id |> print_named_decl let print_about_any loc k = match k with diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 6216d4d531..0eab155796 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -66,7 +66,7 @@ type object_pr = { print_syntactic_def : kernel_name -> std_ppcmds; print_module : bool -> Names.module_path -> std_ppcmds; print_modtype : module_path -> std_ppcmds; - print_named_decl : Id.t * constr option * types -> std_ppcmds; + print_named_decl : Context.Named.Declaration.t -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; diff --git a/printing/printer.ml b/printing/printer.ml index 33b95c2f56..70b5ffcc41 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -30,7 +30,8 @@ let delayed_emacs_cmd s = let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> - (Evd.empty, Global.env()) + let env = Global.env () in + (Evd.from_env env, env) (**********************************************************************) (** Terms *) @@ -50,7 +51,7 @@ let pr_lconstr_core goal_concl_style env sigma t = let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env -let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env +let _ = Hook.set Refine.pr_constr pr_constr_env let pr_lconstr_goal_style_env env = pr_lconstr_core true env let pr_constr_goal_style_env env = pr_constr_core true env @@ -208,10 +209,10 @@ let safe_pr_constr t = let (sigma, env) = get_current_context () in safe_pr_constr_env env sigma t -let pr_universe_ctx c = +let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context Universes.pr_with_global_universes c)) c + (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c else mt() @@ -262,16 +263,19 @@ let pr_var_decl_skel pr_id env sigma (id,c,typ) = let ptyp = (str" : " ++ pt) in (pr_id id ++ hov 0 (pbody ++ ptyp)) -let pr_var_decl env sigma (id,c,typ) = - pr_var_decl_skel pr_id env sigma (id,c,typ) +let pr_var_decl env sigma d = + pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d) let pr_var_list_decl env sigma (l,c,typ) = hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) -let pr_rel_decl env sigma (na,c,typ) = - let pbody = match c with - | None -> mt () - | Some c -> +let pr_rel_decl env sigma decl = + let open Context.Rel.Declaration in + let na = get_name decl in + let typ = get_type decl in + let pbody = match decl with + | LocalAssum _ -> mt () + | LocalDef (_,c,_) -> (* Force evaluation *) let pb = pr_lconstr_env env sigma c in let pb = if isCast c then surround pb else pb in @@ -293,7 +297,7 @@ let pr_named_context_of env sigma = hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) let pr_named_context env sigma ne_context = - hv 0 (Context.fold_named_context + hv 0 (Context.Named.fold_outside (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) ne_context ~init:(mt ())) @@ -306,7 +310,7 @@ let pr_rel_context_of env sigma = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env sigma = let sign_env = - Context.fold_named_list_context + Context.NamedList.fold (fun d pps -> let pidt = pr_var_list_decl env sigma d in (pps ++ fnl () ++ pidt)) @@ -333,7 +337,7 @@ let pr_context_limit n env sigma = else let k = lgsign-n in let _,sign_env = - Context.fold_named_list_context + Context.NamedList.fold (fun d (i,pps) -> if i < k then (i+1, (pps ++str ".")) @@ -400,7 +404,7 @@ let display_name = false (* display a goal name *) let pr_goal_name sigma g = - if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma)) + if display_name then str " " ++ Pp.surround (pr_existential_key sigma g) else mt () (* display the conclusion of a goal *) @@ -420,7 +424,8 @@ let pr_evgl_sign sigma evi = | None -> [], [] | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) in - let ids = List.rev_map pi1 l in + let open Context.Named.Declaration in + let ids = List.rev_map get_id l in let warn = if List.is_empty ids then mt () else (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") @@ -455,14 +460,17 @@ let pr_ne_evar_set hd tl sigma l = else mt () +let pr_selected_subgoal name sigma g = + let pg = default_pr_goal { sigma=sigma ; it=g; } in + v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g + ++ str " is:" ++ cut () ++ pg) + let default_pr_subgoal n sigma = let rec prrec p = function | [] -> error "No such goal." | g::rest -> if Int.equal p 1 then - let pg = default_pr_goal { sigma=sigma ; it=g; } in - v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g - ++ str " is:" ++ cut () ++ pg) + pr_selected_subgoal (int n) sigma g else prrec (p-1) rest in @@ -636,8 +644,8 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ - (match Proof_global.Bullet.suggest p - with None -> str"" | Some s -> fnl () ++ str s) ++ + (let s = Proof_global.Bullet.suggest p in + if Pp.is_empty s then s else fnl () ++ s) ++ fnl () in pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals @@ -652,9 +660,17 @@ let pr_nth_open_subgoal n = let pr_goal_by_id id = let p = Proof_global.give_me_the_proof () in - let g = Goal.get_by_uid id in + try + Proof.in_proof p (fun sigma -> + let g = Evd.evar_key id sigma in + pr_selected_subgoal (pr_id id) sigma g) + with Not_found -> error "No such goal." + +let pr_goal_by_uid uid = + let p = Proof_global.give_me_the_proof () in + let g = Goal.get_by_uid uid in let pr gs = - v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut () + v 0 (str "goal / evar " ++ str uid ++ str " is:" ++ cut () ++ pr_goal gs) in try @@ -715,7 +731,7 @@ let prterm = pr_lconstr type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (* An opaque constant. *) | Transparent of constant @@ -742,7 +758,8 @@ module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) let pr_assumptionset env s = - if ContextObjectMap.is_empty s then + if ContextObjectMap.is_empty s && + engagement env = (PredicativeSet, StratifiedType) then str "Closed under the global context" else let safe_pr_constant env kn = @@ -765,7 +782,7 @@ let pr_assumptionset env s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in + let var = pr_id id ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) | Axiom (kn,[]) -> let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in @@ -774,7 +791,7 @@ let pr_assumptionset env s = let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++ cut() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> - str " used in " ++ str (Names.Label.to_string lbl) ++ + str " used in " ++ pr_label lbl ++ str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) l in (v, ax :: a, o, tr) @@ -788,6 +805,16 @@ let pr_assumptionset env s = let (vars, axioms, opaque, trans) = ContextObjectMap.fold fold s ([], [], [], []) in + let theory = + if is_impredicative_set env then + [str "Set is impredicative"] + else [] + in + let theory = + if type_in_type env then + str "Type hierarchy is collapsed (logic is inconsistent)" :: theory + else theory + in let opt_list title = function | [] -> None | l -> @@ -801,6 +828,7 @@ let pr_assumptionset env s = opt_list (str "Section Variables:") vars; opt_list (str "Axioms:") axioms; opt_list (str "Opaque constants:") opaque; + opt_list (str "Theory:") theory; ] in prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums) @@ -813,3 +841,7 @@ 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 (Evd.pr_evd_level evd) inst ++ str"}" + diff --git a/printing/printer.mli b/printing/printer.mli index 5f56adbe6f..70993bb727 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,7 +10,6 @@ open Pp open Names open Globnames open Term -open Context open Environ open Pattern open Evd @@ -84,7 +83,8 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds -val pr_universe_ctx : Univ.universe_context -> std_ppcmds +val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds +val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) @@ -108,13 +108,13 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds val pr_context_unlimited : env -> evar_map -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds -val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds -val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds -val pr_rel_decl : env -> evar_map -> rel_declaration -> std_ppcmds +val pr_var_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds +val pr_var_list_decl : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds +val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds -val pr_named_context : env -> evar_map -> named_context -> std_ppcmds +val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds val pr_named_context_of : env -> evar_map -> std_ppcmds -val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds +val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds val pr_rel_context_of : env -> evar_map -> std_ppcmds val pr_context_of : env -> evar_map -> std_ppcmds @@ -164,7 +164,7 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *) type context_object = | Variable of Id.t (** A section variable or a Let definition *) (** An axiom and the type it inhabits (if an axiom of the empty type) *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (** An opaque constant. *) | Transparent of constant (** A transparent constant *) @@ -175,7 +175,8 @@ module ContextObjectMap : CMap.ExtS val pr_assumptionset : env -> Term.types ContextObjectMap.t -> std_ppcmds -val pr_goal_by_id : string -> std_ppcmds +val pr_goal_by_id : Id.t -> std_ppcmds +val pr_goal_by_uid : string -> std_ppcmds type printer_pr = { pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; diff --git a/printing/printmod.ml b/printing/printmod.ml index 295d8aaa66..9354cd28d0 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -72,10 +72,10 @@ let print_params env sigma params = if List.is_empty params then mt () else Printer.pr_rel_context env sigma params ++ brk(1,2) -let print_constructors envpar names types = +let print_constructors envpar sigma names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c) + (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c) (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) @@ -83,21 +83,26 @@ let print_constructors envpar names types = let build_ind_type env mip = Inductive.type_of_inductive env mip -let print_one_inductive env mib ((_,i) as ind) = +let print_one_inductive env sigma mib ((_,i) as ind) = let u = if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = extended_rel_list 0 params in + let args = Context.Rel.to_extended_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in + let inst = + if mib.mind_polymorphic then + Printer.pr_universe_instance sigma mib.mind_universes + else mt () + in hov 0 ( - pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ - brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes + pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ + brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) @@ -109,11 +114,13 @@ let print_mutual_inductive env mind mib = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in + let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env mib) inds ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + (print_one_inductive env sigma mib) inds ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -136,12 +143,14 @@ let print_record env mind mib = in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = extended_rel_list 0 params in + let args = Context.Rel.to_extended_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist env cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in + let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let keyword = let open Decl_kinds in match mib.mind_finite with @@ -153,16 +162,16 @@ let print_record env mind mib = hov 0 ( Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ - print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++ + print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ str ":= " ++ pr_id mip.mind_consnames.(0)) ++ brk(1,2) ++ hv 2 (str "{ " ++ prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ - Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then @@ -254,11 +263,16 @@ let nametab_register_modparam mbid mtb = List.iter (nametab_register_body mp dir) struc let print_body is_impl env mp (l,body) = - let name = str (Label.to_string l) in + let name = pr_label l in hov 2 (match body with | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> + let u = + if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + else Univ.Instance.empty + in + let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -267,15 +281,17 @@ let print_body is_impl env mp (l,body) = | None -> mt () | Some env -> str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *) - (Typeops.type_of_constant_type env cb.const_type)) ++ + hov 0 (Printer.pr_ltype_env env sigma + (Vars.subst_instance_constr u + (Typeops.type_of_constant_type env cb.const_type))) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l)) + Printer.pr_lconstr_env env sigma + (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx cb.const_universes) + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes)) | SFBmind mib -> try let env = Option.get env in @@ -315,15 +331,17 @@ let rec print_typ_expr env mp locals mty = let mapp = List.tl lapp in hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++ prlist_with_sep spc (print_modpath locals) mapp ++ str")") - | MEwith(me,WithDef(idl,c))-> + | MEwith(me,WithDef(idl,(c, _)))-> let env' = None in (* TODO: build a proper environment if env <> None *) let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() - ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) - | MEwith(me,WithMod(idl,mp))-> + ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() + ++ Printer.pr_lconstr c) + | MEwith(me,WithMod(idl,mp'))-> let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ - keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) + keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc() + ++ print_modpath locals mp') let print_mod_expr env mp locals = function | MEident mp -> print_modpath locals mp diff --git a/printing/printmod.mli b/printing/printmod.mli index bea4753451..7f7d343927 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli index 5d0d4ab0b4..f71fffdcec 100644 --- a/printing/printmodsig.mli +++ b/printing/printmodsig.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/richprinter.mli b/printing/richprinter.mli index 41c313514b..261d22c4c3 100644 --- a/printing/richprinter.mli +++ b/printing/richprinter.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |