* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Utils;;
;;
-(* 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))
;;