module Agda.Compiler.UHC.MagicTypes
( builtinUnitCtor
, MagicName
, getMagicTypes
, MagicConstrInfo
, MagicTypeInfo
, HsDataType (..)
)
where
import Data.List
import qualified Data.Map as M
import Agda.Compiler.UHC.Bridge
type MagicName = String
data HsDataType
= HsDataType HsName
| HsUnit
type MagicConstrInfo = M.Map MagicName CTag
type MagicTypeInfo = M.Map MagicName (HsDataType, MagicConstrInfo)
getMagicTypes :: MagicTypeInfo
getMagicTypes = M.fromList $ map f primCrTys1
where f :: (MagicName, [(MagicName, CTag)]) -> (MagicName, (HsDataType, MagicConstrInfo))
f (dtMgcNm, constrs) = let dtCrNm = ctagDataTyNm $ snd $ head constrs
in (dtMgcNm, (dtCrNm, M.fromList constrs))
ctagDataTyNm :: CTag -> HsDataType
ctagDataTyNm = destructCTag HsUnit (\dt _ _ _ -> HsDataType dt)
primCrTys1 :: [(
MagicName
, [(MagicName, CTag)]
)]
primCrTys1 =
[( "BOOL",
[ ("TRUE", ctagTrue defaultEHCOpts)
, ("FALSE", ctagFalse defaultEHCOpts)
])
, ("LIST",
[ ("NIL", ctagNil defaultEHCOpts)
, ("CONS", ctagCons defaultEHCOpts)
])
, ("UNIT",
[("UNIT", ctagUnit)])
]
builtinUnitCtor :: HsName
builtinUnitCtor = mkHsName1 "UHC.Agda.Builtins.unit"