2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 let nn_2_on = function
15 | "_" -> Cic.Anonymous
19 let convert_term uri n_fl t =
20 let rec convert_term k = function (* pass k along *)
21 | NCic.Rel i -> Cic.Rel i
22 | NCic.Meta _ -> assert false
23 | NCic.Appl l -> Cic.Appl (List.map (convert_term k) l)
24 | NCic.Prod (n,s,t) ->
25 Cic.Prod (nn_2_on n,convert_term k s, convert_term (k+1) t)
26 | NCic.Lambda (n,s,t) ->
27 Cic.Lambda(nn_2_on n,convert_term k s, convert_term (k+1) t)
28 | NCic.LetIn (n,ty_s,s,t) ->
29 Cic.LetIn (nn_2_on n,convert_term k s,convert_term k ty_s, convert_term (k+1) t)
30 | NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop
31 | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp
32 | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
33 | NCic.Implicit _ -> assert false
34 | NCic.Const (NReference.Ref (_,u,NReference.Ind (_,i))) ->
35 Cic.MutInd (NUri.ouri_of_nuri u,i,[])
36 | NCic.Const (NReference.Ref (_,u,NReference.Con (i,j))) ->
37 Cic.MutConstruct (NUri.ouri_of_nuri u,i,j,[])
38 | NCic.Const (NReference.Ref (_,u,NReference.Def))
39 | NCic.Const (NReference.Ref (_,u,NReference.Decl)) ->
40 Cic.Const (NUri.ouri_of_nuri u,[])
41 | NCic.Match (NReference.Ref (_,u,NReference.Ind (_,i)),oty,t,pl) ->
42 Cic.MutCase (NUri.ouri_of_nuri u,i, convert_term k oty, convert_term k t,
43 List.map (convert_term k) pl)
44 | NCic.Const (NReference.Ref (_,u,NReference.Fix (i,_)))
45 | NCic.Const (NReference.Ref (_,u,NReference.CoFix i)) ->
47 Cic.Rel (n_fl - i + k)
49 let ouri = NUri.ouri_of_nuri u in
51 UriManager.uri_of_string
52 (UriManager.buri_of_uri ouri ^ "/" ^
53 UriManager.name_of_uri ouri ^ string_of_int i ^ ".con") in
60 let convert_fix is_fix uri k fl =
61 let n_fl = List.length fl in
65 (fun (_, name,recno,ty,bo) ->
66 name, recno, convert_term uri n_fl ty, convert_term uri n_fl bo)
73 (fun (_, name,_,ty,bo) ->
74 name, convert_term uri n_fl ty, convert_term uri n_fl bo)
80 let convert_nobj = function
81 | u,_,_,_,NCic.Constant (_, name, Some bo, ty, _) ->
82 [NUri.ouri_of_nuri u,Cic.Constant
83 (name, Some (convert_term u 0 bo), convert_term u 0 ty, [],[])]
84 | u,_,_,_,NCic.Constant (_, name, None, ty, _) ->
85 [NUri.ouri_of_nuri u,Cic.Constant (name, None, convert_term u 0 ty, [],[])]
86 | u,_,_,_,NCic.Fixpoint (is_fix, fl, _) ->
90 UriManager.name_of_uri (NUri.ouri_of_nuri u) ^ string_of_int nth in
91 let buri = UriManager.buri_of_uri (NUri.ouri_of_nuri u) in
92 let uri = UriManager.uri_of_string (buri ^"/"^name^".con") in
95 Some (convert_fix is_fix u nth fl),
96 convert_term u 0 (let _,_,_,ty,_ = List.hd fl in ty), [], []))
97 (let rec seq = function 0 -> [0]|n -> n::seq (n-1) in
98 seq (List.length fl-1))
99 | _,_,_,_,NCic.Inductive _ -> assert false