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 *)
68 let generalize_tac ~term ~status:((proof,goal) as status) =
70 let module P = PrimitiveTactics in
71 let module T = Tacticals in
72 let _,metasenv,_,_ = proof in
73 let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
78 (C.Name "dummy_for_gen")),
79 (CicTypeChecker.type_of_aux' metasenv context term)),
80 (ProofEngineReduction.replace_lifting_csc 1
83 ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
86 ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
91 (* IN FASE DI IMPLEMENTAZIONE *)
93 let decide_equality_tac =
98 let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
100 let module U = UriManager in
101 let module P = PrimitiveTactics in
102 let module T = Tacticals in
103 let _,metasenv,_,_ = proof in
104 let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
105 if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
106 (* controllo che i due termini siano comparabili *)
109 ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
110 ~continuations:[split_tac ; P.intros_tac ~name:"FOO"]
111 else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
119 - field, omega... come ring?