]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/proofEngineStructuralRules.ml
Huge commit for the release. Includes:
[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 open ProofEngineTypes
29
30 let clearbody ~hyp = 
31  let clearbody ~hyp (proof, goal) =
32   let module C = Cic in
33    let curi,metasenv,pbo,pty = 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 =
50                       let ty =
51                        match ty with
52                           Some ty -> ty
53                         | None ->
54                            fst
55                             (CicTypeChecker.type_of_aux' metasenv context term
56                               CicUniv.empty_ugraph) (* TASSI: FIXME *)
57                       in
58                        Some (C.Name hyp, Cic.Decl ty)
59                      in
60                       cleared_entry::context
61                   | None -> None::context
62                   | Some (n,C.Decl t)
63                   | Some (n,C.Def (t,None)) ->
64                      let _,_ =
65                       try
66                        CicTypeChecker.type_of_aux' metasenv context t
67                         CicUniv.empty_ugraph (* TASSI: FIXME *)
68                       with
69                        _ ->
70                          raise
71                           (Fail
72                             (lazy ("The correctness of hypothesis " ^
73                              string_of_name n ^
74                              " relies on the body of " ^ hyp)
75                           ))
76                      in
77                       entry::context
78                   | Some (_,Cic.Def (_,Some _)) -> assert false
79                ) canonical_context []
80              in
81               let _,_ =
82                try
83                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
84                  CicUniv.empty_ugraph (* TASSI: FIXME *)
85                with
86                 _ ->
87                  raise
88                   (Fail
89                    (lazy ("The correctness of the goal relies on the body of " ^
90                     hyp)))
91               in
92                m,canonical_context',ty
93          | t -> t
94        ) metasenv
95      in
96       (curi,metasenv',pbo,pty), [goal]
97  in
98   mk_tactic (clearbody ~hyp)
99
100 let clear ~hyp =
101  let clear ~hyp (proof, goal) =
102   let module C = Cic in
103    let curi,metasenv,pbo,pty = proof in
104     let metano,context,ty =
105      CicUtil.lookup_meta goal metasenv
106     in
107      let string_of_name =
108       function
109          C.Name n -> n
110        | C.Anonymous -> "_"
111      in
112      let metasenv' =
113       List.map
114        (function
115            (m,canonical_context,ty) when m = metano ->
116              let context_changed, canonical_context' =
117               List.fold_right
118                (fun entry (b, context) ->
119                  match entry with
120                     Some (Cic.Name hyp',_) when hyp' = hyp -> 
121                       (true, None::context)
122                   | None -> (b, None::context)
123                   | Some (n,C.Decl t)
124                   | Some (n,Cic.Def (t,Some _))
125                   | Some (n,C.Def (t,None)) ->
126                       if b then
127                          let _,_ =
128                           try
129                            CicTypeChecker.type_of_aux' metasenv context t
130                             CicUniv.empty_ugraph
131                           with _ ->
132                            raise
133                             (Fail
134                               (lazy ("Hypothesis " ^ string_of_name n ^
135                                " uses hypothesis " ^ hyp)))
136                          in
137                           (b, entry::context)
138                       else
139                         (b, entry::context)
140                ) canonical_context (false, [])
141              in
142              if not context_changed then
143                raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
144              let _,_ =
145                try
146                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
147                  CicUniv.empty_ugraph 
148                with _ ->
149                 raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
150               in
151                m,canonical_context',ty
152          | t -> t
153        ) metasenv
154      in
155       (curi,metasenv',pbo,pty), [goal]
156  in
157   mk_tactic (clear ~hyp)
158
159 (* Warning: this tactic has no effect on the proof term.
160    It just changes the name of an hypothesis in the current sequent *)
161 let rename ~from ~to_ =
162  let rename ~from ~to_ (proof, goal) =
163   let module C = Cic in
164    let curi,metasenv,pbo,pty = proof in
165     let metano,context,ty =
166      CicUtil.lookup_meta goal metasenv
167     in
168      let metasenv' =
169       List.map
170        (function
171            (m,canonical_context,ty) when m = metano ->
172              let canonical_context' =
173               List.map
174                (function
175                    Some (Cic.Name hyp,decl_or_def) when hyp = from ->
176                     Some (Cic.Name to_,decl_or_def)
177                  | item -> item
178                ) canonical_context
179              in
180               m,canonical_context',ty
181          | t -> t
182        ) metasenv
183      in
184       (curi,metasenv',pbo,pty), [goal]
185  in
186   mk_tactic (rename ~from ~to_)
187
188 let set_goal n =
189   ProofEngineTypes.mk_tactic
190     (fun (proof, goal) ->
191        let (_, metasenv, _, _) = proof in
192        if CicUtil.exists_meta n metasenv then
193          (proof, [n])
194        else
195          raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n))))