--- /dev/null
+requires="helm-cic helm-ng_kernel"
+version="0.0.1"
+archive(byte)="ng_paramodulation.cma"
+archive(native)="ng_paramodulation.cmxa"
+linkopts=""
--- /dev/null
+terms.cmi:
+pp.cmi: terms.cmi
+founif.cmi: terms.cmi
+index.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
--- /dev/null
+PACKAGE = ng_paramodulation
+
+INTERFACE_FILES = \
+ terms.mli pp.mli founif.mli index.mli orderings.mli
+
+IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
+
+all:
+
+include ../../Makefile.defs
+include ../Makefile.common
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+let unification = assert false
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+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
+
+(*
+val unification:
+ Terms.varlist -> 'a Terms.foterm -> 'a Terms.foterm ->
+ 'a Terms.substitution * Terms.varlist
+
+val matching:
+ Terms.varlist -> Terms.varlist -> 'a Terms.foterm -> 'a Terms.foterm ->
+ 'a Terms.substitution * Terms.varlist
+
+*)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+module type Comparable =
+ sig
+ type t
+ val is_eq : t -> t -> bool
+ end
+
+module C : Comparable =
+ struct
+ type t = NCic.term
+ let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
+ end
+
+ (*
+module C : Comparable =
+ struct
+ type t = Cic.term
+ let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
+ end
+*)
+
+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 ClauseSet = Set.Make(ClauseOT)
+
+module FotermIndexable : Indexable
+with type input = C.t Terms.foterm and
+ type constant_name = C.t = struct
+
+type input = C.t Terms.foterm
+type constant_name = C.t
+
+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 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
+;;
+
+let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;
+
+end
+
+module DiscriminationTree = Make(FotermIndexable)(ClauseSet)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+module type Comparable =
+ sig
+ type t
+ val is_eq : t -> t -> bool
+ end
+
+module C : Comparable
+
+module FotermIndexable : Discrimination_tree.Indexable
+with type constant_name = C.t and
+ type input = C.t Terms.foterm
+
+module ClauseSet : Set.S with type elt = Terms.direction * C.t Terms.unit_clause
+
+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
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $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
+ | 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 ->
+ 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 ->
+ 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 *)
+let compare_weights ((h1, w1) as weight1) ((h2, w2) as weight2)=
+ 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 Lt
+ else if hdiff > 0 then Gt
+ else Eq
+ | (m, _, 0) ->
+ if hdiff <= 0 then Lt
+ else if (- diffs) >= hdiff then Le else Incomparable
+ | (0, _, m) ->
+ if hdiff >= 0 then Gt
+ else if diffs >= (- hdiff) then Ge else Incomparable
+ | (m, _, n) when m > 0 && n > 0 ->
+ 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
+ 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
+
+ | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2
+ | C.Const _, _ -> Lt
+ | _, C.Const _ -> 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
+
+ | 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 ->
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> Eq
+ | _, [] -> Gt
+ | [], _ -> Lt
+ | hd1::tl1, hd2::tl2 ->
+ let o = aux_ordering hd1 hd2 in
+ if o = 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
+ | 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
+ | hd1::tl1, hd2::tl2 ->
+ let o =
+ kbo hd1 hd2
+ in
+ if o = Eq then cmp tl1 tl2
+ else o
+ in
+ let comparison = compare_weights ~normalize:true w1 w2 in
+ match comparison with
+ | Le ->
+ let r = aux t1 t2 in
+ if r = Lt then Lt
+ else if r = 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 ->
+ let r = aux t1 t2 in
+ if r = Gt then Gt
+ else if r = 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 ->
+ let r = aux t1 t2 in
+ if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ cmp tl1 tl2
+ | _, _ -> Incomparable
+ ) else r
+ | res -> res
+;;
+
+let compare_terms = nonrec_kbo;;
+
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $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
+
+
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $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
+
+
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+type 'a foterm =
+ | Leaf of 'a
+ | Var of int
+ | Node of ('a foterm) list
+
+type 'a substitution = (int * 'a foterm) list
+
+type comparison = Lt | Le | Eq | Ge | Gt | Incomparable
+
+type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+type direction = Left2Right | Right2Left | Nodir
+type position = int list
+
+type 'a proof =
+ | Exact of 'a
+ | Step of rule * int * int * direction * position * 'a substitution
+ (* rule, eq1, eq2, direction of eq2, position, substitution *)
+
+type 'a literal =
+ | Equation of 'a foterm (* lhs *)
+ * 'a foterm (* rhs *)
+ * 'a foterm (* type *)
+ * comparison (* orientation *)
+ | Predicate of 'a foterm
+
+type varlist = int list
+
+type 'a unit_clause =
+ int (* ID *)
+ * 'a literal
+ * varlist (* variable list *)
+ * 'a proof (* proof *)
+
+type 'a passive_clause = int * 'a unit_clause (* weight * equation *)
+
+
+module OT =
+ struct
+ type t = int
+ let compare = Pervasives.compare
+ end
+
+module M : Map.S with type key = int
+ = Map.Make(OT)
+
+type 'a bag = 'a unit_clause M.t
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+type 'a foterm =
+ | Leaf of 'a
+ | Var of int
+ | Node of ('a foterm) list
+
+type 'a substitution = (int * 'a foterm) list
+
+type comparison = Lt | Le | Eq | Ge | Gt | Incomparable
+
+type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+type direction = Left2Right | Right2Left | Nodir
+type position = int list
+
+type 'a proof =
+ | Exact of 'a
+ | Step of rule * int * int * direction * position * 'a substitution
+ (* rule, eq1, eq2, direction of eq2, position, substitution *)
+
+type 'a literal =
+ | Equation of 'a foterm (* lhs *)
+ * 'a foterm (* rhs *)
+ * 'a foterm (* type *)
+ * comparison (* orientation *)
+ | Predicate of 'a foterm
+
+type varlist = int list
+
+type 'a unit_clause =
+ int (* ID *)
+ * 'a literal
+ * varlist
+ * 'a proof (* proof *)
+
+type 'a passive_clause = int * 'a unit_clause (* weight * equation *)
+
+module M : Map.S with type key = int
+
+type 'a bag = 'a unit_clause M.t
+
projects / helm.git / commitdiff