{-# LANGUAGE ViewPatterns #-}

{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

module Blagda.Agda where



import           Agda.Interaction.FindFile (SourceFile(..))
import           Agda.Interaction.Imports
import           Agda.Interaction.Options
import           Agda.Syntax.Abstract
import           Agda.Syntax.Abstract.Views
import           Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as Con
import           Agda.Syntax.Info
import           Agda.Syntax.Internal (Type, Dom, domName)
import           Agda.Syntax.Position
import           Agda.Syntax.Scope.Base
import           Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete_)
import           Agda.Syntax.Translation.InternalToAbstract ( Reify(reify) )
import           Agda.TypeChecking.Monad
import           Agda.Utils.FileName
import qualified Agda.Utils.Maybe.Strict as S
import           Agda.Utils.Pretty
import           Control.Monad
import           Control.Monad.IO.Class
import           Data.Foldable
import           Data.Generics
import           Data.List
import           Data.List.NonEmpty (NonEmpty((:|)))
import           Data.Map.Lazy (Map)
import qualified Data.Map.Lazy as Map
import           Data.Maybe
import           Data.Text (Text)
import qualified Data.Text as Text
import           Data.Traversable
import           Development.Shake.FilePath

moduleName :: FilePath -> String
moduleName :: FilePath -> FilePath
moduleName = FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
"." ([FilePath] -> FilePath)
-> (FilePath -> [FilePath]) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
splitDirectories

fakePath :: QName -> Maybe FilePath
fakePath :: QName -> Maybe FilePath
fakePath (QName (MName [Name]
xs) Name
_) =
  [FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe
    [ FilePath
l FilePath -> FilePath -> FilePath
<.> FilePath
"html"
    | FilePath
l <- ([FilePath] -> FilePath) -> [[FilePath]] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
".") ([FilePath] -> [[FilePath]]
forall a. [a] -> [[a]]
inits ((Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> FilePath
render (Doc -> FilePath) -> (Name -> Doc) -> Name -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Name -> Name) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nameConcrete) [Name]
xs))
    , FilePath
l FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
builtinModules
    ]

removeImpls :: Expr -> Expr
removeImpls :: Expr -> Expr
removeImpls (Pi ExprInfo
_ (TypedBinding
x :| [TypedBinding]
xs) Expr
e) =
  [TypedBinding] -> Expr -> Expr
makePi ((TypedBinding -> TypedBinding) -> [TypedBinding] -> [TypedBinding]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Expr) -> TypedBinding -> TypedBinding
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
removeImpls) ([TypedBinding] -> [TypedBinding])
-> [TypedBinding] -> [TypedBinding]
forall a b. (a -> b) -> a -> b
$ (TypedBinding -> Bool) -> [TypedBinding] -> [TypedBinding]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
/= Hiding
Hidden) (Hiding -> Bool)
-> (TypedBinding -> Hiding) -> TypedBinding -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedBinding -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding) (TypedBinding
xTypedBinding -> [TypedBinding] -> [TypedBinding]
forall a. a -> [a] -> [a]
:[TypedBinding]
xs)) (Expr -> Expr
removeImpls Expr
e)
removeImpls (Fun ExprInfo
span Arg Expr
arg Expr
ret) =
  ExprInfo -> Arg Expr -> Expr -> Expr
Fun ExprInfo
span (Expr -> Expr
removeImpls (Expr -> Expr) -> Arg Expr -> Arg Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Expr
arg) (Expr -> Expr
removeImpls Expr
ret)
removeImpls Expr
e = Expr
e

runAgda :: (String -> TCMT IO a) -> IO a
runAgda :: (FilePath -> TCMT IO a) -> IO a
runAgda FilePath -> TCMT IO a
k = do
  Either TCErr a
e <- TCMT IO a -> IO (Either TCErr a)
forall a. TCM a -> IO (Either TCErr a)
runTCMTop (TCMT IO a -> IO (Either TCErr a))
-> TCMT IO a -> IO (Either TCErr a)
forall a b. (a -> b) -> a -> b
$ do
    FilePath
p <- TCMT IO FilePath
setupTCM
    FilePath -> TCMT IO a
k FilePath
p
  case Either TCErr a
e of
    Left TCErr
s -> FilePath -> IO a
forall a. HasCallStack => FilePath -> a
error (TCErr -> FilePath
forall a. Show a => a -> FilePath
show TCErr
s)
    Right a
x -> a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

setupTCM :: TCMT IO String
setupTCM :: TCMT IO FilePath
setupTCM = do
  AbsolutePath
absp <- IO AbsolutePath -> TCMT IO AbsolutePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AbsolutePath -> TCMT IO AbsolutePath)
-> IO AbsolutePath -> TCMT IO AbsolutePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO AbsolutePath
absolute FilePath
"./site"
  AbsolutePath -> CommandLineOptions -> TCM ()
setCommandLineOptions' AbsolutePath
absp CommandLineOptions
defaultOptions{optLocalInterfaces :: Bool
optLocalInterfaces = Bool
True}
  FilePath -> TCMT IO FilePath
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AbsolutePath -> FilePath
filePath AbsolutePath
absp)

killDomainNames :: Type -> Type
killDomainNames :: Type -> Type
killDomainNames = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((Dom Type -> Dom Type) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT Dom Type -> Dom Type
unDomName) where
  unDomName :: Dom Type -> Dom Type
  unDomName :: Dom Type -> Dom Type
unDomName Dom Type
m = Dom Type
m{ domName :: Maybe NamedName
domName = Maybe NamedName
forall a. Maybe a
Nothing }

killQual :: Con.Expr -> Con.Expr
killQual :: Expr -> Expr
killQual = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((QName -> QName) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT QName -> QName
unQual) where
  unQual :: Con.QName -> Con.QName
  unQual :: QName -> QName
unQual (Con.Qual Name
_ QName
x) = QName -> QName
unQual QName
x
  unQual QName
x = QName
x

tcAndLoadPublicNames :: FilePath -> String -> TCMT IO (Map Text Text)
tcAndLoadPublicNames :: FilePath -> FilePath -> TCMT IO (Map Text Text)
tcAndLoadPublicNames FilePath
path FilePath
basepn = do
  Source
source <- SourceFile -> TCM Source
parseSource (SourceFile -> TCM Source)
-> (AbsolutePath -> SourceFile) -> AbsolutePath -> TCM Source
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> SourceFile
SourceFile (AbsolutePath -> TCM Source) -> TCMT IO AbsolutePath -> TCM Source
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO AbsolutePath -> TCMT IO AbsolutePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO AbsolutePath
absolute FilePath
path)
  CheckResult
cr <- Mode -> Source -> TCM CheckResult
typeCheckMain Mode
TypeCheck Source
source

  let iface :: Interface
iface = CheckResult -> Interface
crInterface CheckResult
cr

  ScopeInfo -> TCM ()
setScope (Interface -> ScopeInfo
iInsideScope Interface
iface)
  ScopeInfo
scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope

  [(QName, FilePath, FilePath)]
li <- ([Maybe (QName, FilePath, FilePath)]
 -> [(QName, FilePath, FilePath)])
-> TCMT IO [Maybe (QName, FilePath, FilePath)]
-> TCMT IO [(QName, FilePath, FilePath)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe (QName, FilePath, FilePath)]
-> [(QName, FilePath, FilePath)]
forall a. [Maybe a] -> [a]
catMaybes (TCMT IO [Maybe (QName, FilePath, FilePath)]
 -> TCMT IO [(QName, FilePath, FilePath)])
-> ((QName -> TCMT IO (Maybe (QName, FilePath, FilePath)))
    -> TCMT IO [Maybe (QName, FilePath, FilePath)])
-> (QName -> TCMT IO (Maybe (QName, FilePath, FilePath)))
-> TCMT IO [(QName, FilePath, FilePath)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName]
-> (QName -> TCMT IO (Maybe (QName, FilePath, FilePath)))
-> TCMT IO [Maybe (QName, FilePath, FilePath)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (Set QName -> [QName]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (ScopeInfo -> Set QName
_scopeInScope ScopeInfo
scope)) ((QName -> TCMT IO (Maybe (QName, FilePath, FilePath)))
 -> TCMT IO [(QName, FilePath, FilePath)])
-> (QName -> TCMT IO (Maybe (QName, FilePath, FilePath)))
-> TCMT IO [(QName, FilePath, FilePath)]
forall a b. (a -> b) -> a -> b
$ \QName
name -> do
    Either SigError Definition
t <- QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
name
    case Either SigError Definition
t of
      Left SigError
_ -> Maybe (QName, FilePath, FilePath)
-> TCMT IO (Maybe (QName, FilePath, FilePath))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (QName, FilePath, FilePath)
forall a. Maybe a
Nothing
      Right Definition
d -> do
        Expr
expr <- Type -> TCMT IO Expr
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Type -> TCMT IO Expr) -> (Type -> Type) -> Type -> TCMT IO Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
killDomainNames (Type -> TCMT IO Expr) -> Type -> TCMT IO Expr
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
d
        FilePath
t <- (Expr -> FilePath) -> TCMT IO Expr -> TCMT IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Doc -> FilePath
render (Doc -> FilePath) -> (Expr -> Doc) -> Expr -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Doc
forall a. Pretty a => a -> Doc
pretty (Expr -> Doc) -> (Expr -> Expr) -> Expr -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
killQual) (TCMT IO Expr -> TCMT IO FilePath)
-> (Expr -> TCMT IO Expr) -> Expr -> TCMT IO FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          Expr -> TCMT IO Expr
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ (Expr -> TCMT IO Expr) -> (Expr -> Expr) -> Expr -> TCMT IO Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
removeImpls (Expr -> TCMT IO FilePath) -> Expr -> TCMT IO FilePath
forall a b. (a -> b) -> a -> b
$ Expr
expr

        case Range -> SrcFile
rangeFile (Name -> Range
nameBindingSite (QName -> Name
qnameName QName
name)) of
          S.Just (AbsolutePath -> FilePath
filePath -> FilePath
f)
            | (FilePath
"Agda/Builtin" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` FilePath
f) Bool -> Bool -> Bool
|| (FilePath
"Agda/Primitive" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` FilePath
f) ->
              Maybe (QName, FilePath, FilePath)
-> TCMT IO (Maybe (QName, FilePath, FilePath))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (QName, FilePath, FilePath)
 -> TCMT IO (Maybe (QName, FilePath, FilePath)))
-> Maybe (QName, FilePath, FilePath)
-> TCMT IO (Maybe (QName, FilePath, FilePath))
forall a b. (a -> b) -> a -> b
$ do
                FilePath
fp <- QName -> Maybe FilePath
fakePath QName
name
                (QName, FilePath, FilePath) -> Maybe (QName, FilePath, FilePath)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName
name, FilePath
fp, FilePath
t)
            | Bool
otherwise -> do
              let
                f' :: FilePath
f' = FilePath -> FilePath
moduleName (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
dropExtensions (FilePath -> FilePath -> FilePath
makeRelative FilePath
basepn FilePath
f)
                modMatches :: Bool
modMatches = FilePath
f' FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` Doc -> FilePath
render (QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
name)

              Maybe (QName, FilePath, FilePath)
-> TCMT IO (Maybe (QName, FilePath, FilePath))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (QName, FilePath, FilePath)
 -> TCMT IO (Maybe (QName, FilePath, FilePath)))
-> Maybe (QName, FilePath, FilePath)
-> TCMT IO (Maybe (QName, FilePath, FilePath))
forall a b. (a -> b) -> a -> b
$ do
                Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
modMatches Maybe ()
forall a. Maybe a
Nothing
                (QName, FilePath, FilePath) -> Maybe (QName, FilePath, FilePath)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName
name, FilePath
f' FilePath -> FilePath -> FilePath
<.> FilePath
"html", FilePath
t)
          SrcFile
S.Nothing -> Maybe (QName, FilePath, FilePath)
-> TCMT IO (Maybe (QName, FilePath, FilePath))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (QName, FilePath, FilePath)
forall a. Maybe a
Nothing

  let
    f :: (QName, FilePath, FilePath) -> Maybe (Text, Text)
f (QName
name, FilePath
modn, FilePath
ty) =
      case Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
rStart (Name -> Range
nameBindingSite (QName -> Name
qnameName QName
name)) of
        Just Position' SrcFile
pn -> (Text, Text) -> Maybe (Text, Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FilePath -> Text
Text.pack (FilePath
modn FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"#" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int32 -> FilePath
forall a. Show a => a -> FilePath
show (Position' SrcFile -> Int32
forall a. Position' a -> Int32
posPos Position' SrcFile
pn)), FilePath -> Text
Text.pack FilePath
ty)
        Maybe (Position' SrcFile)
Nothing -> Maybe (Text, Text)
forall a. Maybe a
Nothing

  Map Text Text -> TCMT IO (Map Text Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Text, Text)] -> Map Text Text
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (((QName, FilePath, FilePath) -> Maybe (Text, Text))
-> [(QName, FilePath, FilePath)] -> [(Text, Text)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (QName, FilePath, FilePath) -> Maybe (Text, Text)
f [(QName, FilePath, FilePath)]
li))

makePi :: [TypedBinding] -> Expr -> Expr
makePi :: [TypedBinding] -> Expr -> Expr
makePi [] = Expr -> Expr
forall a. a -> a
id
makePi (TypedBinding
b:[TypedBinding]
bs) = ExprInfo -> NonEmpty TypedBinding -> Expr -> Expr
Pi ExprInfo
exprNoRange (TypedBinding
b TypedBinding -> [TypedBinding] -> NonEmpty TypedBinding
forall a. a -> [a] -> NonEmpty a
:| [TypedBinding]
bs)

builtinModules :: [String]
builtinModules :: [FilePath]
builtinModules =
  [ FilePath
"Agda.Builtin.Bool"
  , FilePath
"Agda.Builtin.Char"
  -- , "Agda.Builtin.Cubical.HCompU"
  -- , "Agda.Builtin.Cubical.Path"
  -- , "Agda.Builtin.Cubical.Sub"
  , FilePath
"Agda.Builtin.Float"
  , FilePath
"Agda.Builtin.FromNat"
  , FilePath
"Agda.Builtin.FromNeg"
  , FilePath
"Agda.Builtin.Int"
  , FilePath
"Agda.Builtin.List"
  , FilePath
"Agda.Builtin.Maybe"
  , FilePath
"Agda.Builtin.Nat"
  , FilePath
"Agda.Builtin.Reflection"
  , FilePath
"Agda.Builtin.Sigma"
  , FilePath
"Agda.Builtin.String"
  , FilePath
"Agda.Builtin.Unit"
  , FilePath
"Agda.Builtin.Word"
  , FilePath
"Agda.Primitive.Cubical"
  , FilePath
"Agda.Primitive"
  ]