Primitives.hs

{-# LANGUAGE OverloadedStrings #-}

module G2.Language.Primitives where

import qualified G2.Language.ExprEnv as E
import G2.Language.KnownValues as KV
import G2.Language.Syntax
import G2.Language.Typing

import Data.Foldable
import qualified Data.Text as T

primStr :: Primitive -> T.Text
primStr Ge = ">="
primStr Gt = ">"
primStr Eq = "=="
primStr Neq = "/="
primStr Lt = "<"
primStr Le = "<="
primStr And = "&&"
primStr Or = "||"
primStr Not = "not"
primStr Implies = "implies"
primStr Iff = "iff"
primStr Plus = "+"
primStr Minus = "-"
primStr Mult = "*"
primStr Div = "/"
primStr DivInt = "/"
primStr Quot = "quot"
primStr Mod = "mod"
primStr Negate = "negate"
primStr SqRt = "sqrt"
primStr IntToFloat = "fromIntegral"
primStr IntToDouble = "fromIntegral"
primStr FromInteger = "fromInteger"
primStr ToInteger = "toInteger"
primStr ToInt = "toInt"
primStr Error = "error"
primStr Undefined = "undefined"
primStr BindFunc = "BindFunc"

strToPrim :: T.Text -> Maybe Primitive
strToPrim "not" = Just Not
strToPrim "&&" = Just And
strToPrim "||" = Just Or
strToPrim ">=" = Just Ge
strToPrim ">" = Just Gt
strToPrim "==" = Just Eq
strToPrim "/=" = Just Neq
strToPrim "<=" = Just Le
strToPrim "<" = Just Lt
strToPrim "+" = Just Plus
strToPrim "-" = Just Minus
strToPrim "*" = Just Mult
strToPrim "quot" = Just Quot
strToPrim "/" = Just Div
strToPrim "mod" = Just Mod
strToPrim "negate" = Just Negate
strToPrim "sqrt" = Just SqRt
strToPrim "error" = Just Error
strToPrim "implies" = Just Implies
strToPrim "iff" = Just Iff
strToPrim _ = Nothing

findPrim :: Primitive -> [(Name, Type)] -> (Name, Type)
findPrim prim [] = error $ "findPrim: not found: " ++ (T.unpack $ primStr prim)
findPrim prim (p@(Name occ _ _ _, _):ps) =
    if primStr prim == occ then p else findPrim prim ps

mkRawPrim :: [(Name, Type)] -> Name -> Expr
mkRawPrim primtys name@(Name occ _ _ _) = 
        case prim of
            Just _ -> foldr (Lam TypeL) cases ids
            Nothing -> Prim Undefined TyBottom
  where
    prim = strToPrim occ

    ty = snd . head $ filter (\p -> name == fst p) primtys
    (forall_ids, ty') = splitTyForAlls ty
    fun_tys = splitTyFuns ty'

    tys = (map typeOf forall_ids) ++ fun_tys

    ids = map (\(i, t) -> Id (Name "a" Nothing i Nothing) t) $ zip [1..] (init tys)
    binds = map (\(i, t) -> Id (Name "b" Nothing i Nothing) t) $ zip [1..] (init tys)

    varIds = map Var ids
    varBinds = map Var binds

    apps = foldl' App (Prim (case prim of
                                    Just p -> p
                                    Nothing -> error $ "PRIM = " ++ show prim) ty) varBinds

    cases = foldr (\(i, b) e -> Case i b [Alt Default e]) apps (zip varIds binds)

-- | Primitive lookup helpers

mkPrim :: Primitive -> E.ExprEnv -> Expr
mkPrim p eenv = case (inClasses, inNum, inPrelude, inClasses2, inBase2, inReal) of
    (Just e, _, _, _, _, _) -> e
    (_, Just e, _, _, _, _) -> e
    (_, _, Just e, _, _, _) -> e
    (_, _, _, Just e, _, _) -> e
    (_, _, _, _, Just e, _) -> e
    (_, _, _, _, _, Just e) -> e
    _ -> error $ "Unrecognized prim " ++ show p ++ " " ++ show (primStr p)
    where
        inClasses = E.occLookup (primStr p) (Just "GHC.Classes") eenv
        inNum = E.occLookup (primStr p) (Just "GHC.Num") eenv
        inPrelude = E.occLookup (primStr p) (Just "Prelude") eenv
        inClasses2 = E.occLookup (primStr p) (Just "GHC.Classes2") eenv
        inBase2 = E.occLookup (primStr p) (Just "GHC.Base2") eenv
        inReal = E.occLookup (primStr p) (Just "GHC.Real") eenv

mkGe :: E.ExprEnv -> Expr
mkGe = mkPrim Ge

mkGt :: E.ExprEnv -> Expr
mkGt = mkPrim Gt

mkEq :: E.ExprEnv -> Expr
mkEq = mkPrim Eq

mkEq' :: KnownValues -> Expr
mkEq' kv = Var (Id (eqFunc kv) TyBottom)

mkNeq :: E.ExprEnv -> Expr
mkNeq = mkPrim Neq

mkLt :: E.ExprEnv -> Expr
mkLt = mkPrim Lt

mkLe :: E.ExprEnv -> Expr
mkLe = mkPrim Le

mkAnd :: E.ExprEnv -> Expr
mkAnd = mkPrim And

mkOr :: E.ExprEnv -> Expr
mkOr = mkPrim Or

mkNot :: E.ExprEnv -> Expr
mkNot = mkPrim Not

mkPlus :: E.ExprEnv -> Expr
mkPlus = mkPrim Plus

mkMinus :: E.ExprEnv -> Expr
mkMinus = mkPrim Minus

mkMult :: E.ExprEnv -> Expr
mkMult = mkPrim Mult

mkDiv :: E.ExprEnv -> Expr
mkDiv = mkPrim Div

mkMod :: E.ExprEnv -> Expr
mkMod = mkPrim Mod

mkNegate :: E.ExprEnv -> Expr
mkNegate = mkPrim Negate

mkImplies :: E.ExprEnv -> Expr
mkImplies = mkPrim Implies

mkIff :: E.ExprEnv -> Expr
mkIff = mkPrim Iff

mkFromInteger :: E.ExprEnv -> Expr
mkFromInteger = mkPrim FromInteger

mkToInteger :: E.ExprEnv -> Expr
mkToInteger = mkPrim ToInteger

-- Primitives on primitive types
mkEqPrimType :: Type -> KnownValues -> Expr
mkEqPrimType t kv =
    Prim Eq $ TyFun t (TyFun t (TyCon (KV.tyBool kv) TYPE))

mkEqPrimInt :: KnownValues -> Expr
mkEqPrimInt = mkEqPrimType TyLitInt

mkEqPrimFloat :: KnownValues -> Expr
mkEqPrimFloat = mkEqPrimType TyLitFloat

mkEqPrimDouble :: KnownValues -> Expr
mkEqPrimDouble = mkEqPrimType TyLitDouble

mkEqPrimChar :: KnownValues -> Expr
mkEqPrimChar = mkEqPrimType TyLitChar