]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_transformations/acic2Ast.ml
Files control.js graphLinks.js utils.js no longer in use.
[helm.git] / helm / ocaml / cic_transformations / acic2Ast.ml
1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
24  *)
25
26 open Printf
27
28 let symbol_table = Hashtbl.create 1024
29
30 let sort_of_string = function
31   | "Prop" -> `Prop
32   | "Set" -> `Set
33   | "Type" -> `Type
34   | "CProp" -> `CProp
35   | _ -> assert false
36
37 let get_types uri =
38   match CicEnvironment.get_obj uri with
39   | Cic.Constant _ -> assert false
40   | Cic.Variable _ -> assert false
41   | Cic.CurrentProof _ -> assert false
42   | Cic.InductiveDefinition (l,_,_) -> l 
43
44 let name_of_inductive_type uri i = 
45   let types = get_types uri in
46   let (name, _, _, _) = try List.nth types i with Not_found -> assert false in
47   name
48
49   (* returns <name, type> pairs *)
50 let constructors_of_inductive_type uri i =
51   let types = get_types uri in
52   let (_, _, _, constructors) = 
53     try List.nth types i with Not_found -> assert false
54   in
55   constructors
56
57   (* returns name only *)
58 let constructor_of_inductive_type uri i j =
59   (try
60     fst (List.nth (constructors_of_inductive_type uri i) (j-1))
61   with Not_found -> assert false)
62
63 let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
64   let register_uri id uri = Hashtbl.add ids_to_uris id uri in
65   let sort_of_id id =
66     try
67       sort_of_string (Hashtbl.find ids_to_inner_sorts id)
68     with Not_found -> assert false
69   in
70   let module Ast = CicAst in
71   let idref id t = Ast.AttributedTerm (`IdRef id, t) in
72   let rec aux = function
73     | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
74     | Cic.AVar (id,uri,subst) ->
75         register_uri id (UriManager.string_of_uri uri);
76         idref id
77           (Ast.Ident (UriManager.name_of_uri uri, astsubst_of_cicsubst subst))
78     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l))
79     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
80     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
81     | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) (* TASSI *)
82     | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
83     | Cic.AImplicit _ -> assert false
84     | Cic.AProd (id,n,s,t) ->
85         let binder_kind =
86           match sort_of_id id with
87           | `Set | `Type -> `Pi
88           | `Prop | `CProp -> `Forall
89         in
90         idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))
91     | Cic.ACast (id,v,t) -> idref id (aux v)
92     | Cic.ALambda (id,n,s,t) ->
93         idref id (Ast.Binder (`Lambda, (n, Some (aux s)), aux t))
94     | Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((n, None), aux s, aux t))
95     | Cic.AAppl (aid,Cic.AConst (sid,uri,subst)::tl) ->
96         let uri_str = UriManager.string_of_uri uri in
97         register_uri sid uri_str;
98         (try 
99           let f = Hashtbl.find symbol_table uri_str in
100           f aid sid tl aux
101         with Not_found ->
102           idref aid
103             (Ast.Appl (idref sid
104               (Ast.Ident (UriManager.name_of_uri uri,
105                 astsubst_of_cicsubst subst)) :: (List.map aux tl))))
106     | Cic.AAppl (aid,Cic.AMutInd (sid,uri,i,subst)::tl) ->
107         let name = name_of_inductive_type uri i in
108         let uri_str = UriManager.string_of_uri uri in
109         let puri_str =
110          uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
111         register_uri sid puri_str;
112         (try 
113           (let f = Hashtbl.find symbol_table puri_str in
114            f aid sid tl aux)
115          with Not_found ->
116            idref aid
117             (Ast.Appl (idref sid
118               (Ast.Ident (name,
119                 astsubst_of_cicsubst subst)) :: (List.map aux tl))))
120     | Cic.AAppl (id,li) -> idref id (Ast.Appl (List.map aux li))
121     | Cic.AConst (id,uri,subst) ->
122         let uri_str = UriManager.string_of_uri uri in
123         register_uri id uri_str;
124         (try
125           let f = Hashtbl.find symbol_table uri_str in
126           f "dummy" id [] aux
127         with Not_found ->
128           idref id
129             (Ast.Ident
130               (UriManager.name_of_uri uri, astsubst_of_cicsubst subst)))
131     | Cic.AMutInd (id,uri,i,subst) ->
132         let name = name_of_inductive_type uri i in
133         let uri_str = UriManager.string_of_uri uri in
134         let puri_str =
135          uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
136         register_uri id puri_str;
137         (try
138           let f = Hashtbl.find symbol_table puri_str in
139           f "dummy" id [] aux
140         with Not_found ->
141           idref id (Ast.Ident (name, astsubst_of_cicsubst subst)))
142     | Cic.AMutConstruct (id,uri,i,j,subst) ->
143         let name = constructor_of_inductive_type uri i j in
144         let uri_str = UriManager.string_of_uri uri in
145         let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in
146         register_uri id puri_str;
147         (try
148           let f = Hashtbl.find symbol_table puri_str in
149           f "dummy" id [] aux
150         with Not_found ->
151           idref id (Ast.Ident (name, astsubst_of_cicsubst subst)))
152     | Cic.AMutCase (id,uri,typeno,ty,te,patterns) ->
153         let name = name_of_inductive_type uri typeno in
154         let constructors = constructors_of_inductive_type uri typeno in
155         let rec eat_branch ty pat =
156           match (ty, pat) with
157           | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') ->
158               let (cv, rhs) = eat_branch t t' in
159               (name, Some (aux s)) :: cv, rhs
160           | _, _ -> [], aux pat
161         in
162         let patterns =
163           List.map2
164             (fun (name, ty) pat ->
165               let (capture_variables, rhs) = eat_branch ty pat in
166               ((name, capture_variables), rhs))
167             constructors patterns
168         in
169         idref id (Ast.Case (aux te, Some name, Some (aux ty), patterns))
170     | Cic.AFix (id, no, funs) -> 
171         let defs = 
172           List.map
173             (fun (_, n, decr_idx, ty, bo) ->
174               ((Cic.Name n, Some (aux ty)), aux bo, decr_idx))
175             funs
176         in
177         let name =
178           try
179             (match List.nth defs no with
180             | (Cic.Name n, _), _, _ -> n
181             | _ -> assert false)
182           with Not_found -> assert false
183         in
184         idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
185     | Cic.ACoFix (id, no, funs) -> 
186         let defs = 
187           List.map
188             (fun (_, n, ty, bo) -> ((Cic.Name n, Some (aux ty)), aux bo, 0))
189             funs
190         in
191         let name =
192           try
193             (match List.nth defs no with
194             | (Cic.Name n, _), _, _ -> n
195             | _ -> assert false)
196           with Not_found -> assert false
197         in
198         idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None)))
199
200   and astsubst_of_cicsubst subst =
201     Some
202       (List.map (fun (uri, annterm) ->
203         (UriManager.name_of_uri uri, aux annterm))
204         subst)
205
206   and astcontext_of_ciccontext context =
207     List.map
208       (function
209         | None -> None
210         | Some annterm -> Some (aux annterm))
211       context
212
213   in
214   aux acic, ids_to_uris
215