+terms.cmi:
pp.cmi: terms.cmi
-fosubst.cmi: terms.cmi
-founif.cmi: terms.cmi
+foSubst.cmi: terms.cmi
+foUnif.cmi: terms.cmi
index.cmi: terms.cmi
orderings.cmi: terms.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
+paramod.cmi:
terms.cmo: terms.cmi
terms.cmx: terms.cmi
pp.cmo: terms.cmi pp.cmi
pp.cmx: terms.cmx pp.cmi
-fosubst.cmo: terms.cmi fosubst.cmi
-fosubst.cmx: terms.cmx fosubst.cmi
-founif.cmo: terms.cmi fosubst.cmi founif.cmi
-founif.cmx: terms.cmx fosubst.cmx founif.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
orderings.cmo: terms.cmi orderings.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 founif.cmi paramod.cmi
-paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx founif.cmx paramod.cmi
+paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi paramod.cmi
+paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx paramod.cmi
+terms.cmi:
pp.cmi: terms.cmi
-fosubst.cmi: terms.cmi
-founif.cmi: terms.cmi
+foSubst.cmi: terms.cmi
+foUnif.cmi: terms.cmi
index.cmi: terms.cmi
orderings.cmi: terms.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
+paramod.cmi:
terms.cmo: terms.cmi
terms.cmx: terms.cmi
pp.cmo: terms.cmi pp.cmi
pp.cmx: terms.cmx pp.cmi
-fosubst.cmo: terms.cmi fosubst.cmi
-fosubst.cmx: terms.cmx fosubst.cmi
-founif.cmo: terms.cmi fosubst.cmi founif.cmi
-founif.cmx: terms.cmx fosubst.cmx founif.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
orderings.cmo: terms.cmi orderings.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 founif.cmi paramod.cmi
-paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx founif.cmx paramod.cmi
+paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi paramod.cmi
+paramod.cmx: terms.cmx pp.cmx nCicBlob.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 foUnif.mli index.mli orderings.mli \
nCicBlob.mli cicBlob.mli paramod.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_______________________________________________________________ *)
+
+module Subst (B : Terms.Blob) = struct
+
+ let id_subst = [];;
+
+ let build_subst 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 lookup_subst i subst = lookup_subst (Terms.Var i) subst;;
+
+ 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
--- /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 $ *)
+
+module Subst (B : Terms.Blob) :
+ sig
+ val id_subst : B.t Terms.substitution
+ val build_subst :
+ int -> B.t Terms.foterm -> B.t Terms.substitution ->
+ B.t Terms.substitution
+ val lookup_subst :
+ int -> B.t Terms.substitution -> B.t Terms.foterm
+ val filter : B.t Terms.substitution -> Terms.varlist -> 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: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+exception UnificationFailure of string Lazy.t;;
+
+module Founif (B : Terms.Blob) = struct
+ module Subst = FoSubst.Subst(B)
+ module U = Terms.Utils(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 i ->
+ let t = lookup i subst in
+ 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
+ let rec unif subst s t =
+ let s = match s with Terms.Var i -> lookup i subst | _ -> s
+ and t = match t with Terms.Var i -> lookup i subst | _ -> t
+
+ in
+ match s, t with
+ | s, t when U.eq_foterm s t -> subst
+ | 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 t s
+ | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
+ unif subst 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.build_subst i t subst in
+ subst
+ | _, Terms.Var _ -> unif subst t s
+ | Terms.Node l1, Terms.Node l2 -> (
+ try
+ List.fold_left2
+ (fun subst' s t -> unif subst' s t)
+ subst l1 l2
+ with Invalid_argument _ ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ )
+ | _, _ ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ in
+ let subst = unif Subst.id_subst t1 t2 in
+ let vars = Subst.filter subst vars in
+ subst, vars
+
+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: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+exception UnificationFailure of string Lazy.t;;
+
+module Founif (B : Terms.Blob) :
+ sig
+
+ 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_______________________________________________________________ *)
-
-module Subst (B : Terms.Blob) = struct
-
- let id_subst = [];;
-
- let build_subst 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 lookup_subst i subst = lookup_subst (Terms.Var i) subst;;
-
- 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
+++ /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 $ *)
-
-module Subst (B : Terms.Blob) :
- sig
- val id_subst : B.t Terms.substitution
- val build_subst :
- int -> B.t Terms.foterm -> B.t Terms.substitution ->
- B.t Terms.substitution
- val lookup_subst :
- int -> B.t Terms.substitution -> B.t Terms.foterm
- val filter : B.t Terms.substitution -> Terms.varlist -> 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: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-
-exception UnificationFailure of string Lazy.t;;
-
-module Founif (B : Terms.Blob) = struct
- module Subst = Fosubst.Subst(B)
- module U = Terms.Utils(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 i ->
- let t = lookup i subst in
- 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
- let rec unif subst s t =
- let s = match s with Terms.Var i -> lookup i subst | _ -> s
- and t = match t with Terms.Var i -> lookup i subst | _ -> t
-
- in
- match s, t with
- | s, t when U.eq_foterm s t -> subst
- | 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 t s
- | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
- unif subst 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.build_subst i t subst in
- subst
- | _, Terms.Var _ -> unif subst t s
- | Terms.Node l1, Terms.Node l2 -> (
- try
- List.fold_left2
- (fun subst' s t -> unif subst' s t)
- subst l1 l2
- with Invalid_argument _ ->
- raise (UnificationFailure (lazy "Inference.unification.unif"))
- )
- | _, _ ->
- raise (UnificationFailure (lazy "Inference.unification.unif"))
- in
- let subst = unif Subst.id_subst t1 t2 in
- let vars = Subst.filter subst vars in
- subst, vars
-
-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: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-
-exception UnificationFailure of string Lazy.t;;
-
-module Founif (B : Terms.Blob) :
- sig
-
- 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
let module B = NCicBlob.NCicBlob(C) in
let module Pp = Pp.Pp (B) in
let res,vars = B.embed t in
- let module FU = Founif.Founif(B) in
+ let module FU = FoUnif.Founif(B) in
let test_unification vars = function
| Terms.Node [_; _; lhs; rhs] ->
prerr_endline "Unification test :";
projects / helm.git / commitdiff