* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Utils;;
let is_identity ((metasenv, context, ugraph) as env) = function
| ((_, _, (ty, left, right, _), menv, _) as equality) ->
- (left = right ||
+ (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))
+;;