{-# LANGUAGE CPP                   #-}
{-# LANGUAGE Strict                #-}
{-# LANGUAGE StrictData            #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# 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
  , exprSort_maybe

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

  -- * Apply Substitution
  , apply
  , defuncEApp

  -- * Exported Sorts
  , boolSort
  , strSort

  -- * Sort-Directed Transformations
  , Elaborate (..)
  , applySorts
  , unElab, unElabSortedReft, unApplyAt
  , toInt

  -- * Predicates on Sorts
  , isFirstOrder
  , isMono

  , runCM0
  ) where

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

import qualified Data.HashMap.Strict       as M
import           Data.IORef
import qualified Data.List                 as L
import           Data.Maybe                (mapMaybe, fromMaybe, catMaybes, isJust)
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup            (Semigroup (..))
#endif


import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Misc
import           Language.Fixpoint.Types hiding   (subst)
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 => 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 (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
    { cm :: HashMap SubcId (SimpC a)
cm      = Located String -> SymEnv -> SimpC a -> SimpC a
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
x SymEnv
senv (SimpC a -> SimpC a)
-> HashMap SubcId (SimpC a) -> HashMap SubcId (SimpC a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm      SInfo a
si
    , bs :: BindEnv
bs      = Located String -> SymEnv -> BindEnv -> BindEnv
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
x SymEnv
senv  (BindEnv -> BindEnv) -> BindEnv -> BindEnv
forall a b. (a -> b) -> a -> b
$  SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs      SInfo a
si
    , asserts :: [Triggered Expr]
asserts = Located String -> SymEnv -> Triggered Expr -> Triggered Expr
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
x SymEnv
senv (Triggered Expr -> Triggered Expr)
-> [Triggered Expr] -> [Triggered Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInfo a -> [Triggered Expr]
forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts SInfo a
si
    }

instance (Elaborate e) => (Elaborate (Triggered e)) where
  elaborate :: Located String -> SymEnv -> Triggered e -> Triggered e
elaborate Located String
x SymEnv
env Triggered e
t = (e -> e) -> Triggered e -> Triggered e
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 (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 :: [Equation]
aenvEqs   = Located String -> SymEnv -> [Equation] -> [Equation]
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
msg SymEnv
env (AxiomEnv -> [Equation]
aenvEqs AxiomEnv
ae) 
    -- MISSING SORTS OOPS, aenvSimpl = elaborate msg env (aenvSimpl ae) 
    }

instance Elaborate Rewrite where 
  elaborate :: Located String -> SymEnv -> Rewrite -> Rewrite
elaborate Located String
msg SymEnv
env Rewrite
rw = Rewrite
rw { smBody :: Expr
smBody = Located String -> SymEnv -> Expr -> Expr
skipElabExpr Located String
msg SymEnv
env' (Rewrite -> Expr
smBody Rewrite
rw) } 
    where 
      env' :: SymEnv
env' = SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv SymEnv
env [(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 :: Expr
eqBody = Located String -> SymEnv -> Expr -> Expr
skipElabExpr Located String
msg SymEnv
env' (Equation -> Expr
eqBody Equation
eq) } 
    where
      env' :: SymEnv
env' = SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv SymEnv
env (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq) 

instance Elaborate Expr where
  elaborate :: Located String -> SymEnv -> Expr -> Expr
elaborate Located String
msg SymEnv
env = Expr -> Expr
elabNumeric (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 Elaborate BindEnv where
  elaborate :: Located String -> SymEnv -> BindEnv -> BindEnv
elaborate Located String
z SymEnv
env = (Int -> (Symbol, SortedReft) -> (Symbol, SortedReft))
-> BindEnv -> BindEnv
mapBindEnv (\Int
i (Symbol
x, SortedReft
sr) -> (Symbol
x, Located String -> SymEnv -> SortedReft -> SortedReft
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (Int -> Symbol -> SortedReft -> Located String
forall a a a.
(Show a, Show a, Show a) =>
a -> a -> a -> Located String
z' Int
i Symbol
x SortedReft
sr) SymEnv
env SortedReft
sr))
    where
      z' :: a -> a -> a -> Located String
z' a
i  a
x a
sr  = Located String
z { val :: String
val = (Located String -> String
forall a. Located a -> a
val Located String
z) String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> a -> a -> String
forall a a a. (Show a, Show a, Show a) => a -> a -> a -> String
msg a
i a
x a
sr }
      msg :: a -> a -> a -> String
msg a
i a
x a
sr  = [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 :: Expr
_crhs = Located String -> SymEnv -> Expr -> Expr
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
msg' SymEnv
env (SimpC a -> Expr
forall a. SimpC a -> Expr
_crhs SimpC a
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
f) 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
    f :: Symbol -> SESearch Sort
f    = (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 :: 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
t ()
_ -> a
t) 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 :: 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 :: 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 (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))
    )

runCM0 :: SrcSpan -> CheckM a -> Either ChError a
runCM0 :: 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
  IORef Int
rn <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
42
  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
rn 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 (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> CheckM Int) -> IO Int -> CheckM Int
forall a b. (a -> b) -> a -> b
$ do
    Int
n <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
rn
    IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Int
rn (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return 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 :: 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 :: 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 :: 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 (m :: * -> *) a. Monad m => a -> m a
return Sort
strSort
checkExpr Symbol -> SESearch Sort
_ (ECon (I SubcId
_))   = Sort -> CheckM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FInt
checkExpr Symbol -> SESearch Sort
_ (ECon (R Double
_))   = Sort -> CheckM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FReal
checkExpr Symbol -> SESearch Sort
_ (ECon (L Text
_ Sort
s)) = Sort -> CheckM Sort
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
boolSort
checkExpr Symbol -> SESearch Sort
_ (PKVar {})     = Sort -> CheckM Sort
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
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 :: (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIte Expr
p' (Expr -> Sort -> Expr
cast Expr
e1' Sort
s) (Expr -> Sort -> Expr
cast 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 (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIte Expr
p' (Expr -> Sort -> Expr
cast Expr
e1' Sort
s) (Expr -> Sort -> Expr
cast 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 (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 (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 (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 (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)
mapM (ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f) [Expr]
ps
  (Expr, Sort) -> CheckM (Expr, Sort)
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)
mapM (ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f) [Expr]
ps
  (Expr, Sort) -> CheckM (Expr, Sort)
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 (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 (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 (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 (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 (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 (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 (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 (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 (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 :: (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)

cast :: Expr -> Sort -> Expr
cast :: Expr -> Sort -> Expr
cast (ECst Expr
e Sort
_) Sort
t = Expr -> Sort -> Expr
ECst Expr
e Sort
t
cast Expr
e          Sort
t = Expr -> Sort -> Expr
ECst Expr
e Sort
t

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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return           ((Expr, Expr, Sort, Sort, Sort)
 -> CheckM (Expr, Expr, Sort, Sort, Sort))
-> (Expr, Expr, Sort, Sort, Sort)
-> CheckM (Expr, Expr, Sort, Sort, Sort)
forall a b. (a -> b) -> a -> b
$ (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, Sort)]
es = (Expr -> (Expr, Sort) -> Expr) -> Expr -> [(Expr, Sort)] -> Expr
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'
  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 :: 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 -> Expr
Vis.stripCasts 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 :: Reft
sr_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
unElab (SortedReft -> Reft
sr_reft SortedReft
sr) }

unApply :: Expr -> Expr
unApply :: Expr -> Expr
unApply = Visitor () () -> () -> () -> Expr -> Expr
forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
Vis.trans (Visitor () ()
forall acc ctx. Monoid acc => Visitor acc ctx
Vis.defaultVisitor { txExpr :: () -> Expr -> Expr
Vis.txExpr = (Expr -> Expr) -> () -> Expr -> Expr
forall a b. a -> b -> a
const 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 :: 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 p. Visitor [Sort] p
vis () []
  where
    defs :: [Sort]
defs   = [Sort -> Sort -> Sort
FFunc Sort
t1 Sort
t2 | Sort
t1 <- [Sort]
basicSorts, Sort
t2 <- [Sort]
basicSorts]
    vis :: Visitor [Sort] p
vis    = (forall t. Visitor [KVar] t
forall acc ctx. Monoid acc => Visitor acc ctx
Vis.defaultVisitor :: Vis.Visitor [KVar] t) { accExpr :: p -> Expr -> [Sort]
Vis.accExpr = p -> Expr -> [Sort]
forall p. p -> Expr -> [Sort]
go }
    go :: p -> Expr -> [Sort]
go p
_ (EApp (ECst (EVar Symbol
f) Sort
t) Expr
_)   -- get types needed for [NOTE:apply-monomorphism]
           | Symbol
f 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
exprSort_maybe 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)

exprSort_maybe :: Expr -> Maybe Sort
exprSort_maybe :: Expr -> Maybe Sort
exprSort_maybe = 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 (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 :: 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 (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 (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 (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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
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 (m :: * -> *) a. Monad m => a -> m a
return Sort
FInt

checkOpTy Symbol -> SESearch Sort
_ Expr
_ Sort
FReal Sort
FReal
  = Sort -> CheckM Sort
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 (m :: * -> *) a. Monad m => a -> m a
return Sort
FReal
checkOpTy Symbol -> SESearch Sort
_ Expr
_ Sort
FReal Sort
FInt
  = Sort -> CheckM Sort
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
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 (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 (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
checkEqConstr Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
θ Symbol
a Sort
t = do
  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 (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 (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 :: (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 (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 (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FInt  Sort
FReal = () -> CheckM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FReal Sort
FInt  = () -> CheckM ()
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
exprSort_maybe Expr
e1
  Sort
t2 <- Expr -> Maybe Sort
exprSort_maybe 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 (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 b a. b -> a
emptyEnv
  where
    emptyEnv :: b -> a
emptyEnv = a -> b -> a
forall a b. a -> b -> a
const (a -> b -> a) -> a -> b -> a
forall a b. (a -> b) -> a -> b
$ 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
"SortChecl: lookup in Empty Env "


--------------------------------------------------------------------------------
-- | 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 :: (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 :: (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 (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Sort] -> 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 (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 (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
unify1 Symbol -> SESearch Sort
_ Maybe Expr
_ !TVSubst
θ !Sort
FInt  !Sort
FReal = TVSubst -> CheckM TVSubst
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 (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 (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 (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') = do
  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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ else TVSubst -> CheckM TVSubst
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 (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 (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 (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 (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 (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 (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
showList :: [TVSubst] -> String -> String
$cshowList :: [TVSubst] -> String -> String
show :: TVSubst -> String
$cshow :: TVSubst -> String
showsPrec :: Int -> TVSubst -> String -> String
$cshowsPrec :: Int -> TVSubst -> String -> String
Show)

instance Semigroup TVSubst where
  (Th HashMap Int Sort
s1) <> :: TVSubst -> TVSubst -> TVSubst
<> (Th HashMap Int Sort
s2) = HashMap Int Sort -> TVSubst
Th (HashMap Int Sort
s1 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 :: 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)