let convert_term = Obj.magic;;

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;;