terms.cmi:
pp.cmi: terms.cmi
foSubst.cmi: terms.cmi
+foUtils.cmi: terms.cmi
foUnif.cmi: terms.cmi
index.cmi: terms.cmi
orderings.cmi: terms.cmi
+superposition.cmi: terms.cmi index.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
paramod.cmi:
pp.cmx: terms.cmx pp.cmi
foSubst.cmo: terms.cmi foSubst.cmi
foSubst.cmx: terms.cmx foSubst.cmi
-foUnif.cmo: terms.cmi foUnif.cmi
-foUnif.cmx: terms.cmx foUnif.cmi
-index.cmo: terms.cmi index.cmi
-index.cmx: terms.cmx index.cmi
+foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
+foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
+foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi
+foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi
+index.cmo: terms.cmi foUtils.cmi index.cmi
+index.cmx: terms.cmx foUtils.cmx index.cmi
orderings.cmo: terms.cmi orderings.cmi
orderings.cmx: terms.cmx orderings.cmi
+superposition.cmo: terms.cmi index.cmi superposition.cmi
+superposition.cmx: terms.cmx index.cmx superposition.cmi
nCicBlob.cmo: terms.cmi nCicBlob.cmi
nCicBlob.cmx: terms.cmx nCicBlob.cmi
cicBlob.cmo: terms.cmi cicBlob.cmi
cicBlob.cmx: terms.cmx cicBlob.cmi
-paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi paramod.cmi
-paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx paramod.cmi
+paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \
+ foUnif.cmi paramod.cmi
+paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \
+ foUnif.cmx paramod.cmi
terms.cmi:
pp.cmi: terms.cmi
foSubst.cmi: terms.cmi
+foUtils.cmi: terms.cmi
foUnif.cmi: terms.cmi
index.cmi: terms.cmi
orderings.cmi: terms.cmi
+superposition.cmi: terms.cmi index.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
paramod.cmi:
pp.cmx: terms.cmx pp.cmi
foSubst.cmo: terms.cmi foSubst.cmi
foSubst.cmx: terms.cmx foSubst.cmi
-foUnif.cmo: terms.cmi foUnif.cmi
-foUnif.cmx: terms.cmx foUnif.cmi
-index.cmo: terms.cmi index.cmi
-index.cmx: terms.cmx index.cmi
+foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
+foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
+foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi
+foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi
+index.cmo: terms.cmi foUtils.cmi index.cmi
+index.cmx: terms.cmx foUtils.cmx index.cmi
orderings.cmo: terms.cmi orderings.cmi
orderings.cmx: terms.cmx orderings.cmi
+superposition.cmo: terms.cmi index.cmi superposition.cmi
+superposition.cmx: terms.cmx index.cmx superposition.cmi
nCicBlob.cmo: terms.cmi nCicBlob.cmi
nCicBlob.cmx: terms.cmx nCicBlob.cmi
cicBlob.cmo: terms.cmi cicBlob.cmi
cicBlob.cmx: terms.cmx cicBlob.cmi
-paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi paramod.cmi
-paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx paramod.cmi
+paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \
+ foUnif.cmi paramod.cmi
+paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \
+ foUnif.cmx paramod.cmi
PACKAGE = ng_paramodulation
INTERFACE_FILES = \
- terms.mli pp.mli foSubst.mli foUnif.mli index.mli orderings.mli \
+ terms.mli pp.mli foSubst.mli foUtils.mli \
+ foUnif.mli index.mli orderings.mli superposition.mli \
nCicBlob.mli cicBlob.mli paramod.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
let pp t = CicPp.pp t names;;
let embed t = assert false;;
+
+ let is_eq_predicate = assert false
+ let saturate = assert false
end
not (is_in_subst m subst))
varlist
;;
+
+ let apply_subst = assert false;;
+ let concat = assert false
end
val lookup_subst :
int -> B.t Terms.substitution -> B.t Terms.foterm
val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist
+ val apply_subst :
+ B.t Terms.substitution -> B.t Terms.foterm -> B.t Terms.foterm
+ val concat:
+ B.t Terms.substitution -> B.t Terms.substitution ->
+ B.t Terms.substitution
end
module Founif (B : Terms.Blob) = struct
module Subst = FoSubst.Subst(B)
- module U = Terms.Utils(B)
+ module U = FoUtils.Utils(B)
let unification vars locked_vars t1 t2 =
let lookup = Subst.lookup_subst in
--- /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: terms.ml 9836 2009-06-05 15:33:35Z denes $ *)
+
+
+module Utils (B : Terms.Blob) = struct
+ module Subst = FoSubst.Subst(B) ;;
+ module Order = Orderings.Orderings(B) ;;
+
+ let rec eq_foterm x y =
+ x == y ||
+ match x, y with
+ | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2
+ | Terms.Var i, Terms.Var j -> i = j
+ | Terms.Node l1, Terms.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
+ | Terms.Leaf t1, Terms.Leaf t2 -> B.compare t1 t2
+ | Terms.Var i, Terms.Var j -> i - j
+ | Terms.Node l1, Terms.Node l2 -> lexicograph compare_foterm l1 l2
+ | Terms.Leaf _, ( Terms.Node _ | Terms.Var _ ) -> ~-1
+ | Terms.Node _, Terms.Leaf _ -> 1
+ | Terms.Node _, Terms.Var _ -> ~-1
+ | Terms.Var _, _ -> 1
+ ;;
+
+ let eq_literal l1 l2 =
+ match l1, l2 with
+ | Terms.Predicate p1, Terms.Predicate p2 -> eq_foterm p1 p2
+ | Terms.Equation (l1,r1,ty1,o1), Terms.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
+ | Terms.Predicate p1, Terms.Predicate p2 -> compare_foterm p1 p2
+ | Terms.Equation (l1,r1,ty1,o1), Terms.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
+ | Terms.Predicate _, Terms.Equation _ -> ~-1
+ | Terms.Equation _, Terms.Predicate _ -> 1
+ ;;
+
+ let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2
+ let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2
+
+ let relocate maxvar varlist =
+ List.fold_right
+ (fun i (maxvar, varlist, s) ->
+ maxvar+1, maxvar::varlist, Subst.build_subst i (Terms.Var maxvar) s)
+ varlist (maxvar+1, [], Subst.id_subst)
+ ;;
+
+ let fresh_unit_clause maxvar (id, lit, varlist, proof) =
+ let maxvar, varlist, subst = relocate maxvar varlist in
+ let lit =
+ match lit with
+ | Terms.Equation (l,r,ty,o) ->
+ let l = Subst.apply_subst subst l in
+ let r = Subst.apply_subst subst r in
+ let ty = Subst.apply_subst subst ty in
+ Terms.Equation (l,r,ty,o)
+ | Terms.Predicate p ->
+ let p = Subst.apply_subst subst p in
+ Terms.Predicate p
+ in
+ let proof =
+ match proof with
+ | Terms.Exact t -> Terms.Exact (Subst.apply_subst subst t)
+ | Terms.Step (rule,c1,c2,dir,pos,s) ->
+ Terms.Step(rule,c1,c2,dir,pos,Subst.concat subst s)
+ in
+ (id, lit, varlist, proof), maxvar
+ ;;
+
+ (* may be moved inside the bag *)
+ let mk_id =
+ let id = ref 0 in
+ fun () -> incr id; !id
+ ;;
+
+ let mk_unit_clause maxvar ty proofterm =
+ let varlist =
+ let rec aux acc = function
+ | Terms.Leaf _ -> acc
+ | Terms.Var i -> if List.mem i acc then acc else i::acc
+ | Terms.Node l -> List.fold_left aux acc l
+ in
+ aux (aux [] ty) proofterm
+ in
+ let lit =
+ match ty with
+ | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.is_eq_predicate eq ->
+ let o = Order.compare_terms l r in
+ Terms.Equation (l, r, ty, o)
+ | t -> Terms.Predicate t
+ in
+ let proof = Terms.Exact proofterm in
+ fresh_unit_clause maxvar (mk_id (), lit, varlist, proof)
+ ;;
+
+end
--- /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: terms.ml 9836 2009-06-05 15:33:35Z denes $ *)
+
+module Utils (B : Terms.Blob) :
+ sig
+ val eq_foterm : B.t Terms.foterm -> B.t Terms.foterm -> bool
+ val compare_foterm : B.t Terms.foterm -> B.t Terms.foterm -> int
+
+ val eq_literal : B.t Terms.literal -> B.t Terms.literal -> bool
+ val compare_literal : B.t Terms.literal -> B.t Terms.literal -> int
+
+ (* mk_unit_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *)
+ val mk_unit_clause :
+ int -> B.t Terms.foterm -> B.t Terms.foterm ->
+ B.t Terms.unit_clause * int
+
+ val eq_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> bool
+ val compare_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> int
+
+ val fresh_unit_clause :
+ int -> B.t Terms.unit_clause -> B.t Terms.unit_clause * int
+ end
(* $Id$ *)
module Index(B : Terms.Blob) = struct
- module U = Terms.Utils(B)
+ module U = FoUtils.Utils(B)
module ClauseOT =
struct
(fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
in (Terms.Node (List.rev res)), vars
| t -> Terms.Leaf t, []
-;;
+ ;;
+
+ let embed t = fst (embed t) ;;
+
+ let saturate t ty =
+ let sty, _, args =
+ NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
+ ty 0
+ in
+ let proof =
+ if args = [] then Terms.Leaf t
+ else Terms.Node (Terms.Leaf t :: List.map embed args)
+ in
+ let sty = embed sty in
+ proof, sty
+ ;;
+
+ let is_eq_predicate t = assert false;;
+
end
in
let module B = NCicBlob.NCicBlob(C) in
let module Pp = Pp.Pp (B) in
- let res,vars = B.embed t in
+ let res = B.embed t in
let module FU = FoUnif.Founif(B) in
- let test_unification vars = function
+ let module IDX = Index.Index(B) in
+ let module Sup = Superposition.Superposition(B) in
+ let test_unification _ = function
| Terms.Node [_; _; lhs; rhs] ->
prerr_endline "Unification test :";
prerr_endline (Pp.pp_foterm lhs);
prerr_endline (Pp.pp_foterm rhs);
- FU.unification vars [] lhs rhs
+ FU.unification [] [] lhs rhs
| _ -> assert false
in
- let subst,vars = test_unification vars res in
+ let subst,vars = test_unification [] res in
prerr_endline "Result :";
prerr_endline (Pp.pp_foterm res);
prerr_endline "Substitution :";
let pp_proof bag ~formatter:f p =
let rec aux eq = function
| Terms.Exact t ->
- Format.fprintf f "%d: Exact (%s)@;" eq (B.pp t)
+ Format.fprintf f "%d: Exact (" eq;
+ pp_foterm f t;
+ Format.fprintf f ")@;";
| Terms.Step (rule,eq1,eq2,dir,pos,subst) ->
Format.fprintf f "%d: %s("
eq (string_of_rule rule);
--- /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: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
+
+module Superposition (B : Terms.Blob) =
+ struct
+ module IDX = Index.Index(B)
+
+ let all_positions t f =
+ let rec aux pos ctx = function
+ | Terms.Leaf a as t -> f t pos ctx
+ | Terms.Var i -> []
+ | Terms.Node l as t->
+ let acc, _, _ =
+ List.fold_left
+ (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *)
+ let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
+ let acc = aux (List.length pre :: pos) newctx t @ acc in
+ if post = [] then acc, l, []
+ else acc, pre @ [t], List.tl post)
+ (f t pos ctx, [], List.tl l) l
+ in
+ acc
+ in
+ aux [] (fun x -> x) t
+ ;;
+
+ let superposition_right table subterm pos context =
+ let _cands = IDX.DT.retrieve_unifiables table subterm in
+ assert false;;
+(*
+ for every cand in cands
+ let subst = FoUnif.unify l_can t
+ (apply_subst subst (c r_cand)), pos, id_cand, subst
+*)
+
+ let superposition_right_step bag (_,selected,_,_) table =
+ match selected with
+ | Terms.Predicate _ -> assert false
+ | Terms.Equation (l,r,_,Terms.Lt) ->
+ let _r's = all_positions r (superposition_right table) in
+ assert false
+ | Terms.Equation (l,r,_,Terms.Gt) -> assert false
+ | _ -> assert false
+ ;;
+
+ end
+
+
+
--- /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: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
+
+
+module Superposition (B : Terms.Blob) :
+ sig
+
+ val superposition_right_step :
+ B.t Terms.bag ->
+ B.t Terms.unit_clause ->
+ Index.Index(B).DT.t ->
+ B.t Terms.bag * B.t Terms.unit_clause list
+
+ end
+
+
+
type position = int list
type 'a proof =
- | Exact of 'a
+ | Exact of 'a foterm
| Step of rule * int * int * direction * position * 'a substitution
(* rule, eq1, eq2, direction of eq2, position, substitution *)
type t
val eq : t -> t -> bool
val compare : t -> t -> int
+ val is_eq_predicate : t -> bool
val pp : t -> string
- val embed : t -> t foterm * int list
+ val embed : t -> t foterm
+ val saturate : t -> t -> t foterm * t foterm
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
type position = int list
type 'a proof =
- | Exact of 'a
+ | Exact of 'a foterm
+ (* for theorems like T : \forall x. C[x] = D[x] the proof is
+ * a foterm like (Node [ Leaf T ; Var i ]), while for the Goal
+ * it is just (Var g), i.e. the identity proof *)
| Step of rule * int * int * direction * position * 'a substitution
(* rule, eq1, eq2, direction of eq2, position, substitution *)
type t
val eq : t -> t -> bool
val compare : t -> t -> int
+ val is_eq_predicate : t -> bool
(* TODO: consider taking in input an imperative buffer for Format
* val pp : Format.formatter -> t -> unit
* *)
val pp : t -> string
- val embed : t -> t foterm * int list
+ val embed : t -> t foterm
+ (* saturate [proof] [type] -> [proof] * [type] *)
+ val saturate : t -> t -> t foterm * t foterm
end
-module Utils (B : Blob) :
- sig
- val eq_foterm : B.t foterm -> B.t foterm -> bool
- val compare_foterm : B.t foterm -> B.t foterm -> int
-
- 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
projects / helm.git / commitdiff