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
+ (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 ->
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? *)