+ let metasenv,subst,_ = sortfy exc metasenv subst context ty in
+ metasenv,subst,t
+;;
+
+let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
+ (*D*) inside 'I'; try let rc =
+ pp (lazy(string_of_int n^" :=?= "^ppterm ~metasenv ~subst ~context t));
+ let exc =
+ UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t) in
+ let move_to_subst i ((_,cc,t,_) as infos) metasenv subst =
+ let metasenv = List.remove_assoc i metasenv in
+ pp(lazy(string_of_int n ^ " :==> "^ ppterm ~metasenv ~subst ~context:cc t));
+ metasenv, (i,infos) :: subst
+ in
+ let delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv subst =
+ pp (lazy(string_of_int n ^ " := 111 = "^
+ 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 rdb 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 is uncertain: " ^ 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 = "^
+ ppterm ~metasenv ~subst ~context:cc 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 rdb test_eq_only metasenv subst context t oldt
+ with NCicUtils.Subst_not_found _ ->
+ move_to_subst n (attrs,cc,t,ty) metasenv subst
+ in
+ 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 in
+ delift_to_subst test_eq_only n lc (attrs,cc,ty) t
+ context metasenv subst
+ | _ -> assert false)
+ | `IsType
+ | `IsTerm ->
+ (match ty,t 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 )
+ 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 lty ^ "=<=" ^
+ ppterm ~metasenv ~subst ~context ty_t));
+ let metasenv, subst =
+ unify rdb false metasenv subst context ty_t lty
+ in
+ delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
+ subst)
+(*
+ | kind, ty, NCic.Meta(m,lcm), _ when List.mem_assoc m subst ->
+ let at,ccm,bo,tym = NCicUtils.lookup_subst m subst in
+ if NCicMetaSubst.is_out_scope_tag at then
+ begin
+ (* Case meta vs out-scope *)
+ pp(lazy("4.1"));
+ let ty_t, ccm, kindm =
+ 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 ^ "=<=" ^
+ ppterm ~metasenv ~subst ~context ty_t));
+ let metasenv, subst =
+ unify rdb false metasenv subst context ty_t lty in
+ (*CSC: here I should call kindfy, but it fails since the second
+ meta in in the susbt, not the metasenv! *)
+ (* let metasenv,subst,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
+ end
+ else
+ let bo = NCicSubstitution.subst_meta lcm bo in
+ instantiate rdb test_eq_only metasenv subst context n lc bo swap
+*)
+ (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
+
+and unify rdb test_eq_only metasenv subst context t1 t2 =
+ (*D*) inside 'U'; try let rc =
+ let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
+ (*D*) inside 'F'; try let rc =
+ pp (lazy(" " ^ ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
+ ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
+ ~subst metasenv));
+ pp (lazy(" " ^ ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^
+ ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
+ ~subst metasenv));
+ if t1 === t2 then
+ metasenv, subst
+(* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
+ else if
+ NCicUntrusted.metas_of_term subst context t1 = [] &&
+ NCicUntrusted.metas_of_term subst context t2 = []
+ then
+ if NCicReduction.are_convertible ~metasenv ~subst context t1 t2 then
+ metasenv,subst
+ else
+ raise (UnificationFailure (lazy "Closed terms not convertible"))
+*)
+ else
+ match (t1,t2) with
+ | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
+ | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
+ prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
+ assert false
+ | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
+ if NCicEnvironment.universe_leq a b then metasenv, subst
+ else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
+ | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
+ if NCicEnvironment.universe_eq a b then metasenv, subst
+ else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
+ | (C.Sort C.Prop,C.Sort (C.Type _)) ->
+ if (not test_eq_only) then metasenv, subst
+ else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
+
+ | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
+ | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+ let metasenv, subst = unify rdb true metasenv subst context s1 s2 in
+ unify rdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
+ | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
+ let metasenv,subst=unify rdb test_eq_only metasenv subst context ty1 ty2 in
+ let metasenv,subst=unify rdb test_eq_only metasenv subst context s1 s2 in
+ let context = (name1, C.Def (s1,ty1))::context in
+ unify rdb test_eq_only metasenv subst context t1 t2
+
+ | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
+ (try
+ let l1 = NCicUtils.expand_local_context l1 in
+ let l2 = NCicUtils.expand_local_context l2 in
+ let metasenv, subst, to_restrict, _ =
+ List.fold_right2
+ (fun t1 t2 (metasenv, subst, to_restrict, i) ->
+ try
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context
+ (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
+ in
+ metasenv, subst, to_restrict, i-1
+ with UnificationFailure _ | Uncertain _ ->
+ metasenv, subst, i::to_restrict, i-1)
+ l1 l2 (metasenv, subst, [], List.length l1)
+ in
+ if to_restrict <> [] then
+ let metasenv, subst, _ =
+ NCicMetaSubst.restrict metasenv subst n1 to_restrict
+ in
+ metasenv, subst
+ else metasenv, subst
+ with
+ | Invalid_argument _ -> assert false
+ | NCicMetaSubst.MetaSubstFailure msg ->
+ try
+ let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
+ let term1 = NCicSubstitution.subst_meta lc1 term in
+ let term2 = NCicSubstitution.subst_meta lc2 term in
+ unify rdb test_eq_only metasenv subst context term1 term2
+ with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
+
+ | NCic.Appl (NCic.Meta (i,_)::_ as l1),
+ NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
+ (try
+ List.fold_left2
+ (fun (metasenv, subst) t1 t2 ->
+ unify rdb test_eq_only metasenv subst context t1 t2)
+ (metasenv,subst) l1 l2
+ with Invalid_argument _ ->
+ raise (UnificationFailure (mk_msg metasenv subst context t1 t2)))
+
+ | _, NCic.Meta (n, _) when is_locked n subst ->
+ (let (metasenv, subst), i =
+ match NCicReduction.whd ~subst context t1 with
+ | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
+ let metasenv, lambda_Mj =
+ lambda_intros rdb metasenv subst context (List.length args)
+ (NCicTypeChecker.typeof ~metasenv ~subst context meta)
+ in
+ unify rdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj,
+ i
+ | NCic.Meta (i,_) -> (metasenv, subst), i
+ | _ ->
+ raise (UnificationFailure (lazy "Locked term vs non
+ flexible term; probably not saturated enough yet!"))
+ in
+ let t1 = NCicReduction.whd ~subst context t1 in
+ let j, lj =
+ match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
+ in
+ let metasenv, subst =
+ instantiate rdb test_eq_only metasenv subst context j lj t2 true
+ in
+ (* We need to remove the out_scope_tags to avoid propagation of
+ them that triggers again the ad-hoc case *)
+ let subst =
+ List.map (fun (i,(tag,ctx,bo,ty)) ->
+ let tag =
+ List.filter
+ (function `InScope | `OutScope _ -> false | _ -> true) tag
+ in
+ i,(tag,ctx,bo,ty)
+ ) subst
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ let term = eta_reduce subst term in
+ let subst = List.filter (fun (j,_) -> j <> i) subst in
+ metasenv, ((i, (name, ctx, term, ty)) :: subst)
+ with Not_found -> assert false))
+
+ | C.Meta (n,lc), t when List.mem_assoc n subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst n subst in
+ let term = NCicSubstitution.subst_meta lc term in
+ unify rdb test_eq_only metasenv subst context term t
+
+ | t, C.Meta (n,lc) when List.mem_assoc n subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst n subst in
+ let term = NCicSubstitution.subst_meta lc term in
+ unify rdb test_eq_only metasenv subst context t term
+
+ | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst i subst in
+ let term = NCicSubstitution.subst_meta l term in
+ unify rdb test_eq_only metasenv subst context
+ (mk_appl ~upto:(List.length args) term args) t2
+
+ | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst i subst in
+ let term = NCicSubstitution.subst_meta l term in
+ unify rdb test_eq_only metasenv subst context t1
+ (mk_appl ~upto:(List.length args) term args)
+
+ | C.Meta (n,lc), t ->
+ instantiate rdb test_eq_only metasenv subst context n lc
+ (NCicReduction.head_beta_reduce ~subst t) false
+
+ | t, C.Meta (n,lc) ->
+ instantiate rdb test_eq_only metasenv subst context n lc
+ (NCicReduction.head_beta_reduce ~subst t) true
+
+ | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
+ let metasenv, lambda_Mj =
+ lambda_intros rdb metasenv subst context (List.length args)
+ (NCicTypeChecker.typeof ~metasenv ~subst context meta)
+ in
+ let metasenv, subst =
+ try
+ unify rdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj
+ with UnificationFailure msg | Uncertain msg when not norm2->
+ (* failure: let's try again argument vs argument *)
+ raise (KeepReducing msg)
+ in
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context t1 t2
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ let term = eta_reduce subst term in
+ let subst = List.filter (fun (j,_) -> j <> i) subst in
+ metasenv, ((i, (name, ctx, term, ty)) :: subst)
+ with Not_found -> assert false)
+
+ | _, NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
+ let metasenv, lambda_Mj =
+ lambda_intros rdb metasenv subst context (List.length args)
+ (NCicTypeChecker.typeof ~metasenv ~subst context meta)