(* TASSI: CONSTRAINTS *)
| C.Sort (C.Type t) ->
let t' = CicUniv.fresh() in
- let ugraph1 = CicUniv.add_gt t' t ugraph in
- (C.Sort (C.Type t')),ugraph1
+ (try
+ let ugraph1 = CicUniv.add_gt t' t ugraph in
+ (C.Sort (C.Type t')),ugraph1
+ with
+ CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
| C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
| C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
| C.Cast (te,ty) as t ->
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
(* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
let t' = CicUniv.fresh() in
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.Type t'),ugraph2
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.Type t'),ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
| (C.Sort _,C.Sort (C.Type t1)) ->
(* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)