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

-- | 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, unApplyAt
  , toInt

  -- * Predicates on Sorts
  , isFirstOrder
  , isMono

  , runCM0
  ) where

--  import           Control.DeepSeq
import           Control.Monad
import           Control.Monad.Except      -- (MonadError(..))
import           Control.Monad.State.Strict

import qualified Data.HashMap.Strict       as M
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 Debug.Trace

--------------------------------------------------------------------------------
-- | 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
forall t. Visitable t => (Expr -> Expr) -> t -> t
Vis.mapExpr 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' -> 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 (Located String) (Expr, Sort)
forall a. SrcSpan -> CheckM a -> Either (Located String) 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 Located String
e   -> 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 (Located String) Sort
forall a. SrcSpan -> CheckM a -> Either (Located String) a
runCM0 SrcSpan
l ((Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e) of
    Left  Located String
e -> 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
e))
    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 (Located String) Sort
forall a. SrcSpan -> CheckM a -> Either (Located String) a
runCM0 SrcSpan
sp ((Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e) of
    Left Located String
_   -> 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   = StateT ChState (Either ChError)
type ChError  = Located String
data ChState  = ChS { ChState -> Int
chCount :: 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 :: CheckM a -> String -> CheckM a
CheckM a
act withError :: CheckM a -> String -> CheckM a
`withError` String
msg = CheckM a
act CheckM a -> (Located String -> CheckM a) -> CheckM a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (\Located String
e -> Located String -> CheckM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (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 (Located String) a
runCM0 SrcSpan
sp CheckM a
act = (a, ChState) -> a
forall a b. (a, b) -> a
fst ((a, ChState) -> a)
-> Either (Located String) (a, ChState)
-> Either (Located String) a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CheckM a -> ChState -> Either (Located String) (a, ChState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT CheckM a
act (Int -> SrcSpan -> ChState
ChS Int
42 SrcSpan
sp)

fresh :: CheckM Int
fresh :: CheckM Int
fresh = do
  !Int
n <- (ChState -> Int) -> CheckM Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ChState -> Int
chCount
  (ChState -> ChState) -> StateT ChState (Either (Located String)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ChState -> ChState)
 -> StateT ChState (Either (Located String)) ())
-> (ChState -> ChState)
-> StateT ChState (Either (Located String)) ()
forall a b. (a -> b) -> a -> b
$ \ChState
s -> ChState
s { chCount :: Int
chCount = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ChState -> Int
chCount ChState
s }
  Int -> CheckM 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
-> StateT ChState (Either (Located String)) ()
-> Either (Located String) ()
forall a. SrcSpan -> CheckM a -> Either (Located String) a
runCM0 SrcSpan
sp (SEnv Sort -> a -> StateT ChState (Either (Located String)) ()
forall a.
Checkable a =>
SEnv Sort -> a -> StateT ChState (Either (Located String)) ()
check SEnv Sort
γ' a
t) of
    Left Located String
e  -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Located String -> String
forall a. Located a -> a
val Located String
e))
    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
-> StateT ChState (Either (Located String)) ()
-> Either (Located String) ()
forall a. SrcSpan -> CheckM a -> Either (Located String) a
runCM0 SrcSpan
sp (SEnv Sort
-> Sort -> a -> StateT ChState (Either (Located String)) ()
forall a.
Checkable a =>
SEnv Sort
-> Sort -> a -> StateT ChState (Either (Located String)) ()
checkSort SEnv Sort
γ' Sort
s a
t) of
    Left Located String
e  -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Located String -> String
forall a. Located a -> a
val Located String
e))
    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
-> StateT ChState (Either (Located String)) ()
-> Either (Located String) ()
forall a. SrcSpan -> CheckM a -> Either (Located String) a
runCM0 SrcSpan
sp (SEnv Sort -> a -> StateT ChState (Either (Located String)) ()
forall a.
Checkable a =>
SEnv Sort -> a -> StateT ChState (Either (Located String)) ()
check SEnv Sort
γ a
t) of
    Left Located String
e   -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Located String -> String
forall a. Located a -> a
val Located String
e))
    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
-> StateT ChState (Either (Located String)) ()
-> Either (Located String) ()
forall a. SrcSpan -> CheckM a -> Either (Located String) a
runCM0 SrcSpan
dummySpan ((Symbol -> SESearch Sort)
-> Expr -> StateT ChState (Either (Located String)) ()
checkPred Symbol -> SESearch Sort
f Expr
p) of
                   Left Located String
_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 -> StateT ChState (Either (Located String)) ()
forall a.
Checkable a =>
SEnv Sort -> a -> StateT ChState (Either (Located String)) ()
check SEnv Sort
γ

instance Checkable Expr where
  check :: SEnv Sort -> Expr -> StateT ChState (Either (Located String)) ()
check SEnv Sort
γ Expr
e = CheckM Sort -> StateT ChState (Either (Located String)) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (CheckM Sort -> StateT ChState (Either (Located String)) ())
-> CheckM Sort -> StateT ChState (Either (Located String)) ()
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 -> StateT ChState (Either (Located String)) ()
checkSort SEnv Sort
γ Sort
s Expr
e = CheckM Sort -> StateT ChState (Either (Located String)) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (CheckM Sort -> StateT ChState (Either (Located String)) ())
-> CheckM Sort -> StateT ChState (Either (Located String)) ()
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 -> StateT ChState (Either (Located String)) ()
check SEnv Sort
γ (RR Sort
s (Reft (Symbol
v, Expr
ra))) = SEnv Sort -> Expr -> StateT ChState (Either (Located String)) ()
forall a.
Checkable a =>
SEnv Sort -> a -> StateT ChState (Either (Located String)) ()
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 -> StateT ChState (Either (Located String)) ()
checkPred Symbol -> SESearch Sort
f Expr
p StateT ChState (Either (Located String)) ()
-> 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 -> StateT ChState (Either (Located String)) ())
-> [Expr] -> StateT ChState (Either (Located String)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Symbol -> SESearch Sort)
-> Expr -> StateT ChState (Either (Located String)) ()
checkPred Symbol -> SESearch Sort
f) [Expr
p, Expr
p'] StateT ChState (Either (Located String)) ()
-> 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 -> StateT ChState (Either (Located String)) ())
-> [Expr] -> StateT ChState (Either (Located String)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Symbol -> SESearch Sort)
-> Expr -> StateT ChState (Either (Located String)) ()
checkPred Symbol -> SESearch Sort
f) [Expr
p, Expr
p'] StateT ChState (Either (Located String)) ()
-> 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 -> StateT ChState (Either (Located String)) ())
-> [Expr] -> StateT ChState (Either (Located String)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Symbol -> SESearch Sort)
-> Expr -> StateT ChState (Either (Located String)) ()
checkPred Symbol -> SESearch Sort
f) [Expr]
ps StateT ChState (Either (Located String)) ()
-> 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 -> StateT ChState (Either (Located String)) ())
-> [Expr] -> StateT ChState (Either (Located String)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Symbol -> SESearch Sort)
-> Expr -> StateT ChState (Either (Located String)) ()
checkPred Symbol -> SESearch Sort
f) [Expr]
ps StateT ChState (Either (Located String)) ()
-> 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') = (Symbol -> SESearch Sort)
-> Brel
-> Expr
-> Expr
-> StateT ChState (Either (Located String)) ()
checkRel Symbol -> SESearch Sort
f Brel
r Expr
e Expr
e' StateT ChState (Either (Located String)) ()
-> 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 -> StateT ChState (Either (Located String)) ()
checkPred Symbol -> SESearch Sort
f Expr
e StateT ChState (Either (Located String)) ()
-> 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.
--------------------------------------------------------------------------------
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))
-> StateT
     ChState (Either (Located String)) (Expr, Sort, Expr, Sort, Sort)
-> StateT
     ChState (Either (Located String)) (Expr, Sort, Expr, Sort, Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv
-> Expr
-> Expr
-> StateT
     ChState (Either (Located String)) (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
-> StateT
     ChState (Either (Located String)) (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) (EIte Expr
p Expr
e1 Expr
e2) = 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
e1
  (Expr
e2', Sort
s2) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  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]
-> StateT ChState (Either (Located String)) [(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]
-> StateT ChState (Either (Located String)) [(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. 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, Sort) -> CheckM (Expr, Sort)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
eq (Expr -> Sort -> Expr
ECst Expr
e1' Sort
t1') (Expr -> Sort -> Expr
ECst Expr
e2' Sort
t2') , 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"

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 (EIte b e1 e2) = EIte b <$> go e1 <*> go 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       <- (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
-> StateT
     ChState (Either (Located String)) (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
  (Sort
s1', Sort
s2', Sort
s) <- (Symbol -> SESearch Sort)
-> Expr -> Expr -> Sort -> Sort -> CheckM (Sort, Sort, Sort)
elabAppSort Symbol -> SESearch Sort
g Expr
e1 Expr
e2 Sort
s1 Sort
s2
  (Expr, Sort, Expr, Sort, Sort)
-> StateT
     ChState (Either (Located String)) (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 (Sort, Sort, Sort)
elabAppSort :: (Symbol -> SESearch Sort)
-> Expr -> Expr -> Sort -> Sort -> CheckM (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
  (Sort, Sort, Sort) -> CheckM (Sort, Sort, Sort)
forall (m :: * -> *) a. Monad m => a -> m a
return           ((Sort, Sort, Sort) -> CheckM (Sort, Sort, Sort))
-> (Sort, Sort, Sort) -> CheckM (Sort, Sort, Sort)
forall a b. (a -> b) -> a -> b
$ (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
forall t. Visitable t => t -> t
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 :: (Vis.Visitable t) => t -> t
unElab :: t -> t
unElab = t -> t
forall t. Visitable t => t -> t
Vis.stripCasts (t -> t) -> (t -> t) -> t -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> t
forall t. Visitable t => t -> t
unApply

unApply :: (Vis.Visitable t) => t -> t
unApply :: t -> t
unApply = Visitor () () -> () -> () -> t -> t
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 <- (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 
  SrcSpan
sp <- (ChState -> SrcSpan)
-> StateT ChState (Either (Located String)) SrcSpan
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ChState -> SrcSpan
chSpan 
  Located String -> CheckM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SrcSpan -> String -> Located String
forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
sp String
err)

-- | 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 -> StateT ChState (Either (Located String)) ()
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

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
<$> (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. 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
<$> (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. 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)
-> StateT ChState (Either (Located String)) (TVSubst, Sort)
-> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> SESearch Sort)
-> Maybe Sort
-> Expr
-> Expr
-> StateT ChState (Either (Located String)) (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
θ  <- (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
-> StateT ChState (Either (Located String)) (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        <- (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)
-> StateT ChState (Either (Located String)) (TVSubst, Sort)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst
su, Sort
t)
    Just Sort
t'    -> do 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)
-> StateT ChState (Either (Located String)) (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 -> StateT ChState (Either (Located String)) ()
checkNumeric Symbol -> SESearch Sort
f Sort
t StateT ChState (Either (Located String)) ()
-> 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
_ Sort
t Sort
t'
  | Sort
t Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t'
  = (Symbol -> SESearch Sort)
-> Sort -> StateT ChState (Either (Located String)) ()
checkNumeric Symbol -> SESearch Sort
f Sort
t StateT ChState (Either (Located String)) ()
-> 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

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 -> StateT ChState (Either (Located String)) ()
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
-> StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort
t Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
FFrac) (StateT ChState (Either (Located String)) ()
 -> StateT ChState (Either (Located String)) ())
-> StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT ChState (Either (Located String)) ()
forall a. String -> CheckM a
throwErrorAt (Sort -> String
errNonFractional Sort
s)
checkFractional Symbol -> SESearch Sort
_ Sort
s
  = Bool
-> StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort -> Bool
isReal Sort
s) (StateT ChState (Either (Located String)) ()
 -> StateT ChState (Either (Located String)) ())
-> StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT ChState (Either (Located String)) ()
forall a. String -> CheckM a
throwErrorAt (Sort -> String
errNonFractional Sort
s)

checkNumeric :: Env -> Sort -> CheckM ()
checkNumeric :: (Symbol -> SESearch Sort)
-> Sort -> StateT ChState (Either (Located String)) ()
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
-> StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
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 -> StateT ChState (Either (Located String)) ()
forall a. String -> CheckM a
throwErrorAt (String -> StateT ChState (Either (Located String)) ())
-> String -> StateT ChState (Either (Located String)) ()
forall a b. (a -> b) -> a -> b
$ Sort -> String
errNonNumeric Sort
s)
checkNumeric Symbol -> SESearch Sort
_ Sort
s
  = Bool
-> StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort -> Bool
isNumeric Sort
s) (String -> StateT ChState (Either (Located String)) ()
forall a. String -> CheckM a
throwErrorAt (String -> StateT ChState (Either (Located String)) ())
-> String -> StateT ChState (Either (Located String)) ()
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 -> StateT ChState (Either (Located String)) ()
checkPred Symbol -> SESearch Sort
f Expr
e = (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e CheckM Sort
-> (Sort -> StateT ChState (Either (Located String)) ())
-> StateT ChState (Either (Located String)) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr -> Sort -> StateT ChState (Either (Located String)) ()
checkBoolSort Expr
e

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

-- | Checking Relations
checkRel :: Env -> Brel -> Expr -> Expr -> CheckM ()
checkRel :: (Symbol -> SESearch Sort)
-> Brel
-> Expr
-> Expr
-> StateT ChState (Either (Located String)) ()
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 <- ((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. CheckM a -> String -> CheckM a
`withError` (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
-> StateT ChState (Either (Located String)) ()
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
-> StateT ChState (Either (Located String)) ()
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
-> StateT ChState (Either (Located String)) ()
checkRelTy Symbol -> SESearch Sort
_ Expr
e Brel
Ueq Sort
s1 Sort
s2     = Expr -> Sort -> Sort -> StateT ChState (Either (Located String)) ()
checkURel Expr
e Sort
s1 Sort
s2
checkRelTy Symbol -> SESearch Sort
_ Expr
e Brel
Une Sort
s1 Sort
s2     = Expr -> Sort -> Sort -> StateT ChState (Either (Located String)) ()
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 -> StateT ChState (Either (Located String)) ()
checkNumeric Symbol -> SESearch Sort
f Sort
s1 StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Symbol -> SESearch Sort)
-> Sort -> StateT ChState (Either (Located String)) ()
checkNumeric Symbol -> SESearch Sort
f Sort
s2) StateT ChState (Either (Located String)) ()
-> String -> StateT ChState (Either (Located String)) ()
forall a. CheckM a -> String -> CheckM a
`withError` (Symbol -> Symbol -> String
errNonNumerics Symbol
l Symbol
l')
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FReal Sort
FReal = () -> StateT ChState (Either (Located String)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FInt  Sort
FReal = () -> StateT ChState (Either (Located String)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
_ Expr
_ Brel
_ Sort
FReal Sort
FInt  = () -> StateT ChState (Either (Located String)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkRelTy Symbol -> SESearch Sort
f Expr
_ Brel
_ Sort
FInt  Sort
s2    = (Symbol -> SESearch Sort)
-> Sort -> StateT ChState (Either (Located String)) ()
checkNumeric    Symbol -> SESearch Sort
f Sort
s2 StateT ChState (Either (Located String)) ()
-> String -> StateT ChState (Either (Located String)) ()
forall a. 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 -> StateT ChState (Either (Located String)) ()
checkNumeric    Symbol -> SESearch Sort
f Sort
s1 StateT ChState (Either (Located String)) ()
-> String -> StateT ChState (Either (Located String)) ()
forall a. 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 -> StateT ChState (Either (Located String)) ()
checkFractional Symbol -> SESearch Sort
f Sort
s2 StateT ChState (Either (Located String)) ()
-> String -> StateT ChState (Either (Located String)) ()
forall a. 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 -> StateT ChState (Either (Located String)) ()
checkFractional Symbol -> SESearch Sort
f Sort
s1 StateT ChState (Either (Located String)) ()
-> String -> StateT ChState (Either (Located String)) ()
forall a. 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 -> StateT ChState (Either (Located String)) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ((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. CheckM a -> String -> CheckM a
`withError` (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 -> StateT ChState (Either (Located String)) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ((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. CheckM a -> String -> CheckM a
`withError` (Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2))
checkRelTy Symbol -> SESearch Sort
_ Expr
e Brel
_  Sort
t1 Sort
t2      = Bool
-> StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort
t1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t2) (String -> StateT ChState (Either (Located String)) ()
forall a. String -> CheckM a
throwErrorAt (String -> StateT ChState (Either (Located String)) ())
-> String -> StateT ChState (Either (Located String)) ()
forall a b. (a -> b) -> a -> b
$ Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2)

checkURel :: Expr -> Sort -> Sort -> CheckM ()
checkURel :: Expr -> Sort -> Sort -> StateT ChState (Either (Located String)) ()
checkURel Expr
e Sort
s1 Sort
s2 = Bool
-> StateT ChState (Either (Located String)) ()
-> StateT ChState (Either (Located String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
b1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b2) (String -> StateT ChState (Either (Located String)) ()
forall a. String -> CheckM a
throwErrorAt (String -> StateT ChState (Either (Located String)) ())
-> String -> StateT ChState (Either (Located String)) ()
forall a b. (a -> b) -> a -> b
$ 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
--------------------------------------------------------------------------------

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
--------------------------------------------------------------------------------
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 (Located String) TVSubst
forall a. SrcSpan -> CheckM a -> Either (Located String) 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 Located String
_   -> 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 (Located String) Sort
forall a. SrcSpan -> CheckM a -> Either (Located String) a
runCM0 SrcSpan
dummySpan ((Symbol -> SESearch Sort) -> [Sort] -> CheckM Sort
unifyTo1M Symbol -> SESearch Sort
f [Sort]
ts) of
      Left Located String
_  -> 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)
-> StateT ChState (Either (Located String)) (TVSubst, Sort)
-> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((TVSubst, Sort)
 -> Sort
 -> StateT ChState (Either (Located String)) (TVSubst, Sort))
-> (TVSubst, Sort)
-> [Sort]
-> StateT ChState (Either (Located String)) (TVSubst, Sort)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (TVSubst, Sort)
-> Sort -> StateT ChState (Either (Located String)) (TVSubst, Sort)
step (TVSubst
emptySubst, Sort
t0) [Sort]
ts
  where 
    step :: (TVSubst, Sort) -> Sort -> CheckM (TVSubst, Sort)
    step :: (TVSubst, Sort)
-> Sort -> StateT ChState (Either (Located String)) (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)
-> StateT ChState (Either (Located String)) (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 = (Symbol -> SESearch Sort)
-> Maybe Expr -> Sort -> Sort -> Maybe TVSubst
unify Symbol -> SESearch Sort
f Maybe Expr
forall a. Maybe a
Nothing
unifyFast Bool
True  Symbol -> SESearch Sort
_ = Sort -> Sort -> Maybe TVSubst
forall a. Eq a => a -> a -> Maybe TVSubst
uMono
  where
    uMono :: a -> a -> Maybe TVSubst
uMono a
t1 a
t2
     | a
t1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
t2   = TVSubst -> Maybe TVSubst
forall a. a -> Maybe a
Just TVSubst
emptySubst
     | Bool
otherwise  = Maybe TVSubst
forall a. Maybe a
Nothing



--------------------------------------------------------------------------------
unifys :: 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 = (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
e TVSubst
emptySubst

unifyMany :: 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')
  = (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
  (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
  (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 -> StateT ChState (Either (Located String)) ()
checkNumeric Symbol -> SESearch Sort
f Sort
t StateT ChState (Either (Located String)) ()
-> String -> StateT ChState (Either (Located String)) ()
forall a. 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 -> StateT ChState (Either (Located String)) ()
checkNumeric Symbol -> SESearch Sort
f Sort
t StateT ChState (Either (Located String)) ()
-> String -> StateT ChState (Either (Located String)) ()
forall a. 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
  (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
forall t. Visitable t => (Expr -> Expr) -> t -> t
Vis.mapExpr 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

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 :: Expr -> Sort -> Sort -> String
errRel :: Expr -> Sort -> Sort -> String
errRel Expr
e Sort
t1 Sort
t2       = 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)