(* $Id$ *)
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string]
let string_of_sort = function
| `Prop -> "Prop"
| `Set -> "Set"
| `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
- | `CProp -> "CProp"
+ | `NType s -> "Type[" ^ s ^ "]"
+ | `NCProp s -> "CProp[" ^ s ^ "]"
+ | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
+
let sort_of_sort = function
| Cic.Prop -> `Prop
| Cic.Set -> `Set
| Cic.Type u -> `Type u
- | Cic.CProp -> `CProp
+ | Cic.CProp u -> `CProp u
(* let hashtbl_add_time = ref 0.0;; *)
| C.Sort C.Set -> `Set
| C.Sort (C.Type u) -> `Type u
| C.Meta _ -> `Type (CicUniv.fresh())
- | C.Sort C.CProp -> `CProp
+ | C.Sort (C.CProp u) -> `CProp u
| t ->
prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
assert false
ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
;;
-let acic_object_of_cic_object ?(eta_fix=false) obj =
+let acic_term_or_object_of_cic_term_or_object ?(eta_fix=false) () =
let module C = Cic in
let module E = Eta_fixing in
let ids_to_terms = Hashtbl.create 503 in
let eta_fix_and_unshare metasenv context t =
let t = if eta_fix then E.eta_fix metasenv context t else t in
Unshare.unshare t in
+ (fun context t ->
+ let map = function
+ | None -> None
+ | Some (n, C.Decl ty) -> Some (n, C.Decl (Unshare.unshare ty))
+ | Some (n, C.Def (bo, ty)) ->
+ Some (n, C.Def (Unshare.unshare bo, Unshare.unshare ty))
+ in
+ let t = Unshare.unshare t in
+ let context = List.map map context in
+ let idrefs = List.map (function _ -> gen_id seed) context in
+ let t = acic_term_of_cic_term_context' ~computeinnertypes:true [] context idrefs t None in
+ t, ids_to_inner_sorts, ids_to_inner_types
+ ),(function obj ->
let aobj =
match obj with
C.Constant (id,Some bo,ty,params,attrs) ->
in
aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
ids_to_conjectures,ids_to_hypotheses
-;;
+);;
+
+let acic_object_of_cic_object ?eta_fix =
+ snd (acic_term_or_object_of_cic_term_or_object ?eta_fix ())
let plain_acic_term_of_cic_term =
let module C = Cic in
in
C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
;;
+
+let acic_term_of_cic_term ?eta_fix =
+ fst (acic_term_or_object_of_cic_term_or_object ?eta_fix ())