Prelude.hs

{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}

{- |
Module      : Verifier.SAW.Prelude
Copyright   : Galois, Inc. 2012-2015
License     : BSD3
Maintainer  : jhendrix@galois.com
Stability   : experimental
Portability : non-portable (language extensions)
-}

module Verifier.SAW.Prelude
  ( Module
  , module Verifier.SAW.Prelude
  , module Verifier.SAW.Prelude.Constants
  ) where

import qualified Data.Map as Map

import Verifier.SAW.ParserUtils
import Verifier.SAW.Prelude.Constants
import Verifier.SAW.SharedTerm
import Verifier.SAW.FiniteValue

import Verifier.SAW.Simulator.Concrete (evalSharedTerm)
import Verifier.SAW.Simulator.Value (asFirstOrderTypeValue)


$(defineModuleFromFileWithFns
  "preludeModule" "scLoadPreludeModule" "prelude/Prelude.sawcore")

-- | Given two terms, compute a term representing a decidable
--   equality test between them.  The terms are assumed to
--   be of the same type, which must be a first-order type.
--   The returned term will be of type @Bool@.
scEq :: SharedContext -> Term -> Term -> IO Term
scEq sc x y = do
  xty <- scTypeOf sc x
  mmap <- scGetModuleMap sc
  case asFirstOrderTypeValue (evalSharedTerm mmap mempty mempty xty) of
    Just fot -> scDecEq sc fot (Just (x,y))
    Nothing  -> fail ("scEq: expected first order type, but got: " ++ showTerm xty)

-- | Given a first-order type, return the decidable equality
--   operation on that type.  If arguments are provided, they
--   will be applied, returning a value of type @Bool@.  If no
--   arguments are provided a function of type @tp -> tp -> Bool@
--   will be returned.
scDecEq ::
  SharedContext ->
  FirstOrderType    {- ^ Type of elements to test for equality -} ->
  Maybe (Term,Term) {- ^ optional arguments to apply -} ->
  IO Term
scDecEq sc fot args = case fot of
  FOTBit ->
    do fn <- scGlobalDef sc "Prelude.boolEq"
       case args of
         Nothing    -> return fn
         Just (x,y) -> scApplyAll sc fn [x,y]

  FOTInt ->
    do fn <- scGlobalDef sc "Prelude.intEq"
       case args of
         Nothing    -> return fn
         Just (x,y) -> scApplyAll sc fn [x,y]

  FOTIntMod m ->
    do fn <- scGlobalDef sc "Prelude.intModEq"
       m' <- scNat sc m
       case args of
         Nothing    -> scApply sc fn m'
         Just (x,y) -> scApplyAll sc fn [m',x,y]

  FOTVec w FOTBit ->
    do fn <- scGlobalDef sc "Prelude.bvEq"
       w' <- scNat sc w
       case args of
         Nothing    -> scApply sc fn w'
         Just (x,y) -> scApplyAll sc fn [w',x,y]

  FOTVec w t ->
    do fn <- scGlobalDef sc "Prelude.vecEq"
       w' <- scNat sc w
       t' <- scFirstOrderType sc t
       subFn <- scDecEq sc t Nothing
       case args of
         Nothing    -> scApplyAll sc fn [w',t',subFn]
         Just (x,y) -> scApplyAll sc fn [w',t',subFn,x,y]

  FOTArray a b ->
    do a' <- scFirstOrderType sc a
       b' <- scFirstOrderType sc b
       fn <- scGlobalDef sc "Prelude.arrayEq"
       case args of
         Nothing    -> scApplyAll sc fn [a',b']
         Just (x,y) -> scApplyAll sc fn [a',b',x,y]

  FOTTuple []  ->
    case args of
      Nothing -> scGlobalDef sc "Prelude.unitEq"
      Just _  -> scBool sc True

  FOTTuple [t] -> scDecEq sc t args

  FOTTuple (t:ts) ->
    do fnLeft  <- scDecEq sc t Nothing
       fnRight <- scDecEq sc (FOTTuple ts) Nothing
       fn      <- scGlobalDef sc "Prelude.pairEq"
       t'      <- scFirstOrderType sc t
       ts'     <- scFirstOrderType sc (FOTTuple ts)
       case args of
         Nothing    -> scApplyAll sc fn [t',ts',fnLeft,fnRight]
         Just (x,y) -> scApplyAll sc fn [t',ts',fnLeft,fnRight,x,y]

  FOTRec fs ->
    case args of
      Just (x,y) ->
           mkRecordEqBody (Map.toList fs) x y

      Nothing -> 
        do x <- scLocalVar sc 1
           y <- scLocalVar sc 0
           tp   <- scFirstOrderType sc fot
           body <-  mkRecordEqBody (Map.toList fs) x y
           scLambdaList sc [("x",tp),("y",tp)] body

 where
  mkRecordEqBody [] _x _y = scBool sc True
  mkRecordEqBody [(f,tp)] x y =
     do xf <- scRecordSelect sc x f
        yf <- scRecordSelect sc y f
        scDecEq sc tp (Just (xf,yf))
  mkRecordEqBody ((f,tp):fs) x y =
     do xf   <- scRecordSelect sc x f
        yf   <- scRecordSelect sc y f
        fp  <- scDecEq sc tp (Just (xf,yf))
        fsp <- mkRecordEqBody fs x y
        scAnd sc fp fsp

-- | For backwards compatibility: @Bool@ used to be a datatype, and so its
-- creation function was called @scPrelude_Bool@ instead of
-- @scApplyPrelude_Bool@
scPrelude_Bool :: SharedContext -> IO Term
scPrelude_Bool = scApplyPrelude_Bool