- match (t1, t2) with
- (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
-(*
- let ok,subst,metasenv,ugraph1 =
- try
- List.fold_left2
- (fun (b,subst,metasenv,ugraph) t1 t2 ->
- if b then true,subst,metasenv,ugraph else
- match t1,t2 with
- None,_
- | _,None -> true,subst,metasenv,ugraph
- | Some t1', Some t2' ->
- (* First possibility: restriction *)
- (* Second possibility: unification *)
- (* Third possibility: convertibility *)
- let b',ugraph1 =
- R.are_convertible subst context t1' t2' ugraph in
- if b' then
- true,subst,metasenv,ugraph1
- else
- (try
- let subst,metasenv,ugraph2 =
- fo_unif_subst
- (* TASSI: is this another try that should use ugraph? *)
- test_equality_only subst context metasenv t1' t2' ugraph
- in
- true,subst,metasenv,ugraph2
- with
- Not_found -> false,subst,metasenv,ugraph1)
- ) (true,subst,metasenv,ugraph) 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,ugraph1
- 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)))
- *)
- 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 _ ->
-prerr_endline ("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
- 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 ugraph =
- fo_unif_subst test_equality_only subst context metasenv
- (lower m1 m2) (upper m1 m2) ugraph
- in
-(*
- begin
- try
- let (_, oldt) = CicMetaSubst.lookup_subst n subst in
- let lifted_oldt = S.subst_meta l oldt in
- let ty_lifted_oldt,ugraph1 =
- type_of_aux' metasenv subst context lifted_oldt ugraph
- in
- let tyt,ugraph2 = type_of_aux' metasenv subst context t ugraph1 in
- let (subst, metasenv, ugraph3) =
- fo_unif_subst_ordered test_equality_only subst context metasenv
- tyt ty_lifted_oldt ugraph2
- in
- fo_unif_subst_ordered
- test_equality_only subst context metasenv t lifted_oldt ugraph3
- with CicMetaSubst.SubstNotFound _ ->
- (* First of all we unify the type of the meta with the type of the term *)
- let subst,metasenv,ugraph1 =
- let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
- (try
- let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in
- fo_unif_subst
- test_equality_only
- subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
- 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,ugraph))
- in
- let t',metasenv,subst =
- try
- (* TASSI: I hope delift does nothing with universes *)
- CicMetaSubst.delift n subst context metasenv l t
- with
- (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
- | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
- in
- let t'',ugraph2 =
- match t' with
- C.Sort (C.Type u) when not test_equality_only ->
- let u' = CicUniv.fresh () in
- let s = C.Sort (C.Type u') in
- let ugraph2 =
- CicUniv.add_ge (upper u u') (lower u u') ugraph1 in
- s,ugraph2
- | _ -> t',ugraph1
- in
- (* Unifying the types may have already instantiated n. Let's check *)
- try
- let (_, oldt) = CicMetaSubst.lookup_subst n subst in
- let lifted_oldt = S.subst_meta l oldt in
- fo_unif_subst_ordered
- test_equality_only subst context metasenv t lifted_oldt ugraph2
+ 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