diff --git a/examples/Vec.lhs b/examples/Vec.lhs --- a/examples/Vec.lhs +++ b/examples/Vec.lhs @@ -57,10 +57,22 @@ > 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 +> vtakePox :: forall n. Pox n -> +> forall x. pi (m :: Nat). Vec ({m} :+ {n}) x -> Vec {m} x +> vtakePox n {Z} xs = VNil +> vtakePox n {S m} (x :> xs) = x :> vtakePox n {m} 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)) + +> data Pox n = Pox + +> pox :: forall box. (forall n. Pox n -> box n) -> (forall n. box n) +> pox f = f Pox + +> newtype TakeBox n = TakeBox +> {unboxTake :: forall x. pi (m :: Nat). Vec ({m} :+ {n}) x -> Vec {m} x} + +> -- vtake :: forall n x. pi (m :: Nat). Vec ({m} :+ {n}) x -> Vec {m} x +> vtake = unboxTake (pox (TakeBox . vtakePox)) diff --git a/she.cabal b/she.cabal --- a/she.cabal +++ b/she.cabal @@ -1,5 +1,5 @@ name: she -version: 0.1 +version: 0.2 homepage: http://personal.cis.strath.ac.uk/~conor/pub/she synopsis: A Haskell preprocessor adding miscellaneous features description: @@ -42,6 +42,7 @@ HaLay Parsley Patsy + Superclass TypesToKinds library diff --git a/src/DeBruijn.lhs b/src/DeBruijn.lhs --- a/src/DeBruijn.lhs +++ b/src/DeBruijn.lhs @@ -18,7 +18,7 @@ > wang xs = L "let" ([Ope Crl] : > intersperse [Semi] (zipWith dang xs [0..]) ++ > [[Clo Crl]]) -> dang x i = [Lid x, Sym "=", Lit (show i)] +> dang x i = [Lid x, Sym "=", Lit (show i), Sym "::", T Ty [Uid "Int"]] > deBruijnMu _ _ = Nothing > deBruijn :: [[Tok]] -> [[Tok]] diff --git a/src/HaLay.lhs b/src/HaLay.lhs --- a/src/HaLay.lhs +++ b/src/HaLay.lhs @@ -381,6 +381,7 @@ > dental (l : ls) = dental ls > redent :: [Tok] -> [[Tok]] -> [[Tok]] +> redent (NL _ : r) ((NL p : _) : tss) = redent (NL p : r) tss > redent nl ((NL _ : _) : tss) = redent nl tss > redent nl (ts : tss) = nl : ts : redent nl tss > redent nl [] = [] @@ -423,7 +424,7 @@ > keywords :: [String] > keywords = ["module", "import", "type", "data", "newtype", "pattern", "kind", > "let", "in", "case", "of", "do", "forall", "class", "instance", -> "family", "where", "if", "then", "else", "deriving"] +> "family", "where", "if", "then", "else", "deriving", "hiding"] > lakeys :: [String] > lakeys = ["let", "of", "do", "where"] diff --git a/src/Main.lhs b/src/Main.lhs --- a/src/Main.lhs +++ b/src/Main.lhs @@ -15,6 +15,7 @@ > import Patsy > import TypesToKinds > import IdiomBrackets +> import Superclass > sheGoes :: FilePath -> [[Tok]] -> [[Tok]] -> ([[Tok]], [[Tok]]) > sheGoes mo inh hs0 = @@ -29,16 +30,18 @@ > hs2'75 = map idiomBrackets hs2'5 > ((ps0, _), _) = traverse getPatsy hersi0 > ((ps1, herso1), hs3) = traverse getPatsy hs2'75 +> (hs3'5, herso2) = superclass nl hersi0 hs3 > hs4 = case prepare (ps0 ++ ps1) of -> Nothing -> hs3 -> Just ps -> map (processes ps) hs3 +> Nothing -> hs3'5 +> Just ps -> map (processes ps) hs3'5 > 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))]] +> (herso0 ++ [[NL (mo ++ ".hers", 0)]] ++ herso1 +> ++ [[NL (mo ++ ".hers", 0)]] ++ herso2))]] > , hs5) > hsAndHers :: String -> FilePath -> String -> IO (String, String) diff --git a/src/Makefile b/src/Makefile --- a/src/Makefile +++ b/src/Makefile @@ -1,6 +1,6 @@ default: she -she: Main.lhs Parsley.lhs Patsy.lhs TypesToKinds.lhs HaLay.lhs Imports.lhs Aspect.lhs +she: Main.lhs Parsley.lhs Patsy.lhs TypesToKinds.lhs HaLay.lhs Imports.lhs Aspect.lhs Superclass.lhs ghc --make Main -o she install: she diff --git a/src/Superclass.lhs b/src/Superclass.lhs new file mode 100644 --- /dev/null +++ b/src/Superclass.lhs @@ -0,0 +1,267 @@ +> module Superclass where + +> import Data.List +> import Control.Applicative +> import Data.Foldable hiding (elem, any) + +> import Parsley +> import HaLay + +In a .hers file, the stored class info will look like + + class C x1 .. xn where + meth1 .. methn -- method names + instance CXT1 => S t1 .. tm where -- default superclass instances + stuff -- classified by method + +In the source, whenever we see + + instance CXT0 => C s1 .. sn where + f1 + ... + fn + hiding instance S' -- just the name + +we should determine which instance declarations to generate: certainly + + instance CXT0 => C s1 .. sn where + fi -- whichever belong to the class + +preceded by whichever of the Ss are not hidden. For each such + + instance CXT1 => S t1 .. tm where + stuff + +process + + instance (CXT0, [si/xi]CXT1) => S [si/xi]t1 .. where + [si/xi]stuff + +in the same way. + +Whenever we see + + class CXT => C x1 .. xn where + meth1 + ... + methn + instance S y1 .. ym where -- the ys are a subset of the xs + stuff + +we must generate Haskell code + + class CXT => C x1 .. xn where + meth1 + ... + methn + +and an entry in the .hers file + + class C x1 .. xn where + meth1 .. methn + instance S y1 .. ym where + stuff + +Note that (contra to email proposal), that separates instance subordination +from superclass status. + +> data ClassInfo = ClassInfo +> { classParams :: [String] +> , classCxt :: [Tok] +> , classStuff :: [String] +> , classInstances :: [Instance] +> } deriving Show + +> data Instance = Instance +> { instanceRawHeader :: [Tok] +> , instanceClass :: String +> , instanceArgs :: [Tok] +> , instanceCxt :: [Tok] +> , instanceMethods :: [[Tok]] +> , instanceHiding :: [String] +> } deriving Show + +> type Classes = [(String, ClassInfo)] + +> isNool :: [Tok] -> Bool +> isNool (NL _ : _) = True +> isNool _ = False + +> classy :: [Tok] -> (([(String, ClassInfo)], [[Tok]]), [[Tok]]) +> classy ts@(KW "class" : T Ty h : L "where" tss : rest) = case parse pHdr h of +> Nothing -> (([], []), [ts]) +> Just (cx, cl, xs) -> (([(cl, ClassInfo +> { classParams = xs +> , classCxt = cx +> , classStuff = residue >>= declares +> , classInstances = filtrate >>= instancy +> })], [KW "class" : T Ty ([Spc " ", Uid cl, Spc " "] ++ +> foldMap (\s -> [Lid s, Spc " "]) xs) : +> L "where" (nl : dstuff : nl : filtrate) : rest, +> [NL ("Dunno.lhs", 0)]]) +> , [KW "class" : T Ty h : L "where" residue : rest]) +> where +> pHdr = (,,) <$> pCxt <* spc <*> uid <*> some (spc *> lid) <* spc +> pCxt = some (tok (/= Sym "=>")) <* teq (Sym "=>") +> <|> [] <$ spc +> nl = nool tss +> nool [] = [] +> nool (t : _) | isNool t = t +> nool (_ : tss) = nool tss +> (filtrate, residue) = partition isInstance tss +> stuff = residue >>= declares +> dstuff = intercalate [Sym ",", Spc " "] (map (return . Lid) stuff) +> isInstance (KW "instance" : _) = True +> isInstance _ = False +> classy ts = (([], []), [ts]) + +> declares :: [Tok] -> [String] +> declares ts = case inf ts of +> Just s -> [s] +> Nothing -> thug ts +> where +> inf (Sym s : _) | elem s [",", "=", "::"] = Nothing +> inf (Sym (':' : _) : ts) = inf ts +> inf (Sym s : _) = Just ("(" ++ s ++ ")") +> inf (Uid _ : ts) = inf ts +> inf (Lid _ : ts) = inf ts +> inf (t : ts) | isSpcT t = inf ts +> inf (Com _ : ts) = inf ts +> inf (B _ _ : ts) = inf ts +> inf _ = Nothing +> thug (t : ts) | isSpcT t = thug ts +> thug (Lid f : ts) = f : commamore ts +> thug (B Rnd [Sym s] : ts) = ("(" ++ s ++ ")") : commamore ts +> thug _ = [] +> commamore (Sym "," : ts) = thug ts +> commamore (t : ts) | isSpcT t = commamore ts +> commamore _ = [] + +> instancy :: [Tok] -> [Instance] +> instancy (KW "instance" : T Ty h : L "where" tss : _) = case parse pHdr h of +> Nothing -> [] +> Just (cx, cl, as) -> [Instance +> { instanceRawHeader = h +> , instanceClass = cl +> , instanceArgs = as +> , instanceCxt = cx +> , instanceMethods = filter (not . isHiding) tss +> , instanceHiding = tss >>= hidings +> }] +> where +> pHdr = (,,) <$> pCxt <* spc <*> uid <*> some (spc *> tok argT) <* spc +> argT (Lid _) = True +> argT (Uid _) = True +> argT (B _ _) = True +> argT _ = False +> pCxt = some (tok (/= Sym "=>")) <* teq (Sym "=>") +> <|> [] <$ spc +> isHiding (KW "hiding" : _) = True +> isHiding _ = False +> hidings (KW "hiding" : ts) = +> case parse (spc *> teq (KW "instance") *> spc *> +> pTag Ty (spc *> uid <* pRest) <* pRest) ts of +> Nothing -> [] +> Just s -> [s] +> hidings _ = [] +> instancy _ = [] + +> splinstance :: [(String, ClassInfo)] -> Instance -> [Instance] +> splinstance cs i = case lookup (instanceClass i) cs of +> Nothing -> [i] +> Just c -> let hs = instanceHiding i +> sups = filter (\ j -> not (elem (instanceClass j) hs)) +> (classInstances c) +> sbst = zip (classParams c) (instanceArgs i) +> (generated, residue) = +> growDefaults cs hs (instanceCxt i) sbst sups (instanceMethods i) +> in i {instanceMethods = residue, instanceHiding = []} : generated + +> growDefaults :: [(String, ClassInfo)] -> [String] -> +> [Tok] -> [(String, Tok)] -> [Instance] -> [[Tok]] -> +> ([Instance], [[Tok]]) +> growDefaults cs hs cxt sbst [] tss = ([], tss) +> growDefaults cs hs cxt sbst (i : is) tss0 = +> let (j, tss1) = growDefault cs hs cxt sbst i tss0 +> (js, tss2) = growDefaults cs hs cxt sbst is tss1 +> in (j ++ js, tss2) + +> owns :: [(String, ClassInfo)] -> String -> [String] +> owns cs c = case lookup c cs of +> Nothing -> [] +> Just c' -> classStuff c' ++ (classInstances c' >>= (owns cs . instanceClass)) +> + +> growDefault :: [(String, ClassInfo)] -> [String] -> +> [Tok] -> [(String, Tok)] -> Instance -> [[Tok]] -> +> ([Instance], [[Tok]]) +> growDefault cs hs cx0 sbst (Instance +> { instanceClass = c +> , instanceArgs = as +> , instanceCxt = cx1 +> , instanceMethods = uss +> , instanceHiding = h +> }) tss = (is, wss) where +> want = owns cs c +> relevant w ts = any (\ s -> elem s w) (declares ts) +> vss = filter (\ ts -> isNool ts || relevant want ts) tss +> explicit = vss >>= declares +> wss = filter (\ ts -> isNool ts || not (relevant want ts)) tss +> uss' = map (munge (sbMu sbst)) $ +> filter (\ us -> isNool us || not (relevant explicit us)) uss +> is = splinstance cs $ Instance +> { instanceClass = c +> , instanceRawHeader = [] +> , instanceArgs = munge (sbTyMu sbst) as +> , instanceCxt = [B Rnd (mergeCxt cx0 (munge (sbTyMu sbst) cx1))] +> , instanceMethods = (uss' ++ vss) +> , instanceHiding = hs ++ h +> } + +> mergeCxt :: [Tok] -> [Tok] -> [Tok] +> mergeCxt [] us = us +> mergeCxt (t : ts) us | isSpcT t = mergeCxt ts us +> mergeCxt (B Rnd ts : _) us = glomCxt ts us +> mergeCxt ts us = glomCxt ts us + +> glomCxt :: [Tok] -> [Tok] -> [Tok] +> glomCxt ts [] = ts +> glomCxt ts (u : us) | isSpcT u = mergeCxt ts us +> glomCxt ts (B Rnd us : _) = ts ++ [Sym ",", Spc " "] ++ us +> glomCxt ts us = ts ++ [Sym ",", Spc " "] ++ us + +> sbMu :: [(String, Tok)] -> [Tok] -> Maybe [Tok] +> sbMu sb (T Ty us : ts) = Just $ T Ty (munge (sbTyMu sb) us) : munge (sbMu sb) ts +> sbMu sb _ = Nothing + +> sbTyMu :: [(String, Tok)] -> [Tok] -> Maybe [Tok] +> sbTyMu sb (Lid s : ts) = (:) <$> lookup s sb <*> Just (munge (sbTyMu sb) ts) +> sbTyMu sb _ = Nothing + +> blatInstance :: Instance -> [[Tok]] +> blatInstance (Instance +> { instanceRawHeader = h +> , instanceClass = c +> , instanceArgs = as +> , instanceCxt = cx +> , instanceMethods = tss +> }) = +> [KW "instance" : T Ty hdr : [L "where" (redent (dental tss) tss)] , dental []] +> where +> hdr = case h of +> [] -> Spc " " : cx ++ [Spc " ", Sym "=>", Spc " ", Uid c] ++ +> foldMap (\ t -> [Spc " ", t]) as ++ [Spc " "] +> _ -> h + +> makeInstances :: [Tok] -> [(String, ClassInfo)] -> [[Tok]] -> [[Tok]] +> makeInstances nl cs [] = [] +> makeInstances nl cs (ts : tss) = case instancy ts of +> [] -> ts : makeInstances nl cs tss +> is -> redent nl (is >>= splinstance cs >>= blatInstance) +> ++ makeInstances nl cs tss + +> superclass :: [Tok] -> [[Tok]] -> [[Tok]] -> ([[Tok]], [[Tok]]) +> superclass nl hers hs0 = (makeInstances nl (cs ++ cs') hs1, nh) where +> ((cs', nh), hs1) = foldMap classy hs0 +> ((cs, _), _) = foldMap classy hers + diff --git a/src/TypesToKinds.lhs b/src/TypesToKinds.lhs --- a/src/TypesToKinds.lhs +++ b/src/TypesToKinds.lhs @@ -175,8 +175,8 @@ > }) = ConTy > { cName = "SheWit" ++ c > , cForall = xs ++ (vs >>= (\v -> [Spc " ", Lid v])) -> -- , cInst = is -> , cInst = cook is (zipWith constra as vs) +> , 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 " ",