-- | Agda backend.
--
-- Generate bindings to Haskell data types for use in Agda.
--
-- Example for abstract syntax generated in Haskell backend:
--
-- > module CPP.Abs where
-- >
-- > import Prelude (Char, Double, Integer, String)
-- > import qualified Prelude as C (Eq, Ord, Show, Read)
-- >
-- > import qualified Data.Text
-- >
-- > newtype Ident = Ident Data.Text.Text
-- >   deriving (C.Eq, C.Ord, C.Show, C.Read)
-- >
-- > data Def = DFun Type Ident [Arg] [Stm]
-- >   deriving (C.Eq, C.Ord, C.Show, C.Read)
-- >
-- > data Arg = ADecl Type Ident
-- >   deriving (C.Eq, C.Ord, C.Show, C.Read)
-- >
-- > data Stm
-- >     = SExp Exp
-- >     | SInit Type Ident Exp
-- >     | SBlock [Stm]
-- >     | SIfElse Exp Stm Stm
-- >   deriving (C.Eq, C.Ord, C.Show, C.Read)
-- >
-- > data Exp
-- >
-- > data Type = Type_bool | Type_int | Type_double | Type_void
-- >   deriving (C.Eq, C.Ord, C.Show, C.Read)
--
-- This should be accompanied by the following Agda code:
--
-- > module CPP.AST where
-- >
-- > open import Agda.Builtin.Char using () renaming (Char to Char)
-- > open import Agda.Builtin.Float public using () renaming (Float to Double)
-- > open import Agda.Builtin.Int   public using () renaming (Int to Integer)
-- > open import Agda.Builtin.List using () renaming (List to #List)
-- > open import Agda.Builtin.String using () renaming
-- >   ( String to #String
-- >   ; primStringFromList to #stringFromList
-- >   )
-- >
-- > {-# FOREIGN GHC import Prelude (Char, Double, Integer, String) #-}
-- > {-# FOREIGN GHC import qualified Data.Text #-}
-- > {-# FOREIGN GHC import qualified CPP.Abs #-}
-- > {-# FOREIGN GHC import CPP.Print (printTree) #-}
-- >
-- > data Ident : Set where
-- >   ident : #String → Ident
-- >
-- > {-# COMPILE GHC Ident = data CPP.Abs.Ident (CPP.Abs.Ident) #-}
-- >
-- > data Def : Set where
-- >   dFun : (t : Type) (x : Ident) (as : List Arg) (ss : List Stm) → Def
-- >
-- > {-# COMPILE GHC Def = data CPP.Abs.Def (CPP.Abs.DFun) #-}
-- >
-- > data Arg : Set where
-- >   aDecl : (t : Type) (x : Ident) → Arg
-- >
-- > {-# COMPILE GHC Arg = data CPP.Abs.Arg (CPP.Abs.ADecl) #-}
-- >
-- > data Stm : Set where
-- >   sExp : (e : Exp) → Stm
-- >   sInit : (t : Type) (x : Ident) (e : Exp) → Stm
-- >   sBlock : (ss : List Stm) → Stm
-- >   sIfElse : (e : Exp) (s s' : Stm) → Stm
-- >
-- > {-# COMPILE GHC Stm = data CPP.Abs.Stm
-- >   ( CPP.Abs.SExp
-- >   | CPP.Abs.SInit
-- >   | CPP.Abs.SBlock
-- >   | CPP.Abs.SIfElse
-- >   ) #-}
-- >
-- > data Type : Set where
-- >   typeBool typeInt typeDouble typeVoid : Type
-- >
-- > {-# COMPILE GHC Type = data CPP.Abs.Type
-- >   ( CPP.Abs.Type_bool
-- >   | CPP.Abs.Type_int
-- >   | CPP.Abs.Type_double
-- >   | CPP.Abs.Type_void
-- >   ) #-}
-- >
-- > -- Binding the BNFC pretty printers.
-- >
-- > printIdent  : Ident → String
-- > printIdent (ident s) = String.fromList s
-- >
-- > postulate
-- >   printType    : Type    → String
-- >   printExp     : Exp     → String
-- >   printStm     : Stm     → String
-- >   printArg     : Arg     → String
-- >   printDef     : Def     → String
-- >   printProgram : Program → String
-- >
-- > {-# COMPILE GHC printType    = \ t -> Data.Text.pack (printTree (t :: CPP.Abs.Type)) #-}
-- > {-# COMPILE GHC printExp     = \ e -> Data.Text.pack (printTree (e :: CPP.Abs.Exp))  #-}
-- > {-# COMPILE GHC printStm     = \ s -> Data.Text.pack (printTree (s :: CPP.Abs.Stm))  #-}
-- > {-# COMPILE GHC printArg     = \ a -> Data.Text.pack (printTree (a :: CPP.Abs.Arg))  #-}
-- > {-# COMPILE GHC printDef     = \ d -> Data.Text.pack (printTree (d :: CPP.Abs.Def))  #-}
-- > {-# COMPILE GHC printProgram = \ p -> Data.Text.pack (printTree (p :: CPP.Abs.Program)) #-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

#if __GLASGOW_HASKELL__ >= 800
{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
#endif

module BNFC.Backend.Agda (makeAgda) where

import Prelude hiding ((<>))
import Control.Monad.State hiding (when)
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.Utils  (parserName, catToType, mkDefName, typeToHaskell')
import BNFC.Options                (SharedOptions, TokenText(..), tokenText)
import BNFC.PrettyPrint
import BNFC.Utils                  (ModuleName, replace, when, table)

type List1 = List1.NonEmpty

-- | How to print the types of constructors in Agda?

data ConstructorStyle
  = UnnamedArg  -- ^ Simply typed, like @E → S → S → S@.
  | NamedArg    -- ^ Dependently typed, like @(e : E) (s₁ s₂ : S) → S@.

-- | Import the builtin numeric types (content of some token categories)?

data ImportNumeric
  = YesImportNumeric  -- ^ Import the numeric types.
  | NoImportNumeric   -- ^ Don't import the numeric types.
  deriving (ImportNumeric -> ImportNumeric -> Bool
(ImportNumeric -> ImportNumeric -> Bool)
-> (ImportNumeric -> ImportNumeric -> Bool) -> Eq ImportNumeric
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)

-- | Entry-point for Agda backend.

makeAgda
  :: String         -- ^ Current time.
  -> SharedOptions  -- ^ Options.
  -> CF             -- ^ Grammar.
  -> Backend
makeAgda :: String -> SharedOptions -> CF -> Backend
makeAgda String
time SharedOptions
opts CF
cf = do
  -- Generate AST bindings.
  String -> Doc -> Backend
forall c. FileContent c => String -> c -> Backend
mkfile (SharedOptions -> String
agdaASTFile SharedOptions
opts) (Doc -> Backend) -> Doc -> Backend
forall a b. (a -> b) -> a -> b
$
    String -> TokenText -> String -> String -> String -> CF -> Doc
cf2AgdaAST String
time (SharedOptions -> TokenText
tokenText SharedOptions
opts) (SharedOptions -> String
agdaASTFileM SharedOptions
opts) (SharedOptions -> String
absFileM SharedOptions
opts) (SharedOptions -> String
printerFileM SharedOptions
opts) CF
cf
  -- Generate parser bindings.
  String -> Doc -> Backend
forall c. FileContent c => String -> c -> Backend
mkfile (SharedOptions -> String
agdaParserFile SharedOptions
opts) (Doc -> Backend) -> Doc -> Backend
forall a b. (a -> b) -> a -> b
$
    String
-> TokenText
-> String
-> String
-> String
-> String
-> Maybe String
-> [Cat]
-> Doc
cf2AgdaParser String
time (SharedOptions -> TokenText
tokenText SharedOptions
opts) (SharedOptions -> String
agdaParserFileM SharedOptions
opts) (SharedOptions -> String
agdaASTFileM SharedOptions
opts) (SharedOptions -> String
errFileM SharedOptions
opts) (SharedOptions -> String
happyFileM SharedOptions
opts)
      Maybe String
layoutMod
      [Cat]
parserCats
  -- Generate an I/O library for the test parser.
  String -> Doc -> Backend
forall c. FileContent c => String -> c -> Backend
mkfile (SharedOptions -> String
agdaLibFile SharedOptions
opts) (Doc -> Backend) -> Doc -> Backend
forall a b. (a -> b) -> a -> b
$
    String -> Doc
agdaLibContents (SharedOptions -> String
agdaLibFileM SharedOptions
opts)
  -- Generate test parser.
  String -> Doc -> Backend
forall c. FileContent c => String -> c -> Backend
mkfile (SharedOptions -> String
agdaMainFile SharedOptions
opts) (Doc -> Backend) -> Doc -> Backend
forall a b. (a -> b) -> a -> b
$
    String -> String -> String -> String -> Bool -> Cat -> Doc
agdaMainContents (SharedOptions -> String
agdaMainFileM SharedOptions
opts) (SharedOptions -> String
agdaLibFileM SharedOptions
opts) (SharedOptions -> String
agdaASTFileM SharedOptions
opts) (SharedOptions -> String
agdaParserFileM SharedOptions
opts)
      (CF -> Bool
hasLayout CF
cf)
      (CF -> Cat
firstEntry CF
cf)
  where
  -- | Generate parsers for the following non-terminals.
  --   This includes parsers for 'CoercCat' and 'ListCat'.
  parserCats :: [Cat]
  parserCats :: [Cat]
parserCats = NonEmpty Cat -> [Cat]
forall a. NonEmpty a -> [a]
List1.toList (NonEmpty Cat -> [Cat]) -> NonEmpty Cat -> [Cat]
forall a b. (a -> b) -> a -> b
$ CF -> NonEmpty Cat
forall f. CFG f -> NonEmpty Cat
allEntryPoints CF
cf
  -- | In case the grammar makes use of layout, pass also the generated layout Haskell module.
  layoutMod :: Maybe String
  layoutMod :: Maybe String
layoutMod = Bool -> Maybe String -> Maybe String
forall m. Monoid m => Bool -> m -> m
when (CF -> Bool
hasLayout CF
cf) (Maybe String -> Maybe String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (SharedOptions -> String
layoutFileM SharedOptions
opts)

-- | Generate AST bindings for Agda.
--
cf2AgdaAST
  :: String  -- ^ Current time.
  -> TokenText
  -> String  -- ^ Module name.
  -> String  -- ^ Haskell Abs module name.
  -> String  -- ^ Haskell Print module name.
  -> CF      -- ^ Grammar.
  -> Doc
cf2AgdaAST :: String -> TokenText -> String -> String -> String -> CF -> Doc
cf2AgdaAST String
time TokenText
tokenText String
mod String
amod String
pmod CF
cf = [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
  [ String -> String -> Doc
preamble String
time String
"abstract syntax data types"
  , [Doc] -> Doc
hsep [ Doc
"module", String -> Doc
text String
mod, Doc
"where" ]
  , ImportNumeric -> Bool -> Bool -> Doc
imports ImportNumeric
YesImportNumeric Bool
False Bool
usesPos
  , Bool -> Doc -> Doc
forall m. Monoid m => Bool -> m -> m
when Bool
usesString (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep [ Doc
"String", Doc
equals, Doc
forall a. IsString a => a
listT, Doc
forall a. IsString a => a
charT ]
  , TokenText -> Bool -> [String] -> Doc
importPragmas TokenText
tokenText Bool
usesPos
      [ [String] -> String
unwords [ String
"qualified", String
amod ]
      , [String] -> String
unwords [ String
pmod, String
"(printTree)" ]
      ]
  , Bool -> Doc -> Doc
forall m. Monoid m => Bool -> m -> m
when Bool
usesPos Doc
defineIntAndPair
  , [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((String, Bool) -> Doc) -> [(String, Bool)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> Bool -> Doc) -> (String, Bool) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((String -> Bool -> Doc) -> (String, Bool) -> Doc)
-> (String -> Bool -> Doc) -> (String, Bool) -> Doc
forall a b. (a -> b) -> a -> b
$ String -> TokenText -> String -> Bool -> Doc
prToken String
amod TokenText
tokenText) [(String, Bool)]
tcats
  , String -> ConstructorStyle -> [Data] -> Doc
absyn String
amod ConstructorStyle
NamedArg [Data]
dats
  , CF -> Doc
definedRules CF
cf
  -- , allTokenCats printToken tcats  -- seem to be included in printerCats
  , String -> [Cat] -> Doc
printers String
amod [Cat]
printerCats
  , Doc
empty -- Make sure we terminate the file with a new line.
  ]
  where
  -- The grammar categories (excluding list, coerce, and token categories):
  dats :: [Data]
  dats :: [Data]
dats = CF -> [Data]
cf2data CF
cf
         -- getAbstractSyntax also includes list categories, which isn't what we need
  -- The user-defined token categories (including Ident).
  tcats :: [(TokenCat, Bool)]
  tcats :: [(String, Bool)]
tcats = (if CF -> Bool
forall f. CFG f -> Bool
hasIdent CF
cf then ((String
catIdent, Bool
False) (String, Bool) -> [(String, Bool)] -> [(String, Bool)]
forall a. a -> [a] -> [a]
:) else [(String, Bool)] -> [(String, Bool)]
forall a. a -> a
id)
    [ (WithPosition String -> String
forall a. WithPosition a -> a
wpThing WithPosition String
name, Bool
b) | TokenReg WithPosition String
name Bool
b Reg
_ <- CF -> [Pragma]
forall function. CFG function -> [Pragma]
cfgPragmas CF
cf ]
  -- Bind printers for the following categories (involves lists and literals).
  printerCats :: [Cat]
  printerCats :: [Cat]
printerCats = [[Cat]] -> [Cat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ (Data -> Cat) -> [Data] -> [Cat]
forall a b. (a -> b) -> [a] -> [b]
map Data -> Cat
forall a b. (a, b) -> a
fst (CF -> [Data]
getAbstractSyntax CF
cf)
    , (String -> Cat) -> [String] -> [Cat]
forall a b. (a -> b) -> [a] -> [b]
map String -> Cat
TokenCat ([String] -> [Cat]) -> [String] -> [Cat]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Eq a => [a] -> [a]
List.nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ CF -> [String]
forall function. CFG function -> [String]
cfgLiterals CF
cf [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, Bool) -> String) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Bool) -> String
forall a b. (a, b) -> a
fst [(String, Bool)]
tcats
    ]
  usesString :: Bool
usesString = String
"String" String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` CF -> [String]
forall function. CFG function -> [String]
cfgLiterals CF
cf
  usesPos :: Bool
usesPos    = CF -> Bool
forall f. CFG f -> Bool
hasPositionTokens CF
cf
  defineIntAndPair :: Doc
defineIntAndPair = [Doc] -> Doc
vsep
    [ [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ Doc
"postulate" ]
      , (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> (String -> Doc) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text) ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> [[String]] -> [String]
table String
" "
        [ [ String
forall a. IsString a => a
intT,      String
":", String
"Set" ]
        , [ String
forall a. IsString a => a
intToNatT, String
":", String
forall a. IsString a => a
intT, String
forall a. IsString a => a
arrow , String
forall a. IsString a => a
natT ]
        , [ String
forall a. IsString a => a
natToIntT, String
":", String
forall a. IsString a => a
natT, String
forall a. IsString a => a
arrow , String
forall a. IsString a => a
intT ]
        ]
      ]
    , [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ String
s -> [Doc] -> Doc
hsep [ Doc
"{-#", Doc
"COMPILE", Doc
"GHC", String -> Doc
text String
s, Doc
"#-}" ]) ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$
        String -> [[String]] -> [String]
table String
" = "
        [ [ String
forall a. IsString a => a
intT,      String
"type Prelude.Int"    ]
        , [ String
forall a. IsString a => a
intToNatT, String
"Prelude.toInteger"   ]
        , [ String
forall a. IsString a => a
natToIntT, String
"Prelude.fromInteger" ]
        ]
    , [Doc] -> Doc
vcat
      [ Doc
"data #Pair (A B : Set) : Set where"
      , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"#pair : A → B → #Pair A B"
      ]
    , Doc
"{-# COMPILE GHC #Pair = data (,) ((,)) #-}"
    ]

-- | Generate parser bindings for Agda.
--
cf2AgdaParser
  :: String  -- ^ Current time.
  -> TokenText
  -> String  -- ^ Module name.
  -> String  -- ^ Agda AST module name.
  -> String  -- ^ Haskell ErrM module name.
  -> String  -- ^ Haskell Par module name.
  -> Maybe String
             -- ^ Does the grammar use layout?  If yes, Haskell Layout module name.
  -> [Cat]   -- ^ Bind parsers for these non-terminals.
  -> Doc
cf2AgdaParser :: String
-> TokenText
-> String
-> String
-> String
-> String
-> Maybe String
-> [Cat]
-> Doc
cf2AgdaParser String
time TokenText
tokenText String
mod String
astmod String
emod String
pmod Maybe String
layoutMod [Cat]
cats = [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
  [ String -> String -> Doc
preamble String
time String
"parsers"
  , [Doc] -> Doc
hsep [ Doc
"module", String -> Doc
text String
mod, Doc
"where" ]
  , ImportNumeric -> Bool -> Bool -> Doc
imports ImportNumeric
NoImportNumeric (Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
layoutMod) Bool
False
  , String -> [String] -> Doc
importCats String
astmod ([String] -> [String]
forall a. Eq a => [a] -> [a]
List.nub [String]
cs)
  , TokenText -> Bool -> [String] -> Doc
importPragmas TokenText
tokenText Bool
False ([String] -> Doc) -> [String] -> Doc
forall a b. (a -> b) -> a -> b
$ [ String -> String
qual String
emod, String
pmod] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [String]
forall a. Maybe a -> [a]
maybeToList (String -> String
qual (String -> String) -> Maybe String -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
layoutMod)
  , Doc
"-- Error monad of BNFC"
  , String -> Doc
prErrM String
emod
  , Doc
"-- Happy parsers"
  , TokenText -> Maybe String -> [Cat] -> Doc
parsers TokenText
tokenText Maybe String
layoutMod [Cat]
cats
  , Doc
empty -- Make sure we terminate the file with a new line.
  ]
  where
  cs :: [String]
  cs :: [String]
cs = (Cat -> Maybe String) -> [Cat] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Cat -> Maybe String
baseCat [Cat]
cats
  baseCat :: Cat -> Maybe String
  baseCat :: Cat -> Maybe String
baseCat = \case
    Cat String
s         -> String -> Maybe String
forall a. a -> Maybe a
Just String
s
    CoercCat String
s Integer
_  -> String -> Maybe String
forall a. a -> Maybe a
Just String
s
    TokenCat String
"Char" -> Maybe String
forall a. Maybe a
Nothing
    TokenCat String
s    -> String -> Maybe String
forall a. a -> Maybe a
Just String
s
    ListCat Cat
c     -> Cat -> Maybe String
baseCat Cat
c
  qual :: String -> String
qual String
m = String
"qualified " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m

-- We prefix the Agda types with "#" to not conflict with user-provided nonterminals.
arrow, charT, integerT, listT, intT, natT, intToNatT, natToIntT, stringT, stringFromListT :: IsString a => a
arrow :: a
arrow = a
"→"
charT :: a
charT           = a
"Char"     -- This is the BNFC name for token type Char!
integerT :: a
integerT        = a
"Integer"  -- This is the BNFC name for token type Integer!
doubleT :: Doc
doubleT         = Doc
"Double"   -- This is the BNFC name for token type Double!
boolT :: Doc
boolT           = Doc
"#Bool"
listT :: a
listT           = a
"#List"
intT :: a
intT            = a
"#Int"     -- Int is the type used by the Haskell backend for line and column positions.
natT :: a
natT            = a
"#Nat"
intToNatT :: a
intToNatT       = a
"#intToNat"
natToIntT :: a
natToIntT       = a
"#natToInt"
stringT :: a
stringT         = a
"#String"
stringFromListT :: a
stringFromListT = a
"#stringFromList"

-- | Preamble: introductory comments.

preamble
  :: String  -- ^ Time stamp.
  -> String  -- ^ Brief characterization of file content.
  -> Doc
preamble :: String -> String -> Doc
preamble String
_time String
what = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
  [ [Doc] -> Doc
hcat [ Doc
"-- Agda bindings for the Haskell ", String -> Doc
text String
what, Doc
"." ]
  , [Doc] -> Doc
hcat [ Doc
"-- Generated by BNFC." ]
  -- -- Time stamp does not work well with BNFC's mkfile logic.
  -- , hcat [ "-- Generated by BNFC at "         , text time, "." ]
  ]

-- | Import statements.

imports
  :: ImportNumeric -- ^ Import also numeric types?
  -> Bool          -- ^ If have layout, import booleans.
  -> Bool          -- ^ If have position tokens, import natural numbers.
  -> Doc
imports :: ImportNumeric -> Bool -> Bool -> Doc
imports ImportNumeric
numeric Bool
layout Bool
pos = [Doc] -> Doc
vcat ([Doc] -> Doc)
-> ([[(String, [(String, Doc)])]] -> [Doc])
-> [[(String, [(String, Doc)])]]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, [(String, Doc)]) -> Doc)
-> [(String, [(String, Doc)])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, [(String, Doc)]) -> Doc
prettyImport ([(String, [(String, Doc)])] -> [Doc])
-> ([[(String, [(String, Doc)])]] -> [(String, [(String, Doc)])])
-> [[(String, [(String, Doc)])]]
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(String, [(String, Doc)])]] -> [(String, [(String, Doc)])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(String, [(String, Doc)])]] -> Doc)
-> [[(String, [(String, Doc)])]] -> Doc
forall a b. (a -> b) -> a -> b
$
  [ Bool -> [(String, [(String, Doc)])] -> [(String, [(String, Doc)])]
forall m. Monoid m => Bool -> m -> m
when Bool
layout
    [ (String
"Agda.Builtin.Bool",   [(String
"Bool", Doc
boolT)]) ]
  , [ (String
"Agda.Builtin.Char",   [(String
"Char", Doc
forall a. IsString a => a
charT)]) ]
  , Bool -> [(String, [(String, Doc)])] -> [(String, [(String, Doc)])]
forall m. Monoid m => Bool -> m -> m
when (ImportNumeric
numeric ImportNumeric -> ImportNumeric -> Bool
forall a. Eq a => a -> a -> Bool
== ImportNumeric
YesImportNumeric) [(String, [(String, Doc)])]
importNumeric
  , [ (String
"Agda.Builtin.List",   [(String
"List", Doc
forall a. IsString a => a
listT)]) ]
  , Bool -> [(String, [(String, Doc)])] -> [(String, [(String, Doc)])]
forall m. Monoid m => Bool -> m -> m
when Bool
pos
    [ (String
"Agda.Builtin.Nat",    [(String
"Nat" , Doc
forall a. IsString a => a
natT )]) ]
  , [ (String
"Agda.Builtin.String", [(String
"String", Doc
forall a. IsString a => a
stringT), (String
"primStringFromList", Doc
forall a. IsString a => a
stringFromListT) ]) ]
  ]
  where
  importNumeric :: [(String, [(String, Doc)])]
  importNumeric :: [(String, [(String, Doc)])]
importNumeric =
    [ (String
"Agda.Builtin.Float public", [(String
"Float", Doc
doubleT)])
    , (String
"Agda.Builtin.Int   public", [(String
"Int", Doc
forall a. IsString a => a
integerT)])
    ]
  prettyImport :: (String, [(String, Doc)]) -> Doc
  prettyImport :: (String, [(String, Doc)]) -> Doc
prettyImport (String
m, [(String, Doc)]
ren) = Int -> Doc -> Doc -> Doc -> Doc -> [Doc] -> Doc
prettyList Int
2 Doc
pre Doc
lparen Doc
rparen Doc
semi ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    ((String, Doc) -> Doc) -> [(String, Doc)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (String
x, Doc
d) -> [Doc] -> Doc
hsep [String -> Doc
text String
x, Doc
"to", Doc
d ]) [(String, Doc)]
ren
    where
    pre :: Doc
pre = [Doc] -> Doc
hsep [ Doc
"open", Doc
"import", String -> Doc
text String
m, Doc
"using", Doc
"()", Doc
"renaming" ]

-- | Import Agda AST.
--
importCats
  :: String    -- ^ Module for Agda AST.
  -> [String]  -- ^ Agda data types to import.
  -> Doc
importCats :: String -> [String] -> Doc
importCats String
m [String]
cs = Int -> Doc -> Doc -> Doc -> Doc -> [Doc] -> Doc
prettyList Int
2 Doc
pre Doc
lparen Doc
rparen Doc
semi ([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
text [String]
cs
  where
  pre :: Doc
pre = [Doc] -> Doc
hsep [ Doc
"open", Doc
"import", String -> Doc
text String
m, Doc
"using" ]

-- | Import pragmas.
--
-- >>> importPragmas ByteStringToken False ["qualified Foo.Abs", "Foo.Print (printTree)", "qualified Foo.Layout"]
-- {-# FOREIGN GHC import Prelude (Bool, Char, Double, Integer, String, (.)) #-}
-- {-# FOREIGN GHC import qualified Data.ByteString.Char8 as BS #-}
-- {-# FOREIGN GHC import qualified Data.Text #-}
-- {-# FOREIGN GHC import qualified Foo.Abs #-}
-- {-# FOREIGN GHC import Foo.Print (printTree) #-}
-- {-# FOREIGN GHC import qualified Foo.Layout #-}
--
importPragmas
  :: TokenText
  -> Bool      -- ^ Do we use position tokens?
  -> [String]  -- ^ Haskell modules to import.
  -> Doc
importPragmas :: TokenText -> Bool -> [String] -> Doc
importPragmas TokenText
tokenText Bool
pos [String]
mods = [Doc] -> Doc
vcat ([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
imp ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [String]
base [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
mods
  where
  imp :: String -> Doc
imp String
s = [Doc] -> Doc
hsep [ Doc
"{-#", Doc
"FOREIGN", Doc
"GHC", Doc
"import", String -> Doc
text String
s, Doc
"#-}" ]
  base :: [String]
base = [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [ String
"Prelude (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
preludeImports String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" ]
    , Bool -> [String] -> [String]
forall m. Monoid m => Bool -> m -> m
when Bool
pos
      [ String
"qualified Prelude" ]
    , case TokenText
tokenText of
        TokenText
TextToken       -> []
        TokenText
StringToken     -> []
        TokenText
ByteStringToken -> [ String
"qualified Data.ByteString.Char8 as BS" ]
    , [ String
"qualified Data.Text" ]
    ]
  preludeImports :: String
preludeImports = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [ String
"Bool", String
"Char", String
"Double", String
"Integer", String
"String", String
"(.)" ]
    , Bool -> [String] -> [String]
forall m. Monoid m => Bool -> m -> m
when Bool
pos
      [ String
"error" ] -- used unqualified by the GHC backend for postulates
    ]

-- * Bindings for the AST.

-- | Pretty-print types for token types similar to @Ident@.

prToken :: ModuleName -> TokenText -> String -> Bool -> Doc
prToken :: String -> TokenText -> String -> Bool -> Doc
prToken String
amod TokenText
tokenText String
t Bool
pos = [Doc] -> Doc
vsep
  [ if Bool
pos then [Doc] -> Doc
vcat
      -- can't use prettyData as it excepts a Cat for the type
      [ [Doc] -> Doc
hsep [ Doc
"data", String -> Doc
text String
t, Doc
":", Doc
"Set", Doc
"where" ]
      , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep
          [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
agdaLower String
t
          , Doc
":"
          , Doc
"#Pair (#Pair #Int #Int)"
          , Cat -> Doc
prettyCat Cat
typ
          , Doc
forall a. IsString a => a
arrow, String -> Doc
text String
t
          ]
      ]
    else ConstructorStyle -> String -> [(String, [Cat])] -> Doc
prettyData ConstructorStyle
UnnamedArg String
t [(String -> String
agdaLower String
t, [ Cat
typ ])]
  , String -> String -> [(String, [Cat])] -> Doc
pragmaData String
amod String
t [(String
t, [])]
  ]
  where
  typ :: Cat
typ = case TokenText
tokenText of
    TokenText
TextToken       -> String -> Cat
Cat String
"#String"
    TokenText
ByteStringToken -> String -> Cat
Cat String
"#String"
    TokenText
StringToken     -> Cat -> Cat
ListCat (String -> Cat
Cat String
"Char")

-- | Pretty-print abstract syntax definition in Agda syntax.
--
--   We print this as one big mutual block rather than doing a
--   strongly-connected component analysis and topological
--   sort by dependency order.
--
absyn :: ModuleName -> ConstructorStyle -> [Data] -> Doc
absyn :: String -> ConstructorStyle -> [Data] -> Doc
absyn String
_amod ConstructorStyle
_style [] = Doc
empty
absyn  String
amod  ConstructorStyle
style [Data]
ds = [Doc] -> Doc
vsep ([Doc] -> Doc) -> ([Data] -> [Doc]) -> [Data] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc
"mutual" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:) ([Doc] -> [Doc]) -> ([Data] -> [Doc]) -> [Data] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Data -> [Doc]) -> [Data] -> [Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2) ([Doc] -> [Doc]) -> (Data -> [Doc]) -> Data -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ConstructorStyle -> Data -> [Doc]
prData String
amod ConstructorStyle
style) ([Data] -> Doc) -> [Data] -> Doc
forall a b. (a -> b) -> a -> b
$ [Data]
ds

-- | Pretty-print Agda data types and pragmas for AST.
--
-- >>> vsep $ prData "Foo" UnnamedArg (Cat "Nat", [ ("Zero", []), ("Suc", [Cat "Nat"]) ])
-- data Nat : Set where
--   zero : Nat
--   suc  : Nat → Nat
-- <BLANKLINE>
-- {-# COMPILE GHC Nat = data Foo.Nat
--   ( Foo.Zero
--   | Foo.Suc
--   ) #-}
--
-- >>> vsep $ prData "Bar" UnnamedArg (Cat "C", [ ("C1", []), ("C2", [Cat "C"]) ])
-- data C : Set where
--   c1 : C
--   c2 : C → C
-- <BLANKLINE>
-- {-# COMPILE GHC C = data Bar.C
--   ( Bar.C1
--   | Bar.C2
--   ) #-}
--
-- We return a list of 'Doc' rather than a single 'Doc' since want
-- to intersperse empty lines and indent it later.
-- If we intersperse the empty line(s) here to get a single 'Doc',
-- we will produce whitespace lines after applying 'nest'.
-- This is a bit of a design problem of the pretty print library:
-- there is no native concept of a blank line; @text ""@ is a bad hack.
--
prData :: ModuleName -> ConstructorStyle -> Data -> [Doc]
prData :: String -> ConstructorStyle -> Data -> [Doc]
prData String
amod ConstructorStyle
style (Cat String
d, [(String, [Cat])]
cs) = String -> ConstructorStyle -> String -> [(String, [Cat])] -> [Doc]
prData' String
amod ConstructorStyle
style String
d [(String, [Cat])]
cs
prData String
_    ConstructorStyle
_     (Cat
c    , [(String, [Cat])]
_ ) = String -> [Doc]
forall a. HasCallStack => String -> a
error (String -> [Doc]) -> String -> [Doc]
forall a b. (a -> b) -> a -> b
$ String
"prData: unexpected category " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Cat -> String
forall a. Show a => a -> String
show Cat
c

-- | Pretty-print Agda data types and pragmas.
--
-- >>> vsep $ prData' "ErrM" UnnamedArg "Err A" [ ("Ok", [Cat "A"]), ("Bad", [ListCat $ Cat "Char"]) ]
-- data Err A : Set where
--   ok  : A → Err A
--   bad : #List Char → Err A
-- <BLANKLINE>
-- {-# COMPILE GHC Err = data ErrM.Err
--   ( ErrM.Ok
--   | ErrM.Bad
--   ) #-}
--
prData' :: ModuleName -> ConstructorStyle -> String -> [(Fun, [Cat])] -> [Doc]
prData' :: String -> ConstructorStyle -> String -> [(String, [Cat])] -> [Doc]
prData' String
amod ConstructorStyle
style String
d [(String, [Cat])]
cs = [ ConstructorStyle -> String -> [(String, [Cat])] -> Doc
prettyData ConstructorStyle
style String
d [(String, [Cat])]
cs , String -> String -> [(String, [Cat])] -> Doc
pragmaData String
amod ([String] -> String
forall a. [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
d) [(String, [Cat])]
cs ]

-- | Pretty-print Agda binding for the BNFC Err monad.
--
-- Note: we use "Err" here since a category "Err" would also conflict
-- with BNFC's error monad in the Haskell backend.
prErrM :: ModuleName -> Doc
prErrM :: String -> Doc
prErrM String
emod = [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> ConstructorStyle -> String -> [(String, [Cat])] -> [Doc]
prData' String
emod ConstructorStyle
UnnamedArg String
"Err A"
  [ (String
"Ok" , [String -> Cat
Cat String
"A"])
  , (String
"Bad", [Cat -> Cat
ListCat (Cat -> Cat) -> Cat -> Cat
forall a b. (a -> b) -> a -> b
$ String -> Cat
Cat String
"Char"])
  ]

-- | Pretty-print AST definition in Agda syntax.
--
-- >>> prettyData UnnamedArg "Nat" [ ("zero", []), ("suc", [Cat "Nat"]) ]
-- data Nat : Set where
--   zero : Nat
--   suc  : Nat → Nat
--
-- >>> prettyData UnnamedArg "C" [ ("C1", []), ("C2", [Cat "C"]) ]
-- data C : Set where
--   c1 : C
--   c2 : C → C
--
-- >>> :{
--   prettyData UnnamedArg "Stm"
--     [ ("block", [ListCat $ Cat "Stm"])
--     , ("while", [Cat "Exp", Cat "Stm"])
--     ]
-- :}
-- data Stm : Set where
--   block : #List Stm → Stm
--   while : Exp → Stm → Stm
--
-- >>> :{
--   prettyData NamedArg "Stm"
--     [ ("block", [ListCat $ Cat "Stm"])
--     , ("if", [Cat "Exp", Cat "Stm", Cat "Stm"])
--     ]
-- :}
-- data Stm : Set where
--   block : (ss : #List Stm) → Stm
--   if    : (e : Exp) (s₁ s₂ : Stm) → Stm
--
prettyData :: ConstructorStyle -> String -> [(Fun, [Cat])] -> Doc
prettyData :: ConstructorStyle -> String -> [(String, [Cat])] -> Doc
prettyData ConstructorStyle
style String
d [(String, [Cat])]
cs = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [ [Doc] -> Doc
hsep [ Doc
"data", String -> Doc
text String
d, Doc
colon, Doc
"Set", Doc
"where" ] ]
  , [(Doc, Doc)] -> [Doc]
mkTSTable ([(Doc, Doc)] -> [Doc]) -> [(Doc, Doc)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((String, [Cat]) -> (Doc, Doc))
-> [(String, [Cat])] -> [(Doc, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (ConstructorStyle -> String -> (String, [Cat]) -> (Doc, Doc)
prettyConstructor ConstructorStyle
style String
d) [(String, [Cat])]
cs
  ]
  where

mkTSTable :: [(Doc,Doc)] -> [Doc]
mkTSTable :: [(Doc, Doc)] -> [Doc]
mkTSTable = (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> (String -> Doc) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text) ([String] -> [Doc])
-> ([(Doc, Doc)] -> [String]) -> [(Doc, Doc)] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [[String]] -> [String]
table String
" : " ([[String]] -> [String])
-> ([(Doc, Doc)] -> [[String]]) -> [(Doc, Doc)] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Doc, Doc) -> [String]) -> [(Doc, Doc)] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (Doc, Doc) -> [String]
mkRow
  where
  mkRow :: (Doc, Doc) -> [String]
mkRow (Doc
c,Doc
t) = [ Doc -> String
render Doc
c, Doc -> String
render Doc
t ]

-- | Generate pragmas to bind Haskell AST to Agda.
--
-- >>> pragmaData "Foo" "Empty" []
-- {-# COMPILE GHC Empty = data Foo.Empty () #-}
--
-- >>> pragmaData "Foo" "Nat" [ ("zero", []), ("suc", [Cat "Nat"]) ]
-- {-# COMPILE GHC Nat = data Foo.Nat
--   ( Foo.zero
--   | Foo.suc
--   ) #-}
--
pragmaData :: ModuleName -> String -> [(Fun, [Cat])] -> Doc
pragmaData :: String -> String -> [(String, [Cat])] -> Doc
pragmaData String
amod String
d [(String, [Cat])]
cs = Int -> Doc -> Doc -> Doc -> Doc -> [Doc] -> Doc
prettyList Int
2 Doc
pre Doc
lparen (Doc
rparen Doc -> Doc -> Doc
<+> Doc
"#-}") Doc
"|" ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
  ((String, [Cat]) -> Doc) -> [(String, [Cat])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> Doc
prettyFun String
amod (String -> Doc)
-> ((String, [Cat]) -> String) -> (String, [Cat]) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, [Cat]) -> String
forall a b. (a, b) -> a
fst) [(String, [Cat])]
cs
  where
  pre :: Doc
pre = [Doc] -> Doc
hsep [ Doc
"{-#", Doc
"COMPILE", Doc
"GHC", String -> Doc
text String
d, Doc
equals, Doc
"data", String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
amod, String
".", String
d ] ]

-- | Pretty-print since rule as Agda constructor declaration.
--
-- >>> prettyConstructor UnnamedArg "D" ("c", [Cat "A", Cat "B", Cat "C"])
-- (c,A → B → C → D)
-- >>> prettyConstructor undefined  "D" ("c1", [])
-- (c1,D)
-- >>> prettyConstructor NamedArg "Stm" ("SIf", map Cat ["Exp", "Stm", "Stm"])
-- (sIf,(e : Exp) (s₁ s₂ : Stm) → Stm)
--
prettyConstructor :: ConstructorStyle -> String -> (Fun,[Cat]) -> (Doc,Doc)
prettyConstructor :: ConstructorStyle -> String -> (String, [Cat]) -> (Doc, Doc)
prettyConstructor ConstructorStyle
style String
d (String
c, [Cat]
as) = (String -> Doc
prettyCon String
c,) (Doc -> (Doc, Doc)) -> Doc -> (Doc, Doc)
forall a b. (a -> b) -> a -> b
$ if [Cat] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Cat]
as then String -> Doc
text String
d else [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
  [ ConstructorStyle -> [Cat] -> Doc
prettyConstructorArgs ConstructorStyle
style [Cat]
as
  , Doc
forall a. IsString a => a
arrow
  , String -> Doc
text String
d
  ]

-- | Print the constructor argument telescope.
--
-- >>> prettyConstructorArgs UnnamedArg [Cat "A", Cat "B", Cat "C"]
-- A → B → C
--
-- >>> prettyConstructorArgs NamedArg (map Cat ["Exp", "Stm", "Stm"])
-- (e : Exp) (s₁ s₂ : Stm)
--
prettyConstructorArgs :: ConstructorStyle -> [Cat] -> Doc
prettyConstructorArgs :: ConstructorStyle -> [Cat] -> Doc
prettyConstructorArgs ConstructorStyle
style [Cat]
as =
  case ConstructorStyle
style of
    ConstructorStyle
UnnamedArg -> [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
List.intersperse Doc
forall a. IsString a => a
arrow [Doc]
ts
    ConstructorStyle
NamedArg   -> [Doc] -> Doc
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
parens ([Doc] -> Doc
hsep [Doc
x, [Doc] -> Doc
hsep [Doc]
xs, Doc
colon, Doc
t])) [(NonEmpty Doc, Doc)]
tel
  where
  ts :: [Doc]
ts  = (Cat -> Doc) -> [Cat] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Cat -> Doc
prettyCat [Cat]
as
  ns :: [Doc]
ns  = ((Maybe Int, String) -> Doc) -> [(Maybe Int, String)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc)
-> ((Maybe Int, String) -> String) -> (Maybe Int, String) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Int, String) -> String
forall a. Show a => (Maybe a, String) -> String
subscript) ([(Maybe Int, String)] -> [Doc]) -> [(Maybe Int, String)] -> [Doc]
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
$ (Cat -> String) -> [Cat] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Cat -> String
nameSuggestion [Cat]
as
  tel :: [(NonEmpty Doc, Doc)]
tel = ((Doc, Doc) -> String) -> [(Doc, Doc)] -> [(NonEmpty Doc, Doc)]
forall c a b. Eq c => ((a, b) -> c) -> [(a, b)] -> [(List1 a, b)]
aggregateOn (Doc -> String
render (Doc -> String) -> ((Doc, Doc) -> Doc) -> (Doc, Doc) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc, Doc) -> Doc
forall a b. (a, b) -> b
snd) ([(Doc, Doc)] -> [(NonEmpty Doc, Doc)])
-> [(Doc, Doc)] -> [(NonEmpty Doc, Doc)]
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc] -> [(Doc, Doc)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Doc]
ns [Doc]
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)
    -- . List1.groupWith f -- Too recent, fails stack-7.8 install

-- | Suggest the name of a bound variable of the given category.
--
-- >>> map nameSuggestion [ ListCat (Cat "Stm"), TokenCat "Var", Cat "Exp" ]
-- ["ss","x","e"]
--
nameSuggestion :: Cat -> String
nameSuggestion :: Cat -> String
nameSuggestion = \case
  ListCat Cat
c     -> Cat -> String
nameSuggestion Cat
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s"
  CoercCat String
d Integer
_  -> String -> String
nameFor String
d
  Cat String
d         -> String -> String
nameFor String
d
  TokenCat{}    -> String
"x"

-- | Suggest the name of a bound variable of the given base category.
--
-- >>> map nameFor ["Stm","ABC","#String"]
-- ["s","a","s"]
--
nameFor :: String -> String
nameFor :: String -> String
nameFor String
d = [ Char -> Char
toLower (Char -> Char) -> Char -> Char
forall a b. (a -> b) -> a -> b
$ String -> Char
forall a. [a] -> a
head (String -> Char) -> String -> Char
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'#') String
d ]

-- | Number duplicate elements in a list consecutively, starting with 1.
--
-- >>> numberUniquely ["a", "b", "a", "a", "c", "b"]
-- [(Just 1,"a"),(Just 1,"b"),(Just 2,"a"),(Just 3,"a"),(Nothing,"c"),(Just 2,"b")]
--
numberUniquely :: forall a. Ord a => [a] -> [(Maybe Int, a)]
numberUniquely :: [a] -> [(Maybe Int, a)]
numberUniquely [a]
as = (a -> StateT (Frequency a) Identity (Maybe Int, a))
-> [a] -> StateT (Frequency a) Identity [(Maybe Int, a)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> StateT (Frequency a) Identity (Maybe Int, a)
step [a]
as StateT (Frequency a) Identity [(Maybe Int, a)]
-> Frequency a -> [(Maybe Int, a)]
forall s a. State s a -> s -> a
`evalState` Frequency a
forall k a. Map k a
Map.empty
  where
  -- First pass: determine frequency of each element.
  counts :: Frequency a
  counts :: Frequency a
counts = (Frequency a -> a -> Frequency a)
-> Frequency a -> [a] -> Frequency a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((a -> Frequency a -> Frequency a)
-> Frequency a -> a -> Frequency a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Frequency a -> Frequency a
forall a. Ord a => a -> Frequency a -> Frequency a
incr) Frequency a
forall k a. Map k a
Map.empty [a]
as
  -- Second pass: consecutively number elements with frequency > 1.
  step :: a -> State (Frequency a) (Maybe Int, a)
  step :: a -> StateT (Frequency a) Identity (Maybe Int, a)
step a
a = do
    -- If the element has a unique occurrence, we do not need to number it.
    let n :: Int
n = Int -> a -> Frequency a -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Int
forall a. HasCallStack => String -> a
error String
"numberUniquelyWith") a
a Frequency a
counts
    if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then (Maybe Int, a) -> StateT (Frequency a) Identity (Maybe Int, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int
forall a. Maybe a
Nothing, a
a) else do
      -- Otherwise, increase the counter for that element and number it
      -- with the new value.
      (Frequency a -> Frequency a) -> StateT (Frequency a) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Frequency a -> Frequency a) -> StateT (Frequency a) Identity ())
-> (Frequency a -> Frequency a) -> StateT (Frequency a) Identity ()
forall a b. (a -> b) -> a -> b
$ a -> Frequency a -> Frequency a
forall a. Ord a => a -> Frequency a -> Frequency a
incr a
a
      (,a
a) (Maybe Int -> (Maybe Int, a))
-> (Frequency a -> Maybe Int) -> Frequency a -> (Maybe Int, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Frequency a -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a (Frequency a -> (Maybe Int, a))
-> StateT (Frequency a) Identity (Frequency a)
-> StateT (Frequency a) Identity (Maybe Int, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (Frequency a) Identity (Frequency a)
forall s (m :: * -> *). MonadState s m => m s
get

-- | A frequency map.
--
--   NB: this type synonym should be local to 'numberUniquely', but
--   Haskell lacks local type synonyms.
--   https://gitlab.haskell.org/ghc/ghc/issues/4020
type Frequency a = Map a Int

-- | Increase the frequency of the given key.
incr :: Ord a => a -> Frequency a -> Frequency a
incr :: a -> Frequency a -> Frequency a
incr = (Maybe Int -> Maybe Int) -> a -> Frequency a -> Frequency a
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter ((Maybe Int -> Maybe Int) -> a -> Frequency a -> Frequency a)
-> (Maybe Int -> Maybe Int) -> a -> Frequency a -> Frequency a
forall a b. (a -> b) -> a -> b
$ Maybe Int -> (Int -> Maybe Int) -> Maybe Int -> Maybe Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1) (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Int -> Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Enum a => a -> a
succ)

-- * Generate the defined constructors.

-- | Generate Haskell code for the @define@d constructors.
definedRules :: CF -> Doc
definedRules :: CF -> Doc
definedRules CF
cf = [Doc] -> Doc
vsep [ WithPosition String -> [String] -> Exp -> Doc
forall f. IsFun f => f -> [String] -> Exp -> Doc
mkDef WithPosition String
f [String]
xs Exp
e | FunDef WithPosition String
f [String]
xs Exp
e <- CF -> [Pragma]
forall function. CFG function -> [Pragma]
cfgPragmas CF
cf ]
  where
    mkDef :: f -> [String] -> Exp -> Doc
mkDef f
f [String]
xs Exp
e = [Doc] -> Doc
vcat ([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
text ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ [String] -> String
unwords [ f -> String
forall f. IsFun f => f -> String
mkDefName f
f, String
":", String -> Type -> String
typeToHaskell' String
"→" (Type -> String) -> Type -> String
forall a b. (a -> b) -> a -> b
$ WithPosition Type -> Type
forall a. WithPosition a -> a
wpThing WithPosition Type
t ]
        | WithPosition Type
t <- Maybe (WithPosition Type) -> [WithPosition Type]
forall a. Maybe a -> [a]
maybeToList (Maybe (WithPosition Type) -> [WithPosition Type])
-> Maybe (WithPosition Type) -> [WithPosition Type]
forall a b. (a -> b) -> a -> b
$ f -> CF -> Maybe (WithPosition Type)
forall a. IsFun a => a -> CF -> Maybe (WithPosition Type)
sigLookup f
f CF
cf
        ]
      , [ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [ f -> String
forall f. IsFun f => f -> String
mkDefName f
f, String
"=", String
"λ" ]
          , (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
agdaLower [String]
xs
          , [ String
"→", Exp -> String
forall a. Show a => a -> String
show (Exp -> String) -> Exp -> String
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
sanitize Exp
e ]
          ]
        ]
      ]
    sanitize :: Exp -> Exp
sanitize = \case
      App String
x [Exp]
es      -> String -> [Exp] -> Exp
App (String -> String
agdaLower String
x) ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Exp
sanitize [Exp]
es
      Var String
x         -> String -> Exp
Var (String -> Exp) -> String -> Exp
forall a b. (a -> b) -> a -> b
$ String -> String
agdaLower String
x
      e :: Exp
e@LitInt{}    -> Exp
e
      e :: Exp
e@LitDouble{} -> Exp
e
      e :: Exp
e@LitChar{}   -> Exp
e
      e :: Exp
e@LitString{} -> Exp
e

-- * Generate bindings for the pretty printers

-- | Generate Agda code to print tokens.
--
-- >>> printToken "Ident"
-- printIdent : Ident → #String
-- printIdent (ident s) = #stringFromList s
--
printToken :: String -> Doc
printToken :: String -> Doc
printToken String
t = [Doc] -> Doc
vcat
  [ [Doc] -> Doc
hsep [ Doc
f, Doc
colon, String -> Doc
text String
t, Doc
forall a. IsString a => a
arrow, Doc
forall a. IsString a => a
stringT ]
  , [Doc] -> Doc
hsep [ Doc
f, Doc
lparen Doc -> Doc -> Doc
<> Doc
c Doc -> Doc -> Doc
<+> Doc
"s" Doc -> Doc -> Doc
<> Doc
rparen, Doc
equals, Doc
forall a. IsString a => a
stringFromListT, Doc
"s" ]
  ]
  where
  f :: Doc
f = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"print" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
  c :: Doc
c = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
agdaLower String
t

-- | Generate Agda bindings to printers for AST.
--
-- >>> printers "Foo" $ map Cat [ "Exp", "Stm" ]
-- -- Binding the pretty printers.
-- <BLANKLINE>
-- postulate
--   printExp : Exp → #String
--   printStm : Stm → #String
-- <BLANKLINE>
-- {-# COMPILE GHC printExp = \ e -> Data.Text.pack (printTree (e :: Foo.Exp)) #-}
-- {-# COMPILE GHC printStm = \ s -> Data.Text.pack (printTree (s :: Foo.Stm)) #-}
--
printers :: ModuleName -> [Cat] -> Doc
printers :: String -> [Cat] -> Doc
printers String
_amod []   = Doc
empty
printers  String
amod [Cat]
cats = [Doc] -> Doc
vsep
  [ Doc
"-- Binding the pretty printers."
  , [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"postulate" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [(Doc, Doc)] -> [Doc]
mkTSTable ((Cat -> (Doc, Doc)) -> [Cat] -> [(Doc, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (Cat -> (Doc, Doc)
prettyTySig) [Cat]
cats)
  , [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Cat -> Doc) -> [Cat] -> [Doc]
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, Doc
forall a. IsString a => a
arrow, Doc
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 = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Cat -> String
nameSuggestion Cat
c
    t :: Doc
t = (Doc -> Doc) -> Doc -> Cat -> Doc
catToType ((String -> Doc
text String
amod Doc -> Doc -> Doc
<> String -> Doc
text String
".") Doc -> Doc -> Doc
<>) Doc
empty Cat
c  -- Removes CoercCat.

-- | Bind happy parsers.
--
-- >>> parsers StringToken Nothing [ListCat (CoercCat "Exp" 2)]
-- postulate
--   parseListExp2 : #String → Err (#List Exp)
-- <BLANKLINE>
-- {-# COMPILE GHC parseListExp2 = pListExp2 . myLexer . Data.Text.unpack #-}
--
-- >>> parsers TextToken Nothing [ListCat (CoercCat "Exp" 2)]
-- postulate
--   parseListExp2 : #String → Err (#List Exp)
-- <BLANKLINE>
-- {-# COMPILE GHC parseListExp2 = pListExp2 . myLexer #-}
--
parsers
  :: TokenText
  -> Maybe String  -- ^ Grammar uses layout?  If yes, Haskell layout module name.
  -> [Cat]         -- ^ Bind parsers for these non-terminals.
  -> Doc
parsers :: TokenText -> Maybe String -> [Cat] -> Doc
parsers TokenText
tokenText Maybe String
layoutMod [Cat]
cats =
  [Doc] -> Doc
vcat (Doc
"postulate" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Cat -> Doc) -> [Cat] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> (Cat -> Doc) -> Cat -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cat -> Doc
prettyTySig) [Cat]
cats)
  Doc -> Doc -> Doc
$++$
  [Doc] -> Doc
vcat ((Cat -> Doc) -> [Cat] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Cat -> Doc
pragmaBind [Cat]
cats)
  where
  -- When grammar uses layout, we parametrize the parser by a boolean @tl@
  -- that indicates whether top layout should be used for this parser.
  -- Also, we add @resolveLayout tl@ to the pipeline after lexing.
  prettyTySig :: Cat -> Doc
  prettyTySig :: Cat -> Doc
prettyTySig Cat
c = [Doc] -> Doc
hsep ([Doc] -> Doc) -> ([[Doc]] -> [Doc]) -> [[Doc]] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Doc]] -> Doc) -> [[Doc]] -> Doc
forall a b. (a -> b) -> a -> b
$
   [ [ Cat -> Doc
agdaParserName Cat
c, Doc
colon ]
   , Bool -> [Doc] -> [Doc]
forall m. Monoid m => Bool -> m -> m
when Bool
layout [ Doc
boolT, Doc
forall a. IsString a => a
arrow ]
   , [ Doc
forall a. IsString a => a
stringT, Doc
forall a. IsString a => a
arrow, Doc
"Err", Cat -> Doc
prettyCatParens Cat
c ]
   ]
  pragmaBind :: Cat -> Doc
  pragmaBind :: Cat -> Doc
pragmaBind Cat
c = [Doc] -> Doc
hsep ([Doc] -> Doc) -> ([[Doc]] -> [Doc]) -> [[Doc]] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Doc]] -> Doc) -> [[Doc]] -> Doc
forall a b. (a -> b) -> a -> b
$
    [ [ Doc
"{-#", Doc
"COMPILE", Doc
"GHC", Cat -> Doc
agdaParserName Cat
c, Doc
equals ]
    , Bool -> [Doc] -> [Doc]
forall m. Monoid m => Bool -> m -> m
when Bool
layout [ Doc
"\\", Doc
"tl", Doc
"->" ]
    , [ Cat -> Doc
parserName Cat
c, Doc
"." ]
    , Bool -> [Doc] -> [Doc]
forall m. Monoid m => Bool -> m -> m
when Bool
layout [ [Doc] -> Doc
hcat [ String -> Doc
text String
lmod, Doc
".", Doc
"resolveLayout" ], Doc
"tl", Doc
"." ]
    , [ Doc
"myLexer" ]
    , case TokenText
tokenText of
        -- Agda's String is Haskell's Data.Text
        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 = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
layoutMod
  lmod :: String
  lmod :: String
lmod = Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
layoutMod

-- * Auxiliary functions

-- | Concatenate documents created from token categories,
--   separated by blank lines.
--
-- >>> allTokenCats text ["T", "U"]
-- T
-- <BLANKLINE>
-- U
allTokenCats :: (TokenCat -> Doc) -> [TokenCat] -> Doc
allTokenCats :: (String -> Doc) -> [String] -> Doc
allTokenCats String -> Doc
f = [Doc] -> Doc
vsep ([Doc] -> Doc) -> ([String] -> [Doc]) -> [String] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
f

-- | Pretty-print a rule name for Haskell.
prettyFun :: ModuleName -> Fun -> Doc
prettyFun :: String -> String -> Doc
prettyFun String
amod String
c = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
amod, String
".", String
c ]

-- | Pretty-print a rule name for Agda.
prettyCon :: Fun -> Doc
prettyCon :: String -> Doc
prettyCon = String -> Doc
text (String -> Doc) -> (String -> String) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
agdaLower

-- | Turn identifier to non-capital identifier.
--   Needed, since in Agda a constructor cannot overload a data type
--   with the same name.
--
-- >>> map agdaLower ["SFun","foo","ABC","HelloWorld","module","Type_int","C1"]
-- ["sFun","foo","aBC","helloWorld","module'","type-int","c1"]
--
agdaLower :: String -> String
agdaLower :: String -> String
agdaLower = String -> String
avoidKeywords (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a. (a -> a) -> [a] -> [a]
updateHead Char -> Char
toLower (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Char -> String -> String
forall a. Eq a => a -> a -> [a] -> [a]
replace Char
'_' Char
'-'
  -- WAS: replace '_' '\'' . BNFC.Utils.mkName agdaKeywords BNFC.Utils.MixedCase
  where
  updateHead :: (a -> a) -> [a] -> [a]
updateHead a -> a
_f []    = []
  updateHead a -> a
f (a
x:[a]
xs) = a -> a
f a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs
  avoidKeywords :: String -> String
avoidKeywords String
s
    | String
s String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
agdaKeywords = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\'"
    | Bool
otherwise = String
s

-- | A list of Agda keywords that would clash with generated names.
agdaKeywords :: Set String
agdaKeywords :: Set String
agdaKeywords = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
"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"

-- | Name of Agda parser binding (mentions precedence).
--
-- >>> agdaParserName $ ListCat $ CoercCat "Exp" 2
-- parseListExp2
--
agdaParserName :: Cat -> Doc
agdaParserName :: Cat -> Doc
agdaParserName Cat
c = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"parse" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Cat -> String
identCat Cat
c

-- | Name of Agda printer binding (does not mention precedence).
--
-- >>> agdaPrinterName $ ListCat $ CoercCat "Exp" 2
-- printListExp
--
agdaPrinterName :: Cat -> Doc
agdaPrinterName :: Cat -> Doc
agdaPrinterName Cat
c = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"print" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Cat -> String
identCat (Cat -> Cat
normCat Cat
c)

-- | Pretty-print a category as Agda type.
--   Ignores precedence.
--
-- >>> prettyCat $ ListCat (CoercCat "Exp" 2)
-- #List Exp
--
prettyCat :: Cat -> Doc
prettyCat :: Cat -> Doc
prettyCat = \case
  Cat String
s        -> String -> Doc
text String
s
  TokenCat String
s   -> String -> Doc
text String
s
  CoercCat String
s Integer
_ -> String -> Doc
text String
s
  ListCat Cat
c    -> Doc
forall a. IsString a => a
listT Doc -> Doc -> Doc
<+> Cat -> Doc
prettyCatParens Cat
c

-- | Pretty-print category in parentheses, if 'compositeCat'.
prettyCatParens :: Cat -> Doc
prettyCatParens :: Cat -> Doc
prettyCatParens Cat
c = Bool -> Doc -> Doc
parensIf (Cat -> Bool
compositeCat Cat
c) (Cat -> Doc
prettyCat Cat
c)

-- | Is the Agda type corresponding to 'Cat' composite (or atomic)?
compositeCat :: Cat -> Bool
compositeCat :: Cat -> Bool
compositeCat = \case
  ListCat{} -> Bool
True
  Cat
_         -> Bool
False


-- * Agda stub to test parser

-- | Write a simple IO library with fixed contents.

agdaLibContents
  :: String      -- ^ Name of Agda library module.
  -> Doc         -- ^ Contents of Agda library module.
agdaLibContents :: String -> Doc
agdaLibContents String
mod = [Doc] -> Doc
vcat
  [ Doc
"-- Generated by BNFC."
  , Doc
"-- Basic I/O library."
  , Doc
""
  , Doc
"module" Doc -> Doc -> Doc
<+> String -> Doc
text String
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      -- ^ Name of Agda main module.
  -> String      -- ^ Name of Agda library module.
  -> String      -- ^ Name of Agda AST module.
  -> String      -- ^ Name of Agda parser module.
  -> Bool        -- ^ Is the grammar using layout?
  -> Cat         -- ^ Category to parse.
  -> Doc         -- ^ Contents of Agda main module.
agdaMainContents :: String -> String -> String -> String -> Bool -> Cat -> Doc
agdaMainContents String
mod String
lmod String
amod String
pmod Bool
layout Cat
c = [Doc] -> Doc
vcat
  [ Doc
"-- Test for Agda binding of parser.  Requires Agda >= 2.5.4."
  , Doc
"-- Generated by BNFC."
  , Doc
""
  , Doc
"module" Doc -> Doc -> Doc
<+> String -> Doc
text String
mod Doc -> Doc -> Doc
<+> Doc
"where"
  , Bool -> Doc -> Doc
forall m. Monoid m => Bool -> m -> m
when Bool
layout Doc
"\nopen import Agda.Builtin.Bool using (true)"
  , Doc
"open import" Doc -> Doc -> Doc
<+> String -> Doc
text String
lmod
  , Doc
"open import" Doc -> Doc -> Doc
<+> String -> Doc
text String
amod Doc -> Doc -> Doc
<+> Doc
"using" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Doc
printer)
  , Doc
"open import" Doc -> Doc -> Doc
<+> String -> Doc
text String
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 ([Doc] -> Doc) -> ([[Doc]] -> [Doc]) -> [[Doc]] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Doc]] -> Doc) -> [[Doc]] -> Doc
forall a b. (a -> b) -> a -> b
$ [ [Doc
parser], Bool -> [Doc] -> [Doc]
forall m. Monoid m => Bool -> m -> m
when Bool
layout [Doc
"true"] ]
    -- Permit use of top-level layout, if any.