module Agda.Compiler.MAlonzo.Primitives where
import Control.Monad.Reader
import Control.Monad.State
import Data.Char
import Data.List as L
import Data.Map as M
import qualified Language.Haskell.Exts.Syntax as HS
import Agda.Compiler.MAlonzo.Compiler (closedTerm)
import Agda.Compiler.MAlonzo.Misc
import Agda.Compiler.MAlonzo.Pretty
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.Utils.Monad
import qualified Agda.Utils.HashMap as HMap
#include "undefined.h"
import Agda.Utils.Impossible
checkTypeOfMain :: QName -> Type -> TCM [HS.Decl] -> TCM [HS.Decl]
checkTypeOfMain q ty ret
| show (nameConcrete $ qnameName q) /= "main" = ret
| otherwise = do
Def io _ <- ignoreSharing <$> primIO
ty <- normalise ty
case ignoreSharing $ unEl ty of
Def d _ | d == io -> (mainAlias :) <$> ret
_ -> do
err <- fsep $
pwords "The type of main should be" ++
[prettyTCM io] ++ pwords " A, for some A. The given type is" ++ [prettyTCM ty]
typeError $ GenericError $ show err
where
mainAlias = HS.FunBind [HS.Match dummy mainLHS [] Nothing mainRHS $ HS.BDecls [] ]
mainLHS = HS.Ident "main"
mainRHS = HS.UnGuardedRhs $ HS.Var $ HS.UnQual $ unqhname "d" q
importsForPrim :: TCM [HS.ModuleName]
importsForPrim =
xForPrim $
L.map (\(s, ms) -> (s, return (L.map HS.ModuleName ms))) $
[ "CHAR" |-> ["Data.Char"]
, "primIsDigit" |-> ["Data.Char"]
, "primIsLower" |-> ["Data.Char"]
, "primIsDigit" |-> ["Data.Char"]
, "primIsAlpha" |-> ["Data.Char"]
, "primIsSpace" |-> ["Data.Char"]
, "primIsAscii" |-> ["Data.Char"]
, "primIsLatin1" |-> ["Data.Char"]
, "primIsPrint" |-> ["Data.Char"]
, "primIsHexDigit" |-> ["Data.Char"]
, "primToUpper" |-> ["Data.Char"]
, "primToLower" |-> ["Data.Char"]
]
where (|->) = (,)
declsForPrim :: TCM [HS.Decl]
declsForPrim = xForPrim $
[ "NATURAL" |-> (++) <$> natToFrom "Integer" mazNatToInteger mazIntegerToNat
<*> natToFrom "Int" mazNatToInt mazIntToNat
, "LIST" |-> forList mazListToHList mazHListToList
, "STRING" |-> forList mazListToString mazStringToList
, "BOOL" |-> decls ["TRUE", "FALSE"]
mazBoolToHBool "let { f <<0>> = True; f <<1>> = False; } in f"
mazHBoolToBool "let { f True = <<0>>; f False = <<1>>; } in f"
, "CHAR" |-> return
[ fakeDS mazCharToInteger
"(fromIntegral . Data.Char.ord :: Char -> Integer)"
]
]
where
infix 1 |->
(|->) = (,)
forList toH toA = decls ["NIL", "CONS"]
toH (concat
["let { f <<0>> = [];"
," f (<<1>> x xs) = x : f (" ++ prettyPrint mazCoerce ++ " xs)"
,"} in f"])
toA (concat
["let { f [] = <<0>>;"
," f (c:cs) = <<1>> c (" ++ prettyPrint mazCoerce ++ " (f cs));"
,"} in f"])
natToFrom hty to from = let
totxt = repl ["<<0>>", "<<1>>", hty, to] $ concat
[ "\\ x -> case x of { <<0>> -> 0 :: <<2>>; "
, "<<1>> x -> 1 + (<<3>> (" ++ prettyPrint mazCoerce ++ " x)) }" ]
fromtxt = repl ["<<0>>", "<<1>>", hty, from] $ concat
[ "\\ x -> if x <= (0 :: <<2>>) then <<0>> "
, "else <<1>> (" ++ prettyPrint mazCoerce ++ " (<<3>> (x - 1)))" ]
in do
ds <- decls ["ZERO", "SUC"] to totxt from fromtxt
let rule name = HS.Rule name HS.AlwaysActive (Just [HS.RuleVar $ HS.Ident "x"])
qname = HS.UnQual . HS.Ident
var = HS.Var . qname
(%) = HS.App
return $ [HS.RulePragmaDecl dummy
[ rule (to ++ "-" ++ from) (var to % (var from % var "x")) (var "x")
, rule (from ++ "-" ++ to) (var from % (var to % var "x")) (var "x")
],
HS.InlineSig dummy True (HS.ActiveFrom 2) (qname to),
HS.InlineSig dummy True (HS.ActiveFrom 2) (qname from)
] ++ ds
decls cs n1 b1 n2 b2 =
do cs' <- mapM pconName cs
return $ zipWith (\ n -> fakeDS n . repl cs') [n1, n2] [b1, b2]
mazNatToInteger, mazIntegerToNat, mazNatToInt, mazIntToNat, mazCharToInteger,
mazListToHList, mazHListToList, mazListToString, mazStringToList,
mazBoolToHBool, mazHBoolToBool :: String
mazNatToInteger = "mazNatToInteger"
mazIntegerToNat = "mazIntegerToNat"
mazNatToInt = "mazNatToInt"
mazIntToNat = "mazIntToNat"
mazCharToInteger = "mazCharToInteger"
mazListToHList = "mazListToHList"
mazHListToList = "mazHListToList"
mazListToString = "mazListToString"
mazStringToList = "mazStringToList"
mazBoolToHBool = "mazBoolToHBool"
mazHBoolToBool = "mazHBoolToBool"
xForPrim :: [(String, TCM [a])] -> TCM [a]
xForPrim table = do
qs <- HMap.keys <$> curDefs
bs <- toList <$> gets stBuiltinThings
let getName (Builtin (Def q _)) = q
getName (Builtin (Con q _)) = conName q
getName (Builtin (Shared p)) = getName (Builtin $ derefPtr p)
getName (Builtin _) = __IMPOSSIBLE__
getName (Prim (PrimFun q _ _)) = q
concat <$> sequence [ maybe (return []) id $ L.lookup s table
| (s, def) <- bs, getName def `elem` qs ]
primBody :: String -> TCM HS.Exp
primBody s = maybe unimplemented (either (hsVarUQ . HS.Ident) id <$>) $
L.lookup s $
[
"primIntegerPlus" |-> binAsis "(+)" "Integer"
, "primIntegerMinus" |-> binAsis "(-)" "Integer"
, "primIntegerTimes" |-> binAsis "(*)" "Integer"
, "primIntegerDiv" |-> binAsis "div" "Integer"
, "primIntegerMod" |-> binAsis "mod" "Integer"
, "primIntegerEquality"|-> rel "(==)" "Integer"
, "primIntegerLess" |-> rel "(<)" "Integer"
, "primIntegerAbs" |-> do toN <- bltQual' "NATURAL" mazIntegerToNat
return $ repl [toN] $ "\\ x -> <<0>> (abs x)"
, "primNatToInteger" |-> bltQual' "NATURAL" mazNatToInteger
, "primShowInteger" |-> return "(show :: Integer -> String)"
, "primLevelZero" |-> return "()"
, "primLevelSuc" |-> return "(\\ _ -> ())"
, "primLevelMax" |-> return "(\\ _ _ -> ())"
, "primNatPlus" |-> binNat "(+)"
, "primNatMinus" |-> binNat "(-)"
, "primNatTimes" |-> binNat "(*)"
, "primNatDivSuc" |-> binNat "(\\ x y -> div x (y + 1))"
, "primNatModSuc" |-> binNat "(\\ x y -> mod x (y + 1))"
, "primNatEquality" |-> relNat "(==)"
, "primNatLess" |-> relNat "(<)"
, "primIntegerToFloat" |-> return "(fromIntegral :: Integer -> Double)"
, "primFloatPlus" |-> return "((+) :: Double -> Double -> Double)"
, "primFloatMinus" |-> return "((-) :: Double -> Double -> Double)"
, "primFloatTimes" |-> return "((*) :: Double -> Double -> Double)"
, "primFloatDiv" |-> return "((/) :: Double -> Double -> Double)"
, "primFloatEquality" |-> rel "(==)" "Double"
, "primFloatLess" |-> rel "(<)" "Double"
, "primRound" |-> return "(round :: Double -> Integer)"
, "primFloor" |-> return "(floor :: Double -> Integer)"
, "primCeiling" |-> return "(ceiling :: Double -> Integer)"
, "primExp" |-> return "(exp :: Double -> Double)"
, "primLog" |-> return "(log :: Double -> Double)"
, "primSin" |-> return "(sin :: Double -> Double)"
, "primShowFloat" |-> return "(show :: Double -> String)"
, "primRound" |-> return "(round :: Double -> Integer)"
, "primCharEquality" |-> rel "(==)" "Char"
, "primIsLower" |-> pred "Data.Char.isLower"
, "primIsDigit" |-> pred "Data.Char.isDigit"
, "primIsAlpha" |-> pred "Data.Char.isAlpha"
, "primIsSpace" |-> pred "Data.Char.isSpace"
, "primIsAscii" |-> pred "Data.Char.isAscii"
, "primIsLatin1" |-> pred "Data.Char.isLatin1"
, "primIsPrint" |-> pred "Data.Char.isPrint"
, "primIsHexDigit" |-> pred "Data.Char.isHexDigit"
, "primToUpper" |-> return "Data.Char.toUpper"
, "primToLower" |-> return "Data.Char.toLower"
, "primCharToNat" |-> do toN <- bltQual' "NATURAL" mazIntToNat
return $ repl [toN] $
"(\\ x -> <<0>> ((fromEnum :: Char -> Int) x))"
, "primNatToChar" |-> do toI <- bltQual' "NATURAL" mazNatToInt
return $ repl[toI] $
"(\\ x -> (toEnum :: Int -> Char) (<<0>> x))"
, "primShowChar" |-> return "(show :: Char -> String)"
, "primStringToList" |-> bltQual' "STRING" mazStringToList
, "primStringFromList" |-> bltQual' "STRING" mazListToString
, "primStringAppend" |-> binAsis "(++)" "String"
, "primStringEquality" |-> rel "(==)" "String"
, "primShowString" |-> return "(show :: String -> String)"
, "primQNameEquality" |-> rel "(==)" "MAlonzo.RTE.QName () ()"
, "primShowQName" |-> return "MAlonzo.RTE.qnameString"
, "primQNameType" |-> return "MAlonzo.RTE.qnameType"
, "primQNameDefinition" |-> return "MAlonzo.RTE.qnameDefinition"
, "primDataConstructors" |-> return "(error \"primDataConstructors: not implemented\")"
, ("primTrustMe" , Right <$> do
refl <- primRefl
closedTerm $ lam "a" (lam "A" (lam "x" (lam "y" refl))))
]
where
x |-> s = (x, Left <$> s)
bin blt op ty from to = do
from' <- bltQual' blt from
to' <- bltQual' blt to
return $ repl [op, opty ty, from', to'] $
"\\ x y -> <<3>> ((<<0>> :: <<1>>) (<<2>> x) (<<2>> y))"
binNat op = bin "NATURAL" op "Integer" mazNatToInteger mazIntegerToNat
binAsis op ty = return $ repl [op, opty ty] $ "((<<0>>) :: <<1>>)"
rel' toTy op ty = do
toHB <- bltQual' "BOOL" mazHBoolToBool
return $ repl [op, ty, toHB, toTy] $
"(\\ x y -> <<2>> ((<<0>> :: <<1>> -> <<1>> -> Bool) (<<3>> x) (<<3>> y)))"
relNat op = do toHI <- bltQual' "NATURAL" mazNatToInteger
rel' toHI op "Integer"
rel op ty = rel' "" op ty
pred p = do toHB <- bltQual' "BOOL" mazHBoolToBool
return $ repl [p, toHB] $ "(\\ x -> <<1>> (<<0>> x))"
opty t = t ++ "->" ++ t ++ "->" ++ t
unimplemented = typeError $ NotImplemented s
lam x t = Lam (setHiding Hidden defaultArgInfo) (Abs x t)
repl :: [String] -> String -> String
repl subs = go where
go ('<':'<':c:'>':'>':s) | 0 <= i && i < length subs = subs !! i ++ go s
where i = ord c ord '0'
go (c:s) = c : go s
go [] = []
pconName :: String -> TCM String
pconName s = toS =<< getBuiltin s where
toS (Con q _) = prettyPrint <$> conhqn (conName q)
toS (Lam _ t) = toS (unAbs t)
toS _ = mazerror $ "pconName" ++ s
hasCompiledData :: [String] -> TCM Bool
hasCompiledData (s:_) = toB =<< getBuiltin s where
toB (Con q _) = do
def <- getConstInfo =<< ignoreAbstractMode (canonicalName (conName q))
return $ case compiledHaskell $ defCompiledRep def of
Just{} -> True
Nothing -> False
toB (Lam _ t) = toB (unAbs t)
toB _ = return False
hasCompiledData _ = return False
bltQual' :: String -> String -> TCM String
bltQual' b s = prettyPrint <$> bltQual b s