Skip to content

Instantly share code, notes, and snippets.

@oisdk

oisdk/dyck.hs Secret

Last active Dec 14, 2020
Embed
What would you like to do?
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# OPTIONS_GHC -Wall -fno-warn-unticked-promoted-constructors #-}
import Data.Kind (Type)
import Data.Foldable (foldlM,foldrM)
import Data.List (inits,tails)
data Nat = Z | S Nat
data DyckSuff (n :: Nat) :: Type where
Done :: DyckSuff Z
Open :: DyckSuff (S n) -> DyckSuff n
Clos :: DyckSuff n -> DyckSuff (S n)
type Dyck = DyckSuff Z
deriving instance Eq (DyckSuff n)
deriving instance Ord (DyckSuff n)
instance Show (DyckSuff n) where
showsPrec _ xs' = showChar '\"' . toString xs'
where
toString :: DyckSuff n -> String -> String
toString Done = showChar '\"'
toString (Open xs) = showChar '(' . toString xs
toString (Clos xs) = showChar ')' . toString xs
data Natty (n :: Nat) :: Type where
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)
enumDyck :: Int -> [Dyck]
enumDyck sz = go Zy sz Done []
where
go, zero, left, right :: Natty n -> Int -> DyckSuff n -> [Dyck] -> [Dyck]
go n m k = zero n m k . left n m k . right n m k
zero Zy 0 k = (k:)
zero _ _ _ = id
left (Sy n) m k = go n m (Open k)
left Zy _ _ = id
right _ 0 _ = id
right n m k = go (Sy n) (m-1) (Clos k)
infixr 5 :-
data Stack (a :: Type) (n :: Nat) :: Type where
Nil :: Stack a Z
(:-) :: a -> Stack a n -> Stack a (S n)
data Tree = Leaf | Tree :*: Tree deriving (Eq, Ord, Show)
dyckToTree :: Dyck -> Tree
dyckToTree dy = go dy (Leaf :- Nil)
where
go :: DyckSuff n -> Stack Tree (S n) -> Tree
go (Open d) ts = go d (Leaf :- ts)
go (Clos d) (t1 :- t2 :- ts) = go d (t2 :*: t1 :- ts)
go Done (t :- Nil) = t
treeToDyck :: Tree -> Dyck
treeToDyck t = go t Done
where
go :: Tree -> DyckSuff n -> DyckSuff n
go Leaf = id
go (xs :*: ys) = go xs . Open . go ys . Clos
data Expr (a :: Type) where
Val :: a -> Expr a
(:+:) :: Expr a -> Expr a -> Expr a
data Code (n :: Nat) (a :: Type) :: Type where
HALT :: Code (S Z) a
PUSH :: a -> Code (S n) a -> Code n a
ADD :: Code (S n) a -> Code (S (S n)) a
type family (+) (n :: Nat) (m :: Nat) :: Nat where
Z + m = m
S n + m = S (n + m)
exec :: Code n Int -> Stack Int (n + m) -> Stack Int (S m)
exec HALT st = st
exec (PUSH v is) st = exec is (v :- st)
exec (ADD is) (t1 :- t2 :- st) = exec is (t2 + t1 :- st)
comp :: Expr a -> Code Z a
comp e = comp' e HALT
where
comp' :: Expr a -> Code (S n) a -> Code n a
comp' (Val x) = PUSH x
comp' (xs :+: ys) = comp' xs . comp' ys . ADD
foldlCode :: ( n. a -> b n -> b (S n))
-> ( n. b (S (S n)) -> b (S n))
-> b m
-> Code m a -> b (S Z)
foldlCode _ _ h HALT = h
foldlCode p a h (PUSH x xs) = foldlCode p a (p x h) xs
foldlCode p a h (ADD xs) = foldlCode p a (a h) xs
shift :: Int -> Stack Int n -> Stack Int (S n)
shift x xs = x :- xs
reduce :: Stack Int (S (S n)) -> Stack Int (S n)
reduce (t1 :- t2 :- st) = t2 + t1 :- st
execFold :: Code Z Int -> Int
execFold = pop . foldlCode shift reduce Nil
pop :: Stack a (S n) -> a
pop (x :- _) = x
enumTrees :: [a] -> [Expr a]
enumTrees = fmap (foldl1 (flip (:+:))) . foldlM f []
where
f [] v = [[Val v]]
f [t1] v = [[Val v, t1]]
f (t1:t2:st) v = (Val v : t1 : t2 : st) : f ((t2 :+: t1) : st) v
data Rose a = a :& Forest a
type Forest a = [Rose a]
dyckToForest :: Dyck -> Forest ()
dyckToForest dy = go dy ([] :- Nil)
where
go :: DyckSuff n -> Stack (Forest ()) (S n) -> Forest ()
go (Open d) ts = go d ([] :- ts)
go (Clos d) (t1 :- t2 :- ts) = go d ((() :& t2 : t1) :- ts)
go Done (t :- Nil) = t
forestToDyck :: Forest () -> Dyck
forestToDyck t = go t Done
where
go :: Forest () -> DyckSuff n -> DyckSuff n
go [] = id
go ((() :& x):xs) = go x . Open . go xs . Clos
enumForests :: [a] -> [Forest a]
enumForests = foldrM f []
where
f x xs = zipWith ((:) . (:&) x) (inits xs) (tails xs)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.