ok simplify the refs back

This commit is contained in:
Mirek Kratochvil 2022-11-15 20:30:53 +01:00
parent 8d5353dc8c
commit e074e454d5
5 changed files with 54 additions and 66 deletions

View file

@ -10,39 +10,45 @@ import qualified Operators as O
bi = Builtin bi = Builtin
hello = hello :: BuiltinFn
bi $ do hello = do
liftIO $ putStrLn "hllo prlg" liftIO $ putStrLn "hllo prlg"
return Nothing return Nothing
printLocals :: BuiltinFn
printLocals = do
return Nothing
addBuiltins :: PrlgEnv () addBuiltins :: PrlgEnv ()
addBuiltins = do addBuiltins = do
a1 <- findStruct "a" 1 a1 <- findStruct "a" 1
a <- findAtom "a" a <- findAtom "a"
b <- findAtom "b" b <- findAtom "b"
c <- findAtom "c" c <- findAtom "c"
varX <- findAtom "X"
b0 <- findStruct "b" 0 b0 <- findStruct "b" 0
any1 <- findStruct "any" 1 any1 <- findStruct "any" 1
eq2 <- findStruct "=" 2 eq2 <- findStruct "=" 2
hello0 <- findStruct "hello" 0 hello0 <- findStruct "hello" 0
fail0 <- findStruct "fail" 0 fail0 <- findStruct "fail" 0
true0 <- findStruct "true" 0 true0 <- findStruct "true" 0
prlgstate0 <- findStruct "prlgstate" 0 printlocals0 <- findStruct "print_locals" 0
debugprint0 <- findStruct "interpreter_state" 0
modify $ \s -> modify $ \s ->
s s
{ defs = { defs =
M.fromList M.fromList
[ (eq2, [[U (LocalRef 0 Nothing), U (LocalRef 0 Nothing), NoGoal]]) [ (eq2, [[U (LocalRef 0 varX), U (LocalRef 0 varX), NoGoal]])
, (a1, [[U (Atom a), NoGoal], [U (Atom b), NoGoal]]) , (a1, [[U (Atom a), NoGoal], [U (Atom b), NoGoal]])
, ( b0 , ( b0
, [ [Goal, U (Struct a1), U (Atom c), LastCall] , [ [Goal, U (Struct a1), U (Atom c), LastCall]
, [Goal, U (Struct a1), U (Atom b), LastCall] , [Goal, U (Struct a1), U (Atom b), LastCall]
]) ])
, (any1, [[U (VoidRef Nothing), NoGoal]]) , (any1, [[U VoidRef, NoGoal]])
, (hello0, [[Invoke hello]]) , (hello0, [[Invoke $ bi hello]])
, (fail0, [[Invoke $ bi backtrack]]) , (fail0, [[Invoke $ bi backtrack]])
, (true0, [[Invoke $ bi (pure Nothing)]]) , (true0, [[Invoke $ bi (pure Nothing)]])
, ( prlgstate0 , ( debugprint0
, [[Invoke $ bi (get >>= liftIO . print >> pure Nothing)]]) , [[Invoke $ bi (get >>= liftIO . print >> pure Nothing)]])
] ]
, ops = [(O.xfy "," 1000), (O.xfx "=" 700)] , ops = [(O.xfy "," 1000), (O.xfx "=" 700)]

View file

@ -9,9 +9,9 @@ import System.Console.Haskeline
data Datum data Datum
= Atom Int -- unifies a constant = Atom Int -- unifies a constant
| Struct Id -- unifies a structure with arity | Struct Id -- unifies a structure with arity
| VoidRef (Maybe Int) -- unifies with anything (references may refer to variable names) | VoidRef -- unifies with anything
| LocalRef Int (Maybe Int) -- code-local variable idx (should not occur on heap) | LocalRef Int Int -- code-local variable idx (should never occur on heap)
| HeapRef Int (Maybe Int) -- heap structure idx | HeapRef Int -- something further on the heap
deriving (Show, Eq, Ord) deriving (Show, Eq, Ord)
data Instr data Instr
@ -34,7 +34,7 @@ data Heap =
emptyHeap = Heap 0 M.empty emptyHeap = Heap 0 M.empty
type Scope = M.Map Int Int type Scope = M.Map Int (Int, Int)
emptyScope :: Scope emptyScope :: Scope
emptyScope = M.empty emptyScope = M.empty

View file

@ -32,7 +32,7 @@ variablizePrlg :: Int -> [Int] -> PrlgInt -> PrlgInt
variablizePrlg void vs (CallI id ps) = variablizePrlg void vs (CallI id ps) =
CallI id $ map (variablizePrlg void vs) ps CallI id $ map (variablizePrlg void vs) ps
variablizePrlg void vs (LiteralI i) variablizePrlg void vs (LiteralI i)
| i == void = VoidI i | i == void = VoidI
| Just idx <- elemIndex i vs = VarI idx i | Just idx <- elemIndex i vs = VarI idx i
| otherwise = LiteralI i | otherwise = LiteralI i
@ -50,8 +50,8 @@ compileGoal x = compileArg x
compileArg :: PrlgInt -> Code compileArg :: PrlgInt -> Code
compileArg (CallI x args) = U (Struct x) : concatMap compileArg args compileArg (CallI x args) = U (Struct x) : concatMap compileArg args
compileArg (LiteralI x) = [U (Atom x)] compileArg (LiteralI x) = [U (Atom x)]
compileArg (VarI x i) = [U (LocalRef x $ Just i)] compileArg (VarI x i) = [U (LocalRef x i)]
compileArg (VoidI i) = [U (VoidRef $ Just i)] compileArg (VoidI) = [U VoidRef]
seqGoals :: [Code] -> Code seqGoals :: [Code] -> Code
seqGoals [] = [NoGoal] seqGoals [] = [NoGoal]

View file

@ -18,7 +18,7 @@ data PrlgInt
= CallI Id [PrlgInt] = CallI Id [PrlgInt]
| LiteralI Int | LiteralI Int
| VarI Int Int | VarI Int Int
| VoidI Int | VoidI
deriving (Show) deriving (Show)
data StrTable = data StrTable =

View file

@ -69,7 +69,6 @@ proveStep = St.get >>= go
, gol = U g:gs , gol = U g:gs
, heap = heap@(Heap _ hmap) , heap = heap@(Heap _ hmap)
}} = unify h g }} = unify h g
{- termination tools -}
where where
uok = c i {cur = cur {hed = hs, gol = gs}} uok = c i {cur = cur {hed = hs, gol = gs}}
setHeap r x = setHeap r x =
@ -77,7 +76,7 @@ proveStep = St.get >>= go
{- heap tools -} {- heap tools -}
deref x = deref x =
case hmap M.!? x of case hmap M.!? x of
Just (HeapRef x' _) -> Just (HeapRef x') ->
if x == x' if x == x'
then FreeRef x' then FreeRef x'
else deref x' else deref x'
@ -88,71 +87,56 @@ proveStep = St.get >>= go
newHeapVars n (Heap nxt m) = newHeapVars n (Heap nxt m) =
let addrs = [nxt + i - 1 | i <- [1 .. n]] let addrs = [nxt + i - 1 | i <- [1 .. n]]
in ( Heap (nxt + n) $ in ( Heap (nxt + n) $
foldr (uncurry M.insert) m [(a, HeapRef a Nothing) | a <- addrs] foldr (uncurry M.insert) m [(a, HeapRef a) | a <- addrs]
, addrs) , addrs)
allocLocal reg scope cont allocLocal (LocalRef reg ident) scope cont
| Just addr <- scope M.!? reg = cont scope heap addr | Just (addr, _) <- scope M.!? reg = cont scope heap addr
| (heap', addr) <- newHeapVar heap = | (heap', addr) <- newHeapVar heap =
cont (M.insert reg addr scope) heap' addr cont (M.insert reg (addr, ident) scope) heap' addr
newHeapStruct addr s@(Struct Id {arity = arity}) cont = newHeapStruct addr s@(Struct Id {arity = arity}) cont =
let (Heap nxt' m', addrs) = newHeapVars (arity + 1) heap let (Heap nxt' m', addrs) = newHeapVars (arity + 1) heap
m'' = m'' =
M.insert addr (HeapRef (head addrs) Nothing) . M.insert addr (HeapRef $ head addrs) . M.insert (head addrs) s $
M.insert (head addrs) s $
m' m'
in cont [HeapRef a Nothing | a <- tail addrs] (Heap nxt' m'') in cont (map HeapRef $ tail addrs) (Heap nxt' m'')
{- simple cases first -} {- simple cases first -}
unify (VoidRef _) (VoidRef _) = uok unify VoidRef VoidRef = uok
unify (Atom a) (Atom b) unify (Atom a) (Atom b)
| a == b = uok | a == b = uok
unify (VoidRef _) (Atom _) = uok unify VoidRef (Atom _) = uok
unify (Atom _) (VoidRef _) = uok unify (Atom _) VoidRef = uok
unify (Struct a) (Struct b) unify (Struct a) (Struct b)
| a == b = uok | a == b = uok
{- unifying a struct with void must cause us to skip the void -} {- unifying a struct with void must cause us to skip the void -}
unify (VoidRef _) (Struct Id {arity = a}) = unify VoidRef (Struct Id {arity = a}) =
c c i {cur = cur {hed = replicate a (U VoidRef) ++ hs, gol = gs}}
i unify (Struct Id {arity = a}) VoidRef =
{ cur = c i {cur = cur {hed = hs, gol = replicate a (U VoidRef) ++ gs}}
cur {hed = replicate a (U $ VoidRef Nothing) ++ hs, gol = gs}
}
unify (Struct Id {arity = a}) (VoidRef _) =
c
i
{ cur =
cur {hed = hs, gol = replicate a (U $ VoidRef Nothing) ++ gs}
}
{- handle local refs; first ignore their combination with voids to save memory -} {- handle local refs; first ignore their combination with voids to save memory -}
unify (LocalRef _ _) (VoidRef _) = uok unify (LocalRef _ _) VoidRef = uok
unify (VoidRef _) (LocalRef _ _) = uok unify VoidRef (LocalRef _ _) = uok
{- allocate heap for LocalRefs and retry with HeapRefs -} {- allocate heap for LocalRefs and retry with HeapRefs -}
unify (LocalRef hv ident) _ = unify lr@(LocalRef _ _) _ =
allocLocal hv (hvar cur) $ \hvar' heap' addr -> allocLocal lr (hvar cur) $ \hvar' heap' addr ->
c c
i i
{ cur = { cur =
cur cur
{ hed = U (HeapRef addr ident) : hs {hed = U (HeapRef addr) : hs, hvar = hvar', heap = heap'}
, hvar = hvar'
, heap = heap'
} }
} unify _ lr@(LocalRef _ _) =
unify _ (LocalRef gv ident) = allocLocal lr (gvar cur) $ \gvar' heap' addr ->
allocLocal gv (gvar cur) $ \gvar' heap' addr ->
c c
i i
{ cur = { cur =
cur cur
{ gol = U (HeapRef addr ident) : gs {gol = U (HeapRef addr) : gs, gvar = gvar', heap = heap'}
, gvar = gvar'
, heap = heap'
}
} }
{- handle heap refs; first ignore their combination with voids again -} {- handle heap refs; first ignore their combination with voids again -}
unify (HeapRef _ _) (VoidRef _) = uok unify (HeapRef _) VoidRef = uok
unify (VoidRef _) (HeapRef _ _) = uok unify VoidRef (HeapRef _) = uok
{- actual HeapRefs, these are dereferenced and then unified (sometimes with copying) -} {- actual HeapRefs, these are dereferenced and then unified (sometimes with copying) -}
unify (HeapRef hr' hident) g = unify (HeapRef hr') g =
case deref hr' of case deref hr' of
FreeRef hr -> FreeRef hr ->
case g of case g of
@ -168,10 +152,10 @@ proveStep = St.get >>= go
cur cur
{hed = map U nhs ++ hs, gol = gs, heap = nheap} {hed = map U nhs ++ hs, gol = gs, heap = nheap}
}) })
HeapRef gr' _ -> HeapRef gr' ->
case deref gr' of case deref gr' of
FreeRef gr -> setHeap hr (HeapRef gr hident) FreeRef gr -> setHeap hr (HeapRef gr)
BoundRef addr _ -> setHeap hr (HeapRef addr hident) BoundRef addr _ -> setHeap hr (HeapRef addr)
_ -> ifail "dangling goal ref (from head ref)" _ -> ifail "dangling goal ref (from head ref)"
BoundRef _ atom@(Atom a) -> unify atom g BoundRef _ atom@(Atom a) -> unify atom g
BoundRef addr struct@(Struct Id {arity = arity}) -> BoundRef addr struct@(Struct Id {arity = arity}) ->
@ -181,13 +165,12 @@ proveStep = St.get >>= go
cur cur
{ hed = { hed =
U struct : U struct :
[U (HeapRef (addr + i) Nothing) | i <- [1 .. arity]] ++ [U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ hs
hs
, gol = U g : gs , gol = U g : gs
} }
} }
_ -> ifail "dangling head ref" _ -> ifail "dangling head ref"
unify h (HeapRef gr' gident) = unify h (HeapRef gr') =
case deref gr' of case deref gr' of
FreeRef gr -> FreeRef gr ->
case h of case h of
@ -212,8 +195,7 @@ proveStep = St.get >>= go
{ hed = U h : hs { hed = U h : hs
, gol = , gol =
U struct : U struct :
[U (HeapRef (addr + i) Nothing) | i <- [1 .. arity]] ++ [U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ gs
gs
} }
} }
_ -> ifail "dangling goal ref" _ -> ifail "dangling goal ref"