]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/oCic2NCic.ml
snapshot inverse tranformation
[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml
1 let convert_term = Obj.magic;;
2
3 let cn_to_s = function
4   | Cic.Anonymous -> "_"
5   | Cic.Name s -> s
6 ;;
7
8 type ctx = Ce of NCic.hypothesis | Fix of int * int
9
10 let splat mk_pi ctx t =
11   List.fold_left
12     (fun t c -> 
13       match c with
14       | Ce (name, NCic.Def (bo,ty)) -> NCic.LetIn (name, ty, bo, t)
15       | Ce (name, NCic.Decl ty) when mk_pi -> NCic.Prod (name, ty, t)
16       | Ce (name, NCic.Decl ty) -> NCic.Lambda (name, ty, t)
17       | Fix _ -> t)
18     t ctx
19 ;;
20
21 let splat_args ctx t = 
22   let n_args =  
23     List.length (List.filter (function Ce _ -> true | _ -> false) ctx)
24   in  
25   if n_args = 0 then t 
26   else
27     let rec aux = function
28       | 0 -> []
29       | n -> aux (n-1) @ [NCic.Rel n]
30     in
31     NCic.Appl (t:: aux n_args)
32 ;;
33
34 let convert_term uri t = 
35   let rec aux octx (ctx : ctx list) n_fix uri = function
36     | Cic.CoFix (k, fl) ->
37         let idx = ref ~-1 in
38         let bctx = 
39           List.map (fun (_,_,_) -> 
40             incr idx; Fix (~-1,!idx)) fl @ ctx 
41         in
42         let buri = 
43           UriManager.uri_of_string 
44            (UriManager.string_of_uri uri^string_of_int (List.length ctx)^".con")
45         in
46         let n_fl = List.length fl in
47         let boctx,_ =
48          List.fold_left
49           (fun (types,len) (n,ty,_) ->
50              (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
51               len+1)) (octx,0) fl
52         in
53         let fl, fixpoints =
54           List.fold_right 
55             (fun (name,ty,bo) (l,fixpoints) -> 
56                let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
57                let bo, fixpoints_bo = aux boctx bctx (n_fix + n_fl) buri bo in
58                (([],name,~-1,splat true ctx ty, splat false ctx bo)::l),
59                fixpoints_ty @ fixpoints_bo @ fixpoints)
60             fl ([],[])
61         in
62         let obj = 
63           NUri.nuri_of_ouri uri,0,[],[],
64             NCic.Fixpoint (false, fl, (`Generated, `Definition)) 
65         in
66         NCic.Const (NReference.reference_of_ouri uri (NReference.CoFix (k))),
67         obj::fixpoints
68     | Cic.Fix (k, fl) ->
69         let idx = ref ~-1 in
70         let rno = ref 0 in
71         let bctx = 
72           List.map (fun (_,recno,_,_) -> 
73             incr idx; if !idx = k then rno := recno;Fix (recno,!idx)) fl @ ctx 
74         in
75         let buri = 
76           UriManager.uri_of_string 
77            (UriManager.string_of_uri uri^string_of_int (List.length ctx)^".con")
78         in
79         let n_fl = List.length fl in
80         let boctx,_ =
81          List.fold_left
82           (fun (types,len) (n,_,ty,_) ->
83              (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
84               len+1)) (octx,0) fl
85         in
86         let fl, fixpoints =
87           List.fold_right 
88             (fun (name,rno,ty,bo) (l,fixpoints) -> 
89                let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
90                let bo, fixpoints_bo = aux boctx bctx (n_fix + n_fl) buri bo in
91                let rno = rno + List.length ctx - n_fix in
92                (([],name,rno,splat true ctx ty, splat false ctx bo)::l),
93                fixpoints_ty @ fixpoints_bo @ fixpoints)
94             fl ([],[])
95         in
96         let obj = 
97           NUri.nuri_of_ouri uri,0,[],[],
98             NCic.Fixpoint (true, fl, (`Generated, `Definition)) 
99         in
100         NCic.Const (NReference.reference_of_ouri uri (NReference.Fix (k,!rno))),
101         obj::fixpoints
102     | Cic.Rel n ->
103         (match List.nth ctx n with
104         | Ce _ -> NCic.Rel (n-n_fix), []
105         | Fix (recno, fixno) ->
106            splat_args ctx 
107            (NCic.Const 
108             (NReference.reference_of_ouri uri (NReference.Fix (fixno,recno)))),
109            [])
110     | Cic.Lambda (name, (s as old_s), t) ->
111         let s, fixpoints_s = aux octx ctx n_fix uri s in
112         let ctx = Ce (cn_to_s name, NCic.Decl s) :: ctx in
113         let octx = Some (name, Cic.Decl old_s) :: octx in
114         let t, fixpoints_t = aux octx ctx n_fix uri t in
115         NCic.Lambda (cn_to_s name, s, t), fixpoints_s @ fixpoints_t
116     | Cic.Prod (name, (s as old_s), t) ->
117         let s, fixpoints_s = aux octx ctx n_fix uri s in
118         let ctx = Ce (cn_to_s name, NCic.Decl s) :: ctx in
119         let octx = Some (name, Cic.Decl old_s) :: octx in
120         let t, fixpoints_t = aux octx ctx n_fix uri t in
121         NCic.Prod (cn_to_s name, s, t), fixpoints_s @ fixpoints_t
122     | Cic.LetIn (name, (s as old_s), t) ->
123         let s, fixpoints_s = aux octx ctx n_fix uri s in
124         let old_ty,_ = 
125           CicTypeChecker.type_of_aux' [] octx old_s CicUniv.oblivion_ugraph 
126         in
127         let ty, fixpoints_ty = aux octx ctx n_fix uri old_ty in
128         let ctx = Ce (cn_to_s name, NCic.Def (s, ty)) :: ctx in
129         let octx = Some (name, Cic.Def (old_s, Some old_ty)) :: octx in
130         let t, fixpoints_t = aux octx ctx n_fix uri t in
131         NCic.LetIn (cn_to_s name, ty, s, t), 
132         fixpoints_s @ fixpoints_t @ fixpoints_ty
133     | Cic.Cast (t,ty) ->
134         let t, fixpoints_t = aux octx ctx n_fix uri t in
135         let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
136         NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
137     | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
138     | Cic.Sort Cic.Set -> NCic.Sort NCic.Set,[]
139     | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
140     | Cic.Sort (Cic.Type _) -> NCic.Sort (NCic.Type 0),[] 
141        (* calculate depth in the univ_graph*)
142     | Cic.Appl l -> 
143         let l, fixpoints =
144           List.fold_right 
145              (fun t (l,acc) -> 
146                let t, fixpoints = aux octx ctx n_fix uri t in 
147                (t::l,fixpoints@acc))
148              l ([],[])
149         in
150         NCic.Appl l, fixpoints
151     | Cic.Const (curi, _) -> 
152         NCic.Const (NReference.reference_of_ouri curi NReference.Def),[]
153     | Cic.MutInd (curi, tyno, _) -> 
154         NCic.Const (NReference.reference_of_ouri curi (NReference.Ind tyno)),[]
155     | Cic.MutConstruct (curi, tyno, consno, _) -> 
156         NCic.Const (NReference.reference_of_ouri curi 
157         (NReference.Con (tyno,consno))),[]
158     | Cic.MutCase (curi, tyno, oty, t, branches) ->
159         let r = NReference.reference_of_ouri curi (NReference.Ind tyno) in
160         let oty, fixpoints_oty = aux octx ctx n_fix uri oty in
161         let t, fixpoints_t = aux octx ctx n_fix uri t in
162         let branches, fixpoints =
163           List.fold_right 
164              (fun t (l,acc) -> 
165                let t, fixpoints = aux octx ctx n_fix uri t in 
166                (t::l,fixpoints@acc))
167              branches ([],[])
168         in
169         NCic.Match (r,oty,t,branches), fixpoints_oty @ fixpoints_t @ fixpoints
170     | Cic.Implicit _ | Cic.Meta _ | Cic.Var _ -> assert false
171   in
172    aux [] [] 0 uri t
173 ;;
174
175 let convert_obj_aux uri = function
176  | Cic.Constant (name, None, ty, _, _) ->
177      let nty, fixpoints = convert_term uri ty in
178      assert(fixpoints = []);
179      NCic.Constant ([], name, None, nty, (`Provided,`Theorem,`Regular)),
180      fixpoints
181  | Cic.Constant (name, Some bo, ty, _, _) ->
182      let nbo, fixpoints_bo = convert_term uri bo in
183      let nty, fixpoints_ty = convert_term uri ty in
184      assert(fixpoints_ty = []);
185      NCic.Constant ([], name, Some nbo, nty, (`Provided,`Theorem,`Regular)),
186      fixpoints_bo @ fixpoints_ty
187  | Cic.InductiveDefinition (_,_,_,_) -> assert false (*
188      let ind = let _,x,_,_ = List.hd itl in x in
189      let itl = 
190        List.map 
191          (fun name, _, ty, cl ->
192             [], name, convert_term ty, 
193               List.map (fun name, ty -> [], name, convert_term ty) cl) 
194          itl        
195      in
196      NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)) *)
197  | Cic.Variable _ 
198  | Cic.CurrentProof _ -> assert false
199 ;;
200
201 let convert_obj uri obj = 
202   let o, fixpoints = convert_obj_aux uri obj in
203   let obj = NUri.nuri_of_ouri uri,0, [], [], o in
204   obj, fixpoints
205 ;;