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
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
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)
--- /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.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
+
--- /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.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
+
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
| 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
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
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
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
--- /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.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
--- /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.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
+
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
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
projects / helm.git / commitdiff