First tests for paramodulation (pretty printer, unification)

[helm.git] / helm / software / components / ng_paramodulation / fosubst.ml

diff --git a/helm/software/components/ng_paramodulation/fosubst.ml b/helm/software/components/ng_paramodulation/fosubst.ml
new file mode 100644 (file)
index 0000000..1b9f262
--- /dev/null
+++ b/helm/software/components/ng_paramodulation/fosubst.ml
@@ -0,0 +1,39 @@
+(*
+    ||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