prim arith hooray

This commit is contained in:
crumbtoo
2023-12-04 11:21:00 -07:00
parent 44030fab0a
commit 7ef3bf1082
2 changed files with 518 additions and 361 deletions

View File

@@ -6,9 +6,9 @@ G-Machine State Transition Rules
Core Transition Rules
*********************
1. Lookup a global by name and push its value onto the stack
#. Lookup a global by name and push its value onto the stack
.. math::
.. math::
\gmrule
{ \mathtt{PushGlobal} \; f : i
& s
@@ -26,10 +26,10 @@ Core Transition Rules
& m
}
2. Allocate an int node on the heap, and push the address of the newly created
#. Allocate an int node on the heap, and push the address of the newly created
node onto the stack
.. math::
.. math::
\gmrule
{ \mathtt{PushInt} \; n : i
& s
@@ -47,11 +47,11 @@ Core Transition Rules
& m
}
3. Allocate an application node on the heap, applying the top of the stack to
#. Allocate an application node on the heap, applying the top of the stack to
the address directly below it. The address of the application node is pushed
onto the stack.
.. math::
.. math::
\gmrule
{ \mathtt{MkAp} : i
& f : x : s
@@ -69,9 +69,9 @@ Core Transition Rules
& m
}
4. Push a function's argument onto the stack
#. Push a function's argument onto the stack
.. math::
.. math::
\gmrule
{ \mathtt{Push} \; n : i
& a_0 : \ldots : a_n : s
@@ -86,9 +86,9 @@ Core Transition Rules
& m
}
5. Tidy up the stack after instantiating a supercombinator
#. Tidy up the stack after instantiating a supercombinator
.. math::
.. math::
\gmrule
{ \mathtt{Slide} \; n : i
& a_0 : \ldots : a_n : s
@@ -103,15 +103,38 @@ Core Transition Rules
& m
}
6. If a number is on top of the stack, :code:`Unwind` leaves the machine in a
halt state
#. If the top of the stack is in WHNF (currently this just means a number) is on
top of the stack, :code:`Unwind` considers evaluation complete. In the case
where the dump is **not** empty, the instruction queue and stack is restored
from the top.
.. math::
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
& \langle i', s' \rangle : d
& h
\begin{bmatrix}
a : \mathtt{NNum} \; n
\end{bmatrix}
& m
}
{ i'
& a : s'
& d
& h
& m
}
#. Bulding on the previous rule, in the case where the dump **is** empty, leave
the machine in a halt state (i.e. with an empty instruction queue).
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
& \nillist
& h
\begin{bmatrix}
a : \mathtt{NNum} \; n
\end{bmatrix}
@@ -119,14 +142,14 @@ Core Transition Rules
}
{ \nillist
& a : s
& d
& \nillist
& h
& m
}
7. If an application is on top of the stack, :code:`Unwind` continues unwinding
#. If an application is on top of the stack, :code:`Unwind` continues unwinding
.. math::
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
@@ -144,11 +167,11 @@ Core Transition Rules
& m
}
8. When a supercombinator is on top of the stack (and the correct number of
#. When a supercombinator is on top of the stack (and the correct number of
arguments have been provided), :code:`Unwind` sets up the stack and jumps to
the supercombinator's code (:math:`\beta`-reduction)
.. math::
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a_0 : \ldots : a_n : s
@@ -169,9 +192,9 @@ Core Transition Rules
& m
}
9. Pop the stack, and update the nth node to point to the popped address
#. Pop the stack, and update the nth node to point to the popped address
.. math::
.. math::
\gmrule
{ \mathtt{Update} \; n : i
& e : f : a_1 : \ldots : a_n : s
@@ -194,9 +217,9 @@ Core Transition Rules
& m
}
10. Pop the stack.
#. Pop the stack.
.. math::
.. math::
\gmrule
{ \mathtt{Pop} \; n : i
& a_1 : \ldots : a_n : s
@@ -211,9 +234,9 @@ Core Transition Rules
& m
}
11. Follow indirections while unwinding
#. Follow indirections while unwinding
.. math::
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
@@ -231,9 +254,9 @@ Core Transition Rules
& m
}
12. Allocate uninitialised heap space
#. Allocate uninitialised heap space
.. math::
.. math::
\gmrule
{ \mathtt{Alloc} \; n : i
& s
@@ -253,30 +276,9 @@ Core Transition Rules
& m
}
13. When unwinding, if the top of the stack is in WHNF (currently this just
means a number), pop the dump
#. Evaluate the top of the stack to WHNF
.. math::
\gmrule
{ \mathtt{Unwind} : \nillist
& a : s
& \langle i', s' \rangle : d
& h
\begin{bmatrix}
a : \mathtt{NNum} \; n
\end{bmatrix}
& m
}
{ i'
& a : s'
& d
& h
& m
}
14. Evaluate the top of the stack to WHNF
.. math::
.. math::
\gmrule
{ \mathtt{Eval} : i
& a : s
@@ -291,11 +293,58 @@ Core Transition Rules
& m
}
#. Reduce a primitive binary operator :math:`*`.
.. math::
\gmrule
{ * : i
& a_1 : a_2 : s
& d
& h
\begin{bmatrix}
a_1 : x \\
a_2 : y
\end{bmatrix}
& m
}
{ i
& a' : s
& d
& h
\begin{bmatrix}
a' : (x * y)
\end{bmatrix}
& m
}
#. Reduce a primitive unary operator :math:`\neg`.
.. math::
\gmrule
{ \neg : i
& a : s
& d
& h
\begin{bmatrix}
a : x
\end{bmatrix}
& m
}
{ i
& a' : s
& d
& h
\begin{bmatrix}
a' : (\neg x)
\end{bmatrix}
& m
}
***************
Extension Rules
***************
1. A sneaky trick to enable sharing of :code:`NNum` nodes. We note that the
#. A sneaky trick to enable sharing of :code:`NNum` nodes. We note that the
global environment is a mapping of plain old strings to heap addresses.
Strings of digits are not considered valid identifiers, so putting them on
the global environment will never conflict with a supercombinator! We abuse
@@ -303,7 +352,7 @@ Extension Rules
node's address. Consider how this rule might impact garbage collection
(remember that the environment is intended for *globals*).
.. math::
.. math::
\gmrule
{ \mathtt{PushInt} \; n : i
& s
@@ -327,10 +376,10 @@ Extension Rules
\text{where $n'$ is the base-10 string rep. of $n$}
}
2. In order for Extension Rule 1. to be effective, we are also required to take
#. In order for the previous rule to be effective, we are also required to take
action when a number already exists in the environment:
.. math::
.. math::
\gmrule
{ \mathtt{PushInt} \; n : i
& s

188
src/GM.hs
View File

@@ -20,9 +20,9 @@ import Text.Printf
import Text.PrettyPrint hiding ((<>))
import Text.PrettyPrint.HughesPJ (maybeParens)
import Data.Foldable (traverse_)
import Debug.Trace
import Control.Arrow ((>>>))
import System.IO (Handle, hPutStrLn)
import Data.Heap as Heap
import Data.Heap
import Core
----------------------------------------------------------------------------------
@@ -52,8 +52,12 @@ data Instr = Unwind
| Pop Int
| Alloc Int
| Eval
-- primitive ops
| Neg
| Add
| Sub
| Mul
| Div
deriving (Show, Eq)
data Node = NNum Int
@@ -123,19 +127,25 @@ isFinal st = null $ st ^. gmCode
step :: GmState -> GmState
step st = case head (st ^. gmCode) of
Unwind -> unwind st
PushGlobal n -> pushGlobal n st
PushInt n -> pushInt n st
Push n -> push n st
MkAp -> mkAp st
Slide n -> slide n st
Pop n -> pop n st
Update n -> update n st
Alloc n -> alloc n st
Unwind -> unwindI st
PushGlobal n -> pushGlobalI n st
PushInt n -> pushIntI n st
Push n -> pushI n st
MkAp -> mkApI st
Slide n -> slideI n st
Pop n -> popI n st
Update n -> updateI n st
Alloc n -> allocI n st
Eval -> evalI st
Neg -> negI st
Add -> addI st
Sub -> subI st
Mul -> mulI st
Div -> divI st
where
pushGlobal :: Name -> GmState -> GmState
pushGlobal k st = st
pushGlobalI :: Name -> GmState -> GmState
pushGlobalI k st = st
& gmCode %~ drop 1
& gmStack .~ s'
where
@@ -147,8 +157,8 @@ step st = case head (st ^. gmCode) of
$ lookup k m
-- Extension Rules 1,2 (sharing)
pushInt :: Int -> GmState -> GmState
pushInt n st = case lookup n' m of
pushIntI :: Int -> GmState -> GmState
pushIntI n st = case lookup n' m of
Just a -> st
& gmCode %~ drop 1
& gmStack .~ s'
@@ -163,7 +173,7 @@ step st = case head (st ^. gmCode) of
& gmStats . stsAllocations %~ succ --
where
s' = a : s
(h',a) = Heap.alloc h (NNum n)
(h',a) = alloc h (NNum n)
m' = (n',a) : m
where
m = st ^. gmEnv
@@ -172,8 +182,8 @@ step st = case head (st ^. gmCode) of
n' = show n
-- Core Rule 2. (no sharing)
-- pushInt :: Int -> GmState -> GmState
-- pushInt n st = st
-- pushIntI :: Int -> GmState -> GmState
-- pushIntI n st = st
-- & gmCode %~ drop 1
-- & gmStack .~ s'
-- & gmHeap .~ h'
@@ -185,8 +195,8 @@ step st = case head (st ^. gmCode) of
-- s' = a : s
-- (h',a) = alloc h (NNum n)
mkAp :: GmState -> GmState
mkAp st = st
mkApI :: GmState -> GmState
mkApI st = st
& gmCode %~ drop 1
& gmStack .~ s'
& gmHeap .~ h'
@@ -197,12 +207,12 @@ step st = case head (st ^. gmCode) of
h = st ^. gmHeap
s' = a : ss
(h',a) = Heap.alloc h (NAp f x)
(h',a) = alloc h (NAp f x)
-- a `Push n` instruction pushes the address of (n+1)-th argument onto
-- the stack.
push :: Int -> GmState -> GmState
push n st = st
pushI :: Int -> GmState -> GmState
pushI n st = st
& gmCode %~ drop 1
& gmStack %~ (a:)
where
@@ -218,16 +228,16 @@ step st = case head (st ^. gmCode) of
-- 1: f 1: f x y
-- 2: f x
-- 3: f x y
slide :: Int -> GmState -> GmState
slide n st = st
slideI :: Int -> GmState -> GmState
slideI n st = st
& gmCode %~ drop 1
& gmStack .~ s'
where
(a:s) = st ^. gmStack
s' = a : drop n s
update :: Int -> GmState -> GmState
update n st = st
updateI :: Int -> GmState -> GmState
updateI n st = st
& gmCode %~ drop 1
& gmStack .~ s
& gmHeap .~ h'
@@ -235,15 +245,15 @@ step st = case head (st ^. gmCode) of
(e:s) = st ^. gmStack
an = s !! n
h' = st ^. gmHeap
& Heap.update an (NInd e)
& update an (NInd e)
pop :: Int -> GmState -> GmState
pop n st = st
popI :: Int -> GmState -> GmState
popI n st = st
& gmCode %~ drop 1
& gmStack %~ drop n
alloc :: Int -> GmState -> GmState
alloc n st = st
allocI :: Int -> GmState -> GmState
allocI n st = st
& gmCode %~ drop 1
& gmStack .~ s'
& gmHeap .~ h'
@@ -256,14 +266,47 @@ step st = case head (st ^. gmCode) of
allocNode :: Int -> GmHeap -> (GmHeap, [Addr])
allocNode 0 g = (g,[])
allocNode k g = allocNode (k-1) g' & _2 %~ (a:)
where (g',a) = Heap.alloc g NUninitialised
where (g',a) = alloc g NUninitialised
evalI :: GmState -> GmState
evalI st = st
-- Unwind performs the actual evaluation; we just set the stage
-- so Unwind knows what to do
& gmCode .~ [Unwind]
-- leave lone scrutinee on stk to be eval'd by Unwind
& gmStack .~ [a]
-- push remaining code & stk to dump
& gmDump %~ ((i,s):)
where
(_:i) = st ^. gmCode
(a:s) = st ^. gmStack
negI :: GmState -> GmState
negI = primitive1 boxInt unboxInt negate
addI, subI, mulI, divI :: GmState -> GmState
addI = primitive2 boxInt unboxInt (+)
subI = primitive2 boxInt unboxInt (-)
mulI = primitive2 boxInt unboxInt (*)
divI = primitive2 boxInt unboxInt div
-- the complex heart of the G-machine
unwind :: GmState -> GmState
unwind st = case hLookupUnsafe a h of
unwindI :: GmState -> GmState
unwindI st = case hLookupUnsafe a h of
NNum n -> st
-- halt; discard all further instructions
& gmCode .~ []
& gmCode .~ i'
& gmStack .~ s'
& gmDump .~ d'
where
s = st ^. gmStack
(i',s',d') = case st ^. gmDump of
-- if the dump is non-empty, restore the instruction
-- queue and stack, and pop the dump
((ii,ss):d) -> (ii,a:ss,d)
-- if the dump is empty, clear the instruction queue and
-- leave the stack as is
[] -> ([], s, [])
NAp f x -> st
-- leave the Unwind instr; continue unwinding
& gmStack %~ (f:)
@@ -293,6 +336,56 @@ step st = case head (st ^. gmCode) of
a = head s
h = st ^. gmHeap
-- TODO: this desperately needs documentation
primitive1 :: (GmState -> b -> GmState) -- boxing function
-> (Addr -> GmState -> a) -- unboxing function
-> (a -> b) -- operator
-> GmState -> GmState -- state transition
primitive1 box unbox f st
= st
& unbox a
& f
& box (st & gmStack .~ s)
& advanceCode
where
putNewStack = gmStack .~ s
(a:s) = st ^. gmStack
r = box (putNewStack st) (f (unbox a st))
-- TODO: this desperately needs documentation
primitive2 :: (GmState -> b -> GmState) -- boxing function
-> (Addr -> GmState -> a) -- unboxing function
-> (a -> a -> b) -- operator
-> GmState -> GmState -- state transition
primitive2 box unbox f st
= st'
& advanceCode
where
(ax:ay:s) = st ^. gmStack
putNewStack = gmStack .~ s
x = unbox ax st
y = unbox ay st
st' = box (putNewStack st) (f x y)
boxInt :: GmState -> Int -> GmState
boxInt st n = st
& gmHeap .~ h'
& gmStack %~ (a:)
where
h = st ^. gmHeap
(h',a) = alloc h (NNum n)
unboxInt :: Addr -> GmState -> Int
unboxInt a st = case hLookup a h of
Just (NNum n) -> n
Just _ -> error "unboxInt received a non-int"
Nothing -> error "unboxInt received an invalid address"
where h = st ^. gmHeap
advanceCode :: GmState -> GmState
advanceCode = gmCode %~ drop 1
----------------------------------------------------------------------------------
compile :: Program -> GmState
@@ -305,10 +398,25 @@ compile p = GmState c [] [] h g sts
type CompiledSC = (Name, Int, Code)
buildInitialHeap :: Program -> (GmHeap, Env)
buildInitialHeap (Program ss) = mapAccumL allocateSc mempty compiled
compiledPrims :: [CompiledSC]
compiledPrims =
[ ("whnf#", 1, [Push 0, Eval, Update 1, Pop 1, Unwind])
-- , unop "negate#" Neg
, ("negate#", 1, [Push 0, Eval, Neg, Update 1, Pop 1, Unwind])
, binop "+#" Add
, binop "-#" Sub
, binop "*#" Mul
, binop "/#" Div
]
where
compiled = fmap compileSc ss
unop k i = (k, 1, [Push 0, Eval, i, Update 1, Pop 1, Unwind])
binop k i = (k, 2, [Push 1, Eval, Push 1, Eval, i, Update 2, Pop 2, Unwind])
buildInitialHeap :: Program -> (GmHeap, Env)
buildInitialHeap (Program ss) = mapAccumL allocateSc mempty compiledScs
where
compiledScs = fmap compileSc ss <> compiledPrims
-- note that we don't count sc allocations in the stats
allocateSc :: GmHeap -> CompiledSC -> (GmHeap, (Name, Addr))