1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
27 let induction_tac ~term ~status:((proof,goal) as status) =
29 let module R = CicReduction in
30 let module P = PrimitiveTactics in
31 let module T = Tacticals in
32 let module S = ProofEngineStructuralRules in
33 let module U = UriManager in
34 let (_,metasenv,_,_) = proof in
35 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
36 let termty = T.type_of_aux' metasenv context term in
37 let uri,exp_named_subst,typeno,args =
39 C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
40 | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> (uri,exp_named_subst,typeno,args)
41 | _ -> raise (ProofEngineTypes.Fail "Induction: Not an Inductive Type to Eliminate")
44 let base = U.buri_of_uri uri in
46 match CicEnvironment.get_obj uri with
47 C.InductiveDefinition (tys,_,_) ->
48 let (name,_,_,_) = List.nth tys typeno in
53 match T.type_of_aux' metasenv context ty with
54 C.Sort C.Prop -> "_ind"
55 | C.Sort C.Set -> "_rec"
56 | C.Sort C.Type -> "_rect"
59 U.uri_of_string (base ^ "/" ^ name ^ ext ^ ".con")
61 apply_tac ~term:(C.Const (eliminator_uri , exp_named_subst)) (* come mi devo comportare con gli args??? *)
65 let elim_type_tac ~term ~status =
67 let module P = PrimitiveTactics in
68 let module T = Tacticals in
70 ~start: (P.cut_tac ~term)
71 ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
75 (* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-)
76 let elim_type_tac ~term ~status =
77 warn "in Ring.elim_type_tac";
78 Tacticals.thens ~start:(cut_tac ~term)
79 ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
85 (* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *)
86 let decompose_tac ~what ~where ~status:((proof,goal) as status) =
88 let module R = CicReduction in
89 let module P = PrimitiveTactics in
90 let module T = Tacticals in
91 let module S = ProofEngineStructuralRules in
93 let rec decomposing ty what =
95 [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *)
98 (C.Appl (hd::_)) -> hd
99 | _ -> decomposing ty tl
102 let (_,metasenv,_,_) = proof in
103 let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
106 ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what))
107 ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where)))) (* ma che ipotesi sto cancellando??? *)
113 let decompose_tac ~clist ~status:((proof,goal) as status) =
114 let module C = Cic in
115 let module R = CicReduction in
116 let module P = PrimitiveTactics in
117 let module T = Tacticals in
118 let module S = ProofEngineStructuralRules in
119 let (_,metasenv,_,_) = proof in
120 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
122 let rec repeat_elim ~term ~status = (* term -> status -> proof * (goal list) *)
124 let (proof, goallist) =
126 ~start:(P.elim_simpl_intros_tac ~term)
127 ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty)))) (* non so che ipotesi sto cancellando??? *)
130 let rec step proof goallist =
134 let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in
135 let (proof'', goallist'') = step proof' tl in
136 proof'', goallist'@goallist''
143 let rec decomposing ty clist = (* term -> (term list) -> bool *)
148 (C.Appl (hd::_)) -> true
149 | _ -> decomposing ty tl
152 let term = decomposing (R.whd context ty) clist in
153 if (term == C.Implicit)
154 then (Fail "Decompose: nothing to decompose or no application")
155 else repeat_elim ~term ~status
159 let decompose_tac ~clist ~status =
160 let module C = Cic in
161 let module R = CicReduction in
162 let module P = PrimitiveTactics in
163 let module T = Tacticals in
164 let module S = ProofEngineStructuralRules in
168 [] -> C.Implicit (* a cosa serve? *)
171 (C.Appl (hd::_)) -> hd
175 let decompose_one_tac ~clist ~status:((proof,goal) as status) =
176 let (_,metasenv,_,_) = proof in
177 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
178 let term = choose (R.whd context ty) clist in
179 if (term == C.Implicit)
180 then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
182 ~start:(P.elim_intros_simpl_tac ~term)
183 ~continuation:(S.clear ~hyp:(List.hd context))
184 (* (S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty)))) (* ma che ipotesi sto cancellando??? *)*)
187 T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status