Haskell Type-level Mini Interpreter

mini_interpreter.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Type.Bool (If)
import Data.Type.Equality (type (==))
import GHC.TypeLits

import Data.Symbol.Ascii

type family Reverse (xs :: [k]) :: [k] where
  Reverse xs = Reverse1 '[] xs

type family Reverse1 (reversed :: [k]) (xs :: [k]) where
  Reverse1 reversed      '[]  = reversed
  Reverse1 reversed (x ': xs) = Reverse1 (x ': reversed) xs

type family Tokenize (sym :: Symbol) :: [Symbol] where
  Tokenize sym = Tokenize1 '[] "" (ToList sym)

type family Tokenize1 (tokens :: [Symbol]) (digits :: Symbol) (syms :: [Symbol]) :: [Symbol] where
  Tokenize1 tokens digits '[]           = Reverse   (If (digits == "")         tokens         (digits ': tokens))
  Tokenize1 tokens digits (" " ': syms) = Tokenize1 (If (digits == "")         tokens         (digits ': tokens)) "" syms
  Tokenize1 tokens digits ("+" ': syms) = Tokenize1 (If (digits == "") ("+" ': tokens) ("+" ': digits ': tokens)) "" syms
  Tokenize1 tokens digits ("*" ': syms) = Tokenize1 (If (digits == "") ("*" ': tokens) ("*" ': digits ': tokens)) "" syms
  Tokenize1 tokens digits ("(" ': syms) = Tokenize1 (If (digits == "") ("(" ': tokens) ("(" ': digits ': tokens)) "" syms
  Tokenize1 tokens digits (")" ': syms) = Tokenize1 (If (digits == "") (")" ': tokens) (")" ': digits ': tokens)) "" syms
  Tokenize1 tokens digits (sym ': syms) = Tokenize1 tokens (AppendSymbol digits sym) syms

type family EvalRPN (syms :: [Symbol]) :: Nat where
  EvalRPN syms = EvalRPN1 '[] syms

type family EvalRPN1 (stack :: [Nat]) (syms :: [Symbol]) :: Nat where
  EvalRPN1      (x ': stack)          '[]  = x
  EvalRPN1 (x ': y ': stack) ("+" ': syms) = EvalRPN1       (x + y ': stack) syms
  EvalRPN1 (x ': y ': stack) ("*" ': syms) = EvalRPN1       (x * y ': stack) syms
  EvalRPN1            stack  (sym ': syms) = EvalRPN1 (ReadNat sym ': stack) syms

type family ShuntingYard (xs :: [Symbol]) :: [Symbol] where
  ShuntingYard xs = ShuntingYard1 '[] '[] xs

type family ShuntingYard1 (output :: [Symbol]) (operators :: [Symbol]) (input :: [Symbol]) :: [Symbol] where
  ShuntingYard1 output '[]                '[]            = Reverse output
  ShuntingYard1 output (sym ': operators) '[]            = ShuntingYard1 (sym ': output)         operators          '[]
  ShuntingYard1 output ("*" ': operators) ("+" ': input) = ShuntingYard1 ("*" ': output)         operators  ("+" ': input)
  ShuntingYard1 output ("+" ': operators) ("+" ': input) = ShuntingYard1 ("+" ': output)         operators  ("+" ': input)
  ShuntingYard1 output         operators  ("+" ': input) = ShuntingYard1         output  ("+" ': operators)         input
  ShuntingYard1 output         operators  ("*" ': input) = ShuntingYard1         output  ("*" ': operators)         input
  ShuntingYard1 output         operators  ("(" ': input) = ShuntingYard1         output  ("(" ': operators)         input
  ShuntingYard1 output ("(" ': operators) (")" ': input) = ShuntingYard1         output          operators          input
  ShuntingYard1 output (sym ': operators) (")" ': input) = ShuntingYard1 (sym ': output)         operators  (")" ': input)
  ShuntingYard1 output         operators  (sym ': input) = ShuntingYard1 (sym ': output)         operators          input

type Calc xs = EvalRPN (ShuntingYard (Tokenize xs))

> :kind! Calc "(1 + 20) * 300"
Calc "(1 + 20) * 300" :: Nat
= 6300

> :kind! Calc "(1 + 1) * (2 + 0) + 10"
Calc "(1 + 1) * (2 + 0) + 10" :: Nat
= 14