{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
module BNFC.Backend.Agda (makeAgda) where
import Prelude hiding ((<>))
import Control.Monad.State hiding (when)
import Data.Bifunctor (second)
import Data.Char
import Data.Function (on)
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty((:|)))
import qualified Data.List.NonEmpty as List1
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (IsString)
import BNFC.CF
import BNFC.Backend.Base (Backend, mkfile)
import BNFC.Backend.Haskell.HsOpts
import BNFC.Backend.Haskell.CFtoAbstract (DefCfg(..), definedRules')
import BNFC.Backend.Haskell.Utils (parserName, catToType, comment)
import BNFC.Options (SharedOptions, TokenText(..), tokenText, functor)
import BNFC.PrettyPrint
import BNFC.Utils (ModuleName, replace, when, table)
data ConstructorStyle
= UnnamedArg
| NamedArg
data ImportNumeric
= YesImportNumeric
| NoImportNumeric
deriving (ImportNumeric -> ImportNumeric -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ImportNumeric -> ImportNumeric -> Bool
$c/= :: ImportNumeric -> ImportNumeric -> Bool
== :: ImportNumeric -> ImportNumeric -> Bool
$c== :: ImportNumeric -> ImportNumeric -> Bool
Eq)
makeAgda
:: String
-> SharedOptions
-> CF
-> Backend
makeAgda :: [Char] -> SharedOptions -> CF -> Backend
makeAgda [Char]
time SharedOptions
opts CF
cf = do
forall c. FileContent c => [Char] -> MakeComment -> c -> Backend
mkfile (SharedOptions -> [Char]
agdaASTFile SharedOptions
opts) MakeComment
comment forall a b. (a -> b) -> a -> b
$
[Char]
-> Bool -> TokenText -> [Char] -> [Char] -> [Char] -> CF -> Doc
cf2AgdaAST [Char]
time (SharedOptions -> Bool
functor SharedOptions
opts) (SharedOptions -> TokenText
tokenText SharedOptions
opts) (SharedOptions -> [Char]
agdaASTFileM SharedOptions
opts) (SharedOptions -> [Char]
absFileM SharedOptions
opts) (SharedOptions -> [Char]
printerFileM SharedOptions
opts) CF
cf
forall c. FileContent c => [Char] -> MakeComment -> c -> Backend
mkfile (SharedOptions -> [Char]
agdaParserFile SharedOptions
opts) MakeComment
comment forall a b. (a -> b) -> a -> b
$
[Char]
-> TokenText
-> [Char]
-> [Char]
-> [Char]
-> [Char]
-> Maybe [Char]
-> [Cat]
-> Doc
cf2AgdaParser [Char]
time (SharedOptions -> TokenText
tokenText SharedOptions
opts) (SharedOptions -> [Char]
agdaParserFileM SharedOptions
opts) (SharedOptions -> [Char]
agdaASTFileM SharedOptions
opts) (SharedOptions -> [Char]
errFileM SharedOptions
opts) (SharedOptions -> [Char]
happyFileM SharedOptions
opts)
Maybe [Char]
layoutMod
[Cat]
parserCats
forall c. FileContent c => [Char] -> MakeComment -> c -> Backend
mkfile (SharedOptions -> [Char]
agdaLibFile SharedOptions
opts) MakeComment
comment forall a b. (a -> b) -> a -> b
$
[Char] -> Doc
agdaLibContents (SharedOptions -> [Char]
agdaLibFileM SharedOptions
opts)
forall c. FileContent c => [Char] -> MakeComment -> c -> Backend
mkfile (SharedOptions -> [Char]
agdaMainFile SharedOptions
opts) MakeComment
comment forall a b. (a -> b) -> a -> b
$
[Char] -> [Char] -> [Char] -> [Char] -> Bool -> Cat -> Doc
agdaMainContents (SharedOptions -> [Char]
agdaMainFileM SharedOptions
opts) (SharedOptions -> [Char]
agdaLibFileM SharedOptions
opts) (SharedOptions -> [Char]
agdaASTFileM SharedOptions
opts) (SharedOptions -> [Char]
agdaParserFileM SharedOptions
opts)
(CF -> Bool
hasLayout CF
cf)
(CF -> Cat
firstEntry CF
cf)
where
parserCats :: [Cat]
parserCats :: [Cat]
parserCats = forall a. NonEmpty a -> [a]
List1.toList forall a b. (a -> b) -> a -> b
$ forall f. CFG f -> List1 Cat
allEntryPoints CF
cf
layoutMod :: Maybe String
layoutMod :: Maybe [Char]
layoutMod = forall m. Monoid m => Bool -> m -> m
when (CF -> Bool
hasLayout CF
cf) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (SharedOptions -> [Char]
layoutFileM SharedOptions
opts)
cf2AgdaAST
:: String
-> Bool
-> TokenText
-> String
-> String
-> String
-> CF
-> Doc
cf2AgdaAST :: [Char]
-> Bool -> TokenText -> [Char] -> [Char] -> [Char] -> CF -> Doc
cf2AgdaAST [Char]
time Bool
havePos TokenText
tokenText [Char]
mod [Char]
amod [Char]
pmod CF
cf = [Doc] -> Doc
vsep forall a b. (a -> b) -> a -> b
$
[ [Char] -> [Char] -> Doc
preamble [Char]
time [Char]
"abstract syntax data types"
, [Doc] -> Doc
hsep [ Doc
"module", [Char] -> Doc
text [Char]
mod, Doc
"where" ]
, ImportNumeric -> Bool -> Bool -> Bool -> Doc
imports ImportNumeric
YesImportNumeric Bool
False Bool
usesPos Bool
havePos
, forall m. Monoid m => Bool -> m -> m
when Bool
usesString forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep [ Doc
"String", Doc
equals, forall a. IsString a => a
listT, forall a. IsString a => a
charT ]
, TokenText -> Bool -> [[Char]] -> Doc
importPragmas TokenText
tokenText Bool
usesPos
[ [[Char]] -> [Char]
unwords [ [Char]
"qualified", [Char]
amod ]
, [[Char]] -> [Char]
unwords [ [Char]
pmod, [Char]
"(printTree)" ]
]
, forall m. Monoid m => Bool -> m -> m
when Bool
usesPos Doc
defineIntAndPair
, forall m. Monoid m => Bool -> m -> m
when Bool
havePos Doc
defineBNFCPosition
, [Doc] -> Doc
vsep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ [Char] -> TokenText -> [Char] -> Bool -> Doc
prToken [Char]
amod TokenText
tokenText) [([Char], Bool)]
tcats
, [Char] -> Bool -> ConstructorStyle -> [Data] -> Doc
absyn [Char]
amod Bool
havePos ConstructorStyle
NamedArg [Data]
dats
, Bool -> CF -> Doc
definedRules Bool
havePos CF
cf
, [Char] -> [Cat] -> Doc
printers [Char]
amod [Cat]
printerCats
, Doc
empty
]
where
dats :: [Data]
dats :: [Data]
dats = CF -> [Data]
cf2data CF
cf
tcats :: [(TokenCat, Bool)]
tcats :: [([Char], Bool)]
tcats = (if forall f. CFG f -> Bool
hasIdent CF
cf then (([Char]
catIdent, Bool
False) forall a. a -> [a] -> [a]
:) else forall a. a -> a
id)
[ (forall a. WithPosition a -> a
wpThing RString
name, Bool
b) | TokenReg RString
name Bool
b Reg
_ <- forall function. CFG function -> [Pragma]
cfgPragmas CF
cf ]
printerCats :: [Cat]
printerCats :: [Cat]
printerCats = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (CF -> [Data]
getAbstractSyntax CF
cf)
, forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Cat
TokenCat forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
List.nub forall a b. (a -> b) -> a -> b
$ forall function. CFG function -> [[Char]]
cfgLiterals CF
cf forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [([Char], Bool)]
tcats
]
usesString :: Bool
usesString = [Char]
"String" forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall function. CFG function -> [[Char]]
cfgLiterals CF
cf
usesPos :: Bool
usesPos = Bool
havePos Bool -> Bool -> Bool
|| forall f. CFG f -> Bool
hasPositionTokens CF
cf
defineIntAndPair :: Doc
defineIntAndPair = [Doc] -> Doc
vsep
[ [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ Doc
"postulate" ]
, forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc
text) forall a b. (a -> b) -> a -> b
$ [Char] -> [[[Char]]] -> [[Char]]
table [Char]
" "
[ [ forall a. IsString a => a
intT, [Char]
":", [Char]
"Set" ]
, [ forall a. IsString a => a
intToNatT, [Char]
":", forall a. IsString a => a
intT, forall a. IsString a => a
uArrow , forall a. IsString a => a
natT ]
, [ forall a. IsString a => a
natToIntT, [Char]
":", forall a. IsString a => a
natT, forall a. IsString a => a
uArrow , forall a. IsString a => a
intT ]
]
]
, [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\ [Char]
s -> [Doc] -> Doc
hsep [ Doc
"{-#", Doc
"COMPILE", Doc
"GHC", [Char] -> Doc
text [Char]
s, Doc
"#-}" ]) forall a b. (a -> b) -> a -> b
$
[Char] -> [[[Char]]] -> [[Char]]
table [Char]
" = "
[ [ forall a. IsString a => a
intT, [Char]
"type Prelude.Int" ]
, [ forall a. IsString a => a
intToNatT, [Char]
"Prelude.toInteger" ]
, [ forall a. IsString a => a
natToIntT, [Char]
"Prelude.fromInteger" ]
]
, [Doc] -> Doc
vcat
[ Doc
"data #Pair (A B : Set) : Set where"
, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ Doc
"#pair : A → B → #Pair A B"
]
, Doc
"{-# COMPILE GHC #Pair = data (,) ((,)) #-}"
]
defineBNFCPosition :: Doc
defineBNFCPosition =
[Doc] -> Doc
hsep [ forall a. IsString a => a
posT, Doc
equals, forall a. IsString a => a
maybeT, Doc -> Doc
parens Doc
intPairT ]
cf2AgdaParser
:: String
-> TokenText
-> String
-> String
-> String
-> String
-> Maybe String
-> [Cat]
-> Doc
cf2AgdaParser :: [Char]
-> TokenText
-> [Char]
-> [Char]
-> [Char]
-> [Char]
-> Maybe [Char]
-> [Cat]
-> Doc
cf2AgdaParser [Char]
time TokenText
tokenText [Char]
mod [Char]
astmod [Char]
emod [Char]
pmod Maybe [Char]
layoutMod [Cat]
cats = [Doc] -> Doc
vsep forall a b. (a -> b) -> a -> b
$
[ [Char] -> [Char] -> Doc
preamble [Char]
time [Char]
"parsers"
, [Doc] -> Doc
hsep [ Doc
"module", [Char] -> Doc
text [Char]
mod, Doc
"where" ]
, ImportNumeric -> Bool -> Bool -> Bool -> Doc
imports ImportNumeric
NoImportNumeric (forall a. Maybe a -> Bool
isJust Maybe [Char]
layoutMod) Bool
False Bool
False
, [Char] -> [[Char]] -> Doc
importCats [Char]
astmod (forall a. Eq a => [a] -> [a]
List.nub [[Char]]
cs)
, TokenText -> Bool -> [[Char]] -> Doc
importPragmas TokenText
tokenText Bool
False forall a b. (a -> b) -> a -> b
$ [ MakeComment
qual [Char]
emod, [Char]
pmod] forall a. [a] -> [a] -> [a]
++ forall a. Maybe a -> [a]
maybeToList (MakeComment
qual forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Char]
layoutMod)
, Doc
"-- Error monad of BNFC"
, [Char] -> Doc
prErrM [Char]
emod
, Doc
"-- Happy parsers"
, TokenText -> Maybe [Char] -> [Cat] -> Doc
parsers TokenText
tokenText Maybe [Char]
layoutMod [Cat]
cats
, Doc
empty
]
where
cs :: [String]
cs :: [[Char]]
cs = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Cat -> Maybe [Char]
baseCat [Cat]
cats
baseCat :: Cat -> Maybe String
baseCat :: Cat -> Maybe [Char]
baseCat = \case
Cat [Char]
s -> forall a. a -> Maybe a
Just [Char]
s
CoercCat [Char]
s Integer
_ -> forall a. a -> Maybe a
Just [Char]
s
TokenCat [Char]
"Char" -> forall a. Maybe a
Nothing
TokenCat [Char]
s -> forall a. a -> Maybe a
Just [Char]
s
ListCat Cat
c -> Cat -> Maybe [Char]
baseCat Cat
c
qual :: MakeComment
qual [Char]
m = [Char]
"qualified " forall a. [a] -> [a] -> [a]
++ [Char]
m
uArrow, charT, integerT, doubleT, boolT, listT, maybeT, nothingT, justT,
intT, natT, intToNatT, natToIntT, pairT, posT, stringT, stringFromListT
:: IsString a => a
uArrow :: forall a. IsString a => a
uArrow = a
"→"
charT :: forall a. IsString a => a
charT = a
"Char"
integerT :: forall a. IsString a => a
integerT = a
"Integer"
doubleT :: forall a. IsString a => a
doubleT = a
"Double"
boolT :: forall a. IsString a => a
boolT = a
"#Bool"
listT :: forall a. IsString a => a
listT = a
"#List"
maybeT :: forall a. IsString a => a
maybeT = a
"#Maybe"
nothingT :: forall a. IsString a => a
nothingT = a
"#nothing"
justT :: forall a. IsString a => a
justT = a
"#just"
intT :: forall a. IsString a => a
intT = a
"#Int"
natT :: forall a. IsString a => a
natT = a
"#Nat"
intToNatT :: forall a. IsString a => a
intToNatT = a
"#intToNat"
natToIntT :: forall a. IsString a => a
natToIntT = a
"#natToInt"
pairT :: forall a. IsString a => a
pairT = a
"#Pair"
posT :: forall a. IsString a => a
posT = a
"#BNFCPosition"
stringT :: forall a. IsString a => a
stringT = a
"#String"
stringFromListT :: forall a. IsString a => a
stringFromListT = a
"#stringFromList"
intPairT :: Doc
intPairT :: Doc
intPairT = [Doc] -> Doc
hsep [ forall a. IsString a => a
pairT, forall a. IsString a => a
intT, forall a. IsString a => a
intT ]
preamble
:: String
-> String
-> Doc
preamble :: [Char] -> [Char] -> Doc
preamble [Char]
_time [Char]
what = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$
[ [Doc] -> Doc
hcat [ Doc
"-- Agda bindings for the Haskell ", [Char] -> Doc
text [Char]
what, Doc
"." ]
]
imports
:: ImportNumeric
-> Bool
-> Bool
-> Bool
-> Doc
imports :: ImportNumeric -> Bool -> Bool -> Bool -> Doc
imports ImportNumeric
numeric Bool
layout Bool
pos Bool
needMaybe = [Doc] -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ([Char], [Doc], [([Char], Doc)]) -> Doc
prettyImport forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
[ forall m. Monoid m => Bool -> m -> m
when Bool
layout
[ ([Char]
"Agda.Builtin.Bool", [], [([Char]
"Bool", forall a. IsString a => a
boolT)]) ]
, [ ([Char]
"Agda.Builtin.Char", [forall a. IsString a => a
charT], [] ) ]
, forall m. Monoid m => Bool -> m -> m
when (ImportNumeric
numeric forall a. Eq a => a -> a -> Bool
== ImportNumeric
YesImportNumeric) [([Char], [Doc], [([Char], Doc)])]
importNumeric
, [ ([Char]
"Agda.Builtin.List", [Doc
"[]", Doc
"_∷_"], [([Char]
"List", forall a. IsString a => a
listT)]) ]
, forall m. Monoid m => Bool -> m -> m
when Bool
needMaybe
[ ([Char]
"Agda.Builtin.Maybe", [], [([Char]
"Maybe", forall a. IsString a => a
maybeT), ([Char]
"nothing", forall a. IsString a => a
nothingT), ([Char]
"just", forall a. IsString a => a
justT)]) ]
, forall m. Monoid m => Bool -> m -> m
when Bool
pos
[ ([Char]
"Agda.Builtin.Nat", [], [([Char]
"Nat" , forall a. IsString a => a
natT )]) ]
, [ ([Char]
"Agda.Builtin.String", [], [([Char]
"String", forall a. IsString a => a
stringT), ([Char]
"primStringFromList", forall a. IsString a => a
stringFromListT) ]) ]
]
where
importNumeric :: [(String, [Doc], [(String, Doc)])]
importNumeric :: [([Char], [Doc], [([Char], Doc)])]
importNumeric =
[ ([Char]
"Agda.Builtin.Float public", [], [([Char]
"Float", forall a. IsString a => a
doubleT)])
, ([Char]
"Agda.Builtin.Int public", [], [([Char]
"Int", forall a. IsString a => a
integerT)])
, ([Char]
"Agda.Builtin.Int" , [], [([Char]
"pos", Doc
"#pos")])
]
prettyImport :: (String, [Doc], [(String, Doc)]) -> Doc
prettyImport :: ([Char], [Doc], [([Char], Doc)]) -> Doc
prettyImport ([Char]
m, [Doc]
use, [([Char], Doc)]
ren)
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], Doc)]
ren = Doc
pre
| Bool
otherwise = Int -> Doc -> Doc -> Doc -> Doc -> [Doc] -> Doc
prettyList Int
2 Doc
pre Doc
lparen Doc
rparen Doc
semi forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map (\ ([Char]
x, Doc
d) -> [Doc] -> Doc
hsep [[Char] -> Doc
text [Char]
x, Doc
"to", Doc
d ]) [([Char], Doc)]
ren
where
pre :: Doc
pre = [Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ Doc
"open", Doc
"import", [Char] -> Doc
text [Char]
m ]
, [ Doc
"using", Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hcat forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"; " [Doc]
use ]
, [ Doc
"renaming" | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], Doc)]
ren) ]
]
importCats
:: String
-> [String]
-> Doc
importCats :: [Char] -> [[Char]] -> Doc
importCats [Char]
m [[Char]]
cs = Int -> Doc -> Doc -> Doc -> Doc -> [Doc] -> Doc
prettyList Int
2 Doc
pre Doc
lparen Doc
rparen Doc
semi forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Doc
text [[Char]]
cs
where
pre :: Doc
pre = [Doc] -> Doc
hsep [ Doc
"open", Doc
"import", [Char] -> Doc
text [Char]
m, Doc
"using" ]
importPragmas
:: TokenText
-> Bool
-> [String]
-> Doc
importPragmas :: TokenText -> Bool -> [[Char]] -> Doc
importPragmas TokenText
tokenText Bool
pos [[Char]]
mods = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Doc
imp forall a b. (a -> b) -> a -> b
$ [[Char]]
base forall a. [a] -> [a] -> [a]
++ [[Char]]
mods
where
imp :: [Char] -> Doc
imp [Char]
s = [Doc] -> Doc
hsep [ Doc
"{-#", Doc
"FOREIGN", Doc
"GHC", Doc
"import", [Char] -> Doc
text [Char]
s, Doc
"#-}" ]
base :: [[Char]]
base = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ [Char]
"Prelude (" forall a. [a] -> [a] -> [a]
++ [Char]
preludeImports forall a. [a] -> [a] -> [a]
++ [Char]
")" ]
, forall m. Monoid m => Bool -> m -> m
when Bool
pos
[ [Char]
"qualified Prelude" ]
, case TokenText
tokenText of
TokenText
TextToken -> []
TokenText
StringToken -> []
TokenText
ByteStringToken -> [ [Char]
"qualified Data.ByteString.Char8 as BS" ]
, [ [Char]
"qualified Data.Text" ]
]
preludeImports :: [Char]
preludeImports = forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
", " forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ [Char]
"Bool", [Char]
"Char", [Char]
"Double", [Char]
"Integer", [Char]
"String", [Char]
"(.)" ]
, forall m. Monoid m => Bool -> m -> m
when Bool
pos
[ [Char]
"error" ]
]
prToken :: ModuleName -> TokenText -> String -> Bool -> Doc
prToken :: [Char] -> TokenText -> [Char] -> Bool -> Doc
prToken [Char]
amod TokenText
tokenText [Char]
t Bool
pos = [Doc] -> Doc
vsep
[ if Bool
pos then [Doc] -> Doc
vcat
[ [Doc] -> Doc
hsep [ Doc
"data", [Char] -> Doc
text [Char]
t, Doc
":", Doc
"Set", Doc
"where" ]
, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep
[ [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ MakeComment
agdaLower [Char]
t
, Doc
":"
, forall a. IsString a => a
pairT
, Doc -> Doc
parens Doc
intPairT
, Cat -> Doc
prettyCat Cat
typ
, forall a. IsString a => a
uArrow, [Char] -> Doc
text [Char]
t
]
]
else ConstructorStyle -> [Char] -> [([Char], [Cat])] -> Doc
prettyData ConstructorStyle
UnnamedArg [Char]
t [(MakeComment
agdaLower [Char]
t, [ Cat
typ ])]
, [Char] -> [Char] -> [Char] -> [([Char], [Cat])] -> Doc
pragmaData [Char]
amod [Char]
t [Char]
t [([Char]
t, [])]
]
where
typ :: Cat
typ = case TokenText
tokenText of
TokenText
TextToken -> [Char] -> Cat
Cat [Char]
"#String"
TokenText
ByteStringToken -> [Char] -> Cat
Cat [Char]
"#String"
TokenText
StringToken -> Cat -> Cat
ListCat ([Char] -> Cat
Cat [Char]
"Char")
absyn :: ModuleName -> Bool -> ConstructorStyle -> [Data] -> Doc
absyn :: [Char] -> Bool -> ConstructorStyle -> [Data] -> Doc
absyn [Char]
_amod Bool
_havePos ConstructorStyle
_style [] = Doc
empty
absyn [Char]
amod Bool
havePos ConstructorStyle
style [Data]
ds = [Doc] -> Doc
vsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc
"mutual" forall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Bool -> ConstructorStyle -> Data -> [Doc]
prData [Char]
amod Bool
havePos ConstructorStyle
style) forall a b. (a -> b) -> a -> b
$ [Data]
ds
prData :: ModuleName -> Bool -> ConstructorStyle -> Data -> [Doc]
prData :: [Char] -> Bool -> ConstructorStyle -> Data -> [Doc]
prData [Char]
amod Bool
True ConstructorStyle
style (Cat [Char]
d, [([Char], [Cat])]
cs) = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ [Doc] -> Doc
hsep [ [Char] -> Doc
text [Char]
d, Doc
equals, [Char] -> Doc
text (MakeComment
sanitize [Char]
primed), forall a. IsString a => a
posT ] ]
, [Char]
-> ConstructorStyle
-> [Char]
-> [Char]
-> [([Char], [Cat])]
-> [Doc]
prData' [Char]
amod ConstructorStyle
style (MakeComment
addP [Char]
d) [Char]
primed [([Char], [Cat])]
cs'
]
where
sanitize :: MakeComment
sanitize = forall a. Eq a => a -> a -> [a] -> [a]
replace Char
'_' Char
'-'
primed :: [Char]
primed = [Char]
d forall a. [a] -> [a] -> [a]
++ [Char]
"'"
param :: [Char]
param = [Char]
"Pos#"
addP :: MakeComment
addP [Char]
c = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [MakeComment
sanitize [Char]
c, [Char]
"' ", [Char]
param]
cs' :: [([Char], [Cat])]
cs' = forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a b. (a -> b) -> a -> b
$ \ [Cat]
cats -> [Char] -> Cat
Cat [Char]
param forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Cat -> Cat
addParam [Cat]
cats) [([Char], [Cat])]
cs
addParam :: Cat -> Cat
addParam :: Cat -> Cat
addParam = \case
Cat [Char]
c -> [Char] -> Cat
Cat forall a b. (a -> b) -> a -> b
$ MakeComment
addP [Char]
c
ListCat Cat
c -> Cat -> Cat
ListCat forall a b. (a -> b) -> a -> b
$ Cat -> Cat
addParam Cat
c
Cat
c -> Cat
c
prData [Char]
amod Bool
False ConstructorStyle
style (Cat [Char]
d, [([Char], [Cat])]
cs) = [Char]
-> ConstructorStyle
-> [Char]
-> [Char]
-> [([Char], [Cat])]
-> [Doc]
prData' [Char]
amod ConstructorStyle
style [Char]
d [Char]
d [([Char], [Cat])]
cs
prData [Char]
_ Bool
_ ConstructorStyle
_ (Cat
c , [([Char], [Cat])]
_ ) = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"prData: unexpected category " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Cat
c
prData' :: ModuleName -> ConstructorStyle -> String -> String -> [(Fun, [Cat])] -> [Doc]
prData' :: [Char]
-> ConstructorStyle
-> [Char]
-> [Char]
-> [([Char], [Cat])]
-> [Doc]
prData' [Char]
amod ConstructorStyle
style [Char]
d [Char]
haskellDataName [([Char], [Cat])]
cs =
[ ConstructorStyle -> [Char] -> [([Char], [Cat])] -> Doc
prettyData ConstructorStyle
style [Char]
d [([Char], [Cat])]
cs
, [Char] -> [Char] -> [Char] -> [([Char], [Cat])] -> Doc
pragmaData [Char]
amod (forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
words [Char]
d) [Char]
haskellDataName [([Char], [Cat])]
cs
]
prErrM :: ModuleName -> Doc
prErrM :: [Char] -> Doc
prErrM [Char]
emod = [Doc] -> Doc
vsep forall a b. (a -> b) -> a -> b
$ [Char]
-> ConstructorStyle
-> [Char]
-> [Char]
-> [([Char], [Cat])]
-> [Doc]
prData' [Char]
emod ConstructorStyle
UnnamedArg [Char]
"Err A" [Char]
"Err"
[ ([Char]
"Ok" , [[Char] -> Cat
Cat [Char]
"A"])
, ([Char]
"Bad", [Cat -> Cat
ListCat forall a b. (a -> b) -> a -> b
$ [Char] -> Cat
Cat [Char]
"Char"])
]
prettyData :: ConstructorStyle -> String -> [(Fun, [Cat])] -> Doc
prettyData :: ConstructorStyle -> [Char] -> [([Char], [Cat])] -> Doc
prettyData ConstructorStyle
style [Char]
d [([Char], [Cat])]
cs = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ [Doc] -> Doc
hsep [ Doc
"data", [Char] -> Doc
text [Char]
d, Doc
colon, Doc
"Set", Doc
"where" ] ]
, [(Doc, Doc)] -> [Doc]
mkTSTable forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (ConstructorStyle -> [Char] -> ([Char], [Cat]) -> (Doc, Doc)
prettyConstructor ConstructorStyle
style [Char]
d) [([Char], [Cat])]
cs
]
where
mkTSTable :: [(Doc,Doc)] -> [Doc]
mkTSTable :: [(Doc, Doc)] -> [Doc]
mkTSTable = forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc
text) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[[Char]]] -> [[Char]]
table [Char]
" : " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Doc, Doc) -> [[Char]]
mkRow
where
mkRow :: (Doc, Doc) -> [[Char]]
mkRow (Doc
c,Doc
t) = [ Doc -> [Char]
render Doc
c, Doc -> [Char]
render Doc
t ]
pragmaData :: ModuleName -> String -> String -> [(Fun, [Cat])] -> Doc
pragmaData :: [Char] -> [Char] -> [Char] -> [([Char], [Cat])] -> Doc
pragmaData [Char]
amod [Char]
d [Char]
haskellDataName [([Char], [Cat])]
cs =
Int -> Doc -> Doc -> Doc -> Doc -> [Doc] -> Doc
prettyList Int
2 Doc
pre Doc
lparen (Doc
rparen Doc -> Doc -> Doc
<+> Doc
"#-}") Doc
"|" forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [Char] -> Doc
prettyFun [Char]
amod forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [([Char], [Cat])]
cs
where
pre :: Doc
pre = [Doc] -> Doc
hsep
[ Doc
"{-#", Doc
"COMPILE", Doc
"GHC", [Char] -> Doc
text [Char]
d, Doc
equals, Doc
"data"
, [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
amod, [Char]
".", [Char]
haskellDataName ]
]
prettyConstructor :: ConstructorStyle -> String -> (Fun,[Cat]) -> (Doc,Doc)
prettyConstructor :: ConstructorStyle -> [Char] -> ([Char], [Cat]) -> (Doc, Doc)
prettyConstructor ConstructorStyle
style [Char]
d ([Char]
c, [Cat]
as) = ([Char] -> Doc
prettyCon [Char]
c,) forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Cat]
as then [Char] -> Doc
text [Char]
d else [Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$
[ ConstructorStyle -> [Cat] -> Doc
prettyConstructorArgs ConstructorStyle
style [Cat]
as
, forall a. IsString a => a
uArrow
, [Char] -> Doc
text [Char]
d
]
prettyConstructorArgs :: ConstructorStyle -> [Cat] -> Doc
prettyConstructorArgs :: ConstructorStyle -> [Cat] -> Doc
prettyConstructorArgs ConstructorStyle
style [Cat]
as =
case ConstructorStyle
style of
ConstructorStyle
UnnamedArg -> [Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
List.intersperse forall a. IsString a => a
uArrow [Doc]
ts
ConstructorStyle
NamedArg -> [Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\ (Doc
x :| [Doc]
xs, Doc
t) -> Doc -> Doc
parens ([Doc] -> Doc
hsep [Doc
x, [Doc] -> Doc
hsep [Doc]
xs, Doc
colon, Doc
t])) [(NonEmpty Doc, Doc)]
tel
where
ts :: [Doc]
ts = forall a b. (a -> b) -> [a] -> [b]
map Cat -> Doc
prettyCat [Cat]
as
ns :: [Doc]
ns = forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Show a => (Maybe a, [Char]) -> [Char]
subscript) forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [(Maybe Int, a)]
numberUniquely forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Cat -> [Char]
nameSuggestion [Cat]
as
tel :: [(NonEmpty Doc, Doc)]
tel = forall c a b. Eq c => ((a, b) -> c) -> [(a, b)] -> [(List1 a, b)]
aggregateOn (Doc -> [Char]
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Doc]
ns [Doc]
ts
deltaSubscript :: Int
deltaSubscript = Char -> Int
ord Char
'₀' forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0'
subscript :: (Maybe a, [Char]) -> [Char]
subscript (Maybe a
m, [Char]
s) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
s (\ a
n -> [Char]
s forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Int -> Char
chr forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
deltaSubscript forall a. Num a => a -> a -> a
+) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
ord) (forall a. Show a => a -> [Char]
show a
n)) Maybe a
m
aggregateOn :: Eq c => ((a,b) -> c) -> [(a,b)] -> [(List1 a,b)]
aggregateOn :: forall c a b. Eq c => ((a, b) -> c) -> [(a, b)] -> [(List1 a, b)]
aggregateOn (a, b) -> c
f
= forall a b. (a -> b) -> [a] -> [b]
map (\ NonEmpty (a, b)
p -> (forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
List1.map forall a b. (a, b) -> a
fst NonEmpty (a, b)
p, forall a b. (a, b) -> b
snd (forall a. NonEmpty a -> a
List1.head NonEmpty (a, b)
p)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (a, b) -> c
f)
nameSuggestion :: Cat -> String
nameSuggestion :: Cat -> [Char]
nameSuggestion = \case
ListCat Cat
c -> Cat -> [Char]
nameSuggestion Cat
c forall a. [a] -> [a] -> [a]
++ [Char]
"s"
CoercCat [Char]
d Integer
_ -> MakeComment
nameFor [Char]
d
Cat [Char]
d -> MakeComment
nameFor [Char]
d
TokenCat{} -> [Char]
"x"
nameFor :: String -> String
nameFor :: MakeComment
nameFor [Char]
d = [ Char -> Char
toLower forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
== Char
'#') [Char]
d ]
numberUniquely :: forall a. Ord a => [a] -> [(Maybe Int, a)]
numberUniquely :: forall a. Ord a => [a] -> [(Maybe Int, a)]
numberUniquely [a]
as = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> State (Frequency a) (Maybe Int, a)
step [a]
as forall s a. State s a -> s -> a
`evalState` forall k a. Map k a
Map.empty
where
counts :: Frequency a
counts :: Frequency a
counts = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> Frequency a -> Frequency a
incr) forall k a. Map k a
Map.empty [a]
as
step :: a -> State (Frequency a) (Maybe Int, a)
step :: a -> State (Frequency a) (Maybe Int, a)
step a
a = do
let n :: Int
n = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (forall a. HasCallStack => [Char] -> a
error [Char]
"numberUniquelyWith") a
a Frequency a
counts
if Int
n forall a. Eq a => a -> a -> Bool
== Int
1 then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, a
a) else do
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Frequency a -> Frequency a
incr a
a
(,a
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
type Frequency a = Map a Int
incr :: Ord a => a -> Frequency a -> Frequency a
incr :: forall a. Ord a => a -> Frequency a -> Frequency a
incr = forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. a -> Maybe a
Just Int
1) (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => a -> a
succ)
agdaDefCfg :: DefCfg
agdaDefCfg :: DefCfg
agdaDefCfg = DefCfg
{ sanitizeName :: MakeComment
sanitizeName = MakeComment
agdaLower
, hasType :: [Char]
hasType = [Char]
":"
, arrow :: [Char]
arrow = forall a. IsString a => a
uArrow
, lambda :: [Char]
lambda = [Char]
"λ"
, cons :: [Char]
cons = [Char]
"_∷_"
, convTok :: MakeComment
convTok = MakeComment
agdaLower
, convLitInt :: Exp -> Exp
convLitInt = \ Exp
e -> forall f. f -> Type -> [Exp' f] -> Exp' f
App [Char]
"#pos" Type
dummyType [Exp
e]
, polymorphism :: [Base] -> [Base]
polymorphism = (forall a. a -> Base' a
BaseT [Char]
"{a : Set}" forall a. a -> [a] -> [a]
:)
}
definedRules :: Bool -> CF -> Doc
definedRules :: Bool -> CF -> Doc
definedRules Bool
havePos = [Doc] -> Doc
vsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefCfg -> Bool -> CF -> [Doc]
definedRules' DefCfg
agdaDefCfg Bool
havePos
printers :: ModuleName -> [Cat] -> Doc
printers :: [Char] -> [Cat] -> Doc
printers [Char]
_amod [] = Doc
empty
printers [Char]
amod [Cat]
cats = [Doc] -> Doc
vsep
[ Doc
"-- Binding the pretty printers."
, [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ Doc
"postulate" forall a. a -> [a] -> [a]
: [(Doc, Doc)] -> [Doc]
mkTSTable (forall a b. (a -> b) -> [a] -> [b]
map (Cat -> (Doc, Doc)
prettyTySig) [Cat]
cats)
, [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Cat -> Doc
pragmaBind [Cat]
cats
]
where
prettyTySig :: Cat -> (Doc, Doc)
prettyTySig Cat
c = (Cat -> Doc
agdaPrinterName Cat
c, [Doc] -> Doc
hsep [ Cat -> Doc
prettyCat Cat
c, forall a. IsString a => a
uArrow, forall a. IsString a => a
stringT ])
pragmaBind :: Cat -> Doc
pragmaBind Cat
c = [Doc] -> Doc
hsep
[ Doc
"{-#", Doc
"COMPILE", Doc
"GHC", Cat -> Doc
agdaPrinterName Cat
c, Doc
equals, Doc
"\\", Doc
y, Doc
"->"
, Doc
"Data.Text.pack", Doc -> Doc
parens (Doc
"printTree" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Doc
y Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> Doc
t)), Doc
"#-}"
]
where
y :: Doc
y = [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ Cat -> [Char]
nameSuggestion Cat
c
t :: Doc
t = (Doc -> Doc) -> Doc -> Cat -> Doc
catToType (([Char] -> Doc
text [Char]
amod Doc -> Doc -> Doc
<> [Char] -> Doc
text [Char]
".") Doc -> Doc -> Doc
<>) Doc
empty Cat
c
parsers
:: TokenText
-> Maybe String
-> [Cat]
-> Doc
parsers :: TokenText -> Maybe [Char] -> [Cat] -> Doc
parsers TokenText
tokenText Maybe [Char]
layoutMod [Cat]
cats =
[Doc] -> Doc
vcat (Doc
"postulate" forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cat -> Doc
prettyTySig) [Cat]
cats)
Doc -> Doc -> Doc
$++$
[Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map Cat -> Doc
pragmaBind [Cat]
cats)
where
prettyTySig :: Cat -> Doc
prettyTySig :: Cat -> Doc
prettyTySig Cat
c = [Doc] -> Doc
hsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
[ [ Cat -> Doc
agdaParserName Cat
c, Doc
colon ]
, forall m. Monoid m => Bool -> m -> m
when Bool
layout [ forall a. IsString a => a
boolT, forall a. IsString a => a
uArrow ]
, [ forall a. IsString a => a
stringT, forall a. IsString a => a
uArrow, Doc
"Err", Cat -> Doc
prettyCatParens Cat
c ]
]
pragmaBind :: Cat -> Doc
pragmaBind :: Cat -> Doc
pragmaBind Cat
c = [Doc] -> Doc
hsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
[ [ Doc
"{-#", Doc
"COMPILE", Doc
"GHC", Cat -> Doc
agdaParserName Cat
c, Doc
equals ]
, forall m. Monoid m => Bool -> m -> m
when Bool
layout [ Doc
"\\", Doc
"tl", Doc
"->" ]
, [ Cat -> Doc
parserName Cat
c, Doc
"." ]
, forall m. Monoid m => Bool -> m -> m
when Bool
layout [ [Doc] -> Doc
hcat [ [Char] -> Doc
text [Char]
lmod, Doc
".", Doc
"resolveLayout" ], Doc
"tl", Doc
"." ]
, [ Doc
"myLexer" ]
, case TokenText
tokenText of
TokenText
TextToken -> []
TokenText
StringToken -> [ Doc
".", Doc
"Data.Text.unpack" ]
TokenText
ByteStringToken -> [ Doc
".", Doc
"BS.pack", Doc
".", Doc
"Data.Text.unpack" ]
, [ Doc
"#-}" ]
]
layout :: Bool
layout :: Bool
layout = forall a. Maybe a -> Bool
isJust Maybe [Char]
layoutMod
lmod :: String
lmod :: [Char]
lmod = forall a. HasCallStack => Maybe a -> a
fromJust Maybe [Char]
layoutMod
prettyFun :: ModuleName -> Fun -> Doc
prettyFun :: [Char] -> [Char] -> Doc
prettyFun [Char]
amod [Char]
c = [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
amod, [Char]
".", [Char]
c ]
prettyCon :: Fun -> Doc
prettyCon :: [Char] -> Doc
prettyCon = [Char] -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. MakeComment
agdaLower
agdaLower :: String -> String
agdaLower :: MakeComment
agdaLower = MakeComment
avoidKeywords forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. (a -> a) -> [a] -> [a]
updateHead Char -> Char
toLower forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => a -> a -> [a] -> [a]
replace Char
'_' Char
'-'
where
updateHead :: (a -> a) -> [a] -> [a]
updateHead a -> a
_f [] = []
updateHead a -> a
f (a
x:[a]
xs) = a -> a
f a
x forall a. a -> [a] -> [a]
: [a]
xs
avoidKeywords :: MakeComment
avoidKeywords [Char]
s
| [Char]
s forall a. Ord a => a -> Set a -> Bool
`Set.member` Set [Char]
agdaKeywords = [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
"\'"
| Bool
otherwise = [Char]
s
agdaKeywords :: Set String
agdaKeywords :: Set [Char]
agdaKeywords = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
words [Char]
"abstract codata coinductive constructor data do eta-equality field forall hiding import in inductive infix infixl infixr instance let macro module mutual no-eta-equality open overlap pattern postulate primitive private public quote quoteContext quoteGoal quoteTerm record renaming rewrite Set syntax tactic unquote unquoteDecl unquoteDef using variable where with"
agdaParserName :: Cat -> Doc
agdaParserName :: Cat -> Doc
agdaParserName Cat
c = [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"parse" forall a. [a] -> [a] -> [a]
++ Cat -> [Char]
identCat Cat
c
agdaPrinterName :: Cat -> Doc
agdaPrinterName :: Cat -> Doc
agdaPrinterName Cat
c = [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"print" forall a. [a] -> [a] -> [a]
++ Cat -> [Char]
identCat (Cat -> Cat
normCat Cat
c)
prettyCat :: Cat -> Doc
prettyCat :: Cat -> Doc
prettyCat = \case
Cat [Char]
s -> [Char] -> Doc
text [Char]
s
TokenCat [Char]
s -> [Char] -> Doc
text [Char]
s
CoercCat [Char]
s Integer
_ -> [Char] -> Doc
text [Char]
s
ListCat Cat
c -> forall a. IsString a => a
listT Doc -> Doc -> Doc
<+> Cat -> Doc
prettyCatParens Cat
c
prettyCatParens :: Cat -> Doc
prettyCatParens :: Cat -> Doc
prettyCatParens Cat
c = Bool -> Doc -> Doc
parensIf (Cat -> Bool
compositeCat Cat
c) (Cat -> Doc
prettyCat Cat
c)
compositeCat :: Cat -> Bool
compositeCat :: Cat -> Bool
compositeCat = \case
Cat [Char]
c -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace [Char]
c
ListCat{} -> Bool
True
Cat
_ -> Bool
False
agdaLibContents
:: String
-> Doc
agdaLibContents :: [Char] -> Doc
agdaLibContents [Char]
mod = [Doc] -> Doc
vcat
[ Doc
"-- Basic I/O library."
, Doc
""
, Doc
"module" Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
mod Doc -> Doc -> Doc
<+> Doc
"where"
, Doc
""
, Doc
"open import Agda.Builtin.IO public using (IO)"
, Doc
"open import Agda.Builtin.List public using (List; []; _∷_)"
, Doc
"open import Agda.Builtin.String public using (String)"
, Doc
" renaming (primStringFromList to stringFromList)"
, Doc
"open import Agda.Builtin.Unit public using (⊤)"
, Doc
""
, Doc
"-- I/O monad."
, Doc
""
, Doc
"postulate"
, Doc
" return : ∀ {a} {A : Set a} → A → IO A"
, Doc
" _>>=_ : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B"
, Doc
""
, Doc
"{-# COMPILE GHC return = \\ _ _ -> return #-}"
, Doc
"{-# COMPILE GHC _>>=_ = \\ _ _ _ _ -> (>>=) #-}"
, Doc
""
, Doc
"infixl 1 _>>=_ _>>_"
, Doc
""
, Doc
"_>>_ : ∀ {b} {B : Set b} → IO ⊤ → IO B → IO B"
, Doc
"_>>_ = λ m m' → m >>= λ _ → m'"
, Doc
""
, Doc
"-- Co-bind and functoriality."
, Doc
""
, Doc
"infixr 1 _=<<_ _<$>_"
, Doc
""
, Doc
"_=<<_ : ∀ {a b} {A : Set a} {B : Set b} → (A → IO B) → IO A → IO B"
, Doc
"k =<< m = m >>= k"
, Doc
""
, Doc
"_<$>_ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → IO A → IO B"
, Doc
"f <$> m = do"
, Doc
" a ← m"
, Doc
" return (f a)"
, Doc
""
, Doc
"-- Binding basic I/O functionality."
, Doc
""
, Doc
"{-# FOREIGN GHC import qualified Data.Text #-}"
, Doc
"{-# FOREIGN GHC import qualified Data.Text.IO #-}"
, Doc
"{-# FOREIGN GHC import qualified System.Exit #-}"
, Doc
"{-# FOREIGN GHC import qualified System.Environment #-}"
, Doc
"{-# FOREIGN GHC import qualified System.IO #-}"
, Doc
""
, Doc
"postulate"
, Doc
" exitFailure : ∀{a} {A : Set a} → IO A"
, Doc
" getArgs : IO (List String)"
, Doc
" putStrLn : String → IO ⊤"
, Doc
" readFiniteFile : String → IO String"
, Doc
""
, Doc
"{-# COMPILE GHC exitFailure = \\ _ _ -> System.Exit.exitFailure #-}"
, Doc
"{-# COMPILE GHC getArgs = fmap (map Data.Text.pack) System.Environment.getArgs #-}"
, Doc
"{-# COMPILE GHC putStrLn = System.IO.putStrLn . Data.Text.unpack #-}"
, Doc
"{-# COMPILE GHC readFiniteFile = Data.Text.IO.readFile . Data.Text.unpack #-}"
]
agdaMainContents
:: String
-> String
-> String
-> String
-> Bool
-> Cat
-> Doc
agdaMainContents :: [Char] -> [Char] -> [Char] -> [Char] -> Bool -> Cat -> Doc
agdaMainContents [Char]
mod [Char]
lmod [Char]
amod [Char]
pmod Bool
layout Cat
c = [Doc] -> Doc
vcat
[ Doc
"-- Test for Agda binding of parser. Requires Agda >= 2.5.4."
, Doc
""
, Doc
"module" Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
mod Doc -> Doc -> Doc
<+> Doc
"where"
, forall m. Monoid m => Bool -> m -> m
when Bool
layout Doc
"\nopen import Agda.Builtin.Bool using (true)"
, Doc
"open import" Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
lmod
, Doc
"open import" Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
amod Doc -> Doc -> Doc
<+> Doc
"using" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Doc
printer)
, Doc
"open import" Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
pmod Doc -> Doc -> Doc
<+> Doc
"using" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Doc
"Err;" Doc -> Doc -> Doc
<+> Doc
parser)
, Doc
""
, Doc
"main : IO ⊤"
, Doc
"main = do"
, Doc
" file ∷ [] ← getArgs where"
, Doc
" _ → do"
, Doc
" putStrLn \"usage: Main <SourceFile>\""
, Doc
" exitFailure"
, Doc
" Err.ok result ←" Doc -> Doc -> Doc
<+> Doc
parseFun Doc -> Doc -> Doc
<+> Doc
"<$> readFiniteFile file where"
, Doc
" Err.bad msg → do"
, Doc
" putStrLn \"PARSE FAILED\\n\""
, Doc
" putStrLn (stringFromList msg)"
, Doc
" exitFailure"
, Doc
" putStrLn \"PARSE SUCCESSFUL\\n\""
, Doc
" putStrLn" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Doc
printer Doc -> Doc -> Doc
<+> Doc
"result")
]
where
printer :: Doc
printer = Cat -> Doc
agdaPrinterName Cat
c
parser :: Doc
parser = Cat -> Doc
agdaParserName Cat
c
parseFun :: Doc
parseFun = [Doc] -> Doc
hsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ [ [Doc
parser], forall m. Monoid m => Bool -> m -> m
when Bool
layout [Doc
"true"] ]