{-# LANGUAGE OverloadedStrings #-}

module Language.Sprite.L1.Prims  where

import qualified Data.Maybe                 as Mb
import qualified Data.Map                   as M
import qualified Language.Fixpoint.Types    as F
import qualified Language.Sprite.Common.UX   as UX
import           Language.Sprite.L1.Types 
import           Language.Sprite.L1.Parse

-- | Primitive Types --------------------------------------------------

constTy :: F.SrcSpan -> Prim -> RType
constTy _ (PInt n) = TBase TInt (F.exprReft (F.expr n)) 
constTy l (PBin o) = binOpTy l o

binOpTy :: F.SrcSpan -> PrimOp -> RType 
binOpTy l o = Mb.fromMaybe err (M.lookup o binOpEnv) 
  where 
    err     = UX.panicS ("Unknown PrimOp: " ++ show o) l

bTrue :: Base -> RType
bTrue b = TBase b mempty

binOpEnv :: M.Map PrimOp RType
binOpEnv = M.fromList 
  [ (BPlus , mkTy "x:int => y:int => int[v|v=x+y]")
  , (BMinus, mkTy "x:int => y:int => int[v|v=x-y]") 
  , (BTimes, mkTy "x:int => y:int => int[v|v=x*y]") 
  , (     , mkTy " x : int = > y : int = >  < = > ( x < y ) } " )
  , ( BGt    , mkTy " x : int = > y : int = >  < = > ( x > y ) } " )
  , ( BEq    , mkTy " x : int = > y : int = >  < = > ( x = y ) } " )
  ]

mkTy :: String -> RType
mkTy = parseWith rtype "prims"  

# LANGUAGE OverloadedStrings #
 | Primitive Types --------------------------------------------------

module Language.Sprite.L1.Prims  where

import qualified Data.Maybe                 as Mb
import qualified Data.Map                   as M
import qualified Language.Fixpoint.Types    as F
import qualified Language.Sprite.Common.UX   as UX
import           Language.Sprite.L1.Types 
import           Language.Sprite.L1.Parse


constTy :: F.SrcSpan -> Prim -> RType
constTy _ (PInt n) = TBase TInt (F.exprReft (F.expr n)) 
constTy l (PBin o) = binOpTy l o

binOpTy :: F.SrcSpan -> PrimOp -> RType 
binOpTy l o = Mb.fromMaybe err (M.lookup o binOpEnv) 
  where 
    err     = UX.panicS ("Unknown PrimOp: " ++ show o) l

bTrue :: Base -> RType
bTrue b = TBase b mempty

binOpEnv :: M.Map PrimOp RType
binOpEnv = M.fromList 
  [ (BPlus , mkTy "x:int => y:int => int[v|v=x+y]")
  , (BMinus, mkTy "x:int => y:int => int[v|v=x-y]") 
  , (BTimes, mkTy "x:int => y:int => int[v|v=x*y]") 
  , (     , mkTy " x : int = > y : int = >  < = > ( x < y ) } " )
  , ( BGt    , mkTy " x : int = > y : int = >  < = > ( x > y ) } " )
  , ( BEq    , mkTy " x : int = > y : int = >  < = > ( x = y ) } " )
  ]

mkTy :: String -> RType
mkTy = parseWith rtype "prims"  
