From: Enrico Tassi Date: Wed, 3 Jun 2009 15:37:06 +0000 (+0000) Subject: functorial abstraction over term blobs X-Git-Tag: make_still_working~3928 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6c4056ea40b96039f24eeda9a1e1900c95bad7c8;p=helm.git functorial abstraction over term blobs --- diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 4ad2daaa3..1b047daac 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,3 +1,4 @@ +terms.cmi: pp.cmi: terms.cmi founif.cmi: terms.cmi index.cmi: terms.cmi @@ -7,8 +8,8 @@ terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: pp.cmi pp.cmx: pp.cmi -founif.cmo: founif.cmi -founif.cmx: founif.cmi +founif.cmo: terms.cmi subst.cmi founif.cmi +founif.cmx: terms.cmx subst.cmx founif.cmi index.cmo: terms.cmi index.cmi index.cmx: terms.cmx index.cmi orderings.cmo: terms.cmi orderings.cmi diff --git a/helm/software/components/ng_paramodulation/founif.ml b/helm/software/components/ng_paramodulation/founif.ml index 451524507..bc18aaf00 100644 --- a/helm/software/components/ng_paramodulation/founif.ml +++ b/helm/software/components/ng_paramodulation/founif.ml @@ -13,55 +13,60 @@ exception UnificationFailure of string Lazy.t;; -let unification vars locked_vars t1 t2 = - let lookup = Subst.lookup_subst in - let rec occurs_check subst what where = - match where with - | Terms.Var i when i = what -> true - | Terms.Var _ -> - let t = lookup where subst in - if t <> where then occurs_check subst what t else false - | Terms.Node l -> List.exists (occurs_check subst what) l - | _ -> false - in - let rec unif subst vars s t = - let s = match s with Terms.Var _ -> lookup s subst | _ -> s - and t = match t with Terms.Var _ -> lookup t subst | _ -> t - +module Founif (B : Terms.Blob) = struct + module Subst = Subst.Subst(B) + + let unification vars locked_vars t1 t2 = + let lookup = Subst.lookup_subst in + let rec occurs_check subst what where = + match where with + | Terms.Var i when i = what -> true + | Terms.Var _ -> + let t = lookup where subst in + if t <> where then occurs_check subst what t else false + | Terms.Node l -> List.exists (occurs_check subst what) l + | _ -> false in - match s, t with - | s, t when s = t -> subst, vars - | Terms.Var i, Terms.Var j - when (List.mem i locked_vars) &&(List.mem j locked_vars) -> - raise - (UnificationFailure (lazy "Inference.unification.unif")) - | Terms.Var i, Terms.Var j when (List.mem i locked_vars) -> - unif subst vars t s - | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) -> - unif subst vars t s - | Terms.Var i, t when occurs_check subst i t -> - raise - (UnificationFailure (lazy "Inference.unification.unif")) - | Terms.Var i, t when (List.mem i locked_vars) -> - raise - (UnificationFailure (lazy "Inference.unification.unif")) - | Terms.Var i, t -> - let subst = Subst.buildsubst i t subst in - subst, vars - | _, Terms.Var _ -> unif subst vars t s - | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt -> - raise (UnificationFailure (lazy "Inference.unification.unif")) - | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> ( - try - List.fold_left2 - (fun (subst', vars) s t -> unif subst' vars s t) - (subst, vars) tls tlt - with Invalid_argument _ -> + let rec unif subst vars s t = + let s = match s with Terms.Var _ -> lookup s subst | _ -> s + and t = match t with Terms.Var _ -> lookup t subst | _ -> t + + in + match s, t with + | s, t when s = t -> subst, vars + | Terms.Var i, Terms.Var j + when (List.mem i locked_vars) &&(List.mem j locked_vars) -> + raise + (UnificationFailure (lazy "Inference.unification.unif")) + | Terms.Var i, Terms.Var j when (List.mem i locked_vars) -> + unif subst vars t s + | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) -> + unif subst vars t s + | Terms.Var i, t when occurs_check subst i t -> + raise + (UnificationFailure (lazy "Inference.unification.unif")) + | Terms.Var i, t when (List.mem i locked_vars) -> + raise + (UnificationFailure (lazy "Inference.unification.unif")) + | Terms.Var i, t -> + let subst = Subst.buildsubst i t subst in + subst, vars + | _, Terms.Var _ -> unif subst vars t s + | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt -> + raise (UnificationFailure (lazy "Inference.unification.unif")) + | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> ( + try + List.fold_left2 + (fun (subst', vars) s t -> unif subst' vars s t) + (subst, vars) tls tlt + with Invalid_argument _ -> + raise (UnificationFailure (lazy "Inference.unification.unif")) + ) + | _, _ -> raise (UnificationFailure (lazy "Inference.unification.unif")) - ) - | _, _ -> - raise (UnificationFailure (lazy "Inference.unification.unif")) - in - let subst, vars = unif Subst.empty_subst vars t1 t2 in - let vars = Subst.filter subst vars in - subst, vars + in + let subst, vars = unif Subst.empty_subst vars t1 t2 in + let vars = Subst.filter subst vars in + subst, vars + +end diff --git a/helm/software/components/ng_paramodulation/founif.mli b/helm/software/components/ng_paramodulation/founif.mli index 2e8018313..55f15e656 100644 --- a/helm/software/components/ng_paramodulation/founif.mli +++ b/helm/software/components/ng_paramodulation/founif.mli @@ -13,12 +13,15 @@ exception UnificationFailure of string Lazy.t;; +module Founif (B : Terms.Blob) : + sig + val unification: Terms.varlist -> (* global varlist for both terms t1 and t2 *) Terms.varlist -> (* locked variables: if equal to FV(t2) we match t1 with t2*) - 'a Terms.foterm -> - 'a Terms.foterm -> - 'a Terms.substitution * Terms.varlist + B.t Terms.foterm -> + B.t Terms.foterm -> + B.t Terms.substitution * Terms.varlist (* val unification: @@ -30,3 +33,5 @@ val matching: 'a Terms.substitution * Terms.varlist *) + + end diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml index 123c51650..d07fba8a4 100644 --- a/helm/software/components/ng_paramodulation/index.ml +++ b/helm/software/components/ng_paramodulation/index.ml @@ -11,68 +11,70 @@ (* $Id$ *) -module type Comparable = - sig - type t - val is_eq : t -> t -> bool - end +module Index(B : Terms.Blob) = struct + module U = Terms.Utils(B) -module C : Comparable = - struct - type t = NCic.term - let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *) - end + module ClauseOT = + struct + type t = Terms.direction * B.t Terms.unit_clause + + let compare (d1,uc1) (d2,uc2) = + let c = Pervasives.compare d1 d2 in + if c <> 0 then c else U.compare_unit_clause uc1 uc2 + ;; + end - (* -module C : Comparable = - struct - type t = Cic.term - let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *) - end -*) + module ClauseSet : + Set.S with type elt = Terms.direction * B.t Terms.unit_clause + = Set.Make(ClauseOT) -open Discrimination_tree + open Discrimination_tree -module ClauseOT : Set.OrderedType - with type t = Terms.direction * C.t Terms.unit_clause = - struct - type t = Terms.direction * C.t Terms.unit_clause - let compare (d1,(id1,_,_,_)) (d2,(id2,_,_,_)) = - Pervasives.compare (d1,id1) (d2,id2) - end + module FotermIndexable : Indexable with + type constant_name = B.t and + type input = B.t Terms.foterm + = + struct -module ClauseSet = Set.Make(ClauseOT) + type input = B.t Terms.foterm + type constant_name = B.t -module FotermIndexable : Indexable -with type input = C.t Terms.foterm and - type constant_name = C.t = struct + let path_string_of = + let rec aux arity = function + | Terms.Leaf a -> [Constant (a, arity)] + | Terms.Var i -> assert (arity = 0); [Variable] + | Terms.Node (Terms.Var _::_) -> assert false + | Terms.Node ([] | [ _ ] ) -> assert false + | Terms.Node (Terms.Node _::_) -> assert false + | Terms.Node (hd::tl) -> + aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) + in + aux 0 + ;; -type input = C.t Terms.foterm -type constant_name = C.t + let compare e1 e2 = + match e1,e2 with + | Constant (a1,ar1), Constant (a2,ar2) -> + let c = B.compare a1 a2 in + if c <> 0 then c else Pervasives.compare ar1 ar2 + | Variable, Variable -> 0 + | Constant _, Variable -> ~-1 + | Variable, Constant _ -> 1 + | Proposition, _ | _, Proposition + | Datatype, _ | _, Datatype + | Dead, _ | _, Dead + | Bound _, _ | _, Bound _ -> assert false + ;; -let path_string_of = - let rec aux arity = function - | Terms.Leaf a -> [Constant (a, arity)] - | Terms.Var i -> assert (arity = 0); [Variable] - | Terms.Node (Terms.Var _::_) -> assert false - | Terms.Node ([] | [ _ ] ) -> assert false - | Terms.Node (Terms.Node _::_) -> assert false - | Terms.Node (hd::tl) -> - aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) - in - aux 0 -;; + let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;; -let compare e1 e2 = - match e1,e2 with - | Constant (a1,ar1), Constant (a2,ar2) -> - if C.is_eq a1 a2 then Pervasives.compare ar1 ar2 - else Pervasives.compare e1 e2 (* TODO: OPTIMIZE *) - | _ -> Pervasives.compare e1 e2 -;; + end -let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;; + module DT : DiscriminationTree with + type constant_name = B.t and + type input = B.t Terms.foterm and + type data = ClauseSet.elt and + type dataset = ClauseSet.t + = Make(FotermIndexable)(ClauseSet) end - -module DiscriminationTree = Make(FotermIndexable)(ClauseSet) diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli index fdecba91f..3f86cc1e0 100644 --- a/helm/software/components/ng_paramodulation/index.mli +++ b/helm/software/components/ng_paramodulation/index.mli @@ -11,21 +11,19 @@ (* $Id$ *) -module type Comparable = +module Index (B : Terms.Blob) : sig - type t - val is_eq : t -> t -> bool - end - -module C : Comparable + module ClauseSet : Set.S with + type elt = Terms.direction * B.t Terms.unit_clause -module FotermIndexable : Discrimination_tree.Indexable -with type constant_name = C.t and - type input = C.t Terms.foterm + module FotermIndexable : Discrimination_tree.Indexable with + type constant_name = B.t and + type input = B.t Terms.foterm -module ClauseSet : Set.S with type elt = Terms.direction * C.t Terms.unit_clause + module DT : Discrimination_tree.DiscriminationTree with + type constant_name = B.t and + type input = B.t Terms.foterm and + type data = ClauseSet.elt and + type dataset = ClauseSet.t -module DiscriminationTree : Discrimination_tree.DiscriminationTree -with type constant_name = C.t -and type input = C.t Terms.foterm -and type data = ClauseSet.elt and type dataset = ClauseSet.t + end diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 4e84c49b6..dde09e81f 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -11,232 +11,234 @@ (* $Id$ *) -(* (weight of constants, [(meta, weight_of_meta)]) *) -type weight = int * (int * int) list;; - -let string_of_weight (cw, mw) = - let s = - String.concat ", " - (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw) - in - Printf.sprintf "[%d; %s]" cw s -;; - -let weight_of_term term = - let vars_dict = Hashtbl.create 5 in - let rec aux = function - | Terms.Var i -> - (try - let oldw = Hashtbl.find vars_dict i in - Hashtbl.replace vars_dict i (oldw+1) - with Not_found -> - Hashtbl.add vars_dict i 1); - 0 - | Terms.Leaf _ -> 1 - | Terms.Node l -> List.fold_left (+) 0 (List.map aux l) - in - let w = aux term in - let l = - Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict [] - in - let compare w1 w2 = - match w1, w2 with - | (m1, _), (m2, _) -> m2 - m1 - in - (w, List.sort compare l) (* from the biggest meta to the smallest (0) *) -;; - -let compute_clause_weight = assert false (* - let factor = 2 in - match o with - | Terms.Lt -> - let w, m = (weight_of_term - ~consider_metas:true ~count_metas_occurrences:false right) in - w + (factor * (List.length m)) ; - | 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)) ; - | 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 - ~consider_metas:true ~count_metas_occurrences:false left) in - w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2)) -*) -;; - -(* 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: - * normalize_weight 5 (3, [(3, 2); (1, 1)]) -> - * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *) -let normalize_weight maxmeta (cw, wl) = - let rec aux = function - | 0 -> [] - | m -> (m, 0)::(aux (m-1)) - in - let tmpl = aux maxmeta in - let wl = - List.sort - (fun (m, _) (n, _) -> Pervasives.compare m n) - (List.fold_left - (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl) - in - (cw, wl) -;; - - -let normalize_weights (cw1, wl1) (cw2, wl2) = - let rec aux wl1 wl2 = - match wl1, wl2 with - | [], [] -> [], [] - | (m, w)::tl1, (n, w')::tl2 when m = n -> - let res1, res2 = aux tl1 tl2 in - (m, w)::res1, (n, w')::res2 - | (m, w)::tl1, ((n, w')::_ as wl2) when m < n -> - let res1, res2 = aux tl1 wl2 in - (m, w)::res1, (m, 0)::res2 - | ((m, w)::_ as wl1), (n, w')::tl2 when m > n -> - let res1, res2 = aux wl1 tl2 in - (n, 0)::res1, (n, w')::res2 - | [], (n, w)::tl2 -> - let res1, res2 = aux [] tl2 in - (n, 0)::res1, (n, w)::res2 - | (m, w)::tl1, [] -> - let res1, res2 = aux tl1 [] in - (m, w)::res1, (m, 0)::res2 - | _, _ -> assert false - in - let cmp (m, _) (n, _) = compare m n in - let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in - (cw1, wl1), (cw2, wl2) -;; - -(* Riazanov: 3.1.5 pag 38 *) -(* TODO: optimize early detection of Terms.Incomparable case *) -let compare_weights (h1, w1) (h2, w2) = - let res, diffs = - try - List.fold_left2 - (fun ((lt, eq, gt), diffs) w1 w2 -> - match w1, w2 with - | (meta1, w1), (meta2, w2) when meta1 = meta2 -> - let diffs = (w1 - w2) + diffs in - let r = compare w1 w2 in - if r < 0 then (lt+1, eq, gt), diffs - else if r = 0 then (lt, eq+1, gt), diffs - else (lt, eq, gt+1), diffs - | _ -> assert false) - ((0, 0, 0), 0) w1 w2 - with Invalid_argument _ -> assert false - in - let hdiff = h1 - h2 in - match res with - | (0, _, 0) -> - if hdiff < 0 then Terms.Lt - else if hdiff > 0 then Terms.Gt - else Terms.Eq - | (m, _, 0) -> - if hdiff <= 0 then Terms.Lt - else if (- diffs) >= hdiff then Terms.Le else Terms.Incomparable - | (0, _, m) -> - 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 t1 t2 = - match t1, t2 with - | Terms.Var _, _ - | _, Terms.Var _ -> Terms.Incomparable - - | 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 - - | Terms.Leaf _, Terms.Node _ -> Terms.Lt - | Terms.Node _, Terms.Leaf _ -> Terms.Gt - - | Terms.Node l1, Terms.Node l2 -> - let rec cmp t1 t2 = - match t1, t2 with - | [], [] -> Terms.Eq - | _, [] -> Terms.Gt - | [], _ -> Terms.Lt - | hd1::tl1, hd2::tl2 -> - let o = aux_ordering hd1 hd2 in - if o = Terms.Eq then cmp tl1 tl2 - else o - in - cmp l1 l2 -;; - -let nonrec_kbo t1 t2 = - let w1 = weight_of_term t1 in - let w2 = weight_of_term t2 in - 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 = +module Orderings (B : Terms.Blob) = struct + + type weight = int * (int * int) list;; + + let string_of_weight (cw, mw) = + let s = + String.concat ", " + (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw) + in + Printf.sprintf "[%d; %s]" cw s + ;; + + let weight_of_term term = + let vars_dict = Hashtbl.create 5 in + let rec aux = function + | Terms.Var i -> + (try + let oldw = Hashtbl.find vars_dict i in + Hashtbl.replace vars_dict i (oldw+1) + with Not_found -> + Hashtbl.add vars_dict i 1); + 0 + | Terms.Leaf _ -> 1 + | Terms.Node l -> List.fold_left (+) 0 (List.map aux l) + in + let w = aux term in + let l = + Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict [] + in + let compare w1 w2 = + match w1, w2 with + | (m1, _), (m2, _) -> m2 - m1 + in + (w, List.sort compare l) (* from the biggest meta to the smallest (0) *) + ;; + + let compute_clause_weight = assert false (* + let factor = 2 in + match o with + | Terms.Lt -> + let w, m = (weight_of_term + ~consider_metas:true ~count_metas_occurrences:false right) in + w + (factor * (List.length m)) ; + | 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)) ; + | 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 + ~consider_metas:true ~count_metas_occurrences:false left) in + w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2)) + *) + ;; + + (* 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: + * normalize_weight 5 (3, [(3, 2); (1, 1)]) -> + * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *) + let normalize_weight maxmeta (cw, wl) = + let rec aux = function + | 0 -> [] + | m -> (m, 0)::(aux (m-1)) + in + let tmpl = aux maxmeta in + let wl = + List.sort + (fun (m, _) (n, _) -> Pervasives.compare m n) + (List.fold_left + (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl) + in + (cw, wl) + ;; + + + let normalize_weights (cw1, wl1) (cw2, wl2) = + let rec aux wl1 wl2 = + match wl1, wl2 with + | [], [] -> [], [] + | (m, w)::tl1, (n, w')::tl2 when m = n -> + let res1, res2 = aux tl1 tl2 in + (m, w)::res1, (n, w')::res2 + | (m, w)::tl1, ((n, w')::_ as wl2) when m < n -> + let res1, res2 = aux tl1 wl2 in + (m, w)::res1, (m, 0)::res2 + | ((m, w)::_ as wl1), (n, w')::tl2 when m > n -> + let res1, res2 = aux wl1 tl2 in + (n, 0)::res1, (n, w')::res2 + | [], (n, w)::tl2 -> + let res1, res2 = aux [] tl2 in + (n, 0)::res1, (n, w)::res2 + | (m, w)::tl1, [] -> + let res1, res2 = aux tl1 [] in + (m, w)::res1, (m, 0)::res2 + | _, _ -> assert false + in + let cmp (m, _) (n, _) = compare m n in + let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in + (cw1, wl1), (cw2, wl2) + ;; + + (* Riazanov: 3.1.5 pag 38 *) + (* TODO: optimize early detection of Terms.Incomparable case *) + let compare_weights (h1, w1) (h2, w2) = + let res, diffs = + try + List.fold_left2 + (fun ((lt, eq, gt), diffs) w1 w2 -> + match w1, w2 with + | (meta1, w1), (meta2, w2) when meta1 = meta2 -> + let diffs = (w1 - w2) + diffs in + let r = compare w1 w2 in + if r < 0 then (lt+1, eq, gt), diffs + else if r = 0 then (lt, eq+1, gt), diffs + else (lt, eq, gt+1), diffs + | _ -> assert false) + ((0, 0, 0), 0) w1 w2 + with Invalid_argument _ -> assert false + in + let hdiff = h1 - h2 in + match res with + | (0, _, 0) -> + if hdiff < 0 then Terms.Lt + else if hdiff > 0 then Terms.Gt + else Terms.Eq + | (m, _, 0) -> + if hdiff <= 0 then Terms.Lt + else if (- diffs) >= hdiff then Terms.Le else Terms.Incomparable + | (0, _, m) -> + 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 t1 t2 = match t1, t2 with - | [], [] -> Terms.Eq - | _, [] -> Terms.Gt - | [], _ -> Terms.Lt - | hd1::tl1, hd2::tl2 -> - let o = - kbo hd1 hd2 + | Terms.Var _, _ + | _, Terms.Var _ -> Terms.Incomparable + + | 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 + + | Terms.Leaf _, Terms.Node _ -> Terms.Lt + | Terms.Node _, Terms.Leaf _ -> Terms.Gt + + | Terms.Node l1, Terms.Node l2 -> + let rec cmp t1 t2 = + match t1, t2 with + | [], [] -> Terms.Eq + | _, [] -> Terms.Gt + | [], _ -> Terms.Lt + | hd1::tl1, hd2::tl2 -> + let o = aux_ordering hd1 hd2 in + if o = Terms.Eq then cmp tl1 tl2 + else o in - if o = Terms.Eq then cmp tl1 tl2 - else o - in - let w1, w2 = normalize_weights w1 w2 in - let comparison = compare_weights w1 w2 in - match comparison with - | Terms.Le -> - let r = aux t1 t2 in - 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 = Terms.Lt then Terms.Lt else Terms.Incomparable - | _, _ -> Terms.Incomparable - ) else Terms.Incomparable - | Terms.Ge -> - let r = aux t1 t2 in - 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 = Terms.Gt then Terms.Gt else Terms.Incomparable - | _, _ -> Terms.Incomparable - ) else Terms.Incomparable - | Terms.Eq -> - let r = aux t1 t2 in - if r = Terms.Eq then ( - match t1, t2 with - | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> - cmp tl1 tl2 - | _, _ -> Terms.Incomparable - ) else r - | res -> res -;; -*) - -let compare_terms = nonrec_kbo;; - + cmp l1 l2 + ;; + + let nonrec_kbo t1 t2 = + let w1 = weight_of_term t1 in + let w2 = weight_of_term t2 in + 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 + | [], [] -> Terms.Eq + | _, [] -> Terms.Gt + | [], _ -> Terms.Lt + | hd1::tl1, hd2::tl2 -> + let o = + kbo hd1 hd2 + in + if o = Terms.Eq then cmp tl1 tl2 + else o + in + let w1, w2 = normalize_weights w1 w2 in + let comparison = compare_weights w1 w2 in + match comparison with + | Terms.Le -> + let r = aux t1 t2 in + 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 = Terms.Lt then Terms.Lt else Terms.Incomparable + | _, _ -> Terms.Incomparable + ) else Terms.Incomparable + | Terms.Ge -> + let r = aux t1 t2 in + 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 = Terms.Gt then Terms.Gt else Terms.Incomparable + | _, _ -> Terms.Incomparable + ) else Terms.Incomparable + | Terms.Eq -> + let r = aux t1 t2 in + if r = Terms.Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + cmp tl1 tl2 + | _, _ -> Terms.Incomparable + ) else r + | res -> res + ;; + *) + + let compare_terms = nonrec_kbo;; + +end diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli index 59cfde124..f2f6a1678 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -11,4 +11,7 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val compare_terms : 'a Terms.foterm -> 'a Terms.foterm -> Terms.comparison +module Orderings (B : Terms.Blob) : + sig + val compare_terms : B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison + end diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index aff9224e0..d663e8155 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -11,9 +11,11 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -let pp_foterm = assert false -let pp_proof = assert false -let pp_substitution = assert false -let pp_unit_clause = assert false - +module Pp (B : Terms.Blob) = struct + let pp_foterm = assert false + let pp_proof = assert false + let pp_substitution = assert false + let pp_unit_clause = assert false + +end diff --git a/helm/software/components/ng_paramodulation/pp.mli b/helm/software/components/ng_paramodulation/pp.mli index 46c588676..dbfca2073 100644 --- a/helm/software/components/ng_paramodulation/pp.mli +++ b/helm/software/components/ng_paramodulation/pp.mli @@ -11,9 +11,12 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val pp_foterm: ('a -> string) -> 'a Terms.foterm -> string -val pp_proof: ('a -> string) -> 'a Terms.bag -> 'a Terms.proof -> string -val pp_substitution: ('a -> string) -> 'a Terms.substitution -> string -val pp_unit_clause: ('a -> string) -> 'a Terms.unit_clause -> string +module Pp (B : Terms.Blob) : + sig + val pp_foterm: B.t Terms.foterm -> string + val pp_proof: B.t Terms.bag -> B.t Terms.proof -> string + val pp_substitution: B.t Terms.substitution -> string + val pp_unit_clause: B.t Terms.unit_clause -> string + end diff --git a/helm/software/components/ng_paramodulation/subst.ml b/helm/software/components/ng_paramodulation/subst.ml index 662a9f0d7..b8cadf48c 100644 --- a/helm/software/components/ng_paramodulation/subst.ml +++ b/helm/software/components/ng_paramodulation/subst.ml @@ -9,26 +9,30 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -let empty_subst = [];; - -let buildsubst n t tail = (n,t) :: tail ;; - -let rec lookup_subst var subst = - match var with - | Terms.Var i -> - (try - lookup_subst (List.assoc i subst) subst - with - Not_found -> var) - | _ -> var -;; - -let is_in_subst i subst = List.mem_assoc i subst;; - -(* filter out from metasenv the variables in substs *) -let filter subst varlist = - List.filter - (fun m -> - not (is_in_subst m subst)) - varlist -;; +module Subst (B : Terms.Blob) = struct + + let empty_subst = [];; + + let buildsubst n t tail = (n,t) :: tail ;; + + let rec lookup_subst var subst = + match var with + | Terms.Var i -> + (try + lookup_subst (List.assoc i subst) subst + with + Not_found -> var) + | _ -> var + ;; + + let is_in_subst i subst = List.mem_assoc i subst;; + + (* filter out from metasenv the variables in substs *) + let filter subst varlist = + List.filter + (fun m -> + not (is_in_subst m subst)) + varlist + ;; + +end diff --git a/helm/software/components/ng_paramodulation/subst.mli b/helm/software/components/ng_paramodulation/subst.mli index 73f5115dd..8747a478f 100644 --- a/helm/software/components/ng_paramodulation/subst.mli +++ b/helm/software/components/ng_paramodulation/subst.mli @@ -11,8 +11,13 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val empty_subst : 'a Terms.substitution -val buildsubst : - int -> 'a Terms.foterm -> 'a Terms.substitution -> 'a Terms.substitution -val lookup_subst : 'a Terms.foterm -> 'a Terms.substitution -> 'a Terms.foterm -val filter : 'a Terms.substitution -> Terms.varlist -> Terms.varlist +module Subst (B : Terms.Blob) : + sig + val empty_subst : B.t Terms.substitution + val buildsubst : + int -> B.t Terms.foterm -> B.t Terms.substitution -> + B.t Terms.substitution + val lookup_subst : + B.t Terms.foterm -> B.t Terms.substitution -> B.t Terms.foterm + val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist + end diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 91ca56271..8fad7187b 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -57,3 +57,70 @@ module M : Map.S with type key = int = Map.Make(OT) type 'a bag = 'a unit_clause M.t + +module type Blob = + sig + type t + val eq : t -> t -> bool + val compare : t -> t -> int + val pp : t -> string + end + +module Utils (B : Blob) = struct + let rec eq_foterm x y = + x == y || + match x, y with + | Leaf t1, Leaf t2 -> B.eq t1 t2 + | Var i, Var j -> i = j + | Node l1, Node l2 -> List.for_all2 eq_foterm l1 l2 + | _ -> false + ;; + + let rec lexicograph f l1 l2 = + match l1, l2 with + | [], [] -> 0 + | x::xs, y::ys -> + let c = f x y in + if c <> 0 then c else lexicograph f xs ys + | [],_ -> ~-1 + | _,[] -> 1 + ;; + + let rec compare_foterm x y = + match x, y with + | Leaf t1, Leaf t2 -> B.compare t1 t2 + | Var i, Var j -> i - j + | Node l1, Node l2 -> lexicograph compare_foterm l1 l2 + | Leaf _, ( Node _ | Var _ ) -> ~-1 + | Node _, Leaf _ -> 1 + | Node _, Var _ -> ~-1 + | Var _, _ -> 1 + ;; + + let eq_literal l1 l2 = + match l1, l2 with + | Predicate p1, Predicate p2 -> eq_foterm p1 p2 + | Equation (l1,r1,ty1,o1), Equation (l2,r2,ty2,o2) -> + o1 = o2 && eq_foterm l1 l2 && eq_foterm r1 r2 && eq_foterm ty1 ty2 + | _ -> false + ;; + + let compare_literal l1 l2 = + match l1, l2 with + | Predicate p1, Predicate p2 -> compare_foterm p1 p2 + | Equation (l1,r1,ty1,o1), Equation (l2,r2,ty2,o2) -> + let c = Pervasives.compare o1 o2 in + if c <> 0 then c else + let c = compare_foterm l1 l2 in + if c <> 0 then c else + let c = compare_foterm r1 r2 in + if c <> 0 then c else + compare_foterm ty1 ty2 + | Predicate _, Equation _ -> ~-1 + | Equation _, Predicate _ -> 1 + ;; + + let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2 + let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2 + +end diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index c49eaff83..3013ed7d0 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -50,3 +50,19 @@ module M : Map.S with type key = int type 'a bag = 'a unit_clause M.t +module type Blob = + sig + type t + val eq : t -> t -> bool + val compare : t -> t -> int + val pp : t -> string + end + +module Utils (B : Blob) : + sig + val eq_literal : B.t literal -> B.t literal -> bool + val compare_literal : B.t literal -> B.t literal -> int + + val eq_unit_clause : B.t unit_clause -> B.t unit_clause -> bool + val compare_unit_clause : B.t unit_clause -> B.t unit_clause -> int + end