p r l g

1 files changed, 56 insertions, 0 deletions

diff --git a/app/Interpreter.hs b/app/Interpreter.hs
new file mode 100644
index 0000000..7610903
--- /dev/null
+++ b/app/Interpreter.hs
@@ -0,0 +1,56 @@
+module Interpreter where
+
+import Data.Function
+import qualified Data.Map as M
+
+{- VAM 2P, done the lazy way -}
+
+data StrTable =
+  StrTable Int (M.Map Int String)
+
+data Instr
+  = Atom Int -- unify a constant
+  | Struct (Int, Int) -- unify a structure with arity
+  | NoGoal -- trivial goal
+  | Goal -- we start a new goal, set up backtracking etc
+  | Call -- all seems okay, call the goal
+  | LastCall -- tail call the goal
+  deriving Show
+
+type Defs = M.Map (Int, Int) [Instr]
+
+data Interp =
+  Interp
+    { defs :: Defs
+    , hed :: [Instr]
+    , gol :: [Instr]
+    , stk :: [[Instr]]
+    }
+
+prove :: [Instr] -> Defs -> Bool
+prove g ds =
+  let i0 = Interp ds [NoGoal] [LastCall] [g]
+      run (Left x) = x
+      run (Right x) = run $ pr Right Left x
+   in run (Right i0)
+
+pr :: (Interp -> a) -> (Bool -> a) -> Interp -> a
+pr c f i = go i
+  where
+    go i@Interp {hed = (Atom a:hs), gol = (Atom b:gs)} -- unify constants
+      | a == b = c i {hed = hs, gol = gs}
+    go i@Interp {hed = (Struct a:hs), gol = (Struct b:gs)} -- unify structs
+      | a == b = c i {hed = hs, gol = gs}
+    go i@Interp {hed = [NoGoal], gol = [LastCall], stk = []} = f True -- final success
+    go i@Interp { hed = [NoGoal]
+                , gol = [LastCall]
+                , stk = ((Goal:Struct f:gs):ss)
+                } -- goal succeeded
+      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = gs, stk = ss}
+    go i@Interp {hed = [NoGoal], gol = (Call:Goal:Struct f:gs)} -- next goal
+      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = gs}
+    go i@Interp {hed = (Goal:Struct f:hs), gol = [LastCall]} -- tail call
+      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = hs}
+    go i@Interp {hed = (Goal:Struct f:hs), gol = (Call:gs), stk = ss} -- normal call
+      | Just nhs <- defs i M.!? f = c i {hed = nhs, gol = hs, stk = gs : ss}
+    go _ = f False -- bad luck