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

-- | 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
  , globalEnv
  , theoryEnv

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

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

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

  -- * Apply Substitution
  , apply
  , defuncEApp

  -- * Exported Sorts
  , boolSort
  , strSort

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

  -- * Predicates on Sorts
  , isFirstOrder
  , isMono

--  , runCM0
  ) where

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

import           Data.Bifunctor (first, second)
import qualified Data.IntMap.Strict       as M
import qualified Data.HashSet              as S
import           Data.IORef
import qualified Data.List                 as L
import           Data.Maybe                (mapMaybe, fromMaybe, isJust)
import qualified Data.HashMap.Strict       as HashMap
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Misc
import           Language.Fixpoint.Types hiding   (subst, GInfo(..), senv)
import qualified Language.Fixpoint.Types.Config as Cfg
import qualified Language.Fixpoint.Types.Visitor  as Vis
import qualified Language.Fixpoint.Smt.Theories   as Thy
import           Text.PrettyPrint.HughesPJ.Compat
import           Text.Printf

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

--import Debug.Trace as Debug

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

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

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


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

type ElabM = Reader Cfg.ElabFlags

data ElabParam = ElabParam
  { ElabParam -> ElabFlags
epFlags :: Cfg.ElabFlags
  , ElabParam -> Located String
epMsg   :: Located String
  , ElabParam -> SymEnv
epEnv   :: SymEnv
  }

class Elaborate a where
  elaborate :: HasCallStack => ElabParam -> a -> a


instance (Loc a) => Elaborate (SInfo a) where
  elaborate :: HasCallStack => ElabParam -> SInfo a -> SInfo a
elaborate ElabParam
ep SInfo a
si = SInfo a
si
    { F.cm      = elaborate ep <$> F.cm      si
    , F.bs      = elaborate ep  $  F.bs      si
    , F.gLits   = coerceSort (epFlags ep) <$> F.gLits   si
    , F.dLits   = coerceSort (epFlags ep) <$> F.dLits   si
    , F.asserts = elaborate ep <$> F.asserts si
    , F.defns   = elaborate ep  $ F.defns    si
    , F.ddecls  = coerceDataDecl (epFlags ep) <$> F.ddecls si
    }


instance (Elaborate e) => (Elaborate (Triggered e)) where
  elaborate :: HasCallStack => ElabParam -> Triggered e -> Triggered e
elaborate ElabParam
ep Triggered e
t = ElabParam -> e -> e
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate ElabParam
ep (e -> e) -> Triggered e -> Triggered e
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Triggered e
t

instance (Elaborate a) => (Elaborate (Maybe a)) where
  elaborate :: HasCallStack => ElabParam -> Maybe a -> Maybe a
elaborate ElabParam
ep Maybe a
t = ElabParam -> a -> a
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate ElabParam
ep (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
t

instance Elaborate Sort where
  elaborate :: HasCallStack => ElabParam -> Sort -> Sort
elaborate ElabParam
ep =  ElabFlags -> Sort -> Sort
coerceSort (ElabParam -> ElabFlags
epFlags ElabParam
ep) (Sort -> Sort) -> (Sort -> Sort) -> Sort -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: HasCallStack => ElabParam -> AxiomEnv -> AxiomEnv
elaborate ElabParam
ep AxiomEnv
ae = AxiomEnv
ae
    { aenvEqs   = elaborate ep (aenvEqs ae)
    -- MISSING SORTS OOPS, aenvSimpl = elaborate msg env (aenvSimpl ae)
    }

instance Elaborate Rewrite where
  elaborate :: HasCallStack => ElabParam -> Rewrite -> Rewrite
elaborate ElabParam
ep Rewrite
rw = Rewrite
rw { smBody = skipElabExpr ep' (smBody rw) }
    where
      ep' :: ElabParam
ep' = ElabParam
ep { epEnv = insertsSymEnv (epEnv ep) undefined }


instance Elaborate Equation where
  elaborate :: HasCallStack => ElabParam -> Equation -> Equation
elaborate ElabParam
ep Equation
eq = Equation
eq { eqBody = skipElabExpr ep' (eqBody eq) }
    where
      ep' :: ElabParam
ep' = ElabParam
ep { epEnv = insertsSymEnv (epEnv ep) (eqArgs eq) }


instance Elaborate DefinedFuns where
  elaborate :: HasCallStack => ElabParam -> DefinedFuns -> DefinedFuns
elaborate ElabParam
ep (MkDefinedFuns [Equation]
eqs) = [Equation] -> DefinedFuns
MkDefinedFuns (ElabParam -> Equation -> Equation
elabDefinedEqn ElabParam
ep (Equation -> Equation) -> [Equation] -> [Equation]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Equation]
eqs)

elabDefinedEqn :: ElabParam -> Equation -> Equation
elabDefinedEqn :: ElabParam -> Equation -> Equation
elabDefinedEqn ElabParam
ep Equation
eq = Equation
eq { eqBody = elaborateExpr ep' (eqBody eq) (Just t')
                          , eqArgs = [(x, tx t) | (x, t) <- eqArgs eq ]
                          , eqSort = t'
                          }
  where
    ep' :: ElabParam
ep' = ElabParam
ep { epEnv = insertsSymEnv (epEnv ep) (eqArgs eq) }
    tx :: Sort -> Sort
tx  = ElabFlags -> Sort -> Sort
coerceSort (ElabParam -> ElabFlags
epFlags ElabParam
ep)
    t' :: Sort
t'  = Sort -> Sort
tx (Equation -> Sort
forall v. EquationV v -> Sort
eqSort Equation
eq)

instance Elaborate Expr where
  elaborate :: HasCallStack => ElabParam -> Expr -> Expr
elaborate ElabParam
p Expr
e = HasCallStack => ElabParam -> Expr -> Maybe Sort -> Expr
ElabParam -> Expr -> Maybe Sort -> Expr
elaborateExpr ElabParam
p Expr
e Maybe Sort
forall a. Maybe a
Nothing

elaborateExpr :: HasCallStack => ElabParam -> Expr -> Maybe Sort -> Expr
elaborateExpr :: HasCallStack => ElabParam -> Expr -> Maybe Sort -> Expr
elaborateExpr (ElabParam ElabFlags
ef Located String
msg SymEnv
env) Expr
e Maybe Sort
t =
  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
. HasCallStack => ElabParam -> Maybe Sort -> Expr -> Expr
ElabParam -> Maybe Sort -> Expr -> Expr
elabExpr (ElabFlags -> Located String -> SymEnv -> ElabParam
ElabParam ElabFlags
ef Located String
msg SymEnv
env') Maybe Sort
t (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
elabFMap (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if ElabFlags -> Bool
Cfg.elabSetBag ElabFlags
ef then Expr -> Expr
elabFSetBagZ3 else Expr -> Expr
forall a. a -> a
id) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e
    where
      env' :: SymEnv
env' = ElabFlags -> SymEnv -> SymEnv
coerceEnv ElabFlags
ef SymEnv
env

skipElabExpr :: ElabParam -> Expr -> Expr
skipElabExpr :: ElabParam -> Expr -> Expr
skipElabExpr ElabParam
ep Expr
e = case ElabParam -> Maybe Sort -> Expr -> Either Error Expr
elabExprE ElabParam
ep Maybe Sort
forall a. Maybe a
Nothing 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 (ElabParam -> SymEnv
epEnv ElabParam
ep) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e'

instance Elaborate (Symbol, Sort) where
  elaborate :: HasCallStack => ElabParam -> (Symbol, Sort) -> (Symbol, Sort)
elaborate ElabParam
ep (Symbol
x, Sort
s) = (Symbol
x, ElabParam -> Sort -> Sort
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate ElabParam
ep Sort
s)

instance Elaborate a => Elaborate [a]  where
  elaborate :: HasCallStack => ElabParam -> [a] -> [a]
elaborate ElabParam
ep [a]
xs = ElabParam -> a -> a
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate ElabParam
ep (a -> a) -> [a] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs

elabNumeric :: Expr -> Expr
elabNumeric :: Expr -> Expr
elabNumeric = (Expr -> Expr) -> Expr -> Expr
Vis.mapExprOnExpr Expr -> Expr
go
  where
    go :: Expr -> Expr
go (ETimes Expr
e1 Expr
e2)
      | String -> Expr -> Sort
exprSort String
"txn1" Expr
e1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
FReal
      , String -> Expr -> Sort
exprSort String
"txn2" Expr
e2 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
FReal
      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
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
forall v. ExprV v -> ExprV v -> ExprV v
ERDiv   Expr
e1 Expr
e2
    go Expr
e
      = Expr
e

instance Elaborate SortedReft where
  elaborate :: HasCallStack => ElabParam -> SortedReft -> SortedReft
elaborate ElabParam
ep (RR Sort
s (Reft (Symbol
v, Expr
e))) = Sort -> ReftV Symbol -> SortedReft
RR (ElabFlags -> Sort -> Sort
coerceSort (ElabParam -> ElabFlags
epFlags ElabParam
ep) Sort
s) ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, Expr
e'))
    where
      e' :: Expr
e'   = HasCallStack => ElabParam -> Expr -> Maybe Sort -> Expr
ElabParam -> Expr -> Maybe Sort -> Expr
elaborateExpr ElabParam
ep' Expr
e (Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
boolSort) -- check that a SortedReft is in fact a bool
      ep' :: ElabParam
ep' = ElabParam
ep { epEnv = insertSymEnv v s (epEnv ep) }

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

instance (Loc a) => Elaborate (SimpC a) where
  elaborate :: HasCallStack => ElabParam -> SimpC a -> SimpC a
elaborate ElabParam
ep SimpC a
c = SimpC a
c {_crhs = elaborate ep' (_crhs c) }
    where
      ep' :: ElabParam
ep' = ElabParam
ep { epMsg = atLoc c (val $ epMsg ep) }

-----------------------------------------------------------------------------------
-- | Replace all finset/finmap/finbag theory operations with array-based encodings.
-----------------------------------------------------------------------------------

-- TODO abstract into a visitor for EApp?

-- TODO there's no actual elaboration happening here, just symbol renaming
elabFMap :: Expr -> Expr
elabFMap :: Expr -> Expr
elabFMap (EApp h :: Expr
h@(EVar Symbol
f) Expr
e)
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.mapDef        = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrConstM) (Expr -> Expr
elabFMap Expr
e)
  | Bool
otherwise              = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
elabFMap Expr
h) (Expr -> Expr
elabFMap Expr
e)
elabFMap (EApp (EApp h :: Expr
h@(EVar Symbol
f) Expr
e1) Expr
e2)
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.mapSel        = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrSelectM) (Expr -> Expr
elabFMap Expr
e1)) (Expr -> Expr
elabFMap Expr
e2)
  | Bool
otherwise              = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
elabFMap Expr
h) (Expr -> Expr
elabFMap Expr
e1)) (Expr -> Expr
elabFMap Expr
e2)
elabFMap (EApp (EApp (EApp h :: Expr
h@(EVar Symbol
f) Expr
e1) Expr
e2) Expr
e3)
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.mapSto        = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrStoreM) (Expr -> Expr
elabFMap Expr
e1)) (Expr -> Expr
elabFMap Expr
e2)) (Expr -> Expr
elabFMap Expr
e3)
  | Bool
otherwise              = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
elabFMap Expr
h) (Expr -> Expr
elabFMap Expr
e1)) (Expr -> Expr
elabFMap Expr
e2)) (Expr -> Expr
elabFMap Expr
e3)
elabFMap (EApp Expr
e1 Expr
e2)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
elabFMap Expr
e1) (Expr -> Expr
elabFMap Expr
e2)
elabFMap (ENeg Expr
e)          = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg (Expr -> Expr
elabFMap Expr
e)
elabFMap (EBin Bop
b Expr
e1 Expr
e2)    = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
b (Expr -> Expr
elabFMap Expr
e1) (Expr -> Expr
elabFMap Expr
e2)
elabFMap (ELet Symbol
x Expr
e1 Expr
e2)    = Symbol -> Expr -> Expr -> Expr
forall v. Symbol -> ExprV v -> ExprV v -> ExprV v
ELet Symbol
x (Expr -> Expr
elabFMap Expr
e1) (Expr -> Expr
elabFMap Expr
e2)
elabFMap (EIte Expr
e1 Expr
e2 Expr
e3)   = Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte (Expr -> Expr
elabFMap Expr
e1) (Expr -> Expr
elabFMap Expr
e2) (Expr -> Expr
elabFMap Expr
e3)
elabFMap (ECst Expr
e Sort
t)        = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst (Expr -> Expr
elabFMap Expr
e) Sort
t
elabFMap (ELam (Symbol, Sort)
b Expr
e)        = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol, Sort)
b (Expr -> Expr
elabFMap Expr
e)
elabFMap (ETApp Expr
e Sort
t)       = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ETApp (Expr -> Expr
elabFMap Expr
e) Sort
t
elabFMap (ETAbs Expr
e Symbol
t)       = Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
ETAbs (Expr -> Expr
elabFMap Expr
e) Symbol
t
elabFMap (PAnd [Expr]
es)         = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd (Expr -> Expr
elabFMap (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
elabFMap (POr [Expr]
es)          = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr (Expr -> Expr
elabFMap (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
elabFMap (PNot Expr
e)          = Expr -> Expr
forall v. ExprV v -> ExprV v
PNot (Expr -> Expr
elabFMap Expr
e)
elabFMap (PImp Expr
e1 Expr
e2)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp (Expr -> Expr
elabFMap Expr
e1) (Expr -> Expr
elabFMap Expr
e2)
elabFMap (PIff Expr
e1 Expr
e2)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff (Expr -> Expr
elabFMap Expr
e1) (Expr -> Expr
elabFMap Expr
e2)
elabFMap (PAtom Brel
r Expr
e1 Expr
e2)   = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r (Expr -> Expr
elabFMap Expr
e1) (Expr -> Expr
elabFMap Expr
e2)
elabFMap (PAll   [(Symbol, Sort)]
bs Expr
e)     = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
bs (Expr -> Expr
elabFMap Expr
e)
elabFMap (PExist [(Symbol, Sort)]
bs Expr
e)     = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
bs (Expr -> Expr
elabFMap Expr
e)
elabFMap (ECoerc Sort
a Sort
t Expr
e)    = Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t (Expr -> Expr
elabFMap Expr
e)
elabFMap (PKVar KVar
k (Su HashMap Symbol Expr
m))  = KVar -> SubstV Symbol -> Expr
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k (HashMap Symbol Expr -> SubstV Symbol
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (Expr -> Expr
elabFMap (Expr -> Expr) -> HashMap Symbol Expr -> HashMap Symbol Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol Expr
m))
elabFMap Expr
e                 = Expr
e


elabFSetBagZ3 :: Expr -> Expr
elabFSetBagZ3 :: Expr -> Expr
elabFSetBagZ3 = Expr -> Expr
go
  where
    go :: Expr -> Expr
go (EApp h :: Expr
h@(EVar Symbol
f) Expr
e)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setEmpty = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrConstS) Expr
forall v. ExprV v
PFalse
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setEmp   = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
Eq (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrConstS) Expr
forall v. ExprV v
PFalse) (Expr -> Expr
go Expr
e)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setSng   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrStoreS) (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrConstS) Expr
forall v. ExprV v
PFalse)) (Expr -> Expr
go Expr
e)) Expr
forall v. ExprV v
PTrue
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setCom   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapNotS) (Expr -> Expr
go Expr
e)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.bagEmpty = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrConstB) (Constant -> Expr
forall v. Constant -> ExprV v
ECon (SubcId -> Constant
I SubcId
0))
      | Bool
otherwise         = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
go Expr
h) (Expr -> Expr
go Expr
e)
    go (EApp (EApp h :: Expr
h@(EVar Symbol
f) Expr
e1) Expr
e2)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setMem   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrSelectS) (Expr -> Expr
go Expr
e2)) (Expr -> Expr
go Expr
e1)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setCup   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapOrS) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setCap   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapAndS) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setAdd   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrStoreS) (Expr -> Expr
go Expr
e2)) (Expr -> Expr
go Expr
e1)) Expr
forall v. ExprV v
PTrue
      -- A \ B == A /\ ~B == ~(A => B)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setDif   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapAndS) (Expr -> Expr
go Expr
e1)) (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapNotS) (Expr -> Expr
go Expr
e2))
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.setSub   = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
Eq (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrConstS) Expr
forall v. ExprV v
PTrue) (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapImpS) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2))
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.bagCount = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrSelectB) (Expr -> Expr
go Expr
e2)) (Expr -> Expr
go Expr
e1)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.bagSng   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrStoreB) (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrConstB) (Constant -> Expr
forall v. Constant -> ExprV v
ECon (SubcId -> Constant
I SubcId
0)))) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.bagCup   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapPlusB) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.bagSub   = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
Eq (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrConstS) Expr
forall v. ExprV v
PTrue) (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapLeB) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2))
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.bagMax   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapIteB) (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapGtB) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2))) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
Thy.bagMin   = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapIteB) (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
Thy.arrMapLeB) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2))) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
      | Bool
otherwise         = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
go Expr
h) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    go (EApp Expr
e1 Expr
e2)       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp   (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (ENeg Expr
e)           = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg   (Expr -> Expr
go Expr
e)
    go (EBin Bop
b Expr
e1 Expr
e2)     = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
b (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (ELet Symbol
x Expr
e1 Expr
e2)     = Symbol -> Expr -> Expr -> Expr
forall v. Symbol -> ExprV v -> ExprV v -> ExprV v
ELet Symbol
x (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (EIte Expr
e1 Expr
e2 Expr
e3)    = Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte   (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2) (Expr -> Expr
go Expr
e3)
    go (ECst Expr
e Sort
t)         = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst   (Expr -> Expr
go Expr
e) Sort
t
    go (ELam (Symbol, Sort)
b Expr
e)         = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol, Sort)
b (Expr -> Expr
go Expr
e)
    go (ETApp Expr
e Sort
t)        = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ETApp  (Expr -> Expr
go Expr
e) Sort
t
    go (ETAbs Expr
e Symbol
t)        = Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
ETAbs  (Expr -> Expr
go Expr
e) Symbol
t
    go (PAnd [Expr]
es)          = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd   (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
    go (POr [Expr]
es)           = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr    (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
    go (PNot Expr
e)           = Expr -> Expr
forall v. ExprV v -> ExprV v
PNot   (Expr -> Expr
go Expr
e)
    go (PImp Expr
e1 Expr
e2)       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp   (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PIff Expr
e1 Expr
e2)       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff   (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PAtom Brel
r Expr
e1 Expr
e2)    = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PAll   [(Symbol, Sort)]
bs Expr
e)      = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
bs (Expr -> Expr
go Expr
e)
    go (PExist [(Symbol, Sort)]
bs Expr
e)      = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
bs (Expr -> Expr
go Expr
e)
    go (ECoerc Sort
a Sort
t Expr
e)     = Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t (Expr -> Expr
go Expr
e)
    go (PKVar KVar
k (Su HashMap Symbol Expr
m))   = KVar -> SubstV Symbol -> Expr
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k (HashMap Symbol Expr -> SubstV Symbol
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (Expr -> Expr
go (Expr -> Expr) -> HashMap Symbol Expr -> HashMap Symbol Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol Expr
m))
    go Expr
e                  = Expr
e

-- | Reverse transformation of elabFSetBagZ3: converts array representations back to set/bag operations
unElabFSetBagZ3 :: Expr -> Expr
unElabFSetBagZ3 :: Expr -> Expr
unElabFSetBagZ3 = Expr -> Expr
go
  where
    -- arr_const_s false -> Set_empty
    go :: Expr -> Expr
go (EApp (EVar Symbol
f) Expr
PFalse)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrConstS = Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setEmpty
    -- arr_const_s false == e -> Set_emp e
    go (PAtom Brel
Eq (EApp (EVar Symbol
f) Expr
PFalse) Expr
e)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrConstS = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setEmp) (Expr -> Expr
go Expr
e)
    -- arr_store_s (arr_const_s false) e true -> Set_sng e
    go (EApp (EApp (EApp (EVar Symbol
f1) (EApp (EVar Symbol
f2) Expr
PFalse)) Expr
e) Expr
PTrue)
      | Symbol
f1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrStoreS Bool -> Bool -> Bool
&& Symbol
f2 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrConstS = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setSng) (Expr -> Expr
go Expr
e)
    -- arr_map_not_s e -> Set_com e
    go (EApp (EVar Symbol
f) Expr
e)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapNotS = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setCom) (Expr -> Expr
go Expr
e)
    -- arr_const_b 0 -> Bag_empty
    go (EApp (EVar Symbol
f) (ECon (I SubcId
0)))
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrConstB = Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.bagEmpty
    -- arr_select_s e2 e1 -> Set_mem e1 e2
    go (EApp (EApp (EVar Symbol
f) Expr
e2) Expr
e1)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrSelectS = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setMem) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_map_or_s e1 e2 -> Set_cup e1 e2
    go (EApp (EApp (EVar Symbol
f) Expr
e1) Expr
e2)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapOrS = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setCup) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_map_and_s e1 e2 -> Set_cap e1 e2
    go (EApp (EApp (EVar Symbol
f) Expr
e1) Expr
e2)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapAndS = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setCap) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_store_s e2 e1 true -> Set_add e1 e2
    go (EApp (EApp (EApp (EVar Symbol
f) Expr
e2) Expr
e1) Expr
PTrue)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrStoreS = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setAdd) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_map_and_s e1 (arr_map_not_s e2) -> Set_dif e1 e2
    go (EApp (EApp (EVar Symbol
f1) Expr
e1) (EApp (EVar Symbol
f2) Expr
e2))
      | Symbol
f1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapAndS Bool -> Bool -> Bool
&& Symbol
f2 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapNotS = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setDif) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_const_s true == arr_map_imp_s e1 e2 -> Set_sub e1 e2
    go (PAtom Brel
Eq (EApp (EVar Symbol
f1) Expr
PTrue) (EApp (EApp (EVar Symbol
f2) Expr
e1) Expr
e2))
      | Symbol
f1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrConstS Bool -> Bool -> Bool
&& Symbol
f2 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapImpS = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.setSub) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_select_b e2 e1 -> Bag_count e1 e2
    go (EApp (EApp (EVar Symbol
f) Expr
e2) Expr
e1)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrSelectB = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.bagCount) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_store_b (arr_const_b 0) e1 e2 -> Bag_sng e1 e2
    go (EApp (EApp (EApp (EVar Symbol
f1) (EApp (EVar Symbol
f2) (ECon (I SubcId
0)))) Expr
e1) Expr
e2)
      | Symbol
f1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrStoreB Bool -> Bool -> Bool
&& Symbol
f2 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrConstB = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.bagSng) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_map_plus_b e1 e2 -> Bag_cup e1 e2
    go (EApp (EApp (EVar Symbol
f) Expr
e1) Expr
e2)
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapPlusB = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.bagCup) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_const_s true == arr_map_le_b e1 e2 -> Bag_sub e1 e2
    go (PAtom Brel
Eq (EApp (EVar Symbol
f1) Expr
PTrue) (EApp (EApp (EVar Symbol
f2) Expr
e1) Expr
e2))
      | Symbol
f1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrConstS Bool -> Bool -> Bool
&& Symbol
f2 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapLeB = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.bagSub) (Expr -> Expr
go Expr
e1)) (Expr -> Expr
go Expr
e2)
    -- arr_map_ite_b (arr_map_gt_b e1 e2) e1 e2 -> Bag_max e1 e2
    go (EApp (EApp (EApp (EVar Symbol
f1) (EApp (EApp (EVar Symbol
f2) Expr
e1a) Expr
e2a)) Expr
e1b) Expr
e2b)
      | Symbol
f1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapIteB Bool -> Bool -> Bool
&& Symbol
f2 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapGtB Bool -> Bool -> Bool
&& Expr
e1a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e1b Bool -> Bool -> Bool
&& Expr
e2a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2b
      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.bagMax) (Expr -> Expr
go Expr
e1a)) (Expr -> Expr
go Expr
e2a)
    -- arr_map_ite_b (arr_map_le_b e1 e2) e1 e2 -> Bag_min e1 e2
    go (EApp (EApp (EApp (EVar Symbol
f1) (EApp (EApp (EVar Symbol
f2) Expr
e1a) Expr
e2a)) Expr
e1b) Expr
e2b)
      | Symbol
f1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapIteB Bool -> Bool -> Bool
&& Symbol
f2 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
Thy.arrMapLeB Bool -> Bool -> Bool
&& Expr
e1a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e1b Bool -> Bool -> Bool
&& Expr
e2a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2b
      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
forall a. IsString a => a
Thy.bagMin) (Expr -> Expr
go Expr
e1a)) (Expr -> Expr
go Expr
e2a)
    -- Recursive cases
    go (EApp Expr
e1 Expr
e2)       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp   (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (ENeg Expr
e)           = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg   (Expr -> Expr
go Expr
e)
    go (EBin Bop
b Expr
e1 Expr
e2)     = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
b (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (ELet Symbol
x Expr
e1 Expr
e2)     = Symbol -> Expr -> Expr -> Expr
forall v. Symbol -> ExprV v -> ExprV v -> ExprV v
ELet Symbol
x (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (EIte Expr
e1 Expr
e2 Expr
e3)    = Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte   (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2) (Expr -> Expr
go Expr
e3)
    go (ECst Expr
e Sort
t)         = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst   (Expr -> Expr
go Expr
e) Sort
t
    go (ELam (Symbol, Sort)
b Expr
e)         = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol, Sort)
b (Expr -> Expr
go Expr
e)
    go (ETApp Expr
e Sort
t)        = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ETApp  (Expr -> Expr
go Expr
e) Sort
t
    go (ETAbs Expr
e Symbol
t)        = Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
ETAbs  (Expr -> Expr
go Expr
e) Symbol
t
    go (PAnd [Expr]
es)          = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd   (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
    go (POr [Expr]
es)           = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr    (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
    go (PNot Expr
e)           = Expr -> Expr
forall v. ExprV v -> ExprV v
PNot   (Expr -> Expr
go Expr
e)
    go (PImp Expr
e1 Expr
e2)       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp   (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PIff Expr
e1 Expr
e2)       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff   (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PAtom Brel
r Expr
e1 Expr
e2)    = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PAll   [(Symbol, Sort)]
bs Expr
e)      = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
bs (Expr -> Expr
go Expr
e)
    go (PExist [(Symbol, Sort)]
bs Expr
e)      = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
bs (Expr -> Expr
go Expr
e)
    go (ECoerc Sort
a Sort
t Expr
e)     = Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t (Expr -> Expr
go Expr
e)
    go (PKVar KVar
k (Su HashMap Symbol Expr
m))   = KVar -> SubstV Symbol -> Expr
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k (HashMap Symbol Expr -> SubstV Symbol
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (Expr -> Expr
go (Expr -> Expr) -> HashMap Symbol Expr -> HashMap Symbol Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol Expr
m))
    go Expr
e                  = Expr
e


elabSorts :: Cfg.ElabFlags -> Expr -> Expr
elabSorts :: ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef (EApp Expr
e1 Expr
e2)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e1) (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e2)
elabSorts ElabFlags
ef (ENeg Expr
e)          = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e)
elabSorts ElabFlags
ef (EBin Bop
b Expr
e1 Expr
e2)    = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
b (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e1) (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e2)
elabSorts ElabFlags
ef (ELet Symbol
x Expr
e1 Expr
e2)    = Symbol -> Expr -> Expr -> Expr
forall v. Symbol -> ExprV v -> ExprV v -> ExprV v
ELet Symbol
x (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e1) (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e2)
elabSorts ElabFlags
ef (EIte Expr
e1 Expr
e2 Expr
e3)   = Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e1) (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e2) (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e3)
elabSorts ElabFlags
ef (ECst Expr
e Sort
s)        = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e) (ElabFlags -> Sort -> Sort
coerceSort ElabFlags
ef Sort
s)
elabSorts ElabFlags
ef (ELam (Symbol, Sort)
b Expr
e)        = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol, Sort)
b (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e)
elabSorts ElabFlags
ef (ETApp Expr
e Sort
s)       = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ETApp (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e) (ElabFlags -> Sort -> Sort
coerceSort ElabFlags
ef Sort
s)
elabSorts ElabFlags
ef (ETAbs Expr
e Symbol
t)       = Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
ETAbs (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e) Symbol
t
elabSorts ElabFlags
ef (PAnd [Expr]
es)         = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
elabSorts ElabFlags
ef (POr [Expr]
es)          = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
elabSorts ElabFlags
ef (PNot Expr
e)          = Expr -> Expr
forall v. ExprV v -> ExprV v
PNot (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e)
elabSorts ElabFlags
ef (PImp Expr
e1 Expr
e2)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e1) (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e2)
elabSorts ElabFlags
ef (PIff Expr
e1 Expr
e2)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e1) (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e2)
elabSorts ElabFlags
ef (PAtom Brel
r Expr
e1 Expr
e2)   = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e1) (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e2)
elabSorts ElabFlags
ef (PAll   [(Symbol, Sort)]
bs Expr
e)     = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
bs (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e)
elabSorts ElabFlags
ef (PExist [(Symbol, Sort)]
bs Expr
e)     = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
bs (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e)
elabSorts ElabFlags
ef (ECoerc Sort
s1 Sort
s2 Expr
e)  = Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc (ElabFlags -> Sort -> Sort
coerceSort ElabFlags
ef Sort
s1) (ElabFlags -> Sort -> Sort
coerceSort ElabFlags
ef Sort
s2) (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef Expr
e)
elabSorts ElabFlags
ef (PKVar KVar
k (Su HashMap Symbol Expr
m))  = KVar -> SubstV Symbol -> Expr
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k (HashMap Symbol Expr -> SubstV Symbol
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (ElabFlags -> Expr -> Expr
elabSorts ElabFlags
ef (Expr -> Expr) -> HashMap Symbol Expr -> HashMap Symbol Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol Expr
m))
elabSorts ElabFlags
_ Expr
e                 = Expr
e

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

validateSort :: Env -> Sort -> Maybe Sort -> CheckM ()
-- validateSort f t (Just t') = void (unifys f (tracepp ("validateSort" ++ show (t, t')) Nothing) [t] [t'])
validateSort :: Env -> Sort -> Maybe Sort -> CheckM ()
validateSort Env
f Sort
t (Just Sort
t') = ReaderT ChState IO TVSubst -> CheckM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (HasCallStack =>
Env -> Maybe Expr -> [Sort] -> [Sort] -> ReaderT ChState IO TVSubst
Env -> Maybe Expr -> [Sort] -> [Sort] -> ReaderT ChState IO TVSubst
unifys Env
f Maybe Expr
forall a. Maybe a
Nothing [Sort
t] [Sort
t'])
validateSort Env
_ Sort
_ Maybe Sort
Nothing   = () -> CheckM ()
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

elabExprE :: ElabParam -> Maybe Sort -> Expr -> Either Error Expr
elabExprE :: ElabParam -> Maybe Sort -> Expr -> Either Error Expr
elabExprE (ElabParam ElabFlags
ef Located String
msg SymEnv
env) Maybe Sort
t Expr
e =
  case SrcSpan -> Maybe ElabFlags -> CheckM Expr -> Either ChError Expr
forall a.
SrcSpan -> Maybe ElabFlags -> CheckM a -> Either ChError a
runCM0 (Located String -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan Located String
msg) (ElabFlags -> Maybe ElabFlags
forall a. a -> Maybe a
Just ElabFlags
ef) (CheckM Expr -> Either ChError Expr)
-> CheckM Expr -> Either ChError Expr
forall a b. (a -> b) -> a -> b
$ do
    (!Expr
e', Sort
eSort) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab (SymEnv
env, Env
envLookup) Expr
e
    Env -> Sort -> Maybe Sort -> CheckM ()
validateSort Env
envLookup Sort
eSort Maybe Sort
t
    IORef (Maybe TVSubst)
finalThetaRef <- (ChState -> IORef (Maybe TVSubst))
-> ReaderT ChState IO (IORef (Maybe TVSubst))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> IORef (Maybe TVSubst)
chTVSubst
    Maybe TVSubst
finalTheta <- IO (Maybe TVSubst) -> ReaderT ChState IO (Maybe TVSubst)
forall a. IO a -> ReaderT ChState IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe TVSubst) -> ReaderT ChState IO (Maybe TVSubst))
-> IO (Maybe TVSubst) -> ReaderT ChState IO (Maybe TVSubst)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe TVSubst) -> IO (Maybe TVSubst)
forall a. IORef a -> IO a
readIORef IORef (Maybe TVSubst)
finalThetaRef
    Expr -> CheckM Expr
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TVSubst -> Expr -> Expr
applyExpr Maybe TVSubst
finalTheta Expr
e') of
    Left (ChError () -> Located String
f') ->
      let e' :: Located String
e' = () -> Located String
f' ()
      in Error -> Either Error Expr
forall a b. a -> Either a b
Left (Error -> Either Error Expr) -> Error -> Either Error Expr
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err (Located String -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan Located String
e') (String -> Doc
d (Located String -> String
forall a. Located a -> a
val Located String
e'))
    Right Expr
elab_e -> Expr -> Either Error Expr
forall a b. b -> Either a b
Right Expr
elab_e
  where
    sEnv :: SEnv Sort
sEnv = SymEnv -> SEnv Sort
seSort SymEnv
env
    envLookup :: Env
envLookup = (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
sEnv)
    d :: String -> Doc
d String
m  = [Doc] -> Doc
vcat [ Doc
"elaborate" Doc -> Doc -> Doc
<+> String -> Doc
text (Located String -> String
forall a. Located a -> a
val Located String
msg) Doc -> Doc -> Doc
<+> Doc
"failed on:"
                , Int -> Doc -> Doc
nest Int
4 (Expr -> Doc
forall a. PPrint a => a -> Doc
pprint Expr
e)
                , Doc
"with error"
                , Int -> Doc -> Doc
nest Int
4 (String -> Doc
text String
m)
                , Doc
"in environment"
                , Int -> Doc -> Doc
nest Int
4 (SEnv Sort -> Doc
forall a. PPrint a => a -> Doc
pprint (SEnv Sort -> Doc) -> SEnv Sort -> Doc
forall a b. (a -> b) -> a -> b
$ SEnv Sort -> Expr -> SEnv Sort
forall e a. Subable e => SEnv a -> e -> SEnv a
subEnv SEnv Sort
sEnv Expr
e)
                ]


--------------------------------------------------------------------------------
-- | 'elabApply' replaces all direct function calls indirect calls via `apply`
--------------------------------------------------------------------------------
elabApply :: SymEnv -> Expr -> Expr
elabApply :: SymEnv -> Expr -> Expr
elabApply SymEnv
env = Expr -> Expr
go
  where
    go :: Expr -> Expr
go Expr
e                  = case Expr -> (Expr, [(Expr, Sort)])
splitArgs Expr
e of
                             (Expr
e', []) -> Expr -> Expr
step Expr
e'
                             (Expr
f , [(Expr, Sort)]
es) -> SymEnv -> Expr -> [(Expr, Sort)] -> Expr
defuncEApp SymEnv
env (Expr -> Expr
go Expr
f) ((Expr -> Expr) -> (Expr, Sort) -> (Expr, Sort)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first 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
forall v. ExprV v
PTrue
    step (POr [])         = Expr
forall v. ExprV v
PFalse
    step (ENeg Expr
e)         = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg (Expr -> Expr
go  Expr
e)
    step (EBin Bop
o Expr
e1 Expr
e2)   = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    step (ELet Symbol
x Expr
e1 Expr
e2)   = Symbol -> Expr -> Expr -> Expr
forall v. Symbol -> ExprV v -> ExprV v -> ExprV v
ELet Symbol
x (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    step (EIte Expr
e1 Expr
e2 Expr
e3)  = Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
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
forall v. ExprV v -> Sort -> ExprV v
ECst (Expr -> Expr
go Expr
e) Sort
t
    step (PAnd [Expr]
ps)        = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
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
forall v. [ExprV v] -> ExprV v
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
forall v. ExprV v -> ExprV v
PNot (Expr -> Expr
go Expr
p)
    step (PImp Expr
p Expr
q)       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp (Expr -> Expr
go Expr
p) (Expr -> Expr
go Expr
q)
    step (PIff Expr
p Expr
q)       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff (Expr -> Expr
go Expr
p) (Expr -> Expr
go Expr
q)
    step (PExist [(Symbol, Sort)]
bs Expr
p)    = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
bs (Expr -> Expr
go Expr
p)
    step (PAll   [(Symbol, Sort)]
bs Expr
p)    = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll   [(Symbol, Sort)]
bs (Expr -> Expr
go Expr
p)
    step (PAtom Brel
r Expr
e1 Expr
e2)  = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
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
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol, Sort)
b       (Expr -> Expr
go Expr
e)
    step (ECoerc Sort
a Sort
t Expr
e)   = Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t   (Expr -> Expr
go Expr
e)
    step (PKVar KVar
k (Su HashMap Symbol Expr
m)) = KVar -> SubstV Symbol -> Expr
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k (HashMap Symbol Expr -> SubstV Symbol
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (Expr -> Expr
go (Expr -> Expr) -> HashMap Symbol Expr -> HashMap Symbol Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol Expr
m))
    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 -> Maybe ElabFlags -> CheckM Sort -> Either ChError Sort
forall a.
SrcSpan -> Maybe ElabFlags -> CheckM a -> Either ChError a
runCM0 SrcSpan
l Maybe ElabFlags
forall a. Maybe a
Nothing (Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e) of
    Left (ChError () -> Located String
f') -> Error -> Sort
forall a. HasCallStack => Error -> a
die (Error -> Sort) -> Error -> Sort
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
l (String -> Doc
d (Located String -> String
forall a. Located a -> a
val (() -> Located String
f' ())))
    Right Sort
s -> Sort
s
  where
    f :: Env
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 -> Maybe ElabFlags -> CheckM Sort -> Either ChError Sort
forall a.
SrcSpan -> Maybe ElabFlags -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp Maybe ElabFlags
forall a. Maybe a
Nothing (Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e) of
    Left ChError
_   -> Maybe Sort
forall a. Maybe a
Nothing
    Right Sort
s  -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
s
  where
    f :: Env
f Symbol
x  = case Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
γ of
            Just Sort
z  -> Sort -> SESearch Sort
forall a. a -> SESearch a
Found Sort
z
            Maybe Sort
Nothing -> [Symbol] -> SESearch Sort
forall a. [Symbol] -> SESearch a
Alts []

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


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

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

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

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

data ChState = ChS { ChState -> IORef Int
chCount :: IORef Int
                   , ChState -> SrcSpan
chSpan  :: SrcSpan
                   , ChState -> ElabFlags
chElabF :: Cfg.ElabFlags
                   , ChState -> IORef (Maybe TVSubst)
chTVSubst :: IORef (Maybe TVSubst)
                   }

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


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

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

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

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

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

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

checkSortedReftFull :: Checkable a => SrcSpan -> SEnv SortedReft -> a -> ElabM (Maybe Doc)
checkSortedReftFull :: forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> a -> ElabM (Maybe Doc)
checkSortedReftFull SrcSpan
sp SEnv SortedReft
γ a
t =
  do ElabFlags
ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     Maybe Doc -> ElabM (Maybe Doc)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Doc -> ElabM (Maybe Doc)) -> Maybe Doc -> ElabM (Maybe Doc)
forall a b. (a -> b) -> a -> b
$ case SrcSpan -> Maybe ElabFlags -> CheckM () -> Either ChError ()
forall a.
SrcSpan -> Maybe ElabFlags -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp (ElabFlags -> Maybe ElabFlags
forall a. a -> Maybe a
Just ElabFlags
ef) (SEnv Sort -> a -> CheckM ()
forall a. Checkable a => SEnv Sort -> a -> CheckM ()
check SEnv Sort
γ' a
t) of
              Left (ChError () -> Located String
f)  -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Located String -> String
forall a. Located a -> a
val (() -> Located String
f ())))
              Right ()
_ -> Maybe Doc
forall a. Maybe a
Nothing
  where
    γ' :: SEnv Sort
γ' = SortedReft -> Sort
sr_sort (SortedReft -> Sort) -> SEnv SortedReft -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEnv SortedReft
γ

checkSortFull :: Checkable a => SrcSpan -> SEnv SortedReft -> Sort -> a -> ElabM (Maybe Doc)
checkSortFull :: forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> Sort -> a -> ElabM (Maybe Doc)
checkSortFull SrcSpan
sp SEnv SortedReft
γ Sort
s a
t =
  do ElabFlags
ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     Maybe Doc -> ElabM (Maybe Doc)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Doc -> ElabM (Maybe Doc)) -> Maybe Doc -> ElabM (Maybe Doc)
forall a b. (a -> b) -> a -> b
$ case SrcSpan -> Maybe ElabFlags -> CheckM () -> Either ChError ()
forall a.
SrcSpan -> Maybe ElabFlags -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp (ElabFlags -> Maybe ElabFlags
forall a. a -> Maybe a
Just ElabFlags
ef) (SEnv Sort -> Sort -> a -> CheckM ()
forall a. Checkable a => SEnv Sort -> Sort -> a -> CheckM ()
checkSort SEnv Sort
γ' Sort
s a
t) of
              Left (ChError () -> Located String
f)  -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Located String -> String
forall a. Located a -> a
val (() -> Located String
f ())))
              Right ()
_ -> Maybe Doc
forall a. Maybe a
Nothing
  where
      γ' :: SEnv Sort
γ' = SortedReft -> Sort
sr_sort (SortedReft -> Sort) -> SEnv SortedReft -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEnv SortedReft
γ

checkSorted :: Checkable a => SrcSpan -> SEnv Sort -> a -> ElabM (Maybe Doc)
checkSorted :: forall a.
Checkable a =>
SrcSpan -> SEnv Sort -> a -> ElabM (Maybe Doc)
checkSorted SrcSpan
sp SEnv Sort
γ a
t =
  do ElabFlags
ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     Maybe Doc -> ElabM (Maybe Doc)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Doc -> ElabM (Maybe Doc)) -> Maybe Doc -> ElabM (Maybe Doc)
forall a b. (a -> b) -> a -> b
$ case SrcSpan -> Maybe ElabFlags -> CheckM () -> Either ChError ()
forall a.
SrcSpan -> Maybe ElabFlags -> CheckM a -> Either ChError a
runCM0 SrcSpan
sp (ElabFlags -> Maybe ElabFlags
forall a. a -> Maybe a
Just ElabFlags
ef) (SEnv Sort -> a -> CheckM ()
forall a. Checkable a => SEnv Sort -> a -> CheckM ()
check SEnv Sort
γ a
t) of
              Left (ChError () -> Located String
f) -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Located String -> String
forall a. Located a -> a
val (() -> Located String
f ())))
              Right ()
_  -> Maybe Doc
forall a. Maybe a
Nothing

pruneUnsortedReft :: SEnv Sort -> Templates -> SortedReft -> SortedReft
pruneUnsortedReft :: SEnv Sort -> Templates -> SortedReft -> SortedReft
pruneUnsortedReft SEnv Sort
_ Templates
t SortedReft
r
  | Templates -> Bool
isEmptyTemplates Templates
t
  = SortedReft
r
pruneUnsortedReft SEnv Sort
γ Templates
t (RR Sort
s (Reft (Symbol
v, Expr
p)))
  | Templates -> Bool
isAnyTemplates Templates
t
  -- this is the old code that checks everything
  = Sort -> ReftV Symbol -> SortedReft
RR Sort
s ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, ([Expr] -> [Expr]) -> Expr -> Expr
forall {v} {v}.
(Fixpoint v, Ord v, Eq v) =>
([ExprV v] -> ListNE (ExprV v)) -> ExprV v -> ExprV v
tx [Expr] -> [Expr]
filterAny Expr
p))
  | Bool
otherwise
  = Sort -> ReftV Symbol -> SortedReft
RR Sort
s ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, ([Expr] -> [Expr]) -> Expr -> Expr
forall {v} {v}.
(Fixpoint v, Ord v, Eq v) =>
([ExprV v] -> ListNE (ExprV v)) -> ExprV v -> ExprV v
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 (Env -> Expr -> Maybe Expr
checkPred' Env
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 (Env -> Expr -> Maybe Expr
checkPred' Env
f Expr
e)
    tx :: ([ExprV v] -> ListNE (ExprV v)) -> ExprV v -> ExprV v
tx [ExprV v] -> ListNE (ExprV v)
f' = ListNE (ExprV v) -> ExprV v
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd (ListNE (ExprV v) -> ExprV v)
-> (ExprV v -> ListNE (ExprV v)) -> ExprV v -> ExprV v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExprV v] -> ListNE (ExprV v)
f' ([ExprV v] -> ListNE (ExprV v))
-> (ExprV v -> [ExprV v]) -> ExprV v -> ListNE (ExprV v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprV v -> [ExprV v]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts
    f :: Env
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' :: Env -> Expr -> Maybe Expr
checkPred' Env
f Expr
p = Maybe Expr
res -- traceFix ("checkPred: p = " ++ showFix p) $ res
  where
    res :: Maybe Expr
res        = case SrcSpan -> Maybe ElabFlags -> CheckM () -> Either ChError ()
forall a.
SrcSpan -> Maybe ElabFlags -> CheckM a -> Either ChError a
runCM0 SrcSpan
dummySpan Maybe ElabFlags
forall a. Maybe a
Nothing (Env -> Expr -> CheckM ()
checkPred Env
f Expr
p) of
                   Left ChError
_err -> String -> Maybe Expr -> Maybe Expr
forall a. PPrint a => String -> a -> a
notracepp (String
"Removing" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
p) Maybe Expr
forall a. Maybe a
Nothing
                   Right ()
_   -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
p

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

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

instance Checkable Expr where
  check :: SEnv Sort -> Expr -> CheckM ()
check SEnv Sort
γ Expr
e =
    do ElabFlags
ef <- (ChState -> ElabFlags) -> ReaderT ChState IO ElabFlags
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> ElabFlags
chElabF
       Sort
_ <- Env -> Expr -> CheckM Sort
checkExpr (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` ElabFlags -> SEnv Sort -> SEnv Sort
coerceSortEnv ElabFlags
ef SEnv Sort
γ) Expr
e
       () -> CheckM ()
forall a. a -> ReaderT ChState IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  checkSort :: SEnv Sort -> Sort -> Expr -> CheckM ()
checkSort SEnv Sort
γ Sort
s Expr
e =
    do ElabFlags
ef <- (ChState -> ElabFlags) -> ReaderT ChState IO ElabFlags
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> ElabFlags
chElabF
       Sort
_ <- Env -> Expr -> CheckM Sort
checkExpr (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` ElabFlags -> SEnv Sort -> SEnv Sort
coerceSortEnv ElabFlags
ef SEnv Sort
γ)
                      (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst Expr
e (if ElabFlags -> Bool
Cfg.elabSetBag ElabFlags
ef then Sort -> Sort
coerceSetBagToArray Sort
s' else Sort
s'))
       () -> CheckM ()
forall a. a -> ReaderT ChState IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
   where
      s' :: Sort
s' = Sort -> Sort
coerceMapToArray Sort
s

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

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

checkExpr Env
f (PAll  [(Symbol, Sort)]
bs Expr
e )   = Env -> Expr -> CheckM Sort
checkExpr (Env -> [(Symbol, Sort)] -> Env
forall a b.
Eq a =>
(a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv Env
f [(Symbol, Sort)]
bs) Expr
e
checkExpr Env
f (PExist [(Symbol, Sort)]
bs Expr
e)   = Env -> Expr -> CheckM Sort
checkExpr (Env -> [(Symbol, Sort)] -> Env
forall a b.
Eq a =>
(a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv Env
f [(Symbol, Sort)]
bs) Expr
e
checkExpr Env
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
<$> Env -> Expr -> CheckM Sort
checkExpr (Env -> [(Symbol, Sort)] -> Env
forall a b.
Eq a =>
(a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv Env
f [(Symbol
x,Sort
t)]) Expr
e
checkExpr Env
f (ECoerc Sort
s Sort
t Expr
e)  = Env -> Expr -> CheckM Sort
checkExpr Env
f (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst Expr
e Sort
s) CheckM Sort -> CheckM Sort -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> ReaderT ChState IO b -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
t
checkExpr Env
_ (ETApp Expr
_ Sort
_)     = String -> CheckM Sort
forall a. HasCallStack => String -> a
error String
"SortCheck.checkExpr: TODO: implement ETApp"
checkExpr Env
_ (ETAbs Expr
_ Symbol
_)     = String -> CheckM Sort
forall a. HasCallStack => String -> a
error String
"SortCheck.checkExpr: TODO: implement ETAbs"

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

--------------------------------------------------------------------------------
-- | Elaborate expressions with types to make polymorphic instantiation explicit.
--------------------------------------------------------------------------------
{-# SCC elab #-}
elab :: ElabEnv -> Expr -> CheckM (Expr, Sort)
--------------------------------------------------------------------------------
elab :: ElabEnv -> Expr -> CheckM (Expr, Sort)
elab f :: ElabEnv
f@(!SymEnv
_, !Env
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 <- Env -> Expr -> Sort -> Sort -> CheckM Sort
checkOpTy Env
g Expr
e Sort
s1 Sort
s2
  let !result :: Expr
result = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o (Expr -> Sort -> Expr
eCst Expr
e1' Sort
s1) (Expr -> Sort -> Expr
eCst Expr
e2' Sort
s2)
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
result, Sort
s)

elab !ElabEnv
f (ECst (EApp !Expr
e1 !Expr
e2) Sort
t) = do
   Expr
ee <- ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
elabAppAs ElabEnv
f Sort
t Expr
e1 Expr
e2
   (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Sort -> Expr
eCst Expr
ee Sort
t, Sort
t)

elab !ElabEnv
f (EApp !Expr
e1 !Expr
e2) = do
  (!Expr
e1', !Sort
s1, !Expr
e2', !Sort
s2, !Sort
s) <- ElabEnv -> Expr -> Expr -> CheckM (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)
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
s)

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

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

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

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

-- TODO: the guard below is because some LH tests generate PKVar with ill-sorted substitutions.
-- However, a cleaner solution could be to modify `Sanitize.restrictKVarDomain` to simply
-- those ill-sorted substitutions right up at the outset.
elab !ElabEnv
f e :: Expr
e@(PKVar KVar
k (Su HashMap Symbol Expr
m)) = do
  Bool
expKvars <- (ChState -> Bool) -> ReaderT ChState IO Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (ElabFlags -> Bool
elabExplicitKvars (ElabFlags -> Bool) -> (ChState -> ElabFlags) -> ChState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChState -> ElabFlags
chElabF)
  if Bool
expKvars
    then do
      [(Symbol, Expr)]
xargs' <- [(Symbol, Expr)]
-> ((Symbol, Expr) -> ReaderT ChState IO (Symbol, Expr))
-> ReaderT ChState IO [(Symbol, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (HashMap Symbol Expr -> [(Symbol, Expr)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap Symbol Expr
m) (((Symbol, Expr) -> ReaderT ChState IO (Symbol, Expr))
 -> ReaderT ChState IO [(Symbol, Expr)])
-> ((Symbol, Expr) -> ReaderT ChState IO (Symbol, Expr))
-> ReaderT ChState IO [(Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ \(Symbol
x, Expr
arg) -> do
        (Expr
arg', Sort
_) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
arg
        (Symbol, Expr) -> ReaderT ChState IO (Symbol, Expr)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
x, Expr
arg')
      (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (KVar -> SubstV Symbol -> Expr
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k (HashMap Symbol Expr -> SubstV Symbol
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su ([(Symbol, Expr)] -> HashMap Symbol Expr
forall k v. Hashable k => [(k, v)] -> HashMap k v
HashMap.fromList [(Symbol, Expr)]
xargs')), Sort
boolSort)
    else
      (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
boolSort)

elab (!SymEnv
_, !Env
f) e :: Expr
e@(EVar !Symbol
x) = do
  !Sort
cs <- Env -> Symbol -> CheckM Sort
checkSym Env
f Symbol
x
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
cs)

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

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

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

elab ElabEnv
f (ELet !Symbol
x !Expr
e1 !Expr
e2) = do
  (!Expr
e1', !Sort
t1) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  (!Expr
e2', !Sort
t2) <- 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
t1)]) Expr
e2
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Expr -> Expr -> Expr
forall v. Symbol -> ExprV v -> ExprV v -> ExprV v
ELet Symbol
x Expr
e1' Expr
e2', Sort
t2)

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

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

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

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

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

elab !ElabEnv
f (POr ![Expr]
ps) = do
  ![(Expr, Sort)]
ps' <- (Expr -> CheckM (Expr, Sort))
-> [Expr] -> ReaderT ChState IO [(Expr, Sort)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f) [Expr]
ps
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Expr
forall v. [ExprV v] -> ExprV v
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
_,!Env
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        <- Env -> Expr -> CheckM Sort
checkExpr Env
g Expr
e1
  !Sort
t2        <- Env -> Expr -> CheckM Sort
checkExpr Env
g Expr
e2
  (!Sort
t1',!Sort
t2') <- Env -> Expr -> Sort -> Sort -> CheckM (Sort, Sort)
unite Env
g Expr
e Sort
t1 Sort
t2 CheckM (Sort, Sort) -> String -> CheckM (Sort, Sort)
forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Expr -> String
errElabExpr Expr
e
  !Expr
e1'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
f Sort
t1' Expr
e1
  !Expr
e2'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
f Sort
t2' Expr
e2
  !Expr
e1''      <- ElabEnv -> Expr -> Sort -> CheckM Expr
eCstAtom ElabEnv
f Expr
e1' Sort
t1'
  !Expr
e2''      <- ElabEnv -> Expr -> Sort -> CheckM Expr
eCstAtom ElabEnv
f Expr
e2' Sort
t2'
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
eq Expr
e1'' Expr
e2'', Sort
boolSort)

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

elab f :: ElabEnv
f@(!SymEnv
env,!Env
_) (PAtom !Brel
r !Expr
e1 !Expr
e2) = do
  !Expr
e1' <- (Expr -> Sort -> Expr) -> (Expr, Sort) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SymEnv -> Expr -> Sort -> Expr
toInt SymEnv
env) ((Expr, Sort) -> Expr) -> CheckM (Expr, Sort) -> CheckM Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  !Expr
e2' <- (Expr -> Sort -> Expr) -> (Expr, Sort) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SymEnv -> Expr -> Sort -> Expr
toInt SymEnv
env) ((Expr, Sort) -> Expr) -> CheckM (Expr, Sort) -> CheckM Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
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
  !ElabFlags
ef <- (ChState -> ElabFlags) -> ReaderT ChState IO ElabFlags
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> ElabFlags
chElabF
  let !bs' :: [(Symbol, Sort)]
bs' = ElabParam -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate (ElabFlags -> Located String -> SymEnv -> ElabParam
ElabParam ElabFlags
ef Located String
"PExist Args" SymEnv
forall a. Monoid a => a
mempty) [(Symbol, Sort)]
bs
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
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
  !ElabFlags
ef <- (ChState -> ElabFlags) -> ReaderT ChState IO ElabFlags
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> ElabFlags
chElabF
  let !bs' :: [(Symbol, Sort)]
bs' = ElabParam -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate (ElabFlags -> Located String -> SymEnv -> ElabParam
ElabParam ElabFlags
ef Located String
"PAll Args" SymEnv
forall a. Monoid a => a
mempty) [(Symbol, Sort)]
bs
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
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
  !ElabFlags
ef <- (ChState -> ElabFlags) -> ReaderT ChState IO ElabFlags
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> ElabFlags
chElabF
  let !t' :: Sort
t' = ElabParam -> Sort -> Sort
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate (ElabFlags -> Located String -> SymEnv -> ElabParam
ElabParam ElabFlags
ef Located String
"ELam Arg" SymEnv
forall a. Monoid a => a
mempty) Sort
t
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x, Sort
t') (Expr -> Sort -> Expr
eCst Expr
e' Sort
s), Sort -> Sort -> Sort
FFunc Sort
t Sort
s)

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

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

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

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

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

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

-- DUPLICATION with `checkApp'`
elabAppAs :: ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
elabAppAs :: ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
elabAppAs env :: ElabEnv
env@(SymEnv
_, Env
f) Sort
t Expr
g Expr
e = do
  Sort
gT       <- Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
g
  Sort
eT       <- Env -> Expr -> CheckM Sort
checkExpr Env
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
forall v. ExprV v -> ExprV v -> ExprV v
EApp Expr
g Expr
e)
  TVSubst
su       <- HasCallStack =>
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
unifyMany Env
f Maybe Expr
ge TVSubst
isu [Sort
oT, Sort
iT] [Sort
t, Sort
eT]
  let tg :: Sort
tg    = TVSubst -> Sort -> Sort
apply TVSubst
su Sort
gT
  Expr
g'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
env Sort
tg Expr
g
  let te :: Sort
te    = TVSubst -> Sort -> Sort
apply TVSubst
su Sort
eT
  Expr
e'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
env Sort
te Expr
e
  Expr -> CheckM Expr
forall a. a -> ReaderT ChState IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure     (Expr -> CheckM Expr) -> Expr -> CheckM Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
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 -> CheckM (Expr, Sort, Expr, Sort, Sort)
elabEApp f :: ElabEnv
f@(SymEnv
_, Env
g) Expr
e1 Expr
e2 = do
  (Expr
e1', Sort
s1)     <- {- notracepp ("elabEApp: e1 = " ++ show e1) <$> -} ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  (Expr
e2', Sort
s2)     <- {- notracepp ("elabEApp: e2 = " ++ show e2) <$> -} ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  (Expr
e1'', Expr
e2'', Sort
s1', Sort
s2', Sort
s) <- Env
-> Expr
-> Expr
-> Sort
-> Sort
-> CheckM (Expr, Expr, Sort, Sort, Sort)
elabAppSort Env
g Expr
e1' Expr
e2' Sort
s1 Sort
s2
  (Expr, Sort, Expr, Sort, Sort)
-> CheckM (Expr, Sort, Expr, Sort, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return           (Expr
e1'', Sort
s1', Expr
e2'', Sort
s2', Sort
s)

elabAppSort :: Env -> Expr -> Expr -> Sort -> Sort -> CheckM (Expr, Expr, Sort, Sort, Sort)
elabAppSort :: Env
-> Expr
-> Expr
-> Sort
-> Sort
-> CheckM (Expr, Expr, Sort, Sort, Sort)
elabAppSort Env
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
forall v. ExprV v -> ExprV v -> ExprV v
EApp Expr
e1 Expr
e2)
  (Sort
sIn, Sort
sOut, TVSubst
su) <- Sort -> CheckM (Sort, Sort, TVSubst)
checkFunSort Sort
s1
  TVSubst
su'             <- Env
-> Maybe Expr
-> TVSubst
-> Sort
-> Sort
-> ReaderT ChState IO TVSubst
unify1 Env
f Maybe Expr
e TVSubst
su Sort
sIn Sort
s2
  Maybe TVSubst -> CheckM ()
composeTVSubst (TVSubst -> Maybe TVSubst
forall a. a -> Maybe a
Just TVSubst
su)
  Maybe TVSubst -> CheckM ()
composeTVSubst (TVSubst -> Maybe TVSubst
forall a. a -> Maybe a
Just TVSubst
su')
  (Expr, Expr, Sort, Sort, Sort)
-> CheckM (Expr, Expr, Sort, Sort, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e1 , Expr
e2, TVSubst -> Sort -> Sort
apply TVSubst
su' Sort
s1, TVSubst -> Sort -> Sort
apply TVSubst
su' Sort
s2, TVSubst -> Sort -> Sort
apply TVSubst
su' Sort
sOut)


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

takeArgs :: SEnv TheorySymbol -> Expr -> [(Expr, a)] -> (Expr, [(Expr, a)])
takeArgs :: forall a.
SEnv TheorySymbol -> Expr -> [(Expr, a)] -> (Expr, [(Expr, a)])
takeArgs SEnv TheorySymbol
env Expr
e [(Expr, a)]
es =
  case SEnv TheorySymbol -> Expr -> Maybe Int
Thy.isSmt2App SEnv TheorySymbol
env Expr
e of
    Just Int
n  -> let ([(Expr, a)]
es1, [(Expr, a)]
es2) = Int -> [(Expr, a)] -> ([(Expr, a)], [(Expr, a)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [(Expr, a)]
es
               in (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
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
forall v. ExprV v -> Sort -> ExprV v
ECst (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
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
forall v. ExprV v -> Sort -> ExprV v
ECst (Symbol -> Expr
forall v. v -> ExprV v
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
forall v. ExprV v -> Sort -> ExprV v
ECst (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp Expr
f (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst Expr
e Sort
s)) Sort
FInt
  where
    isSmtInt :: Bool
isSmtInt  = SymEnv -> Sort -> Bool
isNum SymEnv
env Sort
s
    f :: Expr
f         = Sort -> Expr
toIntAt Sort
s

isNum :: SymEnv -> Sort -> Bool
isNum :: SymEnv -> Sort -> Bool
isNum 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
forall v. ExprV v -> Sort -> ExprV v
ECst (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
toIntName) (Sort -> Sort -> Sort
FFunc Sort
s Sort
FInt)

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

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

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

unApply :: Expr -> Expr
unApply :: Expr -> Expr
unApply = (Expr -> Expr) -> Expr -> Expr
Vis.mapExprOnExpr Expr -> Expr
go
  where
    go :: Expr -> Expr
go (ECst (EApp (EApp Expr
f Expr
e1) Expr
e2) Sort
_)
      | Just Sort
_ <- Expr -> Maybe Sort
unApplyAt Expr
f = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp Expr
e1 Expr
e2
    go (ELam (Symbol
x,Sort
s) Expr
e)         = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x, (Sort -> Sort) -> Sort -> Sort
Vis.mapSort Sort -> Sort
go' Sort
s) Expr
e
    go (PExist [(Symbol, Sort)]
bs Expr
e)          = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist (((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> [a] -> [b]
map ((Sort -> Sort) -> (Symbol, Sort) -> (Symbol, Sort)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Sort -> Sort) -> Sort -> Sort
Vis.mapSort Sort -> Sort
go')) [(Symbol, Sort)]
bs) 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)])
forall {v}.
(Ord v, Fixpoint v, PPrint v) =>
[(ExprV v, Sort)] -> ExprV v -> (ExprV v, [(ExprV v, Sort)])
go []
  where
    go :: [(ExprV v, Sort)] -> ExprV v -> (ExprV v, [(ExprV v, Sort)])
go [(ExprV v, Sort)]
acc (ECst (EApp ExprV v
e1 ExprV v
e) Sort
s) = [(ExprV v, Sort)] -> ExprV v -> (ExprV v, [(ExprV v, Sort)])
go ((ExprV v
e, Sort
s) (ExprV v, Sort) -> [(ExprV v, Sort)] -> [(ExprV v, Sort)]
forall a. a -> [a] -> [a]
: [(ExprV v, Sort)]
acc) ExprV v
e1
    go [(ExprV v, Sort)]
_   e :: ExprV v
e@EApp{}             = String -> (ExprV v, [(ExprV v, Sort)])
forall a. HasCallStack => String -> a
errorstar (String -> (ExprV v, [(ExprV v, Sort)]))
-> String -> (ExprV v, [(ExprV v, Sort)])
forall a b. (a -> b) -> a -> b
$ String
"UNEXPECTED: splitArgs: EApp without output type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ExprV v -> String
forall a. PPrint a => a -> String
showpp ExprV v
e
    go [(ExprV v, Sort)]
acc ExprV v
e                    = (ExprV v
e, [(ExprV v, 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.Foldable t => t -> [Sort]
--------------------------------------------------------------------------------
applySorts :: forall t. Foldable t => t -> [Sort]
applySorts = {- tracepp "applySorts" . -} ([Sort]
defs [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++) ([Sort] -> [Sort]) -> (t -> [Sort]) -> t -> [Sort]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Folder [Sort] () -> () -> [Sort] -> t -> [Sort]
forall t a ctx.
(Foldable t, Monoid a) =>
Folder a ctx -> ctx -> a -> t -> a
Vis.fold Folder [Sort] ()
forall {ctx}. Folder [Sort] ctx
vis () []
  where
    defs :: [Sort]
defs   = [Sort -> Sort -> Sort
FFunc Sort
t1 Sort
t2 | Sort
t1 <- [Sort]
basicSorts, Sort
t2 <- [Sort]
basicSorts]
    vis :: Folder [Sort] ctx
vis    = (Folder [KVar] t
forall {t}. Folder [KVar] t
forall acc ctx. Monoid acc => Folder acc ctx
Vis.defaultFolder :: Vis.Folder [KVar] t) { Vis.accExpr = go }
    go :: p -> Expr -> [Sort]
go p
_ (EApp (ECst (EVar Symbol
f) Sort
t) Expr
_)   -- get types needed for [NOTE:apply-monomorphism]
           | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
applyName
           = [Sort
t]
    go p
_ (ECoerc Sort
t1 Sort
t2 Expr
_)             -- get types needed for [NOTE:coerce-apply]
           = [Sort -> Sort -> Sort
FFunc Sort
t1 Sort
t2]
    go p
_ Expr
_ = []

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

exprSortMaybe :: Expr -> Maybe Sort
exprSortMaybe :: Expr -> Maybe Sort
exprSortMaybe = Expr -> Maybe Sort
forall {v}. ExprV v -> Maybe Sort
go
  where
    go :: ExprV v -> Maybe Sort
go (ECst ExprV v
_ Sort
s) = Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
s
    go (ELam (Symbol
_, Sort
sx) ExprV v
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
<$> ExprV v -> Maybe Sort
go ExprV v
e
    go (EApp ExprV v
e ExprV v
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
<$> ExprV v -> Maybe Sort
go ExprV v
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) -> (Sort -> Maybe TVSubst) -> Sort -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> Sort -> Maybe TVSubst
`unifySorts` Sort
sx) (Sort -> Sort) -> Maybe Sort -> Maybe Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprV v -> Maybe Sort
go ExprV v
ex
    go ExprV v
_ = 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 :: Env -> Expr -> Sort -> Sort -> CheckM (Sort, Sort)
unite Env
f Expr
e Sort
t1 Sort
t2 = do
  TVSubst
su <- HasCallStack =>
Env -> Maybe Expr -> [Sort] -> [Sort] -> ReaderT ChState IO TVSubst
Env -> Maybe Expr -> [Sort] -> [Sort] -> ReaderT ChState IO TVSubst
unifys Env
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2]
  (Sort, Sort) -> CheckM (Sort, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst -> Sort -> Sort
apply TVSubst
su Sort
t1, TVSubst -> Sort -> Sort
apply TVSubst
su Sort
t2)

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

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

-- | Helper for checking symbol occurrences
checkSym :: Env -> Symbol -> CheckM Sort
checkSym :: Env -> Symbol -> CheckM Sort
checkSym Env
f Symbol
x = case Env
f Symbol
x of
  Found Sort
s -> Sort -> CheckM Sort
refreshNegativeTyVars Sort
s CheckM Sort -> (Sort -> CheckM Sort) -> CheckM Sort
forall a b.
ReaderT ChState IO a
-> (a -> ReaderT ChState IO b) -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Sort -> CheckM Sort
instantiate
  Alts [Symbol]
xs -> String -> CheckM Sort
forall a. String -> CheckM a
throwErrorAt (Symbol -> [Symbol] -> String
errUnboundAlts Symbol
x [Symbol]
xs)

-- Negative type variables are implictly universally quantified type variables
refreshNegativeTyVars :: Sort -> CheckM Sort
refreshNegativeTyVars :: Sort -> CheckM Sort
refreshNegativeTyVars Sort
s = do
    let negativeSorts :: HashSet Int
negativeSorts = Sort -> HashSet Int
negSort Sort
s
    [(Int, Sort)]
freshVars <- (Int -> ReaderT ChState IO (Int, Sort))
-> [Int] -> ReaderT ChState IO [(Int, Sort)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Int -> ReaderT ChState IO (Int, Sort)
forall {a}. a -> ReaderT ChState IO (a, Sort)
pair ([Int] -> ReaderT ChState IO [(Int, Sort)])
-> [Int] -> ReaderT ChState IO [(Int, Sort)]
forall a b. (a -> b) -> a -> b
$ HashSet Int -> [Int]
forall a. HashSet a -> [a]
S.toList HashSet Int
negativeSorts
    Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> CheckM Sort) -> Sort -> CheckM Sort
forall a b. (a -> b) -> a -> b
$ ((Int, Sort) -> Sort -> Sort) -> Sort -> [(Int, Sort)] -> Sort
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Int -> Sort -> Sort -> Sort) -> (Int, Sort) -> Sort -> Sort
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Sort -> Sort -> Sort
subst) Sort
s [(Int, Sort)]
freshVars
  where
    pair :: a -> ReaderT ChState IO (a, Sort)
pair a
i = do
      Int
f <- CheckM Int
fresh
      (a, Sort) -> ReaderT ChState IO (a, Sort)
forall a. a -> ReaderT ChState IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
i, Int -> Sort
FVar Int
f)

    negSort :: Sort -> HashSet Int
negSort (FVar Int
i) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Int -> HashSet Int
forall a. Hashable a => a -> HashSet a
S.singleton Int
i
    negSort (FAbs Int
_ Sort
s')      = Sort -> HashSet Int
negSort Sort
s'
    negSort (FFunc Sort
s1 Sort
s2)    = Sort -> HashSet Int
negSort Sort
s1 HashSet Int -> HashSet Int -> HashSet Int
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`S.union` Sort -> HashSet Int
negSort Sort
s2
    negSort (FApp Sort
s1 Sort
s2)     = Sort -> HashSet Int
negSort Sort
s1 HashSet Int -> HashSet Int -> HashSet Int
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`S.union` Sort -> HashSet Int
negSort Sort
s2
    negSort Sort
_                = HashSet Int
forall a. HashSet a
S.empty

-- | Helper for checking let expressions
checkLet :: Env -> Symbol -> Expr -> Expr -> CheckM Sort
checkLet :: Env -> Symbol -> Expr -> Expr -> CheckM Sort
checkLet Env
f Symbol
x Expr
e1 Expr
e2 = do
  Sort
t <- Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e1
  Env -> Expr -> CheckM Sort
checkExpr (Env -> [(Symbol, Sort)] -> Env
forall a b.
Eq a =>
(a -> SESearch b) -> [(a, b)] -> a -> SESearch b
addEnv Env
f [(Symbol
x, Sort
t)]) Expr
e2

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

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

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

-- | Helper for checking cast expressions
checkCst :: Env -> Sort -> Expr -> CheckM Sort
checkCst :: Env -> Sort -> Expr -> CheckM Sort
checkCst Env
f Sort
t (EApp Expr
g Expr
e)
  = Env -> Maybe Sort -> Expr -> Expr -> CheckM Sort
checkApp Env
f (Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
t) Expr
g Expr
e
checkCst Env
f Sort
t Expr
e
  = do Sort
t' <- Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e
       TVSubst
su <- HasCallStack =>
Env -> Maybe Expr -> [Sort] -> [Sort] -> ReaderT ChState IO TVSubst
Env -> Maybe Expr -> [Sort] -> [Sort] -> ReaderT ChState IO TVSubst
unifys Env
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t] [Sort
t'] ReaderT ChState IO TVSubst -> String -> ReaderT ChState IO TVSubst
forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Expr -> Sort -> Sort -> String
errCast Expr
e Sort
t' Sort
t
       Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TVSubst -> Sort -> Sort
apply TVSubst
su Sort
t)

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

checkExprAs :: Env -> Sort -> Expr -> CheckM Sort
checkExprAs :: Env -> Sort -> Expr -> CheckM Sort
checkExprAs Env
f Sort
t (EApp Expr
g Expr
e)
  = Env -> Maybe Sort -> Expr -> Expr -> CheckM Sort
checkApp Env
f (Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
t) Expr
g Expr
e
checkExprAs Env
f Sort
t Expr
e
  = do Sort
t' <- Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e
       TVSubst
θ  <- HasCallStack =>
Env -> Maybe Expr -> [Sort] -> [Sort] -> ReaderT ChState IO TVSubst
Env -> Maybe Expr -> [Sort] -> [Sort] -> ReaderT ChState IO TVSubst
unifys Env
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t'] [Sort
t]
       Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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' :: Env
-> Maybe Sort -> Expr -> Expr -> ReaderT ChState IO (TVSubst, Sort)
checkApp' Env
f Maybe Sort
to Expr
g Expr
e = do
  Sort
gt       <- Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
g
  Sort
et       <- Env -> Expr -> CheckM Sort
checkExpr Env
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
forall v. ExprV v -> ExprV v -> ExprV v
EApp Expr
g Expr
e)
  TVSubst
su        <- HasCallStack =>
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
unifyMany Env
f Maybe Expr
ge TVSubst
isu [Sort
it] [Sort
et]
  let t :: Sort
t     = TVSubst -> Sort -> Sort
apply TVSubst
su Sort
ot
  case Maybe Sort
to of
    Maybe Sort
Nothing    -> (TVSubst, Sort) -> ReaderT ChState IO (TVSubst, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst
su, Sort
t)
    Just Sort
t'    -> do TVSubst
θ' <- HasCallStack =>
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
unifyMany Env
f Maybe Expr
ge TVSubst
su [Sort
t] [Sort
t']
                     let ti :: Sort
ti = TVSubst -> Sort -> Sort
apply TVSubst
θ' Sort
et
                     Sort
_ <- Env -> Sort -> Expr -> CheckM Sort
checkExprAs Env
f Sort
ti Expr
e
                     (TVSubst, Sort) -> ReaderT ChState IO (TVSubst, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst
θ', TVSubst -> Sort -> Sort
apply TVSubst
θ' Sort
t)


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

checkOp :: Env -> Expr -> Bop -> Expr -> CheckM Sort
checkOp :: Env -> Expr -> Bop -> Expr -> CheckM Sort
checkOp Env
f Expr
e1 Bop
o Expr
e2
  = do Sort
t1 <- Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e1
       Sort
t2 <- Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e2
       Env -> Expr -> Sort -> Sort -> CheckM Sort
checkOpTy Env
f (Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o Expr
e1 Expr
e2) Sort
t1 Sort
t2


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

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

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

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

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

checkEqConstr :: Env -> Maybe Expr -> TVSubst -> Symbol -> Sort -> CheckM TVSubst
checkEqConstr :: Env
-> Maybe Expr
-> TVSubst
-> Symbol
-> Sort
-> ReaderT ChState IO TVSubst
checkEqConstr Env
_ Maybe Expr
_  TVSubst
θ Symbol
a (FObj Symbol
b)
  | Symbol
a Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
b
  = TVSubst -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
checkEqConstr Env
f Maybe Expr
e TVSubst
θ Symbol
a Sort
t =
  case Env
f Symbol
a of
    Found Sort
tA -> Env
-> Maybe Expr
-> TVSubst
-> Sort
-> Sort
-> ReaderT ChState IO TVSubst
unify1 Env
f Maybe Expr
e TVSubst
θ Sort
tA Sort
t
    SESearch Sort
_        -> String -> ReaderT ChState IO TVSubst
forall a. String -> CheckM a
throwErrorAt (String -> ReaderT ChState IO TVSubst)
-> String -> ReaderT ChState IO 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 :: Env -> Expr -> CheckM ()
checkPred Env
f Expr
e = Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e CheckM Sort -> (Sort -> CheckM ()) -> CheckM ()
forall a b.
ReaderT ChState IO a
-> (a -> ReaderT ChState IO b) -> ReaderT ChState IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr -> Sort -> CheckM ()
checkBoolSort Expr
e

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

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

checkRel Env
f Brel
r  Expr
e1 Expr
e2 = do
  Sort
t1 <- Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e1
  Sort
t2 <- Env -> Expr -> CheckM Sort
checkExpr Env
f Expr
e2
  Env -> Expr -> Brel -> Sort -> Sort -> CheckM ()
checkRelTy Env
f (Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r Expr
e1 Expr
e2) Brel
r Sort
t1 Sort
t2


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

-- | @a ~~ b@ is translated to @(= a b)@ when producing SMTLIB.
-- But this is only valid if @a@ and @b@ have the same sort in SMTLIB.
-- It turns out that most types are represented with sort Int, so comparing
-- values of different types is not rejected in general by SMT solvers.
--
-- There are at least two exceptions though. The first of them is the type
-- Bool, which is represented with the sort Bool. Therefore, @a ~~ b@ is fine
-- if both arguments have Bool sort, or if neither of them has.
--
-- The other exception is functions, which have a function sort in SMTLIB.
-- But at the moment no @~~@ equalities are produced with function sorts, so
-- that case isn't considered in this function.
--
checkURel :: Expr -> Sort -> Sort -> CheckM ()
checkURel :: Expr -> Sort -> Sort -> CheckM ()
checkURel Expr
e Sort
s1 Sort
s2 = Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
b1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b2) (String -> CheckM ()
forall a. String -> CheckM a
throwErrorAt (String -> CheckM ()) -> String -> CheckM ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => Expr -> Sort -> Sort -> String
Expr -> Sort -> Sort -> String
errRel Expr
e Sort
s1 Sort
s2)
  where
    b1 :: Bool
b1            = Sort
s1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
boolSort
    b2 :: Bool
b2            = Sort
s2 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
boolSort


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

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


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


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


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

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

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

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

 -}
--------------------------------------------------------------------------------
unifys :: HasCallStack => Env -> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
--------------------------------------------------------------------------------
unifys :: HasCallStack =>
Env -> Maybe Expr -> [Sort] -> [Sort] -> ReaderT ChState IO TVSubst
unifys Env
f Maybe Expr
e = HasCallStack =>
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
unifyMany Env
f Maybe Expr
e TVSubst
emptySubst

unifyMany :: HasCallStack => Env -> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany :: HasCallStack =>
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
unifyMany Env
f Maybe Expr
e TVSubst
θ [Sort]
ts [Sort]
ts'
  | [Sort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Sort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts' = (TVSubst -> (Sort, Sort) -> ReaderT ChState IO TVSubst)
-> TVSubst -> [(Sort, Sort)] -> ReaderT ChState IO TVSubst
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Sort -> Sort -> ReaderT ChState IO TVSubst)
-> (Sort, Sort) -> ReaderT ChState IO TVSubst
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Sort -> Sort -> ReaderT ChState IO TVSubst)
 -> (Sort, Sort) -> ReaderT ChState IO TVSubst)
-> (TVSubst -> Sort -> Sort -> ReaderT ChState IO TVSubst)
-> TVSubst
-> (Sort, Sort)
-> ReaderT ChState IO TVSubst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> Maybe Expr
-> TVSubst
-> Sort
-> Sort
-> ReaderT ChState IO TVSubst
unify1 Env
f Maybe Expr
e) TVSubst
θ ([(Sort, Sort)] -> ReaderT ChState IO TVSubst)
-> [(Sort, Sort)] -> ReaderT ChState IO 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 -> ReaderT ChState IO 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 :: Env
-> Maybe Expr
-> TVSubst
-> Sort
-> Sort
-> ReaderT ChState IO TVSubst
unify1 Env
f Maybe Expr
e !TVSubst
θ (FVar !Int
i) !Sort
t
  = Env
-> Maybe Expr
-> TVSubst
-> Int
-> Sort
-> ReaderT ChState IO TVSubst
unifyVar Env
f Maybe Expr
e TVSubst
θ Int
i Sort
t
unify1 Env
f Maybe Expr
e !TVSubst
θ !Sort
t (FVar !Int
i)
  = Env
-> Maybe Expr
-> TVSubst
-> Int
-> Sort
-> ReaderT ChState IO TVSubst
unifyVar Env
f Maybe Expr
e TVSubst
θ Int
i Sort
t
unify1 Env
f Maybe Expr
e !TVSubst
θ (FApp !Sort
t1 !Sort
t2) (FApp !Sort
t1' !Sort
t2')
  = HasCallStack =>
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
unifyMany Env
f Maybe Expr
e TVSubst
θ [Sort
t1, Sort
t2] [Sort
t1', Sort
t2']
unify1 Env
_ Maybe Expr
_ !TVSubst
θ (FTC !FTycon
l1) (FTC !FTycon
l2)
  | FTycon -> Bool
isListTC FTycon
l1 Bool -> Bool -> Bool
&& FTycon -> Bool
isListTC FTycon
l2
  = TVSubst -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
unify1 Env
f Maybe Expr
e !TVSubst
θ t1 :: Sort
t1@(FAbs Int
_ Sort
_) !Sort
t2 = do
  !Sort
t1' <- Sort -> CheckM Sort
instantiate Sort
t1
  HasCallStack =>
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
unifyMany Env
f Maybe Expr
e TVSubst
θ [Sort
t1'] [Sort
t2]
unify1 Env
f Maybe Expr
e !TVSubst
θ !Sort
t1 t2 :: Sort
t2@(FAbs Int
_ Sort
_) = do
  !Sort
t2' <- Sort -> CheckM Sort
instantiate Sort
t2
  HasCallStack =>
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
unifyMany Env
f Maybe Expr
e TVSubst
θ [Sort
t1] [Sort
t2']
unify1 Env
_ Maybe Expr
_ !TVSubst
θ !Sort
s1 !Sort
s2
  | Sort -> Bool
isString Sort
s1, Sort -> Bool
isString Sort
s2
  = TVSubst -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ
unify1 Env
_ Maybe Expr
_ !TVSubst
θ Sort
FInt  Sort
FReal = TVSubst -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ

unify1 Env
_ Maybe Expr
_ !TVSubst
θ Sort
FReal Sort
FInt  = TVSubst -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ

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

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

unify1 Env
f Maybe Expr
e !TVSubst
θ (FFunc !Sort
t1 !Sort
t2) (FFunc !Sort
t1' !Sort
t2') =
  HasCallStack =>
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
Env
-> Maybe Expr
-> TVSubst
-> [Sort]
-> [Sort]
-> ReaderT ChState IO TVSubst
unifyMany Env
f Maybe Expr
e TVSubst
θ [Sort
t1, Sort
t2] [Sort
t1', Sort
t2']

unify1 Env
f Maybe Expr
e TVSubst
θ (FObj Symbol
a) !Sort
t =
  Env
-> Maybe Expr
-> TVSubst
-> Symbol
-> Sort
-> ReaderT ChState IO TVSubst
checkEqConstr Env
f Maybe Expr
e TVSubst
θ Symbol
a Sort
t

unify1 Env
f Maybe Expr
e TVSubst
θ !Sort
t (FObj Symbol
a) =
  Env
-> Maybe Expr
-> TVSubst
-> Symbol
-> Sort
-> ReaderT ChState IO TVSubst
checkEqConstr Env
f Maybe Expr
e TVSubst
θ Symbol
a Sort
t

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

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

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

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

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

subst Int
_  Sort
_   !Sort
s             = Sort
s

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

unifyVar :: Env -> Maybe Expr -> TVSubst -> Int -> Sort -> CheckM TVSubst
unifyVar :: Env
-> Maybe Expr
-> TVSubst
-> Int
-> Sort
-> ReaderT ChState IO TVSubst
unifyVar Env
_ 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 -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ else TVSubst -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sort -> TVSubst -> TVSubst
updateVar Int
j Sort
t' TVSubst
θ)
      Maybe Sort
Nothing       -> TVSubst -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sort -> TVSubst -> TVSubst
updateVar Int
i Sort
t TVSubst
θ)

unifyVar Env
f Maybe Expr
e TVSubst
θ !Int
i !Sort
t
  = case Int -> TVSubst -> Maybe Sort
lookupVar Int
i TVSubst
θ of
      Just (FVar !Int
j) -> TVSubst -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst -> ReaderT ChState IO TVSubst)
-> TVSubst -> ReaderT ChState IO 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 -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TVSubst
θ else Env
-> Maybe Expr
-> TVSubst
-> Sort
-> Sort
-> ReaderT ChState IO TVSubst
unify1 Env
f Maybe Expr
e TVSubst
θ Sort
t Sort
t'
      Maybe Sort
Nothing        -> TVSubst -> ReaderT ChState IO TVSubst
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sort -> TVSubst -> TVSubst
updateVar Int
i Sort
t TVSubst
θ)


--------------------------------------------------------------------------------
-- | Update global subst to be applied to expressions
--------------------------------------------------------------------------------

updateTVSubst :: TVSubst -> CheckM ()
updateTVSubst :: TVSubst -> CheckM ()
updateTVSubst TVSubst
theta = do
  IORef (Maybe TVSubst)
refTheta <- (ChState -> IORef (Maybe TVSubst))
-> ReaderT ChState IO (IORef (Maybe TVSubst))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> IORef (Maybe TVSubst)
chTVSubst
  IO () -> CheckM ()
forall a. IO a -> ReaderT ChState IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CheckM ()) -> IO () -> CheckM ()
forall a b. (a -> b) -> a -> b
$ IORef (Maybe TVSubst)
-> (Maybe TVSubst -> (Maybe TVSubst, ())) -> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (Maybe TVSubst)
refTheta ((Maybe TVSubst -> (Maybe TVSubst, ())) -> IO ())
-> (Maybe TVSubst -> (Maybe TVSubst, ())) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Maybe TVSubst, ()) -> Maybe TVSubst -> (Maybe TVSubst, ())
forall a b. a -> b -> a
const (TVSubst -> Maybe TVSubst
forall a. a -> Maybe a
Just TVSubst
theta, ())

-- local (\s -> s {chTVSubst = theta}) (return ())

mergeTVSubst :: TVSubst -> Maybe TVSubst -> TVSubst
mergeTVSubst :: TVSubst -> Maybe TVSubst -> TVSubst
mergeTVSubst (Th IntMap Sort
m1) Maybe TVSubst
Nothing = IntMap Sort -> TVSubst
Th IntMap Sort
m1
mergeTVSubst (Th IntMap Sort
m1) (Just (Th IntMap Sort
m2)) = IntMap Sort -> TVSubst
Th IntMap Sort
m1 TVSubst -> TVSubst -> TVSubst
forall a. Semigroup a => a -> a -> a
<> IntMap Sort -> TVSubst
Th IntMap Sort
m2

composeTVSubst :: Maybe TVSubst -> CheckM ()
composeTVSubst :: Maybe TVSubst -> CheckM ()
composeTVSubst Maybe TVSubst
Nothing = () -> CheckM ()
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
composeTVSubst (Just TVSubst
theta1) = do
  IORef (Maybe TVSubst)
refTheta <- (ChState -> IORef (Maybe TVSubst))
-> ReaderT ChState IO (IORef (Maybe TVSubst))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ChState -> IORef (Maybe TVSubst)
chTVSubst
  Maybe TVSubst
theta <- IO (Maybe TVSubst) -> ReaderT ChState IO (Maybe TVSubst)
forall a. IO a -> ReaderT ChState IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe TVSubst) -> ReaderT ChState IO (Maybe TVSubst))
-> IO (Maybe TVSubst) -> ReaderT ChState IO (Maybe TVSubst)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe TVSubst) -> IO (Maybe TVSubst)
forall a. IORef a -> IO a
readIORef IORef (Maybe TVSubst)
refTheta
  TVSubst -> CheckM ()
updateTVSubst (TVSubst -> Maybe TVSubst -> TVSubst
mergeTVSubst TVSubst
theta1 Maybe TVSubst
theta)

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

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

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


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

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

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

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

instance Monoid TVSubst where
  mempty :: TVSubst
mempty  = IntMap Sort -> TVSubst
Th IntMap 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 IntMap Sort
m)   = Int -> IntMap Sort -> Maybe Sort
forall a. Int -> IntMap a -> Maybe a
M.lookup Int
i IntMap Sort
m
{-# SCC lookupVar #-}

updateVar :: Int -> Sort -> TVSubst -> TVSubst
updateVar :: Int -> Sort -> TVSubst -> TVSubst
updateVar !Int
i !Sort
t (Th IntMap Sort
m) = IntMap Sort -> TVSubst
Th (Int -> Sort -> IntMap Sort -> IntMap Sort
forall a. Int -> a -> IntMap a -> IntMap a
M.insert Int
i Sort
t IntMap Sort
m)

emptySubst :: TVSubst
emptySubst :: TVSubst
emptySubst = IntMap Sort -> TVSubst
Th IntMap Sort
forall a. IntMap a
M.empty

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

globalEnv :: Cfg.Config -> F.GInfo c a -> SEnv Sort
globalEnv :: forall (c :: * -> *) a. Config -> GInfo c a -> SEnv Sort
globalEnv Config
cfg GInfo c a
finfo = GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits GInfo c a
finfo SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> SEnv Sort
dataEnv
  where
    dataEnv :: SEnv Sort
dataEnv = TheorySymbol -> Sort
F.tsSort (TheorySymbol -> Sort) -> SEnv TheorySymbol -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config -> GInfo c a -> SEnv TheorySymbol
forall (c :: * -> *) a. Config -> GInfo c a -> SEnv TheorySymbol
theoryEnv Config
cfg GInfo c a
finfo

theoryEnv :: Cfg.Config -> F.GInfo c a -> F.SEnv F.TheorySymbol
theoryEnv :: forall (c :: * -> *) a. Config -> GInfo c a -> SEnv TheorySymbol
theoryEnv Config
cfg GInfo c a
si
  =  SMTSolver -> SEnv TheorySymbol
forall a. TheorySymbols a => a -> SEnv TheorySymbol
Thy.theorySymbols (Config -> SMTSolver
Cfg.solver Config
cfg)
  SEnv TheorySymbol -> SEnv TheorySymbol -> SEnv TheorySymbol
forall a. Semigroup a => a -> a -> a
<> DefinedFuns -> SEnv TheorySymbol
forall a. TheorySymbols a => a -> SEnv TheorySymbol
Thy.theorySymbols (GInfo c a -> DefinedFuns
forall (c :: * -> *) a. GInfo c a -> DefinedFuns
F.defns GInfo c a
si)
  SEnv TheorySymbol -> SEnv TheorySymbol -> SEnv TheorySymbol
forall a. Semigroup a => a -> a -> a
<> [DataDecl] -> SEnv TheorySymbol
forall a. TheorySymbols a => a -> SEnv TheorySymbol
Thy.theorySymbols (GInfo c a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls GInfo c a
si)