helm/software/components/ng_kernel/oCic2NCic.ml

   1 let convert_term = Obj.magic;;
   2
   3 let cn_to_s = function
   4   | Cic.Anonymous -> "_"
   5   | Cic.Name s -> s
   6 ;;
   7
   8 let rec convert_fix_definition acc = function
   9   | Cic.Lambda (n,s,t) ->
  10       convert_fix_definition ((n,s)::acc) t
  11   | Cic.Fix (_, [name,rno,ty,bo]) ->
  12       let acc = List.map (fun (n,s) -> cn_to_s n, convert_term s) acc in
  13       let ty = convert_term ty in
  14       let bo = convert_term bo in
  15       Some (true,[[],name,rno,
  16         List.fold_right (fun (n,s) acc -> NCic.Prod(n,s,acc)) acc ty,
  17         List.fold_right (fun (n,s) acc -> NCic.Lambda(n,s,acc)) acc bo])
  18   | Cic.CoFix (_, [name,ty,bo]) ->
  19       let acc = List.map (fun (n,s) -> cn_to_s n, convert_term s) acc in
  20       let ty = convert_term ty in
  21       let bo = convert_term bo in
  22       Some (false,[[],name,0,
  23         List.fold_right (fun (n,s) acc -> NCic.Prod(n,s,acc)) acc ty,
  24         List.fold_right (fun (n,s) acc -> NCic.Lambda(n,s,acc)) acc bo])
  25   | _ -> None
  26 ;;
  27
  28 let convert_obj_aux = function
  29  | Cic.Constant (name, None, ty, _, _) ->
  30      NCic.Constant ([], name, None, convert_term ty,
  31        (`Provided,`Theorem,`Regular))
  32  | Cic.Constant (name, Some bo, ty, _, _) ->
  33      (match convert_fix_definition [] bo with
  34      | None ->
  35          NCic.Constant ([], name, Some (convert_term bo), convert_term ty,
  36            (`Provided,`Theorem,`Regular))
  37      | Some (recursive, ifl) ->
  38          NCic.Fixpoint (recursive, ifl, (`Provided, `Definition)))
  39  | Cic.InductiveDefinition (itl,_,leftno,_) ->
  40      let ind = let _,x,_,_ = List.hd itl in x in
  41      let itl =
  42        List.map
  43          (fun name, _, ty, cl ->
  44             [], name, convert_term ty,
  45               List.map (fun name, ty -> [], name, convert_term ty) cl)
  46          itl
  47      in
  48      NCic.Inductive (ind, leftno, itl, (`Provided, `Regular))
  49  | Cic.Variable _
  50  | Cic.CurrentProof _ -> assert false
  51 ;;
  52
  53 let convert_obj uri obj = NUri.nuri_of_ouri uri,0, [], [], convert_obj_aux obj;;