module Annah.Core (
M.Var(..)
, M.Const(..)
, Arg(..)
, Let(..)
, Data(..)
, Type(..)
, Bind(..)
, Expr(..)
, desugar
, desugarFamily
, desugarNatural
, desugarDo
, desugarList
, desugarPath
, desugarLets
) where
import Control.Applicative (pure, empty)
import Data.String (IsString(..))
import Data.Text.Lazy (Text)
import qualified Morte.Core as M
import Prelude hiding (pi)
data Arg = Arg
{ argName :: Text
, argType :: Expr
} deriving (Show)
data Let = Let
{ letName :: Text
, letArgs :: [Arg]
, letType :: Expr
, letRhs :: Expr
} deriving (Show)
data Type = Type
{ typeName :: Text
, typeDatas :: [Data]
, typeFold :: Text
} deriving (Show)
data Data = Data
{ dataName :: Text
, dataArgs :: [Arg]
} deriving (Show)
data Bind = Bind
{ bindLhs :: Arg
, bindRhs :: Expr
} deriving (Show)
data Expr
= Const M.Const
| Var M.Var
| Lam Text Expr Expr
| Pi Text Expr Expr
| App Expr Expr
| Annot Expr Expr
| Lets [Let] Expr
| Family [Type] Expr
| Natural Integer
| List Expr [Expr]
| Path Expr [(Expr, Expr)] Expr
| Do Expr [Bind] Bind
| Embed M.Path
deriving (Show)
instance IsString Expr where
fromString str = Var (fromString str)
desugar
:: Expr
-> M.Expr M.Path
desugar (Const c ) = M.Const c
desugar (Var v ) = M.Var v
desugar (Lam x _A b ) = M.Lam x (desugar _A) (desugar b)
desugar (Pi x _A _B ) = M.Pi x (desugar _A) (desugar _B)
desugar (App f a ) = M.App (desugar f) (desugar a)
desugar (Embed p ) = M.Embed p
desugar (Annot a _A ) = desugar (Lets [Let "x" [] _A a] "x")
desugar (Lets ls e ) = desugarLets ls e
desugar (Family ts e ) = desugarLets (desugarFamily ts) e
desugar (Natural n ) = desugarNatural n
desugar (List t es ) = desugarList t es
desugar (Path t oms o) = desugarPath t oms o
desugar (Do m bs b ) = desugarDo m bs b
desugarNatural :: Integer -> M.Expr M.Path
desugarNatural n0 =
M.Lam "Nat" (M.Const M.Star)
(M.Lam "Succ" (M.Pi "pred" (M.Var (M.V "Nat" 0)) (M.Var (M.V "Nat" 0)))
(M.Lam "Zero" (M.Var (M.V "Nat" 0))
(go0 n0) ) )
where
go0 n | n <= 0 = M.Var (M.V "Zero" 0)
| otherwise = M.App (M.Var (M.V "Succ" 0)) (go0 (n 1))
desugarList :: Expr -> [Expr] -> M.Expr M.Path
desugarList e0 ts0 =
M.Lam "List" (M.Const M.Star)
(M.Lam "Cons" (M.Pi "head" (desugar0 e0) (M.Pi "tail" "List" "List"))
(M.Lam "Nil" "List" (go ts0)) )
where
go [] = "Nil"
go (t:ts) = M.App (M.App "Cons" (desugar1 t)) (go ts)
desugar0 = M.shift 1 "List" . desugar
desugar1 = M.shift 1 "List" . M.shift 1 "Cons" . M.shift 1 "Nil" . desugar
desugarPath
:: Expr
-> [(Expr, Expr)]
-> Expr
-> M.Expr M.Path
desugarPath c0 oms0 o0 =
M.Lam "Path"
(M.Pi "a" (M.Const M.Star) (M.Pi "b" (M.Const M.Star) (M.Const M.Star)))
(M.Lam "Step"
(M.Pi "a" (M.Const M.Star)
(M.Pi "b" (M.Const M.Star)
(M.Pi "c" (M.Const M.Star)
(M.Pi "head" (M.App (M.App (desugar0 c0) "a") "b")
(M.Pi "tail" (M.App (M.App "Path" "b") "c")
(M.App (M.App "Path" "a") "c") ) ) ) ) )
(M.Lam "End"
(M.Pi "a" (M.Const M.Star) (M.App (M.App "Path" "a") "a"))
(go oms0) ) )
where
desugar0
= M.shift 1 "Path"
. M.shift 1 "a"
. M.shift 1 "b"
. M.shift 1 "c"
. desugar
desugar1
= M.shift 1 "Path"
. M.shift 1 "Step"
. M.shift 1 "End"
. desugar
go [] = M.App "End" (desugar1 o0)
go [(o1, m1)] =
M.App (M.App (M.App (M.App (M.App "Step" o1') o0') o0') m1') (go [] )
where
o0' = desugar1 o0
o1' = desugar1 o1
m1' = desugar1 m1
go ((o1, m1):oms@((o2, _):_)) =
M.App (M.App (M.App (M.App (M.App "Step" o1') o2') o0') m1') (go oms)
where
o0' = desugar1 o0
o1' = desugar1 o1
o2' = desugar1 o2
m1' = desugar1 m1
desugarDo :: Expr -> [Bind] -> Bind -> M.Expr M.Path
desugarDo m bs0 (Bind (Arg x0 _A0) e0) =
M.Lam "Cmd" (M.Const M.Star)
(M.Lam "Bind"
(M.Pi "b" (M.Const M.Star)
(M.Pi "_" (M.App (desugar0 m) "b")
(M.Pi "_" (M.Pi "_" "b" "Cmd") "Cmd") ) )
(M.Lam "Pure" (M.Pi x0 (desugar1 _A0) "Cmd")
(go bs0 (0 :: Int) (0 :: Int)) ) )
where
desugar0
= M.shift 1 "b"
. M.shift 1 "Cmd"
. desugar
desugar1
= M.shift 1 "Bind"
. M.shift 1 "Cmd"
. desugar
desugar2
= M.shift 1 "Pure"
. M.shift 1 "Bind"
. M.shift 1 "Cmd"
. desugar
go [] numPure numBind =
M.App
(M.App (M.App (M.Var (M.V "Bind" numBind)) (desugar2 _A0))
(desugar2 e0) )
(M.Var (M.V "Pure" numPure))
go (Bind (Arg x _A) e:bs) numPure numBind = numBind' `seq` numPure' `seq`
M.App
(M.App
(M.App (M.Var (M.V "Bind" numBind)) (desugar2 _A))
(desugar2 e) )
(M.Lam x (desugar2 _A) (go bs numBind' numPure'))
where
numBind' = if x == "Bind" then numBind + 1 else numBind
numPure' = if x == "Pure" then numPure + 1 else numPure
desugarLets :: [Let] -> Expr -> M.Expr M.Path
desugarLets lets e = apps
where
lams = foldr
(\(Let fn args _Bn _) rest ->
let rhsType = pi args _Bn
in M.Lam fn (desugar rhsType) rest )
(desugar e)
lets
apps = foldr
(\(Let _ args _ bn) rest ->
M.App rest (desugar (lam args bn)) )
lams
(reverse lets)
data Cons = Cons
{ consName :: Text
, consArgs :: [Arg]
, consType :: Expr
}
desugarFamily :: [Type] -> [Let]
desugarFamily familyTypes = typeLets ++ dataLets ++ foldLets
where
typeConstructors :: [Cons]
typeConstructors = do
t <- familyTypes
return (Cons (typeName t) [] (Const M.Star))
dataConstructors :: [Cons]
dataConstructors = do
(tsBefore , t, tsAfter) <- zippers familyTypes
(dsBefore1, d, _ ) <- zippers (typeDatas t)
let dsBefore0 = do
t' <- tsBefore
typeDatas t'
let names1 = map typeName tsAfter
let names2 = map dataName dsBefore0
let names3 = map dataName dsBefore1
let names4 = map argName (dataArgs d)
let typeVar =
typeName t `isShadowedBy` (names1 ++ names2 ++ names3 ++ names4)
return (Cons (dataName d) (dataArgs d) typeVar)
constructors :: [Cons]
constructors = typeConstructors ++ dataConstructors
makeRhs piOrLam con = foldr cons con constructors
where
cons (Cons x args _A) = piOrLam x (pi args _A)
typeLets, foldLets :: [Let]
(typeLets, foldLets) = unzip (do
let folds = map typeFold familyTypes
((_, t, tsAfter), fold) <- zip (zippers typeConstructors) folds
let names1 = map consName tsAfter
let names2 = map consName dataConstructors
let con = consName t `isShadowedBy` (names1 ++ names2)
let typeRhs = makeRhs Pi con
let foldType = Pi "x" con typeRhs
let foldRhs = Lam "x" typeRhs "x"
return ( Let (consName t) [] (consType t) typeRhs
, Let fold [] foldType foldRhs
) )
desugarType :: Expr -> Maybe ([Arg], Expr, Expr)
desugarType (Pi x _A e ) = do
~(args, f, f') <- desugarType e
return (Arg x _A:args, f, f')
desugarType f@(Var (M.V x0 n0)) = do
f' <- go0 dataConstructors x0 n0
return ([], f, f')
where
go0 (d:ds) x n | consName d == x =
if n > 0 then go0 ds x $! n 1 else empty
| otherwise = go0 ds x n
go0 [] x n = go1 (reverse typeLets) x n
go1 (t:ts) x n | letName t == x =
if n > 0 then go1 ts x $! n 1 else pure (letRhs t)
| otherwise = go1 ts x n
go1 [] _ _ = empty
desugarType _ = empty
consVars :: [Text] -> [Expr]
consVars argNames = do
(_, name, namesAfter) <- zippers (map consName constructors)
return (name `isShadowedBy` (argNames ++ namesAfter))
dataLets :: [Let]
dataLets = do
(_, d, dsAfter) <- zippers dataConstructors
let conVar = consName d `isShadowedBy` map consName dsAfter
let conArgs = do
(_, arg, argsAfter) <- zippers (consArgs d)
let names1 = map argName argsAfter
let names2 = map consName constructors
return (case desugarType (argType arg) of
Nothing -> argVar
where
names = names1 ++ names2
argVar = argName arg `isShadowedBy` names
Just (args, _, _) ->
lam args (apply argVar (argExprs ++ consVars names3))
where
names3 = map argName args
names = names1 ++ names2 ++ names3
argVar = argName arg `isShadowedBy` names
argExprs = do
(_, name, namesAfter) <- zippers names3
return (name `isShadowedBy` namesAfter) )
let (lhsArgs, rhsArgs) = unzip (do
arg@(Arg x _A) <- consArgs d
return (case desugarType _A of
Just (args, _B, _B') -> (lhsArg, rhsArg)
where
lhsArg = Arg x (pi args _B )
rhsArg = Arg x (pi args _B')
Nothing -> ( arg, arg) ) )
let letType' = pi lhsArgs (consType d)
let letRhs' = lam rhsArgs (makeRhs Lam (apply conVar conArgs))
return (Let (consName d) [] letType' letRhs')
apply :: Expr -> [Expr] -> Expr
apply f as = foldr (flip App) f (reverse as)
isShadowedBy :: Text -> [Text] -> Expr
x `isShadowedBy` vars = Var (M.V x (length (filter (== x) vars)))
pi, lam :: [Arg] -> Expr -> Expr
pi args e = foldr (\(Arg x _A) -> Pi x _A) e args
lam args e = foldr (\(Arg x _A) -> Lam x _A) e args
zippers :: [a] -> [([a], a, [a])]
zippers [] = []
zippers (stmt:stmts') = z:go z
where
z = ([], stmt, stmts')
go ( _, _, [] ) = []
go (ls, m, r:rs) = z':go z'
where
z' = (m:ls, r, rs)