Frank 0.0 → 0.1
raw patch · 11 files changed
+1764/−1 lines, 11 files
Files
- Check.lhs +214/−0
- Elab.lhs +388/−0
- ElabMonad.lhs +160/−0
- Frank.cabal +2/−1
- Gubbins.lhs +143/−0
- Pa.lhs +107/−0
- Run.lhs +123/−0
- Syntax.lhs +231/−0
- Template.lhs +123/−0
- Types.lhs +159/−0
- Unify.lhs +114/−0
+ Check.lhs view
@@ -0,0 +1,214 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, TypeSynonymInstances,+> FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,+> MultiParamTypeClasses #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module Check where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Prelude hiding (elem, all)+> import Data.Char+> import Data.List hiding (elem, all)+> import Data.Monoid+> import Data.Foldable+> import Data.Traversable+> import Control.Applicative+> import Control.Monad+> import Control.Newtype+> import Data.Void++> import Gubbins+> import Types+> import Pa+> import Syntax+> import Template+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% TError %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data TError+> = TMissing UpId+> | SMissing UpId+> | TArity UpId Int [VT]+> | SArity UpId Int [VT]+> | BadTemplate+> | Cockup String+> | AmbiguousPats [Pat]+> | AmbiguousRaws [Raw]+> | BadPat VT Pat+> | NoConstructor VT Template+> | AppliedPVar String+> | RepeatedPVar Template+> | PatArityError Template+> | RawArityError Template+> | BadLhs [Pat]+> | UnifyVFail VT VT+> | UnifyCFail CT CT+> | UnifySFail Sig Sig+> | BadBunk+> | Useless VT+> | CheckR VT Raw+> | CantDo Sig [Sig]+> | AmbiguousOp Template [Sig]+> | ThunkMismatch CT ([Pat], Raw)+> | BadMessPat [Pat]+> | GuessThunk [([Pat], Raw)]+> | BadHandlerType VT+> | SynCon+> | Line ([Pat], Raw) TError+> | Raw VT Raw TError+> | Dunno Template [Sig] [Template]+> deriving Show++> type Moan = TError :>>: Void+> type Moaning = Free Moan++> moan :: TError -> Moaning x+> moan e = com (e :? absurd)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% checking top level data, signature and function declarations %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data TypeInfo = TypeInfo+> { dataDecls :: [(UpId, (Int, [(Template, [VT])]))]+> , sigDecls :: [(UpId, (Int, [(Template, ([VT], VT))]))]+> , funDecls :: [(Template, (Int, [VT], [Sig], VT))]+> , templateT :: TemplateTable+> } deriving Show++> typeInfo :: Source -> Moaning TypeInfo+> typeInfo src = do+> let dt (n, (xs, cs)) =+> (| ~n, (| ~(length xs), traverse (conTemplate src xs) cs|)|)+> sg (n, (xs, os)) = (| ~n, (| ~(length xs), traverse oper os|)|) where+> oper (vs, v) = (|rass (conTemplate src xs vs) (tScope src xs v)|)+> rass (a, b) c = (a, (b, c))+> fn stuf@(vs, (ss, v)) = do+> let xs = ftvs src stuf+> (t, vs') <- conTemplate src xs vs+> ss' <- tScope src xs ss+> v' <- tScope src xs v+> return (t, (length xs, vs', ss', v'))+> ds <- (| ~ primitiveTypes ++ traverse dt (sourceData src) |)+> ss <- (| ~ primitiveSigs ++ traverse sg (sourceSigs src) |)+> fs <- (| ~primitiveFunDecls ++ traverse fn (sourceDecl src) |)+> let ts = (| fst (|(snd . snd) ds @ |)+> | fst (|(snd . snd) ss @ |)+> | fst fs+> |)+> return $ TypeInfo ds ss fs (TemplateTable ts [] [])++> ftvs :: TMang t => Source -> t -> [UpId]+> ftvs src = ala' UnionList (ala' Const tMang) (var chk mempty mempty)+> where chk u = maybe (maybe [u] (const []) (lookup u primitiveTypes))+> (const []) (lookup u (sourceData src))+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% generating a template and domains from a declaration %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> conTemplate :: Source -> [UpId] -> [Lump] -> Moaning (Template, [VT])+> conTemplate src xs vs = do+> (bs, us) <- go vs+> (|tmp bs, ~us|)+> where+> go [] = return ([], [])+> go (LTy v : vs) = do+> u <- tScope src xs v+> (bs, us) <- go vs+> return (Place : bs, u : us)+> go (LNm n : vs) = do+> (bs, us) <- go vs+> return (Mark n : bs, us)+> tmp [] = moan $ BadTemplate+> tmp (Mark n : bs) | all place bs = (|[Mark n]|)+> tmp bs = (|id (post bs)|)+> post [] = (|[]|)+> post (Place : Place : bs) = moan $ BadTemplate+> post (b : bs) = (| ~b : post bs|)+> place Place = True+> place _ = False+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% type scope and arity checking %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> class TScope x where+> tScope :: Source -> [UpId] -> x -> Moaning x++> instance TScope x => TScope [x] where+> tScope src xs = traverse (tScope src xs)++> instance TScope VT where+> tScope src xs (D x []) | Just i <- findIndex (==x) xs = return (X i)+> tScope src xs (D x vs) = do+> a <- maybe+> (maybe (moan $ TMissing x) (return . fst) (lookup x primitiveTypes))+> (return . length . fst) $+> lookup x (sourceData src)+> if a == length vs+> then (|(D x) (tScope src xs vs)|)+> else moan $ TArity x a vs+> tScope src xs (M os ss v) =+> (|M (tScope src xs os) (tScope src xs ss) (tScope src xs v)|)+> tScope src xs Un = return Un+> tScope src xs Ze = return Ze+> tScope src xs (U c) = (|U (tScope src xs c)|)+> tScope src xs (X _) = moan $ Cockup "X already?"+> tScope src xs (Q _) = moan $ Cockup "Q already?"++> instance TScope CT where+> tScope src xs (v :-> c) = (|tScope src xs v :-> tScope src xs c|)+> tScope src xs (F ss v) = (|F (tScope src xs ss) (tScope src xs v)|)++> instance TScope Sig where+> tScope src xs (s :$ vs) = do+> a <- maybe (maybe (moan $ SMissing s)+> (pure . fst) (lookup s primitiveSigs))+> (pure . length . fst) $+> lookup s (sourceSigs src)+> if a == length vs+> then (| ~s :$ tScope src xs vs|)+> else moan $ SArity s a vs+> tScope src xs Pure = (|Pure|)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% prmimitives %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> primitiveTypes :: [(UpId, (Int, [(Template, [VT])]))]+> primitiveTypes =+> [ (Up "Char", (0, []))+> , (Up "Bool", (0, [([Mark "tt"], []), ([Mark "ff"], [])]))+> ]++> char :: VT+> char = D (Up "Char") []++> bool :: VT+> bool = D (Up "Bool") []++> primitiveFunDecls :: [(Template, (Int, [VT], [Sig], VT))]+> primitiveFunDecls =+> [ ([Place, Mark "=Char=", Place], (0, [char, char], [], bool))+> ]++> primitiveSigs :: [(UpId, (Int, [(Template, ([VT], VT))]))]+> primitiveSigs =+> [ (Up "Console", (0,+> [ ([Mark "inch"], ([], char))+> , ([Mark "ouch"], ([char], Un))+> ]))+> ]
+ Elab.lhs view
@@ -0,0 +1,388 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, GADTs, TypeSynonymInstances, KindSignatures,+> FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,+> MultiParamTypeClasses #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module Elab where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Debug.Trace++> import Prelude hiding (elem, all, foldr, concat)+> import Data.Char+> import Data.List hiding (elem, all, foldr, concat)+> import Data.Monoid+> import Data.Foldable+> import Data.Traversable+> import Control.Applicative+> import Control.Monad+> import Control.Newtype+> import Control.Arrow+> import Data.Void++> import Gubbins+> import Types+> import Pa+> import Syntax+> import ElabMonad+> import Unify+> import Template+> import Check+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Cooked Terms %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data PAT+> = PV String+> | PC Template [PAT] -- void pattern is |PC [] []|+> | PL Char -- char literal+> | PR PAT+> | PO Template [PAT] PAT -- op params continuation++> instance Show PAT where+> show (PV x) = x+> show (PC t ps) = tempShow t (map show ps)+> show (PR p) = "[" ++ show p ++ "]"+> show (PO t ps p) =+> "[" ++ tempShow t (map show ps) ++ " ? " ++ show p ++ "]"++> data Dir+> = CHK+> | SYN++> data TM :: {Dir} -> * where+> H :: HD -> TM {SYN}+> (:/) :: TM {SYN} -> [TM {CHK}] -> TM {SYN}+> PApp :: TM {SYN} -> [TM {CHK}] -> TM {SYN}+> HAN :: TM {SYN} -> TM {CHK} -> TM {SYN}+>+> E :: TM {SYN} -> TM {CHK}+> CL :: Char -> TM {CHK}+> CN :: Template -> [TM {CHK}] -> TM {CHK}+> BUNK :: TM {CHK} -> TM {CHK}+> LAM :: [([PAT], TM {CHK})] -> TM {CHK}++> data HD = VA Int+> | FN Template -- cache the def like a Birdman?+> | OP Template++> hTemp :: Bwd Entry -> HD -> Template+> hTemp g (VA i) = fst (inx g i)+> hTemp g (FN f) = f+> hTemp g (OP o) = o++> gShow :: Bwd Entry -> TM {d} -> String+> gShow g (H h) = tempShow x ["_" | Place <- x] where x = hTemp g h+> gShow g (f :/ []) = gShow g f ++ " !"+> gShow g (H h :/ ts) = tempShow (hTemp g h) (map (gShow g) ts)+> gShow g (f :/ ts) = "(" ++ show f ++ (ts >>= ((' ' :) . show)) ++ ")"+> gShow g (PApp f ts) = "(" ++ show f ++ (ts >>= ((' ' :) . show)) ++ ")"+> gShow g (HAN h e) = "(" ++ gShow g h ++ "?" ++ gShow g e ++ ")"+> gShow g (E t) = gShow g t+> gShow g (CN c ts) = tempShow c (map (gShow g) ts)+> gShow g (BUNK t) = "(" ++ gShow g t ++ " {})"+> gShow g (LAM (a : as)) =+> "{" ++ lShow a ++ (as >>= ((" | " ++) . lShow)) ++ "}" where+> lShow ([], t) = gShow g t+> lShow (ps, t) =+> intercalate " " (map show ps) ++ " -> " ++ gShow (patOn g ps) t+> patOn g [] = g+> patOn g (PV x : ps) = patOn (bind g x) ps+> patOn g (PC _ ps : ps') = patOn (patOn g ps) ps'+> bind g x = g :< ([Mark x] ::: (0, Un)) -- cheeky!++> inx :: Bwd Entry -> Int -> (Template, (Int, VT))+> inx (_ :< (x ::: (i, j))) 0 = (x, (i, j))+> inx (g :< (_ ::: _)) i = inx g (i - 1)+> inx (g :< _) i = inx g i+> inx B0 i = ([Mark ('#' : show i)], (0, Un))++> instance Show (TM {d}) where+> show t = gShow B0 t++++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Type Checking and Synthesis %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> checkR :: VT -> Raw -> ElabM (TM {CHK})+> --checkR v r | trace ("checkR " ++ show (v, r)) $ False = undefined+> checkR v r = hnf v >>= \ v -> err (Raw v r) $ case r of+> RVd -> (|(CN [] []) (-Un =?= v-)|)+> RCh c -> (|(CL c) (-char =?= v-)|)+> RTh prs -> case v of+> U c -> (|LAM (traverse (body c) prs)|)+> _ -> moanE $ GuessThunk prs+> RN n -> checkR v (RA [RN n])+> RBunk -> moanE BadBunk+> RA rs -> (|ttrCh ~v (|rawTree ~rs ~[] @ |) @ |)+> RQ h e -> do+> ss <- getSigsE+> (h, z) <- synR h+> z <- hnf z+> case z of+> U (M hs is u :-> F os w) -> do+> w =?= v+> canDo os+> e <- withSigs (sAct hs ss) $ do+> canDo is+> checkR u e+> (|(E (HAN h e))|)+> _ -> moanE $ BadHandlerType z+> r -> synR r >>= want v++> synR :: Raw -> ElabM (TM {SYN}, VT)+> --synR r | trace ("synR " ++ show r) $ False = undefined+> synR (RN n) = synR (RA [RN n])+> synR RVd = moanE SynCon+> synR RBunk = moanE BadBunk+> synR (RA rs) = rawTree rs [] >>= \ t -> case t of+> TNode f ts -> appSyn f ts+> TLeaf r ts -> synR r >>= \ tv -> mention tv ts+> synR (RTh prs) = moanE $ GuessThunk prs+> synR (RQ h e) = do+> ss <- getSigsE+> (h, v) <- synR h+> v <- hnf v+> case v of+> U (M hs is u :-> F os w) -> do+> canDo os+> e <- withSigs (sAct hs ss) $ do+> canDo is+> checkR u e+> (|(HAN h e, w)|)+> _ -> moanE $ BadHandlerType v++> isBunk :: TTree Raw -> Bool+> isBunk (TLeaf RBunk []) = True+> isBunk _ = False++> ttrCh :: VT -> (TTree Raw) -> ElabM (TM {CHK})+> --ttrCh v t | trace ("ttrCh " ++ show (v, t)) $ False = undefined+> ttrCh v (TNode f ts) = if (not (null ts) && isBunk (last ts))+> then (|BUNK (ttrCh Ze (TNode f (init ts)))|) else do+> info <- getInfoE+> (g, _) <- getCxE+> let constrs = [ (c, ((u, i), vs))+> | (u, (i , cs)) <- dataDecls info+> , (c, vs) <- cs+> ]+> v <- hnf v+> case v of+> D u vs -> case lookup u (dataDecls info) of+> Nothing -> moanE $ TMissing u+> Just (i, cs) -> case lookup f cs of+> Just ws -> (|(CN f) (ttrsCh f (xsub vs ws) ts)|)+> Nothing -> appSyn f ts >>= want v+> Q _ -> case (gFetch g f, filter ((f ==) . fst) constrs) of+> (Nothing, [(_, ((u, m), vs))]) -> do+> ws <- fresh m+> ts <- ttrsCh f (xsub ws vs) ts+> D u ws =?= v+> (|(CN f ts)|)+> _ -> appSyn f ts >>= want v+> _ -> appSyn f ts >>= want v+> ttrCh v (TLeaf r []) = checkR v r+> ttrCh v _ = moanE $ Cockup "oops"++> want :: VT -> (TM {SYN}, VT) -> ElabM (TM {CHK})+> want v (t, u) = (|(E t) (-u =?= v-)|)++> getOps :: [Sig] -> ElabM [(Template, ([VT], (Sig, VT)))]+> getOps [] = return []+> getOps (Pure : _) = return []+> getOps (s@(u :$ vs) : ss) = do+> info <- getInfoE+> (| ~[ (ot, xsub vs (ois, (s, oo)))+> | (u', (i, os)) <- sigDecls info, u == u'+> , (ot, (ois, oo)) <- os+> ] ++ getOps ss |)++> mkOpType :: [Sig] -> ([VT], (Sig, VT)) -> VT+> mkOpType ss (vs, (s, v)) = sAct (U (foldr (:->) (F [s] v) vs)) ss++> appSyn :: Template -> [TTree Raw] -> ElabM (TM {SYN}, VT)+> --appSyn f ts | trace ("appSyn " ++ show (f, ts)) $ False = undefined+> appSyn f ts = do+> info <- getInfoE+> sigs <- getSigsE+> ops <- (|(map (id *** mkOpType sigs)) (getOps sigs)|)+> (g, _) <- getCxE+> case gFetch g f of+> Just (i, (m, v)) -> do+> ws <- fresh m+> let v' = xsub ws v+> --False <- trace ("FOUND: " ++ show f ++ " : " ++ show v') $+> -- return False+> mention (H (VA i), xsub ws v) ts+> Nothing -> case [v | (f', v) <- ops, f == f'] of+> (_:_:_) -> moanE $ AmbiguousOp f sigs+> [v] -> mention (H (OP f), v) ts+> [] -> case lookup f (funDecls info) of+> Just (m, vs, sa, v) -> do+> ws <- fresh m+> mention (H (FN f),+> sAct (xsub ws (U (foldr (:->) (F sa v) vs))) sigs)+> ts+> Nothing -> moanE $ Dunno f sigs (foldMap gnom g)++> gnom :: Entry -> [Template]+> gnom (x ::: _) = [x]+> gnom _ = []++> mention :: (TM {SYN}, VT) -> [TTree Raw] -> ElabM (TM {SYN}, VT)+> mention tv [] = return tv+> mention (t, U c) ts = use t [] c ts+> mention (t, v) ts = moanE $ Useless v++> use :: TM {SYN} -> [TM {CHK}] -> CT -> [TTree Raw] -> ElabM (TM {SYN}, VT)+> use f [] (F ss v) (TLeaf RBang [] : ts) = do+> canDo ss+> mention (f :/ [], v) ts+> use f as (F ss v) ts = do+> canDo ss+> mention (f :/ as, v) ts+> use f as (v :-> c) (t : ts) = do+> a <- ttrCh v t+> use f (as ++ [a]) c ts+> use f as c [] = (|(PApp f as, U c)|)++> canDo :: [Sig] -> ElabM ()+> canDo [] = return ()+> canDo (s : ss) = do+> ss' <- getSigsE+> findSig s ss' ss'+> canDo ss++> findSig :: Sig -> [Sig] -> [Sig] -> ElabM ()+> findSig s [] sd = moanE $ CantDo s sd+> findSig s@(a :$ us) ((b :$ vs) : ss) sd+> | a == b = us =?= vs+> | otherwise = findSig s ss sd++> gFetch :: Bwd Entry -> Template -> Maybe (Int, (Int, VT))+> gFetch B0 _ = Nothing+> gFetch (g :< (x ::: r)) y+> | x == y = Just (0, r)+> | otherwise = (|((1 +) *** id) (gFetch g y)|)+> gFetch (g :< _) y = gFetch g y++> fresh :: Int -> ElabM [VT]+> fresh m = do+> (g, n) <- getCxE+> setCxE (grow g n m)+> return (map Q (take m [n ..]))+> where+> grow g n 0 = (g, n)+> grow g n m = grow (g :< (n :=? Nothing)) (n + 1) (m - 1)++> ttrsCh :: Template -> [VT] -> [TTree Raw] -> ElabM [TM {CHK}]+> ttrsCh f [] [] = return []+> ttrsCh f (v : vs) (t : ts) = (|ttrCh v t : ttrsCh f vs ts|)+> ttrsCh f _ _ = moanE $ RawArityError f++> body :: CT -> ([Pat], Raw) -> ElabM ([PAT], TM {CHK})+> body (v :-> c) (p : ps, r) = do+> v <- hnf v+> (g, p) <- patCh v p+> (ps, t) <- cxLocal g $ body c (ps, r)+> return (p : ps, t)+> body (F ss v) ([], r) = do+> t <- withSigs ss (checkR v r)+> return ([], t)+> body c (ps, r) = moanE $ ThunkMismatch c (ps, r)++> rawTree :: [Raw] -> [TTree Raw] -> ElabM (TTree Raw)+> rawTree rs ts = do+> tbl <- ttT+> case pa (resolve tbl) (map (rawPunc tbl) rs) of+> [(t, [])] -> case t of+> TLeaf (RA rs) ts -> rawTree rs ts+> t -> return (tApp t ts)+> _ -> moanE $ AmbiguousRaws rs+> where+> rawPunc tbl (RN x) | punc tbl x = Left x+> rawPunc tbl p = Right p+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Pattern Checking %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> patCh :: VT -> Pat -> ElabM (Bwd Entry, PAT)+> patCh v (PN x) = do+> info <- getInfoE+> if elem [Mark x] (ttTemplates (templateT info))+> then ttpCh v (TNode [Mark x] [])+> else (|(B0 :< ([Mark x] ::: (0, v)), PV x)|)+> patCh Un PVd = (|(B0, PC [] [])|)+> patCh (D (Up "Char") []) (PCh c) = (|(B0, PL c)|)+> patCh (M os ss v) (PRet p) = (|(id *** PR) (patCh v p)|)+> patCh (M os ss v) (POp ps p) = patTree ps [] >>= \ z -> case z of+> TLeaf p _ -> moanE $ BadMessPat ps+> TNode o ts -> do+> ops <- getOps os+> case [x | (o', x) <- ops, o == o'] of+> [(us, (s, u))] -> do+> (gz, ps) <- ttpsCh o us ts+> (hz, p) <- patCh (U (u :-> F (sAct os ss) v)) p+> (|disjoin gz hz, ~(PO o ps p)|)+> patCh v (PA ps) = patTree ps [] >>= ttpCh v+> patCh v p = moanE $ BadPat v p++> ttpCh :: VT -> TTree Pat -> ElabM (Bwd Entry, PAT)+> ttpCh v (TLeaf p []) = patCh v p+> ttpCh v (TLeaf (PN n) _) = moanE $ AppliedPVar n+> ttpCh t@(D u vs) (TNode c ps) = do+> info <- getInfoE+> case lookup u (dataDecls info) of+> Nothing -> moanE $ TMissing u+> Just (i, cs) ->+> case lookup c cs of+> Nothing -> moanE $ NoConstructor t c+> Just ws -> (|(id *** PC c) (ttpsCh c (xsub vs ws) ps)|)+> ttpCh v (TNode c _) = moanE $ NoConstructor v c++> ttpsCh :: Template -> [VT] -> [TTree Pat] -> ElabM (Bwd Entry, [PAT])+> ttpsCh f [] [] = (| ~B0, ~[] |)+> ttpsCh f (v : vs) (t : ts) = do+> v <- hnf v+> (| disjoinC (ttpCh v t) (ttpsCh f vs ts) @ |)+> ttpsCh f _ _ = moanE $ PatArityError f++> disjoin :: Bwd Entry -> Bwd Entry -> ElabM (Bwd Entry)+> disjoin ez fz = (|(mappend ez fz) (-traverse chk fz-)|) where+> chk e@(x ::: _) = traverse (occ x) ez+> chk e = (|B0|)+> occ x (y ::: _) | x == y = moanE $ RepeatedPVar x+> occ x _ = (|()|)++> disjoinC :: (Bwd Entry, PAT) -> (Bwd Entry, [PAT]) ->+> ElabM (Bwd Entry, [PAT])+> disjoinC (ez, p) (fz, ps) = (|disjoin ez fz, ~(p : ps)|)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Patterns for Template Resolution %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> patTree :: [Pat] -> [TTree Pat] -> ElabM (TTree Pat)+> patTree ps ts = do+> tbl <- (|templateT getInfoE|)+> case pa (resolve tbl) (map (patPunc tbl) ps) of+> [(t, [])] -> case t of+> TLeaf (PA ps) ts -> patTree ps ts+> t -> return (tApp t ts)+> _ -> moanE $ AmbiguousPats ps+> where+> patPunc tbl (PN x) | punc tbl x = Left x+> patPunc tbl p = Right p+
+ ElabMonad.lhs view
@@ -0,0 +1,160 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, TypeSynonymInstances,+> FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,+> MultiParamTypeClasses #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module ElabMonad where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Debug.Trace++> import Prelude hiding (elem, all, foldr, concat)+> import Data.Char+> import Data.List hiding (elem, all, foldr, concat)+> import Data.Monoid+> import Data.Foldable+> import Data.Traversable+> import Control.Applicative+> import Control.Monad+> import Control.Newtype+> import Control.Arrow+> import Data.Void++> import Gubbins+> import Types+> import Pa+> import Syntax+> import Template+> import Check++++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Elaboration Monad and ghastly plumbing %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> type GetSigs = () :>>: [Sig]+> type GetInfo = () :>>: TypeInfo+> type GetCx = () :>>: Cx+> type SetCx = Cx :>>: ()++> type ElabM = Free ((Moan :+: (GetCx :+: SetCx)) :+: (GetSigs :+: GetInfo))++> moanE :: TError -> ElabM a+> moanE e = com (L (L (e :? absurd)))++> getCxE :: ElabM Cx+> getCxE = com (L (R (L (() :? Ret))))++> setCxE :: Cx -> ElabM ()+> setCxE g = com (L (R (R (g :? Ret))))++> modCxE :: (Cx -> Cx) -> ElabM ()+> modCxE f = (|setCxE (|f getCxE|) @ |)++> getSigsE :: ElabM [Sig]+> getSigsE = com (R (L (() :? Ret)))++> getInfoE :: ElabM TypeInfo+> getInfoE = com (R (R (() :? Ret)))++ elabUnify :: UnifyM x -> ElabM x+ elabUnify u = case moc u of+ Right x -> Ret x+ Left (L _) -> moanE UnifyFail+ Left (R (L (_ :? k))) -> getCxE >>= (elabUnify . k)+ Left (R (R (g :? k))) -> setCxE g >>= (elabUnify . k)++> ttT :: ElabM TemplateTable+> ttT = do+> info <- getInfoE+> (g, _) <- getCxE+> let tt = templateT info+> return (tt {ttTemplates = cxTemps g (ttTemplates tt)})+> where+> cxTemps B0 ts = ts+> cxTemps (g :< (x ::: _)) ts = cxTemps g (x : ts)+> cxTemps (g :< _) ts = cxTemps g ts++> cxLocal :: Bwd Entry -> ElabM x -> ElabM x+> cxLocal g c = do+> modCxE (((`mappend` g) . (:< Semicolon)) *** id)+> x <- c+> modCxE (popSemi *** id)+> return x+> where+> popSemi (g :< Semicolon) = g+> popSemi (g :< _) = popSemi g++> withSigs :: [Sig] -> ElabM x -> ElabM x+> withSigs ss c = case moc c of+> Right x -> Ret x+> Left (L (L (e :? k))) -> moanE e+> Left (L (R (L (_ :? k)))) -> getCxE >>= (withSigs ss. k)+> Left (L (R (R (g :? k)))) -> setCxE g >>= (withSigs ss. k)+> Left (R (L (() :? k))) -> withSigs ss (k ss)+> Left (R (R (() :? k))) -> getInfoE >>= (withSigs ss . k) ++> baseInfo :: TypeInfo -> ElabM x -> Either TError x+> baseInfo info = go (B0, 0) where+> go g c = case moc c of+> Right x -> Right x+> Left (L (L (e :? k))) -> Left e+> Left (L (R (L (_ :? k)))) -> go g (k g)+> Left (L (R (R (g :? k)))) -> go g (k ())+> Left (R (L (() :? k))) -> go g (k [Up "" :$ []]) -- the ineffable+> Left (R (R (() :? k))) -> go g (k info)++> err :: (TError -> TError) -> ElabM x -> ElabM x+> err f c = case moc c of+> Right x -> Ret x+> Left (L (L (e :? k))) -> moanE $ f e+> Left (L (R (L (_ :? k)))) -> getCxE >>= (err f . k)+> Left (L (R (R (g :? k)))) -> setCxE g >>= (err f . k)+> Left (R (L (() :? k))) -> getSigsE >>= (err f . k)+> Left (R (R (() :? k))) -> getInfoE >>= (err f . k) ++> hnf :: VT -> ElabM VT+> hnf (Q i) = do+> (g, _) <- getCxE+> return $ improve (Q i) g+> where+> improve (Q i) (g :< (j :=? Just v)) | i == j = improve v g+> improve (Q i) (g :< _) = improve (Q i) g+> improve v _ = v+> hnf v = (|v|)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Datatypes for contexts %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data Entry+> = Semicolon+> | Int :=? Maybe VT+> | Template ::: (Int, VT)+> deriving Show++> type Cx = (Bwd Entry, Int) -- a context and a nonce++> instance TMang Entry where+> tMang s Semicolon = (|Semicolon|)+> tMang s (q :=? mv) = (| ~q :=? tMang s mv|)+> tMang s (x ::: iv) = (| ~x ::: tMang s' iv|) where+> s' (VX i) = pure (X i)+> s' v = s v++> withTopEntry :: (Entry -> ElabM (Bwd Entry)) -> ElabM ()+> withTopEntry f = getCxE >>= \ (g, i) -> case g of+> B0 -> moanE $ Cockup "fell off the bottom of the context"+> g :< e -> do+> setCxE (g, i)+> h <- f e+> modCxE ((`mappend` h) *** id)++
Frank.cabal view
@@ -1,5 +1,5 @@ name: Frank-version: 0.0+version: 0.1 synopsis: An experimental programming language with typed algebraic effects description: An experimental programming language with typed algebraic effects license: PublicDomain@@ -17,6 +17,7 @@ build-depends: base < 5, void, newtype, mtl, she extensions: TypeOperators, KindSignatures, GADTs, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections, FunctionalDependencies, PatternGuards ghc-options: -F -pgmF she+ other-modules: Gubbins, Pa, Types, Template, Syntax, Check, ElabMonad, Unify, Elab, Run source-repository head type: darcs
+ Gubbins.lhs view
@@ -0,0 +1,143 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, FlexibleInstances, FunctionalDependencies,+> RankNTypes #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module Gubbins where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Control.Applicative+> import Control.Newtype+> import Control.Monad.Identity+> import Data.Void+> import Data.Monoid+> import Data.Foldable+> import Data.Traversable+> import Data.List+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Newtype instance for Identity %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> instance Newtype (Identity x) x where+> pack = Identity+> unpack (Identity x) = x+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Higher Kind Show %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> class ShowStarStar f where+> showStarStar :: Show x => f x -> String+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Free Monad, sort of %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data Free f x+> = Ret x+> | Com (forall t. (x -> Free f t) -> f (Free f t))++> instance Monad (Free f) where+> return = Ret+> Ret x >>= f = f x+> Com d >>= f = Com $ \ k -> d $ \ x -> f x >>= k++> com :: Functor f => f (Free f x) -> Free f x+> com ffx = Com $ \ k -> fmap (>>= k) ffx++> moc :: Free f x -> Either (f (Free f x)) x+> moc (Ret x) = Right x+> moc (Com f) = Left (f Ret)++> instance ShowStarStar f => ShowStarStar (Free f) where+> showStarStar c = case moc c of+> Right x -> "(Ret " ++ show x ++ ")"+> Left ffx -> "(Com " ++ showStarStar ffx ++ ")"+> instance (ShowStarStar f, Show x) => Show (Free f x) where+> show = showStarStar++> data (:>>:) s t x = s :? (t -> x)+> instance Functor (s :>>: t) where+> fmap k (s :? f) = s :? (k . f)+> instance Show s => ShowStarStar (s :>>: t) where+> showStarStar (s :? _) = "(" ++ show s ++ " :? ...)"+> instance (Show s, Show x) => Show ((s :>>: t) x) where+> show = showStarStar++> data (:+:) f g x = L (f x) | R (g x)+> instance (Functor f, Functor g) => Functor (f :+: g) where+> fmap k (L fx) = L (fmap k fx)+> fmap k (R gx) = R (fmap k gx)+> instance (ShowStarStar f, ShowStarStar g) => ShowStarStar (f :+: g) where+> showStarStar (L fx) = "(L " ++ showStarStar fx ++ ")"+> showStarStar (R gx) = "(R " ++ showStarStar gx ++ ")"+> instance (ShowStarStar f, ShowStarStar g, Show x)+> => Show ((f :+: g) x) where+> show = showStarStar+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Snoc-lists %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data Bwd x = B0 | Bwd x :< x deriving (Show, Eq, Ord)+> infixl 5 :<++Fish...++> (<><) :: Bwd x -> [x] -> Bwd x+> xz <>< [] = xz+> xz <>< (x : xs) = (xz :< x) <>< xs+> infixl 5 <><++...and chips++> (<>>) :: Bwd x -> [x] -> [x]+> B0 <>> xs = xs+> (xz :< x) <>> xs = xz <>> (x : xs)+> infixr 5 <>>++> instance Monoid (Bwd x) where+> mempty = B0+> mappend xz B0 = xz+> mappend xz (yz :< y) = mappend xz yz :< y++> instance Applicative Bwd where+> hiding instance Functor+> pure x = pure x :< x+> (fz :< f) <*> (sz :< s) = (fz <*> sz) :< f s+> _ <*> _ = B0++> instance Traversable Bwd where+> traverse f B0 = (|B0|)+> traverse f (xz :< x) = (|traverse f xz :< f x|)++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% UnionList %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> newtype UnionList x = UnionList [x] deriving (Show, Eq)+> instance Newtype (UnionList x) [x] where+> pack = UnionList+> unpack (UnionList x) = x+> instance Eq x => Monoid (UnionList x) where+> mempty = UnionList []+> mappend (UnionList a) (UnionList b) = UnionList (union a b)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Missing Traversables %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> instance Traversable ((,) a) where+> hiding instance Functor+> traverse f (a, b) = (| ~a, f b|)+
+ Pa.lhs view
@@ -0,0 +1,107 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, FlexibleInstances, TupleSections,+> GeneralizedNewtypeDeriving #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module Pa where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Data.Char+> import Data.Monoid+> import Control.Applicative+> import Control.Monad++> import Gubbins+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Brackets and Tokens %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data Brk = Rnd | Sqr | Crl deriving (Show, Eq)++> data Tok+> = TB Brk [Tok] Bool+> | TN String+> deriving Show+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Chunking (and lexing) %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> chunk :: String -> [[Tok]]+> chunk = snd . dent . lines where+> dent = foldr+> (\ s (d, gs) -> let sd = s ++ "\n" ++ d in+> if leftA s then ("", lx B0 [] sd : gs) else (sd , gs))+> ("", [])+> leftA (c : cs) = not (isSpace c)+> leftA _ = False++> lx :: Bwd Tok -> [(Brk, Bwd Tok)] -> String -> [Tok]+> lx tz [] [] = tz <>> []+> lx tz ((b, uz) : bs) [] = lx (uz :< TB b (tz <>> []) False) bs []+> lx tz bs ('(' : s) = lx B0 ((Rnd, tz) : bs) s+> lx tz ((Rnd, uz) : bs) (')' : s) = lx (uz :< TB Rnd (tz <>> []) True) bs s+> lx tz bs ('[' : s) = lx B0 ((Sqr, tz) : bs) s+> lx tz ((Sqr, uz) : bs) (']' : s) = lx (uz :< TB Sqr (tz <>> []) True) bs s+> lx tz bs ('{' : s) = lx B0 ((Crl, tz) : bs) s+> lx tz ((Crl, uz) : bs) ('}' : s) = lx (uz :< TB Crl (tz <>> []) True) bs s+> lx tz bs ('\'' : c : '\'' : s)+> | c /= '\\' = lx (tz :< TN ['\'', c, '\'']) bs s+> lx tz bs (c : s)+> | solo c = lx (tz :< TN [c]) bs s+> | isSpace c = lx tz bs s+> | otherwise = let (s0, s1) = span iddy s in lx (tz :< TN (c : s0)) bs s1+> where+> solo c = elem c ",;()[]{}!"+> iddy c = not (isSpace c || solo c)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Parser Monad %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> newtype Pa t x = Pa {pa :: [t] -> [(x, [t])]} deriving Monoid+> instance Monad (Pa t) where+> return x = Pa $ \ ts -> [(x, ts)]+> Pa f >>= k = Pa $ \ ts -> do+> (x, ts) <- f ts+> pa (k x) ts+> instance MonadPlus (Pa t) where+> mzero = mempty+> mplus = mappend++> tok :: (t -> [x]) -> Pa t x+> tok p = Pa $ \ ts -> case ts of+> t : ts -> map (, ts) (p t)+> _ -> []++> eof :: Pa t ()+> eof = Pa $ \ ts -> case ts of+> [] -> [((), [])]+> _ -> []++> sep :: Pa t () -> Pa t x -> Pa t [x]+> sep s p = (| p : many (|id (-s-) p|)+> | []+> |)++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Token-Specific Parsers %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> is :: String -> Pa Tok ()+> is s = tok $ \ t -> case t of+> TN s' | s == s' -> [()]+> _ -> []++> brk :: Brk -> Pa Tok x -> Pa Tok x+> brk b p = tok $ \ t -> case t of+> TB b' ts True | b == b' -> (|fst (pa (p <* eof) ts)|)+> _ -> []
+ Run.lhs view
@@ -0,0 +1,123 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, TypeSynonymInstances,+> FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,+> MultiParamTypeClasses #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module Run where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Prelude hiding (elem, all)+> import Data.Char+> import Data.List hiding (elem, all)+> import Data.Monoid+> import Data.Foldable+> import Data.Traversable+> import Control.Applicative+> import Control.Monad+> import Control.Newtype+> import Data.Void+> import Control.Arrow++> import Gubbins+> import Types+> import Pa+> import Syntax+> import Unify+> import Template+> import Check+> import Elab+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Operational Behaviour %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data VAL+> = VC Template [VAL]+> | VL Char+> | VU COMP+> | VR VAL+> | VO Template [VAL] VAL++> type COMP = [VAL] -> Free Frank VAL++> type Frank = (Template, [VAL]) :>>: VAL++> type Env = [VAL]++> eval :: [(Template, VAL)] -> Env -> TM {d} -> Free Frank VAL+> eval fs g (H (VA i)) = (|(g !! i)|)+> eval fs g (H (FN f)) =+> case lookup f fs of+> Just v -> (|v|)+> Nothing -> error ("Missing definition for " ++ show f)+> eval fs g (H (OP o)) = (|(VU $ \ vs -> com $ (o, vs) :? Ret)|)+> eval fs g (f :/ es) = (|apply (eval fs g f) (traverse (eval fs g) es) @ |)+> eval fs g (PApp f es) = do+> f <- eval fs g f+> us <- traverse (eval fs g) es+> (|(VU $ \ vs -> apply f (us ++ vs))|)+> eval fs g (HAN h e) = (|handle (eval fs g h) ~(eval fs g e) @ |)+> eval fs g (E e) = eval fs g e+> eval fs g (CN c es) = (|(VC c) (traverse (eval fs g) es)|)+> eval fs g (CL c) = (|(VL c)|)+> eval fs g (BUNK e) = eval fs g e -- seeya!+> eval fs g (LAM pes) = (|(VU (lambda fs g pes))|)++> apply :: VAL -> [VAL] -> Free Frank VAL+> apply (VU f) vs = f vs++> handle :: VAL -> Free Frank VAL -> Free Frank VAL+> handle (VU h) e = case moc e of+> Right v -> h [VR v]+> Left ((o, vs) :? k) -> case moc (h [VO o vs (VU (k . head))]) of+> Right v -> Ret v+> Left (([Mark "match"], []) :? _) -> com ((o, vs) :? (handle (VU h) . k))+> Left c -> com c++> lambda :: [(Template, VAL)] -> Env -> [([PAT], TM {CHK})] -> COMP+> lambda fs g ((ps, e) : pes) vs = case matches ps vs g of+> Just g -> eval fs g e+> Nothing -> lambda fs g pes vs+> lambda fs g [] vs = com (([Mark "match"], []) :? undefined) -- cheeky++> matches :: [PAT] -> [VAL] -> Env -> Maybe Env+> matches [] [] = return+> matches (p : ps) (v : vs) = match p v >=> matches ps vs++> match :: PAT -> VAL -> Env -> Maybe Env+> match (PV _) v = (|Just (v :)|)+> match (PC c ps) (VC d vs) | c == d = matches ps vs+> match (PL c) (VL d) | c == d = (|Just id|)+> match (PR p) (VR v) = match p v+> match (PO o ps p) (VO n vs v) | o == n = matches ps vs >=> match p v+> match _ _ = (|Nothing|)++> instance Show VAL where+> show (VC t vs) = tempShow t (map show vs)+> show (VL c) = show c+> show (VU _) = "{...}"+> show (VR v) = "!! VR " ++ show v+> show (VO o vs v) = "!! VO " ++ tempShow o (map show vs) ++ " " ++ show v++> display :: Free Frank VAL -> IO String+> display c = case moc c of+> Right v -> return $ show v+> Left (([Mark "inch"], []) :? k) -> do+> c <- getChar+> display (k (VL c))+> Left (([Mark "ouch"], [VL c]) :? k) -> do+> putChar c+> display (k (VC [] []))+> Left ((o, vs) :? k) -> return $ "Unhandled: " ++ tempShow o (map show vs)++> primitiveDefs :: [(Template, VAL)]+> primitiveDefs =+> [ ([Place, Mark "=Char=", Place], VU $ \ [VL c, VL d] -> Ret $+> if c == d then VC [Mark "tt"] [] else VC [Mark "ff"] [])+> ]
+ Syntax.lhs view
@@ -0,0 +1,231 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, TypeSynonymInstances,+> FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections,+> MultiParamTypeClasses #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module Syntax where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Prelude hiding (elem, all)+> import Data.Char+> import Data.List hiding (elem, all)+> import Data.Monoid+> import Data.Foldable+> import Data.Traversable+> import Control.Applicative+> import Control.Monad+> import Control.Newtype++> import Types+> import Pa+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% top level Source %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data Source = Source+> { sourceData :: [(UpId, ([UpId], [[Lump]]))]+> , sourceSigs :: [(UpId, ([UpId], [([Lump], VT)]))]+> , sourceDecl :: [([Lump], ([Sig], VT))]+> , sourceDefs :: [([Pat], Raw)]+> , sourceNote :: [[Tok]]+> , sourceJunk :: [[Tok]]+> } deriving Show++> instance Monoid Source where+> mempty = Source [] [] [] [] [] []+> mappend (Source x1 x2 x3 x4 x5 x6) (Source y1 y2 y3 y4 y5 y6) =+> Source (x1 ++ y1) (x2 ++ y2) (x3 ++ y3) (x4 ++ y4) (x5 ++ y5) (x6 ++ y6)++> source :: String -> Source+> source = foldMap ch . chunk where+> ch ts = +> case (pa dataP ts, pa sgdP ts, pa declP ts, pa lineP ts, pa noteP ts) of+> ([(d, [])], [], [], [], []) -> Source [d] [] [] [] [] []+> ([], [(s, [])], [], [], []) -> Source [] [s] [] [] [] []+> ([], [], [(f, [])], [], []) -> Source [] [] [f] [] [] []+> ([], [], [], [(l, [])], []) -> Source [] [] [] [l] [] []+> ([], [], [], [], [(n, [])]) -> Source [] [] [] [] [n] []+> _ -> Source [] [] [] [] [] [ts]++> data Lump = LNm String | LTy VT++> instance Show Lump where+> show (LNm x) = x+> show (LTy t) = show t++> instance TMang Lump where+> tMang s (LNm x) = (|LNm ~x|)+> tMang s (LTy t) = (|LTy (tMang s t)|)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% datatypes for Raw terms and patterns %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data Raw+> = RN String+> | RA [Raw]+> | RCh Char+> | RVd+> | RBunk+> | RBang+> | RTh [([Pat],Raw)]+> | RQ Raw Raw+> deriving Show++> data Pat+> = PN String+> | PCh Char+> | PVd+> | PA [Pat]+> | PRet Pat+> | POp [Pat] Pat+> deriving Show+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% top level chunks %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> dataP :: Pa Tok (UpId, ([UpId], [[Lump]]))+> dataP = (| (,) (-is "data"-) upid+> (|(,) (many upid) (-is "="-) (sep (is "|") nomTys) (-eof-) |)+> |)++> sgdP :: Pa Tok (UpId, ([UpId], [([Lump], VT)]))+> sgdP = (| (,) (-is "sig"-) upid+> (|(,) (many upid) (-is "="-) +> (sep (is "|")+> (|nomTys,+> (| id (-brk Sqr eof-) (| id bigVT | Un |) | Un |)|))+> (-eof-) |)+> |)++> declP :: Pa Tok ([Lump], ([Sig], VT))+> declP = (|(,) nomTys (|(brk Sqr sigsP), (| id bigVT | Un |) | ([], Un) |)+> (-eof-)|)++> lineP :: Pa Tok ([Pat], Raw)+> lineP = (|(,) (some patP) (-is "="-) bigRaw (-eof-)|)++> noteP :: Pa Tok [Tok]+> noteP = (|id (-is "note"-) (many (tok return)) (-eof-)|)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% parsing types %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> weeVT :: Pa Tok VT+> weeVT = (| D upid ~[]+> | id (brk Sqr (|M sigsP (-is "?"-)+> (| id (brk Sqr sigsP) | [] |) bigVT|))+> | Ze (-brk Crl eof-)+> | Un (-brk Rnd eof-)+> | U (brk Crl bigCT)+> | id (brk Rnd bigVT)+> |)++> bigVT :: Pa Tok VT+> bigVT = (| D upid (some weeVT)+> | id weeVT+> |)++> bigCT :: Pa Tok CT+> bigCT = (| bigVT :-> (-is "->"-) bigCT+> | F (| id (brk Sqr sigsP) | [] |) bigVT+> |)++> nomTys :: Pa Tok [Lump]+> nomTys = some (| LNm nom | LTy weeVT |)++> sigP :: Pa Tok Sig+> sigP = (| Pure (-brk Crl eof -)+> | upid :$ (many weeVT)+> |)++> sigsP :: Pa Tok [Sig]+> sigsP = sep (is ",") sigP+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% keywords and identifiers %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> keywords :: [String]+> keywords = ["note","sig", "data", "->", ";", ",", "=", "|", "!","?"]++> nom :: Pa Tok String+> nom = tok $ \ t -> case t of+> TN x@(c:_)+> | not (c == '\''), not (isUpper c), not (elem x keywords) -> [x]+> _ -> []++> upid :: Pa Tok UpId+> upid = tok $ \ t -> case t of+> TN x@(c:_) | isUpper c, not (elem x keywords) -> [Up x]+> _ -> []++> lit :: Pa Tok Char+> lit = tok $ \ t -> case t of+> TN ['\'',c,'\''] | c /= '\\' -> [c]+> TN ['\'','\\',c,'\''] -> [d| (c', d) <- escapees, c' == c]+> _ -> []+> where+> escapees =+> [ ('\'', '\'')+> , ('\"', '\"')+> , ('\\', '\\')+> , ('n', '\n')+> , ('r', '\r')+> , ('t', '\t')+> , ('b', '\b')+> ]+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% parsing raw terms and patterns %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> bigRaw :: Pa Tok Raw+> bigRaw = (| RQ medRaw (-is "?"-) bigRaw+> | id medRaw+> |)++> medRaw :: Pa Tok Raw+> medRaw = (| RA (|weeRaw : some weeRaw|)+> | id weeRaw+> |)++> weeRaw :: Pa Tok Raw+> weeRaw = (| RBang (-is "!"-)+> | RN nom+> | RCh lit+> | RVd (-brk Rnd eof-)+> | id (brk Rnd bigRaw)+> | RBunk (-brk Crl eof-)+> | RTh (brk Crl (|clauseP : many (|id (-is "|"-) clauseP|)|))+> |)++> clauseP :: Pa Tok ([Pat], Raw)+> clauseP = (| some patP, (-is "->"-) bigRaw+> | ~[], bigRaw+> |)++> patP :: Pa Tok Pat+> patP = (| PN nom+> | PCh lit+> | PVd (-brk Rnd eof-)+> | PA (brk Rnd (some patP))+> | PRet (brk Sqr patP)+> | id (brk Sqr (|POp (some patP) (-is "?"-) patP|))+> |)++
+ Template.lhs view
@@ -0,0 +1,123 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, FlexibleInstances, MultiParamTypeClasses #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module Template where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Prelude hiding (elem, any)+> import Control.Applicative+> import Control.Monad+> import Data.Foldable+> import Data.Monoid++> import Pa+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Templates %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> type Template = [TBit]+> data TBit = Place | Mark String deriving (Eq, Ord)++> prefix :: Template -> Bool+> prefix (Mark _ : _ : _) = True+> prefix _ = False++> postfix :: Template -> Bool+> postfix (Place : _) = True+> postfix _ = False++> tempShow :: Template -> [String] -> String+> tempShow [Mark c] [] = c+> tempShow bs ss = "(" ++ splice False bs ss ++ ")" where+> splice _ [] [] = ""+> splice True bs ss = " " ++ splice False bs ss+> splice _ [] (s : ss) = s ++ splice True [] ss+> splice _ (Mark m : bs) ss = m ++ splice True bs ss+> splice _ (Place : bs) (s : ss) = s ++ splice True bs ss+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Template Tables %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data TemplateTable = TemplateTable+> { ttTemplates :: [Template] -- what are the templates+> , ttPrecedence :: [(Template, Template)] -- what's outside what+> , ttAssocs :: [(Template, Int)] -- which place associates+> } deriving Show++> punc :: TemplateTable -> String -> Bool+> punc tt s = elem s [x | bs <- ttTemplates tt, Mark x <- bs]++> gassocs :: TemplateTable -> Template -> (Template, Int)+> gassocs tbl t = case lookup t (ttAssocs tbl) of+> Just i -> (t , i)+> _ -> (t , negate 1)++> prLT :: TemplateTable -> ([TBit], Int) -> [TBit] -> Bool+> prLT tbl ([], _) _ = True+> prLT tbl (x, 0) y | x == y = True+> prLT tbl _ [_] = True+> prLT tbl (x, _) y = grLT (ttPrecedence tbl) x y where+> grLT g x y = x /= y && grLE g x y+> grLE g x y | x == y = True+> grLE g x y = any (grLE g x) [z | (z, y') <- g, y == y']+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Templates %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> data TTree x+> = TLeaf x [TTree x]+> | TNode Template [TTree x]+> deriving Show++> tApp :: TTree x -> [TTree x] -> TTree x+> tApp (TLeaf x xs) ys = TLeaf x (xs ++ ys)+> tApp (TNode t xs) ys = TNode t (xs ++ ys)++> resolve :: TemplateTable -> Pa (Either String x) (TTree x)+> resolve tbl = big ([], 0) <* eof where+> is s = tok $ either (guard . (s ==)) mempty+> big ti = (| (mafter ti) medium @ |)+> medium = (| safter small @ |) <|>+> foldMap (\ t -> (| (TNode t) (tmpl t (gassocs tbl t)) |)) pres+> small = tok (either single (return . (`TLeaf` [])))+> mafter ti s = (| (mafter ti) more @ | s |) where+> more = (| id (foldMap+> (\ t -> (| (TNode t . (s :))+> (tmpl t (dock (gassocs tbl t))) |))+> possibles)+> |)+> dock (x : xs, i) = (xs, i - 1)+> possibles = filter (\ u -> postfix u && prLT tbl ti u && grabs s u)+> (ttTemplates tbl)+> grabs (TNode t _) u = prLT tbl (gassocs tbl u) t+> grabs _ _ = True+> safter s = (| safter (| (tApp s . return) small |) @ | s |) where+> tmpl t ([], _) = (|[]|)+> tmpl t (Mark s : ts, i) = (| id (-is s-) (tmpl t (ts, i)) |)+> tmpl t (Place : ts, i) = (| big (t, i) : tmpl t (ts, i - 1) |)+> pres = filter prefix (ttTemplates tbl)+> single t | elem [Mark t] (ttTemplates tbl)+> = [TNode [Mark t] []]+> | otherwise = []+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Show Instances %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> instance Show TBit where+> show Place = "_"+> show (Mark x) = x++
+ Types.lhs view
@@ -0,0 +1,159 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, FlexibleInstances #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module Types where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Control.Newtype+> import Control.Applicative+> import Control.Monad.Identity+> import Data.Traversable+> import Data.List++> import Gubbins+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Datatypes for types %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++Frank has *value types*...++> data VT+> = Ze -- empty type {}+> | Un -- unit type ()+> | U CT -- thunked computation type {C}+> | D UpId [VT] -- type constructor with params D V1 .. Vn+> | M [Sig] [Sig] VT -- message from the first bunch+> | X Int -- rigid type variable X+> | Q Int -- flexible type variable ?X++... and *computation types*.++> data CT+> = VT :-> CT -- function type V -> C+> | F [Sig] VT -- effectful value type [Ss] V+> infixr 4 :->++Types are named by UpId identifiers, beginning in uppercase.++> newtype UpId = Up {ui :: String} deriving (Show, Eq, Ord)++Signatures are named and parametrized.++> data Sig+> = (:$) {sigU :: UpId, sigPs :: [VT]}+> | Pure++++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% The very nice mangler %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> class TMang t where+> tMang :: Applicative f => (Var -> f VT) -> t -> f t++> data Var = VD UpId | VX Int | VQ Int+> vD :: UpId -> VT+> vD u = D u []+> var :: (UpId -> x) -> (Int -> x) -> (Int -> x) -> Var -> x+> var vd vx vq (VD u) = vd u+> var vd vx vq (VX i) = vx i+> var vd vx vq (VQ i) = vq i++> instance TMang VT where+> tMang s Ze = (|Ze|)+> tMang s Un = (|Un|)+> tMang s (U c) = (|U (tMang s c)|)+> tMang s (D u []) = s (VD u)+> tMang s (D u vs) = (|D ~u (tMang s vs)|)+> tMang s (M os ss v) = (|M (tMang s os) (tMang s ss) (tMang s v) |)+> tMang s (X i) = s (VX i)+> tMang s (Q i) = s (VQ i)++> instance TMang CT where+> tMang s (v :-> c) = (|tMang s v :-> tMang s c|)+> tMang s (F ss v) = (|F (tMang s ss) (tMang s v)|)++> instance TMang Sig where+> tMang s (u :$ vs) = (| ~u :$ tMang s vs|)+> tMang s Pure = (|Pure|)++> instance TMang x => TMang [x] where+> tMang = traverse . tMang++> instance TMang x => TMang (Maybe x) where+> tMang = traverse . tMang++> instance (TMang x, TMang y) => TMang (x, y) where+> tMang s (x, y) = (|tMang s x, tMang s y|)++> instance TMang Int where+> tMang s = pure++> xsub :: (TMang t) => [VT] -> t -> t+> xsub vs = ala' Identity tMang (var vD (bof vs) Q) where+> bof [] i = X i+> bof (x : xs) 0 = x+> bof (x : xs) i = bof xs (i - 1)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Sig Action %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++A signature acts on a collection of signatures by shadowing or+disabling. (Might add individual disabling?) We lift structurally.++> class SigAct t where+> sAct :: t -> [Sig] -> t++> instance SigAct [Sig] where+> sAct sa ss = foldr s1 ss sa where+> s1 Pure _ = []+> s1 s@(f :$ _) ss = s : [s' | s'@(f' :$ _) <- ss, f' /= f]++> instance SigAct VT where+> sAct (U c) ss = U (sAct c ss)+> sAct (D n vs) ss = D n (map (`sAct` ss) vs) -- really?+> sAct (M os sa v) ss = M os (sAct sa ss) (sAct v ss)+> sAct t ss = t++> instance SigAct CT where+> sAct (F sa v) ss = F (sAct sa ss) (sAct v ss)+> sAct (v :-> c) ss = sAct v ss :-> sAct c ss++++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Show instances %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> instance Show VT where+> show Ze = "{}"+> show Un = "()"+> show (U c) = "{" ++ show c ++ "}"+> show (D u []) = ui u+> show (D u vs) = "(" ++ ui u ++ (vs >>= ((' ' :) . show)) ++ ")"+> show (M os ss v)+> = "[" ++ intercalate ", " (map show os) ++ " ? "+> ++ (if null ss then "" else "[" ++ intercalate ", " (map show ss) ++ "]")+> ++ show v ++ "]"+> show (X i) = "#" ++ show i+> show (Q i) = "?" ++ show i++> instance Show CT where+> show (v :-> c) = show v ++ " -> " ++ show c+> show (F [] v) = show v+> show (F (s : ss) v)+> = "[" ++ show s ++ (ss >>= ((", " ++) . show)) ++ "] " ++ show v++> instance Show Sig where+> show (u :$ vs) = ui u ++ (vs >>= ((' ' :) . show))+> show Pure = "{}"
+ Unify.lhs view
@@ -0,0 +1,114 @@+> {-# OPTIONS_GHC -F -pgmF she #-}+> {-# LANGUAGE TypeOperators, FunctionalDependencies,+> FlexibleContexts #-}++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> module Unify where++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> import Debug.Trace++> import Control.Newtype+> import Control.Applicative+> import Control.Monad+> import Control.Arrow+> import Data.Monoid+> import Data.Void+> import Data.Function+> import Data.List++> import Gubbins+> import Types+> import Template+> import Check+> import ElabMonad+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Unification Class %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> class Unify t where+> (=?=) :: t -> t -> ElabM ()+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Unification Instances %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> instance Unify VT where+> --s =?= t | trace (show s ++ " =?= " ++ show t) False = undefined+> Ze =?= Ze = return ()+> Un =?= Un = return ()+> U b =?= U c = b =?= c+> D b us =?= D c vs | b == c = us =?= vs+> X i =?= X j | i == j = return ()+> Q i =?= Q j = if i == j then return () else identify i j+> Q i =?= v = solve i [] v+> v =?= Q i = solve i [] v+> s =?= t = moanE $ UnifyVFail s t++> instance Unify CT where+> (u :-> b) =?= (v :-> c) = do u =?= v; b =?= c+> F rr u =?= F ss v = do+> sortBy (compare `on` sigU) rr =?= sortBy (compare `on` sigU) ss+> u =?= v+> s =?= t = moanE $ UnifyCFail s t++> instance Unify Sig where+> (x :$ us) =?= (y :$ vs) | x == y = us =?= vs+> s =?= t = moanE $ UnifySFail s t++> instance Unify t => Unify [t] where+> [] =?= [] = return ()+> (a : as) =?= (b : bs) = do a =?= b; as =?= bs+> _ =?= _ = moanE $ Cockup "arity mismatch"+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Occur Check %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++> qoccur :: TMang t => Int -> t -> Bool+> qoccur q = ala' Any (ala' Const tMang) $+> var (const False) (const False) (q ==)+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%%%%% Identification and Solving %%%%%+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++|identify i j| assumes |i| is not |j|++> identify :: Int -> Int -> ElabM ()+> identify i j = do+> --(g, _) <- getCxE+> --False <- trace ("IDENTIFY " ++ show g ++ show (i, j)) $ return False+> withTopEntry $ \ e -> case e of+> k :=? Nothing+> | k == i -> return (B0 :< (k :=? Just (Q j)))+> | k == j -> return (B0 :< (k :=? Just (Q i)))+> k :=? Just v+> | k == i -> solve j [] v >> return (B0 :< e)+> | k == j -> solve i [] v >> return (B0 :< e)+> _ -> identify i j >> return (B0 :< e)++|solve q es v| assumes |v| is not |Q q|++> solve :: Int -> [Entry] -> VT -> ElabM ()+> solve q es v = do+> --(g, _) <- getCxE+> --False <- trace ("SOLVE " ++ show g ++ show (q, es, v)) $ return False+> withTopEntry $ \ e -> case e of+> q' :=? mu | q' == q ->+> if qoccur q es || qoccur q v+> then moanE $ UnifyVFail (Q q) v+> else case mu of+> Nothing -> return (B0 <>< es :< (q :=? Just v))+> Just u -> do modCxE ((<>< es) *** id); u =?= v; return (B0 :< e)+> q' :=? _ | qoccur q' es || qoccur q' v -> solve q (e : es) v >> return B0+> e -> solve q es v >> return (B0 :< e)