]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/proofEngineStructuralRules.ml
New argument (the identifier) to generalize.
[helm.git] / helm / ocaml / 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 open ProofEngineTypes
27
28 let clearbody ~hyp = 
29  let clearbody ~hyp (proof, goal) =
30   let module C = Cic in
31    match hyp with
32       None -> assert false
33     | Some (_, C.Def (_, Some _)) -> assert false
34     | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
35     | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
36        let curi,metasenv,pbo,pty = proof in
37         let metano,_,_ = CicUtil.lookup_meta goal metasenv in
38          let string_of_name =
39           function
40              C.Name n -> n
41            | C.Anonymous -> "_"
42          in
43          let metasenv' =
44           List.map
45            (function
46                (m,canonical_context,ty) when m = metano ->
47                  let canonical_context' =
48                   List.fold_right
49                    (fun entry context ->
50                      match entry with
51                         t when t == hyp_to_clear_body ->
52                          let cleared_entry =
53                           let ty,_ =
54                            CicTypeChecker.type_of_aux' metasenv context term
55                              CicUniv.empty_ugraph (* TASSI: FIXME *)
56                           in
57                            Some (n_to_clear_body, Cic.Decl ty)
58                          in
59                           cleared_entry::context
60                       | None -> None::context
61                       | Some (n,C.Decl t)
62                       | Some (n,C.Def (t,None)) ->
63                          let _,_ =
64                           try
65                            CicTypeChecker.type_of_aux' metasenv context t
66                              CicUniv.empty_ugraph (* TASSI: FIXME *)
67                           with
68                            _ ->
69                              raise
70                               (Fail
71                                 ("The correctness of hypothesis " ^
72                                  string_of_name n ^
73                                  " relies on the body of " ^
74                                  string_of_name n_to_clear_body)
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                        ("The correctness of the goal relies on the body of " ^
90                         string_of_name n_to_clear_body))
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:hyp_to_clear (proof, goal) =
102   let module C = Cic in
103    match hyp_to_clear with
104       None -> assert false
105     | Some (n_to_clear, _) ->
106        let curi,metasenv,pbo,pty = proof in
107         let metano,context,ty =
108          CicUtil.lookup_meta goal metasenv
109         in
110          let string_of_name =
111           function
112              C.Name n -> n
113            | C.Anonymous -> "_"
114          in
115          let metasenv' =
116           List.map
117            (function
118                (m,canonical_context,ty) when m = metano ->
119                  let canonical_context' =
120                   List.fold_right
121                    (fun entry context ->
122                      match entry with
123                         t when t == hyp_to_clear -> None::context
124                       | None -> None::context
125                       | Some (_,Cic.Def (_,Some _)) -> assert false
126                       | Some (n,C.Decl t)
127                       | Some (n,C.Def (t,None)) ->
128                          let _,_ =
129                           try
130                            CicTypeChecker.type_of_aux' metasenv context t
131                              CicUniv.empty_ugraph (* TASSI: FIXME *)
132                           with
133                            _ ->
134                              raise
135                               (Fail
136                                 ("Hypothesis " ^
137                                  string_of_name n ^
138                                  " uses hypothesis " ^
139                                  string_of_name n_to_clear)
140                               )
141                          in
142                           entry::context
143                    ) canonical_context []
144                  in
145                   let _,_ =
146                    try
147                     CicTypeChecker.type_of_aux' metasenv canonical_context' ty
148                       CicUniv.empty_ugraph (* TASSI: FIXME *)
149                    with
150                     _ ->
151                      raise
152                       (Fail
153                        ("Hypothesis " ^ string_of_name n_to_clear ^
154                         " occurs in the goal"))
155                   in
156                    m,canonical_context',ty
157              | t -> t
158            ) metasenv
159          in
160           (curi,metasenv',pbo,pty), [goal]
161  in
162   mk_tactic (clear ~hyp)