build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
let res =
- (C.Implicit None, (eq_ty, left, right, ordering), newmetasenv, newargs)
+ let w = Utils.compute_equality_weight eq_ty left right in
+ (w, (eq_ty, left, right, ordering), newmetasenv, newargs)
in
Inference.store_proof res newproof;
newmeta, res
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
- let res = (C.Implicit None, (eq_ty, left, right, neworder), [], []) in
+ let res =
+ let w = Utils.compute_equality_weight eq_ty left right in
+ (w, (eq_ty, left, right, neworder), [], [])
+ in
Inference.store_proof res newproof;
res
in
and newmenv = newmetas @ menv'
and newargs = args @ args' in
let eq' =
- (C.Implicit None, (eq_ty, left, right, neworder), newmenv, newargs)
+ let w = Utils.compute_equality_weight eq_ty left right in
+ (w, (eq_ty, left, right, neworder), newmenv, newargs)
and env = (metasenv, context, ugraph) in
let newm, eq' = Inference.fix_metas !maxmeta eq' in
newm, eq'
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 =
type equality =
- Cic.term * (* proof *)
+ int * (* weight *)
(Cic.term * (* type *)
Cic.term * (* left side *)
Cic.term * (* right side *)
returns a list of new clauses inferred with a left superposition step
the negative equation "target" and the positive equation "source"
*)
-val superposition_left: environment -> equality -> equality -> equality list
+(* val superposition_left: environment -> equality -> equality -> equality list *)
(**
superposition_right newmeta env target source
"newmeta" is the first free meta index, i.e. the first number above the
highest meta index: its updated value is also returned
*)
-val superposition_right:
- int -> environment -> equality -> equality -> int * equality list
+(* val superposition_right: *)
+(* int -> environment -> equality -> equality -> int * equality list *)
-val demodulation: int -> environment -> equality -> equality -> int * equality
+(* val demodulation: int -> environment -> equality -> equality -> int * equality *)
val meta_convertibility_eq: equality -> equality -> bool
val string_of_equality: ?env:environment -> equality -> string
-val subsumption: environment -> equality -> equality -> bool
+(* val subsumption: environment -> equality -> equality -> bool *)
val metas_of_term: Cic.term -> int list
;;
-let weight_of_equality (_, (ty, left, right, _), _, _) =
- let meta_number = ref 0 in
- let weight_of t =
- let weight, ml = weight_of_term t in
- meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml);
- weight
- in
- (weight_of ty) + (weight_of left) + (weight_of right), meta_number
-;;
-
-
module OrderedEquality = struct
type t = Inference.equality
match meta_convertibility_eq eq1 eq2 with
| true -> 0
| false ->
- let _, (ty, left, right, _), _, _ = eq1
- and _, (ty', left', right', _), _, _ = eq2 in
-(* let w1, m1 = weight_of_equality eq1 *)
-(* and w2, m2 = weight_of_equality eq2 in *)
- let weight_of t = fst (weight_of_term ~consider_metas:false t) in
- let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
- and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
+ let w1, (ty, left, right, _), _, a = eq1
+ and w2, (ty', left', right', _), _, a' = eq2 in
+(* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
+(* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
+(* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
match Pervasives.compare w1 w2 with
- | 0 -> Pervasives.compare eq1 eq2
-(* let res = Pervasives.compare m1 m2 in *)
-(* if res = 0 then Pervasives.compare eq1 eq2 else res *)
+ | 0 ->
+ let res = (List.length a) - (List.length a') in
+ if res <> 0 then res else (
+ try
+ let res = Pervasives.compare (List.hd a) (List.hd a') in
+ if res <> 0 then res else Pervasives.compare eq1 eq2
+ with _ -> Pervasives.compare eq1 eq2
+(* match a, a' with *)
+(* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
+(* let res = Pervasives.compare i j in *)
+(* if res <> 0 then res else Pervasives.compare eq1 eq2 *)
+(* | _, _ -> Pervasives.compare eq1 eq2 *)
+ )
| res -> res
end
;;
+let compute_equality_weight ty left right =
+ let weight_of t = fst (weight_of_term ~consider_metas:false t) in
+ (weight_of ty) + (weight_of left) + (weight_of right)
+;;
+
+
(* returns a "normalized" version of the polynomial weight wl (with type
* weight list), i.e. a list sorted ascending by meta number,
* from 0 to maxmeta. wl must be sorted descending by meta number. Example:
type pos = Left | Right
val string_of_pos: pos -> string
+
+val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int
projects / helm.git / commitdiff