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 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
28 let assumption_tac ~status:((proof,goal) as status) =
30 let module R = CicReduction in
31 let module S = CicSubstitution in
32 let _,metasenv,_,_ = proof in
33 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
34 let rec find n = function
37 (Some (_, C.Decl t)) when
38 (R.are_convertible context (S.lift n t) ty) -> n
39 | (Some (_, C.Def t)) when
40 (R.are_convertible context
41 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
44 | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
45 in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
48 (* Questa invece era in fourierR.ml
49 let assumption_tac ~status:(proof,goal)=
50 let curi,metasenv,pbo,pty = proof in
51 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
53 let tac_list = List.map
54 ( fun x -> num := !num + 1;
56 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
57 | _ -> ("fake",tcl_fail 1)
61 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
66 (* ANCORA DA DEBUGGARE *)
69 (* IN FASE DI IMPLEMENTAZIONE *)
71 let generalize_tac ~term ~status:((proof,goal) as status) =
73 let module P = PrimitiveTactics in
74 let module T = Tacticals in
75 let _,metasenv,_,_ = proof in
76 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
80 C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 2, []) ;
81 C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 1, [])]) in
82 let tuno = CicTypeChecker.type_of_aux' metasenv context uno in
83 prerr_endline ("#### uno: " ^ CicPp.ppterm uno);
84 prerr_endline ("#### tuno: " ^ CicPp.ppterm tuno);
86 prerr_endline ("#### dummy: " ^ (CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv context term)));
87 prerr_endline ("#### with_what: " ^ CicPp.ppterm (C.Rel 1));
88 prerr_endline ("#### term: " ^ CicPp.ppterm term);
89 prerr_endline ("#### ty: " ^ CicPp.ppterm ty);
96 (C.Name "dummy_for_gen"),
97 (CicTypeChecker.type_of_aux' metasenv context term),
98 (ProofEngineReduction.replace_lifting
100 ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
104 [T.id_tac ; (P.apply_tac ~term:(C.Appl [(C.Rel 1); term]))] (* in quest'ordine o viceversa? provare *)
105 (* [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac] (* in quest'ordine o viceversa? provare *)*)
110 let generalize_tac ~term ~status:((proof,goal) as status) =
111 let module C = Cic in
112 let module H = ProofEngineHelpers in
113 let module P = PrimitiveTactics in
114 let module T = Tacticals in
115 let _,metasenv,_,_ = proof in
116 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
118 let add_decl_tac ~term ~status:(proof, goal) =
119 let module C = Cic in
120 let curi,metasenv,pbo,pty = proof in
121 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
122 let _ = CicTypeChecker.type_of_aux' metasenv context term in
123 let newmeta = H.new_meta ~proof in
124 let context_for_newmeta = (Some (C.Name "dummy_for_gen",C.Decl term))::context in
125 let irl = H.identity_relocation_list_for_metavariable context_for_newmeta in
126 let newmetaty = CicSubstitution.lift 1 ty in
127 let bo' = C.LetIn (C.Name "dummy_for_gen" , term , C.Meta (newmeta,irl)) in
128 let (newproof, _) = H.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty]
130 (newproof, [newmeta])
134 ~start:(add_decl_tac ~term:(CicTypeChecker.type_of_aux' metasenv context term))
137 ~start:(P.cut_tac ~term:(ProofEngineReduction.replace
139 ~with_what:(C.Rel 1) (* dummy_for_gen *)
143 [T.id_tac ; (P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)]))]) (* in quest'ordine o viceversa? provare *)
144 (* [(P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)])) ; T.id_tac]) in quest'ordine o viceversa? provare *)
151 let decide_equality_tac =
156 let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
157 let module C = Cic in
158 let module U = UriManager in
159 let module P = PrimitiveTactics in
160 let module T = Tacticals in
161 let _,metasenv,_,_ = proof in
162 let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
163 if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
164 (* controllo che i due termini siano comparabili *)
167 ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
168 ~continuations:[split_tac ; P.intros_tac ~name:"FOO"]
169 else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
177 - come faccio clear di un ipotesi di cui non so il nome?
178 - differenza tra elim e induction ...e inversion?
179 - come passo a decompose la lista di termini?
180 - ma la rewrite funzionava?
181 - come implemento la generalize?