diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /plugins/funind/g_indfun.ml4 | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 80 |
1 files changed, 30 insertions, 50 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 42e49031..90af20b4 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -1,47 +1,32 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) -open Compat +open Ltac_plugin open Util -open Term open Pp open Constrexpr open Indfun_common open Indfun open Genarg -open Constrarg +open Stdarg open Misctypes +open Pcoq open Pcoq.Prim open Pcoq.Constr -open Pcoq.Tactic +open Pltac DECLARE PLUGIN "recdef_plugin" -let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - -let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence prc l - | ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - -let pr_with_bindings prc prlc (c,bl) = - prc c ++ hv 0 (pr_bindings prc prlc bl) - let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () - | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc b) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) (* Duplication of printing functions because "'a with_bindings" is (internally) not uniform in 'a: indeed constr_with_bindings at the @@ -49,16 +34,12 @@ let pr_fun_ind_using prc prlc _ opt_c = "constr with_bindings"; hence, its printer cannot be polymorphic in (prc,prlc)... *) -let pr_with_bindings_typed prc prlc (c,bl) = - prc c ++ - hv 0 (pr_bindings prc prlc bl) - let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () | Some b -> - let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in - spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b) + let (_, b) = b (Global.env ()) Evd.empty in + spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) ARGUMENT EXTEND fun_ind_using @@ -80,7 +61,6 @@ TACTIC EXTEND newfuninv ] END - let pr_intro_as_pat _prc _ _ pat = match pat with | Some pat -> @@ -88,16 +68,17 @@ let pr_intro_as_pat _prc _ _ pat = str"<simple_intropattern>" | None -> mt () -let out_disjunctive = function - | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) - | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected." +let out_disjunctive = CAst.map (function + | IntroAction (IntroOrAndPattern l) -> l + | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.")) ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] | [] ->[ None ] END - +let functional_induction b c x pat = + Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat)) TACTIC EXTEND newfunind @@ -106,9 +87,9 @@ TACTIC EXTEND newfunind let c = match cl with | [] -> assert false | [c] -> c - | c::cl -> applist(c,cl) + | c::cl -> EConstr.applist(c,cl) in - Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))) princl ] + Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ] END (***** debug only ***) TACTIC EXTEND snewfunind @@ -117,9 +98,9 @@ TACTIC EXTEND snewfunind let c = match cl with | [] -> assert false | [c] -> c - | c::cl -> applist(c,cl) + | c::cl -> EConstr.applist(c,cl) in - Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x (Option.map out_disjunctive pat))) princl ] + Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ] END @@ -143,7 +124,7 @@ END module Gram = Pcoq.Gram module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic +module Tactic = Pltac type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located @@ -157,15 +138,14 @@ GEXTEND Gram GLOBAL: function_rec_definition_loc ; function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> !@loc, g ]] + [ [ g = Vernac.rec_definition -> Loc.tag ~loc:!@loc g ]] ; END let () = let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in - let printer _ _ _ _ = str "<Unavailable printer for rec_definition>" in - Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function @@ -175,7 +155,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) @@ -184,13 +164,13 @@ VERNAC COMMAND EXTEND Function END let pr_fun_scheme_arg (princ_name,fun_name,s) = - Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ + Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ - Ppconstr.pr_glob_sort s + Termops.pr_sort_family s VERNAC ARGUMENT EXTEND fun_scheme_arg PRINTED BY pr_fun_scheme_arg -| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] +| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> [ (princ_name,fun_name,s) ] END @@ -227,7 +207,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> - CErrors.error ("Cannot generate induction principle(s)") + CErrors.user_err Pp.(str "Cannot generate induction principle(s)") | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e |