* http://cs.unibo.it/helm/.
*)
-type sort_kind = [ `Prop | `Set | `Type | `CProp ]
-
-let sort_of_string = function
- | "Prop" -> `Prop
- | "Set" -> `Set
- | "Type" -> `Type
- | "CProp" -> `CProp
- | _ -> assert false
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
let string_of_sort = function
| `Prop -> "Prop"
| `Set -> "Set"
- | `Type -> "Type"
+ | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u)
| `CProp -> "CProp"
let sort_of_sort = function
| Cic.Prop -> `Prop
| Cic.Set -> `Set
- | Cic.Type _ -> `Type
+ | Cic.Type u -> `Type u
| Cic.CProp -> `CProp
(* let hashtbl_add_time = ref 0.0;; *)
match CicReduction.whd context t with
C.Sort C.Prop -> `Prop
| C.Sort C.Set -> `Set
- | C.Sort (C.Type _)
- | C.Meta _ -> `Type
+ | C.Sort (C.Type u) -> `Type u
+ | C.Meta _ -> `Type (CicUniv.fresh())
| C.Sort C.CProp -> `CProp
| t ->
prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
with
Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *)
(* CSC: Type or Set? I can not tell *)
- None,Cic.Sort (Cic.Type (CicUniv.fresh())),`Type,false
+ let u = CicUniv.fresh() in
+ None,Cic.Sort (Cic.Type u),`Type u,false
(* TASSI non dovrebbe fare danni *)
(* *)
in