X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic2OCic.ml;h=5f8279d7e67cb3660652e392b882a49cc4fa63a7;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=13c703dae125d7db24b6a41078b745972b0f1c5e;hpb=8a49ad7c7475e5486ea9ecacc82a07b15fcded6e;p=helm.git diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index 13c703dae..5f8279d7e 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -1,51 +1,117 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) -let rec convert_term k = function (* pass k along *) +(* $Id$ *) + +let ouri_of_nuri u = UriManager.uri_of_string (NUri.string_of_uri u);; + +let ouri_of_reference (NReference.Ref (u,_)) = ouri_of_nuri u;; + +let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];; + +let nn_2_on = function + | "_" -> Cic.Anonymous + | s -> Cic.Name s +;; + +let convert_term uri n_fl t = + let rec convert_term k = function (* pass k along *) | NCic.Rel i -> Cic.Rel i | NCic.Meta _ -> assert false | NCic.Appl l -> Cic.Appl (List.map (convert_term k) l) - | NCic.Prod (n,s,t) -> Cic.Prod (Cic.Name n,convert_term k s, convert_term k t) - | NCic.Lambda (n,s,t) -> Cic.Lambda(Cic.Name n,convert_term k s, convert_term k t) - | NCic.LetIn (n,_,s,t) -> Cic.LetIn (Cic.Name n,convert_term k s, convert_term k t) + | NCic.Prod (n,s,t) -> + Cic.Prod (nn_2_on n,convert_term k s, convert_term (k+1) t) + | NCic.Lambda (n,s,t) -> + Cic.Lambda(nn_2_on n,convert_term k s, convert_term (k+1) t) + | NCic.LetIn (n,ty_s,s,t) -> + Cic.LetIn (nn_2_on n,convert_term k s,convert_term k ty_s, convert_term (k+1) t) | NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop - | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp - | NCic.Sort NCic.Set -> Cic.Sort Cic.Set + | NCic.Sort (NCic.Type u) when + (* BUG HERE: I should use NCicEnvironment.universe_eq, but I do not + want to add this recursion between the modules *) + (*NCicEnvironment.universe_eq*) u=cprop -> Cic.Sort (Cic.CProp (CicUniv.fresh ())) | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ())) | NCic.Implicit _ -> assert false - | NCic.Const (NReference.Ref (_,u,NReference.Ind i)) -> - Cic.MutInd (NUri.ouri_of_nuri u,i,[]) - | NCic.Const (NReference.Ref (_,u,NReference.Con (i,j))) -> - Cic.MutConstruct (NUri.ouri_of_nuri u,i,j,[]) - | NCic.Const (NReference.Ref (_,u,NReference.Def)) - | NCic.Const (NReference.Ref (_,u,NReference.Decl)) -> - Cic.Const (NUri.ouri_of_nuri u,[]) - | NCic.Match (NReference.Ref (_,u,NReference.Ind i),oty,t,pl) -> - Cic.MutCase (NUri.ouri_of_nuri u,i, convert_term k oty, convert_term k t, + | NCic.Const (NReference.Ref (u,NReference.Ind (_,i,_))) -> + Cic.MutInd (ouri_of_nuri u,i,[]) + | NCic.Const (NReference.Ref (u,NReference.Con (i,j,_))) -> + Cic.MutConstruct (ouri_of_nuri u,i,j,[]) + | NCic.Const (NReference.Ref (u,NReference.Def _)) + | NCic.Const (NReference.Ref (u,NReference.Decl)) -> + Cic.Const (ouri_of_nuri u,[]) + | NCic.Match (NReference.Ref (u,NReference.Ind (_,i,_)),oty,t,pl) -> + Cic.MutCase (ouri_of_nuri u,i, convert_term k oty, convert_term k t, List.map (convert_term k) pl) - | NCic.Const (NReference.Ref (_,u,NReference.Fix (i,_))) -> assert false - (* map to rel if is the self-fix, otherwise explode *) - | NCic.Const (NReference.Ref (_,u,NReference.CoFix i)) -> assert false - (* map to rel if is the self-fix, otherwise explode *) + | NCic.Const (NReference.Ref (u,NReference.Fix (i,_,_))) + | NCic.Const (NReference.Ref (u,NReference.CoFix i)) -> + if NUri.eq u uri then + Cic.Rel (n_fl - i + k) + else + let ouri = ouri_of_nuri u in + let ouri = + UriManager.uri_of_string + (UriManager.buri_of_uri ouri ^ "/" ^ + UriManager.name_of_uri ouri ^ string_of_int i ^ ".con") in + Cic.Const (ouri,[]) | _ -> assert false + in + convert_term 0 t ;; -let convert_fix k fl = +let convert_fix is_fix uri k fl = let n_fl = List.length fl in - let fl = - List.map - (fun (_, name,recno,ty,bo) -> - name, recno, convert_term 0 ty, convert_term 0 bo) - fl - in - Cic.Fix (k, fl) + if is_fix then + let fl = + List.map + (fun (_, name,recno,ty,bo) -> + name, recno, convert_term uri n_fl ty, convert_term uri n_fl bo) + fl + in + Cic.Fix (k, fl) + else + let fl = + List.map + (fun (_, name,_,ty,bo) -> + name, convert_term uri n_fl ty, convert_term uri n_fl bo) + fl + in + Cic.CoFix (k, fl) ;; let convert_nobj = function - | _,_,_,_,NCic.Constant (rel, name, Some bo, ty, _) -> - Cic.Constant (name, Some (convert_term 0 bo), convert_term 0 ty, [],[]) - | _,_,_,_,NCic.Constant (rel, name, None, ty, _) -> - Cic.Constant (name, None, convert_term 0 ty, [],[]) - | _,_,_,_,NCic.Fixpoint (is_fix, fl, _) -> - Cic.Constant ("pippo", Some (convert_fix 0 fl), - convert_term 0 (let _,_,_,ty,_ = List.hd fl in ty), [], []) - | _,_,_,_,NCic.Inductive _ -> assert false + | u,_,_,_,NCic.Constant (_, name, Some bo, ty, _) -> + [ouri_of_nuri u,Cic.Constant + (name, Some (convert_term u 0 bo), convert_term u 0 ty, [],[])] + | u,_,_,_,NCic.Constant (_, name, None, ty, _) -> + [ouri_of_nuri u,Cic.Constant (name, None, convert_term u 0 ty, [],[])] + | u,_,_,_,NCic.Fixpoint (is_fix, fl, _) -> + List.map + (fun nth -> + let name = + UriManager.name_of_uri (ouri_of_nuri u) ^ string_of_int nth in + let buri = UriManager.buri_of_uri (ouri_of_nuri u) in + let uri = UriManager.uri_of_string (buri ^"/"^name^".con") in + uri, + Cic.Constant (name, + Some (convert_fix is_fix u nth fl), + convert_term u 0 (let _,_,_,ty,_ = List.hd fl in ty), [], [])) + (let rec seq = function 0 -> [0]|n -> n::seq (n-1) in + seq (List.length fl-1)) + | u,_,_,_,NCic.Inductive (inductive,leftno,itl,_) -> + let itl = + List.map + (function (_,name,ty,cl) -> + let cl=List.map (function (_,name,ty) -> name,convert_term u 0 ty) cl in + name,inductive,convert_term u 0 ty,cl + ) itl + in + [ouri_of_nuri u, Cic.InductiveDefinition (itl,[],leftno,[])] ;;