unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
raise
- (U.UnificationFailure
- (U.failure_msg_of_string "Inference.unification.unif"))
+ (U.UnificationFailure (lazy "Inference.unification.unif"))
| C.Meta (i, l), t -> (
try
let _, _, ty = CicUtil.lookup_meta i menv in
)
| _, C.Meta _ -> unif subst menv t s
| C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
- raise (U.UnificationFailure
- (U.failure_msg_of_string "Inference.unification.unif"))
+ raise (U.UnificationFailure (lazy "Inference.unification.unif"))
| C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
try
List.fold_left2
(fun (subst', menv) s t -> unif subst' menv s t)
(subst, menv) tls tlt
with Invalid_argument _ ->
- raise (U.UnificationFailure
- (U.failure_msg_of_string "Inference.unification.unif"))
+ raise (U.UnificationFailure (lazy "Inference.unification.unif"))
)
| _, _ ->
- raise (U.UnificationFailure
- (U.failure_msg_of_string "Inference.unification.unif"))
+ raise (U.UnificationFailure (lazy "Inference.unification.unif"))
in
let subst, menv = unif [] metasenv t1 t2 in
let menv =
;;
-(* let unification = CicUnification.fo_unif;; *)
+let unification = CicUnification.fo_unif;;
exception MatchingFailure;;
;;
+(*
let equations_blacklist =
List.fold_left
(fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
"cic:/matita/logic/equality/eq_rect.con";
]
;;
+*)
+let equations_blacklist = UriManager.UriSet.empty;;
+
let find_library_equalities dbd context status maxmeta =
let module C = Cic in
let uriset, eqlist =
(List.fold_left
(fun (s, l) (u, e) ->
- if List.exists (meta_convertibility_eq e) l then (
+ if List.exists (meta_convertibility_eq e) (List.map snd l) then (
debug_print
(lazy
(Printf.sprintf "NO!! %s already there!"
(string_of_equality e)));
(UriManager.UriSet.add u s, l)
- ) else (UriManager.UriSet.add u s, e::l))
+ ) else (UriManager.UriSet.add u s, (u, e)::l))
(UriManager.UriSet.empty, []) found)
in
uriset, eqlist, maxm
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
-let is_identity ((_, context, ugraph) as env) = function
- | ((_, _, (ty, left, right, _), _, _) as equality) ->
+let is_identity ((metasenv, context, ugraph) as env) = function
+ | ((_, _, (ty, left, right, _), menv, _) as equality) ->
(left = right ||
- (meta_convertibility left right) ||
- (fst (CicReduction.are_convertible context left right ugraph)))
+ (* (meta_convertibility left right) || *)
+ (fst (CicReduction.are_convertible
+ ~metasenv:(metasenv @ menv) context left right ugraph)))
;;