]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/acic_content/content2cic.ml
more comments
[helm.git] / helm / software / components / acic_content / content2cic.ml
1 (* Copyright (C) 2000, 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 (***************************************************************************)
27 (*                                                                         *)
28 (*                            PROJECT HELM                                 *)
29 (*                                                                         *)
30 (*                Andrea Asperti <asperti@cs.unibo.it>                     *)
31 (*                              17/06/2003                                 *)
32 (*                                                                         *)
33 (***************************************************************************)
34
35 (* $Id$ *)
36
37 exception TO_DO;;
38
39 let proof2cic deannotate p =
40   let rec proof2cic premise_env p =
41     let module C = Cic in 
42     let module Con = Content in
43       let rec extend_premise_env current_env = 
44         function
45             [] -> current_env
46           | p::atl ->
47               extend_premise_env 
48               ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in
49       let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in
50       let body = conclude2cic new_premise_env p.Con.proof_conclude in
51       context2cic premise_env p.Con.proof_context body
52
53   and context2cic premise_env context body =
54     List.fold_right (ce2cic premise_env) context body
55
56   and ce2cic premise_env ce target =
57     let module C = Cic in
58     let module Con = Content in
59       match ce with
60         `Declaration d -> 
61           (match d.Con.dec_name with
62               Some s ->
63                 C.Lambda (C.Name s, deannotate d.Con.dec_type, target)
64             | None -> 
65                 C.Lambda (C.Anonymous, deannotate d.Con.dec_type, target))
66       | `Hypothesis h ->
67           (match h.Con.dec_name with
68               Some s ->
69                 C.Lambda (C.Name s, deannotate h.Con.dec_type, target)
70             | None -> 
71                 C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target))
72       | `Proof p -> 
73           let ty =
74            match p.Con.proof_conclude.Con.conclude_conclusion with
75               None -> (*Cic.Implicit None*) assert false
76             | Some ty -> deannotate ty
77           in
78           (match p.Con.proof_name with
79               Some s ->
80                 C.LetIn (C.Name s, proof2cic premise_env p, ty , target)
81             | None -> 
82                 C.LetIn (C.Anonymous, proof2cic premise_env p, ty, target)) 
83       | `Definition d -> 
84            (match d.Con.def_name with
85               Some s ->
86                 C.LetIn (C.Name s, proof2cic premise_env p, deannotate d.Con.def_type, target)
87             | None -> 
88                 C.LetIn (C.Anonymous, proof2cic premise_env p, deannotate d.Con.def_type, target)) 
89       | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} -> 
90             (match target with
91                C.Rel n ->
92                  (match kind with 
93                     `Recursive l ->
94                       let funs = 
95                         List.map2 
96                           (fun n bo ->
97                              match bo with
98                                `Proof bo ->
99                                   (match 
100                                     bo.Con.proof_conclude.Con.conclude_conclusion,
101                                     bo.Con.proof_name
102                                    with
103                                       Some ty, Some name -> 
104                                        (name,n,deannotate ty,
105                                          proof2cic premise_env bo)
106                                     | _,_ -> assert false)
107                              | _ -> assert false)
108                           l defs in 
109                       C.Fix (n, funs)
110                   | `CoRecursive ->
111                      let funs = 
112                         List.map 
113                           (function bo ->
114                              match bo with
115                               `Proof bo ->
116                                  (match 
117                                     bo.Con.proof_conclude.Con.conclude_conclusion,
118                                     bo.Con.proof_name 
119                                   with
120                                      Some ty, Some name ->
121                                       (name,deannotate ty,
122                                         proof2cic premise_env bo)
123                                    | _,_ -> assert false)
124                              | _ -> assert false)
125                            defs in 
126                       C.CoFix (n, funs)
127                   | _ -> (* no inductive types in local contexts *)
128                        assert false)
129              | _ -> assert false)
130
131   and conclude2cic premise_env conclude =
132     let module C = Cic in 
133     let module Con = Content in
134     if conclude.Con.conclude_method = "TD_Conversion" then
135       (match conclude.Con.conclude_args with
136          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
137        | _ -> prerr_endline "1"; assert false)
138     else if conclude.Con.conclude_method = "BU_Conversion" then
139       (match conclude.Con.conclude_args with
140          [Con.Premise prem] -> 
141            (try List.assoc prem.Con.premise_xref premise_env
142             with Not_found -> 
143               prerr_endline
144                ("Not_found in BU_Conversion: " ^ prem.Con.premise_xref);
145               raise Not_found)
146        | _ -> prerr_endline "2"; assert false)
147     else if conclude.Con.conclude_method = "Exact" then
148       (match conclude.Con.conclude_args with
149          [Con.Term (_,t)] -> deannotate t
150        | [Con.Premise prem] -> 
151            (match prem.Con.premise_n with
152               None -> assert false
153             | Some n -> C.Rel n)
154        | _ -> prerr_endline "3"; assert false)
155     else if conclude.Con.conclude_method = "Intros+LetTac" then
156       (match conclude.Con.conclude_args with
157          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
158        | _ -> prerr_endline "4"; assert false)
159     else if (conclude.Con.conclude_method = "ByInduction" ||
160              conclude.Con.conclude_method = "AndInd" ||
161              conclude.Con.conclude_method = "Exists" ||
162              conclude.Con.conclude_method = "FalseInd") then
163       (match (List.tl conclude.Con.conclude_args) with
164          Con.Term (_,C.AAppl (
165             id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
166            let subst =
167              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in 
168            let cargs = args2cic premise_env args in
169            let cparams_and_IP = List.map deannotate params_and_IP in
170            C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
171        | _ -> prerr_endline "5"; assert false)
172     else if (conclude.Con.conclude_method = "Rewrite") then
173       (match conclude.Con.conclude_args with
174          Con.Term (_,C.AConst (sid,uri,exp_named_subst))::args ->
175            let subst =
176              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
177            let  cargs = args2cic premise_env args in
178            C.Appl (C.Const(uri,subst)::cargs)
179        | _ -> prerr_endline "6"; assert false)
180     else if (conclude.Con.conclude_method = "Case") then
181       (match conclude.Con.conclude_args with
182         Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Premise(prem)::patterns ->
183            C.MutCase
184             (UriManager.uri_of_string uri,
185              int_of_string notype, deannotate ty, 
186              List.assoc prem.Con.premise_xref premise_env,
187              List.map 
188                (function 
189                    Con.ArgProof p -> proof2cic [] p
190                  | _ -> prerr_endline "7a"; assert false) patterns)
191       | Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Term(_,te)::patterns ->           C.MutCase
192             (UriManager.uri_of_string uri,
193              int_of_string notype, deannotate ty, deannotate te,
194              List.map 
195                (function 
196                    (Con.ArgProof p) -> proof2cic [] p
197                  | _ -> prerr_endline "7a"; assert false) patterns) 
198       | _ -> (prerr_endline "7"; assert false))
199     else if (conclude.Con.conclude_method = "Apply") then
200       let cargs = (args2cic premise_env conclude.Con.conclude_args) in
201       C.Appl cargs 
202     else (prerr_endline "8"; assert false)
203
204   and args2cic premise_env l =
205     List.map (arg2cic premise_env) l
206
207   and arg2cic premise_env =
208     let module C = Cic in
209     let module Con = Content in
210     function
211         Con.Aux n -> prerr_endline "8"; assert false
212       | Con.Premise prem ->
213           (match prem.Con.premise_n with
214               Some n -> C.Rel n
215             | None ->
216               (try List.assoc prem.Con.premise_xref premise_env
217                with Not_found -> 
218                   prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
219                   raise Not_found))
220       | Con.Lemma lemma ->
221          CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
222       | Con.Term (_,t) -> deannotate t
223       | Con.ArgProof p -> proof2cic [] p (* empty! *)
224       | Con.ArgMethod s -> raise TO_DO
225
226 in proof2cic [] p
227 ;;
228
229 exception ToDo;;
230
231 let cobj2obj deannotate (id,params,metasenv,obj) =
232  let module K = Content in
233  match obj with
234     `Def (Content.Const,ty,`Proof bo) ->
235       (match metasenv with
236           None ->
237            Cic.Constant
238             (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
239         | Some metasenv' ->
240            let metasenv'' =
241             List.map
242              (function (_,i,canonical_context,term) ->
243                let canonical_context' =
244                 List.map
245                  (function
246                      None -> None
247                    | Some (`Declaration d) 
248                    | Some (`Hypothesis d) ->
249                      (match d with
250                         {K.dec_name = Some n ; K.dec_type = t} ->
251                           Some (Cic.Name n, Cic.Decl (deannotate t))
252                       | _ -> assert false)
253                    | Some (`Definition d) ->
254                       (match d with
255                           {K.def_name = Some n ; K.def_term = t ; K.def_type = ty} ->
256                             Some (Cic.Name n, Cic.Def (deannotate t,deannotate ty))
257                         | _ -> assert false)
258                    | Some (`Proof d) ->
259                       (match d with
260                           {K.proof_name = Some n } ->
261                             Some (Cic.Name n,
262                               Cic.Def ((proof2cic deannotate d),assert false))
263                         | _ -> assert false)
264                  ) canonical_context
265                in
266                 (i,canonical_context',deannotate term)
267              ) metasenv'
268            in
269             Cic.CurrentProof
270              (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
271               []))
272   | _ -> raise ToDo
273 ;;
274
275 let cobj2obj = cobj2obj Deannotate.deannotate_term;;