diff options
Diffstat (limited to 'printing')
-rw-r--r-- | printing/genprint.ml | 11 | ||||
-rw-r--r-- | printing/miscprint.ml | 6 | ||||
-rw-r--r-- | printing/ppannotation.ml | 2 | ||||
-rw-r--r-- | printing/ppannotation.mli | 1 | ||||
-rw-r--r-- | printing/ppconstr.ml | 88 | ||||
-rw-r--r-- | printing/ppconstrsig.mli | 1 | ||||
-rw-r--r-- | printing/pptactic.ml | 1071 | ||||
-rw-r--r-- | printing/pptactic.mli | 13 | ||||
-rw-r--r-- | printing/pptacticsig.mli | 66 | ||||
-rw-r--r-- | printing/ppvernac.ml | 1752 | ||||
-rw-r--r-- | printing/ppvernacsig.mli | 3 | ||||
-rw-r--r-- | printing/prettyp.ml | 48 | ||||
-rw-r--r-- | printing/prettyp.mli | 2 | ||||
-rw-r--r-- | printing/printer.ml | 221 | ||||
-rw-r--r-- | printing/printer.mli | 25 | ||||
-rw-r--r-- | printing/printing.mllib | 4 | ||||
-rw-r--r-- | printing/printmod.ml | 15 | ||||
-rw-r--r-- | printing/richprinter.ml | 25 | ||||
-rw-r--r-- | printing/richprinter.mli | 39 |
19 files changed, 1640 insertions, 1753 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml index d4f792b75..0ec35e07b 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -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/miscprint.ml b/printing/miscprint.ml index 22db3d0bf..7b2c5695f 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -28,14 +28,14 @@ and pr_intro_pattern_action prc = function | IntroInjection pl -> str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ str "]" - | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "/" ++ prc c + | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c | IntroRewrite true -> str "->" | IntroRewrite false -> str "<-" and pr_or_and_intro_pattern prc = function - | [pl] -> + | 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/ppannotation.ml b/printing/ppannotation.ml index df7f925b7..511f93569 100644 --- a/printing/ppannotation.ml +++ b/printing/ppannotation.ml @@ -20,7 +20,6 @@ type t = | AGlobAtomicTacticExpr of glob_atomic_tactic_expr | ARawTacticExpr of raw_tactic_expr | ARawAtomicTacticExpr of raw_atomic_tactic_expr - | ATacticExpr of tactic_expr | AAtomicTacticExpr of atomic_tactic_expr let tag_of_annotation = function @@ -32,7 +31,6 @@ let tag_of_annotation = function | AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr" | ARawTacticExpr _ -> "raw_tactic_expr" | ARawAtomicTacticExpr _ -> "raw_atomic_tactic_expr" - | ATacticExpr _ -> "tactic_expr" | AAtomicTacticExpr _ -> "atomic_tactic_expr" let attributes_of_annotation a = diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli index 84724053e..a0fef1a75 100644 --- a/printing/ppannotation.mli +++ b/printing/ppannotation.mli @@ -23,7 +23,6 @@ type t = | AGlobAtomicTacticExpr of glob_atomic_tactic_expr | ARawTacticExpr of raw_tactic_expr | ARawAtomicTacticExpr of raw_atomic_tactic_expr - | ATacticExpr of tactic_expr | AAtomicTacticExpr of atomic_tactic_expr val tag_of_annotation : t -> string diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e21bfa007..252b0967d 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Pp open Names @@ -136,8 +136,6 @@ 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 @@ -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 @@ -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 @@ -281,6 +279,8 @@ end) = struct | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 + | CPatCast _ -> + assert false in let loc = cases_pattern_expr_loc p in pr_with_comments loc @@ -300,6 +300,7 @@ end) = struct let begin_of_binder = function LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) + | LocalPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false let begin_of_binders = function @@ -348,6 +349,8 @@ end) = struct | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) + | LocalPattern _ -> + assert false let pr_undelimited_binders sep pr_c = prlist_with_sep sep (pr_binder_among_many pr_c) @@ -359,6 +362,8 @@ end) = struct pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) | LocalRawAssum _ :: _ as bdl -> pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl + | LocalPattern (loc,p,tyo) :: _ -> + str "'" ++ pr_patt ltop p | _ -> assert false let pr_binders_gen pr_c sep is_open = @@ -432,6 +437,7 @@ end) = struct let names_of_binder = function | LocalRawAssum (nal,_,_) -> nal | LocalRawDef (_,_) -> [] + | LocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" @@ -457,7 +463,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 +471,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 @@ -495,6 +501,11 @@ end) = struct pr (lapp,L) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) + let pr_record_body_gen pr l = + spc () ++ + prlist_with_sep pr_semicolon + (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l + let pr_forall () = keyword "forall" ++ spc () let pr_fun () = keyword "fun" ++ spc () @@ -527,6 +538,21 @@ end) = struct (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), lfix ) + | CProdN + (_, + [([(_,Name n)],_,_)], + CCases + (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)], + [(_,[(_,[p])],a)])) + when + Id.equal m n && + not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) -> + return ( + hov 0 ( + keyword "forall" ++ spc () ++ str "'" ++ pr_patt ltop p ++ + str "," ++ pr spc ltop a), + llambda + ) | CProdN _ -> let (bl,a) = extract_prod_binders a in return ( @@ -536,6 +562,21 @@ end) = struct str "," ++ pr spc ltop a), lprod ) + | CLambdaN + (_, + [([(_,Name n)],_,_)], + CCases + (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)], + [(_,[(_,[p])],a)])) + when + Id.equal m n && + not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) -> + return ( + hov 0 ( + keyword "fun" ++ spc () ++ str "'" ++ pr_patt ltop p ++ + pr_fun_sep ++ pr spc ltop a), + llambda + ) | CLambdaN _ -> let (bl,a) = extract_lam_binders a in return ( @@ -595,28 +636,17 @@ 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 ++ - prlist_with_sep pr_semicolon - (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l - ++ str" |}"), + hv 0 (str"{|" ++ pr_record_body_gen (pr spc) 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)), @@ -741,6 +771,8 @@ end) = struct let pr_cases_pattern_expr = pr_patt ltop + let pr_record_body = pr_record_body_gen pr + let pr_binders = pr_undelimited_binders spc (pr ltop) end diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli index c711dd8f7..a59fc6d67 100644 --- a/printing/ppconstrsig.mli +++ b/printing/ppconstrsig.mli @@ -50,6 +50,7 @@ module type Pp = sig ('a * Names.Id.t) option * recursion_order_expr -> std_ppcmds + val pr_record_body : (reference * constr_expr) list -> std_ppcmds val pr_binders : local_binder list -> std_ppcmds val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 08f037ca6..917a277c9 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -9,11 +9,12 @@ open Pp open Names open Namegen -open Errors +open CErrors open Util open Constrexpr open Tacexpr open Genarg +open Geninterp open Constrarg open Libnames open Ppextend @@ -26,22 +27,20 @@ open Printer let pr_global x = Nametab.pr_global_env Id.Set.empty x -type grammar_terminals = string option list +type 'a grammar_tactic_prod_item_expr = +| TacTerm of string +| TacNonTerm of Loc.t * 'a * Names.Id.t + +type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { - pptac_args : argument_type list; - pptac_prods : int * grammar_terminals; + pptac_level : int; + pptac_prods : grammar_terminals; } -(* ML Extensions *) -let prtac_tab = Hashtbl.create 17 - (* Tactic notations *) let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty -let declare_ml_tactic_pprule key pt = - Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods - let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab @@ -60,14 +59,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 @@ -93,8 +92,6 @@ module Make : raw_tactic_expr -> std_ppcmds -> std_ppcmds val tag_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds - val tag_tactic_expr - : tactic_expr -> std_ppcmds -> std_ppcmds val tag_atomic_tactic_expr : atomic_tactic_expr -> std_ppcmds -> std_ppcmds end) @@ -105,6 +102,39 @@ module Make let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) + let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with + | None -> false + | Some _ -> true + + let unbox : type a. Val.t -> a Val.typ -> a= fun (Val.Dyn (tag, x)) t -> + match Val.eq tag t with + | None -> assert false + | Some Refl -> x + + let rec pr_value lev v : std_ppcmds = + if has_type v Val.typ_list then + pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list) + else if has_type v Val.typ_opt then + pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt) + else if has_type v Val.typ_pair then + let (v1, v2) = unbox v Val.typ_pair in + str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")" + else + let Val.Dyn (tag, x) = v in + let name = Val.repr tag in + let default = str "<" ++ str name ++ str ">" in + match ArgT.name name with + | None -> default + | Some (ArgT.Any arg) -> + let wit = ExtraArg arg in + match val_tag (Topwit wit) with + | Val.Base t -> + begin match Val.eq t tag with + | None -> default + | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) + end + | _ -> default + let pr_with_occurrences pr (occs,c) = match occs with | AllOccurrences -> @@ -121,7 +151,8 @@ module Make exception ComplexRedFlag let pr_short_red_flag pr r = - if not r.rBeta || not r.rIota || not r.rZeta then raise ComplexRedFlag + if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then + raise ComplexRedFlag else if List.is_empty r.rConst then if r.rDelta then mt () else raise ComplexRedFlag else (if r.rDelta then str "-" else mt ()) ++ @@ -131,9 +162,12 @@ module Make try pr_short_red_flag pr r with complexRedFlags -> (if r.rBeta then pr_arg str "beta" else mt ()) ++ - (if r.rIota then pr_arg str "iota" else mt ()) ++ - (if r.rZeta then pr_arg str "zeta" else mt ()) ++ - (if List.is_empty r.rConst then + (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else + (if r.rMatch then pr_arg str "match" else mt ()) ++ + (if r.rFix then pr_arg str "fix" else mt ()) ++ + (if r.rCofix then pr_arg str "cofix" else mt ())) ++ + (if r.rZeta then pr_arg str "zeta" else mt ()) ++ + (if List.is_empty r.rConst then if r.rDelta then pr_arg str "delta" else mt () else @@ -150,7 +184,8 @@ module Make | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o | Cbv f -> - if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then + if f.rBeta && f.rMatch && f.rFix && f.rCofix && + f.rZeta && f.rDelta && List.is_empty f.rConst then keyword "compute" else hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) @@ -240,8 +275,10 @@ module Make | NoBindings -> mt () let pr_clear_flag clear_flag pp x = - (match clear_flag with Some false -> str "!" | Some true -> str ">" | None -> mt()) - ++ pp x + match clear_flag with + | Some false -> surround (pp x) + | Some true -> str ">" ++ pp x + | None -> pp x let pr_with_bindings prc prlc (c,bl) = prc c ++ pr_bindings prc prlc bl @@ -263,165 +300,73 @@ module Make let with_evars ev s = if ev then "e" ^ s else s + let hov_if_not_empty n p = if Pp.ismt p then p else hov n p - let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) - | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) - | ConstrMayEvalArgType -> - pr_may_eval prc prlc (pr_or_by_notation prref) prpat - (out_gen (rawwit wit_constr_may_eval) x) - | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat) - (out_gen (rawwit wit_red_expr) x) - | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x) - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - pr_sequence map (raw l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match raw o with - | None -> mt () - | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) - in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = raw o in - let p = in_gen (rawwit wit1) p in - let q = in_gen (rawwit wit2) q in - pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q] - in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_raw_print x - - - let rec pr_glb_generic prc prlc prtac prpat x = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) - | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) - | ConstrMayEvalArgType -> - pr_may_eval prc prlc - (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat - (out_gen (glbwit wit_constr_may_eval) x) - | QuantHypArgType -> - pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr - (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat) - (out_gen (glbwit wit_red_expr) x) - | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x) - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in - pr_sequence map (glb l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match glb o with + 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_if_not_empty 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] - 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) + | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match top o with + hov_if_not_empty 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (rawwit wit1) p in + let q = in_gen (rawwit wit2) q in + hov_if_not_empty 0 (pr_sequence (pr_raw_generic_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_if_not_empty 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) + | Some x -> pr_glb_generic_rec 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 = top o in - let p = in_gen (topwit wit1) p in - let q = in_gen (topwit wit2) q in - pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q] - in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_top_print x + hov_if_not_empty 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (glbwit wit1) p in + let q = in_gen (glbwit wit2) q in + let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in + hov_if_not_empty 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 tacarg_using_rule_token pr_gen = function - | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) - | None :: l, a :: al -> - let r = tacarg_using_rule_token pr_gen (l,al) in - pr_gen a :: r - | [], [] -> [] - | _ -> failwith "Inconsistent arguments of extended tactic" + | [] -> [] + | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l + | TacNonTerm (_, (symb, arg), _) :: l -> + pr_gen symb arg :: tacarg_using_rule_token pr_gen l let pr_tacarg_using_rule pr_gen l = let l = match l with - | (Some s :: l, al) -> + | TacTerm s :: l -> (** 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)) + primitive s :: tacarg_using_rule_token pr_gen l | _ -> tacarg_using_rule_token pr_gen l in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev s l = - try - let tags = List.map genarg_tag l in - let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in - let p = pr_tacarg_using_rule pr_gen (pl,l) in - if lev' > lev then surround p else p - with Not_found -> - let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in + let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = + let name = + str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ + str "@" ++ int i + in let args = match l with | [] -> mt () | _ -> spc() ++ pr_sequence pr_gen l @@ -430,36 +375,97 @@ module Make let pr_alias_key key = try - let _,prods = (KNmap.find key !prnotation_tab).pptac_prods in + let prods = (KNmap.find key !prnotation_tab).pptac_prods in (* First printing strategy: only the head symbol *) match prods with - | Some s :: _ -> str s - | _ -> raise Exit - with Not_found | Exit -> + | TacTerm s :: prods -> str s + | _ -> + (* Second printing strategy; if ever Tactic Notation is eventually *) + (* accepting notations not starting with an identifier *) + let rec pr = function + | [] -> [] + | TacTerm s :: prods -> s :: pr prods + | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in + str (String.concat " " (pr prods)) + with Not_found -> KerName.print key let pr_alias_gen pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in - let (lev', pl) = pp.pptac_prods in - let p = pr_tacarg_using_rule pr_gen (pl, l) in - if lev' > lev then surround p else p + let rec pack prods args = match prods, args with + | [], [] -> [] + | TacTerm s :: prods, args -> TacTerm s :: pack prods args + | TacNonTerm (loc, symb, id) :: prods, arg :: args -> + TacNonTerm (loc, (symb, arg), id) :: pack prods args + | _ -> raise Not_found + in + let prods = pack pp.pptac_prods l in + let p = pr_tacarg_using_rule pr_gen prods 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 pr_raw_alias prc prlc prtac prpat = - pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference) - let pr_glob_alias prc prlc prtac prpat = - pr_alias_gen (pr_glb_generic prc prlc prtac prpat) - let pr_alias prc prlc prtac prpat = - pr_alias_gen (pr_top_generic prc prlc prtac prpat) + let pr arg = str "_" in + KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" + + let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg)) + + let is_genarg tag wit = + let ArgT.Any tag = tag in + argument_type_eq (ArgumentType (ExtraArg tag)) wit + + let get_list : type l. l generic_argument -> l generic_argument list option = + function (GenArg (wit, arg)) -> match wit with + | Rawwit (ListArg wit) -> Some (List.map (in_gen (rawwit wit)) arg) + | Glbwit (ListArg wit) -> Some (List.map (in_gen (glbwit wit)) arg) + | _ -> None + + let get_opt : type l. l generic_argument -> l generic_argument option option = + function (GenArg (wit, arg)) -> match wit with + | Rawwit (OptArg wit) -> Some (Option.map (in_gen (rawwit wit)) arg) + | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg) + | _ -> None + + let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds = + fun prtac symb arg -> match symb with + | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg + | Extend.Ulist1 s | Extend.Ulist0 s -> + begin match get_list arg with + | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | Some l -> pr_sequence (pr_any_arg prtac s) l + end + | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) -> + begin match get_list arg with + | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l + end + | Extend.Uopt s -> + begin match get_opt arg with + | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | Some l -> pr_opt (pr_any_arg prtac s) l + end + | Extend.Uentry _ | Extend.Uentryl _ -> + str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + + let rec pr_targ prtac symb arg = match symb with + | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> + prtac (1, Any) arg + | Extend.Uentryl (_, l) -> prtac (l, Any) arg + | _ -> + match arg with + | TacGeneric arg -> + let pr l arg = prtac l (TacGeneric arg) in + pr_any_arg pr symb arg + | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + + let pr_raw_extend_rec prc prlc prtac prpat = + pr_extend_gen (pr_farg prtac) + let pr_glob_extend_rec prc prlc prtac prpat = + pr_extend_gen (pr_farg prtac) + + let pr_raw_alias prc prlc prtac prpat lev key args = + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args + let pr_glob_alias prc prlc prtac prpat lev key args = + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args (**********************************************************************) (* The tactic printer *) @@ -524,10 +530,9 @@ module Make let pr_with_induction_names prc = function | None, None -> mt () - | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat) - | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat) + | Some eqpat, None -> hov 1 (pr_eqn_ipat eqpat) + | None, Some ipat -> hov 1 (pr_as_disjunctive_ipat prc ipat) | Some eqpat, Some ipat -> - spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat) let pr_as_intro_pattern prc ipat = @@ -569,8 +574,8 @@ module Make spc() ++ prc c ++ pr_as_ipat prdc ipat let pr_by_tactic prt = function - | TacId [] -> mt () - | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac + | Some tac -> keyword "by" ++ spc () ++ prt tac + | None -> mt() let pr_hyp_location pr_id = function | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs @@ -583,7 +588,7 @@ module Make str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")" ) occs - let pr_in pp = spc () ++ hov 0 (keyword "in" ++ pp) + let pr_in pp = hov 0 (keyword "in" ++ pp) let pr_simple_hyp_clause pr_id = function | [] -> mt () @@ -620,16 +625,30 @@ module Make | RepeatStar -> str "?" | RepeatPlus -> str "!" - let pr_induction_arg prc prlc = function + let pr_core_destruction_arg prc prlc = function | ElimOnConstr c -> pr_with_bindings prc prlc c | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) | ElimOnAnonHyp n -> int n - let pr_induction_kind = function + let pr_destruction_arg prc prlc (clear_flag,h) = + pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h + + let pr_inversion_kind = function | SimpleInversion -> primitive "simple inversion" | FullInversion -> primitive "inversion" | FullInversionClear -> primitive "inversion_clear" + let pr_range_selector (i, j) = + if Int.equal i j then int i + else int i ++ str "-" ++ int j + + let pr_goal_selector = function + | SelectNth i -> int i ++ str ":" + | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ + str "]" ++ str ":" + | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":" + | SelectAll -> str "all" ++ str ":" + let pr_lazy = function | General -> keyword "multi" | Select -> keyword "lazy" @@ -716,20 +735,13 @@ module Make str " ]") let pr_hintbases = function - | None -> spc () ++ keyword "with" ++ str" *" + | None -> keyword "with" ++ str" *" | Some [] -> mt () - | Some l -> - spc () ++ hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l) + | Some l -> hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l) let pr_auto_using prc = function | [] -> mt () - | l -> spc () ++ - hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l) - - let string_of_debug = function - | Off -> "" - | Debug -> "debug " - | Info -> "info_" + | l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l) let pr_then () = str ";" @@ -756,7 +768,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; @@ -765,13 +776,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_name -> '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,306 +791,216 @@ module Make level :'lev > - let make_pr_tac pr strip_prod_binders tag_atom tag = + let pr_atom pr strip_prod_binders tag_atom = + let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in + let pr_with_bindings_arg_full = pr_with_bindings_arg in + let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in + let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in + + let pr_constrarg c = spc () ++ pr.pr_constr c in + let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in + let pr_intarg n = spc () ++ int n in + + (* Some printing combinators *) + let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in + + let pr_binder_fix (nal,t) = + (* match t with + | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal + | _ ->*) + let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + spc() ++ hov 1 (str"(" ++ s ++ str")") in + + let pr_fix_tac (id,n,c) = + let rec set_nth_name avoid n = function + (nal,ty)::bll -> + if n <= List.length nal then + match List.chop (n-1) nal with + _, (_,Name id) :: _ -> id, (nal,ty)::bll + | bef, (loc,Anonymous) :: aft -> + let id = next_ident_away (Id.of_string"y") avoid in + id, ((bef@(loc,Name id)::aft, ty)::bll) + | _ -> assert false + else + let (id,bll') = set_nth_name avoid (n-List.length nal) bll in + (id,(nal,ty)::bll') + | [] -> assert false in + let (bll,ty) = strip_prod_binders n c in + let names = + List.fold_left + (fun ln (nal,_) -> List.fold_left + (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) + ln nal) + [] bll in + let idarg,bll = set_nth_name names n bll in + let annot = match names with + | [_] -> + mt () + | _ -> + spc() ++ str"{" + ++ keyword "struct" ++ spc () + ++ pr_id idarg ++ str"}" + in + hov 1 (str"(" ++ pr_id id ++ + prlist pr_binder_fix bll ++ annot ++ str" :" ++ + pr_lconstrarg ty ++ str")") in + (* spc() ++ + hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg + c) + *) + let pr_cofix_tac (id,c) = + hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in + + (* Printing tactics as arguments *) + let rec pr_atom0 a = tag_atom a (match a with + | TacIntroPattern (false,[]) -> primitive "intros" + | TacIntroPattern (true,[]) -> primitive "eintros" + | t -> str "(" ++ pr_atom1 t ++ str ")" + ) + + (* Main tactic printer *) + and pr_atom1 a = tag_atom a (match a with + (* Basic tactics *) + | TacIntroPattern (ev,[]) as t -> + pr_atom0 t + | TacIntroPattern (ev,(_::_ as p)) -> + hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++ + prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) + | TacApply (a,ev,cb,inhyp) -> + hov 1 ( + (if a then mt() else primitive "simple ") ++ + primitive (with_evars ev "apply") ++ spc () ++ + prlist_with_sep pr_comma pr_with_bindings_arg cb ++ + pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp + ) + | TacElim (ev,cb,cbo) -> + hov 1 ( + primitive (with_evars ev "elim") + ++ pr_arg pr_with_bindings_arg cb + ++ pr_opt pr_eliminator cbo) + | TacCase (ev,cb) -> + hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb) + | 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) + | TacMutualCofix (id,l) -> + hov 1 ( + primitive "cofix" ++ spc () ++ pr_id id ++ spc() + ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l + ) + | TacAssert (b,Some tac,ipat,c) -> + hov 1 ( + primitive (if b then "assert" else "enough") ++ + pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ + pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + ) + | TacAssert (_,None,ipat,c) -> + hov 1 ( + primitive "pose proof" + ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c + ) + | TacGeneralize l -> + hov 1 ( + primitive "generalize" ++ spc () + ++ prlist_with_sep pr_comma (fun (cl,na) -> + pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) + l + ) + | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> + hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) + | TacLetTac (na,c,cl,b,e) -> + hov 1 ( + (if b then primitive "set" else primitive "remember") ++ + (if b then pr_pose pr.pr_constr pr.pr_lconstr na c + else pr_pose_as_style pr.pr_constr na c) ++ + pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ + pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl) + (* | TacInstantiate (n,c,ConclLocation ()) -> + hov 1 (str "instantiate" ++ spc() ++ + hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ + pr_lconstrarg c ++ str ")" )) + | TacInstantiate (n,c,HypLocation (id,hloc)) -> + hov 1 (str "instantiate" ++ spc() ++ + hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ + pr_lconstrarg c ++ str ")" ) + ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None))) + *) - (* some shortcuts *) - let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in - let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in - let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in - let pr_with_bindings_arg_full = pr_with_bindings_arg in - let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in - let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in + (* Derived basic tactics *) + | TacInductionDestruct (isrec,ev,(l,el)) -> + hov 1 ( + primitive (with_evars ev (if isrec then "induction" else "destruct")) + ++ spc () + ++ prlist_with_sep pr_comma (fun (h,ids,cl) -> + pr_destruction_arg pr.pr_dconstr pr.pr_dconstr h ++ + pr_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++ + pr_opt (pr_clauses None pr.pr_name) cl) l ++ + pr_opt pr_eliminator el + ) - let pr_constrarg c = spc () ++ pr.pr_constr c in - let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in - let pr_intarg n = spc () ++ int n in + (* Conversion *) + | TacReduce (r,h) -> + hov 1 ( + pr_red_expr r + ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h + ) + | TacChange (op,c,h) -> + hov 1 ( + primitive "change" ++ brk (1,1) + ++ ( + match op with + None -> + mt () + | Some p -> + pr.pr_pattern p ++ spc () + ++ keyword "with" ++ spc () + ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h + ) - (* Some printing combinators *) - let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in + (* Equality and inversion *) + | TacRewrite (ev,l,cl,tac) -> + hov 1 ( + primitive (with_evars ev "rewrite") ++ spc () + ++ prlist_with_sep + (fun () -> str ","++spc()) + (fun (b,m,c) -> + pr_orient b ++ pr_multi m ++ + pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c) + l + ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl + ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + ) + | TacInversion (DepInversion (k,c,ids),hyp) -> + hov 1 ( + primitive "dependent " ++ pr_inversion_kind k ++ spc () + ++ pr_quantified_hypothesis hyp + ++ pr_with_inversion_names pr.pr_dconstr ids + ++ pr_with_constr pr.pr_constr c + ) + | TacInversion (NonDepInversion (k,cl,ids),hyp) -> + hov 1 ( + pr_inversion_kind k ++ spc () + ++ pr_quantified_hypothesis hyp + ++ pr_non_empty_arg (pr_with_inversion_names pr.pr_dconstr) ids + ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl + ) + | TacInversion (InversionUsing (c,cl),hyp) -> + hov 1 ( + primitive "inversion" ++ spc() + ++ pr_quantified_hypothesis hyp ++ spc () + ++ keyword "using" ++ spc () ++ pr.pr_constr c + ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl + ) + ) + in + pr_atom1 + + let make_pr_tac pr strip_prod_binders tag_atom tag = let extract_binders = function | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body) | body -> ([],body) in - - let pr_binder_fix (nal,t) = - (* match t with - | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal - | _ ->*) - let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in - spc() ++ hov 1 (str"(" ++ s ++ str")") in - - let pr_fix_tac (id,n,c) = - let rec set_nth_name avoid n = function - (nal,ty)::bll -> - if n <= List.length nal then - match List.chop (n-1) nal with - _, (_,Name id) :: _ -> id, (nal,ty)::bll - | bef, (loc,Anonymous) :: aft -> - let id = next_ident_away (Id.of_string"y") avoid in - id, ((bef@(loc,Name id)::aft, ty)::bll) - | _ -> assert false - else - let (id,bll') = set_nth_name avoid (n-List.length nal) bll in - (id,(nal,ty)::bll') - | [] -> assert false in - let (bll,ty) = strip_prod_binders n c in - let names = - List.fold_left - (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) - ln nal) - [] bll in - let idarg,bll = set_nth_name names n bll in - let annot = match names with - | [_] -> - mt () - | _ -> - spc() ++ str"{" - ++ keyword "struct" ++ spc () - ++ pr_id idarg ++ str"}" - in - hov 1 (str"(" ++ pr_id id ++ - prlist pr_binder_fix bll ++ annot ++ str" :" ++ - pr_lconstrarg ty ++ str")") in - (* spc() ++ - hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg - c) - *) - let pr_cofix_tac (id,c) = - hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in - - (* Printing tactics as arguments *) - let rec pr_atom0 a = tag_atom a (match a with - | TacIntroPattern [] -> primitive "intros" - | TacIntroMove (None,MoveLast) -> primitive "intro" - | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial" - | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto" - | TacClear (true,[]) -> primitive "clear" - | t -> str "(" ++ pr_atom1 t ++ str ")" - ) - - (* Main tactic printer *) - and pr_atom1 a = tag_atom a (match a with - (* Basic tactics *) - | TacIntroPattern [] as t -> - pr_atom0 t - | TacIntroPattern (_::_ as p) -> - hov 1 (primitive "intros" ++ spc () ++ - prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) - | TacIntroMove (None,MoveLast) as t -> - pr_atom0 t - | TacIntroMove (Some id,MoveLast) -> - primitive "intro" ++ spc () ++ pr_id id - | TacIntroMove (ido,hto) -> - hov 1 (primitive "intro" ++ pr_opt pr_id ido ++ - Miscprint.pr_move_location pr.pr_name hto) - | TacExact c -> - hov 1 (primitive "exact" ++ pr_constrarg c) - | TacApply (a,ev,cb,inhyp) -> - hov 1 ( - (if a then mt() else primitive "simple ") ++ - primitive (with_evars ev "apply") ++ spc () ++ - prlist_with_sep pr_comma pr_with_bindings_arg cb ++ - pr_in_hyp_as pr.pr_dconstr pr.pr_name inhyp - ) - | TacElim (ev,cb,cbo) -> - hov 1 ( - primitive (with_evars ev "elim") - ++ pr_arg pr_with_bindings_arg cb - ++ pr_opt pr_eliminator cbo) - | TacCase (ev,cb) -> - hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb) - | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n) - | TacMutualFix (id,n,l) -> - hov 1 ( - primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() - ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l) - | TacCofix ido -> - hov 1 (primitive "cofix" ++ pr_opt pr_id ido) - | TacMutualCofix (id,l) -> - hov 1 ( - primitive "cofix" ++ spc () ++ pr_id id ++ spc() - ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l - ) - | TacAssert (b,Some tac,ipat,c) -> - hov 1 ( - primitive (if b then "assert" else "enough") ++ - pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ - pr_by_tactic (pr.pr_tactic ltop) tac - ) - | TacAssert (_,None,ipat,c) -> - hov 1 ( - primitive "pose proof" - ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c - ) - | TacGeneralize l -> - hov 1 ( - primitive "generalize" ++ spc () - ++ prlist_with_sep pr_comma (fun (cl,na) -> - pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) - l - ) - | TacGeneralizeDep c -> - hov 1 ( - primitive "generalize" ++ spc () ++ str "dependent" - ++ pr_constrarg c - ) - | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> - hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) - | TacLetTac (na,c,cl,b,e) -> - hov 1 ( - (if b then primitive "set" else primitive "remember") ++ - (if b then pr_pose pr.pr_constr pr.pr_lconstr na c - else pr_pose_as_style pr.pr_constr na c) ++ - pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ - pr_clauses (Some b) pr.pr_name cl) - (* | TacInstantiate (n,c,ConclLocation ()) -> - hov 1 (str "instantiate" ++ spc() ++ - hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ - pr_lconstrarg c ++ str ")" )) - | TacInstantiate (n,c,HypLocation (id,hloc)) -> - hov 1 (str "instantiate" ++ spc() ++ - hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ - pr_lconstrarg c ++ str ")" ) - ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None))) - *) - - (* Derived basic tactics *) - | TacInductionDestruct (isrec,ev,(l,el)) -> - hov 1 ( - primitive (with_evars ev (if isrec then "induction" else "destruct")) - ++ spc () - ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) -> - pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++ - pr_with_induction_names pr.pr_dconstr ids ++ - pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++ - pr_opt pr_eliminator el - ) - | TacDoubleInduction (h1,h2) -> - hov 1 ( - primitive "double induction" - ++ pr_arg pr_quantified_hypothesis h1 - ++ pr_arg pr_quantified_hypothesis h2 - ) - - (* Automation tactics *) - | TacTrivial (_,[],Some []) as x -> - pr_atom0 x - | TacTrivial (d,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "trivial" - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - | TacAuto (_,None,[],Some []) as x -> - pr_atom0 x - | TacAuto (d,n,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "auto" - ++ pr_opt (pr_or_var int) n - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - - (* Context management *) - | TacClear (true,[]) as t -> - pr_atom0 t - | TacClear (keep,l) -> - hov 1 ( - primitive "clear" ++ spc () - ++ (if keep then str "- " else mt ()) - ++ prlist_with_sep spc pr.pr_name l - ) - | TacClearBody l -> - hov 1 ( - primitive "clearbody" ++ spc () - ++ prlist_with_sep spc pr.pr_name l - ) - | TacMove (id1,id2) -> - hov 1 ( - primitive "move" - ++ brk (1,1) ++ pr.pr_name id1 - ++ Miscprint.pr_move_location pr.pr_name id2 - ) - | TacRename l -> - hov 1 ( - primitive "rename" ++ brk (1,1) - ++ prlist_with_sep - (fun () -> str "," ++ brk (1,1)) - (fun (i1,i2) -> - pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2) - l - ) - - (* Constructors *) - | TacSplit (ev,l) -> - hov 1 ( - primitive (with_evars ev "exists") - ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l - ) - - (* Conversion *) - | TacReduce (r,h) -> - hov 1 ( - pr_red_expr r - ++ pr_clauses (Some true) pr.pr_name h - ) - | TacChange (op,c,h) -> - hov 1 ( - primitive "change" ++ brk (1,1) - ++ ( - match op with - None -> - mt () - | Some p -> - pr.pr_pattern p ++ spc () - ++ keyword "with" ++ spc () - ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h - ) - - (* Equivalence relations *) - | TacSymmetry cls -> - primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls - - (* Equality and inversion *) - | TacRewrite (ev,l,cl,by) -> - hov 1 ( - primitive (with_evars ev "rewrite") ++ spc () - ++ prlist_with_sep - (fun () -> str ","++spc()) - (fun (b,m,c) -> - pr_orient b ++ pr_multi m ++ - pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c) - l - ++ pr_clauses (Some true) pr.pr_name cl - ++ ( - match by with - | Some by -> pr_by_tactic (pr.pr_tactic ltop) by - | None -> mt() - ) - ) - | TacInversion (DepInversion (k,c,ids),hyp) -> - hov 1 ( - primitive "dependent " ++ pr_induction_kind k ++ spc () - ++ pr_quantified_hypothesis hyp - ++ pr_with_inversion_names pr.pr_dconstr ids - ++ pr_with_constr pr.pr_constr c - ) - | TacInversion (NonDepInversion (k,cl,ids),hyp) -> - hov 1 ( - pr_induction_kind k ++ spc () - ++ pr_quantified_hypothesis hyp - ++ pr_with_inversion_names pr.pr_dconstr ids - ++ pr_simple_hyp_clause pr.pr_name cl - ) - | TacInversion (InversionUsing (c,cl),hyp) -> - hov 1 ( - primitive "inversion" ++ spc() - ++ pr_quantified_hypothesis hyp ++ spc () - ++ keyword "using" ++ spc () ++ pr.pr_constr c - ++ pr_simple_hyp_clause pr.pr_name cl - ) - ) - in - let rec pr_tac inherited tac = let return (doc, l) = (tag tac doc, l) in let (strm, prec) = return (match tac with @@ -1235,10 +1155,11 @@ module Make keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> pr_tac (lcomplete,E) t, lcomplete + | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom | TacAtom (loc,t) -> - pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom + pr_with_comments loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom | TacArg(_,Tacexp e) -> pr.pr_tactic (latom,E) e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> @@ -1261,26 +1182,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 -> @@ -1308,7 +1220,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; @@ -1316,8 +1227,8 @@ module Make pr_constant = pr_or_by_notation pr_reference; pr_reference = pr_reference; pr_name = pr_lident; - pr_generic = Genprint.generic_raw_print; - pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; + pr_generic = pr_raw_generic_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference; + 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 @@ -1329,9 +1240,9 @@ module Make let pr_and_constr_expr pr (c,_) = pr c - let pr_pat_and_constr_expr pr ((c,_),_) = pr c + let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c - let rec pr_glob_tactic_level env n t = + let pr_glob_tactic_level env n t = let glob_printers = (strip_prod_binders_glob_constr) in @@ -1339,7 +1250,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); @@ -1347,8 +1257,10 @@ module Make pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env)); pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; - pr_generic = Genprint.generic_glb_print; - pr_extend = pr_glob_extend + pr_generic = pr_glb_generic_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_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 @@ -1373,39 +1285,49 @@ module Make | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty - let pr_tactic_level env n t = - let typed_printers = - (strip_prod_binders_constr) - in - let prtac n (t:tactic_expr) = + let pr_atomic_tactic_level env n t = + let prtac n (t:atomic_tactic_expr) = let pr = { - pr_tactic = pr_glob_tactic_level env; + pr_tactic = (fun _ _ -> str "<tactic>"); pr_constr = pr_constr_env env Evd.empty; - pr_uconstr = pr_closed_glob_env env Evd.empty; pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_lconstr_env env Evd.empty; - pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); - pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env); - pr_constant = pr_and_short_name (pr_evaluable_reference_env env); + pr_pattern = pr_constr_pattern_env env Evd.empty; + pr_lpattern = pr_lconstr_pattern_env env Evd.empty; + pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; - pr_generic = Genprint.generic_top_print; - pr_extend = pr_extend - (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern; - pr_alias = pr_alias - (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern; + (** Those are not used by the atomic printer *) + pr_generic = (fun _ -> assert false); + pr_extend = (fun _ _ _ -> assert false); + pr_alias = (fun _ _ _ -> assert false); } in - make_pr_tac - pr typed_printers - tag_atomic_tactic_expr tag_tactic_expr - n t + pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t in prtac n t - let pr_tactic env = pr_tactic_level env ltop + 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_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 pr_alias pr lev key args = + pr_alias_gen (fun _ arg -> pr arg) lev key args + + let pr_extend pr lev ml args = + pr_extend_gen pr lev ml args + + let pr_atomic_tactic env = pr_atomic_tactic_level env ltop end @@ -1435,37 +1357,77 @@ include Make (Ppconstr) (struct let tag_glob_atomic_tactic_expr = do_not_tag let tag_raw_tactic_expr = do_not_tag let tag_raw_atomic_tactic_expr = do_not_tag - let tag_tactic_expr = do_not_tag let tag_atomic_tactic_expr = do_not_tag end) (** Registering *) +let run_delayed c = + Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma } + +let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *) + | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (fst (run_delayed g)) + | clear_flag,ElimOnAnonHyp n as x -> x + | clear_flag,ElimOnIdent id as x -> x + 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) (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) ; - Genprint.register_print0 Constrarg.wit_sort - pr_glob_sort pr_glob_sort (pr_sort Evd.empty); + Genprint.register_print0 + Constrarg.wit_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_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 Constrarg.wit_destruction_arg + (pr_destruction_arg pr_constr_expr pr_lconstr_expr) + (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg 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; @@ -1476,16 +1438,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 @@ -1500,7 +1456,6 @@ module Richpp = struct let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a) let tag_raw_tactic_expr e = tag (ARawTacticExpr e) let tag_raw_atomic_tactic_expr a = tag (ARawAtomicTacticExpr a) - let tag_tactic_expr e = tag (ATacticExpr e) let tag_atomic_tactic_expr a = tag (AAtomicTacticExpr a) end) diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 313465614..86e3ea548 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -11,11 +11,15 @@ open Pp open Genarg +open Geninterp open Names open Constrexpr open Tacexpr open Ppextend +type 'a grammar_tactic_prod_item_expr = +| TacTerm of string +| TacNonTerm of Loc.t * 'a * Names.Id.t type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> @@ -32,7 +36,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,14 +45,13 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit -type grammar_terminals = string option list +type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr 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 -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit (** The default pretty-printers produce {!Pp.std_ppcmds} that are diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index ecedc7756..c08d6044d 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -8,11 +8,10 @@ open Pp open Genarg -open Constrexpr +open Geninterp open Tacexpr open Ppextend open Environ -open Pattern open Misctypes module type Pp = sig @@ -32,46 +31,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_name -> raw_generic_argument list -> std_ppcmds - - val pr_glob_extend: - (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (glob_constr_pattern_and_expr -> std_ppcmds) -> int -> - ml_tactic_name -> glob_generic_argument list -> std_ppcmds + + val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds + + val pr_glb_generic : env -> glevel 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_name -> typed_generic_argument list -> std_ppcmds + (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + + val pr_alias_key : Names.KerName.t -> std_ppcmds + + val pr_alias : (Val.t -> std_ppcmds) -> + int -> Names.KerName.t -> Val.t list -> std_ppcmds val pr_alias_key : Names.KerName.t -> std_ppcmds @@ -83,7 +60,7 @@ module type Pp = sig val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds - val pr_tactic : env -> tactic_expr -> std_ppcmds + val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds val pr_hintbases : string list option -> std_ppcmds @@ -93,4 +70,11 @@ 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 + + val pr_value : tolerability -> Val.t -> std_ppcmds + end diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 38add9d2c..0d47b34df 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -9,7 +9,7 @@ open Pp open Names -open Errors +open CErrors open Util open Extend open Vernacexpr @@ -34,6 +34,8 @@ module Make 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_lident (loc,id) = @@ -79,21 +81,11 @@ 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() - let pr_ne_sep sep pr = function - [] -> mt() - | l -> sep() ++ pr l - let pr_set_entry_type = function | ETName -> str"ident" | ETReference -> str"global" @@ -105,18 +97,6 @@ module Make | ETBinder false -> str "closed binder" | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" - let strip_meta id = - let s = Id.to_string id in - if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1)) - else id - - let pr_production_item = function - | TacNonTerm (loc,nt,Some (p,sep)) -> - let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in - str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")" - | TacNonTerm (loc,nt,None) -> str nt - | TacTerm s -> qs s - let pr_comment pr_c = function | CommentConstr c -> pr_c c | CommentString s -> qs s @@ -181,6 +161,11 @@ module Make | HintsReference r -> pr_reference r | HintsConstr c -> pr_c c + let pr_hint_mode = function + | ModeInput -> str"+" + | ModeNoHeadEvar -> str"!" + | ModeOutput -> str"-" + let pr_hints db h pr_c pr_pat = let opth = pr_opt_hintbases db in let pph = @@ -202,8 +187,8 @@ module Make | HintsMode (m, l) -> keyword "Mode" ++ spc () - ++ pr_reference m ++ spc() ++ prlist_with_sep spc - (fun b -> if b then str"+" else str"-") l + ++ pr_reference m ++ spc() ++ + prlist_with_sep spc pr_hint_mode l | HintsConstructors c -> keyword "Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c @@ -243,6 +228,11 @@ module Make | 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 @@ -272,11 +262,12 @@ module Make | _ as c -> brk(0,2) ++ str" :" ++ pr_c c let pr_decl_notation prc ((loc,ntn),c,scopt) = - fnl () ++ keyword "where " ++ qs ntn ++ str " := " ++ prc c ++ + fnl () ++ keyword "where " ++ qs ntn ++ str " := " + ++ Flags.without_option Flags.beautify_file prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt let pr_binders_arg = - pr_ne_sep spc pr_binders + pr_non_empty_arg pr_binders let pr_and_type_binders_arg bl = pr_binders_arg bl @@ -375,6 +366,7 @@ module Make | SetAssoc RightA -> keyword "right associativity" | SetAssoc NonA -> keyword "no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ + | SetOnlyPrinting -> keyword "only printing" | SetOnlyParsing Flags.Current -> keyword "only parsing" | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat("text",s) -> keyword "format " ++ pr_located qs s @@ -385,22 +377,19 @@ 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_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) = + let pr_pure_lconstr c = Flags.without_option Flags.beautify_file pr_lconstr c in + let annot = pr_guard_annot pr_lconstr_expr bl ro in + 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_pure_lconstr def) def + ++ prlist (pr_decl_notation pr_constr) ntn + let pr_statement head (idpl,(bl,c,guard)) = assert (not (Option.is_empty idpl)); let id, pl = Option.get idpl in @@ -417,895 +406,820 @@ module Make (**************************************) (* Pretty printer for vernac commands *) (**************************************) - let make_pr_vernac pr_constr pr_lconstr = - let pr_constrarg c = spc () ++ pr_constr c in - let pr_lconstrarg c = spc () ++ pr_lconstr c in - let pr_intarg n = spc () ++ int n in - let pr_oc = function - None -> str" :" - | Some true -> str" :>" - | Some false -> str" :>>" - in - let pr_record_field ((x, pri), ntn) = - let prx = match x with - | (oc,AssumExpr (id,t)) -> - hov 1 (pr_lname id ++ - pr_oc oc ++ spc() ++ - pr_lconstr_expr t) - | (oc,DefExpr(id,b,opt)) -> (match opt with - | Some t -> - hov 1 (pr_lname id ++ - pr_oc oc ++ spc() ++ - pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) - | None -> - hov 1 (pr_lname id ++ str" :=" ++ spc() ++ - pr_lconstr b)) in - let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in - prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn - in - let pr_record_decl b c fs = - pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") - in - let pr_printable = function - | PrintFullContext -> - keyword "Print All" - | PrintSectionContext s -> - keyword "Print Section" ++ spc() ++ Libnames.pr_reference s - | PrintGrammar ent -> - keyword "Print Grammar" ++ spc() ++ str ent - | PrintLoadPath dir -> - keyword "Print LoadPath" ++ pr_opt pr_dirpath dir - | PrintModules -> - keyword "Print Modules" - | PrintMLLoadPath -> - keyword "Print ML Path" - | PrintMLModules -> - keyword "Print ML Modules" - | PrintDebugGC -> - keyword "Print ML GC" - | PrintGraph -> - keyword "Print Graph" - | PrintClasses -> - keyword "Print Classes" - | PrintTypeClasses -> - keyword "Print TypeClasses" - | PrintInstances qid -> - keyword "Print Instances" ++ spc () ++ pr_smart_global qid - | PrintLtac qid -> - keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid - | PrintCoercions -> - keyword "Print Coercions" - | PrintCoercionPaths (s,t) -> - keyword "Print Coercion Paths" ++ spc() - ++ pr_class_rawexpr s ++ spc() - ++ pr_class_rawexpr t - | PrintCanonicalConversions -> - keyword "Print Canonical Structures" - | PrintTables -> - keyword "Print Tables" - | PrintHintGoal -> - keyword "Print Hint" - | PrintHint qid -> - keyword "Print Hint" ++ spc () ++ pr_smart_global qid - | PrintHintDb -> - keyword "Print Hint *" - | PrintHintDbName s -> - keyword "Print HintDb" ++ spc () ++ str s - | PrintRewriteHintDbName s -> - keyword "Print Rewrite HintDb" ++ spc() ++ str s - | PrintUniverses (b, fopt) -> - let cmd = - if b then "Print Sorted Universes" - else "Print Universes" + 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 pr_dirpath dir + | PrintModules -> + keyword "Print Modules" + | PrintMLLoadPath -> + keyword "Print ML Path" + | PrintMLModules -> + keyword "Print ML Modules" + | PrintDebugGC -> + keyword "Print ML GC" + | PrintGraph -> + keyword "Print Graph" + | PrintClasses -> + keyword "Print Classes" + | PrintTypeClasses -> + keyword "Print TypeClasses" + | PrintInstances qid -> + keyword "Print Instances" ++ spc () ++ pr_smart_global qid + | 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 -> + keyword "Print" ++ spc() ++ pr_smart_global qid + | PrintModuleType qid -> + keyword "Print Module Type" ++ spc() ++ pr_reference qid + | PrintModule qid -> + keyword "Print Module" ++ spc() ++ pr_reference qid + | PrintInspect n -> + keyword "Inspect" ++ spc() ++ int n + | PrintScopes -> + keyword "Print Scopes" + | PrintScope s -> + keyword "Print Scope" ++ spc() ++ str s + | PrintVisibility s -> + keyword "Print Visibility" ++ pr_opt str s + | PrintAbout (qid,gopt) -> + pr_opt (fun g -> int g ++ str ":"++ spc()) gopt + ++ keyword "About" ++ spc() ++ pr_smart_global qid + | PrintImplicit qid -> + keyword "Print Implicit" ++ spc() ++ pr_smart_global qid + (* spiwack: command printing all the axioms and section variables used in a + term *) + | PrintAssumptions (b, t, qid) -> + let cmd = match b, t with + | true, true -> "Print All Dependencies" + | true, false -> "Print Opaque Dependencies" + | false, true -> "Print Transparent Dependencies" + | false, false -> "Print Assumptions" + in + keyword cmd ++ spc() ++ pr_smart_global qid + | PrintNamespace dp -> + keyword "Print Namespace" ++ pr_dirpath dp + | PrintStrategy None -> + keyword "Print Strategies" + | PrintStrategy (Some qid) -> + keyword "Print Strategy" ++ pr_smart_global qid + + let pr_using e = str (Proof_using.to_string e) + + let rec pr_vernac_body v = + let return = Taggers.tag_vernac v in + match v with + | VernacPolymorphic (poly, v) -> + let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in + return (s ++ spc () ++ pr_vernac_body v) + | VernacProgram v -> + return (keyword "Program" ++ spc() ++ pr_vernac_body v) + | VernacLocal (local, v) -> + return (pr_locality local ++ spc() ++ pr_vernac_body v) + + (* Stm *) + | VernacStm JoinDocument -> + return (keyword "Stm JoinDocument") + | VernacStm PrintDag -> + return (keyword "Stm PrintDag") + | VernacStm Finish -> + return (keyword "Stm Finish") + | VernacStm Wait -> + return (keyword "Stm Wait") + | VernacStm (Observe id) -> + return (keyword "Stm Observe " ++ str(Stateid.to_string id)) + | VernacStm (Command v) -> + return (keyword "Stm Command " ++ pr_vernac_body v) + | VernacStm (PGLast v) -> + return (keyword "Stm PGLast " ++ pr_vernac_body v) + + (* Proof management *) + | VernacAbortAll -> + return (keyword "Abort All") + | VernacRestart -> + return (keyword "Restart") + | VernacUnfocus -> + return (keyword "Unfocus") + | VernacUnfocused -> + return (keyword "Unfocused") + | VernacGoal c -> + return (keyword "Goal" ++ pr_lconstrarg c) + | VernacAbort id -> + return (keyword "Abort" ++ pr_opt pr_lident id) + | VernacUndo i -> + return ( + if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i + ) + | VernacUndoTo i -> + return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i) + | VernacBacktrack (i,j,k) -> + return (keyword "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k]) + | VernacFocus i -> + return (keyword "Focus" ++ pr_opt int i) + | VernacShow s -> + let pr_goal_reference = function + | OpenSubgoals -> mt () + | NthGoal n -> spc () ++ int n + | GoalId 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 + | ShowProof -> keyword "Show Proof" + | ShowNode -> keyword "Show Node" + | ShowScript -> keyword "Show Script" + | ShowExistentials -> keyword "Show Existentials" + | ShowUniverses -> keyword "Show Universes" + | ShowTree -> keyword "Show Tree" + | ShowProofNames -> keyword "Show Conjectures" + | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") + | ShowMatch id -> keyword "Show Match " ++ pr_lident id + | ShowThesis -> keyword "Show Thesis" in - keyword cmd ++ pr_opt str fopt - | PrintName qid -> - keyword "Print" ++ spc() ++ pr_smart_global qid - | PrintModuleType qid -> - keyword "Print Module Type" ++ spc() ++ pr_reference qid - | PrintModule qid -> - keyword "Print Module" ++ spc() ++ pr_reference qid - | PrintInspect n -> - keyword "Inspect" ++ spc() ++ int n - | PrintScopes -> - keyword "Print Scopes" - | PrintScope s -> - keyword "Print Scope" ++ spc() ++ str s - | PrintVisibility s -> - keyword "Print Visibility" ++ pr_opt str s - | PrintAbout (qid,gopt) -> - pr_opt (fun g -> int g ++ str ":"++ spc()) gopt - ++ keyword "About" ++ spc() ++ pr_smart_global qid - | PrintImplicit qid -> - keyword "Print Implicit" ++ spc() ++ pr_smart_global qid - (* spiwack: command printing all the axioms and section variables used in a - term *) - | PrintAssumptions (b, t, qid) -> - let cmd = match b, t with - | true, true -> "Print All Dependencies" - | true, false -> "Print Opaque Dependencies" - | false, true -> "Print Transparent Dependencies" - | false, false -> "Print Assumptions" + return (pr_showable s) + | VernacCheckGuard -> + return (keyword "Guarded") + + (* Resetting *) + | VernacResetName id -> + return (keyword "Reset" ++ spc() ++ pr_lident id) + | VernacResetInitial -> + return (keyword "Reset Initial") + | VernacBack i -> + return ( + if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i + ) + | VernacBackTo i -> + return (keyword "BackTo" ++ pr_intarg i) + + (* State management *) + | VernacWriteState s -> + return (keyword "Write State" ++ spc () ++ qs s) + | VernacRestoreState s -> + return (keyword "Restore State" ++ spc() ++ qs s) + + (* Control *) + | VernacLoad (f,s) -> + return ( + keyword "Load" + ++ if f then + (spc() ++ keyword "Verbose" ++ spc()) + else + spc() ++ qs s + ) + | VernacTime (_,v) -> + return (keyword "Time" ++ spc() ++ pr_vernac_body v) + | VernacRedirect (s, (_,v)) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_body v) + | VernacTimeout(n,v) -> + return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v) + | VernacFail v -> + return (keyword "Fail" ++ spc() ++ pr_vernac_body v) + | VernacError _ -> + return (keyword "No-parsing-rule for VernacError") + + (* 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 - keyword cmd ++ spc() ++ pr_smart_global qid - | PrintNamespace dp -> - keyword "Print Namespace" ++ pr_dirpath dp - | PrintStrategy None -> - keyword "Print Strategies" - | PrintStrategy (Some qid) -> - keyword "Print Strategy" ++ pr_smart_global qid - in + return ( + keyword "Arguments Scope" + ++ spc() ++ pr_smart_global q + ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" + ) + | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *) + return ( + hov 0 (hov 0 (keyword "Infix " + ++ qs s ++ str " :=" ++ pr_constrarg q) ++ + pr_syntax_modifiers mv ++ + (match sn with + | None -> mt() + | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) + ) + | VernacNotation (_,c,((_,s),l),opt) -> + return ( + hov 2 (keyword "Notation" ++ spc() ++ qs s ++ + str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++ + (match opt with + | None -> mt() + | Some sc -> str" :" ++ spc() ++ str sc)) + ) + | VernacSyntaxExtension (_,(s,l)) -> + return ( + keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ + pr_syntax_modifiers l + ) + | VernacNotationAddFormat(s,k,v) -> + return ( + keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v + ) - let pr_using e = str (Proof_using.to_string e) in - - let rec pr_vernac v = - let return = Taggers.tag_vernac v in - match v with - | VernacPolymorphic (poly, v) -> - let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in - return (s ++ pr_vernac v) - | VernacProgram v -> - return (keyword "Program" ++ spc() ++ pr_vernac v) - | VernacLocal (local, v) -> - return (pr_locality local ++ spc() ++ pr_vernac v) - - (* Stm *) - | VernacStm JoinDocument -> - return (keyword "Stm JoinDocument") - | VernacStm PrintDag -> - return (keyword "Stm PrintDag") - | VernacStm Finish -> - return (keyword "Stm Finish") - | VernacStm Wait -> - return (keyword "Stm Wait") - | VernacStm (Observe id) -> - return (keyword "Stm Observe " ++ str(Stateid.to_string id)) - | VernacStm (Command v) -> - return (keyword "Stm Command " ++ pr_vernac v) - | VernacStm (PGLast v) -> - return (keyword "Stm PGLast " ++ pr_vernac v) - - (* Proof management *) - | VernacAbortAll -> - return (keyword "Abort All") - | VernacRestart -> - return (keyword "Restart") - | VernacUnfocus -> - return (keyword "Unfocus") - | VernacUnfocused -> - return (keyword "Unfocused") - | VernacGoal c -> - return (keyword "Goal" ++ pr_lconstrarg c) - | VernacAbort id -> - return (keyword "Abort" ++ pr_opt pr_lident id) - | VernacUndo i -> - return ( - if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i - ) - | VernacUndoTo i -> - return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i) - | VernacBacktrack (i,j,k) -> - return (keyword "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k]) - | VernacFocus i -> - return (keyword "Focus" ++ pr_opt int i) - | VernacShow s -> - let pr_goal_reference = function - | OpenSubgoals -> mt () - | NthGoal n -> spc () ++ int n - | GoalId 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 - | ShowProof -> keyword "Show Proof" - | ShowNode -> keyword "Show Node" - | ShowScript -> keyword "Show Script" - | ShowExistentials -> keyword "Show Existentials" - | ShowUniverses -> keyword "Show Universes" - | ShowTree -> keyword "Show Tree" - | ShowProofNames -> keyword "Show Conjectures" - | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") - | ShowMatch id -> keyword "Show Match " ++ pr_lident id - | ShowThesis -> keyword "Show Thesis" - in - return (pr_showable s) - | VernacCheckGuard -> - return (keyword "Guarded") - - (* Resetting *) - | VernacResetName id -> - return (keyword "Reset" ++ spc() ++ pr_lident id) - | VernacResetInitial -> - return (keyword "Reset Initial") - | VernacBack i -> - return ( - if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i - ) - | VernacBackTo i -> - return (keyword "BackTo" ++ pr_intarg i) - - (* State management *) - | VernacWriteState s -> - return (keyword "Write State" ++ spc () ++ qs s) - | VernacRestoreState s -> - return (keyword "Restore State" ++ spc() ++ qs s) - - (* Control *) - | VernacLoad (f,s) -> - return ( - keyword "Load" - ++ if f then - (spc() ++ keyword "Verbose" ++ spc()) - else - spc() ++ qs s - ) - | VernacTime v -> - return (keyword "Time" ++ spc() ++ pr_vernac_list v) - | VernacRedirect (s, v) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v) - | VernacTimeout(n,v) -> - return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v) - | VernacFail v -> - return (keyword "Fail" ++ spc() ++ pr_vernac v) - | VernacError _ -> - return (keyword "No-parsing-rule for VernacError") - - (* Syntax *) - | VernacTacticNotation (n,r,e) -> - return (pr_grammar_tactic_rule n ("",r,e)) - | VernacOpenCloseScope (_,(opening,sc)) -> - return ( - keyword (if opening then "Open " else "Close ") ++ - keyword "Scope" ++ spc() ++ str sc - ) - | VernacDelimiters (sc,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_smart_global cll - ) - | VernacArgumentsScope (q,scl) -> - let pr_opt_scope = function - | None -> str"_" - | Some sc -> str sc - in - return ( - keyword "Arguments Scope" - ++ spc() ++ pr_smart_global q - ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - ) - | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *) - return ( - hov 0 (hov 0 (keyword "Infix " - ++ qs s ++ str " :=" ++ pr_constrarg q) ++ - pr_syntax_modifiers mv ++ - (match sn with - | None -> mt() - | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) - ) - | VernacNotation (_,c,((_,s),l),opt) -> - let ps = - let n = String.length s in - if n > 2 && s.[0] == '\'' && s.[n-1] == '\'' - then - let s' = String.sub s 1 (n-2) in - if String.contains s' '\'' then qs s else str s' - else qs s - in - return ( - hov 2 (keyword "Notation" ++ spc() ++ ps ++ - str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++ - (match opt with - | None -> mt() - | Some sc -> str" :" ++ spc() ++ str sc)) - ) - | VernacSyntaxExtension (_,(s,l)) -> - return ( - keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ - pr_syntax_modifiers l - ) - | VernacNotationAddFormat(s,k,v) -> - return ( - keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v - ) - - (* Gallina *) - | VernacDefinition (d,id,b) -> (* A verifier... *) - let pr_def_token (l,dk) = - let l = match l with Some x -> x | None -> Decl_kinds.Global in - keyword (Kindops.string_of_definition_kind (l,false,dk)) - in - let pr_reduce = function - | None -> mt() - | Some r -> - keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++ - keyword " in" ++ spc() - in - let pr_def_body = function - | DefineBody (bl,red,body,d) -> - let ty = match d with - | None -> mt() - | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty - in - (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) - | ProveBody (bl,t) -> - (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in - let (binds,typ,c) = pr_def_body b in - return ( - hov 2 ( - pr_def_token d ++ spc() - ++ pr_plident 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 None -> keyword "Qed" - | Opaque (Some l) -> - keyword "Qed" ++ spc() ++ str"export" ++ - prlist_with_sep (fun () -> str", ") pr_lident l) - | Some (id,th) -> (match th with - | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id - | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id) + (* Gallina *) + | VernacDefinition (d,id,b) -> (* A verifier... *) + let pr_def_token (l,dk) = + let l = match l with Some x -> x | None -> Decl_kinds.Global in + keyword (Kindops.string_of_definition_kind (l,false,dk)) + in + let pr_reduce = function + | None -> mt() + | Some r -> + keyword "Eval" ++ spc() ++ + pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++ + keyword " in" ++ spc() + in + let pr_def_body = function + | DefineBody (bl,red,body,d) -> + let ty = match d with + | None -> mt() + | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty + in + (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) + | ProveBody (bl,t) -> + (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in + let (binds,typ,c) = pr_def_body b in + return ( + hov 2 ( + pr_def_token d ++ spc() + ++ pr_plident 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 None -> keyword "Qed" + | Opaque (Some l) -> + keyword "Qed" ++ spc() ++ str"export" ++ + prlist_with_sep (fun () -> str", ") pr_lident l) + | Some (id,th) -> (match th with + | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id + | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id) + ) + | VernacExactProof c -> + return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) + | VernacAssumption (stre,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_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 ++ + pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) + | VernacInductive (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_file pr_spc_lconstr c) + in + let pr_constructor_list b l = match l with + | Constructors [] -> mt() + | Constructors l -> + let fst_sep = match l with [_] -> " " | _ -> " | " in + pr_com_at (begin_of_inductive l) ++ + fnl() ++ str fst_sep ++ + prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l + | RecordDecl (c,fs) -> + pr_record_decl b c fs + in + let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) = + hov 0 ( + str key ++ spc() ++ + (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++ + 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 + match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class _ -> "Class" | Variant -> "Variant" + in + return ( + hov 1 (pr_oneind key (List.hd l)) ++ + (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) + ) + + | VernacFixpoint (local, recs) -> + let local = match local with + | Some Discharge -> "Let " + | Some Local -> "Local " + | None | Some Global -> "" + in + return ( + hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ + prlist_with_sep (fun _ -> fnl () ++ keyword "with" + ++ spc ()) pr_rec_definition recs) ) - | VernacExactProof c -> - return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) - | VernacAssumption (stre,_,l) -> - let n = List.length (List.flatten (List.map fst (List.map snd l))) in - 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" " ++ - (if coe then str":>" else str":") ++ - pr_spc_lconstr c) - in - let pr_constructor_list b l = match l with - | Constructors [] -> mt() - | Constructors l -> - let fst_sep = match l with [_] -> " " | _ -> " | " in - pr_com_at (begin_of_inductive l) ++ - fnl() ++ str fst_sep ++ - prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l - | RecordDecl (c,fs) -> - pr_record_decl b c fs - in - let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) = - hov 0 ( - str key ++ spc() ++ - (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 ++ - prlist (pr_decl_notation pr_constr) ntn - in - let key = - let (_,_,_,k,_),_ = List.hd l in - match k with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" - in - return ( - hov 1 (pr_oneind key (List.hd l)) ++ - (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) - ) - - | VernacFixpoint (local, recs) -> - let local = match local with - | Some Discharge -> "Let " - | Some Local -> "Local " - | None | Some Global -> "" - in - let pr_onerec = function - | (((loc,id),pl),ro,bl,type_,def),ntn -> - let annot = pr_guard_annot pr_lconstr_expr bl ro in - 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 - in - return ( - hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ - prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs) - ) - - | VernacCoFixpoint (local, corecs) -> - let local = match local with - | Some Discharge -> keyword "Let" ++ spc () - | Some Local -> keyword "Local" ++ spc () - | None | Some Global -> str "" - in - let pr_onecorec ((((loc,id),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 - in - return ( - hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) - ) - | VernacScheme l -> - return ( - hov 2 (keyword "Scheme" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l) - ) - | VernacCombinedScheme (id, l) -> - return ( - hov 2 (keyword "Combined Scheme" ++ spc() ++ - pr_lident id ++ spc() ++ keyword "from" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) - ) - | VernacUniverse v -> - return ( - hov 2 (keyword "Universe" ++ spc () ++ - prlist_with_sep (fun _ -> str",") pr_lident v) - ) - | VernacConstraint v -> - let pr_uconstraint (l, d, r) = - pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r - in - return ( - hov 2 (keyword "Constraint" ++ spc () ++ - prlist_with_sep (fun _ -> str",") pr_uconstraint v) - ) - - (* Gallina extensions *) - | VernacBeginSection id -> - return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id)) - | VernacEndSegment id -> - return (hov 2 (keyword "End" ++ spc() ++ pr_lident id)) - | VernacNameSectionHypSet (id,set) -> - return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++ - str ":="++spc()++pr_using set)) - | VernacRequire (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, pri) -> - return ( - hov 1 ( - (if abst then keyword "Declare" ++ spc () else mt ()) ++ - keyword "Instance" ++ - (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 ++ - (match props with - | Some (_,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p - | None -> mt())) - ) - - | VernacContext l -> - return ( - hov 1 ( - keyword "Context" ++ spc () ++ pr_and_type_binders_arg l) - ) - - | VernacDeclareInstances (ids, pri) -> - return ( - hov 1 (keyword "Existing" ++ spc () ++ - keyword(String.plural (List.length ids) "Instance") ++ - spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri) - ) - - | VernacDeclareClass id -> - return ( - hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id) - ) - - (* Modules and Module Types *) - | VernacDefineModule (export,m,bl,tys,bd) -> - let b = pr_module_binders bl pr_lconstr in - return ( - hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++ - pr_lident m ++ b ++ - pr_of_module_type pr_lconstr tys ++ - (if List.is_empty bd then mt () else str ":= ") ++ - prlist_with_sep (fun () -> str " <+ ") - (pr_module_ast_inl true pr_lconstr) bd) - ) - | VernacDeclareModule (export,id,bl,m1) -> - let b = pr_module_binders bl pr_lconstr in - return ( - hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++ - pr_lident id ++ b ++ - pr_module_ast_inl true pr_lconstr m1) - ) - | VernacDeclareModuleType (id,bl,tyl,m) -> - let b = pr_module_binders bl pr_lconstr in - let pr_mt = pr_module_ast_inl true pr_lconstr in - return ( - hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++ - prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++ - (if List.is_empty m then mt () else str ":= ") ++ - prlist_with_sep (fun () -> str " <+ ") pr_mt m) - ) - | VernacInclude (mexprs) -> - let pr_m = pr_module_ast_inl false pr_lconstr in - return ( - hov 2 (keyword "Include" ++ spc() ++ - prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) - ) - (* Solving *) - | VernacSolve (i,info,tac,deftac) -> - let pr_goal_selector = function - | SelectNth i -> int i ++ str":" - | SelectId id -> pr_id id ++ str":" - | SelectAll -> str"all" ++ str":" - | SelectAllParallel -> str"par" + + | VernacCoFixpoint (local, corecs) -> + let local = match local with + | Some Discharge -> keyword "Let" ++ spc () + | Some Local -> keyword "Local" ++ spc () + | None | Some Global -> str "" in - let pr_info = - match info with - | None -> mt () - | Some i -> str"Info"++spc()++int i++spc() + 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 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 ()) + hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) + ) + | VernacScheme l -> + return ( + hov 2 (keyword "Scheme" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l) + ) + | VernacCombinedScheme (id, l) -> + return ( + hov 2 (keyword "Combined Scheme" ++ spc() ++ + pr_lident id ++ spc() ++ keyword "from" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) + ) + | VernacUniverse v -> + return ( + hov 2 (keyword "Universe" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_lident v) + ) + | VernacConstraint v -> + let pr_uconstraint (l, d, r) = + pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r + in + return ( + hov 2 (keyword "Constraint" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_uconstraint v) + ) + + (* Gallina extensions *) + | VernacBeginSection id -> + return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id)) + | VernacEndSegment id -> + return (hov 2 (keyword "End" ++ spc() ++ pr_lident id)) + | VernacNameSectionHypSet (id,set) -> + return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++ + str ":="++spc()++pr_using set)) + | VernacRequire (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, pri) -> + return ( + hov 1 ( + (if abst then keyword "Declare" ++ spc () else mt ()) ++ + keyword "Instance" ++ + (match instid with + | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc () + | (_, Anonymous), _ -> mt ()) ++ + pr_and_type_binders_arg sup ++ + str":" ++ spc () ++ + (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ + pr_constr cl ++ pr_priority pri ++ + (match props with + | Some (true,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" ++ spc () ++ pr_and_type_binders_arg l) + ) + + | VernacDeclareInstances (ids, pri) -> + return ( + hov 1 (keyword "Existing" ++ spc () ++ + keyword(String.plural (List.length ids) "Instance") ++ + spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri) + ) + + | VernacDeclareClass id -> + return ( + hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id) + ) + + (* Modules and Module Types *) + | VernacDefineModule (export,m,bl,tys,bd) -> + let b = pr_module_binders bl pr_lconstr in + return ( + hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++ + pr_lident m ++ b ++ + pr_of_module_type pr_lconstr tys ++ + (if List.is_empty bd then mt () else str ":= ") ++ + prlist_with_sep (fun () -> str " <+") + (pr_module_ast_inl true pr_lconstr) bd) + ) + | VernacDeclareModule (export,id,bl,m1) -> + let b = pr_module_binders bl pr_lconstr in + return ( + hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++ + pr_lident id ++ b ++ 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() ++ pr_dirpath dir)) + ) + | VernacRemoveLoadPath s -> + return (keyword "Remove LoadPath" ++ qs s) + | VernacAddMLPath (fl,s) -> + return ( + keyword "Add" + ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) + ++ keyword "ML Path" + ++ qs s + ) + | VernacDeclareMLModule (l) -> + return ( + hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l) + ) + | VernacChdir s -> + return (keyword "Cd" ++ pr_opt qs s) + + (* Commands *) + | VernacCreateHintDb (dbname,b) -> + return ( + hov 1 (keyword "Create HintDb" ++ spc () ++ + str dbname ++ (if b then str" discriminated" else mt ())) + ) + | VernacRemoveHints (dbnames, ids) -> + return ( + hov 1 (keyword "Remove Hints" ++ spc () ++ + prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ + pr_opt_hintbases dbnames) + ) + | VernacHints (_, dbnames,h) -> + return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) + | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> + return ( + hov 2 + (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ + prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ + pr_syntax_modifiers + (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) + ) + | VernacDeclareImplicits (q,[]) -> + return ( + hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q) + ) + | VernacDeclareImplicits (q,impls) -> + return ( + hov 1 (keyword "Implicit Arguments" ++ spc () ++ + spc() ++ pr_smart_global q ++ spc() ++ + prlist_with_sep spc (fun imps -> + str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") + impls) + ) + | VernacArguments (q, impl, nargs, mods) -> + return ( + hov 2 ( + keyword "Arguments" ++ spc() ++ + pr_smart_global q ++ + let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in + let pr_if b x = if b then x else str "" in + let pr_br imp max x = match imp, max with + | true, false -> str "[" ++ x ++ str "]" + | true, true -> str "{" ++ x ++ str "}" + | _ -> x in + let rec aux n l = + match n, l with + | 0, l -> spc () ++ str"/" ++ aux ~-1 l + | _, [] -> mt() + | n, (id,k,s,imp,max) :: tl -> + spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ + aux (n-1) tl in + prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ + (if not (List.is_empty mods) then str" : " else str"") ++ + prlist_with_sep (fun () -> str", " ++ spc()) (function + | `ReductionDontExposeCase -> keyword "simpl nomatch" + | `ReductionNeverUnfold -> keyword "simpl never" + | `DefaultImplicits -> keyword "default implicits" + | `Rename -> keyword "rename" + | `Assert -> keyword "assert" + | `ExtraScopes -> keyword "extra scopes" + | `ClearImplicits -> keyword "clear implicits" + | `ClearScopes -> keyword "clear scopes") + mods) + ) + | VernacReserve bl -> + let n = List.length (List.flatten (List.map fst bl)) in + return ( + hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " ")) + ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl)) + ) + | VernacGeneralizable g -> + return ( + hov 1 (tag_keyword ( + str"Generalizable Variable" ++ + match g with + | None -> str "s none" + | Some [] -> str "s all" + | Some idl -> + str (if List.length idl > 1 then "s " else " ") ++ + prlist_with_sep spc pr_lident idl) + )) + | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k -> + return ( + hov 1 (keyword "Transparent" ++ + spc() ++ prlist_with_sep sep pr_smart_global l) + ) + | VernacSetOpacity(Conv_oracle.Opaque,l) -> + return ( + hov 1 (keyword "Opaque" ++ + spc() ++ prlist_with_sep sep pr_smart_global l) + ) + | VernacSetOpacity _ -> + return ( + 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 (na) -> + return ( + hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None) + ) + | VernacSetOption (na,v) -> + return ( + hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v) + ) + | VernacAddOption (na,l) -> + return ( + hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacRemoveOption (na,l) -> + return ( + hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacMemOption (na,l) -> + return ( + hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l)) + ) + | VernacPrintOption na -> + return ( + hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None) + ) + | VernacCheckMayEval (r,io,c) -> + let pr_mayeval r c = match r with + | Some r0 -> + hov 2 (keyword "Eval" ++ spc() ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++ + spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) + | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) + in + let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in + return (pr_i ++ pr_mayeval r c) + | VernacGlobalCheck c -> + return (hov 2 (keyword "Type" ++ pr_constrarg c)) + | VernacDeclareReduction (s,r) -> + return ( + keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r + ) + | VernacPrint p -> + return (pr_printable p) + | VernacSearch (sea,g,sea_r) -> + return (pr_search sea g sea_r pr_constr_pattern_expr) + | VernacLocate loc -> + let pr_locate =function + | LocateAny qid -> pr_smart_global qid + | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid + | LocateFile f -> keyword "File" ++ spc() ++ qs f + | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid + | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid + | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid + in + return (keyword "Locate" ++ spc() ++ pr_locate loc) + | VernacRegister (id, RegisterInline) -> + return ( + hov 2 + (keyword "Register Inline" ++ spc() ++ pr_lident id) + ) + | VernacComments l -> + return ( + hov 2 + (keyword "Comments" ++ spc() + ++ prlist_with_sep sep (pr_comment pr_constr) l) + ) + + (* Toplevel control *) + | VernacToplevelControl exn -> + return (pr_topcmd exn) + + (* For extension *) + | VernacExtend (s,c) -> + return (pr_extend s c) + | VernacProof (None, None) -> + return (keyword "Proof") + | VernacProof (None, Some e) -> + return (keyword "Proof " ++ spc () ++ + keyword "using" ++ spc() ++ pr_using e) + | VernacProof (Some te, None) -> + return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te) + | VernacProof (Some te, Some e) -> + return ( + keyword "Proof" ++ spc () ++ + keyword "using" ++ spc() ++ pr_using e ++ spc() ++ + keyword "with" ++ spc() ++pr_raw_tactic te ) - | VernacSolveExistential (i,c) -> - return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) - - (* Auxiliary file and library management *) - | VernacAddLoadPath (fl,s,d) -> - return ( - hov 2 - (keyword "Add" ++ - (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ - keyword "LoadPath" ++ spc() ++ qs s ++ - (match d with - | None -> mt() - | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir)) - ) - | VernacRemoveLoadPath s -> - return (keyword "Remove LoadPath" ++ qs s) - | VernacAddMLPath (fl,s) -> - return ( - keyword "Add" - ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) - ++ keyword "ML Path" - ++ qs s - ) - | VernacDeclareMLModule (l) -> - return ( - hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l) - ) - | VernacChdir s -> - return (keyword "Cd" ++ pr_opt qs s) - - (* Commands *) - | VernacDeclareTacticDefinition (rc,l) -> - let pr_tac_body (id, redef, body) = - let idl, body = - match body with - | Tacexpr.TacFun (idl,b) -> idl,b - | _ -> [], body in - pr_ltac_ref id ++ - prlist (function None -> str " _" - | Some id -> spc () ++ pr_id id) idl - ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ - pr_raw_tactic body - in - return ( - hov 1 - (keyword "Ltac" ++ spc () ++ - prlist_with_sep (fun () -> - fnl() ++ keyword "with" ++ spc ()) pr_tac_body l) - ) - | VernacCreateHintDb (dbname,b) -> - return ( - hov 1 (keyword "Create HintDb" ++ spc () ++ - str dbname ++ (if b then str" discriminated" else mt ())) - ) - | VernacRemoveHints (dbnames, ids) -> - return ( - hov 1 (keyword "Remove Hints" ++ spc () ++ - prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ - pr_opt_hintbases dbnames) - ) - | VernacHints (_, dbnames,h) -> - return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> - return ( - hov 2 - (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ - prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++ - pr_syntax_modifiers - (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) - ) - | VernacDeclareImplicits (q,[]) -> - return ( - hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q) - ) - | VernacDeclareImplicits (q,impls) -> - return ( - hov 1 (keyword "Implicit Arguments" ++ spc () ++ - spc() ++ pr_smart_global q ++ spc() ++ - prlist_with_sep spc (fun imps -> - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") - impls) - ) - | VernacArguments (q, impl, nargs, mods) -> - return ( - hov 2 ( - keyword "Arguments" ++ spc() ++ - pr_smart_global q ++ - let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in - let pr_if b x = if b then x else str "" in - let pr_br imp max x = match imp, max with - | true, false -> str "[" ++ x ++ str "]" - | true, true -> str "{" ++ x ++ str "}" - | _ -> x in - let rec aux n l = - match n, l with - | 0, l -> spc () ++ str"/" ++ aux ~-1 l - | _, [] -> mt() - | n, (id,k,s,imp,max) :: tl -> - spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ - aux (n-1) tl in - prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ - if not (List.is_empty mods) then str" : " else str"" ++ - prlist_with_sep (fun () -> str", " ++ spc()) (function - | `ReductionDontExposeCase -> keyword "simpl nomatch" - | `ReductionNeverUnfold -> keyword "simpl never" - | `DefaultImplicits -> keyword "default implicits" - | `Rename -> keyword "rename" - | `Assert -> keyword "assert" - | `ExtraScopes -> keyword "extra scopes" - | `ClearImplicits -> keyword "clear implicits" - | `ClearScopes -> keyword "clear scopes") - mods) - ) - | VernacReserve bl -> - let n = List.length (List.flatten (List.map fst bl)) in - return ( - hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " ")) - ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl)) - ) - | VernacGeneralizable g -> - return ( - hov 1 (tag_keyword ( - str"Generalizable Variable" ++ - match g with - | None -> str "s none" - | Some [] -> str "s all" - | Some idl -> - str (if List.length idl > 1 then "s " else " ") ++ - prlist_with_sep spc pr_lident idl) - )) - | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k -> - return ( - hov 1 (keyword "Transparent" ++ - spc() ++ prlist_with_sep sep pr_smart_global l) - ) - | VernacSetOpacity(Conv_oracle.Opaque,l) -> - return ( - hov 1 (keyword "Opaque" ++ - spc() ++ prlist_with_sep sep pr_smart_global l) - ) - | VernacSetOpacity _ -> - return ( - Errors.anomaly (keyword "VernacSetOpacity used to set something else") - ) - | VernacSetStrategy l -> - let pr_lev = function - | Conv_oracle.Opaque -> keyword "opaque" - | Conv_oracle.Expand -> keyword "expand" - | l when Conv_oracle.is_transparent l -> keyword "transparent" - | Conv_oracle.Level n -> int n - in - let pr_line (l,q) = - hov 2 (pr_lev l ++ spc() ++ - str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") - in - return ( - hov 1 (keyword "Strategy" ++ spc() ++ - hv 0 (prlist_with_sep sep pr_line l)) - ) - | VernacUnsetOption (na) -> - return ( - hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None) - ) - | VernacSetOption (na,v) -> - return ( - hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v) - ) - | VernacAddOption (na,l) -> - return ( - hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l)) - ) - | VernacRemoveOption (na,l) -> - return ( - hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l)) - ) - | VernacMemOption (na,l) -> - return ( - hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l)) - ) - | VernacPrintOption na -> - return ( - hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None) - ) - | VernacCheckMayEval (r,io,c) -> - let pr_mayeval r c = match r with - | Some r0 -> - hov 2 (keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++ - spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) - | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) - in - let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in - return (pr_i ++ pr_mayeval r c) - | VernacGlobalCheck c -> - return (hov 2 (keyword "Type" ++ pr_constrarg c)) - | VernacDeclareReduction (s,r) -> - return ( - keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r - ) - | VernacPrint p -> - return (pr_printable p) - | VernacSearch (sea,g,sea_r) -> - return (pr_search sea g sea_r pr_constr_pattern_expr) - | VernacLocate loc -> - let pr_locate =function - | LocateAny qid -> pr_smart_global qid - | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid - | LocateFile f -> keyword "File" ++ spc() ++ qs f - | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid - | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid - | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid - in - return (keyword "Locate" ++ spc() ++ pr_locate loc) - | VernacRegister (id, RegisterInline) -> - return ( - hov 2 - (keyword "Register Inline" ++ spc() ++ pr_lident id) - ) - | VernacComments l -> - return ( - hov 2 - (keyword "Comments" ++ spc() - ++ prlist_with_sep sep (pr_comment pr_constr) l) - ) - | VernacNop -> - mt() - - (* Toplevel control *) - | VernacToplevelControl exn -> - return (pr_topcmd exn) - - (* For extension *) - | VernacExtend (s,c) -> - return (pr_extend s c) - | VernacProof (None, None) -> - return (keyword "Proof") - | VernacProof (None, Some e) -> - return (keyword "Proof " ++ spc () ++ - keyword "using" ++ spc() ++ pr_using e) - | VernacProof (Some te, None) -> - return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te) - | VernacProof (Some te, Some e) -> - return ( - keyword "Proof" ++ spc () ++ - keyword "using" ++ spc() ++ pr_using e ++ spc() ++ - keyword "with" ++ spc() ++pr_raw_tactic te - ) - | VernacProofMode s -> - return (keyword "Proof Mode" ++ str s) - | VernacBullet b -> - return (begin match b with - | Dash n -> str (String.make n '-') - | Star n -> str (String.make n '*') - | Plus n -> str (String.make n '+') - end ++ spc()) - | VernacSubproof None -> - return (str "{") - | VernacSubproof (Some i) -> - return (keyword "BeginSubproof" ++ spc () ++ int i) - | VernacEndSubproof -> - return (str "}") - - and pr_vernac_list l = - hov 2 (str"[" ++ spc() ++ - prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l - ++ spc() ++ str"]") - - and pr_extend s cl = - let pr_arg a = - try pr_gen a - with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in - try - let rl = Egramml.get_extend_vernac_rule s in - let start,rl,cl = - match rl with - | Egramml.GramTerminal s :: rl -> str s, rl, cl - | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl - | [] -> anomaly (Pp.str "Empty entry") in - let (pp,_) = - List.fold_left - (fun (strm,args) pi -> - let pp,args = match pi with - | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args) - | Egramml.GramTerminal s -> (str s, args) in - (strm ++ spc() ++ pp), args) - (start,cl) rl in - hov 1 pp - with Not_found -> - hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") - - in pr_vernac - - let pr_vernac_body v = make_pr_vernac pr_constr_expr pr_lconstr_expr v - - let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end v - - let pr_vernac x = - try pr_vernac x - with e -> Errors.print e + | 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 (keyword "BeginSubproof" ++ spc () ++ int i) + | VernacEndSubproof -> + return (str "}") + + and 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 (fun x -> x) (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 v = + try pr_vernac_body v ++ sep_end v + with e -> CErrors.print e end diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli index 5d1c89332..5e5e4bcf4 100644 --- a/printing/ppvernacsig.mli +++ b/printing/ppvernacsig.mli @@ -8,6 +8,9 @@ module type Pp = sig + (** Prints a fixpoint body *) + val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds + (** Prints a vernac expression *) val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 4d9d40ae0..f71719cb9 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -11,7 +11,7 @@ *) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -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; @@ -132,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 @@ -168,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 -> @@ -212,15 +215,21 @@ let print_polymorphism ref = else "not universe polymorphic") ] else [] +let print_type_in_type ref = + let unsafe = Global.is_type_in_type ref in + if unsafe then + [ pr_global ref ++ str " relies on an unsafe universe hierarchy"] + else [] + let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt () - | Decl_kinds.BiFinite -> str " and has eta conversion" + | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" + | Decl_kinds.BiFinite -> str " with eta conversion" in - [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] + [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] - + let print_primitive ref = match ref with | IndRef ind -> @@ -241,6 +250,7 @@ let print_name_infos ref = else [] in print_polymorphism ref @ + print_type_in_type ref @ print_primitive ref @ type_info_for_implicit @ print_renames_list (mt()) renames @ @@ -440,11 +450,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 @@ -721,8 +733,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.") @@ -750,8 +762,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 6f3556adb..0eab15579 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -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 ac20eeb6f..28fd92659 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -48,7 +48,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 @@ -184,7 +184,7 @@ let safe_gen f env sigma c = let orig_extern_ref = Constrextern.get_extern_reference () in let extern_ref loc vars r = try orig_extern_ref loc vars r - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Libnames.Qualid (loc, qualid_of_global env r) in Constrextern.set_extern_reference extern_ref; @@ -192,7 +192,7 @@ let safe_gen f env sigma c = let p = f env sigma c in Constrextern.set_extern_reference orig_extern_ref; p - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Constrextern.set_extern_reference orig_extern_ref; str "??" @@ -260,16 +260,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 @@ -291,7 +294,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 ())) @@ -304,7 +307,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)) @@ -331,7 +334,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 ".")) @@ -414,7 +417,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)") @@ -467,25 +471,72 @@ let default_pr_subgoal n sigma = let pr_internal_existential_key ev = str (string_of_existential ev) -let emacs_print_dependent_evars sigma seeds = +let print_evar_constraints gl sigma cstrs = + let pr_env = + match gl with + | None -> fun e' -> pr_context_of e' sigma + | Some g -> + let env = Goal.V82.env sigma g in fun e' -> + begin + if Context.Named.equal (named_context env) (named_context e') then + if Context.Rel.equal (rel_context env) (rel_context e') then mt () + else pr_rel_context_of e' sigma ++ str " |-" ++ spc () + else pr_context_of e' sigma ++ str " |-" ++ spc () + end + in + let pr_evconstr (pbty,env,t1,t2) = + let t1 = Evarutil.nf_evar sigma t1 + and t2 = Evarutil.nf_evar sigma t2 in + str" " ++ + hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++ + str (match pbty with + | Reduction.CONV -> "==" + | Reduction.CUMUL -> "<=") ++ + spc () ++ pr_lconstr_env env sigma t2) + in + prlist_with_sep fnl pr_evconstr cstrs + +let should_print_dependent_evars = ref true + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Printing Dependent Evars Line"; + optkey = ["Printing";"Dependent";"Evars";"Line"]; + optread = (fun () -> !should_print_dependent_evars); + optwrite = (fun v -> should_print_dependent_evars := v) } + +let print_dependent_evars gl sigma seeds = + let constraints = + let _, cstrs = Evd.extract_all_conv_pbs sigma in + if List.is_empty cstrs then mt () + else fnl () ++ str (String.plural (List.length cstrs) "unification constraint") + ++ str":" ++ fnl () ++ hov 0 (print_evar_constraints gl sigma cstrs) + in let evars () = - let evars = Evarutil.gather_dependent_evars sigma seeds in - let evars = - Evar.Map.fold begin fun e i s -> - let e' = pr_internal_existential_key e in - match i with - | None -> s ++ str" " ++ e' ++ str " open," - | Some i -> - s ++ str " " ++ e' ++ str " using " ++ - Evar.Set.fold begin fun d s -> - pr_internal_existential_key d ++ str " " ++ s - end i (str ",") - end evars (str "") + if !should_print_dependent_evars then + let evars = Evarutil.gather_dependent_evars sigma seeds in + let evars = + Evar.Map.fold begin fun e i s -> + let e' = pr_internal_existential_key e in + match i with + | None -> s ++ str" " ++ e' ++ str " open," + | Some i -> + s ++ str " " ++ e' ++ str " using " ++ + Evar.Set.fold begin fun d s -> + pr_internal_existential_key d ++ str " " ++ s + end i (str ",") + end evars (str "") in fnl () ++ str "(dependent evars:" ++ evars ++ str ")" ++ fnl () + else + fnl () ++ + str "(dependent evars: (printing disabled) )" ++ fnl () in - delayed_emacs_cmd evars + constraints ++ delayed_emacs_cmd evars (* Print open subgoals. Checks for uninstantiated existential variables *) (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) @@ -544,7 +595,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals (* Side effect! This has to be made more robust *) let () = match close_cmd with - | Some cmd -> msg_info cmd + | Some cmd -> Feedback.msg_info cmd | None -> () in match goals with @@ -553,12 +604,12 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals let exl = Evarutil.non_instantiated sigma in if Evar.Map.is_empty exl then (str"No more subgoals." - ++ emacs_print_dependent_evars sigma seeds) + ++ print_dependent_evars None sigma seeds) else let pei = pr_evars_int sigma 1 exl in (str "No more subgoals, but there are non-instantiated existential variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + ++ print_dependent_evars None sigma seeds ++ fnl () ++ str "You can use Grab Existential Variables.") end | [g] when not !Flags.print_emacs && pr_first -> @@ -566,7 +617,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals v 0 ( str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg - ++ emacs_print_dependent_evars sigma seeds + ++ print_dependent_evars (Some g) sigma seeds ) | g1::rest -> let goals = print_multiple_goals g1 rest in @@ -578,7 +629,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals ++ pr_goal_tag g1 ++ pr_goal_name sigma g1 ++ cut () ++ goals - ++ emacs_print_dependent_evars sigma seeds + ++ print_dependent_evars (Some g1) sigma seeds ) (**********************************************************************) @@ -622,19 +673,19 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = begin match bgoals,shelf,given_up with | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals | [] , [] , _ -> - msg_info (str "No more subgoals, but there are some goals you gave up:"); + Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> - msg_info (str "All the remaining goals are on the shelf."); + Feedback.msg_info (str "All the remaining goals are on the shelf."); fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> 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 @@ -678,35 +729,10 @@ let pr_prim_rule = function (str"cut " ++ pr_constr t ++ str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | FixRule (f,n,[],_) -> - (str"fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others,j) -> - if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth - | [] -> mt () in - (str"fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - - | Cofix (f,[],_) -> - (str"cofix " ++ pr_id f) - - | Cofix (f,others,j) -> - if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) - | [] -> mt () in - (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) | Refine c -> str(if Termops.occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c - | Thin ids -> - (str"clear " ++ pr_sequence pr_id ids) - | Move (id1,id2) -> (str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) @@ -718,9 +744,14 @@ let prterm = pr_lconstr (* Printer function for sets of Assumptions.assumptions. It is used primarily by the Print Assumptions command. *) +type axiom = + | Constant of constant (* An axiom or a constant. *) + | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) + | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *) + type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of axiom * (Label.t * Context.Rel.t * types) list | Opaque of constant (* An opaque constant. *) | Transparent of constant @@ -728,19 +759,31 @@ type context_object = module OrderedContextObject = struct type t = context_object + + let compare_axiom x y = + match x,y with + | Constant k1 , Constant k2 -> + con_ord k1 k2 + | Positive m1 , Positive m2 -> + MutInd.CanOrd.compare m1 m2 + | Guarded k1 , Guarded k2 -> + con_ord k1 k2 + | _ , Constant _ -> 1 + | _ , Positive _ -> 1 + | _ -> -1 + let compare x y = - match x , y with - | Variable i1 , Variable i2 -> Id.compare i1 i2 - | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2 - | Opaque k1 , Opaque k2 -> con_ord k1 k2 - | Transparent k1 , Transparent k2 -> con_ord k1 k2 - | Axiom _ , Variable _ -> 1 - | Opaque _ , Variable _ - | Opaque _ , Axiom _ -> 1 - | Transparent _ , Variable _ - | Transparent _ , Axiom _ - | Transparent _ , Opaque _ -> 1 - | _ , _ -> -1 + match x , y with + | Variable i1 , Variable i2 -> Id.compare i1 i2 + | Variable _ , _ -> -1 + | _ , Variable _ -> 1 + | Axiom (k1,_) , Axiom (k2, _) -> compare_axiom k1 k2 + | Axiom _ , _ -> -1 + | _ , Axiom _ -> 1 + | Opaque k1 , Opaque k2 -> con_ord k1 k2 + | Opaque _ , _ -> -1 + | _ , Opaque _ -> 1 + | Transparent k1 , Transparent k2 -> con_ord k1 k2 end module ContextObjectSet = Set.Make (OrderedContextObject) @@ -748,7 +791,7 @@ module ContextObjectMap = Map.Make (OrderedContextObject) let pr_assumptionset env s = if ContextObjectMap.is_empty s && - engagement env = (PredicativeSet, StratifiedType) then + engagement env = PredicativeSet then str "Closed under the global context" else let safe_pr_constant env kn = @@ -759,28 +802,37 @@ let pr_assumptionset env s = in let safe_pr_ltype typ = try str " : " ++ pr_ltype typ - with e when Errors.noncritical e -> mt () + with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = let sigma, env = get_current_context () in let env = Environ.push_rel_context rctx env in try str " " ++ pr_ltype_env env sigma typ - with e when Errors.noncritical e -> mt () + with e when CErrors.noncritical e -> mt () + in + let pr_axiom env ax typ = + match ax with + | Constant kn -> + safe_pr_constant env kn ++ safe_pr_ltype typ + | Positive m -> + hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + | Guarded kn -> + hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") in let fold t typ accu = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = 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 + | Axiom (axiom, []) -> + let ax = pr_axiom env axiom typ in (v, ax :: a, o, tr) - | Axiom (kn,l) -> - let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++ + | Axiom (axiom,l) -> + let ax = pr_axiom env axiom 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) @@ -833,4 +885,3 @@ let pr_polymorphic b = 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 3424c41dc..695ab33b2 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -10,7 +10,6 @@ open Pp open Names open Globnames open Term -open Context open Environ open Pattern open Evd @@ -109,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 @@ -162,12 +161,16 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *) (** Declarations for the "Print Assumption" command *) +type axiom = + | Constant of constant (* An axiom or a constant. *) + | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) + | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *) + type context_object = - | Variable of Id.t (** A section variable or a Let definition *) - (** An axiom and the type it inhabits (if an axiom of the empty type) *) - | Axiom of constant * (Label.t * Context.rel_context * types) list - | Opaque of constant (** An opaque constant. *) - | Transparent of constant (** A transparent constant *) + | Variable of Id.t (* A section variable or a Let definition *) + | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Opaque of constant (* An opaque constant. *) + | Transparent of constant module ContextObjectSet : Set.S with type elt = context_object module ContextObjectMap : CMap.ExtS diff --git a/printing/printing.mllib b/printing/printing.mllib index 652a34fa1..bc8f0750e 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -2,12 +2,8 @@ Genprint Pputils Ppannotation Ppconstr -Ppconstrsig Printer Pptactic -Pptacticsig Printmod Prettyp Ppvernac -Ppvernacsig -Richprinter diff --git a/printing/printmod.ml b/printing/printmod.ml index c154b0aaa..c939f54e8 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,7 +65,6 @@ let get_new_id locals id = (** Inductive declarations *) -open Termops open Reduction let print_params env sigma params = @@ -89,7 +88,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = 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 @@ -143,7 +142,7 @@ 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 @@ -255,7 +254,7 @@ let nametab_register_modparam mbid mtb = via a Declaremods function that converts back to module entries *) try Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (* Otherwise, we try to play with the nametab ourselves *) let mp = MPbound mbid in let dir = DirPath.make [MBId.to_id mbid] in @@ -263,7 +262,7 @@ 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 @@ -296,7 +295,7 @@ let print_body is_impl env mp (l,body) = try let env = Option.get env in pr_mutual_inductive_body env (MutInd.make2 mp l) mib - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> let keyword = let open Decl_kinds in match mib.mind_finite with @@ -423,7 +422,7 @@ let print_module with_body mp = try if !short then raise ShortPrinting; unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl () - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> unsafe_print_module None mp with_body me ++ fnl () let print_modtype kn = @@ -434,7 +433,7 @@ let print_modtype kn = (try if !short then raise ShortPrinting; print_signature' true (Some (Global.env ())) kn mtb.mod_type - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> print_signature' true None kn mtb.mod_type)) end diff --git a/printing/richprinter.ml b/printing/richprinter.ml deleted file mode 100644 index d95e19074..000000000 --- a/printing/richprinter.ml +++ /dev/null @@ -1,25 +0,0 @@ -open Richpp - -module RichppConstr = Ppconstr.Richpp -module RichppVernac = Ppvernac.Richpp -module RichppTactic = Pptactic.Richpp - -type rich_pp = - Ppannotation.t Richpp.located Xml_datatype.gxml - * Xml_datatype.xml - -let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag - -let make_richpp pr ast = - let rich_pp = - rich_pp get_annotations (pr ast) - in - let xml = Ppannotation.( - xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp - ) - in - (rich_pp, xml) - -let richpp_vernac = make_richpp RichppVernac.pr_vernac -let richpp_constr = make_richpp RichppConstr.pr_constr_expr -let richpp_tactic env = make_richpp (RichppTactic.pr_tactic env) diff --git a/printing/richprinter.mli b/printing/richprinter.mli deleted file mode 100644 index 261d22c4c..000000000 --- a/printing/richprinter.mli +++ /dev/null @@ -1,39 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <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 *) -(************************************************************************) - -(** This module provides an entry point to "rich" pretty-printers that - produce pretty-printing as done by {!Printer} but with additional - annotations represented as a semi-structured document. - - To understand what are these annotations and how they are represented - as standard XML attributes, please refer to {!Ppannotation}. - - In addition to these annotations, each node of the semi-structured - document contains a [startpos] and an [endpos] attribute that - relate this node to the raw pretty-printing. - Please refer to {!Richpp} for more details. *) - -(** A rich pretty-print is composed of: *) -type rich_pp = - - (** - a generalized semi-structured document whose attributes are - annotations ; *) - Ppannotation.t Richpp.located Xml_datatype.gxml - - (** - an XML document, representing annotations as usual textual - XML attributes. *) - * Xml_datatype.xml - -(** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *) -val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp - -(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *) -val richpp_constr : Constrexpr.constr_expr -> rich_pp - -(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *) -val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp |