- let attrs, cc, ty = NCicUtils.lookup_meta n metasenv in
- match NCicUntrusted.kind_of_meta attrs, ty, t, swap with
- | `IsSort, (NCic.Implicit (`Typeof _) as bot), NCic.Sort (NCic.Type u),false->
- pp(lazy("1"));
- let u = NCicEnvironment.inf ~strict:false u in
- let t = NCic.Sort (NCic.Type (unopt exc u)) in
- move_to_subst n attrs cc t bot metasenv subst
- | `IsSort, (NCic.Implicit (`Typeof _) as bot), NCic.Sort (NCic.Type u),true ->
- pp(lazy("2"));
- let u = NCicEnvironment.sup u in
- let t = NCic.Sort (NCic.Type (unopt exc u)) in
- move_to_subst n attrs cc t bot metasenv subst
- | `IsSort, (NCic.Sort(NCic.Type u1) as ty), NCic.Sort (NCic.Type u2), false ->
- pp(lazy("3"));
- let u =
- NCicEnvironment.inf ~strict:false (u1 @
- unopt exc (NCicEnvironment.inf ~strict:true u2))
- in
- let t = NCic.Sort (NCic.Type (unopt exc u)) in
- move_to_subst n attrs cc t ty metasenv subst
- | `IsSort, (NCic.Sort(NCic.Type u1) as ty), NCic.Sort (NCic.Type u2), true ->
- pp(lazy("4"));
- let u = unopt exc (NCicEnvironment.sup u2) in
- if NCicEnvironment.universe_lt u u1 then
- let t = NCic.Sort (NCic.Type u) in
- move_to_subst n attrs cc t ty metasenv subst
- else (raise exc)
- | _, _, NCic.Meta(m,lcm), _ when List.mem_assoc m subst ->
- (* deref needed for locked metas, maybe should be done outside *)
- let _,_,bo,_ = NCicUtils.lookup_subst m subst in
- let bo = NCicSubstitution.subst_meta lcm bo in
- instantiate rdb test_eq_only metasenv subst context n lc bo swap
- | kind, (NCic.Implicit (`Typeof _) as bot), NCic.Meta(m,lcm), _ ->
- pp(lazy("5"));
- let attrsm, ccm, tym = NCicUtils.lookup_meta m metasenv in
- let kindm = NCicUntrusted.kind_of_meta attrsm in
- let metasenv, t = kindfy exc metasenv subst ccm m lcm tym kindm kind in
- move_to_subst n attrs cc t bot metasenv subst
- | kind, ty, (NCic.Meta(m,_) as t), _ when
- let _, _, tym = NCicUtils.lookup_meta m metasenv in
- (match tym with NCic.Implicit (`Typeof _) -> true | _ -> false) ->
- pp(lazy("6"));
- let attrsm, _, _ = NCicUtils.lookup_meta m metasenv in
- let kindm = NCicUntrusted.kind_of_meta attrsm in
- let metasenv, _ = kindfy exc metasenv subst cc n lc ty kind kindm in
- let attrs, cc, ty = NCicUtils.lookup_meta n metasenv in
- let metasenv = NCicUntrusted.replace_in_metasenv m
- (fun _,_,_ -> attrs,cc,ty) metasenv
- in
- (* XXX *)move_to_subst n attrs cc t ty metasenv subst
- | kind, ty, NCic.Meta(m,lcm), _ ->
- pp(lazy("7"));
- let ty_t, ccm, kindm =
- let at, ccm, tym = NCicUtils.lookup_meta m metasenv in
- NCicSubstitution.subst_meta lcm tym, ccm, NCicUntrusted.kind_of_meta at
- in
- let lty = NCicSubstitution.subst_meta lc ty in
- pp (lazy ("On the types: " ^
- ppterm ~metasenv ~subst ~context lty ^
- (if test_eq_only then " === " else "=<=") ^
- ppterm ~metasenv ~subst ~context ty_t));
- let metasenv, subst =
- unify rdb test_eq_only metasenv subst context ty_t lty
- in
- let metasenv, t = kindfy exc metasenv subst ccm m lcm ty_t kindm kind in
- delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst
- | _, (NCic.Implicit (`Typeof _) as bot), t, swap ->
- pp(lazy("8"));
- let metasenv, t = fix metasenv subst swap test_eq_only exc t in
-(* let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in *)
- (* ty andrebbe deliftato *)
- delift_to_subst test_eq_only n lc attrs cc t bot context metasenv subst
- | _, ty, t, swap ->
- pp(lazy("9"));
- let lty = NCicSubstitution.subst_meta lc ty in
- let metasenv, t = fix metasenv subst swap test_eq_only exc t in
- let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in
- pp (lazy ("On the types: " ^
- ppterm ~metasenv ~subst ~context lty ^
- (if test_eq_only then " === " else "=<=") ^
- ppterm ~metasenv ~subst ~context ty_t));
- let metasenv, subst =
- unify rdb test_eq_only metasenv subst context ty_t lty
- in
- delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst
+ let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in
+ let kind = NCicUntrusted.kind_of_meta attrs in
+ let metasenv,t = fix metasenv subst swap test_eq_only exc t in
+ let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in
+ let metasenv,subst,t =
+ match kind with
+ `IsSort -> sortfy exc metasenv subst context t
+ | `IsType -> tipify exc metasenv subst context t ty_t
+ | `IsTerm -> metasenv,subst,t in
+ match kind with
+ | `IsSort ->
+ (match ty,t with
+ NCic.Implicit (`Typeof _), NCic.Sort _ ->
+ move_to_subst n (attrs,cc,t,ty_t) metasenv subst
+ | NCic.Sort (NCic.Type u1), NCic.Sort s ->
+ let s =
+ match s,swap with
+ NCic.Type u2, false ->
+ NCic.Sort (NCic.Type
+ (unopt exc (NCicEnvironment.inf ~strict:false
+ (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
+ | NCic.Type u2, true ->
+ if NCicEnvironment.universe_lt u2 u1 then
+ NCic.Sort (NCic.Type u2)
+ else (raise exc)
+ | NCic.Prop,_ -> NCic.Sort NCic.Prop
+ in
+ move_to_subst n (attrs,cc,s,ty) metasenv subst
+ | NCic.Implicit (`Typeof _), NCic.Meta _ ->
+ move_to_subst n (attrs,cc,t,ty_t) metasenv subst
+ | _, NCic.Meta _
+ | NCic.Meta _, NCic.Sort _ ->
+ pp (lazy ("On the types: " ^
+ ppterm ~metasenv ~subst ~context ty ^ "=<=" ^
+ ppterm ~metasenv ~subst ~context ty_t));
+ let metasenv, subst =
+ unify rdb false metasenv subst context ty_t ty false in
+ delift_to_subst test_eq_only n lc (attrs,cc,ty) t
+ context metasenv subst
+ | _ -> assert false)
+ | `IsType
+ | `IsTerm ->
+ (match ty with
+ NCic.Implicit (`Typeof _) ->
+ let (metasenv, subst), ty_t =
+ try
+ NCicMetaSubst.delift
+ ~unify:(fun m s c t1 t2 ->
+ let ind = !indent in
+ let res = try Some (unify rdb test_eq_only m s c t1 t2 false )
+ with UnificationFailure _ | Uncertain _ -> None
+ in
+ indent := ind; res)
+ metasenv subst context n lc ty_t
+ with NCicMetaSubst.Uncertain msg ->
+ pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
+ raise (Uncertain msg)
+ | NCicMetaSubst.MetaSubstFailure msg ->
+ pp (lazy ("delift fails: " ^ Lazy.force msg));
+ raise (UnificationFailure msg)
+ in
+ delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
+ subst
+ | _ ->
+ let lty = NCicSubstitution.subst_meta lc ty in
+ pp (lazy ("On the types: " ^
+ ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^
+ ppterm ~metasenv ~subst ~context lty));
+ let metasenv, subst =
+ unify rdb false metasenv subst context ty_t lty false
+ in
+ delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
+ subst)