- match (t1, t2) with
- (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
- let ok,subst,metasenv =
- try
- List.fold_left2
- (fun (b,subst,metasenv) t1 t2 ->
- if b then true,subst,metasenv else
- match t1,t2 with
- None,_
- | _,None -> true,subst,metasenv
- | Some t1', Some t2' ->
- (* First possibility: restriction *)
- (* Second possibility: unification *)
- (* Third possibility: convertibility *)
- if R.are_convertible subst context t1' t2' then
- true,subst,metasenv
- else
- (try
- let subst,metasenv =
- fo_unif_subst
- test_equality_only subst context metasenv t1' t2'
- in
- true,subst,metasenv
- with
- Not_found -> false,subst,metasenv)
- ) (true,subst,metasenv) ln lm
- with
- Invalid_argument _ ->
- raise (UnificationFailure (sprintf
- "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
- in
- if ok then
- subst,metasenv
- else
- raise (UnificationFailure (sprintf
- "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
- (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
- | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
- fo_unif_subst test_equality_only subst context metasenv t2 t1
- | (C.Meta (n,l), t)
- | (t, C.Meta (n,l)) ->
- let swap =
- match t1,t2 with
- C.Meta (n,_), C.Meta (m,_) when n < m -> false
- | _, C.Meta _ -> false
- | _,_ -> true
- in
- let lower = fun x y -> if swap then y else x in
- let upper = fun x y -> if swap then x else y in
- let fo_unif_subst_ordered
- test_equality_only subst context metasenv m1 m2 =
- fo_unif_subst test_equality_only subst context metasenv
- (lower m1 m2) (upper m1 m2)
- in
- begin
- try
- let (_, oldt) = CicMetaSubst.lookup_subst n subst in
- let lifted_oldt = S.lift_meta l oldt in
- let ty_lifted_oldt =
- type_of_aux' metasenv subst context lifted_oldt
- in
- let tyt = type_of_aux' metasenv subst context t in
- let (subst, metasenv) =
- fo_unif_subst_ordered test_equality_only subst context metasenv
- tyt ty_lifted_oldt
- in
- fo_unif_subst_ordered
- test_equality_only subst context metasenv t lifted_oldt
- with CicMetaSubst.SubstNotFound _ ->
- (* First of all we unify the type of the meta with the type of the term *)
- let subst,metasenv =
- let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
- (try
- let tyt = type_of_aux' metasenv subst context t in
- fo_unif_subst
- test_equality_only
- subst context metasenv tyt (S.lift_meta l meta_type)
- with AssertFailure _ ->
- (* TODO huge hack!!!!
- * we keep on unifying/refining in the hope that the problem will be
- * eventually solved. In the meantime we're breaking a big invariant:
- * the terms that we are unifying are no longer well typed in the
- * current context (in the worst case we could even diverge)
- *)
-(*
-prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
-prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
-*)
- (subst, metasenv))
+ let t1 = deref subst t1 in
+ let t2 = deref subst t2 in
+ let b,ugraph =
+ R.are_convertible ~subst ~metasenv context t1 t2 ugraph
+ in
+ if b then
+ subst, metasenv, ugraph
+ else
+ match (t1, t2) with
+ | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
+ let _,subst,metasenv,ugraph1 =
+ (try
+ List.fold_left2
+ (fun (j,subst,metasenv,ugraph) t1 t2 ->
+ match t1,t2 with
+ None,_
+ | _,None -> j+1,subst,metasenv,ugraph
+ | Some t1', Some t2' ->
+ (* First possibility: restriction *)
+ (* Second possibility: unification *)
+ (* Third possibility: convertibility *)
+ let b, ugraph1 =
+ R.are_convertible
+ ~subst ~metasenv context t1' t2' ugraph
+ in
+ if b then
+ j+1,subst,metasenv, ugraph1
+ else
+ (try
+ let subst,metasenv,ugraph2 =
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv t1' t2' ugraph
+ in
+ j+1,subst,metasenv,ugraph2
+ with
+ Uncertain _
+ | UnificationFailure _ ->
+debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j));
+ let metasenv, subst =
+ CicMetaSubst.restrict
+ subst [(n,j)] metasenv in
+ j+1,subst,metasenv,ugraph1)
+ ) (1,subst,metasenv,ugraph) ln lm
+ with
+ Exit ->
+ raise
+ (UnificationFailure "1")
+ (*
+ (sprintf
+ "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
+ (CicMetaSubst.ppterm subst t1)
+ (CicMetaSubst.ppterm subst t2))) *)
+ | Invalid_argument _ ->
+ raise
+ (UnificationFailure "2"))
+ (*
+ (sprintf
+ "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
+ (CicMetaSubst.ppterm subst t1)
+ (CicMetaSubst.ppterm subst t2)))) *)
+ in subst,metasenv,ugraph1
+ | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
+ fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
+ | (C.Meta (n,l), t)
+ | (t, C.Meta (n,l)) ->
+ let swap =
+ match t1,t2 with
+ C.Meta (n,_), C.Meta (m,_) when n < m -> false
+ | _, C.Meta _ -> false
+ | _,_ -> true