From: Enrico Tassi Date: Thu, 4 Jun 2009 08:09:31 +0000 (+0000) Subject: more functors X-Git-Tag: make_still_working~3925 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c1a432c1612f8ed21f5b2220005599c4d9da1d5;p=helm.git more functors --- diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 1b047daac..16b4a0b16 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -4,10 +4,12 @@ founif.cmi: terms.cmi index.cmi: terms.cmi orderings.cmi: terms.cmi subst.cmi: terms.cmi +nCicBlob.cmi: terms.cmi +cicBlob.cmi: terms.cmi terms.cmo: terms.cmi terms.cmx: terms.cmi -pp.cmo: pp.cmi -pp.cmx: pp.cmi +pp.cmo: terms.cmi pp.cmi +pp.cmx: terms.cmx pp.cmi founif.cmo: terms.cmi subst.cmi founif.cmi founif.cmx: terms.cmx subst.cmx founif.cmi index.cmo: terms.cmi index.cmi @@ -16,3 +18,7 @@ orderings.cmo: terms.cmi orderings.cmi orderings.cmx: terms.cmx orderings.cmi subst.cmo: terms.cmi subst.cmi subst.cmx: terms.cmx subst.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 diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile index ccf1b57a4..7eee8d511 100644 --- a/helm/software/components/ng_paramodulation/Makefile +++ b/helm/software/components/ng_paramodulation/Makefile @@ -1,7 +1,8 @@ PACKAGE = ng_paramodulation INTERFACE_FILES = \ - terms.mli pp.mli founif.mli index.mli orderings.mli subst.mli + terms.mli pp.mli founif.mli index.mli orderings.mli subst.mli \ + nCicBlob.mli cicBlob.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_paramodulation/cicBlob.ml b/helm/software/components/ng_paramodulation/cicBlob.ml new file mode 100644 index 000000000..f0caf2591 --- /dev/null +++ b/helm/software/components/ng_paramodulation/cicBlob.ml @@ -0,0 +1,35 @@ +(* + ||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.mli 9822 2009-06-03 15:37:06Z tassi $ *) + +module type CicContext = + sig + val metasenv : Cic.metasenv + val subst : Cic.substitution + val context : Cic.context + end + +module CicBlob(C : CicContext) : Terms.Blob with type t = Cic.term = struct + + type t = Cic.term + + (* XXX this alpha-eq is a bit strange, since it does not take a + * context nor a subst ... *) + let eq x y = CicUtil.alpha_equivalence x y;; + + (* TODO: take this from tactics/paramodulation/utils.ml *) + let compare x y = assert false;; + + let names = List.map (function Some (x,_) -> Some x | _ -> None) C.context;; + let pp t = CicPp.pp t names;; +end + diff --git a/helm/software/components/ng_paramodulation/cicBlob.mli b/helm/software/components/ng_paramodulation/cicBlob.mli new file mode 100644 index 000000000..21f117744 --- /dev/null +++ b/helm/software/components/ng_paramodulation/cicBlob.mli @@ -0,0 +1,22 @@ +(* + ||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.mli 9822 2009-06-03 15:37:06Z tassi $ *) + +module type CicContext = + sig + val metasenv : Cic.metasenv + val subst : Cic.substitution + val context : Cic.context + end + +module CicBlob(C : CicContext) : Terms.Blob with type t = Cic.term + diff --git a/helm/software/components/ng_paramodulation/founif.ml b/helm/software/components/ng_paramodulation/founif.ml index bc18aaf00..5a3f67ae9 100644 --- a/helm/software/components/ng_paramodulation/founif.ml +++ b/helm/software/components/ng_paramodulation/founif.ml @@ -15,6 +15,7 @@ exception UnificationFailure of string Lazy.t;; module Founif (B : Terms.Blob) = struct module Subst = Subst.Subst(B) + module U = Terms.Utils(B) let unification vars locked_vars t1 t2 = let lookup = Subst.lookup_subst in @@ -23,7 +24,7 @@ module Founif (B : Terms.Blob) = struct | 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 + if not (U.eq_foterm t where) then occurs_check subst what t else false | Terms.Node l -> List.exists (occurs_check subst what) l | _ -> false in @@ -33,7 +34,7 @@ module Founif (B : Terms.Blob) = struct in match s, t with - | s, t when s = t -> subst, vars + | s, t when U.eq_foterm s t -> subst, vars | Terms.Var i, Terms.Var j when (List.mem i locked_vars) &&(List.mem j locked_vars) -> raise @@ -52,7 +53,7 @@ module Founif (B : Terms.Blob) = struct 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 -> + | Terms.Node (hds::_),Terms.Node (hdt::_) when not(U.eq_foterm hds hdt)-> raise (UnificationFailure (lazy "Inference.unification.unif")) | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> ( try diff --git a/helm/software/components/ng_paramodulation/founif.mli b/helm/software/components/ng_paramodulation/founif.mli index 55f15e656..fc682c5fc 100644 --- a/helm/software/components/ng_paramodulation/founif.mli +++ b/helm/software/components/ng_paramodulation/founif.mli @@ -16,22 +16,13 @@ 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*) - B.t Terms.foterm -> - B.t Terms.foterm -> - B.t 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 - -*) + val unification: + (* global varlist for both terms t1 and t2 *) + Terms.varlist -> + (* locked variables: if equal to FV(t2) we match t1 with t2*) + Terms.varlist -> + B.t Terms.foterm -> + B.t Terms.foterm -> + B.t Terms.substitution * Terms.varlist end diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml new file mode 100644 index 000000000..87d081dea --- /dev/null +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -0,0 +1,38 @@ +(* + ||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.mli 9822 2009-06-03 15:37:06Z tassi $ *) + +module type NCicContext = + sig + val metasenv : NCic.metasenv + val subst : NCic.substitution + val context : NCic.context + end + +module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct + + type t = NCic.term + + let eq x y = NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; + + let rec compare x y = + match x,y with + | NCic.Rel i, NCic.Rel j -> i-j + | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2 + | NCic.Appl l1, NCic.Appl l2 -> assert false (* TODO *) + | _ -> assert false + ;; + + let pp t = + NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;; + + end diff --git a/helm/software/components/ng_paramodulation/nCicBlob.mli b/helm/software/components/ng_paramodulation/nCicBlob.mli new file mode 100644 index 000000000..5fafaf54f --- /dev/null +++ b/helm/software/components/ng_paramodulation/nCicBlob.mli @@ -0,0 +1,22 @@ +(* + ||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.mli 9822 2009-06-03 15:37:06Z tassi $ *) + +module type NCicContext = + sig + val metasenv : NCic.metasenv + val subst : NCic.substitution + val context : NCic.context + end + +module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term + diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli index f2f6a1678..74989c3eb 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -13,5 +13,12 @@ module Orderings (B : Terms.Blob) : sig - val compare_terms : B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison + + (* This order relation should be: + * - stable for instantiation + * - total on ground terms + *) + val compare_terms : + B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison + end diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 3013ed7d0..f5aaa619f 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -52,14 +52,24 @@ type 'a bag = 'a unit_clause M.t module type Blob = sig + (* Blob is the type for opaque leaves: + * - checking equlity should be efficient + * - atoms have to be equipped with a total order relation + *) type t val eq : t -> t -> bool val compare : t -> t -> int - val pp : t -> string + (* TODO: consider taking in input an imperative buffer for Format + * val pp : Format.formatter -> t -> unit + * *) + val pp : t -> string 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