{-# LANGUAGE CPP                   #-}
{-# LANGUAGE Strict                #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PatternGuards         #-}
{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE RankNTypes            #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

-- | This module has the functions that perform sort-checking, and related
-- operations on Fixpoint expressions and predicates.

module Language.Fixpoint.SortCheck  (
  -- * Sort Substitutions
    TVSubst
  , Env
  , mkSearchEnv

  -- * Checking Well-Formedness
  , checkSorted
  , checkSortedReft
  , checkSortedReftFull
  , checkSortFull
  , pruneUnsortedReft

  -- * Sort inference
  , sortExpr
  , checkSortExpr
  , exprSort
  , exprSortMaybe

  -- * Unify
  , unifyFast
  , unifySorts
  , unifyTo1
  , unifys

  -- * Apply Substitution
  , apply
  , defuncEApp

  -- * Exported Sorts
  , boolSort
  , strSort

  -- * Sort-Directed Transformations
  , Elaborate (..)
  , applySorts
  , elabApply
  , elabExpr
  , elabNumeric
  , unApply
  , unElab
  , unElabSortedReft
  , unApplySortedReft
  , unApplyAt
  , toInt

  -- * Predicates on Sorts
  , isFirstOrder
  , isMono

  , runCM0
  ) where

--  import           Control.DeepSeq
import           Control.Exception (Exception, catch, try, throwIO)
import           Control.Monad
import           Control.Monad.Except      -- (MonadError(..))
import           Control.Monad.Reader

import qualified Data.HashMap.Strict       as M
import           Data.IORef
import qualified Data.List                 as L
import           Data.Maybe                (mapMaybe, fromMaybe, catMaybes, isJust)

import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Misc
import           Language.Fixpoint.Types hiding   (subst, GInfo(..), senv)
import qualified Language.Fixpoint.Types.Visitor  as Vis
import qualified Language.Fixpoint.Smt.Theories   as Thy
import           Text.PrettyPrint.HughesPJ.Compat
import           Text.Printf

import           GHC.Stack
import qualified Language.Fixpoint.Types as F
import           System.IO.Unsafe (unsafePerformIO)

--import Debug.Trace as Debug

-- If set to 'True', enable precise logging via CallStacks.
debugLogs :: Bool
debugLogs :: Bool
debugLogs = Bool
False

traced :: HasCallStack => (HasCallStack => String) -> String
traced :: HasCallStack => (HasCallStack => String) -> String
traced HasCallStack => String
str =
  if Bool
debugLogs
    then let prettified :: String
prettified = CallStack -> String
prettyCallStack (CallStack -> CallStack
popCallStack HasCallStack => CallStack
callStack)
         in HasCallStack => String
str forall a. Semigroup a => a -> a -> a
<> String
" (at " forall a. Semigroup a => a -> a -> a
<> String
prettified forall a. Semigroup a => a -> a -> a
<> String
")"
    else HasCallStack => String
str

--------------------------------------------------------------------------------
-- | Predicates on Sorts -------------------------------------------------------
--------------------------------------------------------------------------------
isMono :: Sort -> Bool
--------------------------------------------------------------------------------
isMono :: Sort -> Bool
isMono             = forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Sort -> a) -> a -> Sort -> a
Vis.foldSort [Int] -> Sort -> [Int]
fv []
  where
    fv :: [Int] -> Sort -> [Int]
fv [Int]
vs (FVar Int
i) = Int
i forall a. a -> [a] -> [a]
: [Int]
vs
    fv [Int]
vs Sort
_        = [Int]
vs


--------------------------------------------------------------------------------
-- | Elaborate: make polymorphic instantiation explicit via casts,
--   make applications monomorphic for SMTLIB. This deals with
--   polymorphism by `elaborate`-ing all refinements except for
--   KVars. THIS IS NOW MANDATORY as sort-variables can be
--   instantiated to `int` and `bool`.
--------------------------------------------------------------------------------
class Elaborate a where
  elaborate :: Located String -> SymEnv -> a -> a


instance (Loc a) => Elaborate (SInfo a) where
  elaborate :: Located String -> SymEnv -> SInfo a -> SInfo a
elaborate Located String
x SymEnv
senv SInfo a
si = SInfo a
si
    { cm :: HashMap SubcId (SimpC a)
F.cm      = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
x SymEnv
senv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm      SInfo a
si
    , bs :: BindEnv a
F.bs      = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
x SymEnv
senv  forall a b. (a -> b) -> a -> b
$  forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs      SInfo a
si
    , asserts :: [Triggered Expr]
F.asserts = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
x SymEnv
senv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
F.asserts SInfo a
si
    }


instance (Elaborate e) => (Elaborate (Triggered e)) where
  elaborate :: Located String -> SymEnv -> Triggered e -> Triggered e
elaborate Located String
x SymEnv
env Triggered e
t = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
x SymEnv
env) Triggered e
t

instance (Elaborate a) => (Elaborate (Maybe a)) where
  elaborate :: Located String -> SymEnv -> Maybe a -> Maybe a
elaborate Located String
x SymEnv
env Maybe a
t = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
x SymEnv
env) Maybe a
t

instance Elaborate Sort where
  elaborate :: Located String -> SymEnv -> Sort -> Sort
elaborate Located String
_ SymEnv
_ = Sort -> Sort
go
   where
      go :: Sort -> Sort
go Sort
s | Sort -> Bool
isString Sort
s = Sort
strSort
      go (FAbs Int
i Sort
s)    = Int -> Sort -> Sort
FAbs Int
i   (Sort -> Sort
go Sort
s)
      go (FFunc Sort
s1 Sort
s2) = Sort -> Sort -> Sort
funSort (Sort -> Sort
go Sort
s1) (Sort -> Sort
go Sort
s2)
      go (FApp Sort
s1 Sort
s2)  = Sort -> Sort -> Sort
FApp    (Sort -> Sort
go Sort
s1) (Sort -> Sort
go Sort
s2)
      go Sort
s             = Sort
s
      funSort :: Sort -> Sort -> Sort
      funSort :: Sort -> Sort -> Sort
funSort = Sort -> Sort -> Sort
FApp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort -> Sort
FApp Sort
funcSort

instance Elaborate AxiomEnv where
  elaborate :: Located String -> SymEnv -> AxiomEnv -> AxiomEnv
elaborate Located String
msg SymEnv
env AxiomEnv
ae = AxiomEnv
ae
    { aenvEqs :: [Equation]
aenvEqs   = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
msg SymEnv
env (AxiomEnv -> [Equation]
aenvEqs AxiomEnv
ae)
    -- MISSING SORTS OOPS, aenvSimpl = elaborate msg env (aenvSimpl ae)
    }

instance Elaborate Rewrite where
  elaborate :: Located String -> SymEnv -> Rewrite -> Rewrite
elaborate Located String
msg SymEnv
env Rewrite
rw = Rewrite
rw { smBody :: Expr
smBody = Located String -> SymEnv -> Expr -> Expr
skipElabExpr Located String
msg SymEnv
env' (Rewrite -> Expr
smBody Rewrite
rw) }
    where
      env' :: SymEnv
env' = SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv SymEnv
env forall a. HasCallStack => a
undefined

instance Elaborate Equation where
  elaborate :: Located String -> SymEnv -> Equation -> Equation
elaborate Located String
msg SymEnv
env Equation
eq = Equation
eq { eqBody :: Expr
eqBody = Located String -> SymEnv -> Expr -> Expr
skipElabExpr Located String
msg SymEnv
env' (Equation -> Expr
eqBody Equation
eq) }
    where
      env' :: SymEnv
env' = SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv SymEnv
env (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq)

instance Elaborate Expr where
  elaborate :: Located String -> SymEnv -> Expr -> Expr
elaborate Located String
msg SymEnv
env = Expr -> Expr
elabNumeric forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Expr -> Expr
elabApply SymEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located String -> SymEnv -> Expr -> Expr
elabExpr Located String
msg SymEnv
env


skipElabExpr :: Located String -> SymEnv -> Expr -> Expr
skipElabExpr :: Located String -> SymEnv -> Expr -> Expr
skipElabExpr Located String
msg SymEnv
env Expr
e = case Located String -> SymEnv -> Expr -> Either Error Expr
elabExprE Located String
msg SymEnv
env Expr
e of
  Left Error
_   -> Expr
e
  Right Expr
e' ->  Expr -> Expr
elabNumeric forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Expr -> Expr
elabApply SymEnv
env forall a b. (a -> b) -> a -> b
$ Expr
e'

instance Elaborate (Symbol, Sort) where
  elaborate :: Located String -> SymEnv -> (Symbol, Sort) -> (Symbol, Sort)
elaborate Located String
msg SymEnv
env (Symbol
x, Sort
s) = (Symbol
x, forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
msg SymEnv
env Sort
s)

instance Elaborate a => Elaborate [a]  where
  elaborate :: Located String -> SymEnv -> [a] -> [a]
elaborate Located String
msg SymEnv
env [a]
xs = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
msg SymEnv
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs

elabNumeric :: Expr -> Expr
elabNumeric :: Expr -> Expr
elabNumeric = (Expr -> Expr) -> Expr -> Expr
Vis.mapExprOnExpr Expr -> Expr
go
  where
    go :: Expr -> Expr
go (ETimes Expr
e1 Expr
e2)
      | String -> Expr -> Sort
exprSort String
"txn1" Expr
e1 forall a. Eq a => a -> a -> Bool
== Sort
FReal
      , String -> Expr -> Sort
exprSort String
"txn2" Expr
e2 forall a. Eq a => a -> a -> Bool
== Sort
FReal
      = Expr -> Expr -> Expr
ERTimes Expr
e1 Expr
e2
    go (EDiv   Expr
e1 Expr
e2)
      | String -> Expr -> Sort
exprSort (String
"txn3: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e1) Expr
e1 forall a. Eq a => a -> a -> Bool
== Sort
FReal
      , String -> Expr -> Sort
exprSort String
"txn4" Expr
e2 forall a. Eq a => a -> a -> Bool
== Sort
FReal
      = Expr -> Expr -> Expr
ERDiv   Expr
e1 Expr
e2
    go Expr
e
      = Expr
e

instance Elaborate SortedReft where
  elaborate :: Located String -> SymEnv -> SortedReft -> SortedReft
elaborate Located String
x SymEnv
env (RR Sort
s (Reft (Symbol
v, Expr
e))) = Sort -> Reft -> SortedReft
RR Sort
s ((Symbol, Expr) -> Reft
Reft (Symbol
v, Expr
e'))
    where
      e' :: Expr
e'   = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
x SymEnv
env' Expr
e
      env' :: SymEnv
env' = Symbol -> Sort -> SymEnv -> SymEnv
insertSymEnv Symbol
v Sort
s SymEnv
env

instance (Loc a) => Elaborate (BindEnv a) where
  elaborate :: Located String -> SymEnv -> BindEnv a -> BindEnv a
elaborate Located String
msg SymEnv
env = forall a.
(Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> BindEnv a -> BindEnv a
mapBindEnv (\Int
i (Symbol
x, SortedReft
sr, a
l) -> (Symbol
x, forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (forall {l} {a} {a} {a}.
(Loc l, Show a, Show a, Show a) =>
l -> a -> a -> a -> Located String
msg' a
l Int
i Symbol
x SortedReft
sr) SymEnv
env SortedReft
sr, a
l))
    where
      msg' :: l -> a -> a -> a -> Located String
msg' l
l a
i a
x a
sr = forall l b. Loc l => l -> b -> Located b
atLoc l
l (forall a. Located a -> a
val Located String
msg forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String
" elabBE",  forall a. Show a => a -> String
show a
i, forall a. Show a => a -> String
show a
x, forall a. Show a => a -> String
show a
sr])

instance (Loc a) => Elaborate (SimpC a) where
  elaborate :: Located String -> SymEnv -> SimpC a -> SimpC a
elaborate Located String
msg SymEnv
env SimpC a
c = SimpC a
c {_crhs :: Expr
_crhs = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
msg' SymEnv
env (forall a. SimpC a -> Expr
_crhs SimpC a
c) }
    where msg' :: Located String
msg'        = forall l b. Loc l => l -> b -> Located b
atLoc SimpC a
c (forall a. Located a -> a
val Located String
msg)

--------------------------------------------------------------------------------
-- | 'elabExpr' adds "casts" to decorate polymorphic instantiation sites.
--------------------------------------------------------------------------------
elabExpr :: Located String -> SymEnv -> Expr -> Expr
elabExpr :: Located String -> SymEnv -> Expr -> Expr
elabExpr Located String
msg SymEnv
env Expr
e = case Located String -> SymEnv -> Expr -> Either Error Expr
elabExprE Located String
msg SymEnv
env Expr
e of
  Left Error
ex  -> forall a. Error -> a
die Error
ex
  Right Expr
e' -> forall a. PPrint a => String -> a -> a
F.notracepp (String
"elabExp " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e) Expr
e'

elabExprE :: Located String -> SymEnv -> Expr -> Either Error Expr
elabExprE :: Located String -> SymEnv -> Expr -> Either Error Expr
elabExprE Located String
msg SymEnv
env Expr
e =
  case forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 (forall a. Loc a => a -> SrcSpan
srcSpan Located String
msg) (ElabEnv -> Expr -> CheckM (Expr, Sort)
elab (SymEnv
env, Symbol -> SESearch Sort
envLookup) Expr
e) of
    Left (ChError () -> Located String
f') ->
      let e' :: Located String
e' = () -> Located String
f' ()
       in forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err (forall a. Loc a => a -> SrcSpan
srcSpan Located String
e') (String -> Doc
d (forall a. Located a -> a
val Located String
e'))
    Right (Expr, Sort)
s  -> forall a b. b -> Either a b
Right (forall a b. (a, b) -> a
fst (Expr, Sort)
s)
  where
    sEnv :: SEnv Sort
sEnv = SymEnv -> SEnv Sort
seSort SymEnv
env
    envLookup :: Symbol -> SESearch Sort
envLookup = (forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
sEnv)
    d :: String -> Doc
d String
m  = [Doc] -> Doc
vcat [ Doc
"elaborate" Doc -> Doc -> Doc
<+> String -> Doc
text (forall a. Located a -> a
val Located String
msg) Doc -> Doc -> Doc
<+> Doc
"failed on:"
                , Int -> Doc -> Doc
nest Int
4 (forall a. PPrint a => a -> Doc
pprint Expr
e)
                , Doc
"with error"
                , Int -> Doc -> Doc
nest Int
4 (String -> Doc
text String
m)
                , Doc
"in environment"
                , Int -> Doc -> Doc
nest Int
4 (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall e a. Subable e => SEnv a -> e -> SEnv a
subEnv SEnv Sort
sEnv Expr
e)
                ]

--------------------------------------------------------------------------------
-- | 'elabApply' replaces all direct function calls indirect calls via `apply`
--------------------------------------------------------------------------------
elabApply :: SymEnv -> Expr -> Expr
elabApply :: SymEnv -> Expr -> Expr
elabApply SymEnv
env = Expr -> Expr
go
  where
    go :: Expr -> Expr
go Expr
e                  = case Expr -> (Expr, [(Expr, Sort)])
splitArgs Expr
e of
                             (Expr
e', []) -> Expr -> Expr
step Expr
e'
                             (Expr
f , [(Expr, Sort)]
es) -> SymEnv -> Expr -> [(Expr, Sort)] -> Expr
defuncEApp SymEnv
env (Expr -> Expr
go Expr
f) (forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst Expr -> Expr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Expr, Sort)]
es)
    step :: Expr -> Expr
step (PAnd [])        = Expr
PTrue
    step (POr [])         = Expr
PFalse
    step (ENeg Expr
e)         = Expr -> Expr
ENeg (Expr -> Expr
go  Expr
e)
    step (EBin Bop
o Expr
e1 Expr
e2)   = Bop -> Expr -> Expr -> Expr
EBin Bop
o (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    step (EIte Expr
e1 Expr
e2 Expr
e3)  = Expr -> Expr -> Expr -> Expr
EIte (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2) (Expr -> Expr
go Expr
e3)
    step (ECst Expr
e Sort
t)       = Expr -> Sort -> Expr
ECst (Expr -> Expr
go Expr
e) Sort
t
    step (PAnd [Expr]
ps)        = [Expr] -> Expr
PAnd (Expr -> Expr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ps)
    step (POr [Expr]
ps)         = [Expr] -> Expr
POr  (Expr -> Expr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ps)
    step (PNot Expr
p)         = Expr -> Expr
PNot (Expr -> Expr
go Expr
p)
    step (PImp Expr
p Expr
q)       = Expr -> Expr -> Expr
PImp (Expr -> Expr
go Expr
p) (Expr -> Expr
go Expr
q)
    step (PIff Expr
p Expr
q)       = Expr -> Expr -> Expr
PIff (Expr -> Expr
go Expr
p) (Expr -> Expr
go Expr
q)
    step (PExist [(Symbol, Sort)]
bs Expr
p)    = [(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
bs (Expr -> Expr
go Expr
p)
    step (PAll   [(Symbol, Sort)]
bs Expr
p)    = [(Symbol, Sort)] -> Expr -> Expr
PAll   [(Symbol, Sort)]
bs (Expr -> Expr
go Expr
p)
    step (PAtom Brel
r Expr
e1 Expr
e2)  = Brel -> Expr -> Expr -> Expr
PAtom Brel
r (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    step e :: Expr
e@EApp {}        = Expr -> Expr
go Expr
e
    step (ELam (Symbol, Sort)
b Expr
e)       = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol, Sort)
b       (Expr -> Expr
go Expr
e)
    step (ECoerc Sort
a Sort
t Expr
e)   = Sort -> Sort -> Expr -> Expr
ECoerc Sort
a Sort
t   (Expr -> Expr
go Expr
e)
    step (PGrad KVar
k Subst
su GradInfo
i Expr
e) = KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
su GradInfo
i (Expr -> Expr
go Expr
e)
    step e :: Expr
e@PKVar{}        = Expr
e
    step e :: Expr
e@ESym{}         = Expr
e
    step e :: Expr
e@ECon{}         = Expr
e
    step e :: Expr
e@EVar{}         = Expr
e
    -- ETApp, ETAbs, PAll, PExist
    step Expr
e                = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"TODO elabApply: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e

--------------------------------------------------------------------------------
-- | Sort Inference ------------------------------------------------------------
--------------------------------------------------------------------------------
sortExpr :: SrcSpan -> SEnv Sort -> Expr -> Sort
sortExpr :: SrcSpan -> SEnv Sort -> Expr -> Sort
sortExpr SrcSpan
l SEnv Sort
γ Expr
e = case forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
l ((Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e) of
    Left (ChError () -> Located String
f') -> forall a. Error -> a
die forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
l (String -> Doc
d (forall a. Located a -> a
val (() -> Located String
f' ())))
    Right Sort
s -> Sort
s
  where
    f :: Symbol -> SESearch Sort
f   = (forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
γ)
    d :: String -> Doc
d String
m = [Doc] -> Doc
vcat [ Doc
"sortExpr failed on expression:"
               , Int -> Doc -> Doc
nest Int
4 (forall a. PPrint a => a -> Doc
pprint Expr
e)
               , Doc
"with error:"
               , Int -> Doc -> Doc
nest Int
4 (String -> Doc
text String
m)
               , Doc
"in environment"
               , Int -> Doc -> Doc
nest Int
4 (forall a. PPrint a => a -> Doc
pprint SEnv Sort
γ)
               ]

checkSortExpr :: SrcSpan -> SEnv Sort -> Expr -> Maybe Sort
checkSortExpr :: SrcSpan -> SEnv Sort -> Expr -> Maybe Sort
checkSortExpr SrcSpan
sp SEnv Sort
γ Expr
e = case forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp ((Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e) of
    Left ChError
_   -> forall a. Maybe a
Nothing
    Right Sort
s  -> forall a. a -> Maybe a
Just Sort
s
  where
    f :: Symbol -> SESearch Sort
f Symbol
x  = case forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
γ of
            Just Sort
z  -> forall a. a -> SESearch a
Found Sort
z
            Maybe Sort
Nothing -> forall a. [Symbol] -> SESearch a
Alts []

subEnv :: (Subable e) => SEnv a -> e -> SEnv a
subEnv :: forall e a. Subable e => SEnv a -> e -> SEnv a
subEnv SEnv a
g e
e = forall v1 v2 a. (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a
intersectWithSEnv forall a b. a -> b -> a
const SEnv a
g SEnv ()
g'
  where
    g' :: SEnv ()
g' = forall a. [(Symbol, a)] -> SEnv a
fromListSEnv forall a b. (a -> b) -> a -> b
$ (, ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Subable a => a -> [Symbol]
syms e
e


--------------------------------------------------------------------------------
-- | Checking Refinements ------------------------------------------------------
--------------------------------------------------------------------------------

-- | Types used throughout checker
type CheckM = ReaderT ChState IO

-- We guard errors with a lambda to prevent accidental eager
-- evaluation of the payload. This module is using -XStrict.
-- See also Note [Lazy error messages].
newtype ChError  = ChError (() -> Located String)

instance Show ChError where
  show :: ChError -> String
show (ChError () -> Located String
f) = forall a. Show a => a -> String
show (() -> Located String
f ())
instance Exception ChError where

data ChState = ChS { ChState -> IORef Int
chCount :: IORef Int, ChState -> SrcSpan
chSpan :: SrcSpan }

type Env      = Symbol -> SESearch Sort
type ElabEnv  = (SymEnv, Env)


--------------------------------------------------------------------------------
mkSearchEnv :: SEnv a -> Symbol -> SESearch a
--------------------------------------------------------------------------------
mkSearchEnv :: forall a. SEnv a -> Symbol -> SESearch a
mkSearchEnv SEnv a
env Symbol
x = forall a. Symbol -> SEnv a -> SESearch a
lookupSEnvWithDistance Symbol
x SEnv a
env

-- withError :: CheckM a -> ChError -> CheckM a
-- act `withError` e' = act `catchError` (\e -> throwError (atLoc e (val e ++ "\n  because\n" ++ val e')))

withError :: HasCallStack => CheckM a -> String -> CheckM a
CheckM a
act withError :: forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` String
msg = do
  ChState
r <- forall r (m :: * -> *). MonadReader r m => m r
ask
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT CheckM a
act ChState
r forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch`
    (\(ChError () -> Located String
f) ->
      forall e a. Exception e => e -> IO a
throwIO forall a b. (a -> b) -> a -> b
$ (() -> Located String) -> ChError
ChError forall a b. (a -> b) -> a -> b
$ \()
_ ->
        let e :: Located String
e = () -> Located String
f ()
         in forall l b. Loc l => l -> b -> Located b
atLoc Located String
e (forall a. Located a -> a
val Located String
e forall a. [a] -> [a] -> [a]
++ String
"\n  because\n" forall a. [a] -> [a] -> [a]
++ String
msg)
    )

-- XXX: Why start at 42?
{-# NOINLINE varCounterRef #-}
varCounterRef :: IORef Int
varCounterRef :: IORef Int
varCounterRef = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef Int
42

-- XXX: Since 'varCounterRef' was made global, this
-- function is not referentially transparent.
-- Each evaluation of the function starts with a different
-- value of counter.
runCM0 :: SrcSpan -> CheckM a -> Either ChError a
runCM0 :: forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp CheckM a
act = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
  forall e a. Exception e => IO a -> IO (Either e a)
try (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT CheckM a
act (IORef Int -> SrcSpan -> ChState
ChS IORef Int
varCounterRef SrcSpan
sp))

fresh :: CheckM Int
fresh :: CheckM Int
fresh = do
  IORef Int
rn <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> IORef Int
chCount
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef Int
rn forall a b. (a -> b) -> a -> b
$ \Int
n -> (Int
nforall a. Num a => a -> a -> a
+Int
1, Int
n)

--------------------------------------------------------------------------------
-- | Checking Refinements ------------------------------------------------------
--------------------------------------------------------------------------------
checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc
checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc
checkSortedReft SEnv SortedReft
env [Symbol]
xs SortedReft
sr = forall b a. b -> ([a] -> b) -> [a] -> b
applyNonNull forall a. Maybe a
Nothing [Symbol] -> Maybe Doc
oops [Symbol]
unknowns
  where
    oops :: [Symbol] -> Maybe Doc
oops                  = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc
text String
"Unknown symbols:" Doc -> Doc -> Doc
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fixpoint a => a -> Doc
toFix
    unknowns :: [Symbol]
unknowns              = [ Symbol
x | Symbol
x <- forall a. Subable a => a -> [Symbol]
syms SortedReft
sr, Symbol
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Symbol
v forall a. a -> [a] -> [a]
: [Symbol]
xs, Bool -> Bool
not (Symbol
x forall a. Symbol -> SEnv a -> Bool
`memberSEnv` SEnv SortedReft
env)]
    Reft (Symbol
v,Expr
_)            = SortedReft -> Reft
sr_reft SortedReft
sr

checkSortedReftFull :: Checkable a => SrcSpan -> SEnv SortedReft -> a -> Maybe Doc
checkSortedReftFull :: forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> a -> Maybe Doc
checkSortedReftFull SrcSpan
sp SEnv SortedReft
γ a
t =
  case forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp (forall a. Checkable a => SEnv Sort -> a -> CheckM ()
check SEnv Sort
γ' a
t) of
    Left (ChError () -> Located String
f)  -> forall a. a -> Maybe a
Just (String -> Doc
text (forall a. Located a -> a
val (() -> Located String
f ())))
    Right ()
_ -> forall a. Maybe a
Nothing
  where
    γ' :: SEnv Sort
γ' = SortedReft -> Sort
sr_sort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEnv SortedReft
γ

checkSortFull :: Checkable a => SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
checkSortFull :: forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
checkSortFull SrcSpan
sp SEnv SortedReft
γ Sort
s a
t =
  case forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp (forall a. Checkable a => SEnv Sort -> Sort -> a -> CheckM ()
checkSort SEnv Sort
γ' Sort
s a
t) of
    Left (ChError () -> Located String
f)  -> forall a. a -> Maybe a
Just (String -> Doc
text (forall a. Located a -> a
val (() -> Located String
f ())))
    Right ()
_ -> forall a. Maybe a
Nothing
  where
      γ' :: SEnv Sort
γ' = SortedReft -> Sort
sr_sort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEnv SortedReft
γ

checkSorted :: Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
checkSorted :: forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
checkSorted SrcSpan
sp SEnv Sort
γ a
t =
  case forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp (forall a. Checkable a => SEnv Sort -> a -> CheckM ()
check SEnv Sort
γ a
t) of
    Left (ChError () -> Located String
f)  -> forall a. a -> Maybe a
Just (String -> Doc
text (forall a. Located a -> a
val (() -> Located String
f ())))
    Right ()
_  -> forall a. Maybe a
Nothing

pruneUnsortedReft :: SEnv Sort -> Templates -> SortedReft -> SortedReft
pruneUnsortedReft :: SEnv Sort -> Templates -> SortedReft -> SortedReft
pruneUnsortedReft SEnv Sort
_ Templates
t SortedReft
r
  | Templates -> Bool
isEmptyTemplates Templates
t
  = SortedReft
r
pruneUnsortedReft SEnv Sort
γ Templates
t (RR Sort
s (Reft (Symbol
v, Expr
p)))
  | Templates -> Bool
isAnyTemplates Templates
t
  -- this is the old code that checks everything
  = Sort -> Reft -> SortedReft
RR Sort
s ((Symbol, Expr) -> Reft
Reft (Symbol
v, ([Expr] -> [Expr]) -> Expr -> Expr
tx [Expr] -> [Expr]
filterAny Expr
p))
  | Bool
otherwise
  = Sort -> Reft -> SortedReft
RR Sort
s ((Symbol, Expr) -> Reft
Reft (Symbol
v, ([Expr] -> [Expr]) -> Expr -> Expr
tx (forall a. (a -> Bool) -> [a] -> [a]
filter Expr -> Bool
filterWithTemplate) Expr
p))
  where
    filterAny :: [Expr] -> [Expr]
filterAny = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Symbol -> SESearch Sort) -> Expr -> Maybe Expr
checkPred' Symbol -> SESearch Sort
f)
    filterWithTemplate :: Expr -> Bool
filterWithTemplate Expr
e =  Bool -> Bool
not (Templates -> Expr -> Bool
matchesTemplates Templates
t Expr
e) Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
isJust ((Symbol -> SESearch Sort) -> Expr -> Maybe Expr
checkPred' Symbol -> SESearch Sort
f Expr
e)
    tx :: ([Expr] -> [Expr]) -> Expr -> Expr
tx [Expr] -> [Expr]
f' = [Expr] -> Expr
pAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
f' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
conjuncts
    f :: Symbol -> SESearch Sort
f    = (forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
γ')
    γ' :: SEnv Sort
γ'   = forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
v Sort
s SEnv Sort
γ
    -- wmsg t r = "WARNING: prune unsorted reft:\n" ++ showFix r ++ "\n" ++ t

checkPred' :: Env -> Expr -> Maybe Expr
checkPred' :: (Symbol -> SESearch Sort) -> Expr -> Maybe Expr
checkPred' Symbol -> SESearch Sort
f Expr
p = Maybe Expr
res -- traceFix ("checkPred: p = " ++ showFix p) $ res
  where
    res :: Maybe Expr
res        = case forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
dummySpan ((Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f Expr
p) of
                   Left ChError
_err -> forall a. PPrint a => String -> a -> a
notracepp (String
"Removing" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
p) forall a. Maybe a
Nothing
                   Right ()
_   -> forall a. a -> Maybe a
Just Expr
p

class Checkable a where
  check     :: SEnv Sort -> a -> CheckM ()
  checkSort :: SEnv Sort -> Sort -> a -> CheckM ()

  checkSort SEnv Sort
γ Sort
_ = forall a. Checkable a => SEnv Sort -> a -> CheckM ()
check SEnv Sort
γ

instance Checkable Expr where
  check :: SEnv Sort -> Expr -> CheckM ()
check SEnv Sort
γ Expr
e = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e
   where f :: Symbol -> SESearch Sort
f =  (forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
γ)

  checkSort :: SEnv Sort -> Sort -> Expr -> CheckM ()
checkSort SEnv Sort
γ Sort
s Expr
e = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f (Expr -> Sort -> Expr
ECst Expr
e Sort
s)
    where
      f :: Symbol -> SESearch Sort
f           =  (forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
γ)

instance Checkable SortedReft where
  check :: SEnv Sort -> SortedReft -> CheckM ()
check SEnv Sort
γ (RR Sort
s (Reft (Symbol
v, Expr
ra))) = forall a. Checkable a => SEnv Sort -> a -> CheckM ()
check SEnv Sort
γ' Expr
ra
   where
     γ' :: SEnv Sort
γ' = forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
v Sort
s SEnv Sort
γ

--------------------------------------------------------------------------------
-- | Checking Expressions ------------------------------------------------------
--------------------------------------------------------------------------------
checkExpr                  :: Env -> Expr -> CheckM Sort
checkExpr :: (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
_ (ESym SymConst
_)       = forall (m :: * -> *) a. Monad m => a -> m a
return Sort
strSort
checkExpr Symbol -> SESearch Sort
_ (ECon (I SubcId
_))   = forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FInt
checkExpr Symbol -> SESearch Sort
_ (ECon (R Double
_))   = forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FReal
checkExpr Symbol -> SESearch Sort
_ (ECon (L Text
_ Sort
s)) = forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
checkExpr Symbol -> SESearch Sort
f (EVar Symbol
x)       = (Symbol -> SESearch Sort) -> Symbol -> CheckM Sort
checkSym Symbol -> SESearch Sort
f Symbol
x
checkExpr Symbol -> SESearch Sort
f (ENeg Expr
e)       = (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkNeg Symbol -> SESearch Sort
f Expr
e
checkExpr Symbol -> SESearch Sort
f (EBin Bop
o Expr
e1 Expr
e2) = (Symbol -> SESearch Sort) -> Expr -> Bop -> Expr -> CheckM Sort
checkOp Symbol -> SESearch Sort
f Expr
e1 Bop
o Expr
e2
checkExpr Symbol -> SESearch Sort
f (EIte Expr
p Expr
e1 Expr
e2) = (Symbol -> SESearch Sort) -> Expr -> Expr -> Expr -> CheckM Sort
checkIte Symbol -> SESearch Sort
f Expr
p Expr
e1 Expr
e2
checkExpr Symbol -> SESearch Sort
f (ECst Expr
e Sort
t)     = (Symbol -> SESearch Sort) -> Sort -> Expr -> CheckM Sort
checkCst Symbol -> SESearch Sort
f Sort
t Expr
e
checkExpr Symbol -> SESearch Sort
f (EApp Expr
g Expr
e)     = (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> CheckM Sort
checkApp Symbol -> SESearch Sort
f forall a. Maybe a
Nothing Expr
g Expr
e
checkExpr Symbol -> SESearch Sort
f (PNot Expr
p)       = (Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f Expr
p forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (PImp Expr
p Expr
p')    = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f) [Expr
p, Expr
p'] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (PIff Expr
p Expr
p')    = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f) [Expr
p, Expr
p'] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (PAnd [Expr]
ps)      = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f) [Expr]
ps forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (POr [Expr]
ps)       = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f) [Expr]
ps forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (PAtom Brel
r Expr
e Expr
e') = HasCallStack =>
(Symbol -> SESearch Sort) -> Brel -> Expr -> Expr -> CheckM ()
checkRel Symbol -> SESearch Sort
f Brel
r Expr
e Expr
e' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
_ PKVar{}        = forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (PGrad KVar
_ Subst
_ GradInfo
_ Expr
e)  = (Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f Expr
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort

checkExpr Symbol -> SESearch Sort
f (PAll  [(Symbol, Sort)]
bs Expr
e )  = (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr (forall a b.
Eq a =>
(a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv Symbol -> SESearch Sort
f [(Symbol, Sort)]
bs) Expr
e
checkExpr Symbol -> SESearch Sort
f (PExist [(Symbol, Sort)]
bs Expr
e)  = (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr (forall a b.
Eq a =>
(a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv Symbol -> SESearch Sort
f [(Symbol, Sort)]
bs) Expr
e
checkExpr Symbol -> SESearch Sort
f (ELam (Symbol
x,Sort
t) Expr
e) = Sort -> Sort -> Sort
FFunc Sort
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr (forall a b.
Eq a =>
(a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv Symbol -> SESearch Sort
f [(Symbol
x,Sort
t)]) Expr
e
checkExpr Symbol -> SESearch Sort
f (ECoerc Sort
s Sort
t Expr
e) = (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f (Expr -> Sort -> Expr
ECst Expr
e Sort
s) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
t
checkExpr Symbol -> SESearch Sort
_ (ETApp Expr
_ Sort
_)    = forall a. HasCallStack => String -> a
error String
"SortCheck.checkExpr: TODO: implement ETApp"
checkExpr Symbol -> SESearch Sort
_ (ETAbs Expr
_ Symbol
_)    = forall a. HasCallStack => String -> a
error String
"SortCheck.checkExpr: TODO: implement ETAbs"

addEnv :: Eq a => (a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv :: forall a b.
Eq a =>
(a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv a -> SESearch b
f [(a, b)]
bs a
x
  = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup a
x [(a, b)]
bs of
      Just b
s  -> forall a. a -> SESearch a
Found b
s
      Maybe b
Nothing -> a -> SESearch b
f a
x

--------------------------------------------------------------------------------
-- | Elaborate expressions with types to make polymorphic instantiation explicit.
--------------------------------------------------------------------------------
{-# SCC elab #-}
elab :: ElabEnv -> Expr -> CheckM (Expr, Sort)
--------------------------------------------------------------------------------
elab :: ElabEnv -> Expr -> CheckM (Expr, Sort)
elab f :: ElabEnv
f@(SymEnv
_, Symbol -> SESearch Sort
g) e :: Expr
e@(EBin Bop
o Expr
e1 Expr
e2) = do
  (Expr
e1', Sort
s1) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  (Expr
e2', Sort
s2) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  Sort
s <- (Symbol -> SESearch Sort) -> Expr -> Sort -> Sort -> CheckM Sort
checkOpTy Symbol -> SESearch Sort
g Expr
e Sort
s1 Sort
s2
  forall (m :: * -> *) a. Monad m => a -> m a
return (Bop -> Expr -> Expr -> Expr
EBin Bop
o (Expr -> Sort -> Expr
eCst Expr
e1' Sort
s1) (Expr -> Sort -> Expr
eCst Expr
e2' Sort
s2), Sort
s)

elab ElabEnv
f (EApp e1 :: Expr
e1@(EApp Expr
_ Expr
_) Expr
e2) = do
  (Expr
e1', Sort
_, Expr
e2', Sort
s2, Sort
s) <- forall a. PPrint a => String -> a -> a
notracepp String
"ELAB-EAPP" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv
-> Expr
-> Expr
-> ReaderT ChState IO (Expr, Sort, Expr, Sort, Sort)
elabEApp ElabEnv
f Expr
e1 Expr
e2
  let e :: Expr
e = Sort -> Expr -> Expr -> Expr
eAppC Sort
s Expr
e1' (Expr -> Sort -> Expr
eCst Expr
e2' Sort
s2)
  let θ :: Maybe TVSubst
θ = (Symbol -> SESearch Sort) -> Expr -> Maybe TVSubst
unifyExpr (forall a b. (a, b) -> b
snd ElabEnv
f) Expr
e
  forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TVSubst -> Expr -> Expr
applyExpr Maybe TVSubst
θ Expr
e, forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
s (TVSubst -> Sort -> Sort
`apply` Sort
s) Maybe TVSubst
θ)

elab ElabEnv
f (EApp Expr
e1 Expr
e2) = do
  (Expr
e1', Sort
s1, Expr
e2', Sort
s2, Sort
s) <- ElabEnv
-> Expr
-> Expr
-> ReaderT ChState IO (Expr, Sort, Expr, Sort, Sort)
elabEApp ElabEnv
f Expr
e1 Expr
e2
  let e :: Expr
e = Sort -> Expr -> Expr -> Expr
eAppC Sort
s (Expr -> Sort -> Expr
eCst Expr
e1' Sort
s1) (Expr -> Sort -> Expr
eCst Expr
e2' Sort
s2)
  let θ :: Maybe TVSubst
θ = (Symbol -> SESearch Sort) -> Expr -> Maybe TVSubst
unifyExpr (forall a b. (a, b) -> b
snd ElabEnv
f) Expr
e
  forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TVSubst -> Expr -> Expr
applyExpr Maybe TVSubst
θ Expr
e, forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
s (TVSubst -> Sort -> Sort
`apply` Sort
s) Maybe TVSubst
θ)

elab ElabEnv
_ e :: Expr
e@(ESym SymConst
_) =
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
strSort)

elab ElabEnv
_ e :: Expr
e@(ECon (I SubcId
_)) =
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
FInt)

elab ElabEnv
_ e :: Expr
e@(ECon (R Double
_)) =
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
FReal)

elab ElabEnv
_ e :: Expr
e@(ECon (L Text
_ Sort
s)) =
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
s)

elab ElabEnv
_ e :: Expr
e@(PKVar KVar
_ Subst
_) =
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
boolSort)

elab ElabEnv
f (PGrad KVar
k Subst
su GradInfo
i Expr
e) =
  (, Sort
boolSort) forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
su GradInfo
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e

elab (SymEnv
_, Symbol -> SESearch Sort
f) e :: Expr
e@(EVar Symbol
x) =
  (Expr
e,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> SESearch Sort) -> Symbol -> CheckM Sort
checkSym Symbol -> SESearch Sort
f Symbol
x

elab ElabEnv
f (ENeg Expr
e) = do
  (Expr
e', Sort
s) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
ENeg Expr
e', Sort
s)

elab f :: ElabEnv
f@(SymEnv
_,Symbol -> SESearch Sort
g) (ECst (EIte Expr
p Expr
e1 Expr
e2) Sort
t) = do
  (Expr
p', Sort
_)   <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
p
  (Expr
e1', Sort
s1) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f (Expr -> Sort -> Expr
eCst Expr
e1 Sort
t)
  (Expr
e2', Sort
s2) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f (Expr -> Sort -> Expr
eCst Expr
e2 Sort
t)
  Sort
s         <- (Symbol -> SESearch Sort)
-> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy Symbol -> SESearch Sort
g Expr
p Expr
e1' Expr
e2' Sort
s1 Sort
s2
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIte Expr
p' (Expr -> Sort -> Expr
eCst Expr
e1' Sort
s) (Expr -> Sort -> Expr
eCst Expr
e2' Sort
s), Sort
t)

elab f :: ElabEnv
f@(SymEnv
_,Symbol -> SESearch Sort
g) (EIte Expr
p Expr
e1 Expr
e2) = do
  Sort
t <- (Symbol -> SESearch Sort) -> Expr -> Expr -> CheckM Sort
getIte Symbol -> SESearch Sort
g Expr
e1 Expr
e2
  (Expr
p', Sort
_)   <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
p
  (Expr
e1', Sort
s1) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f (Expr -> Sort -> Expr
eCst Expr
e1 Sort
t)
  (Expr
e2', Sort
s2) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f (Expr -> Sort -> Expr
eCst Expr
e2 Sort
t)
  Sort
s         <- (Symbol -> SESearch Sort)
-> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy Symbol -> SESearch Sort
g Expr
p Expr
e1' Expr
e2' Sort
s1 Sort
s2
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIte Expr
p' (Expr -> Sort -> Expr
eCst Expr
e1' Sort
s) (Expr -> Sort -> Expr
eCst Expr
e2' Sort
s), Sort
s)

elab ElabEnv
f (ECst Expr
e Sort
t) = do
  (Expr
e', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Sort -> Expr
eCst Expr
e' Sort
t, Sort
t)

elab ElabEnv
f (PNot Expr
p) = do
  (Expr
e', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
p
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
PNot Expr
e', Sort
boolSort)

elab ElabEnv
f (PImp Expr
p1 Expr
p2) = do
  (Expr
p1', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
p1
  (Expr
p2', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
p2
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
PImp Expr
p1' Expr
p2', Sort
boolSort)

elab ElabEnv
f (PIff Expr
p1 Expr
p2) = do
  (Expr
p1', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
p1
  (Expr
p2', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
p2
  forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
PIff Expr
p1' Expr
p2', Sort
boolSort)

elab ElabEnv
f (PAnd [Expr]
ps) = do
  [(Expr, Sort)]
ps' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f) [Expr]
ps
  forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Expr
PAnd (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Expr, Sort)]
ps'), Sort
boolSort)

elab ElabEnv
f (POr [Expr]
ps) = do
  [(Expr, Sort)]
ps' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f) [Expr]
ps
  forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Expr
POr (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Expr, Sort)]
ps'), Sort
boolSort)

elab f :: ElabEnv
f@(SymEnv
_,Symbol -> SESearch Sort
g) e :: Expr
e@(PAtom Brel
eq Expr
e1 Expr
e2) | Brel
eq forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
eq forall a. Eq a => a -> a -> Bool
== Brel
Ne = do
  Sort
t1        <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
g Expr
e1
  Sort
t2        <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
g Expr
e2
  (Sort
t1',Sort
t2') <- (Symbol -> SESearch Sort)
-> Expr -> Sort -> Sort -> CheckM (Sort, Sort)
unite Symbol -> SESearch Sort
g Expr
e  Sort
t1 Sort
t2 forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Expr -> String
errElabExpr Expr
e
  Expr
e1'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
f Sort
t1' Expr
e1
  Expr
e2'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
f Sort
t2' Expr
e2
  Expr
e1''      <- ElabEnv -> Expr -> Sort -> CheckM Expr
eCstAtom ElabEnv
f Expr
e1' Sort
t1'
  Expr
e2''      <- ElabEnv -> Expr -> Sort -> CheckM Expr
eCstAtom ElabEnv
f Expr
e2' Sort
t2'
  forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
eq  Expr
e1'' Expr
e2'' , Sort
boolSort)

elab ElabEnv
f (PAtom Brel
r Expr
e1 Expr
e2)
  | Brel
r forall a. Eq a => a -> a -> Bool
== Brel
Ueq Bool -> Bool -> Bool
|| Brel
r forall a. Eq a => a -> a -> Bool
== Brel
Une = do
  (Expr
e1', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  (Expr
e2', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
r Expr
e1' Expr
e2', Sort
boolSort)

elab f :: ElabEnv
f@(SymEnv
env,Symbol -> SESearch Sort
_) (PAtom Brel
r Expr
e1 Expr
e2) = do
  Expr
e1' <- forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SymEnv -> Expr -> Sort -> Expr
toInt SymEnv
env) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  Expr
e2' <- forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SymEnv -> Expr -> Sort -> Expr
toInt SymEnv
env) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
r Expr
e1' Expr
e2', Sort
boolSort)

elab ElabEnv
f (PExist [(Symbol, Sort)]
bs Expr
e) = do
  (Expr
e', Sort
s) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab (forall a t b.
Eq a =>
(t, a -> SESearch b) -> [(a, b)] -> (t, a -> SESearch b)
elabAddEnv ElabEnv
f [(Symbol, Sort)]
bs) Expr
e
  let bs' :: [(Symbol, Sort)]
bs' = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
"PExist Args" forall a. Monoid a => a
mempty [(Symbol, Sort)]
bs
  forall (m :: * -> *) a. Monad m => a -> m a
return ([(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
bs' Expr
e', Sort
s)

elab ElabEnv
f (PAll [(Symbol, Sort)]
bs Expr
e) = do
  (Expr
e', Sort
s) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab (forall a t b.
Eq a =>
(t, a -> SESearch b) -> [(a, b)] -> (t, a -> SESearch b)
elabAddEnv ElabEnv
f [(Symbol, Sort)]
bs) Expr
e
  let bs' :: [(Symbol, Sort)]
bs' = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
"PAll Args" forall a. Monoid a => a
mempty [(Symbol, Sort)]
bs
  forall (m :: * -> *) a. Monad m => a -> m a
return ([(Symbol, Sort)] -> Expr -> Expr
PAll [(Symbol, Sort)]
bs' Expr
e', Sort
s)

elab ElabEnv
f (ELam (Symbol
x,Sort
t) Expr
e) = do
  (Expr
e', Sort
s) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab (forall a t b.
Eq a =>
(t, a -> SESearch b) -> [(a, b)] -> (t, a -> SESearch b)
elabAddEnv ElabEnv
f [(Symbol
x, Sort
t)]) Expr
e
  let t' :: Sort
t' = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
"ELam Arg" forall a. Monoid a => a
mempty Sort
t
  forall (m :: * -> *) a. Monad m => a -> m a
return ((Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
t') (Expr -> Sort -> Expr
eCst Expr
e' Sort
s), Sort -> Sort -> Sort
FFunc Sort
t Sort
s)

elab ElabEnv
f (ECoerc Sort
s Sort
t Expr
e) = do
  (Expr
e', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e
  forall (m :: * -> *) a. Monad m => a -> m a
return     (Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t Expr
e', Sort
t)

elab ElabEnv
_ (ETApp Expr
_ Sort
_) =
  forall a. HasCallStack => String -> a
error String
"SortCheck.elab: TODO: implement ETApp"
elab ElabEnv
_ (ETAbs Expr
_ Symbol
_) =
  forall a. HasCallStack => String -> a
error String
"SortCheck.elab: TODO: implement ETAbs"


-- | 'eCstAtom' is to support tests like `tests/pos/undef00.fq`
eCstAtom :: ElabEnv -> Expr -> Sort -> CheckM Expr
eCstAtom :: ElabEnv -> Expr -> Sort -> CheckM Expr
eCstAtom f :: ElabEnv
f@(SymEnv
sym,Symbol -> SESearch Sort
g) (EVar Symbol
x) Sort
t
  | Found Sort
s <- Symbol -> SESearch Sort
g Symbol
x
  , Sort -> Bool
isUndef Sort
s
  , Bool -> Bool
not (SymEnv -> Sort -> Bool
isInt SymEnv
sym Sort
t) = (Expr -> Sort -> Expr
`ECst` Sort
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
f Sort
t (Expr -> Expr -> Expr
EApp (forall a. Symbolic a => a -> Expr
eVar Symbol
tyCastName) (forall a. Symbolic a => a -> Expr
eVar Symbol
x))
eCstAtom ElabEnv
_ Expr
e Sort
t = forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Sort -> Expr
ECst Expr
e Sort
t)

isUndef :: Sort -> Bool
isUndef :: Sort -> Bool
isUndef Sort
s = case Sort -> ([Int], Sort)
bkAbs Sort
s of
  ([Int]
is, FVar Int
j) -> Int
j forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
is
  ([Int], Sort)
_            -> Bool
False


elabAddEnv :: Eq a => (t, a -> SESearch b) -> [(a, b)] -> (t, a -> SESearch b)
elabAddEnv :: forall a t b.
Eq a =>
(t, a -> SESearch b) -> [(a, b)] -> (t, a -> SESearch b)
elabAddEnv (t
g, a -> SESearch b
f) [(a, b)]
bs = (t
g, forall a b.
Eq a =>
(a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv a -> SESearch b
f [(a, b)]
bs)

elabAs :: ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs :: ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
f Sort
t Expr
e = forall a. PPrint a => String -> a -> a
notracepp String
_msg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> CheckM Expr
go Expr
e
  where
    _msg :: String
_msg  = String
"elabAs: t = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Sort
t forall a. [a] -> [a] -> [a]
++ String
" e = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e
    go :: Expr -> CheckM Expr
go (EApp Expr
e1 Expr
e2)   = ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
elabAppAs ElabEnv
f Sort
t Expr
e1 Expr
e2
    go Expr
e'              = forall a b. (a, b) -> a
fst    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e'

-- DUPLICATION with `checkApp'`
elabAppAs :: ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
elabAppAs :: ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
elabAppAs env :: ElabEnv
env@(SymEnv
_, Symbol -> SESearch Sort
f) Sort
t Expr
g Expr
e = do
  Sort
gT       <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
g
  Sort
eT       <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e
  (Sort
iT, Sort
oT, TVSubst
isu) <- Sort -> CheckM (Sort, Sort, TVSubst)
checkFunSort Sort
gT
  let ge :: Maybe Expr
ge    = forall a. a -> Maybe a
Just (Expr -> Expr -> Expr
EApp Expr
g Expr
e)
  TVSubst
su       <- HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
ge TVSubst
isu [Sort
oT, Sort
iT] [Sort
t, Sort
eT]
  let tg :: Sort
tg    = TVSubst -> Sort -> Sort
apply TVSubst
su Sort
gT
  Expr
g'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
env Sort
tg Expr
g
  let te :: Sort
te    = TVSubst -> Sort -> Sort
apply TVSubst
su Sort
eT
  Expr
e'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
env Sort
te Expr
e
  forall (m :: * -> *) a. Monad m => a -> m a
return    forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
EApp (Expr -> Sort -> Expr
ECst Expr
g' Sort
tg) (Expr -> Sort -> Expr
ECst Expr
e' Sort
te)

elabEApp  :: ElabEnv -> Expr -> Expr -> CheckM (Expr, Sort, Expr, Sort, Sort)
elabEApp :: ElabEnv
-> Expr
-> Expr
-> ReaderT ChState IO (Expr, Sort, Expr, Sort, Sort)
elabEApp f :: ElabEnv
f@(SymEnv
_, Symbol -> SESearch Sort
g) Expr
e1 Expr
e2 = do
  (Expr
e1', Sort
s1)     <- forall a. PPrint a => String -> a -> a
notracepp (String
"elabEApp1: e1 = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  (Expr
e2', Sort
s2)     <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  (Expr
e1'', Expr
e2'', Sort
s1', Sort
s2', Sort
s) <- (Symbol -> SESearch Sort)
-> Expr
-> Expr
-> Sort
-> Sort
-> CheckM (Expr, Expr, Sort, Sort, Sort)
elabAppSort Symbol -> SESearch Sort
g Expr
e1' Expr
e2' Sort
s1 Sort
s2
  forall (m :: * -> *) a. Monad m => a -> m a
return           (Expr
e1'', Sort
s1', Expr
e2'', Sort
s2', Sort
s)

elabAppSort :: Env -> Expr -> Expr -> Sort -> Sort -> CheckM (Expr, Expr, Sort, Sort, Sort)
elabAppSort :: (Symbol -> SESearch Sort)
-> Expr
-> Expr
-> Sort
-> Sort
-> CheckM (Expr, Expr, Sort, Sort, Sort)
elabAppSort Symbol -> SESearch Sort
f Expr
e1 Expr
e2 Sort
s1 Sort
s2 = do
  let e :: Maybe Expr
e            = forall a. a -> Maybe a
Just (Expr -> Expr -> Expr
EApp Expr
e1 Expr
e2)
  (Sort
sIn, Sort
sOut, TVSubst
su) <- Sort -> CheckM (Sort, Sort, TVSubst)
checkFunSort Sort
s1
  TVSubst
su'             <- (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst
unify1 Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
su Sort
sIn Sort
s2
  forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TVSubst -> Expr -> Expr
applyExpr (forall a. a -> Maybe a
Just TVSubst
su') Expr
e1, Maybe TVSubst -> Expr -> Expr
applyExpr (forall a. a -> Maybe a
Just TVSubst
su') Expr
e2, TVSubst -> Sort -> Sort
apply TVSubst
su' Sort
s1, TVSubst -> Sort -> Sort
apply TVSubst
su' Sort
s2, TVSubst -> Sort -> Sort
apply TVSubst
su' Sort
sOut)


--------------------------------------------------------------------------------
-- | defuncEApp monomorphizes function applications.
--------------------------------------------------------------------------------
defuncEApp :: SymEnv -> Expr -> [(Expr, Sort)] -> Expr
defuncEApp :: SymEnv -> Expr -> [(Expr, Sort)] -> Expr
defuncEApp SymEnv
_env Expr
e [] = Expr
e
defuncEApp SymEnv
env Expr
e [(Expr, Sort)]
es = Expr -> Sort -> Expr
eCst (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Expr -> (Expr, Sort) -> Expr
makeApplication Expr
e' [(Expr, Sort)]
es') (forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last [(Expr, Sort)]
es)
  where
    (Expr
e', [(Expr, Sort)]
es')       = forall a.
SEnv TheorySymbol -> Expr -> [(Expr, a)] -> (Expr, [(Expr, a)])
takeArgs (SymEnv -> SEnv TheorySymbol
seTheory SymEnv
env) Expr
e [(Expr, Sort)]
es

takeArgs :: SEnv TheorySymbol -> Expr -> [(Expr, a)] -> (Expr, [(Expr, a)])
takeArgs :: forall a.
SEnv TheorySymbol -> Expr -> [(Expr, a)] -> (Expr, [(Expr, a)])
takeArgs SEnv TheorySymbol
env Expr
e [(Expr, a)]
es =
  case SEnv TheorySymbol -> Expr -> Maybe Int
Thy.isSmt2App SEnv TheorySymbol
env Expr
e of
    Just Int
n  -> let ([(Expr, a)]
es1, [(Expr, a)]
es2) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [(Expr, a)]
es
               in (Expr -> [Expr] -> Expr
eApps Expr
e (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Expr, a)]
es1), [(Expr, a)]
es2)
    Maybe Int
Nothing -> (Expr
e, [(Expr, a)]
es)

-- 'e1' is the function, 'e2' is the argument, 's' is the OUTPUT TYPE
makeApplication :: Expr -> (Expr, Sort) -> Expr
makeApplication :: Expr -> (Expr, Sort) -> Expr
makeApplication Expr
e1 (Expr
e2, Sort
s) = Expr -> Sort -> Expr
ECst (Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr
EApp Expr
f Expr
e1) Expr
e2) Sort
s
  where
    f :: Expr
f                      = {- notracepp ("makeApplication: " ++ showpp (e2, t2)) $ -} Sort -> Sort -> Expr
applyAt Sort
t2 Sort
s
    t2 :: Sort
t2                     = String -> Expr -> Sort
exprSort String
"makeAppl" Expr
e2

applyAt :: Sort -> Sort -> Expr
applyAt :: Sort -> Sort -> Expr
applyAt Sort
s Sort
t = Expr -> Sort -> Expr
ECst (Symbol -> Expr
EVar Symbol
applyName) (Sort -> Sort -> Sort
FFunc Sort
s Sort
t)

-- JUST make "toInt" call "makeApplication" also, so they are wrapped in apply
-- MAY CAUSE CRASH (apply-on-apply) so rig `isSmt2App` to treat `apply` as SPECIAL.

-- TODO: proper toInt
toInt :: SymEnv -> Expr -> Sort -> Expr
toInt :: SymEnv -> Expr -> Sort -> Expr
toInt SymEnv
env Expr
e Sort
s
  | Bool
isSmtInt  = Expr
e
  | Bool
otherwise = Expr -> Sort -> Expr
ECst (Expr -> Expr -> Expr
EApp Expr
f (Expr -> Sort -> Expr
ECst Expr
e Sort
s)) Sort
FInt
  where
    isSmtInt :: Bool
isSmtInt  = SymEnv -> Sort -> Bool
isInt SymEnv
env Sort
s
    f :: Expr
f         = Sort -> Expr
toIntAt Sort
s

isInt :: SymEnv -> Sort -> Bool
isInt :: SymEnv -> Sort -> Bool
isInt SymEnv
env Sort
s = case Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False (SymEnv -> SEnv DataDecl
seData SymEnv
env) Sort
s of
  SmtSort
SInt    -> Bool
True
  SmtSort
SString -> Bool
True
  SmtSort
SReal   -> Bool
True
  SmtSort
_       -> Bool
False

toIntAt :: Sort -> Expr
toIntAt :: Sort -> Expr
toIntAt Sort
s = Expr -> Sort -> Expr
ECst (Symbol -> Expr
EVar Symbol
toIntName) (Sort -> Sort -> Sort
FFunc Sort
s Sort
FInt)

unElab :: Expr -> Expr
unElab :: Expr -> Expr
unElab = Expr -> Expr
Vis.stripCasts forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
unApply

unElabSortedReft :: SortedReft -> SortedReft
unElabSortedReft :: SortedReft -> SortedReft
unElabSortedReft SortedReft
sr = SortedReft
sr { sr_reft :: Reft
sr_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
unElab (SortedReft -> Reft
sr_reft SortedReft
sr) }

unApplySortedReft :: SortedReft -> SortedReft
unApplySortedReft :: SortedReft -> SortedReft
unApplySortedReft SortedReft
sr = SortedReft
sr { sr_reft :: Reft
sr_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
unApply (SortedReft -> Reft
sr_reft SortedReft
sr) }

unApply :: Expr -> Expr
unApply :: Expr -> Expr
unApply = (Expr -> Expr) -> Expr -> Expr
Vis.mapExprOnExpr Expr -> Expr
go
  where
    go :: Expr -> Expr
go (ECst (EApp (EApp Expr
f Expr
e1) Expr
e2) Sort
_)
      | Just Sort
_ <- Expr -> Maybe Sort
unApplyAt Expr
f = Expr -> Expr -> Expr
EApp Expr
e1 Expr
e2
    go (ELam (Symbol
x,Sort
s) Expr
e)         = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, (Sort -> Sort) -> Sort -> Sort
Vis.mapSort Sort -> Sort
go' Sort
s) Expr
e
    go Expr
e                      = Expr
e

    go' :: Sort -> Sort
go' (FApp (FApp Sort
fs Sort
t1) Sort
t2) | Sort
fs forall a. Eq a => a -> a -> Bool
== Sort
funcSort
          = Sort -> Sort -> Sort
FFunc Sort
t1 Sort
t2
    go' Sort
t = Sort
t


unApplyAt :: Expr -> Maybe Sort
unApplyAt :: Expr -> Maybe Sort
unApplyAt (ECst (EVar Symbol
f) t :: Sort
t@FFunc{})
  | Symbol
f forall a. Eq a => a -> a -> Bool
== Symbol
applyName = forall a. a -> Maybe a
Just Sort
t
unApplyAt Expr
_        = forall a. Maybe a
Nothing


splitArgs :: Expr -> (Expr, [(Expr, Sort)])
splitArgs :: Expr -> (Expr, [(Expr, Sort)])
splitArgs = [(Expr, Sort)] -> Expr -> (Expr, [(Expr, Sort)])
go []
  where
    go :: [(Expr, Sort)] -> Expr -> (Expr, [(Expr, Sort)])
go [(Expr, Sort)]
acc (ECst (EApp Expr
e1 Expr
e) Sort
s) = [(Expr, Sort)] -> Expr -> (Expr, [(Expr, Sort)])
go ((Expr
e, Sort
s) forall a. a -> [a] -> [a]
: [(Expr, Sort)]
acc) Expr
e1
    go [(Expr, Sort)]
_   e :: Expr
e@EApp{}             = forall a. HasCallStack => String -> a
errorstar forall a b. (a -> b) -> a -> b
$ String
"UNEXPECTED: splitArgs: EApp without output type: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e
    go [(Expr, Sort)]
acc Expr
e                    = (Expr
e, [(Expr, Sort)]
acc)

--------------------------------------------------------------------------------
{- | [NOTE:apply-monomorphization]

     Because SMTLIB does not support higher-order functions,
     all _non-theory_ function applications

        EApp e1 e2

     are represented, in SMTLIB, as

        (Eapp (EApp apply e1) e2)

     where 'apply' is 'ECst (EVar "apply") t' and
           't'     is 'FFunc a b'
           'a','b' are the sorts of 'e2' and 'e1 e2' respectively.

     Note that *all polymorphism* goes through this machinery.

     Just before sending to the SMT solver, we use the cast 't'
     to generate a special 'apply_at_t' symbol.

     To let us do the above, we populate 'SymEnv' with the _set_
     of all sorts at which 'apply' is used, computed by 'applySorts'.
 -}

{- | [NOTE:coerce-apply] -- related to [NOTE:apply-monomorphism]

Haskell's GADTs cause a peculiar problem illustrated below:

```haskell
data Field a where
  FInt  :: Field Int
  FBool :: Field Bool

{-@ reflect proj @-}
proj :: Field a -> a -> a
proj fld x = case fld of
               FInt  -> 1 + x
               FBool -> not b
```

## The Problem

The problem is you cannot encode the body of `proj` as a well-sorted refinement:

```haskell
    if is$FInt fld
        then (1 + (coerce (a ~ Int)  x))
        else (not (coerce (a ~ Bool) x))
```

The catch is that `x` is being used BOTH as `Int` and as `Bool`
which is not supported in SMTLIB.

## Approach: Uninterpreted Functions

We encode `coerce` as an explicit **uninterpreted function**:

```haskell
    if is$FInt fld
        then (1 + (coerce@(a -> int)  x))
        else (not (coerce@(a -> bool) x))
```

where we define, extra constants in the style of `apply`

```haskell
   constant coerce@(a -> int ) :: a -> int
   constant coerce@(a -> bool) :: a -> int
```

However, it would not let us verify:


```haskell
{-@ reflect unwrap @-}
unwrap :: Field a -> a -> a
unwrap fld x = proj fld x

{-@ test :: _ -> TT @-}
test =  unwrap FInt  4    == 5
     && unwrap FBool True == False
```

because we'd get

```haskell
  unwrap FInt 4 :: { if is$FInt FInt then (1 + coerce_int_int 4) else ...  }
```

and the UIF nature of `coerce_int_int` renders the VC invalid.

## Solution: Eliminate Trivial Coercions

HOWEVER, the solution here, may simply be to use UIFs when the
coercion is non-trivial (e.g. `a ~ int`) but to eschew them when
they are trivial. That is we would encode:

| Expr                   | SMTLIB             |
|:-----------------------|:-------------------|
| `coerce (a ~ int) x`   | `coerce_a_int x`   |
| `coerce (int ~ int) x` | `x`                |

which, I imagine is what happens _somewhere_ inside GHC too?

-}

--------------------------------------------------------------------------------
applySorts :: Vis.Visitable t => t -> [Sort]
--------------------------------------------------------------------------------
applySorts :: forall t. Visitable t => t -> [Sort]
applySorts = {- tracepp "applySorts" . -} ([Sort]
defs forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> a
Vis.fold forall {ctx}. Visitor [Sort] ctx
vis () []
  where
    defs :: [Sort]
defs   = [Sort -> Sort -> Sort
FFunc Sort
t1 Sort
t2 | Sort
t1 <- [Sort]
basicSorts, Sort
t2 <- [Sort]
basicSorts]
    vis :: Visitor [Sort] ctx
vis    = (forall acc ctx. Monoid acc => Visitor acc ctx
Vis.defaultVisitor :: Vis.Visitor [KVar] t) { accExpr :: ctx -> Expr -> [Sort]
Vis.accExpr = forall {p}. p -> Expr -> [Sort]
go }
    go :: p -> Expr -> [Sort]
go p
_ (EApp (ECst (EVar Symbol
f) Sort
t) Expr
_)   -- get types needed for [NOTE:apply-monomorphism]
           | Symbol
f forall a. Eq a => a -> a -> Bool
== Symbol
applyName
           = [Sort
t]
    go p
_ (ECoerc Sort
t1 Sort
t2 Expr
_)             -- get types needed for [NOTE:coerce-apply]
           = [Sort -> Sort -> Sort
FFunc Sort
t1 Sort
t2]
    go p
_ Expr
_ = []

--------------------------------------------------------------------------------
-- | Expressions sort  ---------------------------------------------------------
--------------------------------------------------------------------------------
exprSort :: String -> Expr -> Sort
exprSort :: String -> Expr -> Sort
exprSort String
msg Expr
e = forall a. a -> Maybe a -> a
fromMaybe (forall a. String -> a
panic String
err') (Expr -> Maybe Sort
exprSortMaybe Expr
e)
  where
    err' :: String
err'        = forall r. PrintfType r => String -> r
printf String
"exprSort [%s] on unexpected expression %s" String
msg (forall a. Show a => a -> String
show Expr
e)

exprSortMaybe :: Expr -> Maybe Sort
exprSortMaybe :: Expr -> Maybe Sort
exprSortMaybe = Expr -> Maybe Sort
go
  where
    go :: Expr -> Maybe Sort
go (ECst Expr
_ Sort
s) = forall a. a -> Maybe a
Just Sort
s
    go (ELam (Symbol
_, Sort
sx) Expr
e) = Sort -> Sort -> Sort
FFunc Sort
sx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Sort
go Expr
e
    go (EApp Expr
e Expr
ex)
      | Just (FFunc Sort
sx Sort
s) <- Sort -> Sort
genSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Sort
go Expr
e
      = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
s (TVSubst -> Sort -> Sort
`apply` Sort
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Sort -> Sort -> Maybe TVSubst
`unifySorts` Sort
sx) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Sort
go Expr
ex)
    go Expr
_ = forall a. Maybe a
Nothing

genSort :: Sort -> Sort
genSort :: Sort -> Sort
genSort (FAbs Int
_ Sort
t) = Sort -> Sort
genSort Sort
t
genSort Sort
t          = Sort
t

unite :: Env -> Expr -> Sort -> Sort -> CheckM (Sort, Sort)
unite :: (Symbol -> SESearch Sort)
-> Expr -> Sort -> Sort -> CheckM (Sort, Sort)
unite Symbol -> SESearch Sort
f Expr
e Sort
t1 Sort
t2 = do
  TVSubst
su <- HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2]
  forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst -> Sort -> Sort
apply TVSubst
su Sort
t1, TVSubst -> Sort -> Sort
apply TVSubst
su Sort
t2)

throwErrorAt :: String -> CheckM a
throwErrorAt :: forall a. String -> CheckM a
throwErrorAt ~String
err' = do -- Lazy pattern needed because we use LANGUAGE Strict in this module
                       -- See Note [Lazy error messages]
  SrcSpan
sp <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> SrcSpan
chSpan
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
throwIO ((() -> Located String) -> ChError
ChError (\()
_ -> forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
sp String
err'))

-- Note [Lazy error messages]
--
-- We don't want to construct error messages early, or
-- we might trigger some expensive computation of editDistance
-- when no error has actually occurred yet.

-- | Helper for checking symbol occurrences
checkSym :: Env -> Symbol -> CheckM Sort
checkSym :: (Symbol -> SESearch Sort) -> Symbol -> CheckM Sort
checkSym Symbol -> SESearch Sort
f Symbol
x = case Symbol -> SESearch Sort
f Symbol
x of
  Found Sort
s -> Sort -> CheckM Sort
instantiate Sort
s
  Alts [Symbol]
xs -> forall a. String -> CheckM a
throwErrorAt (Symbol -> [Symbol] -> String
errUnboundAlts Symbol
x [Symbol]
xs)

-- | Helper for checking if-then-else expressions
checkIte :: Env -> Expr -> Expr -> Expr -> CheckM Sort
checkIte :: (Symbol -> SESearch Sort) -> Expr -> Expr -> Expr -> CheckM Sort
checkIte Symbol -> SESearch Sort
f Expr
p Expr
e1 Expr
e2 = do
  (Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f Expr
p
  Sort
t1 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e1
  Sort
t2 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e2
  (Symbol -> SESearch Sort)
-> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy Symbol -> SESearch Sort
f Expr
p Expr
e1 Expr
e2 Sort
t1 Sort
t2

getIte :: Env -> Expr -> Expr -> CheckM Sort
getIte :: (Symbol -> SESearch Sort) -> Expr -> Expr -> CheckM Sort
getIte Symbol -> SESearch Sort
f Expr
e1 Expr
e2 = do
  Sort
t1 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e1
  Sort
t2 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e2
  (TVSubst -> Sort -> Sort
`apply` Sort
t1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f forall a. Maybe a
Nothing [Sort
t1] [Sort
t2]

checkIteTy :: Env -> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy :: (Symbol -> SESearch Sort)
-> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy Symbol -> SESearch Sort
f Expr
p Expr
e1 Expr
e2 Sort
t1 Sort
t2
  = ((TVSubst -> Sort -> Sort
`apply` Sort
t1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f Maybe Expr
e' [Sort
t1] [Sort
t2]) forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Expr -> Expr -> Sort -> Sort -> String
errIte Expr
e1 Expr
e2 Sort
t1 Sort
t2
  where
    e' :: Maybe Expr
e' = forall a. a -> Maybe a
Just (Expr -> Expr -> Expr -> Expr
EIte Expr
p Expr
e1 Expr
e2)

-- | Helper for checking cast expressions
checkCst :: Env -> Sort -> Expr -> CheckM Sort
checkCst :: (Symbol -> SESearch Sort) -> Sort -> Expr -> CheckM Sort
checkCst Symbol -> SESearch Sort
f Sort
t (EApp Expr
g Expr
e)
  = (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> CheckM Sort
checkApp Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just Sort
t) Expr
g Expr
e
checkCst Symbol -> SESearch Sort
f Sort
t Expr
e
  = do Sort
t' <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e
       ((TVSubst -> Sort -> Sort
`apply` Sort
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just Expr
e) [Sort
t] [Sort
t']) forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Expr -> Sort -> Sort -> String
errCast Expr
e Sort
t' Sort
t

checkApp :: Env -> Maybe Sort -> Expr -> Expr -> CheckM Sort
checkApp :: (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> CheckM Sort
checkApp Symbol -> SESearch Sort
f Maybe Sort
to Expr
g Expr
es
  = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> CheckM (TVSubst, Sort)
checkApp' Symbol -> SESearch Sort
f Maybe Sort
to Expr
g Expr
es

checkExprAs :: Env -> Sort -> Expr -> CheckM Sort
checkExprAs :: (Symbol -> SESearch Sort) -> Sort -> Expr -> CheckM Sort
checkExprAs Symbol -> SESearch Sort
f Sort
t (EApp Expr
g Expr
e)
  = (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> CheckM Sort
checkApp Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just Sort
t) Expr
g Expr
e
checkExprAs Symbol -> SESearch Sort
f Sort
t Expr
e
  = do Sort
t' <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e
       TVSubst
θ  <- HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just Expr
e) [Sort
t'] [Sort
t]
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TVSubst -> Sort -> Sort
apply TVSubst
θ Sort
t

-- | Helper for checking uninterpreted function applications
-- | Checking function application should be curried, e.g.
-- | fromJust :: Maybe a -> a, f :: Maybe (b -> b), x: c |- fromJust f x
--   RJ: The above comment makes no sense to me :(

-- DUPLICATION with 'elabAppAs'
checkApp' :: Env -> Maybe Sort -> Expr -> Expr -> CheckM (TVSubst, Sort)
checkApp' :: (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> CheckM (TVSubst, Sort)
checkApp' Symbol -> SESearch Sort
f Maybe Sort
to Expr
g Expr
e = do
  Sort
gt       <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
g
  Sort
et       <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e
  (Sort
it, Sort
ot, TVSubst
isu) <- Sort -> CheckM (Sort, Sort, TVSubst)
checkFunSort Sort
gt
  let ge :: Maybe Expr
ge    = forall a. a -> Maybe a
Just (Expr -> Expr -> Expr
EApp Expr
g Expr
e)
  TVSubst
su        <- HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
ge TVSubst
isu [Sort
it] [Sort
et]
  let t :: Sort
t     = TVSubst -> Sort -> Sort
apply TVSubst
su Sort
ot
  case Maybe Sort
to of
    Maybe Sort
Nothing    -> forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst
su, Sort
t)
    Just Sort
t'    -> do TVSubst
θ' <- HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
ge TVSubst
su [Sort
t] [Sort
t']
                     let ti :: Sort
ti = TVSubst -> Sort -> Sort
apply TVSubst
θ' Sort
et
                     Sort
_ <- (Symbol -> SESearch Sort) -> Sort -> Expr -> CheckM Sort
checkExprAs Symbol -> SESearch Sort
f Sort
ti Expr
e
                     forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst
θ', TVSubst -> Sort -> Sort
apply TVSubst
θ' Sort
t)


-- | Helper for checking binary (numeric) operations
checkNeg :: Env -> Expr -> CheckM Sort
checkNeg :: (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkNeg Symbol -> SESearch Sort
f Expr
e = do
  Sort
t <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e
  (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric Symbol -> SESearch Sort
f Sort
t forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sort
t

checkOp :: Env -> Expr -> Bop -> Expr -> CheckM Sort
checkOp :: (Symbol -> SESearch Sort) -> Expr -> Bop -> Expr -> CheckM Sort
checkOp Symbol -> SESearch Sort
f Expr
e1 Bop
o Expr
e2
  = do Sort
t1 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e1
       Sort
t2 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e2
       (Symbol -> SESearch Sort) -> Expr -> Sort -> Sort -> CheckM Sort
checkOpTy Symbol -> SESearch Sort
f (Bop -> Expr -> Expr -> Expr
EBin Bop
o Expr
e1 Expr
e2) Sort
t1 Sort
t2


checkOpTy :: Env -> Expr -> Sort -> Sort -> CheckM Sort
checkOpTy :: (Symbol -> SESearch Sort) -> Expr -> Sort -> Sort -> CheckM Sort
checkOpTy Symbol -> SESearch Sort
_ Expr
_ Sort
FInt Sort
FInt
  = forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FInt

checkOpTy Symbol -> SESearch Sort
_ Expr
_ Sort
FReal Sort
FReal
  = forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FReal
-- Coercing int to real is somewhat suspicious, but z3 seems
-- to be ok with it
checkOpTy Symbol -> SESearch Sort
_ Expr
_ Sort
FInt  Sort
FReal
  = forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FReal
checkOpTy Symbol -> SESearch Sort
_ Expr
_ Sort
FReal Sort
FInt
  = forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FReal

checkOpTy Symbol -> SESearch Sort
f Expr
e Sort
t Sort
t'
  | Just TVSubst
s <- (Symbol -> SESearch Sort)
-> Maybe Expr -> Sort -> Sort -> Maybe TVSubst
unify Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just Expr
e) Sort
t Sort
t'
  = (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric Symbol -> SESearch Sort
f (TVSubst -> Sort -> Sort
apply TVSubst
s Sort
t) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst -> Sort -> Sort
apply TVSubst
s Sort
t)

checkOpTy Symbol -> SESearch Sort
_ Expr
e Sort
t Sort
t'
  = forall a. String -> CheckM a
throwErrorAt (Expr -> Sort -> Sort -> String
errOp Expr
e Sort
t Sort
t')

checkFractional :: Env -> Sort -> CheckM ()
checkFractional :: (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkFractional Symbol -> SESearch Sort
f s :: Sort
s@(FObj Symbol
l)
  = do Sort
t <- (Symbol -> SESearch Sort) -> Symbol -> CheckM Sort
checkSym Symbol -> SESearch Sort
f Symbol
l
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort
t forall a. Eq a => a -> a -> Bool
== Sort
FFrac) forall a b. (a -> b) -> a -> b
$ forall a. String -> CheckM a
throwErrorAt (Sort -> String
errNonFractional Sort
s)
checkFractional Symbol -> SESearch Sort
_ Sort
s
  = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort -> Bool
isReal Sort
s) forall a b. (a -> b) -> a -> b
$ forall a. String -> CheckM a
throwErrorAt (Sort -> String
errNonFractional Sort
s)

checkNumeric :: Env -> Sort -> CheckM ()
checkNumeric :: (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric Symbol -> SESearch Sort
f s :: Sort
s@(FObj Symbol
l)
  = do Sort
t <- (Symbol -> SESearch Sort) -> Symbol -> CheckM Sort
checkSym Symbol -> SESearch Sort
f Symbol
l
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort
t forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Sort
FNum, Sort
FFrac, Sort
intSort, Sort
FInt]) (forall a. String -> CheckM a
throwErrorAt forall a b. (a -> b) -> a -> b
$ Sort -> String
errNonNumeric Sort
s)
checkNumeric Symbol -> SESearch Sort
_ Sort
s
  = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort -> Bool
isNumeric Sort
s) (forall a. String -> CheckM a
throwErrorAt forall a b. (a -> b) -> a -> b
$ Sort -> String
errNonNumeric Sort
s)

checkEqConstr :: Env -> Maybe Expr -> TVSubst -> Symbol -> Sort -> CheckM TVSubst
checkEqConstr :: (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Symbol -> Sort -> CheckM TVSubst
checkEqConstr Symbol -> SESearch Sort
_ Maybe Expr
_  TVSubst
θ Symbol
a (FObj Symbol
b)
  | Symbol
a forall a. Eq a => a -> a -> Bool
== Symbol
b
  = forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
checkEqConstr Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ Symbol
a Sort
t =
  case Symbol -> SESearch Sort
f Symbol
a of
    Found Sort
tA -> (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst
unify1 Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ Sort
tA Sort
t
    SESearch Sort
_        -> forall a. String -> CheckM a
throwErrorAt forall a b. (a -> b) -> a -> b
$ Maybe String -> Maybe Expr -> Sort -> Sort -> String
errUnifyMsg (forall a. a -> Maybe a
Just String
"ceq2") Maybe Expr
e (Symbol -> Sort
FObj Symbol
a) Sort
t

--------------------------------------------------------------------------------
-- | Checking Predicates -------------------------------------------------------
--------------------------------------------------------------------------------
checkPred                  :: Env -> Expr -> CheckM ()
checkPred :: (Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f Expr
e = (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr -> Sort -> CheckM ()
checkBoolSort Expr
e

checkBoolSort :: Expr -> Sort -> CheckM ()
checkBoolSort :: Expr -> Sort -> CheckM ()
checkBoolSort Expr
e Sort
s
  | Sort
s forall a. Eq a => a -> a -> Bool
== Sort
boolSort = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise     = forall a. String -> CheckM a
throwErrorAt (Expr -> Sort -> String
errBoolSort Expr
e Sort
s)

-- | Checking Relations
checkRel :: HasCallStack => Env -> Brel -> Expr -> Expr -> CheckM ()
checkRel :: HasCallStack =>
(Symbol -> SESearch Sort) -> Brel -> Expr -> Expr -> CheckM ()
checkRel Symbol -> SESearch Sort
f Brel
Eq Expr
e1 Expr
e2 = do
  Sort
t1 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e1
  Sort
t2 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e2
  TVSubst
su <- HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2] forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` HasCallStack => Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2
  Sort
_  <- (Symbol -> SESearch Sort) -> Sort -> Expr -> CheckM Sort
checkExprAs Symbol -> SESearch Sort
f (TVSubst -> Sort -> Sort
apply TVSubst
su Sort
t1) Expr
e1
  Sort
_  <- (Symbol -> SESearch Sort) -> Sort -> Expr -> CheckM Sort
checkExprAs Symbol -> SESearch Sort
f (TVSubst -> Sort -> Sort
apply TVSubst
su Sort
t2) Expr
e2
  (Symbol -> SESearch Sort)
-> Expr -> Brel -> Sort -> Sort -> CheckM ()
checkRelTy Symbol -> SESearch Sort
f Expr
e Brel
Eq Sort
t1 Sort
t2
  where
    e :: Expr
e = Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq Expr
e1 Expr
e2

checkRel Symbol -> SESearch Sort
f Brel
r  Expr
e1 Expr
e2 = do
  Sort
t1 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e1
  Sort
t2 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e2
  (Symbol -> SESearch Sort)
-> Expr -> Brel -> Sort -> Sort -> CheckM ()
checkRelTy Symbol -> SESearch Sort
f (Brel -> Expr -> Expr -> Expr
PAtom Brel
r Expr
e1 Expr
e2) Brel
r Sort
t1 Sort
t2


checkRelTy :: Env -> Expr -> Brel -> Sort -> Sort -> CheckM ()
checkRelTy :: (Symbol -> SESearch Sort)
-> Expr -> Brel -> Sort -> Sort -> CheckM ()
checkRelTy Symbol -> SESearch Sort
_ Expr
e Brel
Ueq Sort
s1 Sort
s2     = Expr -> Sort -> Sort -> CheckM ()
checkURel Expr
e Sort
s1 Sort
s2
checkRelTy Symbol -> SESearch Sort
_ Expr
e Brel
Une Sort
s1 Sort
s2     = Expr -> Sort -> Sort -> CheckM ()
checkURel Expr
e Sort
s1 Sort
s2
checkRelTy Symbol -> SESearch Sort
f Expr
_ Brel
_ s1 :: Sort
s1@(FObj Symbol
l) s2 :: Sort
s2@(FObj Symbol
l') | Symbol
l forall a. Eq a => a -> a -> Bool
/= Symbol
l'
                             = ((Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric Symbol -> SESearch Sort
f Sort
s1 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric Symbol -> SESearch Sort
f Sort
s2) forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Symbol -> Symbol -> String
errNonNumerics Symbol
l Symbol
l'
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FReal Sort
FReal = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FInt  Sort
FReal = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FReal Sort
FInt  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
f Expr
_ Brel
_ Sort
FInt  Sort
s2    = (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric    Symbol -> SESearch Sort
f Sort
s2 forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Sort -> String
errNonNumeric Sort
s2
checkRelTy Symbol -> SESearch Sort
f Expr
_ Brel
_ Sort
s1    Sort
FInt  = (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric    Symbol -> SESearch Sort
f Sort
s1 forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Sort -> String
errNonNumeric Sort
s1
checkRelTy Symbol -> SESearch Sort
f Expr
_ Brel
_ Sort
FReal Sort
s2    = (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkFractional Symbol -> SESearch Sort
f Sort
s2 forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Sort -> String
errNonFractional Sort
s2
checkRelTy Symbol -> SESearch Sort
f Expr
_ Brel
_ Sort
s1    Sort
FReal = (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkFractional Symbol -> SESearch Sort
f Sort
s1 forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Sort -> String
errNonFractional Sort
s1
checkRelTy Symbol -> SESearch Sort
f Expr
e Brel
Eq Sort
t1 Sort
t2      = forall (f :: * -> *) a. Functor f => f a -> f ()
void (HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2] forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` HasCallStack => Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2)
checkRelTy Symbol -> SESearch Sort
f Expr
e Brel
Ne Sort
t1 Sort
t2      = forall (f :: * -> *) a. Functor f => f a -> f ()
void (HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2] forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` HasCallStack => Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2)
checkRelTy Symbol -> SESearch Sort
_ Expr
e Brel
_  Sort
t1 Sort
t2      = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort
t1 forall a. Eq a => a -> a -> Bool
== Sort
t2) (forall a. String -> CheckM a
throwErrorAt forall a b. (a -> b) -> a -> b
$ HasCallStack => Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2)

checkURel :: Expr -> Sort -> Sort -> CheckM ()
checkURel :: Expr -> Sort -> Sort -> CheckM ()
checkURel Expr
e Sort
s1 Sort
s2 = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
b1 forall a. Eq a => a -> a -> Bool
== Bool
b2) (forall a. String -> CheckM a
throwErrorAt forall a b. (a -> b) -> a -> b
$ HasCallStack => Expr -> Sort -> Sort -> String
errRel Expr
e Sort
s1 Sort
s2)
  where
    b1 :: Bool
b1            = Sort
s1 forall a. Eq a => a -> a -> Bool
== Sort
boolSort
    b2 :: Bool
b2            = Sort
s2 forall a. Eq a => a -> a -> Bool
== Sort
boolSort

--------------------------------------------------------------------------------
-- | Sort Unification on Expressions
--------------------------------------------------------------------------------

{-# SCC unifyExpr #-}
unifyExpr :: Env -> Expr -> Maybe TVSubst
unifyExpr :: (Symbol -> SESearch Sort) -> Expr -> Maybe TVSubst
unifyExpr Symbol -> SESearch Sort
f (EApp Expr
e1 Expr
e2) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes [Maybe TVSubst
θ1, Maybe TVSubst
θ2, Maybe TVSubst
θ]
  where
   θ1 :: Maybe TVSubst
θ1 = (Symbol -> SESearch Sort) -> Expr -> Maybe TVSubst
unifyExpr Symbol -> SESearch Sort
f Expr
e1
   θ2 :: Maybe TVSubst
θ2 = (Symbol -> SESearch Sort) -> Expr -> Maybe TVSubst
unifyExpr Symbol -> SESearch Sort
f Expr
e2
   θ :: Maybe TVSubst
θ  = (Symbol -> SESearch Sort) -> Expr -> Expr -> Maybe TVSubst
unifyExprApp Symbol -> SESearch Sort
f Expr
e1 Expr
e2
unifyExpr Symbol -> SESearch Sort
f (ECst Expr
e Sort
_)
  = (Symbol -> SESearch Sort) -> Expr -> Maybe TVSubst
unifyExpr Symbol -> SESearch Sort
f Expr
e
unifyExpr Symbol -> SESearch Sort
_ Expr
_
  = forall a. Maybe a
Nothing

unifyExprApp :: Env -> Expr -> Expr -> Maybe TVSubst
unifyExprApp :: (Symbol -> SESearch Sort) -> Expr -> Expr -> Maybe TVSubst
unifyExprApp Symbol -> SESearch Sort
f Expr
e1 Expr
e2 = do
  Sort
t1 <- Maybe Sort -> Maybe Sort
getArg forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Sort
exprSortMaybe Expr
e1
  Sort
t2 <- Expr -> Maybe Sort
exprSortMaybe Expr
e2
  (Symbol -> SESearch Sort)
-> Maybe Expr -> Sort -> Sort -> Maybe TVSubst
unify Symbol -> SESearch Sort
f (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
EApp Expr
e1 Expr
e2) Sort
t1 Sort
t2
  where
    getArg :: Maybe Sort -> Maybe Sort
getArg (Just (FFunc Sort
t1 Sort
_)) = forall a. a -> Maybe a
Just Sort
t1
    getArg Maybe Sort
_                   = forall a. Maybe a
Nothing


--------------------------------------------------------------------------------
-- | Sort Unification
--------------------------------------------------------------------------------
{-# SCC unify #-}
unify :: Env -> Maybe Expr -> Sort -> Sort -> Maybe TVSubst
--------------------------------------------------------------------------------
unify :: (Symbol -> SESearch Sort)
-> Maybe Expr -> Sort -> Sort -> Maybe TVSubst
unify Symbol -> SESearch Sort
f Maybe Expr
e Sort
t1 Sort
t2
  = case forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
dummySpan ((Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst
unify1 Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
emptySubst Sort
t1 Sort
t2) of
      Left ChError
_   -> forall a. Maybe a
Nothing
      Right TVSubst
su -> forall a. a -> Maybe a
Just TVSubst
su

--------------------------------------------------------------------------------
unifyTo1 :: Env -> [Sort] -> Maybe Sort
--------------------------------------------------------------------------------
unifyTo1 :: (Symbol -> SESearch Sort) -> [Sort] -> Maybe Sort
unifyTo1 Symbol -> SESearch Sort
f [Sort]
ts
  = case forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
dummySpan ((Symbol -> SESearch Sort) -> [Sort] -> CheckM Sort
unifyTo1M Symbol -> SESearch Sort
f [Sort]
ts) of
      Left ChError
_  -> forall a. Maybe a
Nothing
      Right Sort
t -> forall a. a -> Maybe a
Just Sort
t


--------------------------------------------------------------------------------
unifyTo1M :: Env -> [Sort] -> CheckM Sort
--------------------------------------------------------------------------------
unifyTo1M :: (Symbol -> SESearch Sort) -> [Sort] -> CheckM Sort
unifyTo1M Symbol -> SESearch Sort
_ []     = forall a. String -> a
panic String
"unifyTo1: empty list"
unifyTo1M Symbol -> SESearch Sort
f (Sort
t0:[Sort]
ts) = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (TVSubst, Sort) -> Sort -> CheckM (TVSubst, Sort)
step (TVSubst
emptySubst, Sort
t0) [Sort]
ts
  where
    step :: (TVSubst, Sort) -> Sort -> CheckM (TVSubst, Sort)
    step :: (TVSubst, Sort) -> Sort -> CheckM (TVSubst, Sort)
step (TVSubst
su, Sort
t) Sort
t' = do
      TVSubst
su' <- (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst
unify1 Symbol -> SESearch Sort
f forall a. Maybe a
Nothing TVSubst
su Sort
t Sort
t'
      forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst
su', TVSubst -> Sort -> Sort
apply TVSubst
su' Sort
t)


--------------------------------------------------------------------------------
unifySorts :: Sort -> Sort -> Maybe TVSubst
--------------------------------------------------------------------------------
unifySorts :: Sort -> Sort -> Maybe TVSubst
unifySorts   = Bool -> (Symbol -> SESearch Sort) -> Sort -> Sort -> Maybe TVSubst
unifyFast Bool
False forall {a} {a}. PPrint a => a -> a
emptyEnv
  where
    emptyEnv :: a -> a
emptyEnv a
x = forall a. Error -> a
die forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan forall a b. (a -> b) -> a -> b
$ Doc
"SortCheck: lookup in Empty Env: " forall a. Semigroup a => a -> a -> a
<> forall a. PPrint a => a -> Doc
pprint a
x


--------------------------------------------------------------------------------
-- | Fast Unification; `unifyFast True` is just equality
--------------------------------------------------------------------------------
unifyFast :: Bool -> Env -> Sort -> Sort -> Maybe TVSubst
--------------------------------------------------------------------------------
unifyFast :: Bool -> (Symbol -> SESearch Sort) -> Sort -> Sort -> Maybe TVSubst
unifyFast Bool
False Symbol -> SESearch Sort
f Sort
t1 Sort
t2 = (Symbol -> SESearch Sort)
-> Maybe Expr -> Sort -> Sort -> Maybe TVSubst
unify Symbol -> SESearch Sort
f forall a. Maybe a
Nothing Sort
t1 Sort
t2
unifyFast Bool
True  Symbol -> SESearch Sort
_ Sort
t1 Sort
t2
  | Sort
t1 forall a. Eq a => a -> a -> Bool
== Sort
t2        = forall a. a -> Maybe a
Just TVSubst
emptySubst
  | Bool
otherwise           = forall a. Maybe a
Nothing

{-
eqFast :: Sort -> Sort -> Bool
eqFast = go
  where
    go FAbs {} _       = False
    go (FFunc s1 s2) t = case t of
                          FFunc t1 t2 -> go s1 t1 && go s2 t2
                          _ -> False
    go (FApp s1 s2)  t = case t of
                          FApp t1 t2 ->  go s1 t1 && go s2 t2
                          _ -> False

    go (FTC s1) t      = case t of
                            FTC t1 -> s1 == t1
                            _ -> False

    go FInt FInt           = True
    go FReal FReal         = True
    go FNum FNum           = True
    go FFrac FFrac         = True
    go (FVar i1) (FVar i2) = i1 == i2
    go _ _                 = False

 -}
--------------------------------------------------------------------------------
unifys :: HasCallStack => Env -> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
--------------------------------------------------------------------------------
unifys :: HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f Maybe Expr
e = HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
emptySubst

unifyMany :: HasCallStack => Env -> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany :: HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ [Sort]
ts [Sort]
ts'
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts' = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst
unify1 Symbol -> SESearch Sort
f Maybe Expr
e) TVSubst
θ forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Sort]
ts [Sort]
ts'
  | Bool
otherwise               = forall a. String -> CheckM a
throwErrorAt ([Sort] -> [Sort] -> String
errUnifyMany [Sort]
ts [Sort]
ts')

unify1 :: Env -> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst
unify1 :: (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst
unify1 Symbol -> SESearch Sort
f Maybe Expr
e !TVSubst
θ (FVar !Int
i) !Sort
t
  = (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Int -> Sort -> CheckM TVSubst
unifyVar Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ Int
i Sort
t
unify1 Symbol -> SESearch Sort
f Maybe Expr
e !TVSubst
θ !Sort
t (FVar !Int
i)
  = (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Int -> Sort -> CheckM TVSubst
unifyVar Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ Int
i Sort
t
unify1 Symbol -> SESearch Sort
f Maybe Expr
e !TVSubst
θ (FApp !Sort
t1 !Sort
t2) (FApp !Sort
t1' !Sort
t2')
  = HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ [Sort
t1, Sort
t2] [Sort
t1', Sort
t2']
unify1 Symbol -> SESearch Sort
_ Maybe Expr
_ !TVSubst
θ (FTC !FTycon
l1) (FTC !FTycon
l2)
  | FTycon -> Bool
isListTC FTycon
l1 Bool -> Bool -> Bool
&& FTycon -> Bool
isListTC FTycon
l2
  = forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
unify1 Symbol -> SESearch Sort
f Maybe Expr
e !TVSubst
θ t1 :: Sort
t1@(FAbs Int
_ Sort
_) !Sort
t2 = do
  !Sort
t1' <- Sort -> CheckM Sort
instantiate Sort
t1
  HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ [Sort
t1'] [Sort
t2]
unify1 Symbol -> SESearch Sort
f Maybe Expr
e !TVSubst
θ !Sort
t1 t2 :: Sort
t2@(FAbs Int
_ Sort
_) = do
  !Sort
t2' <- Sort -> CheckM Sort
instantiate Sort
t2
  HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ [Sort
t1] [Sort
t2']
unify1 Symbol -> SESearch Sort
_ Maybe Expr
_ !TVSubst
θ !Sort
s1 !Sort
s2
  | Sort -> Bool
isString Sort
s1, Sort -> Bool
isString Sort
s2
  = forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
unify1 Symbol -> SESearch Sort
_ Maybe Expr
_ !TVSubst
θ Sort
FInt  Sort
FReal = forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ

unify1 Symbol -> SESearch Sort
_ Maybe Expr
_ !TVSubst
θ Sort
FReal Sort
FInt  = forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ

unify1 Symbol -> SESearch Sort
f Maybe Expr
e !TVSubst
θ !Sort
t Sort
FInt = do
  (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric Symbol -> SESearch Sort
f Sort
t forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Maybe Expr -> Sort -> Sort -> String
errUnify Maybe Expr
e Sort
t Sort
FInt
  forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ

unify1 Symbol -> SESearch Sort
f Maybe Expr
e !TVSubst
θ Sort
FInt !Sort
t = do
  (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric Symbol -> SESearch Sort
f Sort
t forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Maybe Expr -> Sort -> Sort -> String
errUnify Maybe Expr
e Sort
FInt Sort
t
  forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ

unify1 Symbol -> SESearch Sort
f Maybe Expr
e !TVSubst
θ (FFunc !Sort
t1 !Sort
t2) (FFunc !Sort
t1' !Sort
t2') =
  HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ [Sort
t1, Sort
t2] [Sort
t1', Sort
t2']

unify1 Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ (FObj Symbol
a) !Sort
t =
  (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Symbol -> Sort -> CheckM TVSubst
checkEqConstr Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ Symbol
a Sort
t

unify1 Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ !Sort
t (FObj Symbol
a) =
  (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Symbol -> Sort -> CheckM TVSubst
checkEqConstr Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ Symbol
a Sort
t

unify1 Symbol -> SESearch Sort
_ Maybe Expr
e TVSubst
θ !Sort
t1 !Sort
t2
  | Sort
t1 forall a. Eq a => a -> a -> Bool
== Sort
t2
  = forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
  | Bool
otherwise
  = forall a. String -> CheckM a
throwErrorAt (Maybe Expr -> Sort -> Sort -> String
errUnify Maybe Expr
e Sort
t1 Sort
t2)

subst :: Int -> Sort -> Sort -> Sort
subst :: Int -> Sort -> Sort -> Sort
subst !Int
j !Sort
tj t :: Sort
t@(FVar !Int
i)
  | Int
i forall a. Eq a => a -> a -> Bool
== Int
j                  = Sort
tj
  | Bool
otherwise               = Sort
t

subst !Int
j !Sort
tj (FApp !Sort
t1 !Sort
t2)  = Sort -> Sort -> Sort
FApp Sort
t1' Sort
t2'
  where
    !t1' :: Sort
t1'                    = Int -> Sort -> Sort -> Sort
subst Int
j Sort
tj Sort
t1
    !t2' :: Sort
t2'                    = Int -> Sort -> Sort -> Sort
subst Int
j Sort
tj Sort
t2

-- subst _ _  !(FTC l)         = FTC l
subst !Int
j !Sort
tj (FFunc !Sort
t1 !Sort
t2) = Sort -> Sort -> Sort
FFunc Sort
t1' Sort
t2'
  where
    !t1' :: Sort
t1'                    = Int -> Sort -> Sort -> Sort
subst Int
j Sort
tj forall a b. (a -> b) -> a -> b
$! Sort
t1
    !t2' :: Sort
t2'                    = Int -> Sort -> Sort -> Sort
subst Int
j Sort
tj forall a b. (a -> b) -> a -> b
$! Sort
t2

subst !Int
j !Sort
tj (FAbs !Int
i !Sort
t)
  | Int
i forall a. Eq a => a -> a -> Bool
== Int
j                  = Int -> Sort -> Sort
FAbs Int
i Sort
t
  | Bool
otherwise               = Int -> Sort -> Sort
FAbs Int
i Sort
t'
  where
    !t' :: Sort
t'                     = Int -> Sort -> Sort -> Sort
subst Int
j Sort
tj Sort
t

subst Int
_  Sort
_   !Sort
s             = Sort
s

--------------------------------------------------------------------------------
instantiate :: Sort -> CheckM Sort
--------------------------------------------------------------------------------
instantiate :: Sort -> CheckM Sort
instantiate !Sort
t = Sort -> CheckM Sort
go Sort
t
  where
    go :: Sort -> CheckM Sort
go (FAbs !Int
i !Sort
t') = do
      !Sort
t''    <- Sort -> CheckM Sort
instantiate Sort
t'
      !Int
v     <- CheckM Int
fresh
      forall (m :: * -> *) a. Monad m => a -> m a
return  forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort -> Sort
subst Int
i (Int -> Sort
FVar Int
v) Sort
t''
    go !Sort
t' =
      forall (m :: * -> *) a. Monad m => a -> m a
return Sort
t'

unifyVar :: Env -> Maybe Expr -> TVSubst -> Int -> Sort -> CheckM TVSubst
unifyVar :: (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Int -> Sort -> CheckM TVSubst
unifyVar Symbol -> SESearch Sort
_ Maybe Expr
_ TVSubst
θ !Int
i t :: Sort
t@(FVar !Int
j)
  = case Int -> TVSubst -> Maybe Sort
lookupVar Int
i TVSubst
θ of
      Just !Sort
t'      -> if Sort
t forall a. Eq a => a -> a -> Bool
== Sort
t' then forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ else forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sort -> TVSubst -> TVSubst
updateVar Int
j Sort
t' TVSubst
θ)
      Maybe Sort
Nothing       -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sort -> TVSubst -> TVSubst
updateVar Int
i Sort
t TVSubst
θ)

unifyVar Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ !Int
i !Sort
t
  = case Int -> TVSubst -> Maybe Sort
lookupVar Int
i TVSubst
θ of
      Just (FVar !Int
j) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Sort -> TVSubst -> TVSubst
updateVar Int
i Sort
t forall a b. (a -> b) -> a -> b
$ Int -> Sort -> TVSubst -> TVSubst
updateVar Int
j Sort
t TVSubst
θ
      Just !Sort
t'       -> if Sort
t forall a. Eq a => a -> a -> Bool
== Sort
t' then forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ else (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst
unify1 Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ Sort
t Sort
t'
      Maybe Sort
Nothing        -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sort -> TVSubst -> TVSubst
updateVar Int
i Sort
t TVSubst
θ)

--------------------------------------------------------------------------------
-- | Applying a Type Substitution ----------------------------------------------
--------------------------------------------------------------------------------
apply :: TVSubst -> Sort -> Sort
--------------------------------------------------------------------------------
apply :: TVSubst -> Sort -> Sort
apply TVSubst
θ          = (Sort -> Sort) -> Sort -> Sort
Vis.mapSort Sort -> Sort
f
  where
    f :: Sort -> Sort
f t :: Sort
t@(FVar Int
i) = forall a. a -> Maybe a -> a
fromMaybe Sort
t (Int -> TVSubst -> Maybe Sort
lookupVar Int
i TVSubst
θ)
    f Sort
t          = Sort
t

applyExpr :: Maybe TVSubst -> Expr -> Expr
applyExpr :: Maybe TVSubst -> Expr -> Expr
applyExpr Maybe TVSubst
Nothing Expr
e  = Expr
e
applyExpr (Just TVSubst
θ) Expr
e = (Expr -> Expr) -> Expr -> Expr
Vis.mapExprOnExpr Expr -> Expr
f Expr
e
  where
    f :: Expr -> Expr
f (ECst Expr
e' Sort
s) = Expr -> Sort -> Expr
ECst Expr
e' (TVSubst -> Sort -> Sort
apply TVSubst
θ Sort
s)
    f Expr
e'          = Expr
e'

--------------------------------------------------------------------------------
_applyCoercion :: Symbol -> Sort -> Sort -> Sort
--------------------------------------------------------------------------------
_applyCoercion :: Symbol -> Sort -> Sort -> Sort
_applyCoercion Symbol
a Sort
t = (Sort -> Sort) -> Sort -> Sort
Vis.mapSort Sort -> Sort
f
  where
    f :: Sort -> Sort
f (FObj Symbol
b)
      | Symbol
a forall a. Eq a => a -> a -> Bool
== Symbol
b    = Sort
t
    f Sort
s           = Sort
s


--------------------------------------------------------------------------------
-- | Deconstruct a function-sort -----------------------------------------------
--------------------------------------------------------------------------------
checkFunSort :: Sort -> CheckM (Sort, Sort, TVSubst)
checkFunSort :: Sort -> CheckM (Sort, Sort, TVSubst)
checkFunSort (FAbs Int
_ Sort
t)    = Sort -> CheckM (Sort, Sort, TVSubst)
checkFunSort Sort
t
checkFunSort (FFunc Sort
t1 Sort
t2) = forall (m :: * -> *) a. Monad m => a -> m a
return (Sort
t1, Sort
t2, TVSubst
emptySubst)
checkFunSort (FVar Int
i)      = do Int
j <- CheckM Int
fresh
                                Int
k <- CheckM Int
fresh
                                forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sort
FVar Int
j, Int -> Sort
FVar Int
k, Int -> Sort -> TVSubst -> TVSubst
updateVar Int
i (Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
j) (Int -> Sort
FVar Int
k)) TVSubst
emptySubst)
checkFunSort Sort
t             = forall a. String -> CheckM a
throwErrorAt (Int -> Sort -> String
errNonFunction Int
1 Sort
t)

--------------------------------------------------------------------------------
-- | API for manipulating Sort Substitutions -----------------------------------
--------------------------------------------------------------------------------

newtype TVSubst = Th (M.HashMap Int Sort) deriving (Int -> TVSubst -> String -> String
[TVSubst] -> String -> String
TVSubst -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [TVSubst] -> String -> String
$cshowList :: [TVSubst] -> String -> String
show :: TVSubst -> String
$cshow :: TVSubst -> String
showsPrec :: Int -> TVSubst -> String -> String
$cshowsPrec :: Int -> TVSubst -> String -> String
Show)

instance Semigroup TVSubst where
  (Th HashMap Int Sort
s1) <> :: TVSubst -> TVSubst -> TVSubst
<> (Th HashMap Int Sort
s2) = HashMap Int Sort -> TVSubst
Th (HashMap Int Sort
s1 forall a. Semigroup a => a -> a -> a
<> HashMap Int Sort
s2)

instance Monoid TVSubst where
  mempty :: TVSubst
mempty  = HashMap Int Sort -> TVSubst
Th forall a. Monoid a => a
mempty
  mappend :: TVSubst -> TVSubst -> TVSubst
mappend = forall a. Semigroup a => a -> a -> a
(<>)

lookupVar :: Int -> TVSubst -> Maybe Sort
lookupVar :: Int -> TVSubst -> Maybe Sort
lookupVar Int
i (Th HashMap Int Sort
m)   = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i HashMap Int Sort
m
{-# SCC lookupVar #-}

updateVar :: Int -> Sort -> TVSubst -> TVSubst
updateVar :: Int -> Sort -> TVSubst -> TVSubst
updateVar !Int
i !Sort
t (Th HashMap Int Sort
m) = HashMap Int Sort -> TVSubst
Th (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Int
i Sort
t HashMap Int Sort
m)

emptySubst :: TVSubst
emptySubst :: TVSubst
emptySubst = HashMap Int Sort -> TVSubst
Th forall k v. HashMap k v
M.empty

--------------------------------------------------------------------------------
-- | Error messages ------------------------------------------------------------
--------------------------------------------------------------------------------

errElabExpr   :: Expr -> String
errElabExpr :: Expr -> String
errElabExpr Expr
e = forall r. PrintfType r => String -> r
printf String
"Elaborate fails on %s" (forall a. PPrint a => a -> String
showpp Expr
e)

errUnifyMsg :: Maybe String -> Maybe Expr -> Sort -> Sort -> String
errUnifyMsg :: Maybe String -> Maybe Expr -> Sort -> Sort -> String
errUnifyMsg Maybe String
msgMb Maybe Expr
eo Sort
t1 Sort
t2
  = forall r. PrintfType r => String -> r
printf String
"Cannot unify %s with %s %s %s"
      (forall a. PPrint a => a -> String
showpp Sort
t1) {- (show t1) -} (forall a. PPrint a => a -> String
showpp Sort
t2) {-(show t2)-} (Maybe Expr -> String
errUnifyExpr Maybe Expr
eo) String
msgStr
    where
      msgStr :: String
msgStr = case Maybe String
msgMb of { Maybe String
Nothing -> String
""; Just String
s -> String
"<< " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" >>"}

errUnify :: Maybe Expr -> Sort -> Sort -> String
errUnify :: Maybe Expr -> Sort -> Sort -> String
errUnify = Maybe String -> Maybe Expr -> Sort -> Sort -> String
errUnifyMsg forall a. Maybe a
Nothing

errUnifyExpr :: Maybe Expr -> String
errUnifyExpr :: Maybe Expr -> String
errUnifyExpr Maybe Expr
Nothing  = String
""
errUnifyExpr (Just Expr
e) = String
"in expression: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e

errUnifyMany :: [Sort] -> [Sort] -> String
errUnifyMany :: [Sort] -> [Sort] -> String
errUnifyMany [Sort]
ts [Sort]
ts'  = forall r. PrintfType r => String -> r
printf String
"Cannot unify types with different cardinalities %s and %s"
                         (forall a. PPrint a => a -> String
showpp [Sort]
ts) (forall a. PPrint a => a -> String
showpp [Sort]
ts')

errRel :: HasCallStack => Expr -> Sort -> Sort -> String
errRel :: HasCallStack => Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2       =
  HasCallStack => (HasCallStack => String) -> String
traced forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"Invalid Relation %s with operand types %s and %s"
                         (forall a. PPrint a => a -> String
showpp Expr
e) (forall a. PPrint a => a -> String
showpp Sort
t1) (forall a. PPrint a => a -> String
showpp Sort
t2)

errOp :: Expr -> Sort -> Sort -> String
errOp :: Expr -> Sort -> Sort -> String
errOp Expr
e Sort
t Sort
t'
  | Sort
t forall a. Eq a => a -> a -> Bool
== Sort
t'          = forall r. PrintfType r => String -> r
printf String
"Operands have non-numeric types %s in %s"
                         (forall a. PPrint a => a -> String
showpp Sort
t) (forall a. PPrint a => a -> String
showpp Expr
e)
  | Bool
otherwise        = forall r. PrintfType r => String -> r
printf String
"Operands have different types %s and %s in %s"
                         (forall a. PPrint a => a -> String
showpp Sort
t) (forall a. PPrint a => a -> String
showpp Sort
t') (forall a. PPrint a => a -> String
showpp Expr
e)

errIte :: Expr -> Expr -> Sort -> Sort -> String
errIte :: Expr -> Expr -> Sort -> Sort -> String
errIte Expr
e1 Expr
e2 Sort
t1 Sort
t2   = forall r. PrintfType r => String -> r
printf String
"Mismatched branches in Ite: then %s : %s, else %s : %s"
                         (forall a. PPrint a => a -> String
showpp Expr
e1) (forall a. PPrint a => a -> String
showpp Sort
t1) (forall a. PPrint a => a -> String
showpp Expr
e2) (forall a. PPrint a => a -> String
showpp Sort
t2)

errCast :: Expr -> Sort -> Sort -> String
errCast :: Expr -> Sort -> Sort -> String
errCast Expr
e Sort
t' Sort
t       = forall r. PrintfType r => String -> r
printf String
"Cannot cast %s of sort %s to incompatible sort %s"
                         (forall a. PPrint a => a -> String
showpp Expr
e) (forall a. PPrint a => a -> String
showpp Sort
t') (forall a. PPrint a => a -> String
showpp Sort
t)

errUnboundAlts :: Symbol -> [Symbol] -> String
errUnboundAlts :: Symbol -> [Symbol] -> String
errUnboundAlts Symbol
x [Symbol]
xs  = forall r. PrintfType r => String -> r
printf String
"Unbound symbol %s --- perhaps you meant: %s ?"
                         (forall a. PPrint a => a -> String
showpp Symbol
x) (forall a. [a] -> [[a]] -> [a]
L.intercalate String
", " (forall a. PPrint a => a -> String
showpp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs))

errNonFunction :: Int -> Sort -> String
errNonFunction :: Int -> Sort -> String
errNonFunction Int
i Sort
t   = forall r. PrintfType r => String -> r
printf String
"The sort %s is not a function with at least %s arguments\n" (forall a. PPrint a => a -> String
showpp Sort
t) (forall a. PPrint a => a -> String
showpp Int
i)

errNonNumeric :: Sort -> String
errNonNumeric :: Sort -> String
errNonNumeric  Sort
l     = forall r. PrintfType r => String -> r
printf String
"The sort %s is not numeric" (forall a. PPrint a => a -> String
showpp Sort
l)

errNonNumerics :: Symbol -> Symbol -> String
errNonNumerics :: Symbol -> Symbol -> String
errNonNumerics Symbol
l Symbol
l'  = forall r. PrintfType r => String -> r
printf String
"FObj sort %s and %s are different and not numeric" (forall a. PPrint a => a -> String
showpp Symbol
l) (forall a. PPrint a => a -> String
showpp Symbol
l')

errNonFractional :: Sort -> String
errNonFractional :: Sort -> String
errNonFractional  Sort
l  = forall r. PrintfType r => String -> r
printf String
"The sort %s is not fractional" (forall a. PPrint a => a -> String
showpp Sort
l)

errBoolSort :: Expr -> Sort -> String
errBoolSort :: Expr -> Sort -> String
errBoolSort     Expr
e Sort
s  = forall r. PrintfType r => String -> r
printf String
"Expressions %s should have bool sort, but has %s" (forall a. PPrint a => a -> String
showpp Expr
e) (forall a. PPrint a => a -> String
showpp Sort
s)