From: Enrico Tassi Date: Mon, 1 Jun 2009 13:49:20 +0000 (+0000) Subject: added a snapshot of comparison X-Git-Tag: make_still_working~3934 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4aaab68e38ccafb352cc2b656e3ec3cf1ef33cab;p=helm.git added a snapshot of comparison --- diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index db250f996..75490d3ba 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -2,6 +2,7 @@ terms.cmi: pp.cmi: terms.cmi founif.cmi: terms.cmi index.cmi: terms.cmi +orderings.cmi: terms.cmi terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: pp.cmi @@ -10,3 +11,5 @@ founif.cmo: founif.cmi founif.cmx: founif.cmi index.cmo: terms.cmi index.cmi index.cmx: terms.cmx index.cmi +orderings.cmo: terms.cmi orderings.cmi +orderings.cmx: terms.cmx orderings.cmi diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt new file mode 100644 index 000000000..75490d3ba --- /dev/null +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -0,0 +1,15 @@ +terms.cmi: +pp.cmi: terms.cmi +founif.cmi: terms.cmi +index.cmi: terms.cmi +orderings.cmi: terms.cmi +terms.cmo: terms.cmi +terms.cmx: terms.cmi +pp.cmo: pp.cmi +pp.cmx: pp.cmi +founif.cmo: founif.cmi +founif.cmx: founif.cmi +index.cmo: terms.cmi index.cmi +index.cmx: terms.cmx index.cmi +orderings.cmo: terms.cmi orderings.cmi +orderings.cmx: terms.cmx orderings.cmi diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index f15454c62..4e84c49b6 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -49,18 +49,18 @@ let weight_of_term term = 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 @@ -117,7 +117,8 @@ let normalize_weights (cw1, wl1) (cw2, wl2) = ;; (* 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 @@ -136,141 +137,106 @@ let compare_weights ((h1, w1) as weight1) ((h2, w2) as weight2)= 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;; diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli index 9d0f47d22..59cfde124 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -11,3 +11,4 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) +val compare_terms : 'a Terms.foterm -> 'a Terms.foterm -> Terms.comparison