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 &&
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 ->
outtype,ugraph5
| C.Fix (i,fl) ->
let types,kl,ugraph1,len =
- (* WAS: list rev list map *)
List.fold_left
(fun (types,kl,ugraph,len) (n,k,ty,_) ->
let _,ugraph1 = type_of_aux ~logger context ty ugraph in