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

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

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

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

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

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

  -- * Apply Substitution
  , apply
  , defuncEApp

  -- * Exported Sorts
  , boolSort
  , strSort

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

  -- * Predicates on Sorts
  , isFirstOrder
  , isMono

--  , runCM0
  ) where

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

import           Data.Bifunctor (first)
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           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 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 :: ElabParam -> a -> a


instance (Loc a) => Elaborate (SInfo a) where
  elaborate :: 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.asserts = elaborate ep <$> F.asserts si
    , F.ddecls  = coerceDataDecl (epFlags ep) <$> F.ddecls si
    }


instance (Elaborate e) => (Elaborate (Triggered e)) where
  elaborate :: ElabParam -> Triggered e -> Triggered e
elaborate ElabParam
ep Triggered e
t = ElabParam -> e -> e
forall a. Elaborate a => 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 :: ElabParam -> Maybe a -> Maybe a
elaborate ElabParam
ep Maybe a
t = ElabParam -> a -> a
forall a. Elaborate a => 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 :: ElabParam -> Sort -> Sort
elaborate ElabParam
_ = 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 :: 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 :: 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 :: 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 Expr where
  elaborate :: ElabParam -> Expr -> Expr
elaborate ElabParam
p Expr
e = ElabParam -> Expr -> Maybe Sort -> Expr
elaborateExpr ElabParam
p Expr
e Maybe Sort
forall a. Maybe a
Nothing

elaborateExpr :: ElabParam -> Expr -> Maybe Sort -> Expr
elaborateExpr :: 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
. 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
. 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 :: ElabParam -> (Symbol, Sort) -> (Symbol, Sort)
elaborate ElabParam
ep (Symbol
x, Sort
s) = (Symbol
x, ElabParam -> Sort -> Sort
forall a. Elaborate a => ElabParam -> a -> a
elaborate ElabParam
ep Sort
s)

instance Elaborate a => Elaborate [a]  where
  elaborate :: ElabParam -> [a] -> [a]
elaborate ElabParam
ep [a]
xs = ElabParam -> a -> a
forall a. Elaborate a => 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 :: ElabParam -> SortedReft -> SortedReft
elaborate ElabParam
ep (RR Sort
s (Reft (Symbol
v, Expr
e))) = Sort -> ReftV Symbol -> SortedReft
RR Sort
s ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, Expr
e'))
    where
      e' :: Expr
e'   = 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 :: 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 => 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 :: 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 (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 (PGrad  KVar
k SubstV Symbol
su GradInfo
i Expr
e) = KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV Symbol
su GradInfo
i (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 Expr
e                 = Expr
e

elabFSetBagZ3 :: Expr -> Expr
elabFSetBagZ3 :: Expr -> Expr
elabFSetBagZ3 (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
elabFSetBagZ3 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
elabFSetBagZ3 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
elabFSetBagZ3 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
elabFSetBagZ3 Expr
h) (Expr -> Expr
elabFSetBagZ3 Expr
e)
elabFSetBagZ3 (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
elabFSetBagZ3 Expr
e2)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e2)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 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
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e2)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 Expr
e2))) (Expr -> Expr
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 Expr
e2))) (Expr -> Expr
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 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
elabFSetBagZ3 Expr
h) (Expr -> Expr
elabFSetBagZ3 Expr
e1)) (Expr -> Expr
elabFSetBagZ3 Expr
e2)
elabFSetBagZ3 (EApp Expr
e1 Expr
e2)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
elabFSetBagZ3 Expr
e1) (Expr -> Expr
elabFSetBagZ3 Expr
e2)
elabFSetBagZ3 (ENeg Expr
e)          = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg (Expr -> Expr
elabFSetBagZ3 Expr
e)
elabFSetBagZ3 (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
elabFSetBagZ3 Expr
e1) (Expr -> Expr
elabFSetBagZ3 Expr
e2)
elabFSetBagZ3 (EIte Expr
e1 Expr
e2 Expr
e3)   = Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte (Expr -> Expr
elabFSetBagZ3 Expr
e1) (Expr -> Expr
elabFSetBagZ3 Expr
e2) (Expr -> Expr
elabFSetBagZ3 Expr
e3)
elabFSetBagZ3 (ECst Expr
e Sort
t)        = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst (Expr -> Expr
elabFSetBagZ3 Expr
e) Sort
t
elabFSetBagZ3 (ELam (Symbol, Sort)
b Expr
e)        = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol, Sort)
b (Expr -> Expr
elabFSetBagZ3 Expr
e)
elabFSetBagZ3 (ETApp Expr
e Sort
t)       = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ETApp (Expr -> Expr
elabFSetBagZ3 Expr
e) Sort
t
elabFSetBagZ3 (ETAbs Expr
e Symbol
t)       = Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
ETAbs (Expr -> Expr
elabFSetBagZ3 Expr
e) Symbol
t
elabFSetBagZ3 (PAnd [Expr]
es)         = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd (Expr -> Expr
elabFSetBagZ3 (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
elabFSetBagZ3 (POr [Expr]
es)          = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr (Expr -> Expr
elabFSetBagZ3 (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
elabFSetBagZ3 (PNot Expr
e)          = Expr -> Expr
forall v. ExprV v -> ExprV v
PNot (Expr -> Expr
elabFSetBagZ3 Expr
e)
elabFSetBagZ3 (PImp Expr
e1 Expr
e2)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp (Expr -> Expr
elabFSetBagZ3 Expr
e1) (Expr -> Expr
elabFSetBagZ3 Expr
e2)
elabFSetBagZ3 (PIff Expr
e1 Expr
e2)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff (Expr -> Expr
elabFSetBagZ3 Expr
e1) (Expr -> Expr
elabFSetBagZ3 Expr
e2)
elabFSetBagZ3 (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
elabFSetBagZ3 Expr
e1) (Expr -> Expr
elabFSetBagZ3 Expr
e2)
elabFSetBagZ3 (PAll   [(Symbol, Sort)]
bs Expr
e)     = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
bs (Expr -> Expr
elabFSetBagZ3 Expr
e)
elabFSetBagZ3 (PExist [(Symbol, Sort)]
bs Expr
e)     = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
bs (Expr -> Expr
elabFSetBagZ3 Expr
e)
elabFSetBagZ3 (PGrad  KVar
k SubstV Symbol
su GradInfo
i Expr
e) = KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV Symbol
su GradInfo
i (Expr -> Expr
elabFSetBagZ3 Expr
e)
elabFSetBagZ3 (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
elabFSetBagZ3 Expr
e)
elabFSetBagZ3 Expr
e                 = Expr
e

--------------------------------------------------------------------------------
-- | 'elabExpr' adds "casts" to decorate polymorphic instantiation sites.
--------------------------------------------------------------------------------
elabExpr :: ElabParam -> Maybe Sort -> Expr ->  Expr
elabExpr :: 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. 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 :: Sort -> Maybe Sort -> CheckM ()
validateSort :: Sort -> Maybe Sort -> CheckM ()
validateSort Sort
t (Just Sort
t')
  | Sort
t Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t'            = () -> 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 (String -> CheckM ()) -> String -> CheckM ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"unexpected sort: got `%s` but expected `%s`" (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t) (Sort -> String
forall a. PPrint a => a -> String
showpp Sort
t')
validateSort 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, Symbol -> SESearch Sort
envLookup) Expr
e
    Sort -> Maybe Sort -> CheckM ()
validateSort 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
s  -> Expr -> Either Error Expr
forall a b. b -> Either a b
Right Expr
s
  where
    sEnv :: SEnv Sort
sEnv = SymEnv -> SEnv Sort
seSort SymEnv
env
    envLookup :: Symbol -> SESearch Sort
envLookup = (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
sEnv)
    d :: String -> Doc
d String
m  = [Doc] -> Doc
vcat [ Doc
"elaborate" Doc -> Doc -> Doc
<+> String -> Doc
text (Located String -> String
forall a. Located a -> a
val Located String
msg) Doc -> Doc -> Doc
<+> Doc
"failed on:"
                , Int -> Doc -> Doc
nest Int
4 (Expr -> Doc
forall a. PPrint a => a -> Doc
pprint Expr
e)
                , Doc
"with error"
                , Int -> Doc -> Doc
nest Int
4 (String -> Doc
text String
m)
                , Doc
"in environment"
                , Int -> Doc -> Doc
nest Int
4 (SEnv Sort -> Doc
forall a. PPrint a => a -> Doc
pprint (SEnv Sort -> Doc) -> SEnv Sort -> Doc
forall a b. (a -> b) -> a -> b
$ SEnv Sort -> Expr -> SEnv Sort
forall e a. Subable e => SEnv a -> e -> SEnv a
subEnv SEnv Sort
sEnv Expr
e)
                ]


--------------------------------------------------------------------------------
-- | 'elabApply' replaces all direct function calls indirect calls via `apply`
--------------------------------------------------------------------------------
elabApply :: SymEnv -> Expr -> Expr
elabApply :: SymEnv -> Expr -> Expr
elabApply SymEnv
env = Expr -> Expr
go
  where
    go :: Expr -> Expr
go Expr
e                  = case Expr -> (Expr, [(Expr, Sort)])
splitArgs Expr
e of
                             (Expr
e', []) -> Expr -> Expr
step Expr
e'
                             (Expr
f , [(Expr, Sort)]
es) -> SymEnv -> Expr -> [(Expr, Sort)] -> Expr
defuncEApp SymEnv
env (Expr -> Expr
go Expr
f) ((Expr -> Expr) -> (Expr, Sort) -> (Expr, Sort)
forall a 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 (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 (PGrad KVar
k SubstV Symbol
su GradInfo
i Expr
e) = KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV Symbol
su GradInfo
i (Expr -> Expr
go Expr
e)
    step e :: Expr
e@PKVar{}        = Expr
e
    step e :: Expr
e@ESym{}         = Expr
e
    step e :: Expr
e@ECon{}         = Expr
e
    step e :: Expr
e@EVar{}         = Expr
e
    -- ETApp, ETAbs, PAll, PExist
    step Expr
e                = String -> Expr
forall a. HasCallStack => String -> a
error (String -> Expr) -> String -> Expr
forall a b. (a -> b) -> a -> b
$ String
"TODO elabApply: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e

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

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

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


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

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

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

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

data ChState = ChS { ChState -> IORef Int
chCount :: IORef Int
                   , ChState -> SrcSpan
chSpan  :: SrcSpan
                   , 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 -> ElabFlags
Cfg.ElabFlags 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 ((Symbol -> SESearch Sort) -> Expr -> Maybe Expr
checkPred' Symbol -> SESearch Sort
f)
    filterWithTemplate :: Expr -> Bool
filterWithTemplate Expr
e =  Bool -> Bool
not (Templates -> Expr -> Bool
matchesTemplates Templates
t Expr
e) Bool -> Bool -> Bool
|| Maybe Expr -> Bool
forall a. Maybe a -> Bool
isJust ((Symbol -> SESearch Sort) -> Expr -> Maybe Expr
checkPred' Symbol -> SESearch Sort
f Expr
e)
    tx :: ([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 :: Symbol -> SESearch Sort
f    = (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`lookupSEnvWithDistance` SEnv Sort
γ')
    γ' :: SEnv Sort
γ'   = Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
v Sort
s SEnv Sort
γ
    -- wmsg t r = "WARNING: prune unsorted reft:\n" ++ showFix r ++ "\n" ++ t

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

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

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

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

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

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

--------------------------------------------------------------------------------
-- | Elaborate expressions with types to make polymorphic instantiation explicit.
--------------------------------------------------------------------------------
{-# SCC elab #-}
elab :: ElabEnv -> Expr -> CheckM (Expr, Sort)
--------------------------------------------------------------------------------
elab :: ElabEnv -> Expr -> CheckM (Expr, Sort)
elab f :: ElabEnv
f@(!SymEnv
_, !Symbol -> SESearch Sort
g) e :: Expr
e@(EBin !Bop
o !Expr
e1 !Expr
e2) = do
  (!Expr
e1', !Sort
s1) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  (!Expr
e2', !Sort
s2) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  !Sort
s <- (Symbol -> SESearch Sort) -> Expr -> Sort -> Sort -> CheckM Sort
checkOpTy Symbol -> SESearch Sort
g Expr
e Sort
s1 Sort
s2
  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 (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)

elab !ElabEnv
_ e :: Expr
e@(PKVar KVar
_ SubstV Symbol
_) =
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Sort
boolSort)

elab !ElabEnv
f (PGrad !KVar
k !SubstV Symbol
su !GradInfo
i !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 (KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV Symbol
su GradInfo
i Expr
e', Sort
boolSort)

elab (!SymEnv
_, !Symbol -> SESearch Sort
f) e :: Expr
e@(EVar !Symbol
x) = do
  !Sort
cs <- (Symbol -> SESearch Sort) -> Symbol -> CheckM Sort
checkSym Symbol -> SESearch Sort
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
_,!Symbol -> SESearch Sort
g) (ECst (EIte !Expr
p !Expr
e1 !Expr
e2) !Sort
t) = do
  (!Expr
p', !Sort
_)   <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
p
  (!Expr
e1', !Sort
s1) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f (Expr -> Sort -> Expr
eCst Expr
e1 Sort
t)
  (!Expr
e2', !Sort
s2) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f (Expr -> Sort -> Expr
eCst Expr
e2 Sort
t)
  !Sort
s          <- (Symbol -> SESearch Sort)
-> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy Symbol -> SESearch Sort
g Expr
p Expr
e1' Expr
e2' Sort
s1 Sort
s2
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
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
_,!Symbol -> SESearch Sort
g) (EIte !Expr
p !Expr
e1 !Expr
e2) = do
  !Sort
t <- (Symbol -> SESearch Sort) -> Expr -> Expr -> CheckM Sort
getIte Symbol -> SESearch Sort
g Expr
e1 Expr
e2
  (!Expr
p', !Sort
_)   <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
p
  (!Expr
e1', !Sort
s1) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f (Expr -> Sort -> Expr
eCst Expr
e1 Sort
t)
  (!Expr
e2', !Sort
s2) <- ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f (Expr -> Sort -> Expr
eCst Expr
e2 Sort
t)
  !Sort
s          <- (Symbol -> SESearch Sort)
-> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy Symbol -> SESearch Sort
g Expr
p Expr
e1' Expr
e2' Sort
s1 Sort
s2
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
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 (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
_,!Symbol -> SESearch Sort
g) e :: Expr
e@(PAtom !Brel
eq !Expr
e1 !Expr
e2) | Brel
eq Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
eq Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Ne = do
  !Sort
t1        <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
g Expr
e1
  !Sort
t2        <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
g Expr
e2
  (!Sort
t1',!Sort
t2') <- (Symbol -> SESearch Sort)
-> Expr -> Sort -> Sort -> CheckM (Sort, Sort)
unite Symbol -> SESearch Sort
g Expr
e Sort
t1 Sort
t2 CheckM (Sort, Sort) -> String -> CheckM (Sort, Sort)
forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Expr -> String
errElabExpr Expr
e
  !Expr
e1'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
f Sort
t1' Expr
e1
  !Expr
e2'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
f Sort
t2' Expr
e2
  !Expr
e1''      <- ElabEnv -> Expr -> Sort -> CheckM Expr
eCstAtom ElabEnv
f Expr
e1' Sort
t1'
  !Expr
e2''      <- ElabEnv -> Expr -> Sort -> CheckM Expr
eCstAtom ElabEnv
f Expr
e2' Sort
t2'
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
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,!Symbol -> SESearch Sort
_) (PAtom !Brel
r !Expr
e1 !Expr
e2) = do
  !Expr
e1' <- (Expr -> Sort -> Expr) -> (Expr, Sort) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SymEnv -> Expr -> Sort -> Expr
toInt SymEnv
env) ((Expr, Sort) -> Expr) -> CheckM (Expr, Sort) -> CheckM Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e1
  !Expr
e2' <- (Expr -> Sort -> Expr) -> (Expr, Sort) -> Expr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SymEnv -> Expr -> Sort -> Expr
toInt SymEnv
env) ((Expr, Sort) -> Expr) -> CheckM (Expr, Sort) -> CheckM Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Expr -> CheckM (Expr, Sort)
elab ElabEnv
f Expr
e2
  (Expr, Sort) -> CheckM (Expr, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
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 => 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 => 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 => 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,Symbol -> SESearch Sort
g) (EVar Symbol
x) Sort
t
  | Found Sort
s <- Symbol -> SESearch Sort
g Symbol
x
  , Sort -> Bool
isUndef Sort
s
  , Bool -> Bool
not (SymEnv -> Sort -> Bool
isNum SymEnv
sym Sort
t) = (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ECst` Sort
t) (Expr -> Expr) -> CheckM Expr -> CheckM Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
f Sort
t (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
tyCastName) (Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
x))
eCstAtom ElabEnv
_ Expr
e Sort
t = Expr -> CheckM Expr
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst Expr
e Sort
t)

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

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

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

-- DUPLICATION with `checkApp'`
elabAppAs :: ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
elabAppAs :: ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
elabAppAs env :: ElabEnv
env@(SymEnv
_, Symbol -> SESearch Sort
f) Sort
t Expr
g Expr
e = do
  Sort
gT       <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
g
  Sort
eT       <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e
  (Sort
iT, Sort
oT, TVSubst
isu) <- Sort -> CheckM (Sort, Sort, TVSubst)
checkFunSort Sort
gT
  let ge :: Maybe Expr
ge    = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp Expr
g Expr
e)
  TVSubst
su       <- HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
(Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> [Sort] -> [Sort] -> CheckM TVSubst
unifyMany Symbol -> SESearch Sort
f Maybe Expr
ge TVSubst
isu [Sort
oT, Sort
iT] [Sort
t, Sort
eT]
  let tg :: Sort
tg    = TVSubst -> Sort -> Sort
apply TVSubst
su Sort
gT
  Expr
g'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
env Sort
tg Expr
g
  let te :: Sort
te    = TVSubst -> Sort -> Sort
apply TVSubst
su Sort
eT
  Expr
e'       <- ElabEnv -> Sort -> Expr -> CheckM Expr
elabAs ElabEnv
env Sort
te Expr
e
  Expr -> CheckM Expr
forall a. a -> ReaderT ChState IO a
forall (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
forall v. ExprV v -> Sort -> ExprV v
ECst Expr
g' Sort
tg) (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
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
_, Symbol -> SESearch Sort
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) <- (Symbol -> SESearch Sort)
-> Expr
-> Expr
-> Sort
-> Sort
-> CheckM (Expr, Expr, Sort, Sort, Sort)
elabAppSort Symbol -> SESearch Sort
g Expr
e1' Expr
e2' Sort
s1 Sort
s2
  (Expr, Sort, Expr, Sort, Sort)
-> 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 :: (Symbol -> SESearch Sort)
-> Expr
-> Expr
-> Sort
-> Sort
-> CheckM (Expr, Expr, Sort, Sort, Sort)
elabAppSort Symbol -> SESearch Sort
f Expr
e1 Expr
e2 Sort
s1 Sort
s2 = do
  let e :: Maybe Expr
e            = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Expr -> Expr
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'             <- (Symbol -> SESearch Sort)
-> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst
unify1 Symbol -> SESearch Sort
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 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. 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 :: (Symbol -> SESearch Sort)
-> Expr -> Sort -> Sort -> CheckM (Sort, Sort)
unite Symbol -> SESearch Sort
f Expr
e Sort
t1 Sort
t2 = do
  TVSubst
su <- HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t1] [Sort
t2]
  (Sort, Sort) -> CheckM (Sort, Sort)
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVSubst -> Sort -> Sort
apply TVSubst
su Sort
t1, TVSubst -> Sort -> Sort
apply TVSubst
su Sort
t2)

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

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

-- | Helper for checking symbol occurrences
checkSym :: Env -> Symbol -> CheckM Sort
checkSym :: (Symbol -> SESearch Sort) -> Symbol -> CheckM Sort
checkSym Symbol -> SESearch Sort
f Symbol
x = case Symbol -> SESearch Sort
f Symbol
x of
  Found Sort
s -> Sort -> CheckM Sort
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 if-then-else expressions
checkIte :: Env -> Expr -> Expr -> Expr -> CheckM Sort
checkIte :: (Symbol -> SESearch Sort) -> Expr -> Expr -> Expr -> CheckM Sort
checkIte Symbol -> SESearch Sort
f Expr
p Expr
e1 Expr
e2 = do
  (Symbol -> SESearch Sort) -> Expr -> CheckM ()
checkPred Symbol -> SESearch Sort
f Expr
p
  Sort
t1 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e1
  Sort
t2 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e2
  (Symbol -> SESearch Sort)
-> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy Symbol -> SESearch Sort
f Expr
p Expr
e1 Expr
e2 Sort
t1 Sort
t2

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

checkIteTy :: Env -> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy :: (Symbol -> SESearch Sort)
-> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort
checkIteTy Symbol -> SESearch Sort
f Expr
p Expr
e1 Expr
e2 Sort
t1 Sort
t2 =
  ((TVSubst -> Sort -> Sort
`apply` Sort
t1) (TVSubst -> Sort) -> CheckM TVSubst -> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f Maybe Expr
e' [Sort
t1] [Sort
t2]) CheckM Sort -> String -> CheckM Sort
forall a. HasCallStack => CheckM a -> String -> CheckM a
`withError` Expr -> Expr -> Sort -> Sort -> String
errIte Expr
e1 Expr
e2 Sort
t1 Sort
t2
  where
    e' :: Maybe Expr
e' = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Expr -> Expr -> Expr
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 :: (Symbol -> SESearch Sort) -> Sort -> Expr -> CheckM Sort
checkCst Symbol -> SESearch Sort
f Sort
t (EApp Expr
g Expr
e)
  = (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> CheckM Sort
checkApp Symbol -> SESearch Sort
f (Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
t) Expr
g Expr
e
checkCst Symbol -> SESearch Sort
f Sort
t Expr
e
  = do Sort
t' <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e
       TVSubst
su <- HasCallStack =>
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
(Symbol -> SESearch Sort)
-> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst
unifys Symbol -> SESearch Sort
f (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Sort
t] [Sort
t'] CheckM TVSubst -> String -> CheckM 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 :: (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> CheckM Sort
checkApp Symbol -> SESearch Sort
f Maybe Sort
to Expr
g Expr
es
  = (TVSubst, Sort) -> Sort
forall a b. (a, b) -> b
snd ((TVSubst, Sort) -> Sort)
-> ReaderT ChState IO (TVSubst, Sort) -> CheckM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> SESearch Sort)
-> Maybe Sort -> Expr -> Expr -> ReaderT ChState IO (TVSubst, Sort)
checkApp' Symbol -> SESearch Sort
f Maybe Sort
to Expr
g Expr
es

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


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

checkOp :: Env -> Expr -> Bop -> Expr -> CheckM Sort
checkOp :: (Symbol -> SESearch Sort) -> Expr -> Bop -> Expr -> CheckM Sort
checkOp Symbol -> SESearch Sort
f Expr
e1 Bop
o Expr
e2
  = do Sort
t1 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e1
       Sort
t2 <- (Symbol -> SESearch Sort) -> Expr -> CheckM Sort
checkExpr Symbol -> SESearch Sort
f Expr
e2
       (Symbol -> SESearch Sort) -> Expr -> Sort -> Sort -> CheckM Sort
checkOpTy Symbol -> SESearch Sort
f (Bop -> Expr -> Expr -> Expr
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 :: (Symbol -> SESearch Sort) -> Expr -> Sort -> Sort -> CheckM Sort
checkOpTy Symbol -> SESearch Sort
_ Expr
_ Sort
FInt Sort
FInt
  = Sort -> CheckM Sort
forall a. a -> ReaderT ChState IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
FInt

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

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

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

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

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

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

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

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

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

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

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


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

--------------------------------------------------------------------------------
unifyTo1 :: Env -> [Sort] -> Maybe Sort
--------------------------------------------------------------------------------
unifyTo1 :: (Symbol -> SESearch Sort) -> [Sort] -> Maybe Sort
unifyTo1 Symbol -> SESearch Sort
f [Sort]
ts
  = case SrcSpan -> 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 ((Symbol -> SESearch Sort) -> [Sort] -> CheckM Sort
unifyTo1M Symbol -> SESearch Sort
f [Sort]
ts) of
      Left ChError
_  -> Maybe Sort
forall a. Maybe a
Nothing
      Right Sort
t -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
t


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


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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subst Int
_  Sort
_   !Sort
s             = Sort
s

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

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

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


--------------------------------------------------------------------------------
-- | 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)