packages feed

she 0.0 → 0.1

raw patch · 17 files changed

+836/−171 lines, 17 filesdep ~basedep ~mtl

Dependency ranges changed: base, mtl

Files

+ examples/Binding.lhs view
@@ -0,0 +1,44 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies #-}++> module Binding where++> import Control.Applicative++> import ShePrelude++> data Tm+>   = V Int+>   | L Tm+>   | Tm :$ Tm+>   deriving Show++> infixl 6 :$++> data Va+>   = F (Va -> Va)+>   | [Va] :- Int    -- backwards++> ($$) :: Va -> Va -> Va+> F f $$ v = f v+> (vs :- p) $$ v = (v : vs) :- p++> ev :: Tm -> [Va] -> Va+> ev (V i)     g = g !! i+> ev (L t)     g = F (\ v -> ev t (v : g))+> ev (f :$ s)  g = (|ev f $$ ev s|) g++> qu :: Int -> Va -> Tm+> qu i (F f)     = L (qu (i + 1) (f ([] :- i)))+> qu i (vs :- j) = foldr (flip (:$)) (V (i - j - 1)) (map (qu i) vs)++> zz :: Tm+> zz = L [.f. L [.x. V x]]+> ss :: Tm+> ss = L [.n. L [.f. L [.x. V f :$ (V n :$ V f :$ V x)]]]++> test3 :: Va+> test3 = ev [.zz.ss. V ss :$ (V ss :$ (V ss :$ V zz))] [ev ss [],ev zz []]++> norm :: Tm -> Tm+> norm t = qu 0 (ev t [])
examples/FH.lhs view
@@ -8,6 +8,7 @@ > import System.IO.Error  > import IFunctor+> import IMonad  > data FHState = FOpen | FClosed > data FHSTATE :: {FHState} -> * where
examples/IFunctor.lhs view
@@ -8,38 +8,3 @@ > class IFunctor (phi :: ({i} -> *) -> {o} -> *) where >   imap :: (s :-> t) -> phi s :-> phi t -> class IFunctor phi => IMonad (phi :: ({i} -> *) -> {i} -> *) where->   iskip :: s :-> phi s->   iextend :: (s :-> phi t) -> (phi s :-> phi t)--> iseq :: IMonad phi => (r :-> phi s) -> (s :-> phi t) -> (r :-> phi t)-> iseq f g = iextend g . f--> (>>-) :: IMonad phi => phi s i -> (s :-> phi t) -> phi t i-> (>>-) = flip iextend--> data (:*) :: (({i} -> *) -> {i} -> *) -> ({i} -> *) -> {i} -> * where->   Ret  :: q i -> (phi :* q) i->   Do   :: phi (phi :* q) i -> (phi :* q) i--> instance IFunctor phi => IFunctor ((:*) phi) where->   imap f = iextend (iskip . f)--> instance IFunctor phi => IMonad ((:*) phi) where->   iskip = Ret->   iextend f (Ret x) = f x->   iextend f (Do d) = Do (imap (iextend f) d)--Some predicates we like.--> data (:-) :: * -> {x} -> {x} -> * where->   V :: a -> (a :- x) x--> ret :: IMonad phi => a -> phi (a :- i) i-> ret a = iskip (V a)--> knownState :: (a -> t i) -> (a :- i) :-> t-> knownState f (V a) = f a--> (?-) :: IMonad phi => phi (a :- j) i -> (a -> phi t j) -> phi t i-> c ?- f = c >>- knownState f
+ examples/IMonad.lhs view
@@ -0,0 +1,42 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE KindSignatures, RankNTypes, TypeOperators, GADTs #-}++> module IMonad where++> import IFunctor++> class IFunctor phi => IMonad (phi :: ({i} -> *) -> {i} -> *) where+>   iskip :: s :-> phi s+>   iextend :: (s :-> phi t) -> (phi s :-> phi t)++> iseq :: IMonad phi => (r :-> phi s) -> (s :-> phi t) -> (r :-> phi t)+> iseq f g = iextend g . f++> (>>-) :: IMonad phi => phi s i -> (s :-> phi t) -> phi t i+> (>>-) = flip iextend++> data (:*) :: (({i} -> *) -> {i} -> *) -> ({i} -> *) -> {i} -> * where+>   Ret  :: q i -> (phi :* q) i+>   Do   :: phi (phi :* q) i -> (phi :* q) i++> instance IFunctor phi => IFunctor ((:*) phi) where+>   imap f = iextend (iskip . f)++> instance IFunctor phi => IMonad ((:*) phi) where+>   iskip = Ret+>   iextend f (Ret x) = f x+>   iextend f (Do d) = Do (imap (iextend f) d)++My favourite predicate.++> data (:-) :: * -> {x} -> {x} -> * where+>   V :: a -> (a :- x) x++> ret :: IMonad phi => a -> phi (a :- i) i+> ret a = iskip (V a)++> knownState :: (a -> t i) -> (a :- i) :-> t+> knownState f (V a) = f a++> (?-) :: IMonad phi => phi (a :- j) i -> (a -> phi t j) -> phi t i+> c ?- f = c >>- knownState f
examples/Path.lhs view
@@ -6,6 +6,7 @@ > import Unsafe.Coerce  > import IFunctor+> import IMonad  > data Path :: ({i,i} -> *) -> {i,i} -> * where >   Nil :: Path r {i,i}
examples/Vec.lhs view
@@ -1,19 +1,66 @@ > {-# OPTIONS_GHC -F -pgmF she #-}-> {-# LANGUAGE GADTs, KindSignatures, TypeOperators #-}+> {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts,+>     MultiParamTypeClasses, UndecidableInstances, ScopedTypeVariables,+>     RankNTypes #-}  > module Vec where  > import Control.Applicative -> data Nat = Z | S Nat+> import ShePrelude +> data Nat :: * where+>   Z :: Nat+>   S :: Nat -> Nat+>   deriving (SheSingleton)++> {-+> data Down :: ({Nat} -> *) -> {Nat} -> * where+>   DNil :: Down x {Z}+>   DCons :: x {n} -> Down x {n} -> Down x {S n}+> -}+ > data Vec :: {Nat} -> * -> * where >   VNil :: Vec {Z} x >   (:>) :: x -> Vec {n} x -> Vec {S n} x+>   deriving () +> instance Show x => Show (Vec {n} x) where+>   show VNil       = "VNil"+>   show (x :> xs)  = show x ++ " :> " ++ show xs+ > vtail :: Vec {S n} x -> Vec {n} x > vtail (x :> xs) = xs -> vapp :: Vec {n} (s -> t) -> Vec {n} s -> Vec {n} t-> vapp VNil VNil = VNil-> vapp (f :> fs) (s :> ss) = f s :> vapp fs ss+> type family (m :: {Nat}) :+ (n :: {Nat}) :: {Nat}+> type instance {Z} :+ n = n+> type instance {S m} :+ n = {S} (m :+ n)++> instance Functor (Vec {n}) where+>   fmap f VNil = VNil+>   fmap f (x :> xs) = f x :> fmap f xs++> vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x+> vappend VNil ys = ys+> vappend (x :> xs) ys = x :> vappend xs ys++> instance {:n :: Nat:} => Applicative (Vec {n}) where+>   pure = vec {:n :: Nat:} where+>     vec :: forall x. pi (n :: Nat). x -> Vec {n} x+>     vec {Z}    x = VNil+>     vec {S n}  x = x :> vec n x+>   (<*>) = vapp where+>     vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t+>     vapp VNil VNil = VNil+>     vapp (f :> fs)  (s :> ss) = f s :> vapp fs ss++> fiveByFive :: Vec {S (S (S (S (S Z))))} Int+> fiveByFive = pure 5++> vtake :: forall x. pi (m :: Nat). pi (n :: Nat). Vec ({m} :+ {n}) x -> Vec {m} x+> vtake {Z}   {n} xs         = VNil+> vtake {S m} {n} (x :> xs)  = x :> vtake {m} {n} xs++> listVec :: [a] -> (pi (n :: Nat). Vec {n} a -> t) -> t+> listVec [] f = f {Z} VNil+> listVec (x : xs) f = listVec xs (\ n ys -> f {S n} (x :> ys))
she.cabal view
@@ -1,5 +1,5 @@ name:               she-version:            0.0+version:            0.1 homepage:           http://personal.cis.strath.ac.uk/~conor/pub/she synopsis:           A Haskell preprocessor adding miscellaneous features description:@@ -12,30 +12,45 @@ author:             Conor McBride maintainer:         conor@strictlypositive.org extra-source-files: src/Makefile+                    examples/Binding.lhs                     examples/Fix.lhs                     examples/FH.lhs                     examples/Hig.lhs                     examples/IFunctor.lhs+                    examples/IMonad.lhs                     examples/Jig.lhs                     examples/Parsley.lhs                     examples/Path.lhs                     examples/Pig.lhs                     examples/Tree.lhs                     examples/Vec.lhs-cabal-version:      >= 1.2+cabal-version:      >= 1.6 build-type:         Simple  executable she     main-is:            Main.lhs -    build-depends:      base >=4 && < 5,+    build-depends:      base >=3 && < 5,                         mtl,                         filepath     hs-source-dirs:     src      other-modules:      Aspect+                        DeBruijn+                        IdiomBrackets                         Imports                         HaLay                         Parsley                         Patsy                         TypesToKinds++library+    exposed-modules:    ShePrelude+    build-depends:      base >=3 && < 5,+                        mtl,+                        filepath+    hs-source-dirs:     src    ++source-repository head+  type:     darcs+  location: http://personal.cis.strath.ac.uk/~conor/pub/she
src/Aspect.lhs view
@@ -22,18 +22,18 @@  > outdent :: [[Tok]] -> [[Tok]] > outdent tss = map (munge nip) tss where->   nip (NL : Spc ss : ts) = Just $->     NL : Spc (replicate (length ss - l) ' ') : munge nip ts+>   nip (NL fl : Spc ss : ts) = Just $+>     NL fl : Spc (replicate (length ss - l) ' ') : munge nip ts >   nip _ = Nothing >   l = skin tss >   skin [] = 0->   skin ([NL, Spc ss] : (t : _) : _) | not (isSpcT t) = length ss+>   skin ([NL _, Spc ss] : (t : _) : _) | not (isSpcT t) = length ss >   skin (_ : tss) = skin tss  > indent :: Int -> [Tok] -> [Tok] > indent i = munge dent where->   dent (NL : Spc ss : ts) = Just $->     NL : Spc (replicate i ' ' ++ ss) : munge dent ts+>   dent (NL fl : Spc ss : ts) = Just $+>     NL fl : Spc (replicate i ' ' ++ ss) : munge dent ts >   dent _ = Nothing  > dropIn :: [Higgle] -> Int -> String -> [[Tok]]@@ -44,12 +44,12 @@  > higOut :: Higgle -> [[Tok]] > higOut (s, tss) =->   [NL] :->   [KW "import", Spc " ", Sym "->", Spc " ", Uid s, Spc " ", KW "where"] :->   (indent 2 <$> tss)+>   [ [NL ("Dunno.lhs", 0)]+>   , [KW "import", Spc " ", Sym "->", Spc " ", Uid s, Spc " ", L "where" (indent 4 <$> tss)]+>   ]  > pDent :: P Tok Int-> pDent = teq NL *> grok spcl next <|> 0 <$ teq NL where+> pDent = pNL *> grok spcl next <|> 0 <$ pNL where >   spcl (Spc ss) = Just (length ss) >   spcl _ = Nothing @@ -68,4 +68,4 @@ >   ep ts = do >     (i, (s, ts)) <- parse ((,) <$> pDent <*> pPiggle) ts >     return $->       NL : Spc (replicate i ' ') : join (dropIn higs i s)+>       NL ("Dunno.lhs", 0): Spc (replicate i ' ') : join (dropIn higs i s) ++ ts
+ src/DeBruijn.lhs view
@@ -0,0 +1,25 @@+> module DeBruijn where++> import Data.List+> import Control.Applicative++> import Parsley+> import HaLay++> deBruijnMu :: [String] -> [Tok] -> Maybe [Tok]+> deBruijnMu xs (B Sqr ss : ts)+>   = (:) <$> parse jig ss <*> pure (munge (deBruijnMu xs) ts) where+>     jig :: P Tok Tok+>     jig = teq (Sym ".") *>+>           (shf xs <$> some (lid <* teq (Sym ".")) <*> pRest)+>     shf xs [] ts = B Rnd (wang xs : KW "in" : Spc " " :+>                           munge (deBruijnMu xs) ts)+>     shf xs (y : ys) ts = shf (y : xs) ys ts+>     wang xs = L "let"  ([Ope Crl] :+>                        intersperse [Semi] (zipWith dang xs [0..]) +++>                        [[Clo Crl]])+>     dang x i = [Lid x, Sym "=", Lit (show i)]+> deBruijnMu _ _ = Nothing++> deBruijn :: [[Tok]] -> [[Tok]]+> deBruijn = map (munge (deBruijnMu []))
src/HaLay.lhs view
@@ -2,7 +2,7 @@  > module HaLay where -> import Control.Arrow+> import Control.Arrow (first) > import Control.Applicative > import Data.Char > import Data.List@@ -17,17 +17,19 @@ Glom a file like this ------------------------------------------------------------------------------ -> ready :: String -> [[Tok]]-> ready = map (munge exTyMu) . fst . getLines (Seek NoLay "") [] .->         tokenize . (,) 0+> ready :: String -> String -> [[Tok]]+> ready f = map (munge exTyMu) . fst . getLines (Seek NoLay "") [] .+>           tokenize . (,) ((f, 0), 0)  ------------------------------------------------------------------------------ Stage 1 : lexing ------------------------------------------------------------------------------ -> tokenize :: (Int, String) -> [(Int, Tok)]-> tokenize = unfoldr (runStateT ((,) <$> gets fst <*> tokIn))+> type Position = (({-file-}String, {-line-}Int), {-col-}Int) +> tokenize :: (Position, String) -> [(Int, Tok)]+> tokenize = unfoldr (runStateT ((,) <$> lCol <*> tokIn))+ > data Tok >   = Lit String >   | Ope BK@@ -40,7 +42,7 @@ >   | Spc String >   | Com String >   | Urk Char->   | NL+>   | NL (String, Int)    -- file and new line >   | B BK [Tok]          -- a bracket >   | L String [[Tok]]    -- some layout >   | T Tag [Tok]         -- a tagged region@@ -48,21 +50,22 @@  > tokOut :: Tok -> String > tokOut t = case t of->   Lit s -> s->   Ope b -> ope b->   Clo b -> clo b->   Uid s -> s->   Lid s -> s->   KW  s -> s->   Sym s -> s->   Semi  -> ";"->   Spc s -> s->   Com s -> s->   Urk c -> [c]->   NL    -> "\n"->   B b ts -> ope b ++ toksOut ts ++ clo b->   L s tss -> s ++ tokssOut tss->   T _ ts -> toksOut ts+>   Lit s      -> s+>   Ope b      -> ope b+>   Clo b      -> clo b+>   Uid s      -> s+>   Lid s      -> s+>   KW  s      -> s+>   Sym s      -> s+>   Semi       -> ";"+>   Spc s      -> s+>   Com s      -> s+>   Urk c      -> [c]+>   NL (f, l)  | isSuffixOf ".hers" f -> "\n"+>              | otherwise -> "{-# LINE " ++ show l ++ " " ++ show f ++ " #-}\n"+>   B b ts     -> ope b ++ toksOut ts ++ clo b+>   L s tss    -> s ++ tokssOut tss+>   T _ ts     -> toksOut ts  > toksOut :: [Tok] -> String > toksOut ts = ts >>= tokOut@@ -70,13 +73,16 @@ > tokssOut tss = tss >>= toksOut  > isSpcT :: Tok -> Bool-> isSpcT (Spc _) = True-> isSpcT NL      = True-> isSpcT (Com _) = True-> isSpcT _       = False+> isSpcT (Spc _)  = True+> isSpcT (NL _)   = True+> isSpcT (Com _)  = True+> isSpcT _        = False  > tokIn :: L Tok > tokIn = Lit <$> ((:) <$> ch '\"' <*> slit)+>     <|> Lit <$> ((:) <$> ch '\'' <*> haha)+>     <|> NL <$ traverse ch "{-# LINE " <*> whur <* traverse ch "\" #-}" <*+>           some (chk isNL cha) >     <|> Com <$ stol <*> ((++) <$> traverse ch "#" <*>  spa (not . isNL)) >     <|> Sym <$>  sym >     <|> Com <$> ((++) <$> traverse ch "--" <*>  spa (not . isNL))@@ -90,20 +96,26 @@ >     <|> Semi <$ ch ';' >     <|> Lit <$> ((:) <$> chk isDigit cha <*> spa isDigit)  -- sod FP now >     <|> Uid <$> ((:) <$> chk isUpper cha <*> spa isIddy)->     <|> klid <$> ((:) <$> chk isLower cha <*> spa isIddy)+>     <|> klid <$> ((:) <$> chk (\ b -> isLower b || b == '_') cha <*> spa isIddy) >     <|> Spc  <$> ((:) <$> chk isHSpace cha <*> spa isHSpace)->     <|> NL <$ chk isNL cha+>     <|> NL <$ some (chk isNL cha) <*> lFLine >     <|> Urk <$> cha >  where >    slit = (:) <$> ch '\\' <*> ((:) <$> cha <*> slit) >      <|> return <$> ch '\"' >      <|> (:) <$> cha <*> slit+>    haha = (:) <$> ch '\\' <*> ((:) <$> cha <*> slit)+>      <|> return <$> ch '\''+>      <|> (:) <$> cha <*> haha >    klid s = if elem s keywords then KW s else Lid s >    comment 0 = pure "" >    comment i = (++) <$> traverse ch "{-" <*> comment (i + 1) >            <|> (++) <$> traverse ch "-}" <*> comment (i - 1) >            <|> (++) <$> ((:) <$> ch '\"' <*> slit) <*> comment i >            <|> (:) <$> cha <*> comment i+>    whur = flip (,) <$> (read <$> some (chk isDigit cha))+>             <* traverse ch " \""+>             <*> spa (not . (=='\"'))  ------------------------------------------------------------------------ Stage 2 : Group according to brackets and layout rules@@ -116,20 +128,42 @@ >   deriving (Show, Eq)  > getChunks :: ChunkMode -> [Tok] -> [(Int, Tok)] -> ([Tok], [(Int, Tok)])-> getChunks _ acc [] = (reverse acc, [])-> getChunks m acc its@((i, t) : its') = case (m, t) of->   _ | isSpcT t -> getChunks m (t : acc) its'->   (Lay _ j, _) | not (null acc) && i <= j -> (reverse acc, its)->   (Lay _ _, Semi) -> (reverse (t : acc), its')->   (Lay k _, KW e) | elem (k, e) layDKillaz -> (reverse acc, its)->   (Lay _ _, Clo _) -> (reverse acc, its)->   (Bra b, Clo b') | b == b' -> (reverse acc, its')->   (m, Ope b) -> case getChunks (Bra b) [] its' of->     (cs, its) -> getChunks m (B b cs : acc) its->   (m, KW e) | elem e lakeys -> case getLines (Seek m e) [] its' of->     (css, its) -> getChunks m ((L e css) : acc) its->   _ -> getChunks m (t : acc) its'+> getChunks m acc its =+>   let (iss, ius) = span gappy its+>       gappy (_, s) = isSpcT s+>       acss = case iss of+>         [] -> acc+>         _  -> reverse (map snd iss) ++ acc+>   in case ius of+>        [] -> (reverse acc, its)+>        ((i, t) : its') -> case (m, t) of+>          (Lay _ j, _) | not (null acc) && i <= j -> (reverse acc, its)+>          (Lay _ _, Semi) -> (reverse acc, its)+>          (Lay k _, KW e) | elem (k, e) layDKillaz -> (reverse acc, its)+>          (Lay _ _, Clo _) -> (reverse acc, its)+>          (Bra b, Clo b') | b == b' -> (reverse acss, its')+>          (m, Ope b) -> case getChunks (Bra b) [] its' of+>            (cs, its) -> getChunks m (B b cs : acss) its+>          (m, KW e) | elem e lakeys -> case getLines (Seek m e) [] its' of+>            (css, its) -> getChunks m ((L e css) : acss) its+>          _ -> getChunks m (t : acss) its' + getChunks :: ChunkMode -> [Tok] -> [(Int, Tok)] -> ([Tok], [(Int, Tok)])+ getChunks _ acc [] = (reverse acc, [])+ getChunks m acc its@((i, t) : its') = case (m, t) of+   _ | isSpcT t -> getChunks m (t : acc) its'+   (Lay _ j, _) | not (null acc) && i <= j -> (reverse acc, its)+   (Lay _ _, Semi) -> (reverse (t : acc), its')+   (Lay k _, KW e) | elem (k, e) layDKillaz -> (reverse acc, its)+   (Lay _ _, Clo _) -> (reverse acc, its)+   (Bra b, Clo b') | b == b' -> (reverse acc, its')+   (m, Ope b) -> case getChunks (Bra b) [] its' of+     (cs, its) -> getChunks m (B b cs : acc) its+   (m, KW e) | elem e lakeys -> case getLines (Seek m e) [] its' of+     (css, its) -> getChunks m ((L e css) : acc) its+   _ -> getChunks m (t : acc) its'++ > data LineMode >   = Bracing >   | Seek ChunkMode String@@ -137,34 +171,73 @@ >   deriving (Show, Eq)  > getLines :: LineMode -> [[Tok]] -> [(Int, Tok)] -> ([[Tok]], [(Int, Tok)])-> getLines _ acc [] = (reverse acc, [])-> getLines m acc ((_, s) : its) | isSpcT s = eat [s] its where->   eat sacc ((_, s) : its) | isSpcT s = eat (s : sacc) its->   eat sacc its = getLines m (reverse (splendid (reverse sacc)) ++ acc) its-> getLines m acc its@((i, t) : its') = case (m, t) of->   (Edge k j, _)->     | i == j -> case getChunks (Lay k i) [] its of->       ([], its) -> (reverse acc, its)->       (cs, its) -> getLines (Edge k i) (reverse (splendid cs) ++ acc) its->     | otherwise -> (reverse acc, its)->   (Seek m s, Ope Crl) -> getLines Bracing ([Ope Crl] : acc) its'->   (Seek (Lay k j) s, _)->     | j < i -> getLines (Edge s i) acc its->     | otherwise -> (reverse acc, its)->   (Seek NoLay s, _) -> getLines (Edge s i) acc its->   (Bracing, Clo Crl) -> (reverse ([Clo Crl] : acc), its')->   (Bracing, _) -> case getChunks NoLay [] its of->       ([], its) -> (reverse acc, its)->       (cs, its) -> getLines Bracing (cs : acc) its+> getLines m acc its =+>   let (iss, ius) = span gappy its+>       gappy (_, Semi) = True+>       gappy (_, s) = isSpcT s+>       acss = case iss of+>         [] -> acc+>         _  -> reverse (splendid (map snd iss)) ++ acc+>   in case ius of+>        [] -> (reverse acc, its)+>        ((i, t) : its') -> case (m, t) of+>          (Bracing, Clo Crl) -> (reverse ([Clo Crl] :  acss), its')+>          (_, Clo _) -> (reverse acc, its)+>          (Edge k j, _)+>            | i >= j -> case getChunks (Lay k i) [] ius of+>              ([], _) -> (reverse acc, its)+>              (cs, ius) -> getLines (Edge k i) (reverse (splendid cs) ++ acss) ius+>            | otherwise -> (reverse acc, its)+>          (Seek m s, Ope Crl) | properBrace its'+>            -> getLines Bracing ([Ope Crl] : acss) its'+>          (Seek (Lay k j) s, _)+>            | j < i -> getLines (Edge s i) acss ius+>            | otherwise -> (reverse acc, its)+>          (Seek (Bra b) s,_) -> getLines (Edge s i) acss ius+>          (Seek NoLay s, _) -> getLines (Edge s i) acss ius+>          (Bracing, _) -> case getChunks NoLay [] its of+>             ([], _) -> (reverse acc, its)+>             (cs, ius) -> getLines Bracing (cs : acss) ius +> properBrace :: [(Int, Tok)] -> Bool+> properBrace [] = True+> properBrace ((_, Clo Crl) : _) = False+> properBrace ((_, Semi) : _) = True+> properBrace ((_, Sym s) : _) | elem s ["->", "<-", "="] = True+> properBrace (_ : its) = properBrace its+++ getLines :: LineMode -> [[Tok]] -> [(Int, Tok)] -> ([[Tok]], [(Int, Tok)])+ getLines _ acc [] = (reverse acc, [])+ getLines m acc ((_, s) : its) | isSpcT s = eat [s] its where+   eat sacc ((_, s) : its) | isSpcT s = eat (s : sacc) its+   eat sacc its = getLines m (reverse (splendid (reverse sacc)) ++ acc) its+ getLines m acc its@((i, t) : its') = case (m, t) of+   (Bracing, Clo Crl) -> (reverse ([Clo Crl] : acc), its')+   (_, Clo _) -> (reverse acc, its)+   (Edge k j, _)+     | i == j -> case getChunks (Lay k i) [] its of+       ([], its) -> (reverse acc, its)+       (cs, its) -> getLines (Edge k i) (reverse (splendid cs) ++ acc) its+     | otherwise -> (reverse acc, its)+   (Seek m s, Ope Crl) -> getLines Bracing ([Ope Crl] : acc) its'+   (Seek (Lay k j) s, _)+     | j < i -> getLines (Edge s i) acc its+     | otherwise -> (reverse acc, its)+   (Seek (Bra b) s,_) -> getLines (Edge s i) acc its+   (Seek NoLay s, _) -> getLines (Edge s i) acc its+   (Bracing, _) -> case getChunks NoLay [] its of+       ([], its) -> (reverse acc, its)+       (cs, its) -> getLines Bracing (cs : acc) its+ > layDKillaz :: [(String, String)] > layDKillaz = [("of", "where"), ("do", "where"), ("let", "in")]  > splendid :: [Tok] -> [[Tok]] > splendid [] = [[]]-> splendid (NL : ts) = case splendid ts of->   (ss : sss) | all isSpcT ss  -> [] : (NL : ss) : sss->              | otherwise      -> (NL : ss) : sss+> splendid (NL fl : ts) = case splendid ts of+>   (ss : sss) | all isSpcT ss  -> [] : (NL fl : ss) : sss+>              | otherwise      -> (NL fl : ss) : sss > splendid (t : ts) = case splendid ts of >   (us : sss) -> (t : us) : sss @@ -176,7 +249,7 @@  > tender :: Tok -> Bool > tender (L _ _ ) = True-> tender t = elem t [Semi, Sym "=", Sym ",", Sym "|", KW "in"]+> tender t = elem t [Semi, Sym "=", Sym ",", Sym "|", KW "in", KW "deriving"]  > exTyMu :: [Tok] -> Maybe [Tok] > exTyMu (t : ts)@@ -184,7 +257,7 @@ >   = Just $ t : u : munge exTyMu vs >   | elem t [KW "data", KW "newtype"] >   = Just $ case vs of->       Sym "=" : vs -> t : u : Sym "=" : [T Ty vs]  -- dodgy or what?+>       Sym "=" : vs -> t : u : Sym "=" : oldStyle vs >       _ -> t : u : munge exTyMu vs >   | elem t [KW "type"] >   = Just $ case vs of@@ -194,6 +267,22 @@ >     (u, vs) = first (T Ty . munge tyMu) (span (not . tender) ts) > exTyMu _ = Nothing +> oldStyle :: [Tok] -> [Tok]+> oldStyle ts = case parse (pSep (teq (Sym "|")) (many (tok (/= Sym "|")))) ts of+>     Just tss -> intercalate [Sym "|"] (map go tss)+>   where+>     noInfT (Sym (':':_)) = False+>     noInfT _ = True+>     go ts = case span noInfT ts of+>       (as, (t : bs)) -> [T Ty (munge tyMu as), t, T Ty (munge tyMu bs)]+>       _ -> case span isSpcT ts of+>         (ss, t : ts) -> ss ++ t : map ho ts+>         _ -> ts+>     ho s | isSpcT s = s+>     ho (Sym s) = Sym s+>     ho (B Crl ts) = B Crl (munge exTyMu ts)+>     ho t = T Ty (munge tyMu [t])+ > tyMu :: [Tok] -> Maybe [Tok] > tyMu (Sym "::" : ts) = Just $ Sym "::" : u : munge tyMu vs >   where@@ -217,6 +306,11 @@ > spc :: P Tok () > spc = () <$ many (tok isSpcT) +> pNL :: P Tok ()+> pNL = grok h next where+>   h (NL _)  = Just ()+>   h _       = Nothing+ > uid :: P Tok String > uid = grok h next where >   h (Uid s) = Just s@@ -282,18 +376,18 @@ >   easy (t : ts) = tokOut t ++ easy ts  > dental :: [[Tok]] -> [Tok]-> dental [] = [NL]-> dental (l@(NL : _) : (c : _) : _) | not (isSpcT c) = l+> dental [] = [NL ("Dunno.lhs", 0)]+> dental (l@(NL _ : _) : (c : _) : _) | not (isSpcT c) = l > dental (l : ls) = dental ls  > redent :: [Tok] -> [[Tok]] -> [[Tok]]-> redent nl ((NL : _) : tss) = redent nl tss+> redent nl ((NL _ : _) : tss) = redent nl tss > redent nl (ts : tss) = nl : ts : redent nl tss > redent nl [] = []  > preamble :: [[Tok]] -> [[Tok]] -> [[Tok]] > preamble ls [] = ls-> preamble ls ms@(l@(NL : _) : (c : _) : _) | not (isSpcT c) =+> preamble ls ms@(l@(NL _ : _) : (c : _) : _) | not (isSpcT c) = >   redent l ls ++ ms > preamble ls (m : ms) = m : preamble ls ms @@ -312,7 +406,7 @@ > isIddy b = isAlphaNum b || elem b "_'"  > isInfy :: Char -> Bool-> isInfy b = elem b "!#$%&*+-.:/<=>?@\\^|~"+> isInfy b = elem b "!#$%&*+-,.:/<=>?@\\^|~"  > data BK = Rnd | Sqr | Crl deriving (Show, Eq) @@ -329,25 +423,33 @@ > keywords :: [String] > keywords = ["module", "import", "type", "data", "newtype", "pattern", "kind", >             "let", "in", "case", "of", "do", "forall", "class", "instance",->             "family", "where", "if", "then", "else"]+>             "family", "where", "if", "then", "else", "deriving"]  > lakeys :: [String] > lakeys = ["let", "of", "do", "where"]  > width :: [Tok] -> Int-> width ts = case span (/= NL) ts of+> width ts = case span noNL ts of >   (ts, []) -> length (ts >>= tokOut)->   (_, NL : ts) -> width ts+>   (_, NL _ : ts) -> width ts+>   where noNL (NL _)  = False+>         noNL _       = True  ------------------------------------------------------------------------ The lexer monad ------------------------------------------------------------------------ -> type L = StateT (Int, String) Maybe+> type L =  StateT  (Position, String) Maybe +> lFLine :: L (String, Int)+> lFLine = gets $ \ ((fl, _), _) -> fl++> lCol :: L Int+> lCol = gets $ \ ((_, c), _) -> c+ > instance Alternative L where->   empty = StateT $ \ is -> empty->   p <|> q = StateT $ \ is -> runStateT p is <|> runStateT q is+>   empty    = StateT $ \ is -> empty+>   p <|> q  = StateT $ \ is -> runStateT p is <|> runStateT q is  > instance Applicative L where >   pure = return@@ -356,15 +458,15 @@ > cha :: L Char > cha = StateT moo where >   moo (i, []) = Nothing->   moo (i, c : s) | isNL c = Just (c, (0, s))->                  | c == '\t'->                  = if mod i 8 == 7 then Just (' ', (i + 1, s))->                                    else Just (' ', (i + 1, c : s))->                  | otherwise = Just (c, (i + 1, s))+>   moo ((fl@(f,l),i), c : s)+>     | isNL c     = Just (c, (((f, l + 1), 0), s))+>     | c == '\t'  = if mod i 8 == 7  then Just (' ', ((fl, i + 1), s))+>                                     else Just (' ', ((fl, i + 1), c : s))+>     | otherwise  = Just (c, ((fl, i + 1), s))  > stol :: L () > stol = do->   i <- gets fst+>   i <- lCol >   guard (i == 0)  > chk :: (t -> Bool) -> L t -> L t@@ -377,10 +479,10 @@ > spa p = (:) <$> chk p cha <*> spa p  <|> pure []  > sym :: L String-> sym = StateT $ \ (i, s) -> case h s of+> sym = StateT $ \ ((fl, i), s) -> case h s of >   ("", _) -> Nothing >   ("--", _) -> Nothing->   (s, t) -> Just (s, (i + length s, t))+>   (s, t) -> Just (s, ((fl, i + length s), t)) >  where >   h (s@('-':'}':_)) = ("", s) >   h (c : s) | isInfy c = first (c :) (h s)
+ src/IdiomBrackets.lhs view
@@ -0,0 +1,78 @@+> module IdiomBrackets where++> import Control.Applicative++> import HaLay+> import Parsley++> pIBAlts :: P Tok [[Tok]]+> pIBAlts = teq (Sym "|") *> many (many (tok (/= Sym "|")) <* teq (Sym "|"))++> pInfA :: P Tok ([Tok], Tok, [Tok])+> pInfA = (,,) <$> many (tok (not . infSym)) <*> tok infSym <*> pRest where+>   infSym (Sym s) = not (elem s ["~", "@"])+>   infSym _ = False++> ia :: Tok -> String -> Tok -> Tok+> ia x o y = B Rnd [x, Spc " ", Sym o, Spc " ", y]++> ip :: Tok -> Tok+> ip t = B Rnd [Lid "pure", Spc " ", t]++> iGrok :: Tok -> [Tok] -> Tok+> iGrok f [] = f+> iGrok f (s : ts) | isSpcT s = iGrok f ts+> iGrok f (Sym "@" : ts) = iGrok (B Rnd [Lid "join", Spc " ", f]) ts+> iGrok f (Sym "~" : Spc _ : ts) = iGrok f (Sym "~" : ts)+> iGrok f (Sym "~" : t : ts) = iGrok (ia f "<*>" (ip t)) ts+> iGrok f (B Rnd (Sym "%" : us) : ts) = iGrok (ia f "<*" (iGnore "%" us)) ts+> iGrok f (B Rnd (Sym "-" : us) : ts) = iGrok (ia f "<*" (iGnore "-" us)) ts+> iGrok f (t : ts) = iGrok (ia f "<*>" t) ts++> iGnore :: String -> [Tok] -> Tok+> iGnore z ts = case parse (pSep (teq Semi) (many (tok notSep)) <* teq (Sym z)) ts of+>     Nothing -> ip (B Rnd [])+>     Just [] -> ip (B Rnd [])+>     Just [ts] -> B Rnd ts+>     Just (ts : tss) -> foldl (\ a bs -> ia a "<*" (B Rnd bs)) (B Rnd ts) tss+>   where+>     notSep Semi = False+>     notSep (Sym x) | x == z = False+>     notSep _ = True++> iStart :: [Tok] -> Tok+> iStart [] = ip (B Rnd [])+> iStart (s : ts) | isSpcT s = iStart ts+> iStart (B Rnd (Sym "%" : us) : ts) = ia (iGnore "%" us) "*>" (iStart ts)+> iStart (B Rnd (Sym "-" : us) : ts) = ia (iGnore "-" us) "*>" (iStart ts)+> iStart (t : ts) = iGrok (ip t) ts++> iIA :: Tok -> [Tok] -> Tok+> iIA f [] = f+> iIA f (s : ts) | isSpcT s = iIA f ts+> iIA f (Sym "@" : ts) = iIA (B Rnd [Lid "join", Spc " ", f]) ts+> iIA f (Sym "~" : Spc _ : ts) = iIA f (Sym "~" : ts)+> iIA f (Sym "~" : t : ts) = iIA (ia f "<*>" (ip t)) ts+> iIA f (B Rnd (Sym "%" : us) : ts) = iIA (ia f "<*" (iGnore "%" us)) ts+> iIA f (B Rnd (Sym "-" : us) : ts) = iIA (ia f "<*" (iGnore "-" us)) ts+> iIA f (t : ts) = let (us, vs) = span yum ts in iIA (ia f "<*>" (B Rnd (t : us))) vs+>   where yum (B Rnd (Sym "%" : _)) = False+>         yum (Sym "@") = False+>         yum _ = True++> iPro :: [Tok] -> Tok+> iPro ts = case parse pInfA ts of+>   Nothing -> iStart ts+>   Just (as, o, bs) -> iIA (iIA (ip (B Rnd [o])) as) bs++> rejig :: [[Tok]] -> Tok+> rejig [] = Lid "empty"+> rejig [ts] = iPro ts+> rejig (ts : tss) = ia (iPro ts) "<|>" (rejig tss)++> idiomBrackets :: [Tok] -> [Tok]+> idiomBrackets = munge ibMu where+>   ibMu (B Rnd us : ts) = case parse pIBAlts us of+>     Just uss -> Just $ rejig (map (munge ibMu) uss) : munge ibMu ts+>     Nothing -> Nothing+>   ibMu _ = Nothing
src/Imports.lhs view
@@ -3,8 +3,9 @@ > import Control.Applicative > import System.IO.Error > import System.FilePath-> import Data.Foldable+> import Data.Foldable hiding (elem) > import Data.Monoid+> import Data.Maybe  > import HaLay > import Parsley@@ -20,10 +21,26 @@ > grokImports cs = foldMap pure $ parse pImport cs  > getHers :: [String] -> IO [[Tok]]-> getHers p = ready <$>  tryReadFile (joinPath p <.> "hers")+> getHers p = ready f <$> tryReadFile f where f = joinPath p <.> "hers"  > storySoFar :: [[Tok]] -> IO [[Tok]]-> storySoFar hs = foldMap getHers (hs >>= grokImports)+> storySoFar hs = oneOfEach [] <$> foldMap getHers (hs >>= grokImports)++> pModule :: P Tok String+> pModule = (teq (KW "module") *> spc *> uid) <* pRest++> oneOfEach :: [String] -> [[Tok]] -> [[Tok]]+> oneOfEach xs [] = []+> oneOfEach xs (ts : tss) = case parse pModule ts of+>   Just x | elem x xs  -> oneOfEach xs tss+>          | otherwise  -> ts : oneOfEach (x : xs) tss+>   Nothing -> ts : oneOfEach xs tss++> pModuleGuts :: P Tok [[Tok]]+> pModuleGuts = teq (KW "module") *> spc *> uid *> spc *> pLay "where" pRest++> getGuts :: [[Tok]] -> [[Tok]]+> getGuts = foldMap (fromMaybe [] . parse pModuleGuts)  > instance Monoid x => Monoid (IO x) where >   mempty = pure mempty
src/Main.lhs view
@@ -5,34 +5,47 @@ > import Data.Char > import Data.Traversable > import Data.Foldable+> import Data.List+> import Debug.Trace  > import HaLay > import Imports > import Aspect+> import DeBruijn > import Patsy > import TypesToKinds+> import IdiomBrackets -> sheGoes :: [[Tok]] -> [[Tok]] -> ([[Tok]], [[Tok]])-> sheGoes hersi0 hs0 =+> sheGoes :: FilePath -> [[Tok]] -> [[Tok]] -> ([[Tok]], [[Tok]])+> sheGoes mo inh hs0 = >   let nl = dental hs0->       (higs0, hersi1) = foldMap higgle hersi0+>       hersi0 = getGuts inh+>       (higs0, _) = foldMap higgle hersi0 >       (higs1, hs1) = foldMap higgle hs0 >       higs = higs0 ++ higs1->       herso0 = higs >>= higOut+>       herso0 = higs1 >>= higOut >       hs2 = piggle higs hs1->       ((ps0, herso1), _) = traverse getPatsy hersi1->       ((ps1, herso2), hs3) = traverse getPatsy hs2+>       hs2'5 = deBruijn hs2+>       hs2'75 = map idiomBrackets hs2'5+>       ((ps0, _), _) = traverse getPatsy hersi0+>       ((ps1, herso1), hs3) = traverse getPatsy hs2'75 >       hs4 = case prepare (ps0 ++ ps1) of >               Nothing -> hs3 >               Just ps -> map (processes ps) hs3->       hs5 = typesToKinds hs4 ++ redent nl (hs4 >>= dataGrok)->   in  (herso0 ++ [[NL]] ++ herso1 ++ [[NL]] ++ herso2, hs5)+>       hs5 = typesToKinds (noDerSing hs4) +++>             redent nl ((hs4 >>= dataGrok) ++ (hs4 >>= singGrok))+>   in  (inh +++>        [[NL (mo ++ ".hers", 0)],+>         [KW "module", Spc " ", Uid mo, Spc " ", L "where"+>           (redent [NL (mo ++ ".hers", 0), Spc "  "]+>            (herso0 ++ [[NL (mo ++ ".hers", 0)]] ++ herso1))]]+>       , hs5) -> hsAndHers :: String -> IO (String, String)-> hsAndHers s = do->   let ihs = ready s+> hsAndHers :: String -> FilePath -> String -> IO (String, String)+> hsAndHers f mo s = do+>   let ihs = ready f s >   pcs <- storySoFar ihs->   let (hers, hs) = sheGoes pcs ihs+>   let (hers, hs) = sheGoes mo pcs ihs >   return (tokssOut hs, tokssOut hers)  > main :: IO ()@@ -43,7 +56,7 @@ >   putStrLn y >   putStrLn z >   f <- readFile y->   (f', h) <- hsAndHers f+>   (f', h) <- hsAndHers x (takeBaseName x) f >   writeFile x' h >   writeFile z f'
src/Makefile view
@@ -5,3 +5,34 @@  install: she 	sudo cp she /usr/local/bin/+# DO NOT DELETE: Beginning of Haskell dependencies+Parsley.o : Parsley.lhs+HaLay.o : HaLay.lhs+HaLay.o : Parsley.hi+Imports.o : Imports.lhs+Imports.o : Parsley.hi+Imports.o : HaLay.hi+Aspect.o : Aspect.lhs+Aspect.o : Parsley.hi+Aspect.o : HaLay.hi+DeBruijn.o : DeBruijn.lhs+DeBruijn.o : HaLay.hi+DeBruijn.o : Parsley.hi+Patsy.o : Patsy.lhs+Patsy.o : HaLay.hi+Patsy.o : Parsley.hi+TypesToKinds.o : TypesToKinds.lhs+TypesToKinds.o : Parsley.hi+TypesToKinds.o : HaLay.hi+IdiomBrackets.o : IdiomBrackets.lhs+IdiomBrackets.o : Parsley.hi+IdiomBrackets.o : HaLay.hi+Main.o : Main.lhs+Main.o : IdiomBrackets.hi+Main.o : TypesToKinds.hi+Main.o : Patsy.hi+Main.o : DeBruijn.hi+Main.o : Aspect.hi+Main.o : Imports.hi+Main.o : HaLay.hi+# DO NOT DELETE: End of Haskell dependencies
src/Patsy.lhs view
@@ -17,19 +17,19 @@  > getPatsy :: [Tok] -> (([Patsy], [[Tok]]), [Tok]) > getPatsy cs = case parse pPatsy cs of->   Just p -> (([p], [cs,[NL]]), jigger p)+>   Just p -> (([p], [cs,[NL ("Dunno.lhs", 0)]]), jigger p) >   _      -> (([], []), cs)  > jigger :: Patsy -> [Tok] > jigger (s, (as, cs)) =->   Lid ("patsy" ++ s) : (as >>= \a -> [Spc " ", Lid a]) +++>   Lid ("-- patsy" ++ s) : (as >>= \a -> [Spc " ", Lid a]) ++ >   [Spc " ", Sym "=", Spc " "] ++ cs  > subst :: [(String, Tok)] -> Tok -> Tok > subst xcs (Lid x) = case lookup x xcs of >   Just c -> c >   Nothing -> Lid x-> subst xcs (Spc _) = Spc " "+> subst xcs s | isSpcT s = Spc " " > subst xcs (B Rnd cs) = B Rnd (map (subst xcs) cs) > subst xcs (B Sqr cs) = B Sqr (map (subst xcs) cs) > subst xcs (B Crl cs) = B Crl (recs False cs) where@@ -63,7 +63,7 @@ > process :: [Patsy] -> Tok -> Maybe Tok > process ps (Lid y) = Just (Lid y) > process ps (Uid c) = case lookup c ps of->   Just (xs, cs) -> Just (abstract xs cs)+>   Just (xs, cs) -> Just (abstract xs (map (subst []) cs)) >   Nothing -> Just (Uid c) > process ps (B Rnd cs) = Just $ B Rnd (processes ps cs) > process ps (B Sqr cs) = Just $ B Sqr (processes ps cs)
+ src/ShePrelude.lhs view
@@ -0,0 +1,42 @@+> {-# LANGUAGE TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses, GADTs,+>     ScopedTypeVariables, FlexibleContexts+> #-}++> module ShePrelude where++> data SheProxy (ty :: *) (tm :: *) where SheProxy :: SheProxy ty tm+> class SheChecks (ty :: *) (tm :: *) where+>   sheTypes :: SheProxy ty tm -> SheSingleton ty tm+> data family SheSingleton ty :: * -> *++> data SheTyLeft x = SheTyLeft x+> data SheTyRight x = SheTyRight x+> data instance SheSingleton (Either s t) dummy where+>   SheWitLeft   :: SheSingleton s x -> SheSingleton (Either s t) (SheTyLeft x)+>   SheWitRight  :: SheSingleton t x -> SheSingleton (Either s t) (SheTyRight x)+> instance SheChecks s x => SheChecks (Either s t) (SheTyLeft x) where+>   sheTypes _ = SheWitLeft (sheTypes (SheProxy :: SheProxy s x))+> instance SheChecks t x => SheChecks (Either s t) (SheTyRight x) where+>   sheTypes _ = SheWitRight (sheTypes (SheProxy :: SheProxy t x))++> data SheTyTrue = SheTyTrue+> data SheTyFalse = SheTyFalse+> data instance SheSingleton Bool dummy where+>   SheWitTrue   :: SheSingleton Bool SheTyTrue+>   SheWitFalse  :: SheSingleton Bool SheTyFalse+> instance SheChecks Bool SheTyTrue where+>   sheTypes _ = SheWitTrue+> instance SheChecks Bool SheTyFalse where+>   sheTypes _ = SheWitFalse++> data SheSpecialNil = SheSpecialNil+> data (:$#$#$#:) x y = (:$#$#$#:) x y+> data instance SheSingleton [t] dummy where+>   SheSpecialWitNil :: SheSingleton [t] SheSpecialNil+>   (:$%$%$%:) :: SheSingleton t x -> SheSingleton [t] xs ->+>                 SheSingleton [t] (x :$#$#$#: xs)+> instance SheChecks [t] SheSpecialNil where+>   sheTypes _ = SheSpecialWitNil+> instance (SheChecks t x, SheChecks [t] xs) => SheChecks [t] (x :$#$#$#: xs) where+>   sheTypes _ = (sheTypes (SheProxy :: SheProxy t x)) :$%$%$%:+>                (sheTypes (SheProxy :: SheProxy [t] xs))
src/TypesToKinds.lhs view
@@ -1,6 +1,7 @@ > module TypesToKinds where  > import Control.Applicative+> import Data.List  > import HaLay > import Parsley@@ -14,12 +15,14 @@  > blat :: (Tok, Int) -> [Tok] > blat (c, j) =->     [KW "data", T Ty (cxs ++ [Spc " "]), Sym "=", T Ty cxs] where->   cxs = Spc " " : c : ([1 .. j] >>= (\k -> [Spc " ", Lid ("x" ++ show k)]))+>     [KW "data", T Ty (cxs id ++ [Spc " "]), Sym "="] ++ cxs ty where+>   cxs f = Spc " " : c :+>           ([1 .. j] >>= (\k -> [Spc " ", f (Lid ("x" ++ show k))]))+>   ty t = T Ty [t]  > fillet :: [Tok] -> [(Tok, Int)] > fillet [] = []-> fillet (Sym "=" : [T Ty cs]) =+> fillet (Sym "=" : cs) = >   case parse (pSep (spc *> teq (Sym "|")) (spc *> pOldSyn)) cs of >     Just sis -> sis >     _ -> []@@ -27,25 +30,25 @@ > fillet (_ : cs) = fillet cs  > pOldSyn :: P Tok (Tok, Int)-> pOldSyn = (\s -> (jig s, 2)) <$ pArg <*> infC <* pArg+> pOldSyn = (\s -> (jig s, 2)) <$ pArg <* spc <*> infC <* pArg >       <|> (,) <$> pCId->               <*> (length <$> many pArg <|> pBr Crl pFields) >               <* spc+>               <*> (pBr Crl pFields <|> length <$> many pArg)+>               <* spc  > jig :: String -> Tok > jig s = (B Rnd [Sym (":$#$#$#" ++ s)])  > pArg :: P Tok () > pArg = spc <* (->   () <$ lid <|>->   () <$ uid <|>->   pBr Rnd (() <$ pRest) <|>->   pBr Sqr (() <$ pRest) <|>+>   (() <$ pTag Ty pRest) <|> >   teq (Sym "!") *> pArg >   )  > pFields :: P Tok Int-> pFields = 0 <$ pEnd <|> (1 +) <$ lid <*> pFields <|> next *> pFields+> pFields = 0 <$ pEnd+>       <|> (1 +) <$ lid <*> pFields  -- right, assuming types are chunked+>       <|> next *> pFields  > gadtSyn :: [Tok] -> [(Tok, Int)] > gadtSyn cs = case parse pGDecl cs of@@ -65,21 +68,260 @@ >      <|> (1 +) <$ teq (Sym "->") <*> pArity >      <|> next *> pArity +> pTele :: P Tok ([(String, [Tok])], [Tok])+> pTele = (,)  <$> some (spc *> pBr Rnd piB) <* spc <* teq (Sym ".")+>              <*> pRest+>              where+>    piB :: P Tok (String, [Tok])+>    piB = (,) <$ spc <*> lid <* spc <* teq (Sym "::") <* spc <*> pRest+ > tyTTK :: [Tok] -> Maybe [Tok]-> tyTTK (B Crl [T Ex us] : ts) =->   Just $ B Rnd (munge exTTK us) : munge tyTTK ts-> tyTTK (B Crl [T Ty us] : ts) =->   Just $ Sym "*" : munge tyTTK ts+> tyTTK (B Crl [T Ex (Sym ":" : us)] : ts) = case parse pProxyRequest us of+>   Just (tm, ty) -> Just $+>     [Uid "SheChecks", Spc " ", B Rnd ty, Spc " ", B Rnd (munge exTTK tm)]+>     ++ munge tyTTK ts+>   _ -> Nothing+> tyTTK (B Crl [T Ex us] : ts)  = Just $ B Rnd (munge exTTK us) : munge tyTTK ts+> tyTTK (B Rnd us : ts) = (: munge tyTTK ts) <$> (sing <$> parse pSing us) where+>   sing t = B Rnd [Uid "SheSingleton", Spc " ", B Rnd t]+>   pSing = spc *> teq (Sym "::") *> pTag Ki pRest+> tyTTK (Lid "pi" : ts)         = pity <$> parse pTele ts where+>   pity :: ([(String, [Tok])], [Tok]) -> [Tok]+>   pity (xss, ts) =+>     [KW "forall", Spc " "] +++>     (xss >>= \ (x, _) -> [Lid x, Spc " "]) +++>     [Sym ".", Spc " "] +++>     (xss >>= \ (x, ss) ->+>       [Uid "SheSingleton", Spc " ", B Rnd (munge tyTTK ss), Spc " ", Lid x,+>        Spc " ", Sym "->", Spc " "]) +++>     munge tyTTK ts+> tyTTK (T Ki us : ts)          = Just $ T Ki (munge kiTTK us) : munge tyTTK ts > tyTTK _ = Nothing +> kiTTK :: [Tok] -> Maybe [Tok]+> kiTTK (B Crl [T Ty us] : ts)  = Just $ Sym "*" : munge kiTTK ts+> kiTTK (Lid "pi" : ts)         = piki <$> parse pTele ts where+>   piki :: ([(String, [Tok])], [Tok]) -> [Tok]+>   piki (xks, ts) =+>     (xks >>= \ (_, ks) ->+>       [B Rnd (munge kiTTK ks), Spc " ", Sym "->", Spc " "]) +++>     munge kiTTK ts+> kiTTK (KW "forall" : ts)      = case span (/= Sym ".") ts of+>   (_, _ : ts) -> Just $ munge kiTTK ts+>   _ -> Nothing+> kiTTK _ = Nothing+ > ttkMu :: [Tok] -> Maybe [Tok] > ttkMu (T Ty us : ts) = Just $ T Ty (munge tyTTK us) : munge ttkMu ts+> ttkMu (B Crl (Sym ":" : us) : ts) = case parse pProxyRequest us of+>   Just (tm, ty) -> Just $ proxyRequest tm ty : munge ttkMu ts+>   _ -> Nothing+> ttkMu (B Crl us : ts)+>   | piArg us = Just $ B Rnd (munge witMu us) : munge ttkMu ts+>   where+>     piArg xs | elem (Sym "=") xs = False+>     piArg xs | elem (Sym "::") xs = False+>     piArg _ = True > ttkMu _ = Nothing +> pProxyRequest :: P Tok ([Tok], [Tok])+> pProxyRequest = (,) <$> some (tok (/= Sym "::")) <* teq (Sym "::") <* spc+>                     <*> pTag Ty (some (tok (/= Sym ":")) <* teq (Sym ":"))++> witMu :: [Tok] -> Maybe [Tok]+> witMu (B Sqr us : ts) = Just $ mkL (munge witMu us) : munge witMu ts where+>   mkL [] = Uid "SheSpecialWitNil"+>   mkL ts = case span (/= Sym ",") ts of+>     (ss, []) ->+>       B Rnd [B Rnd ss, Spc " ", Sym ":$%$%$%:", Spc " ", Uid "SheSpecialNil"]+>     (ss, _ : ts) ->+>       B Rnd [B Rnd ss, Spc " ", Sym ":$%$%$%:", Spc " ", mkL ts]+> witMu (Uid s : ts) = Just $ Uid ("SheWit" ++ s) : munge witMu ts+> witMu (Sym (':' : s) : ts) = Just $ Sym (":$%$%$%:" ++ s) : munge witMu ts+> witMu _ = Nothing+ > exTTK :: [Tok] -> Maybe [Tok]+> exTTK (B Sqr us : ts) = Just $ mkL (munge exTTK us) : munge exTTK ts where+>   mkL [] = Uid "SheSpecialNil"+>   mkL ts = case span (/= Sym ",") ts of+>     (ss, []) ->+>       B Rnd [B Rnd ss, Spc " ", Sym ":$#$#$#:", Spc " ", Uid "SheSpecialNil"]+>     (ss, _ : ts) ->+>       B Rnd [B Rnd ss, Spc " ", Sym ":$#$#$#:", Spc " ", mkL ts] > exTTK (Uid s : ts) = Just $ Uid ("SheTy" ++ s) : munge exTTK ts > exTTK (Sym (':' : s) : ts) = Just $ Sym (":$#$#$#:" ++ s) : munge exTTK ts > exTTK _ = Nothing  > typesToKinds :: [[Tok]] -> [[Tok]] > typesToKinds = map (munge ttkMu)++> data ConTy = ConTy+>   { cName     :: String+>   , cForall   :: [Tok]+>   , cInst     :: [Tok]+>   , cArgs     :: [[Tok]]+>   , cFam      :: [Tok]+>   , cIndices  :: [Tok]+>   } deriving (Show)++> sing :: ConTy -> ConTy+> sing (ConTy+>   { cName     = c+>   , cForall   = xs+>   , cInst     = is+>   , cArgs     = as+>   , cFam      = ds+>   , cIndices  = ss+>   }) = ConTy+>   { cName     = "SheWit" ++ c+>   , cForall   = xs ++ (vs >>= (\v -> [Spc " ", Lid v]))+>  -- , cInst     = is +>   , cInst     = cook is (zipWith constra as vs)+>   , cArgs     = zipWith singa as vs+>   , cFam      = [B Rnd ([Uid "SheSingleton", Spc " "] ++ ds ++ Spc " " : ss)]+>   , cIndices  = ss  ++ [Spc " ",+>                     B Rnd  (mkPref (sheTy c) :+>                            (vs >>= (\ v -> [Spc " ", Lid v])))]+>   } where+>   vs = zipWith (\ _ i -> "sha" ++ show i) as [0..]+>   singa ts v = [Uid "SheSingleton", Spc " ", B Rnd ts, Spc " ", Lid v]+>   constra ts v = [Uid "SheChecks", Spc " ", B Rnd ts, Spc " ", Lid v]+>   cook is [] | all isSpcT is = is+>   cook (B Rnd is : _) cs = cook is cs+>   cook is cs+>     | all isSpcT is = [B Rnd (intercalate [Sym ",", Spc " "] cs)]+>     | otherwise = [B Rnd (intercalate [Sym ",", Spc " "] (is : cs))]++> conTyOut :: ConTy -> [Tok]+> conTyOut (ConTy+>   { cName     = c+>   , cForall   = xs+>   , cInst     = is+>   , cArgs     = as+>   , cFam      = ds+>   , cIndices  = ss+>   }) = [Uid c, Spc " ", Sym "::", Spc " ", T Ty (+>        fao xs +++>        cio is +++>        (as >>= \ ts -> ts ++ [Spc " ", Sym "->", Spc " "]) +++>        ds ++ Spc " " : ss)]+>   where+>     fao xs | all isSpcT xs = xs+>            | otherwise = [KW "forall", Spc " "] ++ xs ++ [Sym ".", Spc " "]+>     cio xs | all isSpcT xs = xs+>            | otherwise = xs ++ [Spc " ", Sym "=>", Spc " "]++> pGConTy :: P Tok ConTy+> pGConTy = (ConTy <$ spc <*> uid <* spc <* teq (Sym "::") <* spc) >>= \f ->+>           pTag Ty (f <$> pFA <*> pCI <*> many pARG <* spc <*> (((:[]). Uid) <$> uid)+>                    <*> pRest)+>   where+>     pFA = spc *> (+>             teq (KW "forall") *> some (tok (/= Sym ".")) <* teq (Sym ".")+>             <|> [] <$ spc)+>     pCI = some (tok (/= Sym "=>")) <* teq (Sym "=>")+>           <|> [] <$ spc+>     pARG = some (tok (/= Sym "->")) <* teq (Sym "->")++> mkPref :: Tok -> Tok+> mkPref t@(Sym _) = B Rnd [t]+> mkPref t = t++> sheTy :: String -> Tok+> sheTy (':' : s) = Sym (":$#$#$#:" ++ s)+> sheTy s = Uid ("SheTy" ++ s)++> pGADT :: P Tok ((String, Int), ([ConTy], [String]))+> pGADT = (,)+>   <$   tok (`elem` [KW "data", KW "newtype"]) <* spc+>   <*>  pTag Ty ((,) <$ spc <*> uid <* spc <*>  pGArity <* pRest) <* spc+>   <*>  pLay "where" ((,) <$> pGCons <*> pDer)+>   <*   pRest+>   where+>     pGArity = length <$> many (lid <* spc)+>               <|> (teq (Sym "::") *> spc *> pTag Ki pArity)+>     pGCons = tok (all isSpcT) *> pGCons+>              <|> (:) <$> grok (parse pGConTy) next <*> pGCons+>              <|> pure []+>     pDer = grok (parse pDeriving) next <* pRest <|> pure []++> pDeriving :: P Tok [String]+> pDeriving = teq (KW "deriving") *> spc *>+>             (pure <$> uid <|>+>             pBr Rnd (spc *> pSep (spc *> teq (Sym ",") *> spc) uid <* spc))++ singGrok :: [Tok] -> [[Tok]]+ singGrok ts = case parse pGADT ts of+   Just ((s, i), (cs, ds)) | elem "SheSingleton" ds ->+    let vs = [1..i] >>= \v -> [Spc " ", Lid ("x" ++ show i)] in+    [[KW "type",+      T Ty [Spc " ", KW "instance", Spc " ", Uid "SheSingleton", Spc " ",+           B Rnd (Uid s : vs), Spc " "],+      Sym "=",+      T Ty (Spc " " : Uid ("SheSing" ++ s) : vs)],[NL ("Dunno.lhs",0)],+     [KW "data", Spc " ", Uid ("SheSing" ++ s), Spc " ", Sym "::",+      T Ki (concat (replicate i [Spc " ", Sym "*", Spc " ", Sym "->"]) +++           [Spc " ", Sym "*", Spc " ", Sym "->", Spc " ", Sym "*", Spc " "]),+      L "where" (cs >>= \ c -> [[NL ("Dunno.lhs",0), Spc "    "], conTyOut (sing c)])],[NL ("Dunno.lhs",0)]] +++     (cs >>= \ c -> [checkI c, [NL ("Dunno.lhs",0)]])+   _ -> []++> singGrok :: [Tok] -> [[Tok]]+> singGrok ts = case parse pGADT ts of+>   Just ((s, i), (cs, ds)) | elem "SheSingleton" ds ->+>    let vs = [1..i] >>= \v -> [Spc " ", Lid ("x" ++ show i)] in+>     [[KW "data",+>       T Ty [Spc " ", KW "instance", Spc " ", Uid "SheSingleton", Spc " ",+>            B Rnd (Uid s : vs), Spc " ", Uid "dummy", Spc " ",+>       L "where" (cs >>= \ c -> [[NL ("Dunno.lhs",0), Spc "    "], conTyOut (sing c)])]],+>      [NL ("Dunno.lhs",0)]] +++>      (cs >>= \ c -> [checkI c, [NL ("Dunno.lhs",0)]])+>   _ -> []++> checkI :: ConTy -> [Tok]+> checkI  (ConTy+>   { cName     = c+>   , cForall   = xs+>   , cInst     = is+>   , cArgs     = as+>   , cFam      = ds+>   , cIndices  = ss+>   }) =+>   [KW "instance",+>    T Ty (Spc " " : prems ais +++>     [Uid "SheChecks", Spc " ", B Rnd (ds ++ Spc " " : ss), Spc " ",+>      B Rnd (mkPref (sheTy c) : (ais >>= (\ (_, v) -> [Spc " ", Lid v]))),+>      Spc " "]),+>    L "where" [[Spc " "],+>      [Lid "sheTypes", Spc " ", Lid "_", Spc " ", Sym "=", Spc " ",+>       Uid ("SheWit" ++ c)] ++ (ais >>= poxy)+>      ]+>   ]+>   where+>     ais = zipWith (\ty i -> (ty, "sha" ++ show i)) as [0..]+>     prems [] = []+>     prems [tyv] = cnstr tyv ++ [Spc " " , Sym "=>", Spc " "]+>     prems (tyv : tyvs) =+>       [B Rnd (cnstr tyv +++>               (tyvs >>= \tyv -> [Sym ",", Spc " "] ++ cnstr tyv)),+>        Spc " " , Sym "=>", Spc " "]+>     cnstr (ty, v) = [Uid "SheChecks", Spc " ", B Rnd ty, Spc " ", Lid v]+>     poxy (ty, v) = [Spc " ", proxyRequest [Lid v] ty]++> proxyRequest :: [Tok] -> [Tok] -> Tok+> proxyRequest tm ty = B Rnd [+>       Lid "sheTypes", Spc " ", B Rnd [+>         Uid "SheProxy", Spc " ", Sym "::", T Ty [Spc " ",+>           Uid "SheProxy", Spc " ", B Rnd ty, Spc " ", B Rnd (munge exTTK tm)+>       ]]]++> noDerSing :: [[Tok]] -> [[Tok]]+> noDerSing = map (munge ndsMu) where+>   ndsMu ts = case parse pDeriving ts of+>     Just xs -> Just $ mkDer (filter (/= "SheSingleton") xs)+>     _ -> Nothing+>   mkDer [] = []+>   mkDer [x] = [KW "deriving", Spc " ", Uid x]+>   mkDer (x : xs) =+>     [KW "deriving", Spc " ",+>      B Rnd (Uid x : (xs >>= \x -> [Sym ",", Spc " ", Uid x]))]