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 ->
| C.MutCase (uri,i,outtype,term,pl) ->
(match term with
C.Rel m when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let cl' =
List.map
(fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl
+ (id, snd (split_prods ~subst tys paramsno ty))) cl in
+ let lefts =
+ match tl with
+ [] -> assert false
+ | (_,_,ty,_)::_ ->
+ fst (split_prods ~subst [] paramsno ty)
in
- (tys,List.length tl,isinductive,paramsno,cl')
+ (tys@lefts,List.length tl,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
(fun (p,(_,c)) i ->
let rl' =
let debrujinedte = debrujin_constructor uri len c in
- recursive_args tys 0 len debrujinedte
+ recursive_args lefts_and_tys 0 len debrujinedte
in
let (e,safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let cl' =
List.map
(fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl
+ (id, snd (split_prods ~subst tys paramsno ty))) cl in
+ let lefts =
+ match tl with
+ [] -> assert false
+ | (_,_,ty,_)::_ ->
+ fst (split_prods ~subst [] paramsno ty)
in
- (tys,List.length tl,isinductive,paramsno,cl')
+ (tys@lefts,List.length tl,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
(fun (p,(_,c)) i ->
let rl' =
let debrujinedte = debrujin_constructor uri len c in
- recursive_args tys 0 len debrujinedte
+ recursive_args lefts_and_tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
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 ->
| C.MutCase (uri,i,outtype,term,pl) ->
(match CicReduction.whd ~subst context term with
C.Rel m when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let debrujinedty = debrujin_constructor uri len ty in
(id, snd (split_prods ~subst tys paramsno ty),
snd (split_prods ~subst tys paramsno debrujinedty)
- )) cl
+ )) cl in
+ let lefts =
+ match tl with
+ [] -> assert false
+ | (_,_,ty,_)::_ ->
+ fst (split_prods ~subst [] paramsno ty)
in
- (tys,len,isinductive,paramsno,cl')
+ (tys@lefts,len,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
(fun (p,(_,c,brujinedc)) i ->
- let rl' = recursive_args tys 0 len brujinedc in
+ let rl' = recursive_args lefts_and_tys 0 len brujinedc in
let (e,safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
in
guarded_by_destructors ~subst context' n' nn' kl x' safes' e
) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let cl' =
List.map
(fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl
+ (id, snd (split_prods ~subst tys paramsno ty))) cl in
+ let lefts =
+ match tl with
+ [] -> assert false
+ | (_,_,ty,_)::_ ->
+ fst (split_prods ~subst [] paramsno ty)
in
- (tys,List.length tl,isinductive,paramsno,cl')
+ (tys@lefts,List.length tl,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
(fun (p,(_,c)) i ->
let rl' =
let debrujinedte = debrujin_constructor uri len c in
- recursive_args tys 0 len debrujinedte
+ recursive_args lefts_and_tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
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
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? *)