- let metasenv = remove_and_hope i in
- let metasenv =
- (i,(None,[],NCic.Implicit (`Typeof i)))::
- List.filter (fun i',_ -> i <> i') metasenv
- in
- metasenv,subst,t
- | NCic.Appl (NCic.Meta _::_) ->
- raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
- | t when could_reduce t ->
- raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
- | _ ->
- raise (UnificationFailure (lazy "Trying to instantiate a metavariable that represents a sort with a term")))
- | _ ->
- pp (lazy (
- "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
- ppcontext ~metasenv ~subst context ^
- ppmetasenv ~subst metasenv));
- let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
- let t, ty_t =
- try t, NCicTypeChecker.typeof ~subst ~metasenv context t
- with
- | NCicTypeChecker.AssertFailure msg ->
- (pp (lazy "fine typeof (fallimento)");
- let ft = fix_sorts swap exc_to_be t in
- if ft == t then
- (prerr_endline ( ("ILLTYPED: " ^
- NCicPp.ppterm ~metasenv ~subst ~context t
- ^ "\nBECAUSE:" ^ Lazy.force msg ^
- ppcontext ~metasenv ~subst context ^
- ppmetasenv ~subst metasenv
- ));
- assert false)
- else
- try
- pp (lazy ("typeof: " ^
- NCicPp.ppterm ~metasenv ~subst ~context ft));
- ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
- with NCicTypeChecker.AssertFailure _ ->
- assert false)
- | NCicTypeChecker.TypeCheckerFailure msg ->
- prerr_endline (Lazy.force msg);
- prerr_endline (
- "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
- ppcontext ~metasenv ~subst context ^
- ppmetasenv ~subst metasenv);
- pp msg; assert false
- in
- let lty = NCicSubstitution.subst_meta lc ty in
- match ty_t with
- | NCic.Implicit _ ->
- raise (UnificationFailure
- (lazy "trying to unify a term with a type"))
- | ty_t ->
- pp (lazy ("On the types: " ^
- NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
- NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
- ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
- let metasenv,subst =
- try
- unify test_eq_only metasenv subst context lty ty_t
- with NCicEnvironment.BadConstraint _ as exc ->
- let ty_t = fix_sorts swap exc_to_be ty_t in
- try unify test_eq_only metasenv subst context lty ty_t
- with _ -> raise exc in
- metasenv, subst, t
- in
- pp (lazy(string_of_int n ^ " := 111 = "^
- NCicPp.ppterm ~metasenv ~subst ~context t));
- let (metasenv, subst), t =
- try
- NCicMetaSubst.delift
- ~unify:(fun m s c t1 t2 ->
- let ind = !indent in
- let res =
- try Some (unify test_eq_only m s c t1 t2 )
- with UnificationFailure _ | Uncertain _ -> None
- in
- indent := ind; res)
- metasenv subst context n lc t
- with NCicMetaSubst.Uncertain msg ->
- pp (lazy ("delift fails: " ^ Lazy.force msg));
- raise (Uncertain msg)
- | NCicMetaSubst.MetaSubstFailure msg ->
- pp (lazy ("delift fails: " ^ Lazy.force msg));
- raise (UnificationFailure msg)
- in
- pp (lazy(string_of_int n ^ " := 222 = "^
- NCicPp.ppterm ~metasenv ~subst ~context:ctx t
- ^ ppmetasenv ~subst metasenv));
- (* Unifying the types may have already instantiated n. *)
- try
- let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
- let oldt = NCicSubstitution.subst_meta lc oldt in
- let t = NCicSubstitution.subst_meta lc t in
- (* conjecture: always fail --> occur check *)
- unify test_eq_only metasenv subst context oldt t
- with NCicUtils.Subst_not_found _ ->
- (* by cumulativity when unify(?,Type_i)
- * we could ? := Type_j with j <= i... *)
- let subst = (n, (name, ctx, t, ty)) :: subst in
- pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
- ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
- let metasenv =
- List.filter (fun (m,_) -> not (n = m)) metasenv