# Definition

PLAN is a combinator interpreter. It is defined by the following pseudocode:

```
Every PLAN vaue is either a pin x:<i>, a law x:{n a b}, an app x:(f g), a
nat x:@, or a black hole x:<>.  Black holes only exist during evaluation.

(o <- x) mutates o in place, replacing it's value with x.

Run F(x) to normalize a value.

E(o:@)     = o                          | F(o) =
E(o:<x>)   = o                          |     E(o)
E(o:(f x)) =                            |     when o:(f x)
    E(f)                                |          F(f); F(x)
    when A(f)=1                         |     o
        o <- X(o,o)                     |
        E(o)                            | N(o) = E(o); if o:@ then o else 0
    o                                   |
E(o:{n a b}) =                          | I(f, (e x), 0) = x
    if a!=0 then o else                 | I(f, e,     0) = e
        o <- <>                         | I(f, (e x), n) = I(f, e, n-1)
        o <- R(0,o,b)                   | I(f, e,     n) = f
        E(o)                            |
                                        | A((f x))     = A(f)-1
X((f x), e)         = X(f,e)            | A(<p>)       = A(p)
X(<p>, e)           = X(p,e)            | A({n a b})   = a
X({n a b}, e)       = R(a,e,b)          | A(n:@)       = I(1, (3 5 3), n)
X(0, (_ n a b))     = {N(n) N(a) F(b)}  |
X(1, (_ p l a n x)) = P(p,l,a,n,E(x))   | R(n,e,b:@) | b≤n = I(x,e,(n-b))
X(2, (_ z p x))     = C(z,p,N(x))       | R(n,e,(0 f x))   = (R(n,e,f) R(n,e,x))
X(3, (_ x))         = N(x)+1            | R(n,e,(1 v b))   = L(n,e,v,b)
X(4, (_ x))         = <F(x)>            | R(n,e,(2 x))     = x
                                        | R(n,e,x)         = x
C(z,p,n) = if n=0 then z else (p (n-1)) |
                                        | L(n,e,v,b) =
P(p,l,a,n,(f x))   = (a f x)            |     x := <>
P(p,l,a,n,<x>)     = (p x)              |     f := (e x)
P(p,l,a,n,{n a b}) = (l n a b)          |     x <- R(n+1,f,v)
P(p,l,a,n,x:@}     = (n x)              |     R(n+1,f,b)
```

A Haskell implementation is about 180 lines, with examples:

```haskell
import Control.DeepSeq
import Numeric.Natural
import Data.List

data Val
    = PIN !Val
    | LAW !Natural !Natural !Val
    | APP !Val Val
    | NAT !Natural

instance NFData Val where
  rnf (APP f x) = rnf f `seq` rnf x
  rnf _         = ()

f % x | arity f == 1 = subst f [x]
f % x | otherwise    = APP f x

arity (APP f _)     = arity f - 1
arity (PIN (NAT n)) = case n of 1->3; 3->3; 4->5; _->1
arity (PIN i)       = arity i
arity (LAW _ a _)   = fromIntegral a :: Integer
arity (NAT n)       = 0

pat p _ _ _ (PIN x)     = (p % x)
pat _ l _ _ (LAW n a b) = (l % NAT n % NAT a % b)
pat _ _ a _ (APP f x)   = (a % f % x)
pat _ _ _ n x@NAT{}     = (n % x)

kal n e (NAT b) | b<=n          = e !! fromIntegral (n-b)
kal n e (NAT 0 `APP` f `APP` x) = (kal n e f % kal n e x)
kal _ _ (NAT 2 `APP` x)         = x
kal _ _ x                       = x

run :: Natural -> [Val] -> Val -> Val
run arity ie body = res
  where (n, e, res::Val) = go arity ie body
        go i acc (NAT 1 `APP` v `APP` k') = go (i+1) (kal n e v : acc) k'
        go i acc x                        = (i, acc, kal n e x)

subst (APP f x)       xs = subst f (x:xs)
subst x@(PIN l@LAW{}) xs = exec l (x:xs)
subst (PIN i)         xs = subst i xs
subst x               xs = exec x (x:xs)

nat (NAT n) = n
nat _       = 0

exec (LAW n a b) xs                    = run a (reverse xs) b
exec (NAT 0)     [_,x]                 = PIN (force x)
exec (NAT 1)     [_,n,a,b] | nat a > 0 = LAW (nat n) (nat a) (force b)
exec (NAT 2)     [_,x]                 = NAT (nat x + 1)
exec (NAT 3)     [_,z,p,x]             = case nat x of 0->z; n->(p % NAT (n-1))
exec (NAT 4)     [_,p,l,a,n,x]         = pat p l a n x
exec f           e                     = error $ show ("crash", (f:e))


-- Some Examples ---------------------------------------------------------------

instance Num Val where fromInteger i = NAT (fromIntegral i)

showApp (APP f x) xs = showApp f (x:xs)
showApp f         xs = "(" <> intercalate " " (show <$> (f:xs)) <> ")"

instance Show Val where
    show (PIN i)     = concat ["<", show i, ">"]
    show (LAW n a b) = concat ["{", show n, " ", show a, " ", show b, "}"]
    show (APP f x)   = showApp f [x]
    show (NAT n)     = show n

pin=(PIN 0)
law=(PIN 1)
inc=(PIN 2)
natCase=(PIN 3)
planCase=(PIN 4)

k  = law % 0 % 2 % 1        --  k a _ = a
k3 = law % 0 % 4 % 1        --  k3 v _ _ _ = v
i  = law % 0 % 1 % 1        --  i x = x
z1 = law % 0 % 1 % (2 % 0)  --  z1 _ = 0
z3 = law % 0 % 3 % (2 % 0)  --  z3 _ _ _ = 0

appHead=(planCase % 0 % 0 % k % 0)
toNat=(natCase % 0 % inc)
dec=(natCase % 0 % i)

-- helpers for building laws
a f x = (0 % f % x)
lawE n a b = (law % n % a % b)

-- length of an array
--
--     lenHelp len h t = inc (len h)
--     len x = planCase z1 z3 (\len h t -> inc (len h))  n x
lenHelp = lawE 0 3 (inc `a` (1 `a` 2))
len = lawE 0 1 (((planCase % z1 % z3) `a` (lenHelp `a` 0)) `a` z1 `a` 1)

-- getting the tag of an ADT:
--
-- head (APP h t) = h
-- head x         = x
--
-- tag x = toNat (head x)
head' = lawE 0 3 (1 `a` 2)    -- \head h t -> head h
headF = lawE 0 1 (planCase `a` (k `a` 1) `a` (k3 `a` 1) `a` (head' `a` 0) `a` i `a` 1)
tag   = lawE 0 1 (toNat `a` (headF `a` 1))

chk :: Val -> Val -> IO ()
chk x y = do
    putStrLn ("assert " <> show x <> " " <> show y)
    if (x == y) then pure () else error "FAIL"

deriving instance Eq Val

main = do
    -- increment, make a law, make a pin
    chk 5           $ inc % 4
    chk (LAW 1 2 3) $ law % 1 % 2 % 3
    chk (PIN 5)     $ pin % (inc % 4)

    -- pattern match on nats
    chk 9 $ toNat % 9

    chk 0 $ toNat % (pin % 9)

    -- pattern match on PLAN values
    chk (1%2)     (planCase % 1 % 0 % 0 % 0 % (pin%2))
    chk (1%2%3%4) (planCase % 0 % 1 % 0 % 0 % (law%2%3%4))
    chk (1%2%3)   (planCase % 0 % 0 % 1 % 0 % (2%3))
    chk (1%2)     (planCase % 0 % 0 % 0 % 1 % 2)

    -- basic laws
    chk (LAW 0 2 0) $ law % 0 % 2 % 0 % 7 % 8
    chk 7           $ law % 0 % 2 % 1 % 7 % 8
    chk 8           $ law % 0 % 2 % 2 % 7 % 8
    chk 3           $ law % 0 % 2 % 3 % 7 % 8

    -- force a value by using it to build a law and the running it.
    chk 1 (law % 0 % 1 % (2 % 1) % 0)

    -- select finite part of infinite value
    chk 1 (appHead % (law % 99 % 1 % (1 % (0%1%2) % 2) % 1))

    -- running pins:
    chk (LAW 1 2 0)      $ pin % law % 1 % 2 % 0
    chk (LAW 1 2 0)      $ pin % (law%1) % 2 % 0
    chk (PIN(LAW 1 2 0)) $ pin % (law%1%2%0) % 3 % 4
    chk (PIN(LAW 1 2 0)) $ pin % (pin % (law%1%2%0)) % 3 % 4

    chk 9 ( law % 0 % 1 % 1 % 9 )
    chk 8 ( law % 0 % 1 % (1 % 1 % 2) % 8 )

    chk 7 ( law % 0 % 1 %  --  ? ($0 $1)
               (1 % 3 %    --  @ $2 = $3
               (1 % 7 %    --  @ $3 = 9
               2))         --  $2
           % 9)

    -- more complex example
    chk (1%(0%2))
             (law%0%1%           --   | ? ($0 $1)
               (1% (0%(2%0)%3)%  --     @ $2 = (0 $3)
               (1% (2%2)%        --     @ $3 = 2
                (0%1%2)))%       --     | ($1 $2)
             1)                  --   1

    -- trivial cycles are okay if not used.
    chk 7 ( (law % 0 % 1 %  --   | ? ($0 $1)
              (1% 7%        --     @ $2 = 7
              (1% 3%        --     @ $3 = $3
                            --     $2
               2))%         --   9
            9))

    -- length of array
    chk 9 (len % (0 % 1 % 2 % 3 % 4 % 5 % 6 % 7 % 8 % 9))

    -- head of closure
    chk 7   (headF % (7 % 1 % 2 % 3 % 4 % 5 % 6 % 7 % 8 % 9))
    chk law (headF % (law % 1 % 2))

    -- tag of ADT (head cast to nat)
    chk 7 (tag % (7 % 1 % 2 % 3 % 4 % 5 % 6 % 7 % 8 % 9))
    chk 0 (tag % (law % 1 % 2))
```


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://opfn.gitbook.io/pallas/plan/definition.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.