1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
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 Datum
= Atom Int -- unifies a constant
| Struct (Int, Int) -- unifies a structure with arity
-- | VoidVar -- unifies with anything
-- | LocalVar Int -- unifies with a local variable (possibly making a new one when it's not in use yet)
-- | Ref Int -- unifies with the referenced value on the heap (not to be used in code)
deriving (Show, Eq, Ord)
data Instr
= U Datum -- something unifiable
| 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
| Cut -- remove all alternative clauses of the current goal
deriving (Show)
type Code = [Instr]
type Defs = M.Map (Int, Int) [Code]
data Cho =
Cho
{ hed :: Code -- head pointer
, gol :: Code -- goal pointer
, stk :: [Code] -- remaining "and" goals
, cut :: [Cho] -- snapshot of choicepoints
}
deriving (Show)
data Interp =
Interp
{ defs :: Defs -- global definitions for lookup
, cur :: Cho -- the choice that is being evaluated right now
, cho :: [Cho] -- remaining choice points
}
deriving (Show)
prove :: Code -> Defs -> Either (Interp, String) Bool
prove g ds =
let i0 =
Interp
{defs = ds, cur = Cho {hed = g, gol = [LastCall], stk = [], cut = []}, cho = []}
run (Left x) = x
run (Right x) = run $ proveStep Right Left x
in run (Right i0)
{- this gonna need Either String Bool for errors later -}
proveStep :: (Interp -> a) -> (Either (Interp, String) Bool -> a) -> Interp -> a
proveStep c f i = go i
where
ifail msg = f $ Left (i, msg)
withDef fn
| Just d <- defs i M.!? fn = ($ d)
| otherwise = const $ ifail $ "no definition: " ++ show fn
{- Backtracking -}
backtrack i@Interp {cho = chos}
{- if available, restore the easiest choicepoint -}
| (cho:chos) <- chos = c i {cur = cho, cho = chos}
{- if there's no other choice, answer no -}
| otherwise = f (Right False)
{- Unification -}
go i@Interp {cur = cur@Cho {hed = U a:hs, gol = U b:gs}} -- unify constants
= unify a b
where
uok = c i {cur = cur {hed = hs, gol = gs}}
unify (Atom a) (Atom b)
| a == b = uok
unify (Struct a) (Struct b)
| a == b = uok
unify _ _ = backtrack i
{- Resulution -}
go i@Interp {cur = cur@Cho {hed = hed, gol = gol, stk = stk}, cho = chos}
{- top-level success -}
| [NoGoal] <- hed
, [LastCall] <- gol
, [] <- stk = f (Right True)
{- succeed and return to caller -}
| [NoGoal] <- hed
, [LastCall] <- gol
, (Goal:U (Struct fn):gs):ss <- stk =
withDef fn $ \(hs:ohs) ->
c
i
{ cur = cur {hed = hs, gol = gs, stk = ss}
, cho = [Cho oh gs ss chos | oh <- ohs] ++ chos
}
{- start matching next goal -}
| [NoGoal] <- hed
, (Call:Goal:U (Struct fn):gs) <- gol =
withDef fn $ \(hs:ohs) ->
c
i
{ cur = cur {hed = hs, gol = gs}
, cho = [Cho oh gs stk chos | oh <- ohs] ++ chos
}
{- goal head matching succeeded, make a normal call -}
| (Goal:U (Struct fn):ngs) <- hed
, (Call:gs) <- gol =
withDef fn $ \(hs:ohs) ->
c
i
{ cur = cur {hed = hs, gol = ngs, stk = gs : stk}
, cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
}
{- R: Successful match continued by tail call -}
| (Goal:U (Struct fn):ngs) <- hed
, [LastCall] <- gol =
withDef fn $ \(hs:ohs) ->
c
i
{ cur = cur {hed = hs, gol = ngs}
, cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
}
{- The End -}
go _ = ifail "impossible instruction combo"
|
