+let convert_term = Obj.magic;;
-let convert_obj obj = Obj.magic obj
+let cn_to_s = function
+ | Cic.Anonymous -> "_"
+ | Cic.Name s -> s
+;;
+
+let rec convert_fix_definition acc = function
+ | Cic.Lambda (n,s,t) ->
+ convert_fix_definition ((n,s)::acc) t
+ | Cic.Fix (_, [name,rno,ty,bo]) ->
+ let acc = List.map (fun (n,s) -> cn_to_s n, convert_term s) acc in
+ let ty = convert_term ty in
+ let bo = convert_term bo in
+ Some (true,[[],name,rno,
+ List.fold_right (fun (n,s) acc -> NCic.Prod(n,s,acc)) acc ty,
+ List.fold_right (fun (n,s) acc -> NCic.Lambda(n,s,acc)) acc bo])
+ | Cic.CoFix (_, [name,ty,bo]) ->
+ let acc = List.map (fun (n,s) -> cn_to_s n, convert_term s) acc in
+ let ty = convert_term ty in
+ let bo = convert_term bo in
+ Some (false,[[],name,0,
+ List.fold_right (fun (n,s) acc -> NCic.Prod(n,s,acc)) acc ty,
+ List.fold_right (fun (n,s) acc -> NCic.Lambda(n,s,acc)) acc bo])
+ | _ -> None
+;;
+
+let convert_obj_aux = function
+ | Cic.Constant (name, None, ty, _, _) ->
+ NCic.Constant ([], name, None, convert_term ty,
+ (`Provided,`Theorem,`Regular))
+ | Cic.Constant (name, Some bo, ty, _, _) ->
+ (match convert_fix_definition [] bo with
+ | None ->
+ NCic.Constant ([], name, Some (convert_term bo), convert_term ty,
+ (`Provided,`Theorem,`Regular))
+ | Some (recursive, ifl) ->
+ NCic.Fixpoint (recursive, ifl, (`Provided, `Definition)))
+ | Cic.InductiveDefinition (itl,_,leftno,_) ->
+ let ind = let _,x,_,_ = List.hd itl in x in
+ let itl =
+ List.map
+ (fun name, _, ty, cl ->
+ [], name, convert_term ty,
+ List.map (fun name, ty -> [], name, convert_term ty) cl)
+ itl
+ in
+ NCic.Inductive (ind, leftno, itl, (`Provided, `Regular))
+ | Cic.Variable _
+ | Cic.CurrentProof _ -> assert false
+;;
+
+let convert_obj uri obj = NUri.nuri_of_ouri uri,0, [], [], convert_obj_aux obj;;
projects / helm.git / commitdiff