let len = List.length fl in
let n_plus_len = n + len in
let nn_plus_len = nn + len in
- let tys =
- List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
List.fold_right
(fun (_,_,ty,bo) i ->
let len = List.length fl in
let n_plus_len = n + len in
let nn_plus_len = nn + len in
- let tys =
- List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
List.fold_right
(fun (_,ty,bo) i ->
let n_plus_len = n + len
and nn_plus_len = nn + len
and x_plus_len = x + len
- and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+ and tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
and safes' = List.map (fun x -> x + len) safes in
List.fold_right
(fun (_,_,ty,bo) i ->
let n_plus_len = n + len
and nn_plus_len = nn + len
and x_plus_len = x + len
- and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+ and tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
and safes' = List.map (fun x -> x + len) safes in
List.fold_right
(fun (_,ty,bo) i ->
let n_plus_len = n + len
and nn_plus_len = nn + len
and x_plus_len = x + len
- and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+ and tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
and safes' = List.map (fun x -> x + len) safes in
List.fold_right
(fun (_,_,ty,bo) i ->
let n_plus_len = n + len
and nn_plus_len = nn + len
and x_plus_len = x + len
- and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+ and tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
and safes' = List.map (fun x -> x + len) safes in
List.fold_right
(fun (_,ty,bo) i ->
let n_plus_len = n + len
and nn_plus_len = nn + len
(*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
- and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+ and tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
+ in
List.fold_right
(fun (_,ty,bo) i ->
i && does_not_occur ~subst context n nn ty &&
let n_plus_len = n + len
and nn_plus_len = nn + len
(*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
- and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
+ and tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
+ in
List.fold_right
(fun (_,_,ty,bo) i ->
i && does_not_occur ~subst context n nn ty &&
let n_plus_len = n + len
and nn_plus_len = nn + len
(*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
- and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+ and tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
+ in
List.fold_right
(fun (_,ty,bo) i ->
i && does_not_occur ~subst context n nn ty &&
(* 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
- (* TASSI: CONSTRAINTS *)
+ (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 "21"))
+ | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
| C.Cast (te,ty) as t ->
let _,ugraph1 = type_of_aux ~logger context ty ugraph in
let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
in
if not b then
raise
- (TypeCheckerFailure (lazy ("Case analasys: sort elimination not allowed")));
+ (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed")));
(* let's check if the type of branches are right *)
- let parsno =
+ let parsno,constructorsno =
let obj,_ =
try
CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
with Not_found -> assert false
in
match obj with
- C.InductiveDefinition (_,_,parsno,_) -> parsno
+ C.InductiveDefinition (il,_,parsno,_) ->
+ let _,_,_,cl =
+ try List.nth il i with Failure _ -> assert false
+ in
+ parsno, List.length cl
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
UriManager.string_of_uri uri)))
- in
+ in
+ if List.length pl <> constructorsno then
+ raise (TypeCheckerFailure
+ (lazy ("Wrong number of cases in case analysis"))) ;
let (_,branches_ok,ugraph5) =
List.fold_left
(fun (j,b,ugraph) p ->
in
outtype,ugraph5
| C.Fix (i,fl) ->
- let types_times_kl,ugraph1 =
- (* WAS: list rev list map *)
+ let types,kl,ugraph1,len =
List.fold_left
- (fun (l,ugraph) (n,k,ty,_) ->
+ (fun (types,kl,ugraph,len) (n,k,ty,_) ->
let _,ugraph1 = type_of_aux ~logger context ty ugraph in
- ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
- ) ([],ugraph) fl
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ k::kl,ugraph1,len+1)
+ ) ([],[],ugraph,0) fl
in
- let (types,kl) = List.split types_times_kl in
- let len = List.length types in
let ugraph2 =
List.fold_left
(fun ugraph (name,x,ty,bo) ->
let (_,_,ty,_) = List.nth fl i in
ty,ugraph2
| C.CoFix (i,fl) ->
- let types,ugraph1 =
+ let types,ugraph1,len =
List.fold_left
- (fun (l,ugraph) (n,ty,_) ->
+ (fun (l,ugraph,len) (n,ty,_) ->
let _,ugraph1 =
type_of_aux ~logger context ty ugraph in
- (Some (C.Name n,(C.Decl ty))::l,ugraph1)
- ) ([],ugraph) fl
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
+ ugraph1,len+1)
+ ) ([],ugraph,0) fl
in
- let len = List.length types in
let ugraph2 =
List.fold_left
(fun ugraph (_,ty,bo) ->
| (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? *)