From 297b0cb44bbe8ec7304ca635c566815167266d4a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Jun 2015 11:28:44 +0200 Subject: Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again. --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4e889e55f0..c4689c918d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -656,7 +656,7 @@ module Make | VernacBindScope (sc,cll) -> return ( keyword "Bind Scope" ++ spc () ++ str sc ++ - spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_smart_global cll + spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll ) | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function -- cgit v1.2.3 From 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 14 Sep 2015 18:35:48 +0200 Subject: Univs: Add universe binding lists to definitions ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. --- printing/ppvernac.ml | 32 ++++++++++++++++++++++---------- 1 file changed, 22 insertions(+), 10 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4e889e55f0..71dcd15cc7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -43,6 +43,12 @@ module Make else pr_id id + let pr_plident (lid, l) = + pr_lident lid ++ + (match l with + | Some l -> prlist_with_sep spc pr_lident l + | None -> mt()) + let string_of_fqid fqid = String.concat "." (List.map Id.to_string fqid) @@ -387,10 +393,16 @@ module Make hov 0 (prlist_with_sep sep pr_production_item pil ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) - let pr_statement head (id,(bl,c,guard)) = - assert (not (Option.is_empty id)); + let pr_univs pl = + match pl with + | None -> mt () + | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}" + + let pr_statement head (idpl,(bl,c,guard)) = + assert (not (Option.is_empty idpl)); + let id, pl = Option.get idpl in hov 2 - (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++ + (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ str":" ++ pr_spc_lconstr c) @@ -729,7 +741,7 @@ module Make return ( hov 2 ( pr_def_token d ++ spc() - ++ pr_lident id ++ binds ++ typ + ++ pr_plident id ++ binds ++ typ ++ (match c with | None -> mt() | Some cc -> str" :=" ++ spc() ++ cc)) @@ -781,10 +793,10 @@ module Make | RecordDecl (c,fs) -> pr_record_decl b c fs in - let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) = + let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) = hov 0 ( str key ++ spc() ++ - (if coe then str"> " else str"") ++ pr_lident id ++ + (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++ pr_and_type_binders_arg indpar ++ spc() ++ Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ str" :=") ++ pr_constructor_list k lc ++ @@ -808,9 +820,9 @@ module Make | None | Some Global -> "" in let pr_onerec = function - | ((loc,id),ro,bl,type_,def),ntn -> + | (((loc,id),pl),ro,bl,type_,def),ntn -> let annot = pr_guard_annot pr_lconstr_expr bl ro in - pr_id id ++ pr_binders_arg bl ++ annot + pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn @@ -826,8 +838,8 @@ module Make | Some Local -> keyword "Local" ++ spc () | None | Some Global -> str "" in - let pr_onecorec (((loc,id),bl,c,def),ntn) = - pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ + let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) = + pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ spc() ++ pr_lconstr_expr c ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn -- cgit v1.2.3 From 0c766b2e3b54d96713a79e40661653c5486822a8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 20 Sep 2015 01:23:26 +0200 Subject: Print Assumptions shows engagement. Seems to be morally required since we have the -type-in-type flag. --- printing/printer.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index 33b95c2f56..18e4902255 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -742,7 +742,8 @@ module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) let pr_assumptionset env s = - if ContextObjectMap.is_empty s then + if ContextObjectMap.is_empty s && + engagement env = (PredicativeSet, StratifiedType) then str "Closed under the global context" else let safe_pr_constant env kn = @@ -788,6 +789,16 @@ let pr_assumptionset env s = let (vars, axioms, opaque, trans) = ContextObjectMap.fold fold s ([], [], [], []) in + let theory = + if is_impredicative_set env then + [str "Set is impredicative"] + else [] + in + let theory = + if type_in_type env then + str "Type hierarchy is collapsed (logic is inconsistent)" :: theory + else theory + in let opt_list title = function | [] -> None | l -> @@ -801,6 +812,7 @@ let pr_assumptionset env s = opt_list (str "Section Variables:") vars; opt_list (str "Axioms:") axioms; opt_list (str "Opaque constants:") opaque; + opt_list (str "Theory:") theory; ] in prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums) -- cgit v1.2.3 From 92ee78086f1ca89646ac69a00256ff45fcaee22c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 5 Oct 2015 17:00:11 +0200 Subject: Univs: fix printing bug #3797. --- printing/printmod.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'printing') diff --git a/printing/printmod.ml b/printing/printmod.ml index a80bbb146a..53d0508c7f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -259,6 +259,10 @@ let print_body is_impl env mp (l,body) = | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> + let u = + if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + else Univ.Instance.empty + in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -268,14 +272,16 @@ let print_body is_impl env mp (l,body) = | Some env -> str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *) - (Typeops.type_of_constant_type env cb.const_type)) ++ + (Vars.subst_instance_constr u + (Typeops.type_of_constant_type env cb.const_type))) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l)) + Printer.pr_lconstr_env env Evd.empty + (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx cb.const_universes) + Printer.pr_universe_ctx (Univ.instantiate_univ_context cb.const_universes)) | SFBmind mib -> try let env = Option.get env in -- cgit v1.2.3 From d37aab528dca587127b9f9944e1521e4fc3d9cc7 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 7 Oct 2015 13:11:52 +0200 Subject: Univs: add Strict Universe Declaration option (on by default) This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option. --- printing/ppconstr.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 650b8f7262..ea705e335e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -140,8 +140,8 @@ end) = struct let pr_univ l = match l with - | [x] -> str x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")" + | [_,x] -> str x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")" let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" @@ -174,7 +174,7 @@ end) = struct tag_type (str "Set") | GType u -> (match u with - | Some u -> str u + | Some (_,u) -> str u | None -> tag_type (str "Type")) let pr_universe_instance l = -- cgit v1.2.3 From ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Oct 2015 14:11:19 +0200 Subject: Goptions: new value type: optional string These options can be set to a string value, but also unset. Internal data is of type string option. --- printing/ppvernac.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 71dcd15cc7..76f97fce1e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -166,6 +166,8 @@ module Make (* This should not happen because of the grammar *) | IntValue (Some n) -> spc() ++ int n | StringValue s -> spc() ++ str s + | StringOptValue None -> mt() + | StringOptValue (Some s) -> spc() ++ str s | BoolValue b -> mt() in pr_printoption a None ++ pr_opt_value b -- cgit v1.2.3 From 33d153a01f2814c6e5486c07257667254b91fa0c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 7 Oct 2015 15:08:27 +0200 Subject: Axioms now support the universe binding syntax. We artificially restrict the syntax though, because it is unclear of what the semantics of several axioms in a row is, in particular about the resolution of remaining evars. --- printing/ppvernac.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 76f97fce1e..00c276bdbe 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -356,6 +356,7 @@ module Make | l -> prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l + (* prlist_with_sep pr_semicolon (pr_params pr_c) *) @@ -774,11 +775,12 @@ module Make return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) | VernacAssumption (stre,_,l) -> let n = List.length (List.flatten (List.map fst (List.map snd l))) in - return ( - hov 2 - (pr_assumption_token (n > 1) stre ++ spc() ++ - pr_ne_params_list pr_lconstr_expr l) - ) + let pr_params (c, (xl, t)) = + hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++ + (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) + in + let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in + return (hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ assumptions)) | VernacInductive (p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ -- cgit v1.2.3 From 666568377cbe1c18ce479d32f6359aa61af6d553 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Oct 2015 16:36:53 +0200 Subject: Type delayed_open_constr is now monotonic. --- printing/pptactic.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index e8ccd29c8a..72d2eedcc3 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1437,6 +1437,9 @@ end) (** Registering *) +let run_delayed c = + Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma } + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in @@ -1447,7 +1450,7 @@ let () = 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) -- cgit v1.2.3 From 89be9efbf6dbd8a04fb8ccab4c9aa7a11b9a0f03 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 11:16:47 -0400 Subject: Printing of @{} instances for polymorphic references in Print and About. --- printing/prettyp.ml | 14 +++++++++++--- printing/printer.ml | 4 ++++ printing/printer.mli | 1 + printing/printmod.ml | 6 +++++- 4 files changed, 21 insertions(+), 4 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b8c5fd4cfc..7e625af0de 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,7 +73,11 @@ let print_ref reduce ref = in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in - hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ + let inst = + if Global.is_polymorphic ref then Printer.pr_universe_instance univs + else mt () + in + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype typ ++ Printer.pr_universe_ctx univs) (********************************) @@ -473,6 +477,10 @@ let print_typed_body (val_0,typ) = let ungeneralized_type_of_constant_type t = Typeops.type_of_constant_type (Global.env ()) t +let print_instance cb = + if cb.const_polymorphic then pr_universe_instance cb.const_universes + else mt() + let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in @@ -485,11 +493,11 @@ let print_constant with_values sep sp = match val_0 with | None -> str"*** [ " ++ - print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ + print_basename sp ++ print_instance cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ Printer.pr_universe_ctx univs | _ -> - print_basename sp ++ str sep ++ cut () ++ + print_basename sp ++ print_instance cb ++ str sep ++ cut () ++ (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ Printer.pr_universe_ctx univs) diff --git a/printing/printer.ml b/printing/printer.ml index 18e4902255..f4852b1089 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -825,3 +825,7 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () +let pr_universe_instance ctx = + let inst = Univ.UContext.instance ctx in + str"@{" ++ Univ.Instance.pr Univ.Level.pr inst ++ str"}" + diff --git a/printing/printer.mli b/printing/printer.mli index 5f56adbe6f..25a4aa166b 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -84,6 +84,7 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds +val pr_universe_instance : Univ.universe_context -> std_ppcmds val pr_universe_ctx : Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 53d0508c7f..8031de27d4 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -94,8 +94,12 @@ let print_one_inductive env mib ((_,i) as ind) = let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in + let inst = + if mib.mind_polymorphic then Printer.pr_universe_instance mib.mind_universes + else mt () + in hov 0 ( - pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++ + pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env Evd.empty params ++ str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes -- cgit v1.2.3 From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 12:36:20 -0400 Subject: Univs: local names handling. Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. --- printing/prettyp.ml | 38 ++++++++++++++++++++++++-------------- printing/printer.ml | 8 ++++---- printing/printer.mli | 4 ++-- printing/printmod.ml | 38 ++++++++++++++++++++++---------------- 4 files changed, 52 insertions(+), 36 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 7e625af0de..84649e6ebf 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,12 +73,15 @@ let print_ref reduce ref = in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in + let env = Global.env () in + let bl = Universes.universe_binders_of_global ref in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let inst = - if Global.is_polymorphic ref then Printer.pr_universe_instance univs + if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () in - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype typ ++ - Printer.pr_universe_ctx univs) + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ + Printer.pr_universe_ctx sigma univs) (********************************) (** Printing implicit arguments *) @@ -467,18 +470,19 @@ let gallina_print_section_variable id = print_named_decl id ++ with_line_skip (print_name_infos (VarRef id)) -let print_body = function - | Some c -> pr_lconstr c +let print_body env evd = function + | Some c -> pr_lconstr_env env evd c | None -> (str"") -let print_typed_body (val_0,typ) = - (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ) +let print_typed_body env evd (val_0,typ) = + (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) let ungeneralized_type_of_constant_type t = Typeops.type_of_constant_type (Global.env ()) t -let print_instance cb = - if cb.const_polymorphic then pr_universe_instance cb.const_universes +let print_instance sigma cb = + if cb.const_polymorphic then + pr_universe_instance sigma cb.const_universes else mt() let print_constant with_values sep sp = @@ -489,17 +493,23 @@ let print_constant with_values sep sp = let univs = Univ.instantiate_univ_context (Global.universes_of_constant_body cb) in + let ctx = + Evd.evar_universe_context_of_binders + (Universes.universe_binders_of_global (ConstRef sp)) + in + let env = Global.env () and sigma = Evd.from_ctx ctx in + let pr_ltype = pr_ltype_env env sigma in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> str"*** [ " ++ - print_basename sp ++ print_instance cb ++ str " : " ++ cut () ++ pr_ltype typ ++ + print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_universe_ctx univs + Printer.pr_universe_ctx sigma univs | _ -> - print_basename sp ++ print_instance cb ++ str sep ++ cut () ++ - (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ - Printer.pr_universe_ctx univs) + print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ + (if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++ + Printer.pr_universe_ctx sigma univs) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ diff --git a/printing/printer.ml b/printing/printer.ml index f4852b1089..202b4f2bc7 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -208,10 +208,10 @@ let safe_pr_constr t = let (sigma, env) = get_current_context () in safe_pr_constr_env env sigma t -let pr_universe_ctx c = +let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context Universes.pr_with_global_universes c)) c + (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c else mt() @@ -825,7 +825,7 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () -let pr_universe_instance ctx = +let pr_universe_instance evd ctx = let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr Univ.Level.pr inst ++ str"}" + str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}" diff --git a/printing/printer.mli b/printing/printer.mli index 25a4aa166b..0a44e4f103 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -84,8 +84,8 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds -val pr_universe_instance : Univ.universe_context -> std_ppcmds -val pr_universe_ctx : Univ.universe_context -> std_ppcmds +val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds +val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 8031de27d4..1d275c1aa6 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -72,10 +72,10 @@ let print_params env sigma params = if List.is_empty params then mt () else Printer.pr_rel_context env sigma params ++ brk(1,2) -let print_constructors envpar names types = +let print_constructors envpar sigma names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c) + (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c) (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) @@ -83,7 +83,7 @@ let print_constructors envpar names types = let build_ind_type env mip = Inductive.type_of_inductive env mip -let print_one_inductive env mib ((_,i) as ind) = +let print_one_inductive env sigma mib ((_,i) as ind) = let u = if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes else Univ.Instance.empty in @@ -95,13 +95,14 @@ let print_one_inductive env mib ((_,i) as ind) = let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in let inst = - if mib.mind_polymorphic then Printer.pr_universe_instance mib.mind_universes + if mib.mind_polymorphic then + Printer.pr_universe_instance sigma mib.mind_universes else mt () in hov 0 ( - pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ - brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes + pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ + brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) @@ -113,11 +114,13 @@ let print_mutual_inductive env mind mib = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in + let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env mib) inds ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + (print_one_inductive env sigma mib) inds ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -146,6 +149,8 @@ let print_record env mind mib = let cstrtype = hnf_prod_applist env cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in + let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let keyword = let open Decl_kinds in match mib.mind_finite with @@ -157,16 +162,16 @@ let print_record env mind mib = hov 0 ( Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ - print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++ + print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ str ":= " ++ pr_id mip.mind_consnames.(0)) ++ brk(1,2) ++ hv 2 (str "{ " ++ prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ - Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then @@ -267,6 +272,7 @@ let print_body is_impl env mp (l,body) = if cb.const_polymorphic then Univ.UContext.instance cb.const_universes else Univ.Instance.empty in + let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -275,17 +281,17 @@ let print_body is_impl env mp (l,body) = | None -> mt () | Some env -> str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *) + hov 0 (Printer.pr_ltype_env env sigma (Vars.subst_instance_constr u (Typeops.type_of_constant_type env cb.const_type))) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env Evd.empty + Printer.pr_lconstr_env env sigma (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context cb.const_universes)) + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes)) | SFBmind mib -> try let env = Option.get env in -- cgit v1.2.3 From 48ffb1173702f86fa6cb6392f7876d7da5e5d6b6 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 29 Oct 2015 20:52:32 +0100 Subject: Make the code of compare functions linear in the number of constructors. This scheme has been advised by @gashe on #79. Interestingly there are several comparison functions in Coq which were already implemented with this scheme. --- printing/printer.ml | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index 18e4902255..12782a428a 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -724,18 +724,17 @@ module OrderedContextObject = struct type t = context_object 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, _) -> con_ord 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) -- cgit v1.2.3 From 4e643d134f02cfa9a73754c3cf48048541324834 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 31 Oct 2015 15:49:09 +0100 Subject: Adding syntax "Show id" to show goal named id (shelved or not). --- printing/ppvernac.ml | 3 ++- printing/printer.ml | 21 ++++++++++++++++----- printing/printer.mli | 3 ++- 3 files changed, 20 insertions(+), 7 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 00c276bdbe..72b9cafe3f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -594,7 +594,8 @@ module Make let pr_goal_reference = function | OpenSubgoals -> mt () | NthGoal n -> spc () ++ int n - | GoalId n -> spc () ++ str n in + | GoalId id -> spc () ++ pr_id id + | GoalUid n -> spc () ++ str n in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n diff --git a/printing/printer.ml b/printing/printer.ml index 202b4f2bc7..2e112f9ace 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -455,14 +455,17 @@ let pr_ne_evar_set hd tl sigma l = else mt () +let pr_selected_subgoal name sigma g = + let pg = default_pr_goal { sigma=sigma ; it=g; } in + v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g + ++ str " is:" ++ cut () ++ pg) + let default_pr_subgoal n sigma = let rec prrec p = function | [] -> error "No such goal." | g::rest -> if Int.equal p 1 then - let pg = default_pr_goal { sigma=sigma ; it=g; } in - v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g - ++ str " is:" ++ cut () ++ pg) + pr_selected_subgoal (int n) sigma g else prrec (p-1) rest in @@ -652,9 +655,17 @@ let pr_nth_open_subgoal n = let pr_goal_by_id id = let p = Proof_global.give_me_the_proof () in - let g = Goal.get_by_uid id in + try + Proof.in_proof p (fun sigma -> + let g = Evd.evar_key id sigma in + pr_selected_subgoal (pr_id id) sigma g) + with Not_found -> error "No such goal." + +let pr_goal_by_uid uid = + let p = Proof_global.give_me_the_proof () in + let g = Goal.get_by_uid uid in let pr gs = - v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut () + v 0 (str "goal / evar " ++ str uid ++ str " is:" ++ cut () ++ pr_goal gs) in try diff --git a/printing/printer.mli b/printing/printer.mli index 0a44e4f103..5c60b89366 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -176,7 +176,8 @@ module ContextObjectMap : CMap.ExtS val pr_assumptionset : env -> Term.types ContextObjectMap.t -> std_ppcmds -val pr_goal_by_id : string -> std_ppcmds +val pr_goal_by_id : Id.t -> std_ppcmds +val pr_goal_by_uid : string -> std_ppcmds type printer_pr = { pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; -- cgit v1.2.3 From cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Dec 2015 15:18:42 +0100 Subject: Dead code from August 2014 in apply in. --- printing/pptactic.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index a669aef9a8..bc559460e0 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -581,8 +581,7 @@ module Make let pr_in_hyp_as prc pr_id = function | None -> mt () - | Some (clear,id,ipat) -> - pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat + | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat let pr_clauses default_is_concl pr_id = function | { onhyps=Some []; concl_occs=occs } -- cgit v1.2.3 From 281bed69ee7d4a7638d07f07f9d6722b897f29cc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 3 Dec 2015 14:59:27 +0100 Subject: Improving over printing of let-tuple (see #4447). For instance, #4447 is now printed: λ Ca Da : ℕAlg, let (ℕ, ℕ0) := (Ca, Da) in let (C, p) := ℕ in let (c₀, cs) := p in let (D, p0) := ℕ0 in let (d₀, ds) := p0 in {h : C → D & ((h c₀ = d₀) * (∀ c : C, h (cs c) = ds (h c)))%type} : ℕAlg → ℕAlg → Type --- printing/ppconstr.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index ea705e335e..663b8b8101 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -638,13 +638,13 @@ end) = struct | CLetTuple (_,nal,(na,po),c,b) -> return ( hv 0 ( - keyword "let" ++ spc () ++ - hov 0 (str "(" ++ + hov 2 (keyword "let" ++ spc () ++ + hov 1 (str "(" ++ prlist_with_sep sep_v pr_lname nal ++ str ")" ++ - pr_simple_return_type (pr mt) na po ++ str " :=" ++ - pr spc ltop c ++ spc () - ++ keyword "in") ++ + pr_simple_return_type (pr mt) na po ++ str " :=") ++ + pr spc ltop c + ++ keyword " in") ++ pr spc ltop b), lletin ) -- cgit v1.2.3 From 0aba678e885fa53fa649de59eb1d06b4af3a847c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Dec 2015 20:42:07 +0100 Subject: Getting rid of the dynamic node of the tactic AST. --- printing/pptactic.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 766222156a..97917d2c72 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1263,9 +1263,6 @@ module Make 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) -> -- cgit v1.2.3 From 6899d3aa567436784a08af4e179c2ef1fa504a02 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 21 Nov 2015 00:17:21 +0100 Subject: Moving extended_rel_vect/extended_rel_list to the kernel. It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file. --- printing/printmod.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'printing') diff --git a/printing/printmod.ml b/printing/printmod.ml index 1d275c1aa6..d6f847cc71 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,6 +65,7 @@ let get_new_id locals id = (** Inductive declarations *) +open Context open Termops open Reduction -- cgit v1.2.3 From 597e5dd737dd235222798153b2342ae609519348 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 16 Dec 2015 20:03:45 +0100 Subject: Getting rid of some hardwired generic arguments. --- printing/pptactic.ml | 40 +++++++++++++--------------------------- 1 file changed, 13 insertions(+), 27 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 97917d2c72..dfb8837eca 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -275,15 +275,7 @@ module Make | 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 @@ -320,17 +312,7 @@ module Make 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 @@ -363,16 +345,7 @@ module Make | 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 @@ -1461,6 +1434,19 @@ let () = (fun (c,_) -> Printer.pr_glob_constr c) Printer.pr_closed_glob ; + 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 { Evd.it = it } -> pr_bindings_no_with pr_constr pr_lconstr 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 { Evd.it = it } -> pr_with_bindings pr_constr pr_lconstr 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; -- cgit v1.2.3 From eee16239f6b00400c8a13b787c310bcb11c37afe Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 12:06:24 +0100 Subject: Tying the loop in tactic printing API. --- printing/pptactic.ml | 76 +++++++++++++++++++++++++++++++----------------- printing/pptacticsig.mli | 45 +++++++--------------------- printing/ppvernac.ml | 8 +---- 3 files changed, 60 insertions(+), 69 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index dfb8837eca..4d14cae7a7 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -265,12 +265,12 @@ module Make let with_evars ev s = if ev then "e" ^ s else s - let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = + let rec pr_raw_generic_rec 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) + | GenArgType -> pr_raw_generic_rec 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 @@ -278,14 +278,14 @@ module Make | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = - let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in + let map x = pr_raw_generic_rec 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) + | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in hov 0 (opt_unpack { opt_unpacker } x) | PairArgType _ -> @@ -293,7 +293,7 @@ module Make 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] + pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q] in hov 0 (pair_unpack { pair_unpacker } x) | ExtraArgType s -> @@ -301,12 +301,12 @@ module Make with Not_found -> Genprint.generic_raw_print x - let rec pr_glb_generic prc prlc prtac prpat x = + let rec pr_glb_generic_rec 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) + | GenArgType -> pr_glb_generic_rec prc prlc prtac prpat (out_gen (glbwit wit_genarg) x) | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) | ConstrMayEvalArgType -> pr_may_eval prc prlc @@ -315,14 +315,14 @@ module Make | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = - let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in + let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in pr_sequence map (glb l) in hov 0 (list_unpack { list_unpacker } x) | OptArgType _ -> let opt_unpacker wit o = match glb o with | None -> mt () - | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) + | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in hov 0 (opt_unpack { opt_unpacker } x) | PairArgType _ -> @@ -330,32 +330,32 @@ module Make 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] + pr_sequence (pr_glb_generic_rec 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 = + let rec pr_top_generic_rec 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) + | GenArgType -> pr_top_generic_rec 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) | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = - let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in + let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in pr_sequence map (top l) in hov 0 (list_unpack { list_unpacker } x) | OptArgType _ -> let opt_unpacker wit o = match top o with | None -> mt () - | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) + | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in hov 0 (opt_unpack { opt_unpacker } x) | PairArgType _ -> @@ -363,7 +363,7 @@ module Make 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] + pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in hov 0 (pair_unpack { pair_unpacker } x) | ExtraArgType s -> @@ -415,19 +415,19 @@ module Make 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_extend_rec prc prlc prtac prpat = + pr_extend_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference) + let pr_glob_extend_rec prc prlc prtac prpat = + pr_extend_gen (pr_glb_generic_rec prc prlc prtac prpat) + let pr_extend_rec prc prlc prtac prpat = + pr_extend_gen (pr_top_generic_rec prc prlc prtac prpat) let pr_raw_alias prc prlc prtac prpat = - pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference) + pr_alias_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference) let pr_glob_alias prc prlc prtac prpat = - pr_alias_gen (pr_glb_generic prc prlc prtac prpat) + pr_alias_gen (pr_glb_generic_rec prc prlc prtac prpat) let pr_alias prc prlc prtac prpat = - pr_alias_gen (pr_top_generic prc prlc prtac prpat) + pr_alias_gen (pr_top_generic_rec prc prlc prtac prpat) (**********************************************************************) (* The tactic printer *) @@ -1282,7 +1282,7 @@ module Make pr_reference = pr_reference; pr_name = pr_lident; pr_generic = Genprint.generic_raw_print; - pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; + pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; } in make_pr_tac @@ -1313,7 +1313,7 @@ module Make pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; pr_generic = Genprint.generic_glb_print; - pr_extend = pr_glob_extend + pr_extend = pr_glob_extend_rec (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); pr_alias = pr_glob_alias @@ -1355,7 +1355,7 @@ module Make pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; pr_generic = Genprint.generic_top_print; - pr_extend = pr_extend + pr_extend = pr_extend_rec (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) (pr_glob_tactic_level env) pr_constr_pattern; pr_alias = pr_alias @@ -1370,6 +1370,28 @@ module Make in prtac n t + let pr_raw_generic env = pr_raw_generic_rec + pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference + + let pr_glb_generic env = pr_glb_generic_rec + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + + let pr_top_generic env = pr_top_generic_rec + (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) + (pr_glob_tactic_level env) pr_constr_pattern + + let pr_raw_extend env = pr_raw_extend_rec + pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr + + let pr_glob_extend env = pr_glob_extend_rec + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + + let pr_extend env = pr_extend_rec + (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) + (pr_glob_tactic_level env) pr_constr_pattern + let pr_tactic env = pr_tactic_level env ltop end diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 1631bda377..1c17d04928 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -32,45 +32,20 @@ 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 -> + + val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds + + val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds + + val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds + + val pr_raw_extend: env -> int -> ml_tactic_entry -> raw_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 -> + val pr_glob_extend: env -> int -> ml_tactic_entry -> glob_generic_argument list -> std_ppcmds - val pr_extend : - (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (constr_pattern -> std_ppcmds) -> int -> + val pr_extend : env -> int -> ml_tactic_entry -> typed_generic_argument list -> std_ppcmds val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 72b9cafe3f..d79fb45618 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -79,13 +79,7 @@ module Make | VernacEndSubproof -> str"" | _ -> str"." - let pr_gen t = - pr_raw_generic - pr_constr_expr - pr_lconstr_expr - pr_raw_tactic_level - pr_constr_expr - pr_reference t + let pr_gen t = pr_raw_generic (Global.env ()) t let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() -- cgit v1.2.3 From e181c9b043e64342c1e51763f4fe88c78bc4736d Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 12:20:47 +0100 Subject: CLEANUP: Vernacexpr.vernac_expr Originally, "VernacTime" and "VernacRedirect" were defined like this: type vernac_expr = ... | VernacTime of vernac_list | VernacRedirect of string * vernac_list ... where type vernac_list = located_vernac_expr list Currently, that list always contained one and only one element. So I propose changing the definition of these two variants in the following way: | VernacTime of located_vernac_expr | VernacRedirect of string * located_vernac_expr which covers all our current needs and enforces the invariant related to the number of commands that are part of the "VernacTime" and "VernacRedirect" variants. --- printing/ppvernac.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index d79fb45618..0f065e251b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -635,10 +635,10 @@ module Make else spc() ++ qs s ) - | VernacTime v -> - return (keyword "Time" ++ spc() ++ pr_vernac_list v) - | VernacRedirect (s, v) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v) + | VernacTime (_,v) -> + return (keyword "Time" ++ spc() ++ pr_vernac v) + | VernacRedirect (s, (_,v)) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v) | VernacFail v -> @@ -1030,7 +1030,7 @@ module Make return (keyword "Cd" ++ pr_opt qs s) (* Commands *) - | VernacDeclareTacticDefinition (rc,l) -> + | VernacDeclareTacticDefinition l -> let pr_tac_body (id, redef, body) = let idl, body = match body with @@ -1262,11 +1262,6 @@ module Make | VernacEndSubproof -> return (str "}") - and pr_vernac_list l = - hov 2 (str"[" ++ spc() ++ - prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l - ++ spc() ++ str"]") - and pr_extend s cl = let pr_arg a = try pr_gen a -- cgit v1.2.3 From 493b5d18971c8c19eaeccfc992d1212c6479d227 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:38:19 +0100 Subject: CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular command is mapped. --- printing/ppvernac.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 0f065e251b..5110cf7b23 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1224,8 +1224,6 @@ module Make (keyword "Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) ) - | VernacNop -> - mt() (* Toplevel control *) | VernacToplevelControl exn -> -- cgit v1.2.3 From 20641795624dbb03da0401e4dc503660e5e73df6 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:50:40 +0100 Subject: CLEANUP: Vernacexpr.VernacDeclareTacticDefinition The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that. --- printing/ppvernac.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5110cf7b23..f216c599d0 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1031,12 +1031,17 @@ module Make (* Commands *) | VernacDeclareTacticDefinition l -> - let pr_tac_body (id, redef, body) = + let pr_tac_body tacdef_body = + let id, redef, body = + match tacdef_body with + | TacticDefinition ((_,id), body) -> str (Id.to_string id), false, body + | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body + in let idl, body = match body with | Tacexpr.TacFun (idl,b) -> idl,b | _ -> [], body in - pr_ltac_ref id ++ + id ++ prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ -- cgit v1.2.3 From 1b5f85d38db7a0d7cb9a4b9491a5563461373182 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 17:31:25 +0100 Subject: CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified --- printing/ppconstr.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 663b8b8101..56429410cb 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -457,7 +457,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 +465,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 @@ -611,12 +611,12 @@ end) = struct ++ 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)), -- cgit v1.2.3 From b2beb9087628de23679a831e6273b91816f1ed27 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Dec 2015 19:24:17 +0100 Subject: Using dynamic values in tactic evaluation. --- printing/pptacticsig.mli | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'printing') diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 1c17d04928..d154e0b663 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -48,6 +48,12 @@ module type Pp = sig val pr_extend : env -> int -> ml_tactic_entry -> typed_generic_argument list -> std_ppcmds + val pr_extend_gen : + ('a -> std_ppcmds) -> int -> ml_tactic_entry -> 'a list -> std_ppcmds + + val pr_alias_gen : ('a -> std_ppcmds) -> + int -> Names.KerName.t -> 'a list -> std_ppcmds + val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds val pr_raw_tactic : raw_tactic_expr -> std_ppcmds -- cgit v1.2.3 From 329b5b9ed526d572d7df066dc99486e1dcb9e4cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 17:18:06 +0100 Subject: Removing the now useless genarg generic argument. --- printing/pptactic.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 4d14cae7a7..b511300758 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -270,7 +270,6 @@ module Make | 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_rec 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 @@ -306,7 +305,6 @@ module Make | 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_rec prc prlc prtac prpat (out_gen (glbwit wit_genarg) x) | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) | ConstrMayEvalArgType -> pr_may_eval prc prlc @@ -342,7 +340,6 @@ module Make | 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_rec 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) | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) -- cgit v1.2.3 From 589130e87d68227d25800e7506666eaf1d47a25a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 17:30:09 +0100 Subject: Changing the toplevel type of the int_or_var generic type to int. --- printing/pptactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b511300758..94cbc54e94 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -337,7 +337,7 @@ module Make let rec pr_top_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x) + | IntOrVarArgType -> 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) | ConstrArgType -> prc (out_gen (topwit wit_constr) x) -- cgit v1.2.3 From 5835804bd69a193b9ea29b6d4c8d0cc03530ccdd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 18:04:14 +0100 Subject: Removing ad-hoc interpretation rules for tactic notations and their genarg. Now that types can share the same dynamic representation, we do not have to transtype the topelvel values dynamically and just take advantage of the standard interpretation function. --- printing/pptactic.ml | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 94cbc54e94..9c6da350fa 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -267,13 +267,9 @@ module Make let rec pr_raw_generic_rec 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) | 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) | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = @@ -302,14 +298,9 @@ module Make let rec pr_glb_generic_rec 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) | 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) | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = @@ -337,11 +328,9 @@ module Make let rec pr_top_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | IntOrVarArgType -> 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) | ConstrArgType -> prc (out_gen (topwit wit_constr) x) - | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x) | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = @@ -1432,6 +1421,8 @@ 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 @@ -1462,6 +1453,11 @@ let () = (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 { Evd.it = it } -> pr_bindings_no_with pr_constr pr_lconstr it); + Genprint.register_print0 Constrarg.wit_constr_may_eval + (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr) + (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr) + (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr)) + pr_constr; Genprint.register_print0 Constrarg.wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) -- cgit v1.2.3 From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 22:35:09 +0100 Subject: Do not compose "str" and "to_string" whenever possible. For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read. --- printing/ppconstr.ml | 6 +++--- printing/ppvernac.ml | 2 +- printing/printer.ml | 4 ++-- printing/printmod.ml | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 56429410cb..d15c3ee2f1 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -153,11 +153,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 +182,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 diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f216c599d0..4957199903 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1034,7 +1034,7 @@ module Make let pr_tac_body tacdef_body = let id, redef, body = match tacdef_body with - | TacticDefinition ((_,id), body) -> str (Id.to_string id), false, body + | TacticDefinition ((_,id), body) -> pr_id id, false, body | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body in let idl, body = diff --git a/printing/printer.ml b/printing/printer.ml index 2e112f9ace..7c031ea536 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -777,7 +777,7 @@ let pr_assumptionset env s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in + let var = pr_id id ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) | Axiom (kn,[]) -> let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in @@ -786,7 +786,7 @@ let pr_assumptionset env s = let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++ cut() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> - str " used in " ++ str (Names.Label.to_string lbl) ++ + str " used in " ++ pr_label lbl ++ str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) l in (v, ax :: a, o, tr) diff --git a/printing/printmod.ml b/printing/printmod.ml index d6f847cc71..e0b1d55be2 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -264,7 +264,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 -- cgit v1.2.3 From daa7cb065a238c7d4ee394e00315d66d023e5259 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Dec 2015 17:55:25 +0100 Subject: Removing auto from the tactic AST. --- printing/pptactic.ml | 19 ------------------- 1 file changed, 19 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 9c6da350fa..ff83ac3e9e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -807,8 +807,6 @@ module Make let rec pr_atom0 a = tag_atom a (match a with | TacIntroPattern [] -> primitive "intros" | TacIntroMove (None,MoveLast) -> primitive "intro" - | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial" - | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto" | TacClear (true,[]) -> primitive "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" ) @@ -917,23 +915,6 @@ module Make ++ pr_arg pr_quantified_hypothesis h2 ) - (* Automation tactics *) - | TacTrivial (_,[],Some []) as x -> - pr_atom0 x - | TacTrivial (d,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "trivial" - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - | TacAuto (_,None,[],Some []) as x -> - pr_atom0 x - | TacAuto (d,n,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "auto" - ++ pr_opt (pr_or_var int) n - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - (* Context management *) | TacClear (true,[]) as t -> pr_atom0 t -- cgit v1.2.3 From 77e6eda6388aba117476f6c8445c4b61ebdbc33e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Dec 2015 00:44:58 +0100 Subject: Tentative API fix for tactic arguments to be fed to tclWITHHOLES. The previous implementation was a source of evar leaks if misused, as it created values coming together with their current evar_map. This is dead wrong if the value is not used on the spot. To fix this, we rather return a ['a delayed_open] object. Two argument types were modified: bindings and constr_bindings. The open_constr argument should also be fixed, but it is more entangled and thus I leave it for another commit. --- printing/pptactic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index ff83ac3e9e..b98738ce31 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1433,7 +1433,7 @@ let () = 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 { Evd.it = it } -> pr_bindings_no_with pr_constr pr_lconstr it); + (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it))); Genprint.register_print0 Constrarg.wit_constr_may_eval (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr) (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr) @@ -1442,7 +1442,7 @@ let () = 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 { Evd.it = it } -> pr_with_bindings pr_constr pr_lconstr it); + (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it))); Genprint.register_print0 Stdarg.wit_int int int int; Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; -- cgit v1.2.3 From cb2f6a95ee72edb956f419a24f8385c8ae7f96f4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 28 Dec 2015 02:08:42 +0100 Subject: Removing the special status of open_constr generic argument. We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state. --- printing/pptactic.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b98738ce31..6e051a1fc0 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -270,7 +270,6 @@ module Make | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x) | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) - | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in @@ -301,7 +300,6 @@ module Make | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x) | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) - | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in @@ -331,7 +329,6 @@ module Make | IdentArgType -> pr_id (out_gen (topwit wit_ident) x) | VarArgType -> pr_id (out_gen (topwit wit_var) x) | ConstrArgType -> prc (out_gen (topwit wit_constr) x) - | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) | ListArgType _ -> let list_unpacker wit l = let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in @@ -1425,6 +1422,12 @@ let () = (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)) -- cgit v1.2.3 From 203b0eaac832af3b62e484c1aef89a02ffe8e29b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Dec 2015 18:31:17 +0100 Subject: External tactics and notations now accept any tactic argument. This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant. --- printing/pptactic.ml | 43 ++++++++++++++++++++++++++++++------------- printing/pptacticsig.mli | 15 ++++++--------- 2 files changed, 36 insertions(+), 22 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 6e051a1fc0..4cb7e9fb38 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -371,10 +371,11 @@ module Make in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = + let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l = try let pp_rules = Hashtbl.find prtac_tab s in let pp = pp_rules.(i) in + let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found 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 @@ -389,28 +390,35 @@ module Make in str "<" ++ name ++ str ">" ++ args - let pr_alias_gen pr_gen lev key l = + let pr_alias_gen check pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in let (lev', pl) = pp.pptac_prods in + let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found in let p = pr_tacarg_using_rule pr_gen (pl, l) in if lev' > lev then surround p else p with Not_found -> KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" + let check_type t arg = match arg with + | TacGeneric arg -> argument_type_eq t (genarg_tag arg) + | _ -> false + + let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false + let pr_raw_extend_rec prc prlc prtac prpat = - pr_extend_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference) + pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) let pr_glob_extend_rec prc prlc prtac prpat = - pr_extend_gen (pr_glb_generic_rec prc prlc prtac prpat) + pr_extend_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) let pr_extend_rec prc prlc prtac prpat = - pr_extend_gen (pr_top_generic_rec prc prlc prtac prpat) + pr_extend_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) let pr_raw_alias prc prlc prtac prpat = - pr_alias_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference) + pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) let pr_glob_alias prc prlc prtac prpat = - pr_alias_gen (pr_glb_generic_rec prc prlc prtac prpat) + pr_alias_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) let pr_alias prc prlc prtac prpat = - pr_alias_gen (pr_top_generic_rec prc prlc prtac prpat) + pr_alias_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) (**********************************************************************) (* The tactic printer *) @@ -716,8 +724,8 @@ module Make pr_reference : 'ref -> std_ppcmds; pr_name : 'nam -> std_ppcmds; pr_generic : 'lev generic_argument -> std_ppcmds; - pr_extend : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds; - pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds; + pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds; + pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds; } constraint 'a = < @@ -1352,9 +1360,18 @@ module Make (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_extend env = pr_extend_rec - (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern + let check_val_type t arg = + let t = Genarg.val_tag (Obj.magic t) in (** FIXME *) + let Val.Dyn (t', _) = arg in + match Genarg.Val.eq t t' with + | None -> false + | Some _ -> true + + let pr_alias pr lev key args = + pr_alias_gen check_val_type pr lev key args + + let pr_extend pr lev ml args = + pr_extend_gen check_val_type pr lev ml args let pr_tactic env = pr_tactic_level env ltop diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index d154e0b663..01f240f6b8 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -40,19 +40,16 @@ module type Pp = sig val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds val pr_raw_extend: env -> int -> - ml_tactic_entry -> raw_generic_argument list -> std_ppcmds + ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds val pr_glob_extend: env -> int -> - ml_tactic_entry -> glob_generic_argument list -> std_ppcmds + ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds - val pr_extend : env -> int -> - ml_tactic_entry -> typed_generic_argument list -> std_ppcmds + val pr_extend : + (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds - val pr_extend_gen : - ('a -> std_ppcmds) -> int -> ml_tactic_entry -> 'a list -> std_ppcmds - - val pr_alias_gen : ('a -> std_ppcmds) -> - int -> Names.KerName.t -> 'a list -> std_ppcmds + val pr_alias : (Val.t -> std_ppcmds) -> + int -> Names.KerName.t -> Val.t list -> std_ppcmds val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds -- cgit v1.2.3 From 1a157442dff4bfa127af467c49280e79889acde7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 26 Dec 2015 10:07:19 +0100 Subject: Do not compose List.length with List.filter. --- printing/prettyp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 84649e6ebf..08228cb209 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -132,7 +132,7 @@ 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 nprods = List.count (fun (_,b,_) -> Option.is_empty b) ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in List.exists is_status_implicit lastimpl -- cgit v1.2.3 From f3e611b2115b425f875e971ac9ff7534c2af2800 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 31 Dec 2015 13:56:40 +0100 Subject: Separation of concern in TacAlias API. The TacAlias node now only contains the arguments fed to the tactic notation. The binding variables are worn by the tactic representation in Tacenv. --- printing/pptactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 4cb7e9fb38..50a543968a 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1201,7 +1201,7 @@ 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 -- cgit v1.2.3 From a5e1b40b93e47a278746ee6752474891cd856c29 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 31 Dec 2015 19:26:02 +0100 Subject: Simplification of grammar_prod_item type. Actually the identifier was never used and just carried along. --- printing/ppvernac.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4957199903..daba18bad2 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -105,10 +105,9 @@ module Make else id let pr_production_item = function - | TacNonTerm (loc,nt,Some (p,sep)) -> + | TacNonTerm (loc, nt, (p, sep)) -> let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")" - | TacNonTerm (loc,nt,None) -> str nt | TacTerm s -> qs s let pr_comment pr_c = function -- cgit v1.2.3 From 2c8275ee3e0e5cd4eb8afd24047fda7f864e0e4e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 16:50:02 +0100 Subject: Remove useless rec flags. --- printing/pptactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 50a543968a..7800f1edb3 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1268,7 +1268,7 @@ module Make let pr_pat_and_constr_expr pr ((c,_),_) = pr c - let rec pr_glob_tactic_level env n t = + let pr_glob_tactic_level env n t = let glob_printers = (strip_prod_binders_glob_constr) in -- cgit v1.2.3 From 5129c5b02bcab1426636d18583ec7a4a46195f0a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 16:55:03 +0100 Subject: Reduce dependencies of interface files. --- printing/pptacticsig.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing') diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 01f240f6b8..5b89266553 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -8,11 +8,9 @@ open Pp open Genarg -open Constrexpr open Tacexpr open Ppextend open Environ -open Pattern open Misctypes module type Pp = sig -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- printing/ppconstr.ml | 2 -- printing/pptactic.ml | 5 ----- 2 files changed, 7 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d15c3ee2f1..c07057a096 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -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 diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7800f1edb3..a5716279f3 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -685,11 +685,6 @@ module Make | l -> spc () ++ hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l) - let string_of_debug = function - | Off -> "" - | Debug -> "debug " - | Info -> "info_" - let pr_then () = str ";" let ltop = (5,E) -- cgit v1.2.3 From 5d26829704b2602ede45183cba54ab219e453c0e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:57:06 +0100 Subject: Use streams rather than strings to handle bullet suggestions. --- printing/printer.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index 7c031ea536..b6dda93c22 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -639,8 +639,8 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ - (match Proof_global.Bullet.suggest p - with None -> str"" | Some s -> fnl () ++ str s) ++ + (let s = Proof_global.Bullet.suggest p in + if Pp.is_empty s then s else fnl () ++ s) ++ fnl () in pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- printing/printer.ml | 8 ++++---- printing/printer.mli | 13 ++++++------- printing/printmod.ml | 5 ++--- 3 files changed, 12 insertions(+), 14 deletions(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index 2e112f9ace..773127c772 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -293,7 +293,7 @@ let pr_named_context_of env sigma = hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) let pr_named_context env sigma ne_context = - hv 0 (Context.fold_named_context + hv 0 (Context.Named.fold_outside (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) ne_context ~init:(mt ())) @@ -306,7 +306,7 @@ let pr_rel_context_of env sigma = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env sigma = let sign_env = - Context.fold_named_list_context + Context.NamedList.fold (fun d pps -> let pidt = pr_var_list_decl env sigma d in (pps ++ fnl () ++ pidt)) @@ -333,7 +333,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 ".")) @@ -726,7 +726,7 @@ let prterm = pr_lconstr type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (* An opaque constant. *) | Transparent of constant diff --git a/printing/printer.mli b/printing/printer.mli index 5c60b89366..bdb295a478 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 @@ -165,7 +164,7 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *) type context_object = | Variable of Id.t (** A section variable or a Let definition *) (** An axiom and the type it inhabits (if an axiom of the empty type) *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (** An opaque constant. *) | Transparent of constant (** A transparent constant *) diff --git a/printing/printmod.ml b/printing/printmod.ml index d6f847cc71..d277d3782a 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,7 +65,6 @@ let get_new_id locals id = (** Inductive declarations *) -open Context open Termops open Reduction @@ -90,7 +89,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 @@ -144,7 +143,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 -- cgit v1.2.3 From a1aff01d16bad2f44392fd5cb804092e12e558ed Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:19:51 +0100 Subject: CLEANUP: removing unused field I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around. --- printing/ppconstr.ml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index c07057a096..3343997823 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -593,17 +593,9 @@ end) = struct return (p, lproj) | CApp (_,(None,a),l) -> return (pr_app (pr mt) a l, lapp) - | CRecord (_,w,l) -> - let beg = - match w with - | None -> - spc () - | Some t -> - spc () ++ pr spc ltop t ++ spc () - ++ keyword "with" ++ spc () - in + | CRecord (_,l) -> return ( - hv 0 (str"{|" ++ beg ++ + hv 0 (str"{|" ++ spc () ++ prlist_with_sep pr_semicolon (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l ++ str" |}"), -- cgit v1.2.3 From 67b9b34d409c793dc449104525684852353ee064 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Jan 2016 21:40:23 +0100 Subject: Removing ident and var generic arguments. --- printing/pptactic.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index a5716279f3..df5f57dac1 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -267,8 +267,6 @@ module Make let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = match Genarg.genarg_tag x with - | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = @@ -297,8 +295,6 @@ module Make let rec pr_glb_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = @@ -326,8 +322,6 @@ module Make let rec pr_top_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | IdentArgType -> pr_id (out_gen (topwit wit_ident) x) - | VarArgType -> pr_id (out_gen (topwit wit_var) x) | ConstrArgType -> prc (out_gen (topwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = @@ -1415,6 +1409,10 @@ let () = (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) -- cgit v1.2.3 From 448866f0ec5291d58677d8fccbefde493ade0ee2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Jan 2016 22:20:16 +0100 Subject: Removing constr generic argument. --- printing/pptactic.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index df5f57dac1..a8fa8313f2 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -267,7 +267,6 @@ module Make let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = match Genarg.genarg_tag x with - | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in @@ -295,7 +294,6 @@ module Make let rec pr_glb_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in @@ -322,7 +320,6 @@ module Make let rec pr_top_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | ConstrArgType -> prc (out_gen (topwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in @@ -1426,6 +1423,12 @@ let () = ; Genprint.register_print0 Constrarg.wit_sort pr_glob_sort pr_glob_sort (pr_sort Evd.empty); + Genprint.register_print0 + Constrarg.wit_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr -- cgit v1.2.3 From 28ac569f0f8a0ae27552e4e4c20fc06ce12c720d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 Jan 2016 23:34:52 +0100 Subject: Tactic notation printing accesses all the token data. --- printing/pptactic.ml | 39 +++++++++++++++++++++++---------------- printing/pptactic.mli | 6 +++--- 2 files changed, 26 insertions(+), 19 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index a8fa8313f2..5bc242b2b2 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -26,11 +26,11 @@ open Printer let pr_global x = Nametab.pr_global_env Id.Set.empty x -type grammar_terminals = string option list +type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list type pp_tactic = { - pptac_args : argument_type list; - pptac_prods : int * grammar_terminals; + pptac_level : int; + pptac_prods : grammar_terminals; } (* ML Extensions *) @@ -345,16 +345,22 @@ module Make with Not_found -> Genprint.generic_top_print x let rec tacarg_using_rule_token pr_gen = function - | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) - | None :: l, a :: al -> + | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) + | Egramml.GramNonTerminal _ :: l, a :: al -> let r = tacarg_using_rule_token pr_gen (l,al) in pr_gen a :: r | [], [] -> [] | _ -> failwith "Inconsistent arguments of extended tactic" + type any_arg = AnyArg : 'a Genarg.raw_abstract_argument_type -> any_arg + + let filter_arg = function + | Egramml.GramTerminal _ -> None + | Egramml.GramNonTerminal (_, t, _) -> Some (AnyArg t) + let pr_tacarg_using_rule pr_gen l = let l = match l with - | (Some s :: l, al) -> + | (Egramml.GramTerminal s :: l, al) -> (** First terminal token should be considered as the name of the tactic, so we tag it differently than the other terminal tokens. *) primitive s :: (tacarg_using_rule_token pr_gen (l, al)) @@ -366,10 +372,10 @@ module Make try let pp_rules = Hashtbl.find prtac_tab s in let pp = pp_rules.(i) in - let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found in - let (lev', pl) = pp.pptac_prods in - let p = pr_tacarg_using_rule pr_gen (pl,l) in - if lev' > lev then surround p else p + let args = List.map_filter filter_arg pp.pptac_prods in + let () = if not (List.for_all2eq check args l) then raise Not_found in + let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + if pp.pptac_level > lev then surround p else p with Not_found -> let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ @@ -384,15 +390,15 @@ module Make let pr_alias_gen check pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in - let (lev', pl) = pp.pptac_prods in - let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found in - let p = pr_tacarg_using_rule pr_gen (pl, l) in - if lev' > lev then surround p else p + let args = List.map_filter filter_arg pp.pptac_prods in + let () = if not (List.for_all2eq check args l) then raise Not_found in + let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + if pp.pptac_level > lev then surround p else p with Not_found -> KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" - let check_type t arg = match arg with - | TacGeneric arg -> argument_type_eq t (genarg_tag arg) + let check_type t arg = match t, arg with + | AnyArg t, TacGeneric arg -> argument_type_eq (unquote t) (genarg_tag arg) | _ -> false let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false @@ -1347,6 +1353,7 @@ module Make (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) let check_val_type t arg = + let AnyArg t = t in let t = Genarg.val_tag (Obj.magic t) in (** FIXME *) let Val.Dyn (t', _) = arg in match Genarg.Val.eq t t' with diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 30b9483db7..57c7f67fd4 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -41,11 +41,11 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit -type grammar_terminals = string option list +type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list type pp_tactic = { - pptac_args : argument_type list; - pptac_prods : int * grammar_terminals; + pptac_level : int; + pptac_prods : grammar_terminals; } val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit -- cgit v1.2.3 From 0d1345ea2423fc418a470786b0b33b80df3a67bc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 Jan 2016 01:08:21 +0100 Subject: Temporary commit getting rid of Obj.magic unsafety for Genarg. This will allow an easier landing of the rewriting of Genarg. --- printing/pptactic.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 5bc242b2b2..e7443fd02e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1354,11 +1354,12 @@ module Make let check_val_type t arg = let AnyArg t = t in - let t = Genarg.val_tag (Obj.magic t) in (** FIXME *) - let Val.Dyn (t', _) = arg in - match Genarg.Val.eq t t' with - | None -> false - | Some _ -> true +(* let t = Genarg.val_tag (Obj.magic t) in *) +(* let Val.Dyn (t', _) = arg in *) +(* match Genarg.Val.eq t t' with *) +(* | None -> false *) +(* | Some _ -> true *) + true (** FIXME *) let pr_alias pr lev key args = pr_alias_gen check_val_type pr lev key args -- cgit v1.2.3 From d3ee6b2fbcd0fbb666af7f1920446e809e8d6e1e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 Jan 2016 01:58:05 +0100 Subject: Getting rid of the awkward unpack mechanism from Genarg. --- printing/genprint.ml | 6 +-- printing/pptactic.ml | 125 +++++++++++++++++++++++---------------------------- 2 files changed, 59 insertions(+), 72 deletions(-) (limited to 'printing') diff --git a/printing/genprint.ml b/printing/genprint.ml index ade69ef831..58c41e839e 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -40,6 +40,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/pptactic.ml b/printing/pptactic.ml index e7443fd02e..53b0c091a5 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -265,84 +265,71 @@ module Make let with_evars ev s = if ev then "e" ^ s else s - let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = - match Genarg.genarg_tag x with - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - pr_sequence map (raw l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match raw o with + let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = raw o in - let p = in_gen (rawwit wit1) p in - let q = in_gen (rawwit wit2) q in - pr_sequence (pr_raw_generic_rec 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_rec prc prlc prtac prpat x = - match Genarg.genarg_tag x with - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in - pr_sequence map (glb l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match glb o with + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (rawwit wit1) p in + let q = in_gen (rawwit wit2) q in + hov 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q]) + | ExtraArg s -> + try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x) + with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x) + + + let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () | Some x -> pr_glb_generic_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 = glb o in - let p = in_gen (glbwit wit1) p in - let q = in_gen (glbwit wit2) q in - pr_sequence (pr_glb_generic_rec 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_rec prc prlc prtac prpat x = - match Genarg.genarg_tag x with - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in - pr_sequence map (top l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match top o with + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (glbwit wit1) p in + let q = in_gen (glbwit wit2) q in + let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in + hov 0 ans + | ExtraArg s -> + try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x) + with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x) + + let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = top o in - let p = in_gen (topwit wit1) p in - let q = in_gen (topwit wit2) q in - pr_sequence (pr_top_generic_rec 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 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (topwit wit1) p in + let q = in_gen (topwit wit2) q in + let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in + hov 0 ans + | ExtraArg s -> + try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x) + with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x) let rec tacarg_using_rule_token pr_gen = function | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- printing/genprint.ml | 2 +- printing/genprint.mli | 2 +- printing/miscprint.ml | 2 +- printing/miscprint.mli | 2 +- printing/ppannotation.ml | 2 +- printing/ppannotation.mli | 2 +- printing/ppconstr.ml | 2 +- printing/ppconstr.mli | 2 +- printing/ppconstrsig.mli | 2 +- printing/pptactic.ml | 2 +- printing/pptactic.mli | 2 +- printing/pptacticsig.mli | 2 +- printing/pputils.ml | 2 +- printing/pputils.mli | 2 +- printing/ppvernac.ml | 2 +- printing/ppvernac.mli | 2 +- printing/ppvernacsig.mli | 2 +- printing/prettyp.ml | 2 +- printing/prettyp.mli | 2 +- printing/printer.ml | 2 +- printing/printer.mli | 2 +- printing/printmod.ml | 2 +- printing/printmod.mli | 2 +- printing/printmodsig.mli | 2 +- printing/richprinter.mli | 2 +- 25 files changed, 25 insertions(+), 25 deletions(-) (limited to 'printing') diff --git a/printing/genprint.ml b/printing/genprint.ml index ade69ef831..d4f792b753 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 "]" -- cgit v1.2.3 From 5cbcc8fd761df0779f6202fef935f07cfef8a228 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 23 Jan 2016 15:17:29 -0500 Subject: Implement support for universe binder lists in Instance and Program Fixpoint/Definition. --- printing/ppvernac.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index d2f59e7b8d..38add9d2c8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -925,8 +925,9 @@ module Make hov 1 ( (if abst then keyword "Declare" ++ spc () else mt ()) ++ keyword "Instance" ++ - (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | - Anonymous -> mt ()) ++ + (match instid with + | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc () + | (_, Anonymous), _ -> mt ()) ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ pr_constr cl ++ pr_priority pri ++ -- cgit v1.2.3 From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 29 Jan 2016 10:13:12 +0100 Subject: CLEANUP: Context.{Rel,Named}.Declaration.t Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- printing/prettyp.ml | 31 ++++++++++++++++++------------- printing/prettyp.mli | 2 +- printing/printer.ml | 18 +++++++++++------- 3 files changed, 30 insertions(+), 21 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b448df3375..b7b1d67f03 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -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.count (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 -> @@ -440,11 +443,13 @@ let print_named_def name body typ = let print_named_assum name typ = str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" -let gallina_print_named_decl (id,c,typ) = - let s = Id.to_string id in - match c with - | Some body -> print_named_def s body typ - | None -> print_named_assum s typ +let gallina_print_named_decl = + let open Context.Named.Declaration in + function + | LocalAssum (id, typ) -> + print_named_assum (Id.to_string id) typ + | LocalDef (id, body, typ) -> + print_named_def (Id.to_string id) body typ let assumptions_for_print lna = List.fold_right (fun na env -> add_name na env) lna empty_names_context @@ -721,8 +726,8 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - let (_,c,typ) = Global.lookup_named str in - (print_named_decl (str,c,typ)) + let open Context.Named.Declaration in + str |> Global.lookup_named |> set_id str |> print_named_decl with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") @@ -750,8 +755,8 @@ let print_opaque_name qid = let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let (_,c,ty) = lookup_named id env in - print_named_decl (id,c,ty) + let open Context.Named.Declaration in + lookup_named id env |> set_id id |> print_named_decl let print_about_any loc k = match k with diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 6f3556adba..0eab155796 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 93850e41fa..5f4371f2d0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -262,16 +262,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 @@ -420,7 +423,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)") -- cgit v1.2.3 From f46a5686853353f8de733ae7fbd21a3a61977bc7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Feb 2016 15:32:58 +0100 Subject: Do not give a name to anonymous evars anymore. See bug #4547. The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced. --- printing/printer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index 5ad0e45319..63755d7ff7 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -400,7 +400,7 @@ let display_name = false (* display a goal name *) let pr_goal_name sigma g = - if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma)) + if display_name then str " " ++ Pp.surround (pr_existential_key sigma g) else mt () (* display the conclusion of a goal *) -- cgit v1.2.3 From f358d7b4c962f5288ad9ce2dc35802666c882422 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 22 Feb 2016 10:32:57 +0100 Subject: The tactic generic argument now returns a value rather than a glob_expr. The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side. --- printing/pptactic.ml | 10 ++++++---- printing/pptactic.mli | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c00036bb3c..ed85b21478 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -61,7 +61,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 let genarg_pprule = ref String.Map.empty @@ -106,6 +106,8 @@ module Make let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) + let pr_value _ _ = str "(* FIXME *)" + let pr_with_occurrences pr (occs,c) = match occs with | AllOccurrences -> @@ -1308,10 +1310,10 @@ module Make pr_generic = Genprint.generic_top_print; pr_extend = pr_extend_rec (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern; + pr_value pr_constr_pattern; pr_alias = pr_alias (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern; + pr_value pr_constr_pattern; } in make_pr_tac @@ -1330,7 +1332,7 @@ module Make let pr_top_generic env = pr_top_generic_rec (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern + pr_value pr_constr_pattern let pr_raw_extend env = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 2bc64509f0..31a5a5d4a8 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -32,7 +32,7 @@ type 'a glob_extra_genarg_printer = type 'a extra_genarg_printer = (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds val declare_extra_genarg_pprule : -- cgit v1.2.3 From ee162ba3b28fccca0a2b3ea4b1e0811006840570 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 24 Feb 2016 10:07:57 +0100 Subject: Removing the MetaIdArg entry of tactic expressions. This was historically used together with the <:tactic< ... >> quotation to insert foreign code as $foo, but it actually only survived in the implementation of Tauto. With the removal of the quotation feature, this is now totally obsolete. --- printing/pptactic.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index ed85b21478..12667d0f24 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1189,10 +1189,6 @@ module Make else str"(" ++ strm ++ str")" and pr_tacarg = function - | 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 -> -- cgit v1.2.3 From 48327426b59144f1a7181092068077c5a6df7c60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 10:45:31 +0100 Subject: Moving the "fix" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 12667d0f24..fe0be9b255 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -828,7 +828,6 @@ module Make ++ pr_opt pr_eliminator cbo) | TacCase (ev,cb) -> hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb) - | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> hov 1 ( primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() -- cgit v1.2.3 From bda8b2e8f90235ca875422f211cb781068b20b3c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 10:54:08 +0100 Subject: Moving the "cofix" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index fe0be9b255..05c3b3bf42 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -832,8 +832,6 @@ module Make 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() -- cgit v1.2.3 From d0bc16d1a0626f4137797bbf0c91e972a0ff43ac Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:05:26 +0100 Subject: Moving the "clear" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 9 --------- 1 file changed, 9 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 05c3b3bf42..c61b80c834 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -793,7 +793,6 @@ module Make let rec pr_atom0 a = tag_atom a (match a with | TacIntroPattern [] -> primitive "intros" | TacIntroMove (None,MoveLast) -> primitive "intro" - | TacClear (true,[]) -> primitive "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" ) @@ -899,14 +898,6 @@ module Make ) (* 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 () -- cgit v1.2.3 From 7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:20:26 +0100 Subject: Moving the "clearbody" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 5 ----- 1 file changed, 5 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c61b80c834..b1d6fb0c0f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -898,11 +898,6 @@ module Make ) (* Context management *) - | TacClearBody l -> - hov 1 ( - primitive "clearbody" ++ spc () - ++ prlist_with_sep spc pr.pr_name l - ) | TacMove (id1,id2) -> hov 1 ( primitive "move" -- cgit v1.2.3 From 6c4fcb156dea5a71fd227606b87333ae00aacb69 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:35:34 +0100 Subject: Moving the "generalize dependent" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 5 ----- 1 file changed, 5 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b1d6fb0c0f..f4007e25e1 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -854,11 +854,6 @@ module Make pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacGeneralizeDep c -> - hov 1 ( - primitive "generalize" ++ spc () ++ str "dependent" - ++ pr_constrarg c - ) | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) | TacLetTac (na,c,cl,b,e) -> -- cgit v1.2.3 From ae3bbff3ca2564fe24bdf3dd517c82807eae9151 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 12:11:52 +0100 Subject: Moving the "symmetry" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f4007e25e1..689ac6e4eb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -935,10 +935,6 @@ module Make ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h ) - (* Equivalence relations *) - | TacSymmetry cls -> - primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> hov 1 ( -- cgit v1.2.3 From 293222e49ff81bc1299b3822d2a8c526ca803307 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 12:40:45 +0100 Subject: Moving the "exists" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 689ac6e4eb..2c57cb811e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -725,7 +725,6 @@ module Make (* some shortcuts *) let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in - let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in let pr_with_bindings_arg_full = pr_with_bindings_arg in let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in @@ -909,13 +908,6 @@ module Make l ) - (* Constructors *) - | TacSplit (ev,l) -> - hov 1 ( - primitive (with_evars ev "exists") - ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l - ) - (* Conversion *) | TacReduce (r,h) -> hov 1 ( -- cgit v1.2.3 From 1397f791b1699b0f04d971465270d5b2df9a6d7f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 13:32:39 +0100 Subject: Moving the "move" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2c57cb811e..36863906ea 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -892,12 +892,6 @@ module Make ) (* Context management *) - | 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) -- cgit v1.2.3 From 098d283e58966124cfe0e97a3229a9e7e6284120 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Mar 2016 15:04:35 +0100 Subject: Removing the UConstr entry of the tactic_arg AST. This was redundant with the wit_uconstr generic argument, so there was no real point on keeping it there. --- printing/pptactic.ml | 7 ------- 1 file changed, 7 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 36863906ea..fdc1288aec 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -696,7 +696,6 @@ module Make type 'a printer = { pr_tactic : tolerability -> 'tacexpr -> std_ppcmds; pr_constr : 'trm -> std_ppcmds; - pr_uconstr : 'utrm -> std_ppcmds; pr_lconstr : 'trm -> std_ppcmds; pr_dconstr : 'dtrm -> std_ppcmds; pr_pattern : 'pat -> std_ppcmds; @@ -711,7 +710,6 @@ module Make constraint 'a = < term :'trm; - utrm :'utrm; dterm :'dtrm; pattern :'pat; constant :'cst; @@ -1153,8 +1151,6 @@ module Make 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 -> @@ -1182,7 +1178,6 @@ module Make let pr = { pr_tactic = pr_raw_tactic_level; pr_constr = pr_constr_expr; - pr_uconstr = pr_constr_expr; pr_dconstr = pr_constr_expr; pr_lconstr = pr_lconstr_expr; pr_pattern = pr_constr_pattern_expr; @@ -1213,7 +1208,6 @@ module Make let pr = { pr_tactic = prtac; pr_constr = pr_and_constr_expr (pr_glob_constr_env env); - pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env); pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); @@ -1255,7 +1249,6 @@ module Make let pr = { pr_tactic = pr_glob_tactic_level env; pr_constr = pr_constr_env env Evd.empty; - pr_uconstr = pr_closed_glob_env env Evd.empty; pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_lconstr_env env Evd.empty; pr_pattern = pr_constr_pattern_env env Evd.empty; -- cgit v1.2.3 From 9e96794d6a4327761ce1ff992351199919431be1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 19:01:38 +0100 Subject: Moving Tactic_debug to tactics/ folder. --- printing/pptactic.ml | 11 ----------- printing/pptacticsig.mli | 5 +++++ 2 files changed, 5 insertions(+), 11 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index fdc1288aec..7d5e7772c3 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1415,17 +1415,6 @@ let () = let printer _ _ prtac = prtac (0, E) in declare_extra_genarg_pprule wit_tactic printer printer printer -let _ = Hook.set Tactic_debug.tactic_printer - (fun x -> pr_glob_tactic (Global.env()) x) - -let _ = Hook.set Tactic_debug.match_pattern_printer - (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp) - -let _ = Hook.set Tactic_debug.match_rule_printer - (fun rl -> - pr_match_rule false (pr_glob_tactic (Global.env())) - (fun (_,p) -> pr_constr_pattern p) rl) - module Richpp = struct include Make (Ppconstr.Richpp) (struct diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index c5ec6bb092..b98b6c67e7 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -67,4 +67,9 @@ module type Pp = sig ('constr -> std_ppcmds) -> ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds + val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds + + val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('b, 'a) match_rule -> std_ppcmds + end -- cgit v1.2.3 From ffac73b8f3f3bf6877ce652eecac7849b7c2a182 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 23:00:58 +0100 Subject: Moving Autorewrite to Hightatctic. --- printing/ppvernac.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index ffec926a84..a101540aba 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -486,8 +486,6 @@ module Make keyword "Print Hint *" | PrintHintDbName s -> keyword "Print HintDb" ++ spc () ++ str s - | PrintRewriteHintDbName s -> - keyword "Print Rewrite HintDb" ++ spc() ++ str s | PrintUniverses (b, fopt) -> let cmd = if b then "Print Sorted Universes" -- cgit v1.2.3 From 4341f37cf3c51ed82c23f05846c8e6e8823d3cd6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 10 Mar 2016 19:02:16 +0100 Subject: Primitive projections: protect kernel from erroneous definitions. E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive records with eta for which conversion is incomplete. - Eta-conversion only applies to BiFinite inductives - Finiteness information is now checked by the kernel (the constructor types must be strictly non recursive for BiFinite declarations). --- printing/prettyp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fd51fd6b0f..4d9d40ae08 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -215,8 +215,8 @@ let print_polymorphism ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite -> mt () - | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion" + | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt () + | Decl_kinds.BiFinite -> str " and has eta conversion" in [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] | _ -> [] -- cgit v1.2.3 From d868820ad1f00b896c5f44f18678fac2f8e0f720 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 13:18:10 +0100 Subject: Supporting "(@foo) args" in patterns, where "@foo" has no arguments. --- printing/ppconstr.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 8a0df18ca5..1866ca5042 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -244,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 -- cgit v1.2.3 From ce2ffd090bd64963279cbbb84012d1b266ed9918 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 01:43:29 +0100 Subject: Moving VernacSolve to an EXTEND-based definition. --- printing/ppvernac.ml | 18 ------------------ 1 file changed, 18 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a101540aba..887a14d2bf 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -979,24 +979,6 @@ module Make prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) ) (* Solving *) - | VernacSolve (i,info,tac,deftac) -> - let pr_goal_selector = function - | SelectNth i -> int i ++ str":" - | SelectId id -> pr_id id ++ str":" - | SelectAll -> str"all" ++ str":" - | SelectAllParallel -> str"par" - in - let pr_info = - match info with - | None -> mt () - | Some i -> str"Info"++spc()++int i++spc() - in - return ( - (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++ - pr_info ++ - pr_raw_tactic tac - ++ (if deftac then str ".." else mt ()) - ) | VernacSolveExistential (i,c) -> return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) -- cgit v1.2.3 From 2cf8f76ea6a15d46b57d5c4ecf9513683561e284 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 18:46:54 +0100 Subject: Removing the untyped representation of genargs. --- printing/genprint.ml | 5 +++-- printing/pptactic.ml | 4 ++-- 2 files changed, 5 insertions(+), 4 deletions(-) (limited to 'printing') diff --git a/printing/genprint.ml b/printing/genprint.ml index d8bd81c4cc..0ec35e07be 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 ""); glb = (fun _ -> str ""); diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7d5e7772c3..d99a5f0d89 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -67,8 +67,8 @@ type 'a extra_genarg_printer = 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 -- cgit v1.2.3 From 0af598b77a6242d796c66884477a046448ef1e21 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 01:31:43 +0100 Subject: Moving Tactic Notation to an EXTEND based command. --- printing/ppvernac.ml | 13 ------------- 1 file changed, 13 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 887a14d2bf..88bb805a72 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -378,17 +378,6 @@ 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 () @@ -644,8 +633,6 @@ module Make return (keyword "No-parsing-rule for VernacError") (* Syntax *) - | VernacTacticNotation (n,r,e) -> - return (pr_grammar_tactic_rule n ("",r,e)) | VernacOpenCloseScope (_,(opening,sc)) -> return ( keyword (if opening then "Open " else "Close ") ++ -- cgit v1.2.3 From 01cd0dd64e4faa52b5094a99e2c31ecc4e7b767d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 02:09:54 +0100 Subject: Moving Print Ltac to an EXTEND based command. --- printing/ppvernac.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 88bb805a72..edd32e8337 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -455,8 +455,6 @@ module Make keyword "Print TypeClasses" | PrintInstances qid -> keyword "Print Instances" ++ spc () ++ pr_smart_global qid - | PrintLtac qid -> - keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid | PrintCoercions -> keyword "Print Coercions" | PrintCoercionPaths (s,t) -> -- cgit v1.2.3 From 4f52bd681ad9bbcbbd68406a58b47d8e962336ed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 02:23:21 +0100 Subject: Moving the Ltac definition command to an EXTEND based command. --- printing/ppvernac.ml | 23 ----------------------- 1 file changed, 23 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index edd32e8337..c1f5e122bd 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -995,29 +995,6 @@ module Make return (keyword "Cd" ++ pr_opt qs s) (* Commands *) - | VernacDeclareTacticDefinition l -> - let pr_tac_body tacdef_body = - let id, redef, body = - match tacdef_body with - | TacticDefinition ((_,id), body) -> pr_id id, false, body - | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body - in - let idl, body = - match body with - | Tacexpr.TacFun (idl,b) -> idl,b - | _ -> [], body in - 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 () ++ -- cgit v1.2.3 From 93a77f3cb8ee36072f93b4c0ace6f0f9c19f51a3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 18:41:37 +0100 Subject: Moving Refine to its proper module. --- printing/printer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index b89005887f..2e67fa5ff1 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -50,7 +50,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 -- cgit v1.2.3 From dc7b77f09fe5e59e6e48486d9a8c0bdc6acf83b7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 16:59:15 +0100 Subject: Adding a new Ltac generic argument for forced tactics returing unit. --- printing/pptactic.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index d99a5f0d89..982c18ec61 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1415,6 +1415,11 @@ let () = let printer _ _ prtac = prtac (0, E) in declare_extra_genarg_pprule wit_tactic printer printer printer +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 include Make (Ppconstr.Richpp) (struct -- cgit v1.2.3 From 7e7b5684d8f8066b90fca3395104af7241b8aed6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 25 Mar 2016 16:46:50 +0100 Subject: Univs: fix get_current_context (bug #4603, part I) Return an evar_map with the right universes, when there are no focused subgoals or the proof is finished. --- printing/printer.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index 63755d7ff7..4e740bffe2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -30,7 +30,8 @@ let delayed_emacs_cmd s = let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> - (Evd.empty, Global.env()) + let env = Global.env () in + (Evd.from_env env, env) (**********************************************************************) (** Terms *) -- cgit v1.2.3 From 1f6a31d138bcfcf341f28772de7c5e08906167c5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 8 Apr 2016 00:19:49 +0200 Subject: Fixing printing of Tactic Notations with tactic arguments. --- printing/pptactic.ml | 36 +++++++++++++++++++----------------- 1 file changed, 19 insertions(+), 17 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 982c18ec61..c175b206db 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -341,11 +341,9 @@ module Make | [], [] -> [] | _ -> failwith "Inconsistent arguments of extended tactic" - type any_arg = AnyArg : 'a Genarg.raw_abstract_argument_type -> any_arg - let filter_arg = function | Egramml.GramTerminal _ -> None - | Egramml.GramNonTerminal (_, t, _) -> Some (AnyArg t) + | Egramml.GramNonTerminal (_, Rawwit t, _) -> Some (ArgumentType t) let pr_tacarg_using_rule pr_gen l = let l = match l with @@ -386,25 +384,25 @@ module Make with Not_found -> KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" - let check_type t arg = match t, arg with - | AnyArg t, TacGeneric arg -> argument_type_eq (unquote t) (genarg_tag arg) - | _ -> false + let check_type t arg = match arg with + | TacGeneric arg -> argument_type_eq t (genarg_tag arg) + | _ -> argument_type_eq t (ArgumentType wit_tactic) - let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false + let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg)) let pr_raw_extend_rec prc prlc prtac prpat = - pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) + pr_extend_gen check_type (pr_farg prtac) let pr_glob_extend_rec prc prlc prtac prpat = - pr_extend_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) + pr_extend_gen check_type (pr_farg prtac) let pr_extend_rec prc prlc prtac prpat = - pr_extend_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) + pr_extend_gen check_type (pr_farg prtac) let pr_raw_alias prc prlc prtac prpat = - pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) + pr_alias_gen check_type (pr_farg prtac) let pr_glob_alias prc prlc prtac prpat = - pr_alias_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) + pr_alias_gen check_type (pr_farg prtac) let pr_alias prc prlc prtac prpat = - pr_alias_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) + pr_alias_gen check_type (pr_farg prtac) (**********************************************************************) (* The tactic printer *) @@ -1185,7 +1183,7 @@ 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_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 @@ -1215,7 +1213,9 @@ 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_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)); @@ -1256,7 +1256,9 @@ module Make 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_generic = pr_top_generic_rec + (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) + pr_value pr_constr_pattern; pr_extend = pr_extend_rec (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) pr_value pr_constr_pattern; @@ -1291,7 +1293,7 @@ module Make (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) let check_val_type t arg = - let AnyArg t = t in + let ArgumentType t = t in (* let t = Genarg.val_tag (Obj.magic t) in *) (* let Val.Dyn (t', _) = arg in *) (* match Genarg.Val.eq t t' with *) -- cgit v1.2.3 From b5420538da04984ca42eb4284a9be27f3b5ba021 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 8 Apr 2016 00:58:56 +0200 Subject: Fixing printing of toplevel values. This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all. --- printing/pptactic.ml | 24 ++++++++++++++++++++---- printing/pptacticsig.mli | 2 ++ 2 files changed, 22 insertions(+), 4 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c175b206db..355a6a7d64 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -106,7 +106,23 @@ module Make let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) - let pr_value _ _ = str "(* FIXME *)" + let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with + | Val.List tag -> + pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x + | Val.Opt tag -> pr_opt (fun x -> pr_value lev (Val.Dyn (tag, x))) x + | Val.Pair (tag1, tag2) -> + str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++ + pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")" + | Val.Base t -> + let name = Val.repr t 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.eq (val_tag (Topwit wit)) (Val.Base t) with + | None -> default + | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) let pr_with_occurrences pr (occs,c) = match occs with @@ -1245,7 +1261,7 @@ module Make let typed_printers = (strip_prod_binders_constr) in - let prtac n (t:tactic_expr) = + let rec prtac n (t:tactic_expr) = let pr = { pr_tactic = pr_glob_tactic_level env; pr_constr = pr_constr_env env Evd.empty; @@ -1261,10 +1277,10 @@ module Make pr_value pr_constr_pattern; pr_extend = pr_extend_rec (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - pr_value pr_constr_pattern; + prtac pr_constr_pattern; pr_alias = pr_alias (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - pr_value pr_constr_pattern; + prtac pr_constr_pattern; } in make_pr_tac diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index b98b6c67e7..95cf541fd7 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -72,4 +72,6 @@ module type Pp = sig 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 -- cgit v1.2.3 From ce71ac17268f11ddd92f4bea85cbdd9c62acbc21 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 9 Apr 2016 11:56:53 +0200 Subject: In pr_clauses, do not print a leading space by default so that it can be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND. --- printing/pptactic.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 355a6a7d64..7dae97acf2 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -542,7 +542,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 () @@ -829,7 +829,7 @@ module Make (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 + pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp ) | TacElim (ev,cb,cbo) -> hov 1 ( @@ -873,7 +873,7 @@ module Make (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) + 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" :=" ++ @@ -918,7 +918,7 @@ module Make | TacReduce (r,h) -> hov 1 ( pr_red_expr r - ++ pr_clauses (Some true) pr.pr_name h + ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h ) | TacChange (op,c,h) -> hov 1 ( @@ -930,7 +930,7 @@ module Make | Some p -> pr.pr_pattern p ++ spc () ++ keyword "with" ++ spc () - ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h + ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h ) (* Equality and inversion *) @@ -943,7 +943,7 @@ module Make 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 + ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl ++ ( match by with | Some by -> pr_by_tactic (pr.pr_tactic ltop) by @@ -962,14 +962,14 @@ module Make 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 + ++ 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_simple_hyp_clause pr.pr_name cl + ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl ) ) in -- cgit v1.2.3 From b5cc4ac65764b0866bf57caa6f9aa7fa631eabf1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 9 Apr 2016 16:14:29 +0200 Subject: Fixing extra space in printing inductive types with no explicit type given. --- printing/ppvernac.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 55f8f909f0..0b761881dc 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -778,8 +778,8 @@ module Make 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 ++ + 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 -- cgit v1.2.3 From fa2fa0b2e6ca0fbfb9a9278af211d4ef533b6791 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 9 Apr 2016 16:15:15 +0200 Subject: Simplifying code for printing VERNAC EXTEND. --- printing/ppvernac.ml | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 0b761881dc..9054ba0b67 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1213,22 +1213,15 @@ module Make with Failure _ -> str "" in try let rl = Egramml.get_extend_vernac_rule s in - let start,rl,cl = - match rl with - | Egramml.GramTerminal s :: rl -> str s, rl, cl - | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl - | [] -> anomaly (Pp.str "Empty entry") in - let (pp,_) = - List.fold_left - (fun (strm,args) pi -> - let pp,args = match pi with - | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args) - | Egramml.GramTerminal s -> (str s, args) in - (strm ++ spc() ++ pp), args) - (start,cl) rl in - hov 1 pp + 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) ++ prlist_with_sep sep pr_arg cl ++ str ")") + hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") in pr_vernac -- cgit v1.2.3 From a2664de27eabbba7fc357305679112aef99e1f74 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 9 Apr 2016 16:39:55 +0200 Subject: Removing automatic printing of leading space in auto_using and hintbases so that it does not put extra space when auto is defined as a TACTIC EXTEND. --- printing/pptactic.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7dae97acf2..7d7ebd1416 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -675,15 +675,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) + | l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l) let pr_then () = str ";" -- cgit v1.2.3 From a2d3f5fc3167962f9bf549ba32f0105fff766422 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 9 Apr 2016 17:10:10 +0200 Subject: Removing extra spaces in printing arguments of VERNAC EXTEND. --- printing/pptactic.ml | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7d7ebd1416..4b2dc49a5e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -109,7 +109,7 @@ module Make let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with | Val.List tag -> pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x - | Val.Opt tag -> pr_opt (fun x -> pr_value lev (Val.Dyn (tag, x))) x + | Val.Opt tag -> pr_opt_no_spc (fun x -> pr_value lev (Val.Dyn (tag, x))) x | Val.Pair (tag1, tag2) -> str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")" @@ -282,24 +282,25 @@ 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_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) = match wit with | ListArg wit -> let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in let ans = pr_sequence map x in - hov 0 ans + hov_if_not_empty 0 ans | OptArg wit -> let ans = match x with | None -> mt () | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - hov 0 ans + 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 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q]) + 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) @@ -310,19 +311,19 @@ module Make | ListArg wit -> let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in let ans = pr_sequence map x in - hov 0 ans + hov_if_not_empty 0 ans | OptArg wit -> let ans = match x with | None -> mt () | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in - hov 0 ans + 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 0 ans + 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) @@ -332,19 +333,19 @@ module Make | ListArg wit -> let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in let ans = pr_sequence map x in - hov 0 ans + hov_if_not_empty 0 ans | OptArg wit -> let ans = match x with | None -> mt () | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in - hov 0 ans + hov_if_not_empty 0 ans | PairArg (wit1, wit2) -> let p, q = x in let p = in_gen (topwit wit1) p in let q = in_gen (topwit wit2) q in let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in - hov 0 ans + hov_if_not_empty 0 ans | ExtraArg s -> try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x) with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x) -- cgit v1.2.3 From 4ebc7c27f04f2bcc3cf7160ae9ec177d1ca11707 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 10 Apr 2016 02:24:17 +0200 Subject: Extruding the print_atom primitive. --- printing/pptactic.ml | 469 +++++++++++++++++++++++++-------------------------- 1 file changed, 234 insertions(+), 235 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 4b2dc49a5e..1e6c46e759 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -732,247 +732,246 @@ module Make level :'lev > - let make_pr_tac pr strip_prod_binders tag_atom tag = - - (* some shortcuts *) - let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in - let pr_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 rec 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 [] -> primitive "intros" + | TacIntroMove (None,MoveLast) -> primitive "intro" + | 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_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_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 + ) + | 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))) + *) - let extract_binders = function - | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body) - | body -> ([],body) 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 ((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 + ) - 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" - | 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_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_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 - ) - | 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))) - *) - - (* 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 - ) + (* Context management *) + | 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 + ) - (* Context management *) - | 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 - ) + (* 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 + ) - (* 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 + (* 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_non_empty_arg (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_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 - (* 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_non_empty_arg (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_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 + 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 rec pr_tac inherited tac = let return (doc, l) = (tag tac doc, l) in let (strm, prec) = return (match tac with @@ -1130,7 +1129,7 @@ module Make | 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)) -> -- cgit v1.2.3 From 2da7bf6327e1f35321f121de9560604b758f0472 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 10 Apr 2016 02:37:41 +0200 Subject: Removing the ad-hoc tactic_expr type. This type was actually only used by the debug printer of tactics, and only for atomic tactics. Furthermore, that type was asymmetric, as the underlying tacexpr type was set to be glob_tactic, when the semantics would have required a Val.t type. Furthermore, this type is absent from every contrib I have seen, which hints again in favour of its lack of meaning. --- printing/ppannotation.ml | 2 -- printing/ppannotation.mli | 1 - printing/pptactic.ml | 44 ++++++++++++-------------------------------- printing/pptacticsig.mli | 2 +- printing/richprinter.ml | 1 - printing/richprinter.mli | 3 --- 6 files changed, 13 insertions(+), 40 deletions(-) (limited to 'printing') diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml index df7f925b73..511f93569c 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 84724053ed..a0fef1a757 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/pptactic.ml b/printing/pptactic.ml index 1e6c46e759..3cff541b06 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -94,8 +94,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) @@ -411,15 +409,11 @@ module Make pr_extend_gen check_type (pr_farg prtac) let pr_glob_extend_rec prc prlc prtac prpat = pr_extend_gen check_type (pr_farg prtac) - let pr_extend_rec prc prlc prtac prpat = - pr_extend_gen check_type (pr_farg prtac) let pr_raw_alias prc prlc prtac prpat = pr_alias_gen check_type (pr_farg prtac) let pr_glob_alias prc prlc prtac prpat = pr_alias_gen check_type (pr_farg prtac) - let pr_alias prc prlc prtac prpat = - pr_alias_gen check_type (pr_farg prtac) (**********************************************************************) (* The tactic printer *) @@ -528,9 +522,8 @@ module Make | ipat -> spc() ++ prc c ++ pr_as_ipat prdc ipat - let pr_by_tactic prt = function - | TacId [] -> mt () - | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac + let pr_by_tactic prt tac = + spc() ++ keyword "by" ++ spc () ++ prt tac let pr_hyp_location pr_id = function | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs @@ -732,7 +725,7 @@ module Make level :'lev > - let rec pr_atom pr strip_prod_binders tag_atom = + 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 @@ -1255,13 +1248,10 @@ 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 rec 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 ""); pr_constr = pr_constr_env env Evd.empty; pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_lconstr_env env Evd.empty; @@ -1270,21 +1260,13 @@ module Make pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; - pr_generic = pr_top_generic_rec - (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - pr_value pr_constr_pattern; - pr_extend = pr_extend_rec - (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - prtac pr_constr_pattern; - pr_alias = pr_alias - (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - prtac 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 @@ -1321,7 +1303,7 @@ module Make let pr_extend pr lev ml args = pr_extend_gen check_val_type pr lev ml args - let pr_tactic env = pr_tactic_level env ltop + let pr_atomic_tactic env = pr_atomic_tactic_level env ltop end @@ -1351,7 +1333,6 @@ 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) @@ -1449,7 +1430,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/pptacticsig.mli b/printing/pptacticsig.mli index 95cf541fd7..d4858bac4f 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -57,7 +57,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 diff --git a/printing/richprinter.ml b/printing/richprinter.ml index d95e190749..5f39f36eab 100644 --- a/printing/richprinter.ml +++ b/printing/richprinter.ml @@ -22,4 +22,3 @@ let make_richpp pr ast = 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 index 261d22c4c3..c9e84e3eb4 100644 --- a/printing/richprinter.mli +++ b/printing/richprinter.mli @@ -34,6 +34,3 @@ 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 -- cgit v1.2.3 From d78784bd86d3d571bb2891356e9e9718c69976ba Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 10 Apr 2016 14:30:25 +0200 Subject: Fixing printing of "destruct in" after ce71ac17268f. --- printing/pptactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 3cff541b06..19536d9f83 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -878,7 +878,7 @@ module Make ++ 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_clauses None pr.pr_name) cl) l ++ pr_opt pr_eliminator el ) | TacDoubleInduction (h1,h2) -> -- cgit v1.2.3 From 87a81fd7e6ff6b45c76690471eb671ba4b005338 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 Apr 2016 18:59:16 +0200 Subject: Moving and enhancing the grammar_tactic_prod_item_expr type. --- printing/ppvernac.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9054ba0b67..f0548238a7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -104,12 +104,6 @@ module Make 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, (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")" - | TacTerm s -> qs s - let pr_comment pr_c = function | CommentConstr c -> pr_c c | CommentString s -> qs s -- cgit v1.2.3