Spec.hs

module Language.Nock5K.Spec where
import Control.Monad.Instances

-- * Structures
{-| #spec-l3#
  A noun is an atom or a cell.  An atom is any natural number.
  A cell is an ordered pair of nouns.
-}
data Noun = Atom !Integer | !Noun :- !Noun deriving (Eq)

-- | Monad representing either a computed result or an error message.
type Nock = Either String

-- * Reductions
nock, wut, lus, tis, fas, tar :: Noun -> Nock Noun

{-| #spec-l8#

@
  nock(a)           *a
@-}
nock = tar

{- spec-l9
  [a b c]           [a [b c]]
-}
infixr 1 :-

{-| #spec-l11#

@
  ?[a b]            0
  ?a                1
@-}
wut (a :- b)  = return $ Atom 0
wut a         = return $ Atom 1

{-| #spec-l13#

@
  +[a b]            +[a b]
  +a                1 + a
@-}
lus (a :- b)  = Left "+[a b]"
lus (Atom a)  = return $ Atom (1 + a)

{-| #spec-l15#

@
  =[a a]            0
  =[a b]            1
  =a                =a
@-}
tis (a :- a') | a == a'  = return $ Atom 0
tis (a :- b)             = return $ Atom 1
tis a                    = Left "=a"

{-| #spec-l19#

@
  \/[1 a]            a
  \/[2 a b]          a
  \/[3 a b]          b
  \/[(a + a) b]      \/[2 \/[a b]]
  \/[(a + a + 1) b]  \/[3 \/[a b]]
  \/a                \/a
@-}
fas (Atom 1 :- a)          = return a
fas (Atom 2 :- a :- b)     = return a
fas (Atom 3 :- a :- b)     = return b
fas (Atom a :- b) | a > 3  = do  x <- fas $ Atom (a `div` 2) :- b
                                 fas $ Atom (2 + (a `mod` 2)) :- x
fas a                      = Left "/a"

{-| #spec-l26#

@
  \*[a [b c] d]      [\*[a b c] \*[a d]]

\  \*[a 0 b]          \/[b a]
  \*[a 1 b]          b
  \*[a 2 b c]        \*[\*[a b] \*[a c]]
  \*[a 3 b]          ?\*[a b]
  \*[a 4 b]          +\*[a b]
  \*[a 5 b]          =\*[a b]

\  \*[a 6 b c d]      \*[a 2 [0 1] 2 [1 c d] [1 0] 2 [1 2 3] [1 0] 4 4 b]
  \*[a 7 b c]        \*[a 2 b 1 c]
  \*[a 8 b c]        \*[a 7 [[7 [0 1] b] 0 1] c]
  \*[a 9 b c]        \*[a 7 c 2 [0 1] 0 b]
  \*[a 10 [b c] d]   \*[a 8 c 7 [0 3] d]
  \*[a 10 b c]       \*[a c]

\  \*a                \*a
@-}
tar (a :- (b :- c) :- d)             = do x <- tar (a :- b :- c)
                                          y <- tar (a :- d)
                                          return $ x :- y

tar (a :- Atom 0 :- b)               = fas $ b :- a
tar (a :- Atom 1 :- b)               = return b
tar (a :- Atom 2 :- b :- c)          = do  x <- tar (a :- b)
                                           y <- tar (a :- c)
                                           tar $ x :- y
tar (a :- Atom 3 :- b)               = tar (a :- b) >>= wut
tar (a :- Atom 4 :- b)               = tar (a :- b) >>= lus
tar (a :- Atom 5 :- b)               = tar (a :- b) >>= tis

tar (a :- Atom 6 :- b :- c :- d)     = tar (a :- Atom 2 :- (Atom 0 :- Atom 1) :-
                                            Atom 2 :- (Atom 1 :- c :- d) :-
                                            (Atom 1 :- Atom 0) :- Atom 2 :-
                                            (Atom 1 :- Atom 2 :- Atom 3) :-
                                            (Atom 1 :- Atom 0) :- Atom 4 :-
                                            Atom 4 :- b)
tar (a :- Atom 7 :- b :- c)          = tar (a :- Atom 2 :- b :- Atom 1 :- c)
tar (a :- Atom 8 :- b :- c)          = tar (a :- Atom 7 :-
                                            ((Atom 7 :- (Atom 0 :- Atom 1) :- b) :-
                                             Atom 0 :- Atom 1) :- c)
tar (a :- Atom 9 :- b :- c)          = tar (a :- Atom 7 :- c :- Atom 2 :-
                                            (Atom 0 :- Atom 1) :- Atom 0 :- b)
tar (a :- Atom 10 :- (b :- c) :- d)  = tar (a :- Atom 8 :- c :- Atom 7 :-
                                            (Atom 0 :- Atom 3) :- d)
tar (a :- Atom 10 :- b :- c)         = tar (a :- c)

tar a                                = Left "*a"