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

-- | 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.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 CallStack
HasCallStack => CallStack
callStack)
         in String
HasCallStack => String
str String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" (at " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
prettified String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"
    else String
HasCallStack => String
str

--------------------------------------------------------------------------------
-- | Predicates on Sorts -------------------------------------------------------
--------------------------------------------------------------------------------
isMono :: Sort -> Bool
--------------------------------------------------------------------------------
isMono :: Sort -> Bool
isMono             = [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Int] -> Bool) -> (Sort -> [Int]) -> Sort -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Int] -> Sort -> [Int]) -> [Int] -> Sort -> [Int]
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 Int -> [Int] -> [Int]
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
    { F.cm      = elaborate x senv <$> F.cm      si
    , F.bs      = elaborate x senv  $  F.bs      si
    , F.asserts = elaborate x senv <$> F.asserts 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 = (e -> e) -> Triggered e -> Triggered e
forall a b. (a -> b) -> Triggered a -> Triggered b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Located String -> SymEnv -> e -> e
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 = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Located String -> SymEnv -> a -> a
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 (Sort -> Sort -> Sort) -> (Sort -> Sort) -> Sort -> Sort -> Sort
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   = elaborate msg env (aenvEqs 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 = skipElabExpr msg env' (smBody rw) }
    where
      env' :: SymEnv
env' = SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv SymEnv
env [(Symbol, Sort)]
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 = skipElabExpr msg env' (eqBody 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 (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Expr -> Expr
elabApply SymEnv
env (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
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 (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Expr -> Expr
elabApply SymEnv
env (Expr -> Expr) -> Expr -> Expr
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, Located String -> SymEnv -> Sort -> Sort
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 = Located String -> SymEnv -> a -> a
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
msg SymEnv
env (a -> a) -> [a] -> [a]
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 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
FReal
      , String -> Expr -> Sort
exprSort String
"txn2" Expr
e2 Sort -> Sort -> Bool
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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e1) Expr
e1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
FReal
      , String -> Expr -> Sort
exprSort String
"txn4" Expr
e2 Sort -> Sort -> Bool
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'   = Located String -> SymEnv -> Expr -> Expr
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 = (Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> BindEnv a -> BindEnv a
forall a.
(Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> BindEnv a -> BindEnv a
mapBindEnv (\Int
i (Symbol
x, SortedReft
sr, a
l) -> (Symbol
x, Located String -> SymEnv -> SortedReft -> SortedReft
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (a -> Int -> Symbol -> SortedReft -> Located String
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 = l -> String -> Located String
forall l b. Loc l => l -> b -> Located b
atLoc l
l (Located String -> String
forall a. Located a -> a
val Located String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String
" elabBE",  a -> String
forall a. Show a => a -> String
show a
i, a -> String
forall a. Show a => a -> String
show a
x, a -> String
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 = elaborate msg' env (_crhs c) }
    where msg' :: Located String
msg'        = SimpC a -> String -> Located String
forall l b. Loc l => l -> b -> Located b
atLoc SimpC a
c (Located String -> String
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  -> Error -> Expr
forall a. Error -> a
die Error
ex
  Right Expr
e' -> String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
F.notracepp (String
"elabExp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
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 SrcSpan -> CheckM (Expr, Sort) -> Either ChError (Expr, Sort)
forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 (Located String -> SrcSpan
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 Error -> Either Error Expr
forall a b. a -> Either a b
Left (Error -> Either Error Expr) -> Error -> Either Error Expr
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err (Located String -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan Located String
e') (String -> Doc
d (Located String -> String
forall a. Located a -> a
val Located String
e'))
    Right (Expr, Sort)
s  -> Expr -> Either Error Expr
forall a b. b -> Either a b
Right ((Expr, Sort) -> Expr
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 = (Symbol -> SEnv Sort -> SESearch Sort
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 (Located String -> String
forall a. Located a -> a
val Located String
msg) Doc -> Doc -> Doc
<+> Doc
"failed on:"
                , Int -> Doc -> Doc
nest Int
4 (Expr -> Doc
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 (SEnv Sort -> Doc
forall a. PPrint a => a -> Doc
pprint (SEnv Sort -> Doc) -> SEnv Sort -> Doc
forall a b. (a -> b) -> a -> b
$ SEnv Sort -> Expr -> SEnv Sort
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) ((Expr -> Expr) -> (Expr, Sort) -> (Expr, Sort)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst Expr -> Expr
go ((Expr, Sort) -> (Expr, Sort)) -> [(Expr, Sort)] -> [(Expr, Sort)]
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 (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ps)
    step (POr [Expr]
ps)         = [Expr] -> Expr
POr  (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
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                = String -> Expr
forall a. HasCallStack => String -> a
error (String -> Expr) -> String -> Expr
forall a b. (a -> b) -> a -> b
$ String
"TODO elabApply: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
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 SrcSpan -> CheckM Sort -> Either ChError Sort
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') -> Error -> Sort
forall a. Error -> a
die (Error -> Sort) -> Error -> Sort
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
l (String -> Doc
d (Located String -> String
forall a. Located a -> a
val (() -> Located String
f' ())))
    Right Sort
s -> Sort
s
  where
    f :: Symbol -> SESearch Sort
f   = (Symbol -> SEnv Sort -> SESearch Sort
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 (Expr -> Doc
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 (SEnv Sort -> Doc
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 SrcSpan -> CheckM Sort -> Either ChError Sort
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
_   -> Maybe Sort
forall a. Maybe a
Nothing
    Right Sort
s  -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
s
  where
    f :: Symbol -> SESearch Sort
f Symbol
x  = case Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
γ of
            Just Sort
z  -> Sort -> SESearch Sort
forall a. a -> SESearch a
Found Sort
z
            Maybe Sort
Nothing -> [Symbol] -> SESearch Sort
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 = (a -> () -> a) -> SEnv a -> SEnv () -> SEnv a
forall v1 v2 a. (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a
intersectWithSEnv a -> () -> a
forall a b. a -> b -> a
const SEnv a
g SEnv ()
g'
  where
    g' :: SEnv ()
g' = [(Symbol, ())] -> SEnv ()
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv ([(Symbol, ())] -> SEnv ()) -> [(Symbol, ())] -> SEnv ()
forall a b. (a -> b) -> a -> b
$ (, ()) (Symbol -> (Symbol, ())) -> [Symbol] -> [(Symbol, ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> [Symbol]
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) = Located String -> String
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 = Symbol -> SEnv a -> SESearch a
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 <- ReaderT ChState IO ChState
forall r (m :: * -> *). MonadReader r m => m r
ask
  IO a -> CheckM a
forall a. IO a -> ReaderT ChState IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> CheckM a) -> IO a -> CheckM a
forall a b. (a -> b) -> a -> b
$ CheckM a -> ChState -> IO a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT CheckM a
act ChState
r IO a -> (ChError -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch`
    (\(ChError () -> Located String
f) ->
      ChError -> IO a
forall e a. Exception e => e -> IO a
throwIO (ChError -> IO a) -> ChError -> IO a
forall a b. (a -> b) -> a -> b
$ (() -> Located String) -> ChError
ChError ((() -> Located String) -> ChError)
-> (() -> Located String) -> ChError
forall a b. (a -> b) -> a -> b
$ \()
_ ->
        let e :: Located String
e = () -> Located String
f ()
         in Located String -> String -> Located String
forall l b. Loc l => l -> b -> Located b
atLoc Located String
e (Located String -> String
forall a. Located a -> a
val Located String
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n  because\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg)
    )

-- XXX: Why start at 42?
{-# NOINLINE varCounterRef #-}
varCounterRef :: IORef Int
varCounterRef :: IORef Int
varCounterRef = IO (IORef Int) -> IORef Int
forall a. IO a -> a
unsafePerformIO (IO (IORef Int) -> IORef Int) -> IO (IORef Int) -> IORef Int
forall a b. (a -> b) -> a -> b
$ Int -> IO (IORef Int)
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 = IO (Either ChError a) -> Either ChError a
forall a. IO a -> a
unsafePerformIO (IO (Either ChError a) -> Either ChError a)
-> IO (Either ChError a) -> Either ChError a
forall a b. (a -> b) -> a -> b
$ do
  IO a -> IO (Either ChError a)
forall e a. Exception e => IO a -> IO (Either e a)
try (CheckM a -> ChState -> IO a
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 <- (ChState -> IORef Int) -> ReaderT ChState IO (IORef Int)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> IORef Int
chCount
  IO Int -> CheckM Int
forall a. IO a -> ReaderT ChState IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> CheckM Int) -> IO Int -> CheckM Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> (Int -> (Int, Int)) -> IO Int
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef Int
rn ((Int -> (Int, Int)) -> IO Int) -> (Int -> (Int, Int)) -> IO Int
forall a b. (a -> b) -> a -> b
$ \Int
n -> (Int
nInt -> Int -> Int
forall 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 = Maybe Doc -> ([Symbol] -> Maybe Doc) -> [Symbol] -> Maybe Doc
forall b a. b -> ([a] -> b) -> [a] -> b
applyNonNull Maybe Doc
forall a. Maybe a
Nothing [Symbol] -> Maybe Doc
oops [Symbol]
unknowns
  where
    oops :: [Symbol] -> Maybe Doc
oops                  = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> ([Symbol] -> Doc) -> [Symbol] -> Maybe Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc
text String
"Unknown symbols:" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> ([Symbol] -> Doc) -> [Symbol] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> Doc
forall a. Fixpoint a => a -> Doc
toFix
    unknowns :: [Symbol]
unknowns              = [ Symbol
x | Symbol
x <- SortedReft -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms SortedReft
sr, Symbol
x Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Symbol
v Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
xs, Bool -> Bool
not (Symbol
x Symbol -> SEnv SortedReft -> Bool
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 SrcSpan -> CheckM () -> Either ChError ()
forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp (SEnv Sort -> a -> CheckM ()
forall a. Checkable a => SEnv Sort -> a -> CheckM ()
check SEnv Sort
γ' a
t) of
    Left (ChError () -> Located String
f)  -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Located String -> String
forall a. Located a -> a
val (() -> Located String
f ())))
    Right ()
_ -> Maybe Doc
forall a. Maybe a
Nothing
  where
    γ' :: SEnv Sort
γ' = SortedReft -> Sort
sr_sort (SortedReft -> Sort) -> SEnv SortedReft -> SEnv 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 SrcSpan -> CheckM () -> Either ChError ()
forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp (SEnv Sort -> Sort -> a -> CheckM ()
forall a. Checkable a => SEnv Sort -> Sort -> a -> CheckM ()
checkSort SEnv Sort
γ' Sort
s a
t) of
    Left (ChError () -> Located String
f)  -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Located String -> String
forall a. Located a -> a
val (() -> Located String
f ())))
    Right ()
_ -> Maybe Doc
forall a. Maybe a
Nothing
  where
      γ' :: SEnv Sort
γ' = SortedReft -> Sort
sr_sort (SortedReft -> Sort) -> SEnv SortedReft -> SEnv 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 SrcSpan -> CheckM () -> Either ChError ()
forall a. SrcSpan -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp (SEnv Sort -> a -> CheckM ()
forall a. Checkable a => SEnv Sort -> a -> CheckM ()
check SEnv Sort
γ a
t) of
    Left (ChError () -> Located String
f)  -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Located String -> String
forall a. Located a -> a
val (() -> Located String
f ())))
    Right ()
_  -> Maybe Doc
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 ((Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter Expr -> Bool
filterWithTemplate) Expr
p))
  where
    filterAny :: [Expr] -> [Expr]
filterAny = (Expr -> Maybe Expr) -> [Expr] -> [Expr]
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
|| Maybe Expr -> 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 ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
f' ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
conjuncts
    f :: Symbol -> SESearch Sort
f    = (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
γ')
    γ' :: SEnv Sort
γ'   = Symbol -> Sort -> 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 SrcSpan -> CheckM () -> Either ChError ()
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 -> String -> Maybe Expr -> Maybe Expr
forall a. PPrint a => String -> a -> a
notracepp (String
"Removing" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
p) Maybe Expr
forall a. Maybe a
Nothing
                   Right ()
_   -> Expr -> Maybe Expr
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
_ = SEnv Sort -> a -> CheckM ()
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 = CheckM Sort -> CheckM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (CheckM Sort -> CheckM ()) -> CheckM Sort -> CheckM ()
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 =  (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
γ)

  checkSort :: SEnv Sort -> Sort -> Expr -> CheckM ()
checkSort SEnv Sort
γ Sort
s Expr
e = CheckM Sort -> CheckM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (CheckM Sort -> CheckM ()) -> CheckM Sort -> CheckM ()
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           =  (Symbol -> SEnv Sort -> SESearch Sort
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))) = SEnv Sort -> Expr -> CheckM ()
forall a. Checkable a => SEnv Sort -> a -> CheckM ()
check SEnv Sort
γ' Expr
ra
   where
     γ' :: SEnv Sort
γ' = Symbol -> Sort -> SEnv Sort -> 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
_)       = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
strSort
checkExpr Symbol -> SESearch Sort
_ (ECon (I SubcId
_))   = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FInt
checkExpr Symbol -> SESearch Sort
_ (ECon (R Double
_))   = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FReal
checkExpr Symbol -> SESearch Sort
_ (ECon (L Text
_ Sort
s)) = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
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 Maybe Sort
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 CheckM () -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (PImp Expr
p Expr
p')    = (Expr -> CheckM ()) -> [Expr] -> CheckM ()
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'] CheckM () -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (PIff Expr
p Expr
p')    = (Expr -> CheckM ()) -> [Expr] -> CheckM ()
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'] CheckM () -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (PAnd [Expr]
ps)      = (Expr -> CheckM ()) -> [Expr] -> CheckM ()
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 CheckM () -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
f (POr [Expr]
ps)       = (Expr -> CheckM ()) -> [Expr] -> CheckM ()
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 CheckM () -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
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 ()
(Symbol -> SESearch Sort) -> Brel -> Expr -> Expr -> CheckM ()
checkRel Symbol -> SESearch Sort
f Brel
r Expr
e Expr
e' CheckM () -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
_ PKVar{}        = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
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 CheckM () -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
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 ((Symbol -> SESearch Sort)
-> [(Symbol, Sort)] -> Symbol -> SESearch Sort
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 ((Symbol -> SESearch Sort)
-> [(Symbol, Sort)] -> Symbol -> SESearch Sort
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 (Sort -> Sort) -> CheckM Sort -> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr ((Symbol -> SESearch Sort)
-> [(Symbol, Sort)] -> Symbol -> SESearch Sort
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) CheckM Sort -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
t
checkExpr Symbol -> SESearch Sort
_ (ETApp Expr
_ Sort
_)    = String -> CheckM Sort
forall a. HasCallStack => String -> a
error String
"SortCheck.checkExpr: TODO: implement ETApp"
checkExpr Symbol -> SESearch Sort
_ (ETAbs Expr
_ Symbol
_)    = String -> CheckM Sort
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 a -> [(a, b)] -> Maybe b
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup a
x [(a, b)]
bs of
      Just b
s  -> b -> SESearch b
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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) <- String
-> (Expr, Sort, Expr, Sort, Sort) -> (Expr, Sort, Expr, Sort, Sort)
forall a. PPrint a => String -> a -> a
notracepp String
"ELAB-EAPP" ((Expr, Sort, Expr, Sort, Sort) -> (Expr, Sort, Expr, Sort, Sort))
-> ReaderT ChState IO (Expr, Sort, Expr, Sort, Sort)
-> ReaderT ChState IO (Expr, Sort, Expr, Sort, Sort)
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 (ElabEnv -> Symbol -> SESearch Sort
forall a b. (a, b) -> b
snd ElabEnv
f) Expr
e
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TVSubst -> Expr -> Expr
applyExpr Maybe TVSubst
θ Expr
e, Sort -> (TVSubst -> Sort) -> Maybe TVSubst -> Sort
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 (ElabEnv -> Symbol -> SESearch Sort
forall a b. (a, b) -> b
snd ElabEnv
f) Expr
e
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TVSubst -> Expr -> Expr
applyExpr Maybe TVSubst
θ Expr
e, Sort -> (TVSubst -> Sort) -> Maybe TVSubst -> Sort
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
_) =
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
strSort)

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

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

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

elab ElabEnv
_ e :: Expr
e@(PKVar KVar
_ Subst
_) =
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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) (Expr -> (Expr, Sort))
-> ((Expr, Sort) -> Expr) -> (Expr, Sort) -> (Expr, Sort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
su GradInfo
i (Expr -> Expr) -> ((Expr, Sort) -> Expr) -> (Expr, Sort) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Sort) -> Expr
forall a b. (a, b) -> a
fst ((Expr, Sort) -> (Expr, Sort))
-> CheckM (Expr, Sort) -> CheckM (Expr, Sort)
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,) (Sort -> (Expr, Sort)) -> CheckM Sort -> CheckM (Expr, Sort)
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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' <- (Expr -> CheckM (Expr, Sort))
-> [Expr] -> ReaderT ChState IO [(Expr, Sort)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f) [Expr]
ps
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Expr
PAnd ((Expr, Sort) -> Expr
forall a b. (a, b) -> a
fst ((Expr, Sort) -> Expr) -> [(Expr, Sort)] -> [Expr]
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' <- (Expr -> CheckM (Expr, Sort))
-> [Expr] -> ReaderT ChState IO [(Expr, Sort)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f) [Expr]
ps
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Expr
POr ((Expr, Sort) -> Expr
forall a b. (a, b) -> a
fst ((Expr, Sort) -> Expr) -> [(Expr, Sort)] -> [Expr]
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 Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
eq Brel -> Brel -> Bool
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 CheckM (Sort, Sort) -> String -> CheckM (Sort, Sort)
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'
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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 Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Ueq Bool -> Bool -> Bool
|| Brel
r Brel -> Brel -> Bool
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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' <- (Expr -> Sort -> Expr) -> (Expr, Sort) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SymEnv -> Expr -> Sort -> Expr
toInt SymEnv
env) ((Expr, Sort) -> Expr) -> CheckM (Expr, Sort) -> CheckM Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  Expr
e2' <- (Expr -> Sort -> Expr) -> (Expr, Sort) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SymEnv -> Expr -> Sort -> Expr
toInt SymEnv
env) ((Expr, Sort) -> Expr) -> CheckM (Expr, Sort) -> CheckM Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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 (ElabEnv -> [(Symbol, Sort)] -> ElabEnv
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' = Located String -> SymEnv -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
"PExist Args" SymEnv
forall a. Monoid a => a
mempty [(Symbol, Sort)]
bs
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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 (ElabEnv -> [(Symbol, Sort)] -> ElabEnv
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' = Located String -> SymEnv -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
"PAll Args" SymEnv
forall a. Monoid a => a
mempty [(Symbol, Sort)]
bs
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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 (ElabEnv -> [(Symbol, Sort)] -> ElabEnv
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' = Located String -> SymEnv -> Sort -> Sort
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
"ELam Arg" SymEnv
forall a. Monoid a => a
mempty Sort
t
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
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
_) =
  String -> CheckM (Expr, Sort)
forall a. HasCallStack => String -> a
error String
"SortCheck.elab: TODO: implement ETApp"
elab ElabEnv
_ (ETAbs Expr
_ Symbol
_) =
  String -> CheckM (Expr, Sort)
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) (Expr -> Expr) -> CheckM Expr -> CheckM Expr
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 (Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
tyCastName) (Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
x))
eCstAtom ElabEnv
_ Expr
e Sort
t = Expr -> CheckM Expr
forall a. a -> ReaderT ChState IO a
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 Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
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, (a -> SESearch b) -> [(a, b)] -> a -> SESearch b
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 = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
notracepp String
_msg (Expr -> Expr) -> CheckM Expr -> CheckM Expr
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 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" e = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
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'              = (Expr, Sort) -> Expr
forall a b. (a, b) -> a
fst    ((Expr, Sort) -> Expr) -> CheckM (Expr, Sort) -> CheckM Expr
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    = Expr -> Maybe Expr
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
(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
  Expr -> CheckM Expr
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return    (Expr -> CheckM Expr) -> Expr -> CheckM Expr
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)     <- String -> (Expr, Sort) -> (Expr, Sort)
forall a. PPrint a => String -> a -> a
notracepp (String
"elabEApp1: e1 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e1) ((Expr, Sort) -> (Expr, Sort))
-> CheckM (Expr, Sort) -> CheckM (Expr, Sort)
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
  (Expr, Sort, Expr, Sort, Sort)
-> ReaderT ChState IO (Expr, Sort, Expr, Sort, Sort)
forall a. a -> ReaderT ChState IO a
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            = Expr -> Maybe Expr
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
  (Expr, Expr, Sort, Sort, Sort)
-> CheckM (Expr, Expr, Sort, Sort, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TVSubst -> Expr -> Expr
applyExpr (TVSubst -> Maybe TVSubst
forall a. a -> Maybe a
Just TVSubst
su') Expr
e1, Maybe TVSubst -> Expr -> Expr
applyExpr (TVSubst -> Maybe TVSubst
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 ((Expr -> (Expr, Sort) -> Expr) -> Expr -> [(Expr, Sort)] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
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') ((Expr, Sort) -> Sort
forall a b. (a, b) -> b
snd ((Expr, Sort) -> Sort) -> (Expr, Sort) -> Sort
forall a b. (a -> b) -> a -> b
$ [(Expr, Sort)] -> (Expr, Sort)
forall a. HasCallStack => [a] -> a
last [(Expr, Sort)]
es)
  where
    (Expr
e', [(Expr, Sort)]
es')       = SEnv TheorySymbol
-> Expr -> [(Expr, Sort)] -> (Expr, [(Expr, Sort)])
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) = Int -> [(Expr, a)] -> ([(Expr, a)], [(Expr, a)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [(Expr, a)]
es
               in (Expr -> [Expr] -> Expr
eApps Expr
e ((Expr, a) -> Expr
forall a b. (a, b) -> a
fst ((Expr, a) -> Expr) -> [(Expr, a)] -> [Expr]
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 (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
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 = mapPredReft unElab (sr_reft sr) }

unApplySortedReft :: SortedReft -> SortedReft
unApplySortedReft :: SortedReft -> SortedReft
unApplySortedReft SortedReft
sr = SortedReft
sr { sr_reft = mapPredReft unApply (sr_reft 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 Sort -> Sort -> Bool
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 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
applyName = Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
t
unApplyAt Expr
_        = Maybe Sort
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) (Expr, Sort) -> [(Expr, Sort)] -> [(Expr, Sort)]
forall a. a -> [a] -> [a]
: [(Expr, Sort)]
acc) Expr
e1
    go [(Expr, Sort)]
_   e :: Expr
e@EApp{}             = String -> (Expr, [(Expr, Sort)])
forall a. HasCallStack => String -> a
errorstar (String -> (Expr, [(Expr, Sort)]))
-> String -> (Expr, [(Expr, Sort)])
forall a b. (a -> b) -> a -> b
$ String
"UNEXPECTED: splitArgs: EApp without output type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
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 [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++) ([Sort] -> [Sort]) -> (t -> [Sort]) -> t -> [Sort]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Visitor [Sort] () -> () -> [Sort] -> t -> [Sort]
forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> a
Vis.fold Visitor [Sort] ()
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    = (Visitor [KVar] t
forall {t}. Visitor [KVar] t
forall acc ctx. Monoid acc => Visitor acc ctx
Vis.defaultVisitor :: Vis.Visitor [KVar] t) { Vis.accExpr = go }
    go :: p -> Expr -> [Sort]
go p
_ (EApp (ECst (EVar Symbol
f) Sort
t) Expr
_)   -- get types needed for [NOTE:apply-monomorphism]
           | Symbol
f Symbol -> Symbol -> Bool
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 = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe (String -> Sort
forall a. String -> a
panic String
err') (Expr -> Maybe Sort
exprSortMaybe Expr
e)
  where
    err' :: String
err'        = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"exprSort [%s] on unexpected expression %s" String
msg (Expr -> String
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) = Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
s
    go (ELam (Symbol
_, Sort
sx) Expr
e) = Sort -> Sort -> Sort
FFunc Sort
sx (Sort -> Sort) -> Maybe Sort -> Maybe Sort
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 (Sort -> Sort) -> Maybe Sort -> Maybe Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Sort
go Expr
e
      = Sort -> (TVSubst -> Sort) -> Maybe TVSubst -> Sort
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
s (TVSubst -> Sort -> Sort
`apply` Sort
s) (Maybe TVSubst -> Sort) -> Maybe (Maybe TVSubst) -> Maybe Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Sort -> Sort -> Maybe TVSubst
`unifySorts` Sort
sx) (Sort -> Maybe TVSubst) -> Maybe Sort -> Maybe (Maybe TVSubst)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Sort
go Expr
ex)
    go Expr
_ = Maybe Sort
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
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2]
  (Sort, Sort) -> CheckM (Sort, Sort)
forall a. a -> ReaderT ChState IO a
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 <- (ChState -> SrcSpan) -> ReaderT ChState IO SrcSpan
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> SrcSpan
chSpan
  IO a -> CheckM a
forall a. IO a -> ReaderT ChState IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> CheckM a) -> IO a -> CheckM a
forall a b. (a -> b) -> a -> b
$ ChError -> IO a
forall e a. Exception e => e -> IO a
throwIO ((() -> Located String) -> ChError
ChError (\()
_ -> SrcSpan -> String -> Located String
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 -> String -> CheckM Sort
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) (TVSubst -> Sort) -> CheckM TVSubst -> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f Maybe Expr
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) (TVSubst -> Sort) -> CheckM TVSubst -> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f Maybe Expr
e' [Sort
t1] [Sort
t2]) CheckM Sort -> String -> CheckM Sort
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' = Expr -> Maybe Expr
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 (Sort -> Maybe Sort
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) (TVSubst -> Sort) -> CheckM TVSubst -> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t] [Sort
t']) CheckM Sort -> String -> CheckM Sort
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
  = (TVSubst, Sort) -> Sort
forall a b. (a, b) -> b
snd ((TVSubst, Sort) -> Sort)
-> ReaderT ChState IO (TVSubst, Sort) -> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> ReaderT ChState IO (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 (Sort -> Maybe Sort
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
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t'] [Sort
t]
       Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> CheckM Sort) -> Sort -> CheckM Sort
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 -> ReaderT ChState IO (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    = Expr -> Maybe Expr
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
(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    -> (TVSubst, Sort) -> ReaderT ChState IO (TVSubst, Sort)
forall a. a -> ReaderT ChState IO a
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
(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
                     (TVSubst, Sort) -> ReaderT ChState IO (TVSubst, Sort)
forall a. a -> ReaderT ChState IO a
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 CheckM () -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
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
  = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FInt

checkOpTy Symbol -> SESearch Sort
_ Expr
_ Sort
FReal Sort
FReal
  = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
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
  = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FReal
checkOpTy Symbol -> SESearch Sort
_ Expr
_ Sort
FReal Sort
FInt
  = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
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 (Expr -> Maybe Expr
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) CheckM () -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
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'
  = String -> CheckM Sort
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
       Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort
t Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
FFrac) (CheckM () -> CheckM ()) -> CheckM () -> CheckM ()
forall a b. (a -> b) -> a -> b
$ String -> CheckM ()
forall a. String -> CheckM a
throwErrorAt (Sort -> String
errNonFractional Sort
s)
checkFractional Symbol -> SESearch Sort
_ Sort
s
  = Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort -> Bool
isReal Sort
s) (CheckM () -> CheckM ()) -> CheckM () -> CheckM ()
forall a b. (a -> b) -> a -> b
$ String -> CheckM ()
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
       Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort
t Sort -> [Sort] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Sort
FNum, Sort
FFrac, Sort
intSort, Sort
FInt]) (String -> CheckM ()
forall a. String -> CheckM a
throwErrorAt (String -> CheckM ()) -> String -> CheckM ()
forall a b. (a -> b) -> a -> b
$ Sort -> String
errNonNumeric Sort
s)
checkNumeric Symbol -> SESearch Sort
_ Sort
s
  = Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort -> Bool
isNumeric Sort
s) (String -> CheckM ()
forall a. String -> CheckM a
throwErrorAt (String -> CheckM ()) -> String -> CheckM ()
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 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
b
  = TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
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
_        -> String -> CheckM TVSubst
forall a. String -> CheckM a
throwErrorAt (String -> CheckM TVSubst) -> String -> CheckM TVSubst
forall a b. (a -> b) -> a -> b
$ Maybe String -> Maybe Expr -> Sort -> Sort -> String
errUnifyMsg (String -> Maybe String
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 CheckM Sort -> (Sort -> CheckM ()) -> CheckM ()
forall a b.
ReaderT ChState IO a
-> (a -> ReaderT ChState IO b) -> ReaderT ChState IO b
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 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
boolSort = () -> CheckM ()
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise     = String -> CheckM ()
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
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2] CheckM TVSubst -> String -> CheckM TVSubst
forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` HasCallStack => Expr -> Sort -> Sort -> String
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 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
l'
                             = ((Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric Symbol -> SESearch Sort
f Sort
s1 CheckM () -> CheckM () -> CheckM ()
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Symbol -> SESearch Sort) -> Sort -> CheckM ()
checkNumeric Symbol -> SESearch Sort
f Sort
s2) CheckM () -> String -> CheckM ()
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 = () -> CheckM ()
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FInt  Sort
FReal = () -> CheckM ()
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FReal Sort
FInt  = () -> CheckM ()
forall a. a -> ReaderT ChState IO a
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 CheckM () -> String -> CheckM ()
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 CheckM () -> String -> CheckM ()
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 CheckM () -> String -> CheckM ()
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 CheckM () -> String -> CheckM ()
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      = CheckM TVSubst -> CheckM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2] CheckM TVSubst -> String -> CheckM TVSubst
forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` HasCallStack => Expr -> Sort -> Sort -> String
Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2)
checkRelTy Symbol -> SESearch Sort
f Expr
e Brel
Ne Sort
t1 Sort
t2      = CheckM TVSubst -> CheckM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2] CheckM TVSubst -> String -> CheckM TVSubst
forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` HasCallStack => Expr -> Sort -> Sort -> String
Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2)
checkRelTy Symbol -> SESearch Sort
_ Expr
e Brel
_  Sort
t1 Sort
t2      = Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort
t1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t2) (String -> CheckM ()
forall a. String -> CheckM a
throwErrorAt (String -> CheckM ()) -> String -> CheckM ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => Expr -> Sort -> Sort -> String
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 = Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
b1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b2) (String -> CheckM ()
forall a. String -> CheckM a
throwErrorAt (String -> CheckM ()) -> String -> CheckM ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => Expr -> Sort -> Sort -> String
Expr -> Sort -> Sort -> String
errRel Expr
e Sort
s1 Sort
s2)
  where
    b1 :: Bool
b1            = Sort
s1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
boolSort
    b2 :: Bool
b2            = Sort
s2 Sort -> Sort -> Bool
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) = TVSubst -> Maybe TVSubst
forall a. a -> Maybe a
Just (TVSubst -> Maybe TVSubst) -> TVSubst -> Maybe TVSubst
forall a b. (a -> b) -> a -> b
$ [TVSubst] -> TVSubst
forall a. Monoid a => [a] -> a
mconcat ([TVSubst] -> TVSubst) -> [TVSubst] -> TVSubst
forall a b. (a -> b) -> a -> b
$ [Maybe TVSubst] -> [TVSubst]
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
_
  = Maybe TVSubst
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 (Maybe Sort -> Maybe Sort) -> Maybe Sort -> Maybe Sort
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 (Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
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
_)) = Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
t1
    getArg Maybe Sort
_                   = 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 SrcSpan -> CheckM TVSubst -> Either ChError TVSubst
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
_   -> Maybe TVSubst
forall a. Maybe a
Nothing
      Right TVSubst
su -> TVSubst -> Maybe TVSubst
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 SrcSpan -> CheckM Sort -> Either ChError Sort
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
_  -> Maybe Sort
forall a. Maybe a
Nothing
      Right Sort
t -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
t


--------------------------------------------------------------------------------
unifyTo1M :: Env -> [Sort] -> CheckM Sort
--------------------------------------------------------------------------------
unifyTo1M :: (Symbol -> SESearch Sort) -> [Sort] -> CheckM Sort
unifyTo1M Symbol -> SESearch Sort
_ []     = String -> CheckM Sort
forall a. String -> a
panic String
"unifyTo1: empty list"
unifyTo1M Symbol -> SESearch Sort
f (Sort
t0:[Sort]
ts) = (TVSubst, Sort) -> Sort
forall a b. (a, b) -> b
snd ((TVSubst, Sort) -> Sort)
-> ReaderT ChState IO (TVSubst, Sort) -> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((TVSubst, Sort) -> Sort -> ReaderT ChState IO (TVSubst, Sort))
-> (TVSubst, Sort) -> [Sort] -> ReaderT ChState IO (TVSubst, Sort)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (TVSubst, Sort) -> Sort -> ReaderT ChState IO (TVSubst, Sort)
step (TVSubst
emptySubst, Sort
t0) [Sort]
ts
  where
    step :: (TVSubst, Sort) -> Sort -> CheckM (TVSubst, Sort)
    step :: (TVSubst, Sort) -> Sort -> ReaderT ChState IO (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 Maybe Expr
forall a. Maybe a
Nothing TVSubst
su Sort
t Sort
t'
      (TVSubst, Sort) -> ReaderT ChState IO (TVSubst, Sort)
forall a. a -> ReaderT ChState IO a
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 Symbol -> SESearch Sort
forall {a} {a}. PPrint a => a -> a
emptyEnv
  where
    emptyEnv :: a -> a
emptyEnv a
x = Error -> a
forall a. Error -> a
die (Error -> a) -> Error -> a
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ Doc
"SortCheck: lookup in Empty Env: " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> a -> Doc
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 Maybe Expr
forall a. Maybe a
Nothing Sort
t1 Sort
t2
unifyFast Bool
True  Symbol -> SESearch Sort
_ Sort
t1 Sort
t2
  | Sort
t1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t2        = TVSubst -> Maybe TVSubst
forall a. a -> Maybe a
Just TVSubst
emptySubst
  | Bool
otherwise           = Maybe TVSubst
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
(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'
  | [Sort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Sort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts' = (TVSubst -> (Sort, Sort) -> CheckM TVSubst)
-> TVSubst -> [(Sort, Sort)] -> CheckM TVSubst
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Sort -> Sort -> CheckM TVSubst) -> (Sort, Sort) -> CheckM TVSubst
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Sort -> Sort -> CheckM TVSubst)
 -> (Sort, Sort) -> CheckM TVSubst)
-> (TVSubst -> Sort -> Sort -> CheckM TVSubst)
-> TVSubst
-> (Sort, Sort)
-> CheckM TVSubst
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
θ ([(Sort, Sort)] -> CheckM TVSubst)
-> [(Sort, Sort)] -> CheckM TVSubst
forall a b. (a -> b) -> a -> b
$ [Sort] -> [Sort] -> [(Sort, Sort)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Sort]
ts [Sort]
ts'
  | Bool
otherwise               = String -> CheckM TVSubst
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
(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
  = TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
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
(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
(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
  = TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
unify1 Symbol -> SESearch Sort
_ Maybe Expr
_ !TVSubst
θ Sort
FInt  Sort
FReal = TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ

unify1 Symbol -> SESearch Sort
_ Maybe Expr
_ !TVSubst
θ Sort
FReal Sort
FInt  = TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
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 CheckM () -> String -> CheckM ()
forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Maybe Expr -> Sort -> Sort -> String
errUnify Maybe Expr
e Sort
t Sort
FInt
  TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
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 CheckM () -> String -> CheckM ()
forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Maybe Expr -> Sort -> Sort -> String
errUnify Maybe Expr
e Sort
FInt Sort
t
  TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
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
(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 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t2
  = TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
  | Bool
otherwise
  = String -> CheckM TVSubst
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 Int -> Int -> Bool
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 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$! Sort
t1
    !t2' :: Sort
t2'                    = Int -> Sort -> Sort -> Sort
subst Int
j Sort
tj (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$! Sort
t2

subst !Int
j !Sort
tj (FAbs !Int
i !Sort
t)
  | Int
i Int -> Int -> Bool
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
      Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return  (Sort -> CheckM Sort) -> Sort -> CheckM Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort -> Sort
subst Int
i (Int -> Sort
FVar Int
v) Sort
t''
    go !Sort
t' =
      Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
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 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t' then TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ else TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sort -> TVSubst -> TVSubst
updateVar Int
j Sort
t' TVSubst
θ)
      Maybe Sort
Nothing       -> TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
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) -> TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst -> CheckM TVSubst) -> TVSubst -> CheckM TVSubst
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> TVSubst -> TVSubst
updateVar Int
i Sort
t (TVSubst -> TVSubst) -> TVSubst -> TVSubst
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> TVSubst -> TVSubst
updateVar Int
j Sort
t TVSubst
θ
      Just !Sort
t'       -> if Sort
t Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t' then TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
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        -> TVSubst -> CheckM TVSubst
forall a. a -> ReaderT ChState IO a
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) = Sort -> Maybe Sort -> Sort
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 Symbol -> Symbol -> Bool
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) = (Sort, Sort, TVSubst) -> CheckM (Sort, Sort, TVSubst)
forall a. a -> ReaderT ChState IO a
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
                                (Sort, Sort, TVSubst) -> CheckM (Sort, Sort, TVSubst)
forall a. a -> ReaderT ChState IO a
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             = String -> CheckM (Sort, Sort, TVSubst)
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
(Int -> TVSubst -> String -> String)
-> (TVSubst -> String)
-> ([TVSubst] -> String -> String)
-> Show TVSubst
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> TVSubst -> String -> String
showsPrec :: Int -> TVSubst -> String -> String
$cshow :: TVSubst -> String
show :: TVSubst -> String
$cshowList :: [TVSubst] -> String -> String
showList :: [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 HashMap Int Sort -> HashMap Int Sort -> HashMap Int Sort
forall a. Semigroup a => a -> a -> a
<> HashMap Int Sort
s2)

instance Monoid TVSubst where
  mempty :: TVSubst
mempty  = HashMap Int Sort -> TVSubst
Th HashMap Int Sort
forall a. Monoid a => a
mempty
  mappend :: TVSubst -> TVSubst -> TVSubst
mappend = TVSubst -> TVSubst -> TVSubst
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)   = Int -> HashMap Int Sort -> Maybe Sort
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 (Int -> Sort -> HashMap Int Sort -> HashMap Int Sort
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 HashMap Int Sort
forall k v. HashMap k v
M.empty

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

errElabExpr   :: Expr -> String
errElabExpr :: Expr -> String
errElabExpr Expr
e = String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Elaborate fails on %s" (Expr -> String
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
  = String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Cannot unify %s with %s %s %s"
      (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t1) {- (show t1) -} (Sort -> String
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
"<< " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
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 Maybe String
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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e

errUnifyMany :: [Sort] -> [Sort] -> String
errUnifyMany :: [Sort] -> [Sort] -> String
errUnifyMany [Sort]
ts [Sort]
ts'  = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Cannot unify types with different cardinalities %s and %s"
                         ([Sort] -> String
forall a. PPrint a => a -> String
showpp [Sort]
ts) ([Sort] -> String
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
(HasCallStack => String) -> String
traced ((HasCallStack => String) -> String)
-> (HasCallStack => String) -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Invalid Relation %s with operand types %s and %s"
                         (Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e) (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t1) (Sort -> String
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 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t'          = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Operands have non-numeric types %s in %s"
                         (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t) (Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e)
  | Bool
otherwise        = String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Operands have different types %s and %s in %s"
                         (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t) (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t') (Expr -> String
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   = String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Mismatched branches in Ite: then %s : %s, else %s : %s"
                         (Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e1) (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t1) (Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e2) (Sort -> String
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       = String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Cannot cast %s of sort %s to incompatible sort %s"
                         (Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e) (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t') (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t)

errUnboundAlts :: Symbol -> [Symbol] -> String
errUnboundAlts :: Symbol -> [Symbol] -> String
errUnboundAlts Symbol
x [Symbol]
xs  = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Unbound symbol %s --- perhaps you meant: %s ?"
                         (Symbol -> String
forall a. PPrint a => a -> String
showpp Symbol
x) (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
", " (Symbol -> String
forall a. PPrint a => a -> String
showpp (Symbol -> String) -> [Symbol] -> [String]
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   = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The sort %s is not a function with at least %s arguments\n" (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t) (Int -> String
forall a. PPrint a => a -> String
showpp Int
i)

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

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

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

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