|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
inductive.ML
Sprache: SML
Haftungsausschluß.mlg KontaktText {Text[63] Isabelle[125] Abap[217]}diese Dinge liegen außhalb unserer Verantwortung
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
{
open Ltac_plugin
open Util
open Pp
open Constrexpr
open Indfun_common
open Indfun
open Stdarg
open Tacarg
open Tactypes
open Pcoq.Prim
open Pcoq.Constr
open Pltac
}
DECLARE PLUGIN "recdef_plugin"
{
let pr_fun_ind_using env sigma prc prlc _ opt_c =
match opt_c with
| None -> mt ()
| Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env sigma) (prlc env sigma) b)
(* Duplication of printing functions because "'a with_bindings" is
(internally) not uniform in 'a: indeed constr_with_bindings at the
"typed" level has type "open_constr with_bindings" instead of
"constr with_bindings"; hence, its printer cannot be polymorphic in
(prc,prlc)... *)
let pr_fun_ind_using_typed prc prlc _ opt_c =
match opt_c with
| None -> mt ()
| Some b ->
let env = Global.env () in
let evd = Evd.from_env env in
let (_, b) = b env evd in
spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env evd) (prlc env evd) b)
}
ARGUMENT EXTEND fun_ind_using
TYPED AS constr_with_bindings option
PRINTED BY { pr_fun_ind_using_typed }
RAW_PRINTED BY { pr_fun_ind_using env sigma }
GLOB_PRINTED BY { pr_fun_ind_using env sigma }
| [ "using" constr_with_bindings(c) ] -> { Some c }
| [ ] -> { None }
END
TACTIC EXTEND newfuninv
| [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] ->
{
Proofview.V82.tactic (Invfun.invfun hyp fname)
}
END
{
let pr_intro_as_pat _prc _ _ pat =
match pat with
| Some pat ->
spc () ++ str "as" ++ spc () ++ (* Miscprint.pr_intro_pattern prc pat *)
str"<simple_intropattern>"
| None -> mt ()
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 intro_pattern option 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
| ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
{
let c = match cl with
| [] -> assert false
| [c] -> c
| c::cl -> EConstr.applist(c,cl)
in
Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl }
END
(***** debug only ***)
TACTIC EXTEND snewfunind
| ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
{
let c = match cl with
| [] -> assert false
| [c] -> c
| c::cl -> EConstr.applist(c,cl)
in
Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl }
END
{
let pr_constr_comma_sequence env sigma prc _ _ = prlist_with_sep pr_comma (prc env sigma)
}
ARGUMENT EXTEND constr_comma_sequence'
TYPED AS constr list
PRINTED BY { pr_constr_comma_sequence env sigma }
| [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l }
| [ constr(c) ] -> { [c] }
END
{
let pr_auto_using env sigma prc _prlc _prt = Pptactic.pr_auto_using (prc env sigma)
}
ARGUMENT EXTEND auto_using'
TYPED AS constr list
PRINTED BY { pr_auto_using env sigma }
| [ "using" constr_comma_sequence'(l) ] -> { l }
| [ ] -> { [] }
END
{
module Vernac = Pvernac.Vernac_
module Tactic = Pltac
type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
Genarg.create_arg "function_rec_definition_loc"
let function_rec_definition_loc =
Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
}
GRAMMAR EXTEND Gram
GLOBAL: function_rec_definition_loc ;
function_rec_definition_loc:
[ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]]
;
END
{
let () =
let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
}
(* TASSI: n'importe quoi ! *)
VERNAC COMMAND EXTEND Function
| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
=> { let hard = List.exists (function
| _,((_,(Some { CAst.v = CMeasureRec _ }
| Some { CAst.v = CWfRec _}),_,_,_),_) -> true
| _,((_,Some { CAst.v = CStructRec _ },_,_,_),_)
| _,((_,None,_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
(Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
with
| Vernacextend.VtSideff ids, _ when hard ->
Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
| x -> x }
-> { do_generate_principle false (List.map snd recsl) }
END
{
let pr_fun_scheme_arg (princ_name,fun_name,s) =
Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++
Sorts.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_family(s) ] -> { (princ_name,fun_name,s) }
END
{
let warning_error names e =
let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
match e with
| Building_graph e ->
let names = pr_enum Libnames.pr_qualid names in
let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
warn_cannot_define_graph (names,error)
| Defining_principle e ->
let names = pr_enum Libnames.pr_qualid names in
let error = if do_observe () then CErrors.print e else mt () in
warn_cannot_define_principle (names,error)
| _ -> raise e
}
VERNAC COMMAND EXTEND NewFunctionalScheme
| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
=> { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
->
{ fun ~pstate ->
begin
try
Functional_principles_types.build_scheme fas; pstate
with
| Functional_principles_types.No_graph_found ->
begin
match fas with
| (_,fun_name,_)::_ ->
begin
let pstate = make_graph ~pstate (Smartlocate.global_with_alias fun_name) in
try Functional_principles_types.build_scheme fas; pstate
with
| Functional_principles_types.No_graph_found ->
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; pstate
end
| _ -> assert false (* we can only have non empty list *)
end
| e when CErrors.noncritical e ->
let names = List.map (fun (_,na,_) -> na) fas in
warning_error names e; pstate
end
}
END
(***** debug only ***)
VERNAC COMMAND EXTEND NewFunctionalCase
| ["Functional" "Case" fun_scheme_arg(fas) ]
=> { Vernacextend.(VtSideff[pi1 fas], VtLater) }
-> { Functional_principles_types.build_case_scheme fas }
END
(***** debug only ***)
VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
| ![ proof ] ["Generate" "graph" "for" reference(c)] ->
{ make_graph (Smartlocate.global_with_alias c) }
END
[ Seitenstruktur1.78Drucken
]
|
|
|
|
|
|
