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

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

-- | 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)) #-}

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)

-- | 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 :: [Char] -> SharedOptions -> CF -> Backend
makeAgda [Char]
time SharedOptions
opts CF
cf = do
  -- Generate AST bindings.
  [Char] -> MakeComment -> Doc -> Backend
forall c. FileContent c => [Char] -> MakeComment -> c -> Backend
mkfile (SharedOptions -> [Char]
agdaASTFile SharedOptions
opts) MakeComment
comment (Doc -> Backend) -> Doc -> Backend
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
  -- Generate parser bindings.
  [Char] -> MakeComment -> Doc -> Backend
forall c. FileContent c => [Char] -> MakeComment -> c -> Backend
mkfile (SharedOptions -> [Char]
agdaParserFile SharedOptions
opts) MakeComment
comment (Doc -> Backend) -> Doc -> Backend
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
  -- Generate an I/O library for the test parser.
  [Char] -> MakeComment -> Doc -> Backend
forall c. FileContent c => [Char] -> MakeComment -> c -> Backend
mkfile (SharedOptions -> [Char]
agdaLibFile SharedOptions
opts) MakeComment
comment (Doc -> Backend) -> Doc -> Backend
forall a b. (a -> b) -> a -> b
$
    [Char] -> Doc
agdaLibContents (SharedOptions -> [Char]
agdaLibFileM SharedOptions
opts)
  -- Generate test parser.
  [Char] -> MakeComment -> Doc -> Backend
forall c. FileContent c => [Char] -> MakeComment -> c -> Backend
mkfile (SharedOptions -> [Char]
agdaMainFile SharedOptions
opts) MakeComment
comment (Doc -> Backend) -> Doc -> Backend
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
  -- | 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 [Char]
layoutMod = Bool -> Maybe [Char] -> Maybe [Char]
forall m. Monoid m => Bool -> m -> m
when (CF -> Bool
hasLayout CF
cf) (Maybe [Char] -> Maybe [Char]) -> Maybe [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just (SharedOptions -> [Char]
layoutFileM SharedOptions
opts)

-- | Generate AST bindings for Agda.
--
cf2AgdaAST
  :: String  -- ^ Current time.
  -> Bool    -- ^ Include positions information in the AST? (`--functor`)
  -> TokenText
  -> String  -- ^ Module name.
  -> String  -- ^ Haskell Abs module name.
  -> String  -- ^ Haskell Print module name.
  -> CF      -- ^ Grammar.
  -> 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 ([Doc] -> Doc) -> [Doc] -> Doc
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
  , 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 -> [[Char]] -> Doc
importPragmas TokenText
tokenText Bool
usesPos
      [ [[Char]] -> [Char]
unwords [ [Char]
"qualified", [Char]
amod ]
      , [[Char]] -> [Char]
unwords [ [Char]
pmod, [Char]
"(printTree)" ]
      ]
  , Bool -> Doc -> Doc
forall m. Monoid m => Bool -> m -> m
when Bool
usesPos Doc
defineIntAndPair
  , Bool -> Doc -> Doc
forall m. Monoid m => Bool -> m -> m
when Bool
havePos Doc
defineBNFCPosition
  , [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (([Char], Bool) -> Doc) -> [([Char], Bool)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (([Char] -> Bool -> Doc) -> ([Char], Bool) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (([Char] -> Bool -> Doc) -> ([Char], Bool) -> Doc)
-> ([Char] -> Bool -> Doc) -> ([Char], Bool) -> Doc
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
  -- , allTokenCats printToken tcats  -- seem to be included in printerCats
  , [Char] -> [Cat] -> Doc
printers [Char]
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 :: [([Char], Bool)]
tcats = (if CF -> Bool
forall f. CFG f -> Bool
hasIdent CF
cf then (([Char]
catIdent, Bool
False) ([Char], Bool) -> [([Char], Bool)] -> [([Char], Bool)]
forall a. a -> [a] -> [a]
:) else [([Char], Bool)] -> [([Char], Bool)]
forall a. a -> a
id)
    [ (WithPosition [Char] -> [Char]
forall a. WithPosition a -> a
wpThing WithPosition [Char]
name, Bool
b) | TokenReg WithPosition [Char]
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)
    , ([Char] -> Cat) -> [[Char]] -> [Cat]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Cat
TokenCat ([[Char]] -> [Cat]) -> [[Char]] -> [Cat]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [[Char]]
forall a. Eq a => [a] -> [a]
List.nub ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ CF -> [[Char]]
forall function. CFG function -> [[Char]]
cfgLiterals CF
cf [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ (([Char], Bool) -> [Char]) -> [([Char], Bool)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], Bool) -> [Char]
forall a b. (a, b) -> a
fst [([Char], Bool)]
tcats
    ]
  usesString :: Bool
usesString = [Char]
"String" [Char] -> [[Char]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` CF -> [[Char]]
forall function. CFG function -> [[Char]]
cfgLiterals CF
cf
  usesPos :: Bool
usesPos    = Bool
havePos Bool -> Bool -> Bool
|| 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" ]
      , ([Char] -> Doc) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> ([Char] -> Doc) -> [Char] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc
text) ([[Char]] -> [Doc]) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[[Char]]] -> [[Char]]
table [Char]
" "
        [ [ [Char]
forall a. IsString a => a
intT,      [Char]
":", [Char]
"Set" ]
        , [ [Char]
forall a. IsString a => a
intToNatT, [Char]
":", [Char]
forall a. IsString a => a
intT, [Char]
forall a. IsString a => a
uArrow , [Char]
forall a. IsString a => a
natT ]
        , [ [Char]
forall a. IsString a => a
natToIntT, [Char]
":", [Char]
forall a. IsString a => a
natT, [Char]
forall a. IsString a => a
uArrow , [Char]
forall a. IsString a => a
intT ]
        ]
      ]
    , [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ([Char] -> Doc) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ [Char]
s -> [Doc] -> Doc
hsep [ Doc
"{-#", Doc
"COMPILE", Doc
"GHC", [Char] -> Doc
text [Char]
s, Doc
"#-}" ]) ([[Char]] -> [Doc]) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> a -> b
$
        [Char] -> [[[Char]]] -> [[Char]]
table [Char]
" = "
        [ [ [Char]
forall a. IsString a => a
intT,      [Char]
"type Prelude.Int"    ]
        , [ [Char]
forall a. IsString a => a
intToNatT, [Char]
"Prelude.toInteger"   ]
        , [ [Char]
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 (Doc -> Doc) -> Doc -> Doc
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 [ Doc
forall a. IsString a => a
posT, Doc
equals, Doc
forall a. IsString a => a
maybeT, Doc -> Doc
parens Doc
intPairT ]

-- | 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 :: [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 ([Doc] -> Doc) -> [Doc] -> Doc
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 (Maybe [Char] -> Bool
forall a. Maybe a -> Bool
isJust Maybe [Char]
layoutMod) Bool
False Bool
False
  , [Char] -> [[Char]] -> Doc
importCats [Char]
astmod ([[Char]] -> [[Char]]
forall a. Eq a => [a] -> [a]
List.nub [[Char]]
cs)
  , TokenText -> Bool -> [[Char]] -> Doc
importPragmas TokenText
tokenText Bool
False ([[Char]] -> Doc) -> [[Char]] -> Doc
forall a b. (a -> b) -> a -> b
$ [ MakeComment
qual [Char]
emod, [Char]
pmod] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ Maybe [Char] -> [[Char]]
forall a. Maybe a -> [a]
maybeToList (MakeComment
qual MakeComment -> Maybe [Char] -> Maybe [Char]
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 -- Make sure we terminate the file with a new line.
  ]
  where
  cs :: [String]
  cs :: [[Char]]
cs = (Cat -> Maybe [Char]) -> [Cat] -> [[Char]]
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         -> [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    CoercCat [Char]
s Integer
_  -> [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    TokenCat [Char]
"Char" -> Maybe [Char]
forall a. Maybe a
Nothing
    TokenCat [Char]
s    -> [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    ListCat Cat
c     -> Cat -> Maybe [Char]
baseCat Cat
c
  qual :: MakeComment
qual [Char]
m = [Char]
"qualified " [Char] -> MakeComment
forall a. [a] -> [a] -> [a]
++ [Char]
m

-- We prefix the Agda types with "#" to not conflict with user-provided nonterminals.
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"     -- This is the BNFC name for token type Char!
integerT :: forall a. IsString a => a
integerT        = a
"Integer"  -- This is the BNFC name for token type Integer!
doubleT :: forall a. IsString a => a
doubleT         = a
"Double"   -- This is the BNFC name for token type 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"     -- Int is the type used by the Haskell backend for line and column positions.
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 [ Doc
forall a. IsString a => a
pairT, Doc
forall a. IsString a => a
intT, Doc
forall a. IsString a => a
intT ]

-- | Preamble: introductory comments.

preamble
  :: String  -- ^ Time stamp.
  -> String  -- ^ Brief characterization of file content.
  -> Doc
preamble :: [Char] -> [Char] -> Doc
preamble [Char]
_time [Char]
what = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
  [ [Doc] -> Doc
hcat [ Doc
"-- Agda bindings for the Haskell ", [Char] -> Doc
text [Char]
what, Doc
"." ]
  -- -- 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 information, import natural numbers.
  -> Bool          -- ^ Do we need @Maybe@?
  -> Doc
imports :: ImportNumeric -> Bool -> Bool -> Bool -> Doc
imports ImportNumeric
numeric Bool
layout Bool
pos Bool
needMaybe = [Doc] -> Doc
vcat ([Doc] -> Doc)
-> ([[([Char], [Doc], [([Char], Doc)])]] -> [Doc])
-> [[([Char], [Doc], [([Char], Doc)])]]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Char], [Doc], [([Char], Doc)]) -> Doc)
-> [([Char], [Doc], [([Char], Doc)])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], [Doc], [([Char], Doc)]) -> Doc
prettyImport ([([Char], [Doc], [([Char], Doc)])] -> [Doc])
-> ([[([Char], [Doc], [([Char], Doc)])]]
    -> [([Char], [Doc], [([Char], Doc)])])
-> [[([Char], [Doc], [([Char], Doc)])]]
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[([Char], [Doc], [([Char], Doc)])]]
-> [([Char], [Doc], [([Char], Doc)])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[([Char], [Doc], [([Char], Doc)])]] -> Doc)
-> [[([Char], [Doc], [([Char], Doc)])]] -> Doc
forall a b. (a -> b) -> a -> b
$
  [ Bool
-> [([Char], [Doc], [([Char], Doc)])]
-> [([Char], [Doc], [([Char], Doc)])]
forall m. Monoid m => Bool -> m -> m
when Bool
layout
    [ ([Char]
"Agda.Builtin.Bool",   [],            [([Char]
"Bool", Doc
forall a. IsString a => a
boolT)]) ]
  , [ ([Char]
"Agda.Builtin.Char",   [Doc
forall a. IsString a => a
charT],       []               ) ]
  , Bool
-> [([Char], [Doc], [([Char], Doc)])]
-> [([Char], [Doc], [([Char], Doc)])]
forall m. Monoid m => Bool -> m -> m
when (ImportNumeric
numeric ImportNumeric -> ImportNumeric -> Bool
forall a. Eq a => a -> a -> Bool
== ImportNumeric
YesImportNumeric) [([Char], [Doc], [([Char], Doc)])]
importNumeric
  , [ ([Char]
"Agda.Builtin.List",   [Doc
"[]", Doc
"_∷_"], [([Char]
"List", Doc
forall a. IsString a => a
listT)]) ]
  , Bool
-> [([Char], [Doc], [([Char], Doc)])]
-> [([Char], [Doc], [([Char], Doc)])]
forall m. Monoid m => Bool -> m -> m
when Bool
needMaybe
    [ ([Char]
"Agda.Builtin.Maybe",  [], [([Char]
"Maybe", Doc
forall a. IsString a => a
maybeT), ([Char]
"nothing", Doc
forall a. IsString a => a
nothingT), ([Char]
"just", Doc
forall a. IsString a => a
justT)]) ]
  , Bool
-> [([Char], [Doc], [([Char], Doc)])]
-> [([Char], [Doc], [([Char], Doc)])]
forall m. Monoid m => Bool -> m -> m
when Bool
pos
    [ ([Char]
"Agda.Builtin.Nat",    [],            [([Char]
"Nat" , Doc
forall a. IsString a => a
natT )]) ]
  , [ ([Char]
"Agda.Builtin.String", [], [([Char]
"String", Doc
forall a. IsString a => a
stringT), ([Char]
"primStringFromList", Doc
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", Doc
forall a. IsString a => a
doubleT)])
    , ([Char]
"Agda.Builtin.Int   public", [], [([Char]
"Int", Doc
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)
    | [([Char], Doc)] -> Bool
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 ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
        (([Char], Doc) -> Doc) -> [([Char], Doc)] -> [Doc]
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 ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ Doc
"open", Doc
"import", [Char] -> Doc
text [Char]
m ]
      , [ Doc
"using", Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"; " [Doc]
use ]
      , [ Doc
"renaming" | Bool -> Bool
not ([([Char], Doc)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], Doc)]
ren) ]
      ]

-- | Import Agda AST.
--
importCats
  :: String    -- ^ Module for Agda AST.
  -> [String]  -- ^ Agda data types to import.
  -> 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 ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ([Char] -> Doc) -> [[Char]] -> [Doc]
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" ]

-- | 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 information?
  -> [String]  -- ^ Haskell modules to import.
  -> Doc
importPragmas :: TokenText -> Bool -> [[Char]] -> Doc
importPragmas TokenText
tokenText Bool
pos [[Char]]
mods = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ([Char] -> Doc) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Doc
imp ([[Char]] -> [Doc]) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [[Char]]
base [[Char]] -> [[Char]] -> [[Char]]
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 = [[[Char]]] -> [[Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [ [Char]
"Prelude (" [Char] -> MakeComment
forall a. [a] -> [a] -> [a]
++ [Char]
preludeImports [Char] -> MakeComment
forall a. [a] -> [a] -> [a]
++ [Char]
")" ]
    , Bool -> [[Char]] -> [[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 = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
", " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[[Char]]] -> [[Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [ [Char]
"Bool", [Char]
"Char", [Char]
"Double", [Char]
"Integer", [Char]
"String", [Char]
"(.)" ]
    , Bool -> [[Char]] -> [[Char]]
forall m. Monoid m => Bool -> m -> m
when Bool
pos
      [ [Char]
"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 :: [Char] -> TokenText -> [Char] -> Bool -> Doc
prToken [Char]
amod TokenText
tokenText [Char]
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", [Char] -> Doc
text [Char]
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
          [ [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ MakeComment
agdaLower [Char]
t
          , Doc
":"
          , Doc
forall a. IsString a => a
pairT
          , Doc -> Doc
parens Doc
intPairT
          , Cat -> Doc
prettyCat Cat
typ
          , Doc
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")

-- | 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 -> 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 ([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
. [Char] -> Bool -> ConstructorStyle -> Data -> [Doc]
prData [Char]
amod Bool
havePos 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" False 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 "Foo" True UnnamedArg (Cat "Nat", [ ("Zero", []), ("Suc", [Cat "Nat"]) ])
-- Nat = Nat' #BNFCPosition
-- <BLANKLINE>
-- data Nat' Pos# : Set where
--   zero : Pos# → Nat' Pos#
--   suc  : Pos# → Nat' Pos# → Nat' Pos#
-- <BLANKLINE>
-- {-# COMPILE GHC Nat' = data Foo.Nat'
--   ( Foo.Zero
--   | Foo.Suc
--   ) #-}
--
-- >>> vsep $ prData "Bar" False 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 -> Bool -> ConstructorStyle -> Data -> [Doc]
prData :: [Char] -> Bool -> ConstructorStyle -> Data -> [Doc]
prData [Char]
amod Bool
True  ConstructorStyle
style (Cat [Char]
d, [([Char], [Cat])]
cs) = [[Doc]] -> [Doc]
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), Doc
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
  -- Replace _ by - in Agda names to avoid illegal names like Foo_'.
  sanitize :: MakeComment
sanitize = Char -> Char -> MakeComment
forall a. Eq a => a -> a -> [a] -> [a]
replace Char
'_' Char
'-'
  primed :: [Char]
primed   = [Char]
d [Char] -> MakeComment
forall a. [a] -> [a] -> [a]
++ [Char]
"'"
  param :: [Char]
param    = [Char]
"Pos#"
  addP :: MakeComment
addP [Char]
c   = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [MakeComment
sanitize [Char]
c, [Char]
"' ", [Char]
param]
  cs' :: [([Char], [Cat])]
cs'      = (([Char], [Cat]) -> ([Char], [Cat]))
-> [([Char], [Cat])] -> [([Char], [Cat])]
forall a b. (a -> b) -> [a] -> [b]
map (([Cat] -> [Cat]) -> ([Char], [Cat]) -> ([Char], [Cat])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (([Cat] -> [Cat]) -> ([Char], [Cat]) -> ([Char], [Cat]))
-> ([Cat] -> [Cat]) -> ([Char], [Cat]) -> ([Char], [Cat])
forall a b. (a -> b) -> a -> b
$ \ [Cat]
cats -> [Char] -> Cat
Cat [Char]
param Cat -> [Cat] -> [Cat]
forall a. a -> [a] -> [a]
: (Cat -> Cat) -> [Cat] -> [Cat]
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 ([Char] -> Cat) -> [Char] -> Cat
forall a b. (a -> b) -> a -> b
$ MakeComment
addP [Char]
c
    ListCat Cat
c -> Cat -> Cat
ListCat (Cat -> Cat) -> Cat -> Cat
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])]
_ ) = [Char] -> [Doc]
forall a. HasCallStack => [Char] -> a
error ([Char] -> [Doc]) -> [Char] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [Char]
"prData: unexpected category " [Char] -> MakeComment
forall a. [a] -> [a] -> [a]
++ Cat -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Cat
c

-- | Pretty-print Agda data types and pragmas.
--
-- >>> vsep $ prData' "ErrM" UnnamedArg "Err A" "Err_" [ ("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 -> 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 ([[Char]] -> [Char]
forall a. [a] -> a
head ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
words [Char]
d) [Char]
haskellDataName [([Char], [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 :: [Char] -> Doc
prErrM [Char]
emod = [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
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 (Cat -> Cat) -> Cat -> Cat
forall a b. (a -> b) -> a -> b
$ [Char] -> Cat
Cat [Char]
"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 -> [Char] -> [([Char], [Cat])] -> Doc
prettyData ConstructorStyle
style [Char]
d [([Char], [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", [Char] -> Doc
text [Char]
d, Doc
colon, Doc
"Set", Doc
"where" ] ]
  , [(Doc, Doc)] -> [Doc]
mkTSTable ([(Doc, Doc)] -> [Doc]) -> [(Doc, Doc)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (([Char], [Cat]) -> (Doc, Doc))
-> [([Char], [Cat])] -> [(Doc, Doc)]
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 = ([Char] -> Doc) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> ([Char] -> Doc) -> [Char] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc
text) ([[Char]] -> [Doc])
-> ([(Doc, Doc)] -> [[Char]]) -> [(Doc, Doc)] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[[Char]]] -> [[Char]]
table [Char]
" : " ([[[Char]]] -> [[Char]])
-> ([(Doc, Doc)] -> [[[Char]]]) -> [(Doc, Doc)] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Doc, Doc) -> [[Char]]) -> [(Doc, Doc)] -> [[[Char]]]
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 ]

-- | Generate pragmas to bind Haskell AST to Agda.
--
-- >>> pragmaData "Foo" "Empty" "Bar" []
-- {-# COMPILE GHC Empty = data Foo.Bar () #-}
--
-- >>> pragmaData "Foo" "Nat" "Natty" [ ("zero", []), ("suc", [Cat "Nat"]) ]
-- {-# COMPILE GHC Nat = data Foo.Natty
--   ( Foo.zero
--   | Foo.suc
--   ) #-}
--
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
"|" ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    (([Char], [Cat]) -> Doc) -> [([Char], [Cat])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [Char] -> Doc
prettyFun [Char]
amod ([Char] -> Doc)
-> (([Char], [Cat]) -> [Char]) -> ([Char], [Cat]) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char], [Cat]) -> [Char]
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 ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
amod, [Char]
".", [Char]
haskellDataName ]
    ]

-- | 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 -> [Char] -> ([Char], [Cat]) -> (Doc, Doc)
prettyConstructor ConstructorStyle
style [Char]
d ([Char]
c, [Cat]
as) = ([Char] -> Doc
prettyCon [Char]
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 [Char] -> Doc
text [Char]
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
uArrow
  , [Char] -> Doc
text [Char]
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
uArrow [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, [Char]) -> Doc) -> [(Maybe Int, [Char])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Doc
text ([Char] -> Doc)
-> ((Maybe Int, [Char]) -> [Char]) -> (Maybe Int, [Char]) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Int, [Char]) -> [Char]
forall {a}. Show a => (Maybe a, [Char]) -> [Char]
subscript) ([(Maybe Int, [Char])] -> [Doc]) -> [(Maybe Int, [Char])] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [(Maybe Int, [Char])]
forall a. Ord a => [a] -> [(Maybe Int, a)]
numberUniquely ([[Char]] -> [(Maybe Int, [Char])])
-> [[Char]] -> [(Maybe Int, [Char])]
forall a b. (a -> b) -> a -> b
$ (Cat -> [Char]) -> [Cat] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Cat -> [Char]
nameSuggestion [Cat]
as
  tel :: [(NonEmpty Doc, Doc)]
tel = ((Doc, Doc) -> [Char]) -> [(Doc, Doc)] -> [(NonEmpty Doc, Doc)]
forall c a b. Eq c => ((a, b) -> c) -> [(a, b)] -> [(List1 a, b)]
aggregateOn (Doc -> [Char]
render (Doc -> [Char]) -> ((Doc, Doc) -> Doc) -> (Doc, Doc) -> [Char]
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, [Char]) -> [Char]
subscript (Maybe a
m, [Char]
s) = [Char] -> (a -> [Char]) -> Maybe a -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
s (\ a
n -> [Char]
s [Char] -> MakeComment
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> MakeComment
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 -> [Char]
forall a. Show a => a -> [Char]
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 :: forall c a b. Eq c => ((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 -> [Char]
nameSuggestion = \case
  ListCat Cat
c     -> Cat -> [Char]
nameSuggestion Cat
c [Char] -> MakeComment
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"

-- | Suggest the name of a bound variable of the given base category.
--
-- >>> map nameFor ["Stm","ABC","#String"]
-- ["s","a","s"]
--
nameFor :: String -> String
nameFor :: MakeComment
nameFor [Char]
d = [ Char -> Char
toLower (Char -> Char) -> Char -> Char
forall a b. (a -> b) -> a -> b
$ [Char] -> Char
forall a. [a] -> a
head ([Char] -> Char) -> [Char] -> Char
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> MakeComment
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'#') [Char]
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 :: forall a. Ord a => [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 ([Char] -> Int
forall a. HasCallStack => [Char] -> a
error [Char]
"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 :: forall a. Ord a => a -> Frequency a -> Frequency a
incr = (Maybe Int -> Maybe Int) -> a -> Map a Int -> Map a Int
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter ((Maybe Int -> Maybe Int) -> a -> Map a Int -> Map a Int)
-> (Maybe Int -> Maybe Int) -> a -> Map a Int -> Map a Int
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.

agdaDefCfg :: DefCfg
agdaDefCfg :: DefCfg
agdaDefCfg = DefCfg
  { sanitizeName :: MakeComment
sanitizeName = MakeComment
agdaLower
  , hasType :: [Char]
hasType      = [Char]
":"
  , arrow :: [Char]
arrow        = [Char]
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 -> [Char] -> Type -> [Exp] -> Exp
forall f. f -> Type -> [Exp' f] -> Exp' f
App [Char]
"#pos" Type
dummyType [Exp
e]
  , polymorphism :: [Base] -> [Base]
polymorphism = ([Char] -> Base
forall a. a -> Base' a
BaseT [Char]
"{a : Set}" Base -> [Base] -> [Base]
forall a. a -> [a] -> [a]
:)
  }

-- | Generate Haskell code for the @define@d constructors.
definedRules :: Bool -> CF -> Doc
definedRules :: Bool -> CF -> Doc
definedRules Bool
havePos = [Doc] -> Doc
vsep ([Doc] -> Doc) -> (CF -> [Doc]) -> CF -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefCfg -> Bool -> CF -> [Doc]
definedRules' DefCfg
agdaDefCfg Bool
havePos

-- * Generate bindings for the pretty printers

-- UNUSED
-- -- | Generate Agda code to print tokens.
-- --
-- -- >>> printToken "Ident"
-- -- printIdent : Ident → #String
-- -- printIdent (ident s) = #stringFromList s
-- --
-- printToken :: String -> Doc
-- printToken t = vcat
--   [ hsep [ f, colon, text t, uArrow, stringT ]
--   , hsep [ f, lparen <> c <+> "s" <> rparen, equals, stringFromListT, "s" ]
--   ]
--   where
--   f = text $ "print" ++ t
--   c = text $ agdaLower 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 :: [Char] -> [Cat] -> Doc
printers [Char]
_amod []   = Doc
empty
printers  [Char]
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
uArrow, 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 = [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
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  -- 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 [Char] -> [Cat] -> Doc
parsers TokenText
tokenText Maybe [Char]
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
forall a. IsString a => a
boolT, Doc
forall a. IsString a => a
uArrow ]
   , [ Doc
forall a. IsString a => a
stringT, Doc
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 ([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 [ [Char] -> Doc
text [Char]
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 [Char] -> Bool
forall a. Maybe a -> Bool
isJust Maybe [Char]
layoutMod
  lmod :: String
  lmod :: [Char]
lmod = Maybe [Char] -> [Char]
forall a. HasCallStack => Maybe a -> a
fromJust Maybe [Char]
layoutMod

-- * Auxiliary functions

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

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

-- | Pretty-print a rule name for Agda.
prettyCon :: Fun -> Doc
prettyCon :: [Char] -> Doc
prettyCon = [Char] -> Doc
text ([Char] -> Doc) -> MakeComment -> [Char] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MakeComment
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 :: MakeComment
agdaLower = MakeComment
avoidKeywords MakeComment -> MakeComment -> MakeComment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> MakeComment
forall {a}. (a -> a) -> [a] -> [a]
updateHead Char -> Char
toLower MakeComment -> MakeComment -> MakeComment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Char -> MakeComment
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 :: MakeComment
avoidKeywords [Char]
s
    | [Char]
s [Char] -> Set [Char] -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set [Char]
agdaKeywords = [Char]
s [Char] -> MakeComment
forall a. [a] -> [a] -> [a]
++ [Char]
"\'"
    | Bool
otherwise = [Char]
s

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

-- | Name of Agda parser binding (mentions precedence).
--
-- >>> agdaParserName $ ListCat $ CoercCat "Exp" 2
-- parseListExp2
--
agdaParserName :: Cat -> Doc
agdaParserName :: Cat -> Doc
agdaParserName Cat
c = [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"parse" [Char] -> MakeComment
forall a. [a] -> [a] -> [a]
++ Cat -> [Char]
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 = [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"print" [Char] -> MakeComment
forall a. [a] -> [a] -> [a]
++ Cat -> [Char]
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 [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    -> 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
  Cat [Char]
c     -> (Char -> Bool) -> [Char] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace [Char]
c
  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 :: [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      -- ^ 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 :: [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"
  , 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
<+> [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 ([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.