X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic2OCic.ml;h=57465b0748440403093d87efb67a562f20752ffe;hb=f2f9699ce6c656e62ae18148bce61f8bb945dc7a;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..57465b074 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -1,51 +1,104 @@ +(* + ||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 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 _) -> 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.Ind (_,i))) -> + Cic.MutInd (ouri_of_nuri u,i,[]) | NCic.Const (NReference.Ref (_,u,NReference.Con (i,j))) -> - Cic.MutConstruct (NUri.ouri_of_nuri u,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 (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, + 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), [], []) + | 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)) | _,_,_,_,NCic.Inductive _ -> assert false ;;