let compute_clause_weight = assert false (*
let factor = 2 in
match o with
- | Lt ->
+ | Terms.Lt ->
let w, m = (weight_of_term
~consider_metas:true ~count_metas_occurrences:false right) in
w + (factor * (List.length m)) ;
- | Le -> assert false
- | Gt ->
+ | Terms.Le -> assert false
+ | Terms.Gt ->
let w, m = (weight_of_term
~consider_metas:true ~count_metas_occurrences:false left) in
w + (factor * (List.length m)) ;
- | Ge -> assert false
- | Eq
- | Incomparable ->
+ | Terms.Ge -> assert false
+ | Terms.Eq
+ | Terms.Incomparable ->
let w1, m1 = (weight_of_term
~consider_metas:true ~count_metas_occurrences:false right) in
let w2, m2 = (weight_of_term
;;
(* Riazanov: 3.1.5 pag 38 *)
-let compare_weights ((h1, w1) as weight1) ((h2, w2) as weight2)=
+(* TODO: optimize early detection of Terms.Incomparable case *)
+let compare_weights (h1, w1) (h2, w2) =
let res, diffs =
try
List.fold_left2
let hdiff = h1 - h2 in
match res with
| (0, _, 0) ->
- if hdiff < 0 then Lt
- else if hdiff > 0 then Gt
- else Eq
+ if hdiff < 0 then Terms.Lt
+ else if hdiff > 0 then Terms.Gt
+ else Terms.Eq
| (m, _, 0) ->
- if hdiff <= 0 then Lt
- else if (- diffs) >= hdiff then Le else Incomparable
+ if hdiff <= 0 then Terms.Lt
+ else if (- diffs) >= hdiff then Terms.Le else Terms.Incomparable
| (0, _, m) ->
- if hdiff >= 0 then Gt
- else if diffs >= (- hdiff) then Ge else Incomparable
- | (m, _, n) when m > 0 && n > 0 ->
- Incomparable
+ if hdiff >= 0 then Terms.Gt
+ else if diffs >= (- hdiff) then Terms.Ge else Terms.Incomparable
+ | (m, _, n) when m > 0 && n > 0 -> Terms.Incomparable
| _ -> assert false
;;
-let rec aux_ordering ?(recursion=true) t1 t2 =
- let module C = Cic in
- let compare_uris u1 u2 =
- let res =
- compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) in
- if res < 0 then Lt
- else if res = 0 then Eq
- else Gt
- in
+let rec aux_ordering t1 t2 =
match t1, t2 with
- | C.Meta _, _
- | _, C.Meta _ -> Incomparable
-
- | t1, t2 when t1 = t2 -> Eq
-
- | C.Rel n, C.Rel m -> if n > m then Lt else Gt
- | C.Rel _, _ -> Lt
- | _, C.Rel _ -> Gt
+ | Terms.Var _, _
+ | _, Terms.Var _ -> Terms.Incomparable
- | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2
- | C.Const _, _ -> Lt
- | _, C.Const _ -> Gt
+ | Terms.Leaf a1, Terms.Leaf a2 ->
+ let cmp = Pervasives.compare a1 a2 in
+ if cmp = 0 then Terms.Eq else if cmp < 0 then Terms.Lt else Terms.Gt
- | C.MutInd (u1, tno1, _), C.MutInd (u2, tno2, _) ->
- let res = compare_uris u1 u2 in
- if res <> Eq then res
- else
- let res = compare tno1 tno2 in
- if res = 0 then Eq else if res < 0 then Lt else Gt
- | C.MutInd _, _ -> Lt
- | _, C.MutInd _ -> Gt
+ | Terms.Leaf _, Terms.Node _ -> Terms.Lt
+ | Terms.Node _, Terms.Leaf _ -> Terms.Gt
- | C.MutConstruct (u1, tno1, cno1, _), C.MutConstruct (u2, tno2, cno2, _) ->
- let res = compare_uris u1 u2 in
- if res <> Eq then res
- else
- let res = compare (tno1,cno1) (tno2,cno2) in
- if res = 0 then Eq else if res < 0 then Lt else Gt
- | C.MutConstruct _, _ -> Lt
- | _, C.MutConstruct _ -> Gt
-
- | C.Appl l1, C.Appl l2 when recursion ->
+ | Terms.Node l1, Terms.Node l2 ->
let rec cmp t1 t2 =
match t1, t2 with
- | [], [] -> Eq
- | _, [] -> Gt
- | [], _ -> Lt
+ | [], [] -> Terms.Eq
+ | _, [] -> Terms.Gt
+ | [], _ -> Terms.Lt
| hd1::tl1, hd2::tl2 ->
let o = aux_ordering hd1 hd2 in
- if o = Eq then cmp tl1 tl2
+ if o = Terms.Eq then cmp tl1 tl2
else o
in
cmp l1 l2
- | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion ->
- aux_ordering h1 h2
-
- | t1, t2 ->
- debug_print
- (lazy
- (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
- (CicPp.ppterm t1) (CicPp.ppterm t2)));
- Incomparable
;;
let nonrec_kbo t1 t2 =
let w1 = weight_of_term t1 in
let w2 = weight_of_term t2 in
- match compare_weights ~normalize:true w1 w2 with
- | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
- | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
- | Eq -> aux_ordering t1 t2
+ let w1, w2 = normalize_weights w1 w2 in
+ match compare_weights w1 w2 with
+ | Terms.Le -> if aux_ordering t1 t2 = Terms.Lt then Terms.Lt else Terms.Incomparable
+ | Terms.Ge -> if aux_ordering t1 t2 = Terms.Gt then Terms.Gt else Terms.Incomparable
+ | Terms.Eq -> aux_ordering t1 t2
| res -> res
;;
+(*
let rec kbo t1 t2 =
let aux = aux_ordering ~recursion:false in
let w1 = weight_of_term t1
and w2 = weight_of_term t2 in
let rec cmp t1 t2 =
match t1, t2 with
- | [], [] -> Eq
- | _, [] -> Gt
- | [], _ -> Lt
+ | [], [] -> Terms.Eq
+ | _, [] -> Terms.Gt
+ | [], _ -> Terms.Lt
| hd1::tl1, hd2::tl2 ->
let o =
kbo hd1 hd2
in
- if o = Eq then cmp tl1 tl2
+ if o = Terms.Eq then cmp tl1 tl2
else o
in
- let comparison = compare_weights ~normalize:true w1 w2 in
+ let w1, w2 = normalize_weights w1 w2 in
+ let comparison = compare_weights w1 w2 in
match comparison with
- | Le ->
+ | Terms.Le ->
let r = aux t1 t2 in
- if r = Lt then Lt
- else if r = Eq then (
+ if r = Terms.Lt then Terms.Lt
+ else if r = Terms.Eq then (
match t1, t2 with
| Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- if cmp tl1 tl2 = Lt then Lt else Incomparable
- | _, _ -> Incomparable
- ) else Incomparable
- | Ge ->
+ if cmp tl1 tl2 = Terms.Lt then Terms.Lt else Terms.Incomparable
+ | _, _ -> Terms.Incomparable
+ ) else Terms.Incomparable
+ | Terms.Ge ->
let r = aux t1 t2 in
- if r = Gt then Gt
- else if r = Eq then (
+ if r = Terms.Gt then Terms.Gt
+ else if r = Terms.Eq then (
match t1, t2 with
| Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- if cmp tl1 tl2 = Gt then Gt else Incomparable
- | _, _ -> Incomparable
- ) else Incomparable
- | Eq ->
+ if cmp tl1 tl2 = Terms.Gt then Terms.Gt else Terms.Incomparable
+ | _, _ -> Terms.Incomparable
+ ) else Terms.Incomparable
+ | Terms.Eq ->
let r = aux t1 t2 in
- if r = Eq then (
+ if r = Terms.Eq then (
match t1, t2 with
| Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
cmp tl1 tl2
- | _, _ -> Incomparable
+ | _, _ -> Terms.Incomparable
) else r
| res -> res
;;
+*)
let compare_terms = nonrec_kbo;;
projects / helm.git / commitdiff