type equality =
- Cic.term * (* proof *)
+ int * (* weight *)
(Cic.term * (* type *)
Cic.term * (* left side *)
Cic.term * (* right side *)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
Printf.printf "OK: %s\n" (CicPp.ppterm term);
let o = !Utils.compare_terms t1 t2 in
- let e = (p, (ty, t1, t2, o), newmetas, args) in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, (ty, t1, t2, o), newmetas, args) in
store_proof e (BasicProof p);
Some e, (newmeta+1)
| _ -> None, newmeta
let t1 = S.lift index t1
and t2 = S.lift index t2 in
let o = !Utils.compare_terms t1 t2 in
- let e = (C.Rel index, (ty, t1, t2, o), [], []) in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, (ty, t1, t2, o), [], []) in
store_proof e (BasicProof (C.Rel index));
Some e, (newmeta+1)
| _ -> None, newmeta
;;
-let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
+let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) =
let table = Hashtbl.create (List.length args) in
let newargs, _ =
List.fold_right
(function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
in
(newmeta + (List.length newargs) + 1,
- (repl proof, (ty, left, right, o), menv', newargs))
+ (weight, (ty, left, right, o), menv', newargs))
;;
let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
| Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
let o = !Utils.compare_terms t1 t2 in
- let e = (proof, (ty, t1, t2, o), [], []) in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, (ty, t1, t2, o), [], []) in
store_proof e (BasicProof proof);
e
(* (proof, (ty, t1, t2, o), [], []) *)
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
+(*
let superposition_left (metasenv, context, ugraph) target source =
let module C = Cic in
let module S = CicSubstitution in
(!maxmeta,
(List.filter ok (new1 @ new2 @ new3 @ new4)))
;;
+*)
let is_identity ((_, context, ugraph) as env) = function
;;
+(*
let demodulation newmeta (metasenv, context, ugraph) target source =
let module C = Cic in
let module S = CicSubstitution in
);
res
;;
+*)
let extract_differing_subterms t1 t2 =