From: denes <??>
Date: Mon, 1 Jun 2009 16:36:42 +0000 (+0000)
Subject: First implementation of unification on foterms
X-Git-Tag: make_still_working~3932
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4514417676056e0be6cc481a931e70a627882867;p=helm.git

First implementation of unification on foterms
---

diff --git a/helm/software/components/ng_paramodulation/founif.ml b/helm/software/components/ng_paramodulation/founif.ml
index 125bded70..451524507 100644
--- a/helm/software/components/ng_paramodulation/founif.ml
+++ b/helm/software/components/ng_paramodulation/founif.ml
@@ -11,4 +11,57 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-let unification = assert false
+exception UnificationFailure of string Lazy.t;;
+
+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 _ ->
+        let t = lookup where subst in
+        if 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 vars s t =
+    let s = match s with Terms.Var _ -> lookup s subst | _ -> s
+    and t = match t with Terms.Var _ -> lookup t subst | _ -> t
+    
+    in
+    match s, t with
+    | s, t when s = t -> subst, vars
+    | 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 vars t s
+    | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
+        unif subst vars 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.buildsubst i t subst in
+        subst, vars
+    | _, Terms.Var _ -> unif subst vars t s
+    | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt ->
+        raise (UnificationFailure (lazy "Inference.unification.unif"))
+    | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
+        try
+          List.fold_left2
+            (fun (subst', vars) s t -> unif subst' vars s t)
+            (subst, vars) tls tlt
+        with Invalid_argument _ ->
+          raise (UnificationFailure (lazy "Inference.unification.unif"))
+      )
+    | _, _ ->
+        raise (UnificationFailure (lazy "Inference.unification.unif"))
+  in
+  let subst, vars = unif Subst.empty_subst vars t1 t2 in
+  let vars = Subst.filter subst vars in
+  subst, vars
diff --git a/helm/software/components/ng_paramodulation/founif.mli b/helm/software/components/ng_paramodulation/founif.mli
index d959fc309..2e8018313 100644
--- a/helm/software/components/ng_paramodulation/founif.mli
+++ b/helm/software/components/ng_paramodulation/founif.mli
@@ -11,6 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+exception UnificationFailure of string Lazy.t;;
+
 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*)