* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Utils;;
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) ->
- (left = right ||
- (meta_convertibility left right) ||
- (fst (CicReduction.are_convertible context left right ugraph)))
+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
+ ~metasenv:(metasenv @ menv) context left right ugraph)))
+;;
+
+
+let term_of_equality equality =
+ let _, _, (ty, left, right, _), menv, args = equality in
+ let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
+ let argsno = List.length args in
+ let t =
+ CicSubstitution.lift argsno
+ (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+ in
+ snd (
+ List.fold_right
+ (fun a (n, t) ->
+ match a with
+ | Cic.Meta (i, _) ->
+ let name = Cic.Name ("X" ^ (string_of_int n)) in
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ let t =
+ ProofEngineReduction.replace
+ ~equality:eq ~what:[i]
+ ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
+ in
+ (n-1, Cic.Prod (name, ty, t))
+ | _ -> assert false)
+ args (argsno, t))
;;