- (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
- with
- CicMetaSubst.SubstNotFound _ ->
- let (_, context, _) = CicUtil.lookup_meta n metasenv in
- let subst = (n, (context, t'')) :: subst in
- let metasenv =
-(* CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
- CicMetaSubst.apply_subst_metasenv subst metasenv
- in
- subst, metasenv,ugraph2
-(* (n,t'')::subst, metasenv *)
- end
-*)
+ (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