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