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