]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/proofEngineStructuralRules.ml
we were generating a name for the main fix twice
[helm.git] / helm / software / components / tactics / proofEngineStructuralRules.ml
1 (* Copyright (C) 2002, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
28 module PET = ProofEngineTypes
29 module C = Cic
30
31 let clearbody ~hyp = 
32  let clearbody (proof, goal) =
33    let curi,metasenv,_subst,pbo,pty, attrs = proof in
34     let metano,_,_ = CicUtil.lookup_meta goal metasenv in
35      let string_of_name =
36       function
37          C.Name n -> n
38        | C.Anonymous -> "_"
39      in
40      let metasenv' =
41       List.map
42        (function
43            (m,canonical_context,ty) when m = metano ->
44              let canonical_context' =
45               List.fold_right
46                (fun entry context ->
47                  match entry with
48                     Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' ->
49                      let cleared_entry = Some (C.Name hyp, Cic.Decl ty) in
50                       cleared_entry::context
51                   | None -> None::context
52                   | Some (n,C.Decl t) ->
53                      let _,_ =
54                       try
55                        CicTypeChecker.type_of_aux' metasenv context t
56                         CicUniv.oblivion_ugraph (* TASSI: FIXME *)
57                       with
58                        _ ->
59                          raise
60                           (PET.Fail
61                             (lazy ("The correctness of hypothesis " ^
62                              string_of_name n ^
63                              " relies on the body of " ^ hyp)
64                           ))
65                      in
66                       entry::context
67                   | Some (n,Cic.Def (te,ty)) ->
68                      (try
69                        ignore
70                         (CicTypeChecker.type_of_aux' metasenv context te
71                           CicUniv.oblivion_ugraph (* TASSI: FIXME *));
72                        ignore
73                         (CicTypeChecker.type_of_aux' metasenv context ty
74                           CicUniv.oblivion_ugraph (* TASSI: FIXME *));
75                       with
76                        _ ->
77                          raise
78                           (PET.Fail
79                             (lazy ("The correctness of hypothesis " ^
80                              string_of_name n ^
81                              " relies on the body of " ^ hyp)
82                           )));
83                      entry::context
84                ) canonical_context []
85              in
86               let _,_ =
87                try
88                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
89                  CicUniv.oblivion_ugraph (* TASSI: FIXME *)
90                with
91                 _ ->
92                  raise
93                   (PET.Fail
94                    (lazy ("The correctness of the goal relies on the body of " ^
95                     hyp)))
96               in
97                m,canonical_context',ty
98          | t -> t
99        ) metasenv
100      in
101       (curi,metasenv',_subst,pbo,pty, attrs), [goal]
102  in
103   PET.mk_tactic clearbody
104
105 let clear_one ~hyp =
106  let clear_one (proof, goal) =
107    let curi,metasenv,_subst,pbo,pty, attrs = proof in
108     let metano,context,ty =
109      CicUtil.lookup_meta goal metasenv
110     in
111      let string_of_name =
112       function
113          C.Name n -> n
114        | C.Anonymous -> "_"
115      in
116      let metasenv' =
117       List.map
118        (function
119            (m,canonical_context,ty) when m = metano ->
120              let context_changed, canonical_context' =
121               List.fold_right
122                (fun entry (b, context) ->
123                  match entry with
124                     Some (Cic.Name hyp',_) when hyp' = hyp -> 
125                       (true, None::context)
126                   | None -> (b, None::context)
127                   | Some (n,C.Decl t)
128                   | Some (n,Cic.Def (t,_)) ->
129                       if b then
130                          let _,_ =
131                           try
132                            CicTypeChecker.type_of_aux' metasenv context t
133                             CicUniv.oblivion_ugraph
134                           with _ ->
135                            raise
136                             (PET.Fail
137                               (lazy ("Hypothesis " ^ string_of_name n ^
138                                " uses hypothesis " ^ hyp)))
139                          in
140                           (b, entry::context)
141                       else
142                         (b, entry::context)
143                ) canonical_context (false, [])
144              in
145              if not context_changed then
146                raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
147              let _,_ =
148                try
149                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
150                  CicUniv.oblivion_ugraph 
151                with _ ->
152                 raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
153               in
154                m,canonical_context',ty
155          | t -> t
156        ) metasenv
157      in
158       (curi,metasenv',_subst,pbo,pty, attrs), [goal]
159  in
160   PET.mk_tactic clear_one
161
162 let clear ~hyps =
163    let clear status =
164       let aux status hyp = 
165          match PET.apply_tactic (clear_one ~hyp) status with
166             | proof, [g] -> proof, g
167             | _          -> raise (PET.Fail (lazy "clear: internal error"))
168       in
169       let proof, g = List.fold_left aux status hyps in
170       proof, [g]
171    in
172    PET.mk_tactic clear
173
174 (* Warning: this tactic has no effect on the proof term.
175    It just changes the name of an hypothesis in the current sequent *)
176 let rename ~froms ~tos =
177    let rename (proof, goal) =
178       let error = "rename: lists of different length" in
179       let assocs = 
180          try List.combine froms tos
181          with Invalid_argument _ -> raise (PET.Fail (lazy error))
182       in
183       let curi, metasenv, _subst, pbo, pty, attrs = proof in
184       let metano, _, _ = CicUtil.lookup_meta goal metasenv in      
185       let rename_map = function
186          | Some (Cic.Name hyp, decl_or_def) as entry ->
187             begin try Some (Cic.Name (List.assoc hyp assocs), decl_or_def)
188             with Not_found -> entry end
189          | entry -> entry
190       in
191       let map = function
192          | m, canonical_context, ty when m = metano ->
193             let canonical_context = List.map rename_map canonical_context in
194             m, canonical_context, ty
195          | conjecture -> conjecture
196       in
197       let metasenv = List.map map metasenv in
198       (curi, metasenv, _subst, pbo, pty, attrs), [goal]
199    in
200    PET.mk_tactic rename