{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Type.Zipper -- Copyright : (C) 2016 Csongor Kiss -- License : BSD3 -- Maintainer : Csongor Kiss <kiss.csongor.kiss@gmail.com> -- Stability : experimental -- Portability : non-portable -- -- The list zipper data structure with a focused element (at the type-level). -- -- Used for storing the registers and the instructions because of -- its performance benefits. -- ----------------------------------------------------------------------------- module Data.Type.Zipper where import GHC.TypeLits -- |Polymorphic list zipper. -- -- Some functions that operate on Zippers are partial. -- Instead of having to mess with promoted Maybes and whatnot, this -- constructor represent an erroneous operation. data Zipper a where Zip :: [a] -> a -> [a] -> Zipper a Invalid :: Zipper a -- |Construct `Zipper a` from `[a]`. -- The list must contain at least one element for the Zipper to be valid. -- The resulting Zipper focuses on the first element of the list, -- the tail of the list is found to the right. type family FromList (xs :: [k]) :: Zipper k where FromList '[] = 'Invalid FromList (x ': xs) = 'Zip '[] x xs -- |Extract the focused element. type family Extract (zipper :: Zipper k) :: k where Extract ('Zip p c n) = c -- |Replace the focused element with a new one. type family Replace (zipper :: Zipper k) (with :: k) :: Zipper k where Replace ('Zip p c n) with = 'Zip p with n -- |Create a list from the Zipper by appending together the left lift, the -- focused element and the right list in this order. type family ToList (zipper :: Zipper k) :: [k] where ToList ('Zip '[] e n) = e ': n ToList ('Zip (p ': ps) e n) = ToList ('Zip ps p (e ': n)) -- |Shift the focus to the left type family Left (by :: Nat) (zipper :: Zipper k) :: Zipper k where Left 0 z = z Left n ('Zip (p ': prevs) cur next) = Left (n - 1) ('Zip prevs p (cur ': next)) Left n z = 'Invalid -- |Shift the focus to the right type family Right (by :: Nat) (zipper :: Zipper k) :: Zipper k where Right 0 z = z Right by ('Zip prevs cur (n ': next)) = Right (by - 1) ('Zip (cur ': prevs) n next) Right n z = 'Invalid