{-# LANGUAGE OverloadedStrings #-}

module BNFC.Backend.Agda.AbstractSyntax where

import BNFC.CF
import BNFC.Options.GlobalOptions
import BNFC.Prelude

import BNFC.Backend.Agda.IOLib
import BNFC.Backend.Agda.Main
import BNFC.Backend.Agda.Options
import BNFC.Backend.Agda.State
import BNFC.Backend.Agda.Utilities.ReservedWords
import BNFC.Backend.Agda.Utilities.Utils

import BNFC.Backend.Common.Utils as Utils
import BNFC.Backend.CommonInterface.Backend

import BNFC.Backend.Haskell.AbstractSyntax (cf2abs)
import BNFC.Backend.Haskell.Options (TokenText (..))
import BNFC.Backend.Haskell.Template (cf2template)
import BNFC.Backend.Haskell.Utilities.Utils

import Control.Monad.State

import           Data.Bifunctor  (second)
import qualified Data.Map as Map
import           Data.List       (intersperse)
import qualified BNFC.Utils.List1 as List1
import           Data.String     (fromString)

import Prettyprinter

import System.FilePath ( takeBaseName )


agdaAbstractSyntax :: LBNF -> State AgdaBackendState Result
agdaAbstractSyntax :: LBNF -> State AgdaBackendState Result
agdaAbstractSyntax LBNF
lbnf = do
  AgdaBackendState
st    <- StateT AgdaBackendState Identity AgdaBackendState
forall s (m :: * -> *). MonadState s m => m s
get
  Result
ioLib <- State AgdaBackendState Result
agdaIOLib
  Result
main  <- LBNF -> State AgdaBackendState Result
agdaMain LBNF
lbnf
  let cfName :: String
cfName      = String -> String
takeBaseName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ GlobalOptions -> String
optInput (GlobalOptions -> String) -> GlobalOptions -> String
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> GlobalOptions
globalOpt AgdaBackendState
st
      hsRules :: [(Type, [(Label, ([Type], (Integer, ARHS)))])]
hsRules     = [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
filterRules ([(Type, [(Label, ([Type], (Integer, ARHS)))])]
 -> [(Type, [(Label, ([Type], (Integer, ARHS)))])])
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
hsAstRules AgdaBackendState
st
      agdaRules :: [(Type, [(Label, [Type])])]
agdaRules   = AgdaBackendState -> [(Type, [(Label, [Type])])]
agdaAstRules AgdaBackendState
st
      hasData :: Bool
hasData     = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [(Type, [(Label, ([Type], (Integer, ARHS)))])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, [(Label, ([Type], (Integer, ARHS)))])]
hsRules
      hsFuns :: [(LabelName, Function)]
hsFuns      = AgdaBackendState -> [(LabelName, Function)]
hsFunctions AgdaBackendState
st
      agdaFuns :: [(LabelName, Function)]
agdaFuns    = AgdaBackendState -> [(LabelName, Function)]
agdaFunctions AgdaBackendState
st
      toks :: [(LabelName, TokenDef)]
toks        = AgdaBackendState -> [(LabelName, TokenDef)]
tokens AgdaBackendState
st
      tokensNames :: [LabelName]
tokensNames = (LabelName, TokenDef) -> LabelName
forall a b. (a, b) -> a
fst ((LabelName, TokenDef) -> LabelName)
-> [(LabelName, TokenDef)] -> [LabelName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LabelName, TokenDef)]
toks
      inDirectory :: Bool
inDirectory = AgdaBackendOptions -> Bool
inDir (AgdaBackendOptions -> Bool) -> AgdaBackendOptions -> Bool
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
      nSpace :: Maybe String
nSpace      = AgdaBackendOptions -> Maybe String
nameSpace (AgdaBackendOptions -> Maybe String)
-> AgdaBackendOptions -> Maybe String
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
      funct :: Bool
funct       = AgdaBackendOptions -> Bool
functor (AgdaBackendOptions -> Bool) -> AgdaBackendOptions -> Bool
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
      gen :: Bool
gen         = AgdaBackendOptions -> Bool
generic (AgdaBackendOptions -> Bool) -> AgdaBackendOptions -> Bool
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
      absSyntaxHaskell :: String
absSyntaxHaskell =
        LBNF
-> String
-> Bool
-> Maybe String
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(LabelName, Function)]
-> [(LabelName, TokenDef)]
-> Bool
-> Bool
-> Bool
-> TokenText
-> String
cf2abs LBNF
lbnf String
cfName Bool
inDirectory Maybe String
nSpace [(Type, [(Label, ([Type], (Integer, ARHS)))])]
hsRules [(LabelName, Function)]
hsFuns [(LabelName, TokenDef)]
toks Bool
funct Bool
gen Bool
hasData TokenText
TextToken
      templateHaskell :: String
templateHaskell  =
        [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [LabelName] -> String -> Bool -> Maybe String -> Bool -> String
cf2template [(Type, [(Label, ([Type], (Integer, ARHS)))])]
hsRules [LabelName]
tokensNames String
cfName Bool
inDirectory Maybe String
nSpace Bool
funct
      astAgda :: String
astAgda = LBNF
-> String
-> Bool
-> Maybe String
-> [(Type, [(Label, [Type])])]
-> [(LabelName, Function)]
-> [(LabelName, TokenDef)]
-> [LabelName]
-> Bool
-> String
cf2AST LBNF
lbnf String
cfName Bool
inDirectory Maybe String
nSpace [(Type, [(Label, [Type])])]
agdaRules [(LabelName, Function)]
agdaFuns [(LabelName, TokenDef)]
toks [LabelName]
tokensNames Bool
funct
  Result -> State AgdaBackendState Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> State AgdaBackendState Result)
-> Result -> State AgdaBackendState Result
forall a b. (a -> b) -> a -> b
$
    [ (Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Abs" String
"hs", String
absSyntaxHaskell)
    , (Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Skel" String
"hs", String
templateHaskell)
    , (Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"AST" String
"agda", String
astAgda)
    ]
    Result -> Result -> Result
forall a. [a] -> [a] -> [a]
++
    Result
ioLib
    Result -> Result -> Result
forall a. [a] -> [a] -> [a]
++
    Result
main

  where

    filterRules :: [(Type, [(Label, ([Type], (Integer, ARHS)))])]
                -> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
    filterRules :: [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
filterRules [(Type, [(Label, ([Type], (Integer, ARHS)))])]
rules =
      ((Type, [(Label, ([Type], (Integer, ARHS)))]) -> Bool)
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (\(Type
_,[(Label, ([Type], (Integer, ARHS)))]
l) -> Bool -> Bool
not ([(Label, ([Type], (Integer, ARHS)))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Label, ([Type], (Integer, ARHS)))]
l))
      (([(Label, ([Type], (Integer, ARHS)))]
 -> [(Label, ([Type], (Integer, ARHS)))])
-> (Type, [(Label, ([Type], (Integer, ARHS)))])
-> (Type, [(Label, ([Type], (Integer, ARHS)))])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
Data.Bifunctor.second ([String]
-> [(Label, ([Type], (Integer, ARHS)))]
-> [(Label, ([Type], (Integer, ARHS)))]
filterLabelsAST [String]
fNames) ((Type, [(Label, ([Type], (Integer, ARHS)))])
 -> (Type, [(Label, ([Type], (Integer, ARHS)))]))
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
-> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Type, [(Label, ([Type], (Integer, ARHS)))])]
rules)

    -- Functions names.
    fNames :: [String]
    fNames :: [String]
fNames = LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (LabelName -> String) -> [LabelName] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map LabelName (WithPosition Function) -> [LabelName]
forall k a. Map k a -> [k]
Map.keys (LBNF -> Map LabelName (WithPosition Function)
_lbnfFunctions LBNF
lbnf)

cf2AST :: LBNF
       -> String
       -> Bool
       -> Maybe String
       -> [(Type, [(Label, [Type])])]
       -> [(LabelName,Function)]
       -> [(CatName,TokenDef)]
       -> [CatName]
       -> Bool
       -> String
cf2AST :: LBNF
-> String
-> Bool
-> Maybe String
-> [(Type, [(Label, [Type])])]
-> [(LabelName, Function)]
-> [(LabelName, TokenDef)]
-> [LabelName]
-> Bool
-> String
cf2AST LBNF
lbnf String
cfName Bool
inDir Maybe String
nameSpace [(Type, [(Label, [Type])])]
astRules [(LabelName, Function)]
functions [(LabelName, TokenDef)]
toks [LabelName]
toksName Bool
functor =
  LayoutOptions -> Doc () -> String
docToString LayoutOptions
defaultLayoutOptions (Doc () -> String) -> Doc () -> String
forall a b. (a -> b) -> a -> b
$
    LBNF
-> String
-> Bool
-> Maybe String
-> [(Type, [(Label, [Type])])]
-> [(LabelName, Function)]
-> [(LabelName, TokenDef)]
-> [LabelName]
-> Bool
-> Doc ()
cf2doc LBNF
lbnf String
cfName Bool
inDir Maybe String
nameSpace [(Type, [(Label, [Type])])]
astRules [(LabelName, Function)]
functions [(LabelName, TokenDef)]
toks [LabelName]
toksName Bool
functor

cf2doc :: LBNF
       -> String
       -> Bool
       -> Maybe String
       -> [(Type, [(Label, [Type])])]
       -> [(LabelName,Function)]
       -> [(CatName,TokenDef)]
       -> [CatName]
       -> Bool
       -> Doc ()
cf2doc :: LBNF
-> String
-> Bool
-> Maybe String
-> [(Type, [(Label, [Type])])]
-> [(LabelName, Function)]
-> [(LabelName, TokenDef)]
-> [LabelName]
-> Bool
-> Doc ()
cf2doc LBNF
lbnf String
cfName Bool
inDir Maybe String
nameSpace [(Type, [(Label, [Type])])]
astRules [(LabelName, Function)]
functions [(LabelName, TokenDef)]
toks [LabelName]
toksNames Bool
functor =
  ([Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ())
-> ([Doc ()] -> [Doc ()]) -> [Doc ()] -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
intersperse Doc ()
forall ann. Doc ann
emptyDoc) ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ [[Doc ()]] -> [Doc ()]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [ Doc ()
"-- File generated by the BNF Converter."
    , Doc ()
"-- Agda bindings for the Haskell abstract syntax data types."
    , Doc ()
"module" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
agdaASTName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"where"
    , ImportNumeric -> Bool -> Bool -> Bool -> Doc ()
imports ImportNumeric
YesImportNumeric Bool
False Bool
usesPos Bool
functor
    ]
    , Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
usesString [ Doc ()
"String = #List Char" ]
    , [ Bool -> [String] -> Doc ()
importPragmas Bool
usesPos
        [ String
"qualified " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hsAbsName, String
hsPrinterName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (printTree)" ] ]
    , Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
usesPos [ Doc ()
intAndPair ]
    , Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
functor [ Doc ()
bnfcPosition ]
    , Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
hasTokens [ String -> [(LabelName, TokenDef)] -> Doc ()
prTokens String
hsAbsName [(LabelName, TokenDef)]
toks ]
    , Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
hasData [ Bool
-> String
-> ConstructorStyle
-> [(Type, [(Label, [Type])])]
-> Doc ()
prDatas Bool
functor String
hsAbsName ConstructorStyle
NamedArg [(Type, [(Label, [Type])])]
astRules ]
    , Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
hasFunctions [ Bool -> [(LabelName, Function)] -> Doc ()
prFunctions Bool
functor [(LabelName, Function)]
functions ]
    , [ String -> [Type] -> [BuiltinCat] -> [LabelName] -> Doc ()
printerBindings String
hsAbsName [Type]
astCats [BuiltinCat]
usedBuiltins [LabelName]
toksNames ]
  ]

  where

    intAndPair :: Doc ()
    intAndPair :: Doc ()
intAndPair = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
      [ Doc ()
"postulate"
      , Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ()
"#Int      : Set"
      , Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ()
"#intToNat : #Int → #Nat"
      , Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ()
"#natToInt : #Nat → #Int"
      , Doc ()
forall ann. Doc ann
emptyDoc
      , Doc ()
"{-# COMPILE GHC #Int      = type Prelude.Int    #-}"
      , Doc ()
"{-# COMPILE GHC #intToNat = Prelude.toInteger   #-}"
      , Doc ()
"{-# COMPILE GHC #natToInt = Prelude.fromInteger #-}"
      , Doc ()
forall ann. Doc ann
emptyDoc
      , Doc ()
"data #Pair (A B : Set) : Set where"
      , Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ()
"#pair : A → B → #Pair A B"
      , Doc ()
forall ann. Doc ann
emptyDoc
      , Doc ()
"{-# COMPILE GHC #Pair = data (,) ((,)) #-}"
      ]

    bnfcPosition :: Doc ()
    bnfcPosition :: Doc ()
bnfcPosition = Doc ()
"#BNFCPosition = #Maybe (#Pair #Int #Int)"

    agdaASTName :: ModuleName
    agdaASTName :: String
agdaASTName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"AST"

    hsAbsName :: ModuleName
    hsAbsName :: String
hsAbsName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"Abs"

    hsPrinterName :: ModuleName
    hsPrinterName :: String
hsPrinterName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"Print"

    usesPos :: Bool
    usesPos :: Bool
usesPos = Bool
hasPosTokens Bool -> Bool -> Bool
|| (Bool
hasData Bool -> Bool -> Bool
&& Bool
functor)

    hasPosTokens :: Bool
    hasPosTokens :: Bool
hasPosTokens = (WithPosition TokenDef -> Bool)
-> Map LabelName (WithPosition TokenDef) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any WithPosition TokenDef -> Bool
isPositionToken (LBNF -> Map LabelName (WithPosition TokenDef)
_lbnfTokenDefs LBNF
lbnf)

    usesString :: Bool
    usesString :: Bool
usesString = BuiltinCat
BString BuiltinCat -> [BuiltinCat] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map BuiltinCat (List1 Position) -> [BuiltinCat]
forall k a. Map k a -> [k]
Map.keys (LBNF -> Map BuiltinCat (List1 Position)
_lbnfASTBuiltins LBNF
lbnf)

    astCats :: [Type]
    astCats :: [Type]
astCats = (Type, [(Label, [Type])]) -> Type
forall a b. (a, b) -> a
fst ((Type, [(Label, [Type])]) -> Type)
-> [(Type, [(Label, [Type])])] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Type, [(Label, [Type])])]
astRules

    usedBuiltins :: [BuiltinCat]
    usedBuiltins :: [BuiltinCat]
usedBuiltins = Map BuiltinCat (List1 Position) -> [BuiltinCat]
forall k a. Map k a -> [k]
Map.keys (Map BuiltinCat (List1 Position) -> [BuiltinCat])
-> Map BuiltinCat (List1 Position) -> [BuiltinCat]
forall a b. (a -> b) -> a -> b
$ LBNF -> Map BuiltinCat (List1 Position)
_lbnfASTBuiltins LBNF
lbnf

    hasData :: Bool
    hasData :: Bool
hasData = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [(Type, [(Label, [Type])])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, [(Label, [Type])])]
astRules

    hasTokens :: Bool
    hasTokens :: Bool
hasTokens = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [(LabelName, TokenDef)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(LabelName, TokenDef)]
toks

    hasFunctions :: Bool
    hasFunctions :: Bool
hasFunctions = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [(LabelName, Function)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(LabelName, Function)]
functions


-- | Print Agda types for user defined tokens.

prTokens :: ModuleName -> [(CatName,TokenDef)] -> Doc ()
prTokens :: String -> [(LabelName, TokenDef)] -> Doc ()
prTokens String
hsAbsName = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ())
-> ([(LabelName, TokenDef)] -> [Doc ()])
-> [(LabelName, TokenDef)]
-> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
intersperse Doc ()
forall ann. Doc ann
emptyDoc ([Doc ()] -> [Doc ()])
-> ([(LabelName, TokenDef)] -> [Doc ()])
-> [(LabelName, TokenDef)]
-> [Doc ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((LabelName, TokenDef) -> Doc ())
-> [(LabelName, TokenDef)] -> [Doc ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> (LabelName, TokenDef) -> Doc ()
prToken String
hsAbsName)

prToken :: ModuleName -> (CatName,TokenDef) -> Doc ()
prToken :: String -> (LabelName, TokenDef) -> Doc ()
prToken String
hsAbsName (LabelName
cName, TokenDef
def) = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
    [ Doc ()
"data" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
tokenNameAgda Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
": Set where"
    , if TokenDef -> Bool
isPosToken TokenDef
def
      then Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ Doc ()
tokenConstructorName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
": #Pair (#Pair #Int #Int) #String →" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
        Doc ()
tokenNameAgda
      else Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ Doc ()
tokenConstructorName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
": #String →" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
tokenNameAgda
    , Doc ()
forall ann. Doc ann
emptyDoc
    , Doc ()
"{-# COMPILE GHC" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
tokenNameHs Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"=" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"data" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
qualifiedToken Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
       Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens Doc ()
qualifiedToken Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"#-}"
    ]

  where

    tokenNameAgda :: Doc ()
    tokenNameAgda :: Doc ()
tokenNameAgda = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (LabelName -> String) -> LabelName -> String
forall a b. (a -> b) -> a -> b
$ LabelName -> LabelName
avoidAgdaReservedWords LabelName
cName

    tokenNameHs :: Doc ()
    tokenNameHs :: Doc ()
tokenNameHs = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList LabelName
cName

    tokenConstructorName :: Doc ()
    tokenConstructorName :: Doc ()
tokenConstructorName = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (LabelName -> String) -> LabelName -> String
forall a b. (a -> b) -> a -> b
$ LabelName -> LabelName
agdaLower LabelName
cName

    qualifiedToken :: Doc ()
    qualifiedToken :: Doc ()
qualifiedToken = String -> Doc ()
forall a. IsString a => String -> a
fromString String
hsAbsName Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
forall ann. Doc ann
dot Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
tokenNameHs

-- | Print Agda types for categories in AST rules.

prDatas :: Bool
        -> ModuleName
        -> ConstructorStyle
        -> [(Type, [(Label, [Type])])]
        -> Doc ()
prDatas :: Bool
-> String
-> ConstructorStyle
-> [(Type, [(Label, [Type])])]
-> Doc ()
prDatas Bool
functor String
absName ConstructorStyle
style [(Type, [(Label, [Type])])]
astRules = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc ()
"mutual"
  , Doc ()
forall ann. Doc ann
emptyDoc
  , Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc () -> Doc ()) -> ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ())
-> ([Doc ()] -> [Doc ()]) -> [Doc ()] -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
intersperse Doc ()
forall ann. Doc ann
emptyDoc ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$
    ((Type, [(Label, [Type])]) -> Doc ())
-> [(Type, [(Label, [Type])])] -> [Doc ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool
-> String
-> ConstructorStyle
-> (Type, [(Label, [Type])])
-> Doc ()
prData Bool
functor String
absName ConstructorStyle
style) [(Type, [(Label, [Type])])]
astRules
  ]

-- | Pretty-print Agda data types and pragmas for AST.

prData :: Bool
       -> ModuleName
       -> ConstructorStyle
       -> (Type, [(Label, [Type])])
       -> Doc ()
prData :: Bool
-> String
-> ConstructorStyle
-> (Type, [(Label, [Type])])
-> Doc ()
prData Bool
True String
absName ConstructorStyle
style (Type
t, [(Label, [Type])]
labelsItems) = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc ()
tName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"=" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
hsDataName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"#BNFCPosition"
  , String
-> ConstructorStyle
-> Doc ()
-> Doc ()
-> [(Label, [Type])]
-> Doc ()
prData' String
absName ConstructorStyle
style Doc ()
agdaDataName Doc ()
hsDataName [(Label, [Type])]
labelsItemsWithParam
  ]
  where
    -- Add param to rhs non terminals.
    labelsItemsWithParam :: [(Label, [Type])]
    labelsItemsWithParam :: [(Label, [Type])]
labelsItemsWithParam = ([Type] -> [Type]) -> (Label, [Type]) -> (Label, [Type])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Type -> Type
addParam (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ((Label, [Type]) -> (Label, [Type]))
-> [(Label, [Type])] -> [(Label, [Type])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Label, [Type])]
labelsItems

    agdaDataName :: Doc ()
    agdaDataName :: Doc ()
agdaDataName = String -> Doc ()
forall a. IsString a => String -> a
fromString (Type -> String
printTypeName (Type -> String) -> Type -> String
forall a b. (a -> b) -> a -> b
$ Type -> Type
addParam (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
avoidResWordsType Type
t )

    hsDataName :: Doc ()
    hsDataName :: Doc ()
hsDataName = String -> Doc ()
forall a. IsString a => String -> a
fromString (Type -> String
printTypeName Type
t ) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"'"

    tName :: Doc ()
    tName :: Doc ()
tName = String -> Doc ()
forall a. IsString a => String -> a
fromString ( String -> String
sanitize (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Type -> String
printTypeName Type
t )

    addParam :: Type -> Type
    addParam :: Type -> Type
addParam (BaseType BaseCat
b)  = BaseCat -> Type
BaseType (BaseCat -> Type) -> BaseCat -> Type
forall a b. (a -> b) -> a -> b
$ BaseCat -> BaseCat
addP BaseCat
b
    addParam (ListType Type
tt) = Type -> Type
addParam Type
tt

    addP :: BaseCat -> BaseCat
    addP :: BaseCat -> BaseCat
addP = \case
      BuiltinCat BuiltinCat
b -> BuiltinCat -> BaseCat
BuiltinCat BuiltinCat
b
      IdentCat   IdentCat
i -> IdentCat -> BaseCat
IdentCat IdentCat
i
      TokenCat   LabelName
x -> LabelName -> BaseCat
TokenCat LabelName
x
      BaseCat    LabelName
x -> LabelName -> BaseCat
BaseCat (LabelName -> BaseCat) -> LabelName -> BaseCat
forall a b. (a -> b) -> a -> b
$ LabelName
x LabelName -> LabelName -> LabelName
forall a. Semigroup a => a -> a -> a
<> LabelName
"' Pos#"

prData Bool
False String
absName ConstructorStyle
style (Type
t, [(Label, [Type])]
labelsItems) =
  String
-> ConstructorStyle
-> Doc ()
-> Doc ()
-> [(Label, [Type])]
-> Doc ()
prData' String
absName ConstructorStyle
style Doc ()
agdaDataName Doc ()
hsDataName [(Label, [Type])]
labelsItems

  where

    hsDataName :: Doc ()
    hsDataName :: Doc ()
hsDataName = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ Type -> String
printTypeName Type
t

    agdaDataName :: Doc ()
    agdaDataName :: Doc ()
agdaDataName = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ Type -> String
printTypeName (Type -> String) -> Type -> String
forall a b. (a -> b) -> a -> b
$ Type -> Type
avoidResWordsType Type
t

-- | Pretty-print Agda data types and pragmas.

prData' :: ModuleName
        -> ConstructorStyle
        -> Doc () -- Agda data name
        -> Doc () -- Haskell data name
        -> [(Label, [Type])]
        -> Doc ()
prData' :: String
-> ConstructorStyle
-> Doc ()
-> Doc ()
-> [(Label, [Type])]
-> Doc ()
prData' String
absName ConstructorStyle
style Doc ()
agdaDataName Doc ()
hsDataName [(Label, [Type])]
labelsItems = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ ConstructorStyle -> Doc () -> [(Label, [Type])] -> Doc ()
prettyData ConstructorStyle
style Doc ()
agdaDataName [(Label, [Type])]
labelsItems
  , Doc ()
forall ann. Doc ann
emptyDoc
  , String -> Doc () -> Doc () -> [Doc ()] -> Doc ()
compilePragma String
absName Doc ()
agdaDataName Doc ()
hsDataName [Doc ()]
labels
  ]

  where

    labels :: [Doc ()]
    labels :: [Doc ()]
labels = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ())
-> ((Label, [Type]) -> String) -> (Label, [Type]) -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> String
printLabelName (Label -> String)
-> ((Label, [Type]) -> Label) -> (Label, [Type]) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Label, [Type]) -> Label
forall a b. (a, b) -> a
fst ((Label, [Type]) -> Doc ()) -> [(Label, [Type])] -> [Doc ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Label, [Type])]
labelsItems


-- | Pretty-print AST definition in Agda syntax.

prettyData :: ConstructorStyle -> Doc () -> [(Label, [Type])] -> Doc ()
prettyData :: ConstructorStyle -> Doc () -> [(Label, [Type])] -> Doc ()
prettyData ConstructorStyle
style Doc ()
typeName [(Label, [Type])]
labelsItems = Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
hang Int
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc ()
"data" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
typeName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"Set where"
  ,  [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ ConstructorStyle -> Doc () -> (Label, [Type]) -> Doc ()
printCase ConstructorStyle
style Doc ()
typeName ((Label, [Type]) -> Doc ()) -> [(Label, [Type])] -> [Doc ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Label, [Type])]
labelsItems
  ]

printCase :: ConstructorStyle -> Doc () -> (Label, [Type]) -> Doc ()
printCase :: ConstructorStyle -> Doc () -> (Label, [Type]) -> Doc ()
printCase ConstructorStyle
style Doc ()
typeName (Label
label, [Type]
args) =
  if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args
  then Doc ()
constructor Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
typeName
  else Doc ()
constructor Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ConstructorStyle -> [Type] -> Doc ()
printConstructorArgs ConstructorStyle
style [Type]
args Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
    String -> Doc ()
forall a. IsString a => String -> a
fromString String
uArrow Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
typeName
  where
    constructor :: Doc ()
    constructor :: Doc ()
constructor = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ Label -> String
printLabelName (Label -> String) -> Label -> String
forall a b. (a -> b) -> a -> b
$ Label -> Label
lowerLabel Label
label


printConstructorArgs :: ConstructorStyle -> [Type] -> Doc ()
printConstructorArgs :: ConstructorStyle -> [Type] -> Doc ()
printConstructorArgs ConstructorStyle
style [Type]
args =
  case ConstructorStyle
style of
    ConstructorStyle
UnnamedArg -> [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ (String -> Doc ()) -> [String] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc ()
forall a. IsString a => String -> a
fromString ([String] -> [Doc ()]) -> [String] -> [Doc ()]
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
uArrow [String]
ts
    ConstructorStyle
NamedArg   -> [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ ((NonEmpty (Doc ()), Doc ()) -> Doc ())
-> [(NonEmpty (Doc ()), Doc ())] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Doc ()
x :| [Doc ()]
xs, Doc ()
t) -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens ([Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep [Doc ()
x, [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep [Doc ()]
xs, Doc ()
forall ann. Doc ann
colon, Doc ()
t])) [(NonEmpty (Doc ()), Doc ())]
tel
  where
  -- Arguments types.
  ts :: [String]
  ts :: [String]
ts  = (Type -> String) -> [Type] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Type -> String
prettyType [Type]
args
  -- Arguments names.
  ns :: [String]
  ns :: [String]
ns  = ((Maybe Int, String) -> String)
-> [(Maybe Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Int, String) -> String
forall a. Show a => (Maybe a, String) -> String
subscript ([(Maybe Int, String)] -> [String])
-> [(Maybe Int, String)] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [(Maybe Int, String)]
forall a. Ord a => [a] -> [(Maybe Int, a)]
numberUniquely ([String] -> [(Maybe Int, String)])
-> [String] -> [(Maybe Int, String)]
forall a b. (a -> b) -> a -> b
$ (Type -> String) -> [Type] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Type -> String
nameSuggestion [Type]
args
  -- Arguments names grouped by type.
  tel :: [(List1 (Doc ()), Doc ())]
  tel :: [(NonEmpty (Doc ()), Doc ())]
tel = (NonEmpty String -> NonEmpty (Doc ()))
-> (String -> Doc ())
-> (NonEmpty String, String)
-> (NonEmpty (Doc ()), Doc ())
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> NonEmpty String -> NonEmpty (Doc ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) String -> Doc ()
forall a. IsString a => String -> a
fromString ((NonEmpty String, String) -> (NonEmpty (Doc ()), Doc ()))
-> [(NonEmpty String, String)] -> [(NonEmpty (Doc ()), Doc ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((String, String) -> String)
-> Result -> [(NonEmpty String, String)]
forall c a b. Eq c => ((a, b) -> c) -> [(a, b)] -> [(List1 a, b)]
aggregateOn (String, String) -> String
forall a b. (a, b) -> b
snd ([String] -> [String] -> Result
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
ns [String]
ts)
  deltaSubscript :: Int
deltaSubscript = Char -> Int
ord Char
'₀' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0' -- exploiting that '0' comes before '₀' in character table
  subscript :: (Maybe a, String) -> String
subscript (Maybe a
m, String
s) = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
s (\ a
n -> String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Char
chr (Int -> Char) -> (Char -> Int) -> Char -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
deltaSubscript Int -> Int -> Int
forall a. Num a => a -> a -> a
+) (Int -> Int) -> (Char -> Int) -> Char -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
ord) (a -> String
forall a. Show a => a -> String
show a
n)) Maybe a
m
  -- Aggregate consecutive arguments of the same type.
  aggregateOn :: Eq c => ((a,b) -> c) -> [(a,b)] -> [(List1 a,b)]
  aggregateOn :: ((a, b) -> c) -> [(a, b)] -> [(List1 a, b)]
aggregateOn (a, b) -> c
f
    = (NonEmpty (a, b) -> (List1 a, b))
-> [NonEmpty (a, b)] -> [(List1 a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\ NonEmpty (a, b)
p -> (((a, b) -> a) -> NonEmpty (a, b) -> List1 a
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
List1.map (a, b) -> a
forall a b. (a, b) -> a
fst NonEmpty (a, b)
p, (a, b) -> b
forall a b. (a, b) -> b
snd (NonEmpty (a, b) -> (a, b)
forall a. NonEmpty a -> a
List1.head NonEmpty (a, b)
p)))
    ([NonEmpty (a, b)] -> [(List1 a, b)])
-> ([(a, b)] -> [NonEmpty (a, b)]) -> [(a, b)] -> [(List1 a, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, b) -> (a, b) -> Bool) -> [(a, b)] -> [NonEmpty (a, b)]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.groupBy (c -> c -> Bool
forall a. Eq a => a -> a -> Bool
(==) (c -> c -> Bool) -> ((a, b) -> c) -> (a, b) -> (a, b) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (a, b) -> c
f)

prettyType :: Type -> String
prettyType :: Type -> String
prettyType = \case
  BaseType BaseCat
bc -> BaseCat -> String
printBaseCatName BaseCat
bc
  ListType Type
ty -> String
"#List " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
prettyType Type
ty

compilePragma :: ModuleName -> Doc () -> Doc () -> [Doc ()] -> Doc ()
compilePragma :: String -> Doc () -> Doc () -> [Doc ()] -> Doc ()
compilePragma String
absName Doc ()
agdaTypeName Doc ()
hsTypeName [Doc ()]
labels = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc ()
"{-# COMPILE GHC" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
agdaTypeName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"= data" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
      String -> Doc ()
forall a. IsString a => String -> a
fromString String
absName Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
forall ann. Doc ann
dot Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
hsTypeName
  , [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ (Doc () -> Doc () -> Doc ()) -> [Doc ()] -> [Doc ()] -> [Doc ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
      (\ Doc ()
a Doc ()
b -> Doc ()
a Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
absName Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
forall ann. Doc ann
dot Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
b)
      (Doc ()
"(" Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
: Doc () -> [Doc ()]
forall a. a -> [a]
repeat Doc ()
"|")
      [Doc ()]
labels
  , Doc ()
") #-}"
  ]

-- | Generate Haskell/Agda code for the @define@d constructors.
prFunctions :: Bool -> [(LabelName,Function)] -> Doc ()
prFunctions :: Bool -> [(LabelName, Function)] -> Doc ()
prFunctions Bool
functor = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ())
-> ([(LabelName, Function)] -> [Doc ()])
-> [(LabelName, Function)]
-> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
intersperse Doc ()
forall ann. Doc ann
emptyDoc ([Doc ()] -> [Doc ()])
-> ([(LabelName, Function)] -> [Doc ()])
-> [(LabelName, Function)]
-> [Doc ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((LabelName, Function) -> Doc ())
-> [(LabelName, Function)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> (LabelName, Function) -> Doc ()
prFunction Bool
functor)

prFunction :: Bool -> (LabelName,Function) -> Doc ()
prFunction :: Bool -> (LabelName, Function) -> Doc ()
prFunction Bool
functor (LabelName
lName, Function
fun) = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep [ Doc ()
header, Doc ()
withBody ]

  where

    funName :: Doc ()
    funName :: Doc ()
funName = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList LabelName
lName
    arrow :: Doc ()
    arrow :: Doc ()
arrow = String -> Doc ()
forall a. IsString a => String -> a
fromString String
uArrow
    header :: Doc ()
    header :: Doc ()
header = Doc ()
funName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
":" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
paramsTypes Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
arrow Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
returnType
    paramsTypes :: Doc ()
    paramsTypes :: Doc ()
paramsTypes =
      if Bool
functor
      then Doc ()
"{A : Set} a" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
arrow Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep (Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
intersperse Doc ()
arrow (Type -> Doc ()
paramT (Type -> Doc ()) -> [Type] -> [Doc ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
types))
      else [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep (Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
intersperse Doc ()
arrow (Type -> Doc ()
paramT (Type -> Doc ()) -> [Type] -> [Doc ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
types))
    paramT :: Type -> Doc ()
    paramT :: Type -> Doc ()
paramT Type
t =
      if Bool
functor Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isBuiltinType Type
t)
      then (String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> (Type -> String) -> Type -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
printTypeName) Type
t Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"' a"
      else (String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> (Type -> String) -> Type -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
printTypeName) Type
t
    types :: [Type]
    types :: [Type]
types = Parameter -> Type
paramType (Parameter -> Type) -> [Parameter] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Function -> [Parameter]
funPars Function
fun
    returnType :: Doc ()
    returnType :: Doc ()
returnType =
      if Bool
functor
      then (String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> (Function -> String) -> Function -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
printTypeName (Type -> String) -> (Function -> Type) -> Function -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Function -> Type
funType) Function
fun Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"' a"
      else (String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> (Function -> String) -> Function -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
printTypeName (Type -> String) -> (Function -> Type) -> Function -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Function -> Type
funType) Function
fun
    paramsNames :: [Doc ()]
    paramsNames :: [Doc ()]
paramsNames = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> (Parameter -> String) -> Parameter -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (LabelName -> String)
-> (Parameter -> LabelName) -> Parameter -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parameter -> LabelName
paramName (Parameter -> Doc ()) -> [Parameter] -> [Doc ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Function -> [Parameter]
funPars Function
fun
    withBody :: Doc ()
    withBody :: Doc ()
withBody =
      Doc ()
funName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
args Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"=" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
      (String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> (Function -> String) -> Function -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String -> Exp -> String
printExp Bool
functor String
functorParam (Exp -> String) -> (Function -> Exp) -> Function -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Function -> Exp
funBody) Function
fun
    args :: Doc ()
    args :: Doc ()
args =
      if Bool
functor
      then [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep (String -> Doc ()
forall a. IsString a => String -> a
fromString String
functorParam Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
: [Doc ()]
paramsNames)
      else [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep [Doc ()]
paramsNames
    functorParam :: String
    functorParam :: String
functorParam = String -> String
mkFunctorParam String
"a"
    mkFunctorParam :: String -> String
    mkFunctorParam :: String -> String
mkFunctorParam String
a =
      if String
a String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (String
l String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
paramNames)
      then String
a
      else String -> String
mkFunctorParam (String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'")
      where
        l :: String
        l :: String
l = LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList LabelName
lName
        paramNames :: [String]
        paramNames :: [String]
paramNames = LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (LabelName -> String)
-> (Parameter -> LabelName) -> Parameter -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parameter -> LabelName
paramName (Parameter -> String) -> [Parameter] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Function -> [Parameter]
funPars Function
fun

printerBindings :: ModuleName   -- Abs module name.
                -> [Type]       -- AST category names.
                -> [BuiltinCat] -- Used builtins.
                -> [CatName]    -- User defined tokens names.
                -> Doc ()
printerBindings :: String -> [Type] -> [BuiltinCat] -> [LabelName] -> Doc ()
printerBindings String
absName [Type]
astCats [BuiltinCat]
builtins [LabelName]
toks = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc ()
"-- Binding the pretty printers."
  , [(Doc (), Doc ())] -> Doc ()
prPrinterBindings ([(Doc (), Doc ())] -> Doc ()) -> [(Doc (), Doc ())] -> Doc ()
forall a b. (a -> b) -> a -> b
$ [Doc ()] -> [Doc ()] -> [(Doc (), Doc ())]
forall a b. [a] -> [b] -> [(a, b)]
zip [Doc ()]
agdaPrinters [Doc ()]
agdaTypes
  , Doc ()
forall ann. Doc ann
emptyDoc
  , [(Doc (), (Doc (), Doc ()))] -> Doc ()
prPrinterPragmas ([(Doc (), (Doc (), Doc ()))] -> Doc ())
-> [(Doc (), (Doc (), Doc ()))] -> Doc ()
forall a b. (a -> b) -> a -> b
$ [Doc ()] -> [(Doc (), Doc ())] -> [(Doc (), (Doc (), Doc ()))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Doc ()]
agdaPrinters [(Doc (), Doc ())]
hsTypes
  ]
  where

    agdaPrinters :: [Doc ()]
    agdaPrinters :: [Doc ()]
agdaPrinters =
      (Type -> Doc ()) -> [Type] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (\Type
t -> Doc ()
"print" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall a. IsString a => String -> a
fromString (Type -> String
identType (Type -> String) -> Type -> String
forall a b. (a -> b) -> a -> b
$ Type -> Type
avoidResWordsType Type
t)) [Type]
astCats
      [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++
      (LabelName -> Doc ()) -> [LabelName] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (\LabelName
t -> Doc ()
"print" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall a. IsString a => String -> a
fromString (LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (LabelName -> String) -> LabelName -> String
forall a b. (a -> b) -> a -> b
$ LabelName -> LabelName
avoidAgdaReservedWords LabelName
t)) [LabelName]
toks
      [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++
      (BuiltinCat -> Doc ()) -> [BuiltinCat] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (\BuiltinCat
b -> Doc ()
"print" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> BuiltinCat -> Doc ()
builtinDoc BuiltinCat
b) [BuiltinCat]
builtins

    agdaTypes :: [Doc ()]
    agdaTypes :: [Doc ()]
agdaTypes =
      (Type -> Doc ()) -> [Type] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> (Type -> String) -> Type -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
prettyType (Type -> String) -> (Type -> Type) -> Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
avoidResWordsType) [Type]
astCats
      [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++
      (LabelName -> Doc ()) -> [LabelName] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> (LabelName -> String) -> LabelName -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (LabelName -> String)
-> (LabelName -> LabelName) -> LabelName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelName -> LabelName
avoidAgdaReservedWords) [LabelName]
toks
      [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++
      (BuiltinCat -> Doc ()) -> [BuiltinCat] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map BuiltinCat -> Doc ()
builtinDoc [BuiltinCat]
builtins

    -- hs types with names suggestions
    hsTypes :: [(Doc (), Doc())]
    hsTypes :: [(Doc (), Doc ())]
hsTypes =
      (Type -> (Doc (), Doc ())) -> [Type] -> [(Doc (), Doc ())]
forall a b. (a -> b) -> [a] -> [b]
map
      (\Type
t ->
        if Type -> Bool
isListType Type
t
        then
          ( Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
brackets (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String
forall a. [a] -> [a] -> [a]
(++) (String
absName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".") (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Type -> String
printTypeName Type
t
          , String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ Type -> String
nameSuggestion Type
t
          )
        else
          ( String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String
forall a. [a] -> [a] -> [a]
(++) (String
absName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".") (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Type -> String
printTypeName Type
t
          , String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ Type -> String
nameSuggestion Type
t
          )
      )
      [Type]
astCats
      [(Doc (), Doc ())] -> [(Doc (), Doc ())] -> [(Doc (), Doc ())]
forall a. [a] -> [a] -> [a]
++
      (LabelName -> (Doc (), Doc ()))
-> [LabelName] -> [(Doc (), Doc ())]
forall a b. (a -> b) -> [a] -> [b]
map (\LabelName
t -> (String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String
forall a. [a] -> [a] -> [a]
(++) (String
absName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".") (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList LabelName
t, Doc ()
"x")) [LabelName]
toks
      [(Doc (), Doc ())] -> [(Doc (), Doc ())] -> [(Doc (), Doc ())]
forall a. [a] -> [a] -> [a]
++
      (BuiltinCat -> (Doc (), Doc ()))
-> [BuiltinCat] -> [(Doc (), Doc ())]
forall a b. (a -> b) -> [a] -> [b]
map (\BuiltinCat
b -> (BuiltinCat -> Doc ()
builtinDoc BuiltinCat
b, Doc ()
"x")) [BuiltinCat]
builtins

    builtinDoc :: BuiltinCat -> Doc ()
    builtinDoc :: BuiltinCat -> Doc ()
builtinDoc BuiltinCat
b = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ LabelName -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (LabelName -> String) -> LabelName -> String
forall a b. (a -> b) -> a -> b
$ BuiltinCat -> LabelName
printBuiltinCat BuiltinCat
b

prPrinterBindings :: [(Doc (), Doc ())] -> Doc ()
prPrinterBindings :: [(Doc (), Doc ())] -> Doc ()
prPrinterBindings [(Doc (), Doc ())]
names = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc ()
"postulate"
  , Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ ((Doc (), Doc ()) -> Doc ()) -> [(Doc (), Doc ())] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Doc (), Doc ()) -> Doc ()
prPrinterBinding [(Doc (), Doc ())]
names
  ]

prPrinterBinding :: (Doc (), Doc ()) -> Doc ()
prPrinterBinding :: (Doc (), Doc ()) -> Doc ()
prPrinterBinding (Doc ()
agdaPrinter, Doc ()
agdaType) =
  Doc ()
agdaPrinter Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
agdaType Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
uArrow Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"#String"

prPrinterPragmas :: [(Doc (), (Doc (), Doc()))] -> Doc ()
prPrinterPragmas :: [(Doc (), (Doc (), Doc ()))] -> Doc ()
prPrinterPragmas [(Doc (), (Doc (), Doc ()))]
names = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ ((Doc (), (Doc (), Doc ())) -> Doc ())
-> [(Doc (), (Doc (), Doc ()))] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Doc (), (Doc (), Doc ())) -> Doc ()
prPrinterPragma [(Doc (), (Doc (), Doc ()))]
names

prPrinterPragma :: (Doc (), (Doc (), Doc())) -> Doc ()
prPrinterPragma :: (Doc (), (Doc (), Doc ())) -> Doc ()
prPrinterPragma (Doc ()
agdaPrinter, (Doc ()
hsType, Doc ()
varName)) = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep
  [ Doc ()
"{-# COMPILE GHC"
  , Doc ()
agdaPrinter Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"="
  , Doc ()
forall ann. Doc ann
backslash Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
varName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"->" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"Data.Text.pack"
  , Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ Doc ()
"printTree" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens (Doc ()
varName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"::" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
hsType)
  , Doc ()
"#-}"]