TODO: Look at when on laptop

Code.markdown

https://github.com/phadej/metametapost/tree/34eb0d757655d15317d58f549e9cf4c794cff79e/src/MetaMetaPost

• https://github.com/phadej/metametapost/blob/34eb0d757655d15317d58f549e9cf4c794cff79e/src/MetaMetaPost/Simplifier.hs

simplify :: Expr SomePrim (Type s) a -> Either String (MP s a)
simplify (Var a)                = pure (MPApp (MPVar a))
simplify (Prim (SomePrim p))    = simplifyPrim0 p
simplify (Lam _ _)              = throwError "Non-applied lambda abstraction"
simplify (Let (TyScalar s) e b) = mpLet s <$> simplify e <*> transverseScope simplify b
simplify (Let (_ :-> _) e b)    = simplify (instantiate1 e b)
simplify (App f x)              = case whnf f of
    Lam _ b                   -> simplify (instantiate1 x b)
    Prim (SomePrim p)         -> simplifyPrim1 p x
    App (Prim (SomePrim p)) y -> simplifyPrim2 p y x
    _                         -> throwError $ "Non-primitive application"
 
-- ...

simplifyPrim2 :: forall arity s a. IArity arity
                => Prim arity
                -> Expr SomePrim (Type s) a
                -> Expr SomePrim (Type s) a
                -> Either String (MP s a)
simplifyPrim2 p x y = case iarity :: SArity arity of
    Arity0 -> throwError $ "Application of 0-arity primitive: " ++ show p
    Arity1 -> throwError $ "Over-application of 1-arity primitive: " ++ show p
    Arity2 -> (\x' y' -> floatTop (MPApp2 p (pure x') (pure y')))
        <$> simplify x
        <*> simplify y

TODO

Something like

data Exp :: Type -> Type where
  I :: Int -> Exp Int
  T :: Exp Bool
  F :: Exp Bool
  A :: Exp Int -> Exp Int -> Exp Int

class    Elem a where
instance Elem Int
instance Elem Bool

specialElimExp :: Exp a -> ((Eq a, Show a) => r) -> r
specialElimE = \case
  I i ->  ...

and then create, not only

pattern Eval :: a -> Exp a
pattern Eval a <- (eval -> e)
  where Eval a =

gah never mind, I wanted

pattern Eval :: (Eq a, Show a) => () => a -> Expr a

https://pdfs.semanticscholar.org/bc0d/09a0807399cf0a8f3c1f3c37063bfb45fa9f.pdf

The data type STM implements data constructors for all STM-operations, where continuations
corresponding to the >>=-operator for sequencing are packed into the constructors.

data STM a = Return a
  | Retry
  | ∀ b. NewTVar b (TVar b → STM a)
  | ∀ b. ReadTVar (TVar b) (b → STM a)
  | ∀ b. WriteTVar (TVar b) b (STM a)
  | ∀ b. OrElse (STM b) (STM b) (b → STM a)

The STM-operations generate the corresponding data, and the monad instance for the type
STM is implemented straightforward, where the bind-operator >>= combines the actions:

newTVar :: a → STM (TVar a) writeTVar :: TVar a → a → STM ()
newTVar a = NewTVar a return writeTVar v x = WriteTVar v x (return ())

readTVar :: TVar a → STM a
readTVar a = ReadTVar a return

orElse :: STM a → STM a → STM a
orElse a1 a2 = OrElse a1 a2 return

retry :: STM a 
retry = Retry

instance Monad STM where
  return = Return

  m >>= f = case m of 
    Return x → f x
    Retry → Retry
    NewTVar x ct → NewTVar x (λi → ct >>= f)
    ReadTVar x ct → ReadTVar x (λi → ct >>= f)
    WriteTVar v x ct → WriteTVar v x (ct >>= f)
    OrElse a1 a2 ct → OrElse a1 a2 (λi → ct >>= f)