Typesafe rewriting patterns example

P.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Rewriting.P where

import Data.Type.Bool

data Pattern vars where
  Var :: V n -> Pattern '[n]
  Fn :: String -> All Pattern varss -> Pattern (Concat varss)

data Rule where
  (:==>) :: (Subset us vs ~ 'True) => Pattern vs -> Pattern us -> Rule

data All f xs where
  Nil :: All f '[]
  (:+) :: f x -> All f xs -> All f (x ': xs)

infixr 4 :+

mapToList :: forall f xs b. (forall a. f a -> b) -> All f xs -> [b]
mapToList f Nil = []
mapToList f (l :+ ls) = f l : mapToList f ls

type family Concat (xss :: [[k]]) :: [k] where
  Concat '[] = '[]
  Concat (xs ': xss) = xs ++ Concat xss

type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

type family Elem (x :: k) (xs :: [k]) :: Bool where
  Elem x '[] = 'False
  Elem x (x ': ys) = 'True
  Elem x (y ': ys) = Elem x ys

type family Subset (xs :: [k]) (ys :: [k]) :: Bool where
  Subset '[] ys = 'True
  Subset (x ': xs) ys = Elem x ys && Subset xs ys

data Nat = Zero | Succ Nat

data SNat :: Nat -> * where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

newtype V (n :: Nat) = V (SNat n)

snatToInt :: forall (n :: Nat). SNat n -> Int
snatToInt SZero = 0
snatToInt (SSucc n) = 1 + snatToInt n

x0 :: V Zero
x0 = V SZero

x1 :: V (Succ Zero)
x1 = V (SSucc SZero)

x2 :: V (Succ (Succ Zero))
x2 = V (SSucc (SSucc SZero))

r1 :: Rule
r1 = Fn "-" (Var x0 :+ Var x0 :+ Nil) :==> Fn "0" Nil

ww = Fn "+" (Var x0 :+ Fn "+" (Var x1 :+ Var x2 :+ Nil) :+ Nil)

qq = Fn "+" (Var x2 :+ Var x1 :+ Var x0 :+ Var x0 :+ Nil)

r2 :: Rule
r2 = Fn "+" (Var x0 :+ Fn "+" (Var x1 :+ Var x2 :+ Nil) :+ Nil) :==> Fn "+" (Var x2 :+ Var x1 :+ Var x0 :+ Var x0 :+ Nil)

data Sexp where
  SVar :: Int -> Sexp
  SFn :: String -> [Sexp] -> Sexp
  deriving (Show, Eq)

toSexp :: Pattern vars -> Sexp
toSexp (Var (V x)) = SVar (snatToInt x)
toSexp (Fn f ps) = SFn f (mapToList toSexp ps)

ruleToSexp (lhs :==> rhs) = (toSexp lhs, toSexp rhs)

r1Sexp = ruleToSexp r1

r2Sexp = ruleToSexp r2

-- Example of invalid rule
-- Error: "Couldn't match type 'False' with 'True'"
-- r3 :: Rule
-- r3 = Fn "+" (Var x0 :+ Fn "+" (Var x1 :+ Nil) :+ Nil) :==> Fn "+" (Var x0 :+ Var x1 :+ Var x2 :+ Nil)