{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} module BNFC.Backend.Agda.Utilities.Utils where import BNFC.Backend.Common.Utils as Utils import BNFC.CF import BNFC.Prelude import Control.Monad.State import qualified Data.Map as Map import Data.String (fromString) import Data.List (intercalate) import Prettyprinter -- | 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 (Eq) 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 numeric layout hasPos needMaybe = vsep $ concat [ Utils.when layout [ "open import Agda.Builtin.Bool using () renaming (Bool to #Bool)" ] , [ "open import Agda.Builtin.Char using (Char)" ] , Utils.when (numeric == YesImportNumeric) [ importNumeric ] , [ "open import Agda.Builtin.List using ([]; _∷_) renaming (List to #List)" ] , Utils.when needMaybe [ hang 2 $ vsep [ "open import Agda.Builtin.Maybe using () renaming" , "( Maybe to #Maybe" , "; nothing to #nothing" , "; just to #just" , ")" ] ] , Utils.when hasPos [ "open import Agda.Builtin.Nat using () renaming (Nat to #Nat)" ] , [ hang 2 $ vsep [ "open import Agda.Builtin.String using () renaming" , "( String to #String" , "; primStringFromList to #stringFromList" , ")" ] ] ] where importNumeric :: Doc () importNumeric = vsep [ "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.Int using () renaming (pos to #pos)" ] importPragmas :: Bool -- ^ Do we use position information? -> [ModuleName] -- ^ Haskell modules to import. -> Doc () importPragmas pos mods = vsep $ map imp $ base ++ mods where imp :: String -> Doc () imp p = "{-# FOREIGN GHC import" <+> fromString p <+> "#-}" base :: [String] base = concat [ ["Prelude (" ++ preludeImports ++ ")"] , Utils.when pos [ "qualified Prelude" ] , [ "qualified Data.Text" ] ] preludeImports :: String preludeImports = intercalate ", " $ ["Bool", "Char", "Double", "Integer", "String", "(.)", "Either (..)" ] ++ Utils.when pos [ "error" ] -- used unqualified by the GHC backend for postulates -- Replace _ by - in Agda names to avoid illegal names like Foo_'. sanitize :: String -> String sanitize = replace '_' '-' -- | 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@. -- | Suggest the name of a bound variable of the given category. -- -- >>> map nameSuggestion -- [ ListType (BaseType (BaseCat 'S':|"tm")), BaseType (TokenCat 'V':|"ar"), (BaseType (BaseCat 'E':|"xp") ] -- ["ss","x","e"] -- nameSuggestion :: Type -> String nameSuggestion = \case BaseType bc -> case bc of BuiltinCat b -> nameFor $ printBuiltinCat b IdentCat _ -> "x" TokenCat _ -> "x" BaseCat x -> nameFor x ListType ty -> nameSuggestion ty ++ "s" -- | Suggest the name of a bound variable of the given base category. -- -- >>> map nameFor ["Stm","ABC","#String"] -- ["s","a","s"] -- nameFor :: String1 -> String nameFor d = [ toLower $ head $ dropWhile (== '#') $ toList 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 as = mapM step as `evalState` Map.empty where -- First pass: determine frequency of each element. counts :: Frequency a counts = foldl (flip incr) Map.empty as -- Second pass: consecutively number elements with frequency > 1. step :: a -> State (Frequency a) (Maybe Int, a) step a = do -- If the element has a unique occurrence, we do not need to number it. let n = Map.findWithDefault (error "numberUniquelyWith") a counts if n == 1 then return (Nothing, a) else do -- Otherwise, increase the counter for that element and number it -- with the new value. modify $ incr a gets ((, a) . Map.lookup a) -- | 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 = Map.alter $ maybe (Just 1) (Just . succ) uArrow :: String uArrow = "→"