+ let patterns_of pl =
+ let constructors, leftno =
+ let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in
+ let _,_,_,cl = List.nth tys n in
+ cl,leftno
+ in
+ let rec eat_branch n ty context ctx pat =
+ match (ty, pat) with
+ | TSkip t,_
+ | Forall (_,_,t),_
+ | Arrow (_, t), _ when n > 0 ->
+ eat_branch (pred n) t context ctx pat
+ | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
+ (*CSC: unify the three cases below? *)
+ | Arrow (_, t), NCic.Lambda (name, ty, t') ->
+ let ctx =
+ (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
+ let ctx =
+ (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | TSkip t,NCic.Lambda (name, ty, t') ->
+ let ctx = None::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | Top,_ -> assert false (* IMPOSSIBLE *)
+ | TSkip _, _
+ | Forall _,_
+ | Arrow _,_ -> assert false (*BUG here, eta-expand!*)
+ | _, _ -> context,ctx, pat
+ in
+ try
+ List.map2
+ (fun (_, _name, ty) pat ->
+ (*BUG: recomputing every time the type of the constructor*)
+ let ty = typ_of status ~metasenv context ty in
+ let context,lhs,rhs = eat_branch leftno ty context [] pat in
+ let rhs =
+ (* UnsafeCoerce not always required *)
+ UnsafeCoerce (term_of status ~metasenv context rhs)
+ in
+ lhs,rhs
+ ) constructors pl
+ with Invalid_argument _ -> assert false
+ in