{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE CPP #-}

-- | Load and parse '.l3' files
module L3.Loader.Loader
  ( wrapPrelude,
    embeddedPrelude,
    embeddedPreludeIO,
    takeDirectoryName,
    takeNamespacedFileName,
    loadPrelude,
    tauSubst,
    tauNorm,
  )
where

import Data.Bifunctor (bimap, first, second)
import Data.ByteString (ByteString)
import Data.FileEmbed (embedDir, embedDirListing, getDir)
import Data.List (partition)
import qualified Data.Text (unpack)
import Data.Text.Encoding (decodeUtf8)
import L3.Core
import L3.Log
import L3.Parse
import L3.Util
import System.FilePath
import Prelude hiding (FilePath, error)

trace :: String -> a -> a
trace = String -> String -> a -> a
forall a. String -> String -> a -> a
traceU String
"Loader"

debugIO :: String -> IO ()
debugIO = String -> String -> IO ()
debugM String
"Loader"

-- | Get the last directory name from a path
takeDirectoryName :: FilePath -> String
takeDirectoryName :: String -> String
takeDirectoryName String
p = String -> String -> String
forall a. String -> a -> a
trace (String
"takeDirectoryName " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
p) (String -> String
takeDirectoryName' String
p)

takeDirectoryName' :: String -> String
takeDirectoryName' = [String] -> String
forall a. [a] -> a
last ([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
splitPath (String -> [String]) -> (String -> String) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeDirectory

-- | Format a file into either non-namespaced `file` or namespaced `dir`@`file`
takeNamespacedFileName :: FilePath -> String
takeNamespacedFileName :: String -> String
takeNamespacedFileName String
f = String -> String -> String
forall a. String -> a -> a
trace (String
"takeNamespacedFileName " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
f) (String -> String
takeNamespacedFileName' String
f)

takeNamespacedFileName' :: String -> String
takeNamespacedFileName' String
f = case (String -> (String, String)
splitFileName (String -> (String, String))
-> (String -> String) -> String -> (String, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
dropExtension) String
f of
  (String
"./", String
file) -> String
file
  (String
ns, String
"@") -> String -> String
forall a. [a] -> [a]
init String
ns
  (String
ns, String
file) -> String -> String
forall a. [a] -> [a]
init String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file

embeddedPreludeIO :: IO [(FilePath, ByteString)]
embeddedPreludeIO :: IO [(String, ByteString)]
embeddedPreludeIO = String -> IO ()
debugIO String
"embeddedPreludeIO" IO () -> IO [(String, ByteString)] -> IO [(String, ByteString)]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO [(String, ByteString)]
embeddedPreludeIO'

embeddedPreludeIO' :: IO [(String, ByteString)]
embeddedPreludeIO' = ((String, ByteString) -> Bool)
-> [(String, ByteString)] -> [(String, ByteString)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
".l3") (String -> Bool)
-> ((String, ByteString) -> String) -> (String, ByteString) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeExtension (String -> String)
-> ((String, ByteString) -> String)
-> (String, ByteString)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, ByteString) -> String
forall a b. (a, b) -> a
fst) ([(String, ByteString)] -> [(String, ByteString)])
-> IO [(String, ByteString)] -> IO [(String, ByteString)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO [(String, ByteString)]
getDir String
"prelude"

-- | Embed and retrieve all '.l3' files in the prelude directory
embeddedPrelude :: [(FilePath, ByteString)]
embeddedPrelude :: [(String, ByteString)]
embeddedPrelude = String -> [(String, ByteString)] -> [(String, ByteString)]
forall a. String -> a -> a
trace String
"embeddedPrelude" [(String, ByteString)]
embeddedPrelude'

embeddedPrelude' :: [(String, ByteString)]
embeddedPrelude' = ((String, ByteString) -> Bool)
-> [(String, ByteString)] -> [(String, ByteString)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
".l3") (String -> Bool)
-> ((String, ByteString) -> String) -> (String, ByteString) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeExtension (String -> String)
-> ((String, ByteString) -> String)
-> (String, ByteString)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, ByteString) -> String
forall a b. (a, b) -> a
fst) $(embedDir "prelude")

-- | Lex and parse the prelude into a type-context and expression-context
loadPrelude :: [(FilePath, ByteString)] -> (ShowCtx, ShowCtx)
loadPrelude :: [(String, ByteString)] -> (ShowCtx, ShowCtx)
loadPrelude [(String, ByteString)]
embedded = String -> (ShowCtx, ShowCtx) -> (ShowCtx, ShowCtx)
forall a. String -> a -> a
trace (String
"loadPrelude " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, ByteString)] -> String
forall a. Show a => a -> String
show [(String, ByteString)]
embedded) ([(String, ByteString)] -> (ShowCtx, ShowCtx)
loadPrelude' [(String, ByteString)]
embedded)

loadPrelude' :: [(String, ByteString)] -> (ShowCtx, ShowCtx)
loadPrelude' [(String, ByteString)]
embedded = ([(Name, Expr Name)] -> ShowCtx
forall a. [(a, Expr a)] -> Context a
Ctx [(Name, Expr Name)]
τ, [(Name, Expr Name)] -> ShowCtx
forall a. [(a, Expr a)] -> Context a
Ctx [(Name, Expr Name)]
ε)
  where
    preludeExprs :: [(String, Expr Name)]
preludeExprs = ((String, ByteString) -> (String, Expr Name))
-> [(String, ByteString)] -> [(String, Expr Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((ByteString -> Expr Name)
-> (String, ByteString) -> (String, Expr Name)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Result (Expr Name) -> Expr Name
forall a. Result a -> a
throwL (Result (Expr Name) -> Expr Name)
-> (ByteString -> Result (Expr Name)) -> ByteString -> Expr Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Result (Expr Name)
parseExpr ([Token] -> Result (Expr Name))
-> (ByteString -> [Token]) -> ByteString -> Result (Expr Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result [Token] -> [Token]
forall a. Result a -> a
throwL (Result [Token] -> [Token])
-> (ByteString -> Result [Token]) -> ByteString -> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Result [Token]
lexSrc (String -> Result [Token])
-> (ByteString -> String) -> ByteString -> Result [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
Data.Text.unpack (Text -> String) -> (ByteString -> Text) -> ByteString -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Text
decodeUtf8)) [(String, ByteString)]
embedded
    types :: [(String, Expr Name)]
types = ((String, Expr Name) -> Bool)
-> [(String, Expr Name)] -> [(String, Expr Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"@") (String -> Bool)
-> ((String, Expr Name) -> String) -> (String, Expr Name) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeBaseName (String -> String)
-> ((String, Expr Name) -> String) -> (String, Expr Name) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Expr Name) -> String
forall a b. (a, b) -> a
fst) [(String, Expr Name)]
preludeExprs
    τ :: [(Name, Expr Name)]
τ = ((String, Expr Name) -> (Name, Expr Name))
-> [(String, Expr Name)] -> [(Name, Expr Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> Name)
-> (Expr Name -> Expr Name)
-> (String, Expr Name)
-> (Name, Expr Name)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (String -> Name
Name (String -> Name) -> (String -> String) -> String -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeDirectoryName) (Result (Expr Name) -> Expr Name
forall a. Result a -> a
throwL (Result (Expr Name) -> Expr Name)
-> (Expr Name -> Result (Expr Name)) -> Expr Name -> Expr Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr Name -> Result (Expr Name)
forall a. (Eq a, Enum a, Show a) => Expr a -> Result (Expr a)
inferType0)) [(String, Expr Name)]
types
    ε :: [(Name, Expr Name)]
ε = ((String, Expr Name) -> (Name, Expr Name))
-> [(String, Expr Name)] -> [(Name, Expr Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> Name) -> (String, Expr Name) -> (Name, Expr Name)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (String -> Name
Name (String -> Name) -> (String -> String) -> String -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
takeNamespacedFileName)) [(String, Expr Name)]
preludeExprs

-- | Substitute all occurrences of a variable v with an expression e, but only where
-- v appears in a type.
tauSubst :: (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
tauSubst :: a -> Expr a -> Expr a -> Expr a
tauSubst a
v Expr a
e Expr a
e' = String -> Expr a -> Expr a
forall a. String -> a -> a
trace (String
"tauSubst " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show Expr a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show Expr a
e') (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
tauSubst' a
v Expr a
e Expr a
e')

tauSubst' :: a -> Expr a -> Expr a -> Expr a
tauSubst' a
v Expr a
e (Lam a
v' Expr a
ta Expr a
b) | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v' = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Lam a
v' (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
ta) Expr a
b
tauSubst' a
v Expr a
e (Lam a
v' Expr a
ta Expr a
b) = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Lam a
v' (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
ta) (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
tauSubst a
v Expr a
e Expr a
b)
tauSubst' a
v Expr a
e (Pi a
v' Expr a
ta Expr a
tb) | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v' = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Pi a
v' (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
ta) Expr a
tb
tauSubst' a
v Expr a
e (Pi a
v' Expr a
ta Expr a
tb) = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Pi a
v' (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
ta) (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
tauSubst a
v Expr a
e Expr a
tb)
tauSubst' a
v Expr a
e (App Expr a
f Expr a
a) = Expr a -> Expr a -> Expr a
forall a. Expr a -> Expr a -> Expr a
App (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
tauSubst a
v Expr a
e Expr a
f) (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
tauSubst a
v Expr a
e Expr a
a)
tauSubst' a
_ Expr a
_ Expr a
e' = Expr a
e'

-- | Partially evaluate the types of an expression through lambda-application substitutions.
-- This should remain correct, but allows for binding types and evaluating by-reference.
tauNorm :: (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm :: Expr a -> Expr a
tauNorm Expr a
e = String -> Expr a -> Expr a
forall a. String -> a -> a
trace (String
"tauNorm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show Expr a
e) (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm' Expr a
e)

tauNorm' :: Expr a -> Expr a
tauNorm' (App Expr a
f Expr a
a) = case Expr a
f of
  Lam a
v Expr a
ta Expr a
b -> Expr a -> Expr a -> Expr a
forall a. Expr a -> Expr a -> Expr a
App (a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Lam a
v Expr a
ta (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm (Expr a -> Expr a) -> Expr a -> Expr a
forall a b. (a -> b) -> a -> b
$ a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
tauSubst a
v (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm Expr a
a) Expr a
b)) (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm Expr a
a)
  Expr a
_ -> Expr a -> Expr a -> Expr a
forall a. Expr a -> Expr a -> Expr a
App (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm Expr a
f) (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm Expr a
a)
tauNorm' (Lam a
v Expr a
ta Expr a
b) = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Lam a
v (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm Expr a
ta) (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm Expr a
b)
tauNorm' (Pi a
v Expr a
ta Expr a
b) = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Pi a
v (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm Expr a
ta) (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm Expr a
b)
tauNorm' Expr a
e = Expr a
e

-- | Fold the prelude context through lambda application into a type-context and expression-context-mapper.
--  That is, `let a = x in b` <=> `(λ a -> b) x`
wrapPrelude :: [(FilePath, ByteString)] -> (ShowCtx, ShowExpr -> ShowExpr)
wrapPrelude :: [(String, ByteString)] -> (ShowCtx, Expr Name -> Expr Name)
wrapPrelude [(String, ByteString)]
embedded = String
-> (ShowCtx, Expr Name -> Expr Name)
-> (ShowCtx, Expr Name -> Expr Name)
forall a. String -> a -> a
trace (String
"wrapPrelude " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, ByteString)] -> String
forall a. Show a => a -> String
show [(String, ByteString)]
embedded) ([(String, ByteString)] -> (ShowCtx, Expr Name -> Expr Name)
wrapPrelude' [(String, ByteString)]
embedded)

#ifdef TAUSUBSTITUTE
wrapPrelude' :: [(String, ByteString)] -> (ShowCtx, Expr Name -> Expr Name)
wrapPrelude' [(String, ByteString)]
embedded = ([(Name, Expr Name)] -> ShowCtx
forall a. [(a, Expr a)] -> Context a
Ctx [(Name, Expr Name)]
τ, Expr Name -> Expr Name
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
tauNorm (Expr Name -> Expr Name)
-> (Expr Name -> Expr Name) -> Expr Name -> Expr Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr Name -> Expr Name)
 -> (Name, Expr Name) -> Expr Name -> Expr Name)
-> (Expr Name -> Expr Name)
-> [(Name, Expr Name)]
-> Expr Name
-> Expr Name
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr Name -> Expr Name
f (Name
n, Expr Name
e) Expr Name
x -> Name -> Expr Name -> Expr Name -> Expr Name
forall a. a -> Expr a -> Expr a -> Expr a
Lam Name
n (Result (Expr Name) -> Expr Name
forall a. Result a -> a
throwL (Result (Expr Name) -> Expr Name)
-> Result (Expr Name) -> Expr Name
forall a b. (a -> b) -> a -> b
$ Expr Name -> Result (Expr Name)
forall a. (Eq a, Enum a, Show a) => Expr a -> Result (Expr a)
inferType0 Expr Name
e) (Expr Name -> Expr Name
f Expr Name
x) Expr Name -> Expr Name -> Expr Name
forall a. Expr a -> Expr a -> Expr a
`App` Expr Name
e) Expr Name -> Expr Name
forall a. a -> a
id [(Name, Expr Name)]
ε)
#else
wrapPrelude' embedded = (Ctx τ, foldl (\f (n, e) x -> Lam n (throwL $ inferType0 e) (f x) `App` e) id ε)
#endif
  where
    (Ctx [(Name, Expr Name)]
τ, Ctx [(Name, Expr Name)]
ε) = [(String, ByteString)] -> (ShowCtx, ShowCtx)
loadPrelude [(String, ByteString)]
embedded