{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,
MultiParamTypeClasses, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
normaliseAll, normaliseBlocking, toValue, quoteTerm,
rt_simplify, simplify, inlineSmall,
specialise, unfold, convEq, convEq',
Def(..), CaseInfo(..), CaseDefs(..),
Accessibility(..), Injectivity, Totality(..), TTDecl, PReason(..), MetaInformation(..),
Context, initContext, ctxtAlist, next_tvar,
addToCtxt, setAccess, setInjective, setTotal, setRigCount,
setMetaInformation, addCtxtDef, addTyDecl,
addDatatype, addCasedef, simplifyCasedef, addOperator,
lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
mapDefCtxt, tcReducible,
lookupTotalAccessibility,
lookupTotal, lookupTotalExact, lookupInjectiveExact,
lookupRigCount, lookupRigCountExact,
lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
conGuarded,
Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
visibleDefinitions,
isUniverse, linearCheck, linearCheckArg) where
import Idris.Core.CaseTree
import Idris.Core.TT
import Control.Monad
import Control.Monad.State
import Data.List
import Data.Maybe (listToMaybe)
import GHC.Generics (Generic)
import qualified Data.Map.Strict as Map
data EvalState = ES { EvalState -> [(Name, Int)]
limited :: [(Name, Int)],
EvalState -> Int
nexthole :: Int,
EvalState -> Bool
blocking :: Bool }
deriving Int -> EvalState -> ShowS
[EvalState] -> ShowS
EvalState -> String
(Int -> EvalState -> ShowS)
-> (EvalState -> String)
-> ([EvalState] -> ShowS)
-> Show EvalState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EvalState -> ShowS
showsPrec :: Int -> EvalState -> ShowS
$cshow :: EvalState -> String
show :: EvalState -> String
$cshowList :: [EvalState] -> ShowS
showList :: [EvalState] -> ShowS
Show
type Eval a = State EvalState a
data EvalOpt = Spec
| Simplify Bool
| AtREPL
| RunTT
| Unfold
deriving (Int -> EvalOpt -> ShowS
[EvalOpt] -> ShowS
EvalOpt -> String
(Int -> EvalOpt -> ShowS)
-> (EvalOpt -> String) -> ([EvalOpt] -> ShowS) -> Show EvalOpt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EvalOpt -> ShowS
showsPrec :: Int -> EvalOpt -> ShowS
$cshow :: EvalOpt -> String
show :: EvalOpt -> String
$cshowList :: [EvalOpt] -> ShowS
showList :: [EvalOpt] -> ShowS
Show, EvalOpt -> EvalOpt -> Bool
(EvalOpt -> EvalOpt -> Bool)
-> (EvalOpt -> EvalOpt -> Bool) -> Eq EvalOpt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EvalOpt -> EvalOpt -> Bool
== :: EvalOpt -> EvalOpt -> Bool
$c/= :: EvalOpt -> EvalOpt -> Bool
/= :: EvalOpt -> EvalOpt -> Bool
Eq)
initEval :: EvalState
initEval = [(Name, Int)] -> Int -> Bool -> EvalState
ES [] Int
0 Bool
False
data Value = VP NameType Name Value
| VV Int
| VBind Bool Name (Binder Value) (Value -> Eval Value)
| VBLet RigCount Int Name Value Value Value
| VApp Value Value
| VType UExp
| VUType Universe
| VErased
| VImpossible
| VConstant Const
| VProj Value Int
| VTmp Int
canonical :: Value -> Bool
canonical :: Value -> Bool
canonical (VP (DCon Int
_ Int
_ Bool
_) Name
_ Value
_) = Bool
True
canonical (VP (TCon Int
_ Int
_) Name
_ Value
_) = Bool
True
canonical (VApp Value
f Value
a) = Value -> Bool
canonical Value
f
canonical (VConstant Const
_) = Bool
True
canonical (VType UExp
_) = Bool
True
canonical (VUType Universe
_) = Bool
True
canonical Value
VErased = Bool
True
canonical Value
_ = Bool
False
instance Show Value where
show :: Value -> String
show Value
x = TT Name -> String
forall a. Show a => a -> String
show (TT Name -> String) -> TT Name -> String
forall a b. (a -> b) -> a -> b
$ State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
100 Value
x) EvalState
initEval
instance Show (a -> b) where
show :: (a -> b) -> String
show a -> b
x = String
"<<fn>>"
normaliseC :: Context -> Env -> TT Name -> TT Name
normaliseC :: Context -> Env -> TT Name -> TT Name
normaliseC Context
ctxt Env
env TT Name
t
= State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [] (((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) TT Name
t []
Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval
normaliseAll :: Context -> Env -> TT Name -> TT Name
normaliseAll :: Context -> Env -> TT Name -> TT Name
normaliseAll Context
ctxt Env
env TT Name
t
= State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [] (((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) TT Name
t [EvalOpt
AtREPL]
Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval
normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name
normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name
normaliseBlocking Context
ctxt Env
env [Name]
blocked TT Name
t
= State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt ((Name -> (Name, Int)) -> [Name] -> [(Name, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, Int
0)) [Name]
blocked)
(((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) TT Name
t [EvalOpt
AtREPL]
Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval
normalise :: Context -> Env -> TT Name -> TT Name
normalise :: Context -> Env -> TT Name -> TT Name
normalise = Bool -> Context -> Env -> TT Name -> TT Name
normaliseTrace Bool
False
normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
normaliseTrace Bool
tr Context
ctxt Env
env TT Name
t
= State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
tr Context
ctxt [] (((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t) []
Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval
toValue :: Context -> Env -> TT Name -> Value
toValue :: Context -> Env -> TT Name -> Value
toValue Context
ctxt Env
env TT Name
t
= Eval Value -> EvalState -> Value
forall s a. State s a -> s -> a
evalState (Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [] (((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) TT Name
t []) EvalState
initEval
quoteTerm :: Value -> TT Name
quoteTerm :: Value -> TT Name
quoteTerm Value
val = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval
specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->
(TT Name, [(Name, Int)])
specialise :: Context
-> Env -> [(Name, Int)] -> TT Name -> (TT Name, [(Name, Int)])
specialise Context
ctxt Env
env [(Name, Int)]
limits TT Name
t
= let (TT Name
tm, EvalState
st) =
State EvalState (TT Name) -> EvalState -> (TT Name, EvalState)
forall s a. State s a -> s -> (a, s)
runState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt []
(((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
[EvalOpt
Spec]
Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) (EvalState
initEval { limited = limits }) in
(TT Name
tm, EvalState -> [(Name, Int)]
limited EvalState
st)
simplify :: Context -> Env -> TT Name -> TT Name
simplify :: Context -> Env -> TT Name -> TT Name
simplify Context
ctxt Env
env TT Name
t
= State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [(String -> Name
sUN String
"lazy", Int
0),
(String -> Name
sUN String
"force", Int
0),
(String -> Name
sUN String
"Force", Int
0),
(String -> Name
sUN String
"assert_smaller", Int
0),
(String -> Name
sUN String
"assert_total", Int
0),
(String -> Name
sUN String
"par", Int
0),
(String -> Name
sUN String
"prim__syntactic_eq", Int
0),
(String -> Name
sUN String
"fork", Int
0)]
(((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
[Bool -> EvalOpt
Simplify Bool
True]
Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval
inlineSmall :: Context -> Env -> TT Name -> TT Name
inlineSmall :: Context -> Env -> TT Name -> TT Name
inlineSmall Context
ctxt Env
env TT Name
t
= State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt []
(((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
[Bool -> EvalOpt
Simplify Bool
False]
Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval
rt_simplify :: Context -> Env -> TT Name -> TT Name
rt_simplify :: Context -> Env -> TT Name -> TT Name
rt_simplify Context
ctxt Env
env TT Name
t
= State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [(String -> Name
sUN String
"lazy", Int
0),
(String -> Name
sUN String
"force", Int
0),
(String -> Name
sUN String
"Force", Int
0),
(String -> Name
sUN String
"par", Int
0),
(String -> Name
sUN String
"prim__syntactic_eq", Int
0),
(String -> Name
sUN String
"prim_fork", Int
0)]
(((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
[EvalOpt
RunTT]
Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval
unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
unfold Context
ctxt Env
env [(Name, Int)]
ns TT Name
t
= State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [(Name, Int)]
ns
(((Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
[EvalOpt
Unfold]
Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval
finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))
finalEntry :: (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry (Name
n, RigCount
r, Binder (TT Name)
b) = (Name
n, RigCount
r, (TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise Binder (TT Name)
b)
usable :: Bool
-> Bool
-> Int
-> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
usable :: Bool
-> Bool
-> Int
-> Name
-> [(Name, Int)]
-> Eval (Bool, [(Name, Int)])
usable Bool
False Bool
uf Int
depthlimit Name
n [] = (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [])
usable Bool
True Bool
uf Int
depthlimit Name
n [(Name, Int)]
ns
= do ES [(Name, Int)]
ls Int
num Bool
b <- StateT EvalState Identity EvalState
forall s (m :: * -> *). MonadState s m => m s
get
if Bool
b then (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
else case Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
ls of
Just Int
0 -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
Just Int
i -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [(Name, Int)]
ns)
Maybe Int
_ -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
usable Bool
False Bool
uf Int
depthlimit Name
n [(Name, Int)]
ns
= case Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
ns of
Just Int
0 -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
Just Int
i -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)]))
-> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a b. (a -> b) -> a -> b
$ (Bool
True, (Name
n, Int -> Int
forall a. Num a => a -> a
abs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
: ((Name, Int) -> Bool) -> [(Name, Int)] -> [(Name, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', Int
_) -> Name
nName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ns)
Maybe Int
_ -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)]))
-> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a b. (a -> b) -> a -> b
$ if Bool
uf
then (Bool
False, [(Name, Int)]
ns)
else (Bool
True, (Name
n, Int
depthlimit) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
: ((Name, Int) -> Bool) -> [(Name, Int)] -> [(Name, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', Int
_) -> Name
nName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ns)
fnCount :: Int -> Name -> Eval ()
fnCount :: Int -> Name -> Eval ()
fnCount Int
inc Name
n
= do ES [(Name, Int)]
ls Int
num Bool
b <- StateT EvalState Identity EvalState
forall s (m :: * -> *). MonadState s m => m s
get
case Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
ls of
Just Int
i -> do EvalState -> Eval ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalState -> Eval ()) -> EvalState -> Eval ()
forall a b. (a -> b) -> a -> b
$ [(Name, Int)] -> Int -> Bool -> EvalState
ES ((Name
n, (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
inc)) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
:
((Name, Int) -> Bool) -> [(Name, Int)] -> [(Name, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', Int
_) -> Name
nName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ls) Int
num Bool
b
Maybe Int
_ -> () -> Eval ()
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
setBlock :: Bool -> Eval ()
setBlock :: Bool -> Eval ()
setBlock Bool
b = do ES [(Name, Int)]
ls Int
num Bool
_ <- StateT EvalState Identity EvalState
forall s (m :: * -> *). MonadState s m => m s
get
EvalState -> Eval ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([(Name, Int)] -> Int -> Bool -> EvalState
ES [(Name, Int)]
ls Int
num Bool
b)
deduct :: Name -> Eval ()
deduct = Int -> Name -> Eval ()
fnCount Int
1
reinstate :: Name -> Eval ()
reinstate = Int -> Name -> Eval ()
fnCount (-Int
1)
eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
[EvalOpt] -> Eval Value
eval :: Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
traceon Context
ctxt [(Name, Int)]
ntimes Env
genv TT Name
tm [EvalOpt]
opts = [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [] Bool
True [] TT Name
tm where
spec :: Bool
spec = EvalOpt
Spec EvalOpt -> [EvalOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
simpl :: Bool
simpl = Bool -> EvalOpt
Simplify Bool
True EvalOpt -> [EvalOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts Bool -> Bool -> Bool
|| Bool -> EvalOpt
Simplify Bool
False EvalOpt -> [EvalOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
simpl_inline :: Bool
simpl_inline = Bool -> EvalOpt
Simplify Bool
False EvalOpt -> [EvalOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
runtime :: Bool
runtime = EvalOpt
RunTT EvalOpt -> [EvalOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
atRepl :: Bool
atRepl = EvalOpt
AtREPL EvalOpt -> [EvalOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
unfold :: Bool
unfold = EvalOpt
Unfold EvalOpt -> [EvalOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
noFree :: [(a, Value)] -> Bool
noFree = (Value -> Bool) -> [Value] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Value -> Bool
canonical ([Value] -> Bool)
-> ([(a, Value)] -> [Value]) -> [(a, Value)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Value) -> Value) -> [(a, Value)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (a, Value) -> Value
forall a b. (a, b) -> b
snd
blockSimplify :: CaseInfo -> Name -> t Name -> Bool
blockSimplify (CaseInfo Bool
inl Bool
always Bool
dict) Name
n t Name
stk
| Bool
runtime
= if Bool
always then Bool
False
else Bool -> Bool
not (Bool
inl Bool -> Bool -> Bool
|| Bool
dict) Bool -> Bool -> Bool
|| Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
n t Name
stk
| Bool
simpl
= (Bool -> Bool
not Bool
inl Bool -> Bool -> Bool
|| Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
n t Name
stk)
Bool -> Bool -> Bool
|| (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"prim__syntactic_eq")
| Bool
otherwise = Bool
False
getCases :: CaseDefs -> ([Name], SC)
getCases CaseDefs
cd | Bool
simpl = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd
| Bool
runtime = CaseDefs -> ([Name], SC)
cases_runtime CaseDefs
cd
| Bool
otherwise = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd
ev :: [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (P NameType
_ Name
n TT Name
ty)
| Just (Let RigCount
_ TT Name
t TT Name
v) <- Name -> Env -> Maybe (Binder (TT Name))
forall n. Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
lookupBinder Name
n Env
genv = [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
v
ev [(Name, Int)]
ntimes_in [Name]
stk Bool
top [(Name, Value)]
env (P NameType
Ref Name
n TT Name
ty)
= do let limit :: Int
limit = if Bool
simpl then Int
100 else Int
10000
(Bool
u, [(Name, Int)]
ntimes) <- Bool
-> Bool
-> Int
-> Name
-> [(Name, Int)]
-> Eval (Bool, [(Name, Int)])
usable Bool
spec Bool
unfold Int
limit Name
n [(Name, Int)]
ntimes_in
let red :: Bool
red = Bool
u Bool -> Bool -> Bool
&& (Name -> Context -> Bool
tcReducible Name
n Context
ctxt Bool -> Bool -> Bool
|| Bool
spec Bool -> Bool -> Bool
|| (Bool
atRepl Bool -> Bool -> Bool
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env)
Bool -> Bool -> Bool
|| Bool
runtime Bool -> Bool -> Bool
|| Bool
unfold
Bool -> Bool -> Bool
|| String -> Name
sUN String
"assert_total" Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
stk)
if Bool
red then
do let val :: Maybe (Def, Accessibility)
val = Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n (Bool
spec Bool -> Bool -> Bool
|| Bool
unfold Bool -> Bool -> Bool
|| (Bool
atRepl Bool -> Bool -> Bool
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env) Bool -> Bool -> Bool
|| Bool
runtime) Context
ctxt
case Maybe (Def, Accessibility)
val of
Just (Function TT Name
_ TT Name
tm, Accessibility
Public) ->
[(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
stk) Bool
True [(Name, Value)]
env TT Name
tm
Just (TyDecl NameType
nt TT Name
ty, Accessibility
_) -> do Value
vty <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
True [(Name, Value)]
env TT Name
ty
Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ NameType -> Name -> Value -> Value
VP NameType
nt Name
n Value
vty
Just (CaseOp CaseInfo
ci TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
cd, Accessibility
acc)
| (Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Public Bool -> Bool -> Bool
|| Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Hidden) Bool -> Bool -> Bool
&&
[Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (([Name], SC) -> [Name]
forall a b. (a, b) -> a
fst (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd)) ->
let ([Name]
ns, SC
tree) = CaseDefs -> ([Name], SC)
getCases CaseDefs
cd in
if CaseInfo -> Name -> [Name] -> Bool
forall {t :: * -> *}.
Foldable t =>
CaseInfo -> Name -> t Name -> Bool
blockSimplify CaseInfo
ci Name
n [Name]
stk
then (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
else
do (Maybe Value, [Value])
c <- [(Name, Int)]
-> Name
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Name]
-> [Value]
-> SC
-> StateT EvalState Identity (Maybe Value, [Value])
evCase [(Name, Int)]
ntimes Name
n (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
stk) Bool
top [(Name, Value)]
env [Name]
ns [] SC
tree
case (Maybe Value, [Value])
c of
(Maybe Value
Nothing, [Value]
_) -> (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
(Just Value
v, [Value]
_) -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
Maybe (Def, Accessibility)
_ -> (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
else (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (P NameType
nt Name
n TT Name
ty)
= (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
nt Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (V Int
i)
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Value)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Value)]
env Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ (Name, Value) -> Value
forall a b. (a, b) -> b
snd ([(Name, Value)]
env [(Name, Value)] -> Int -> (Name, Value)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
| Bool
otherwise = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Int -> Value
VV Int
i
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Bind Name
n (Let RigCount
c TT Name
t TT Name
v) TT Name
sc)
| (Bool -> Bool
not (Bool
runtime Bool -> Bool -> Bool
|| Bool
simpl_inline Bool -> Bool -> Bool
|| Bool
unfold)) Bool -> Bool -> Bool
|| Name -> TT Name -> Int
forall n. Eq n => n -> TT n -> Int
occurrences Name
n TT Name
sc Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2
= do Value
v' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
v
Value
sc' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top ((Name
n, Value
v') (Name, Value) -> [(Name, Value)] -> [(Name, Value)]
forall a. a -> [a] -> [a]
: [(Name, Value)]
env) TT Name
sc
Int -> Value -> Eval Value
wknV (-Int
1) Value
sc'
| Bool
otherwise
= do Value
t' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
t
Value
v' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
v
EvalState
hs <- StateT EvalState Identity EvalState
forall s (m :: * -> *). MonadState s m => m s
get
let vd :: Int
vd = EvalState -> Int
nexthole EvalState
hs
EvalState -> Eval ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalState
hs { nexthole = vd + 1 })
Value
sc' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top ((Name
n, NameType -> Name -> Value -> Value
VP NameType
Bound (Int -> String -> Name
sMN Int
vd String
"vlet") Value
VErased) (Name, Value) -> [(Name, Value)] -> [(Name, Value)]
forall a. a -> [a] -> [a]
: [(Name, Value)]
env) TT Name
sc
Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ RigCount -> Int -> Name -> Value -> Value -> Value -> Value
VBLet RigCount
c Int
vd Name
n Value
t' Value
v' Value
sc'
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Bind Name
n (NLet TT Name
t TT Name
v) TT Name
sc)
= do Value
t' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
Value
v' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
v)
Value
sc' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top ((Name
n, Value
v') (Name, Value) -> [(Name, Value)] -> [(Name, Value)]
forall a. a -> [a] -> [a]
: [(Name, Value)]
env) TT Name
sc
Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Binder Value -> (Value -> Eval Value) -> Value
VBind Bool
True Name
n (RigCount -> Value -> Value -> Binder Value
forall b. RigCount -> b -> b -> Binder b
Let RigCount
RigW Value
t' Value
v') (\Value
x -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
sc')
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Bind Name
n Binder (TT Name)
b TT Name
sc)
= do Binder Value
b' <- [(Name, Value)]
-> Binder (TT Name) -> StateT EvalState Identity (Binder Value)
vbind [(Name, Value)]
env Binder (TT Name)
b
let n' :: Name
n' = Name -> [Name] -> Name
uniqueName Name
n (((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
genv [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ((Name, Value) -> Name) -> [(Name, Value)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Value) -> Name
forall a b. (a, b) -> a
fst [(Name, Value)]
env)
Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Binder Value -> (Value -> Eval Value) -> Value
VBind Bool
True
Name
n' Binder Value
b' (\Value
x -> [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
False ((Name
n', Value
x)(Name, Value) -> [(Name, Value)] -> [(Name, Value)]
forall a. a -> [a] -> [a]
:[(Name, Value)]
env) TT Name
sc)
where vbind :: [(Name, Value)]
-> Binder (TT Name) -> StateT EvalState Identity (Binder Value)
vbind [(Name, Value)]
env Binder (TT Name)
t
= (TT Name -> Eval Value)
-> Binder (TT Name) -> StateT EvalState Identity (Binder Value)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder a -> m (Binder b)
fmapMB (\TT Name
tm -> [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
tm)) Binder (TT Name)
t
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env
(App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ d :: TT Name
d@(P NameType
_ (UN Text
dly) TT Name
_) l :: TT Name
l@(P NameType
_ (UN Text
lco) TT Name
_)) TT Name
t) TT Name
arg)
| Text
dly Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" Bool -> Bool -> Bool
&& Text
lco Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Infinite" Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
unfold Bool -> Bool -> Bool
|| Bool
simpl)
= do let (TT Name
f, [TT Name]
_) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
arg
let ntimes' :: [(Name, Int)]
ntimes' = case TT Name
f of
P NameType
_ Name
fn TT Name
_ -> (Name
fn, Int
0) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
: [(Name, Int)]
ntimes
TT Name
_ -> [(Name, Int)]
ntimes
Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec (Eval () -> Eval ()) -> Eval () -> Eval ()
forall a b. (a -> b) -> a -> b
$ Bool -> Eval ()
setBlock Bool
True
Value
d' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes' [Name]
stk Bool
False [(Name, Value)]
env TT Name
d
Value
l' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes' [Name]
stk Bool
False [(Name, Value)]
env TT Name
l
Value
t' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes' [Name]
stk Bool
False [(Name, Value)]
env TT Name
t
Value
arg' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes' [Name]
stk Bool
False [(Name, Value)]
env TT Name
arg
Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec (Eval () -> Eval ()) -> Eval () -> Eval ()
forall a b. (a -> b) -> a -> b
$ Bool -> Eval ()
setBlock Bool
False
[(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes' [Name]
stk Bool
top [(Name, Value)]
env [Value
l',Value
t',Value
arg'] Value
d'
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ n :: Name
n@(UN Text
at) TT Name
_) TT Name
_) TT Name
arg)
| Just (CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
_, Accessibility
_) <- Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n (Bool
spec Bool -> Bool -> Bool
|| (Bool
atRepl Bool -> Bool -> Bool
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env)Bool -> Bool -> Bool
|| Bool
runtime) Context
ctxt,
Text
at Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"assert_total" Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
simpl Bool -> Bool -> Bool
|| Bool
unfold)
= [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
stk) Bool
top [(Name, Value)]
env TT Name
arg
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (App AppStatus Name
_ TT Name
f TT Name
a)
= do Value
f' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
False [(Name, Value)]
env TT Name
f
Value
a' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
False [(Name, Value)]
env TT Name
a
[(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [Value
a'] Value
f'
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Proj TT Name
t Int
i)
= do
Value
t' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
t
Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> (Value, [Value]) -> Value
doProj Value
t' (Value -> (Value, [Value])
getValArgs Value
t'))
where doProj :: Value -> (Value, [Value]) -> Value
doProj Value
t' (VP (DCon Int
_ Int
_ Bool
_) Name
_ Value
_, [Value]
args)
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Value] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args = [Value]
args[Value] -> Int -> Value
forall a. HasCallStack => [a] -> Int -> a
!!Int
i
doProj Value
t' (Value, [Value])
_ = Value -> Int -> Value
VProj Value
t' Int
i
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Constant Const
c) = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Const -> Value
VConstant Const
c
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
Erased = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
VErased
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
Impossible = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
VImpossible
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Inferred TT Name
tm) = [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
tm
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (TType UExp
i) = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ UExp -> Value
VType UExp
i
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (UType Universe
u) = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Universe -> Value
VUType Universe
u
evApply :: [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [Value]
args (VApp Value
f Value
a)
= [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Value
aValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
args) Value
f
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [Value]
args Value
f
= [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> Value
-> [Value]
-> Eval Value
apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env Value
f [Value]
args
apply :: [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> Value
-> [Value]
-> Eval Value
apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (VBind Bool
True Name
n (Lam RigCount
_ Value
t) Value -> Eval Value
sc) (Value
a:[Value]
as)
= do Value
a' <- Value -> Eval Value
sc Value
a
Value
app <- [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> Value
-> [Value]
-> Eval Value
apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env Value
a' [Value]
as
Int -> Value -> Eval Value
wknV Int
1 Value
app
apply [(Name, Int)]
ntimes_in [Name]
stk Bool
top [(Name, Value)]
env f :: Value
f@(VP NameType
Ref Name
n Value
ty) [Value]
args
= do let limit :: Int
limit = if Bool
simpl then Int
100 else Int
10000
(Bool
u, [(Name, Int)]
ntimes) <- Bool
-> Bool
-> Int
-> Name
-> [(Name, Int)]
-> Eval (Bool, [(Name, Int)])
usable Bool
spec Bool
unfold Int
limit Name
n [(Name, Int)]
ntimes_in
let red :: Bool
red = Bool
u Bool -> Bool -> Bool
&& (Name -> Context -> Bool
tcReducible Name
n Context
ctxt Bool -> Bool -> Bool
|| Bool
spec Bool -> Bool -> Bool
|| (Bool
atRepl Bool -> Bool -> Bool
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env)
Bool -> Bool -> Bool
|| Bool
unfold Bool -> Bool -> Bool
|| Bool
runtime
Bool -> Bool -> Bool
|| String -> Name
sUN String
"assert_total" Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
stk)
if Bool
red then
do let val :: Maybe (Def, Accessibility)
val = Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n (Bool
spec Bool -> Bool -> Bool
|| Bool
unfold Bool -> Bool -> Bool
|| (Bool
atRepl Bool -> Bool -> Bool
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env) Bool -> Bool -> Bool
|| Bool
runtime) Context
ctxt
case Maybe (Def, Accessibility)
val of
Just (CaseOp CaseInfo
ci TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
cd, Accessibility
acc)
| Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Public Bool -> Bool -> Bool
|| Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Hidden ->
let ([Name]
ns, SC
tree) = CaseDefs -> ([Name], SC)
getCases CaseDefs
cd in
if CaseInfo -> Name -> [Name] -> Bool
forall {t :: * -> *}.
Foldable t =>
CaseInfo -> Name -> t Name -> Bool
blockSimplify CaseInfo
ci Name
n [Name]
stk
then Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n Value
ty) [Value]
args
else
do (Maybe Value, [Value])
c <- [(Name, Int)]
-> Name
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Name]
-> [Value]
-> SC
-> StateT EvalState Identity (Maybe Value, [Value])
evCase [(Name, Int)]
ntimes Name
n (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
stk) Bool
top [(Name, Value)]
env [Name]
ns [Value]
args SC
tree
case (Maybe Value, [Value])
c of
(Maybe Value
Nothing, [Value]
_) -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n Value
ty) [Value]
args
(Just Value
v, [Value]
rest) -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [Value]
rest Value
v
Just (Operator TT Name
_ Int
i [Value] -> Maybe Value
op, Accessibility
_) ->
if (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Value] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args)
then case [Value] -> Maybe Value
op (Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
take Int
i [Value]
args) of
Maybe Value
Nothing -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n Value
ty) [Value]
args
Just Value
v -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
drop Int
i [Value]
args) Value
v
else Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n Value
ty) [Value]
args
Maybe (Def, Accessibility)
_ -> case [Value]
args of
[] -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
f
[Value]
_ -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env Value
f [Value]
args
else case [Value]
args of
(Value
a : [Value]
as) -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env Value
f (Value
aValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
as)
[] -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
f
apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env Value
f (Value
a:[Value]
as) = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env Value
f (Value
aValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
as)
apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env Value
f [] = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
f
unload :: [(Name, Value)] -> Value -> [Value] -> Value
unload :: [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env Value
f [] = Value
f
unload [(Name, Value)]
env Value
f (Value
a:[Value]
as) = [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env (Value -> Value -> Value
VApp Value
f Value
a) [Value]
as
evCase :: [(Name, Int)]
-> Name
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Name]
-> [Value]
-> SC
-> StateT EvalState Identity (Maybe Value, [Value])
evCase [(Name, Int)]
ntimes Name
n [Name]
stk Bool
top [(Name, Value)]
env [Name]
ns [Value]
args SC
tree
| [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Value] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args
= do let args' :: [Value]
args' = Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
take ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns) [Value]
args
let rest :: [Value]
rest = Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
drop ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns) [Value]
args
Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec (Eval () -> Eval ()) -> Eval () -> Eval ()
forall a b. (a -> b) -> a -> b
$ Name -> Eval ()
deduct Name
n
Maybe Value
t <- [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> SC
-> Eval (Maybe Value)
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args') SC
tree
Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec (Eval () -> Eval ()) -> Eval () -> Eval ()
forall a b. (a -> b) -> a -> b
$ case Maybe Value
t of
Maybe Value
Nothing -> Name -> Eval ()
reinstate Name
n
Just Value
_ -> () -> Eval ()
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(Maybe Value, [Value])
-> StateT EvalState Identity (Maybe Value, [Value])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Value
t, [Value]
rest)
| Bool
otherwise = (Maybe Value, [Value])
-> StateT EvalState Identity (Maybe Value, [Value])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Value
forall a. Maybe a
Nothing, [Value]
args)
evTree :: [(Name, Int)] -> [Name] -> Bool ->
[(Name, Value)] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
evTree :: [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> SC
-> Eval (Maybe Value)
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap (UnmatchedCase String
str) = Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap (STerm TT Name
tm)
= do let etm :: TT Name
etm = [Name] -> TT Name -> TT Name
forall n. Eq n => [n] -> TT n -> TT n
pToVs (((Name, Value) -> Name) -> [(Name, Value)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Value) -> Name
forall a b. (a, b) -> a
fst [(Name, Value)]
amap) TT Name
tm
Value
etm' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk (Bool -> Bool
not (TT Name -> Bool
forall {n}. TT n -> Bool
conHeaded TT Name
tm))
([(Name, Value)]
amap [(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall a. [a] -> [a] -> [a]
++ [(Name, Value)]
env) TT Name
etm
Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Value -> Eval (Maybe Value))
-> Maybe Value -> Eval (Maybe Value)
forall a b. (a -> b) -> a -> b
$ Value -> Maybe Value
forall a. a -> Maybe a
Just Value
etm'
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap (ProjCase TT Name
t [CaseAlt' (TT Name)]
alts)
= do Value
t' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
t
[(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> Value
-> [CaseAlt' (TT Name)]
-> Eval (Maybe Value)
doCase [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap Value
t' [CaseAlt' (TT Name)]
alts
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap (Case CaseType
_ Name
n [CaseAlt' (TT Name)]
alts)
= case Name -> [(Name, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Value)]
amap of
Just Value
v -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> Value
-> [CaseAlt' (TT Name)]
-> Eval (Maybe Value)
doCase [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap Value
v [CaseAlt' (TT Name)]
alts
Maybe Value
_ -> Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap SC
ImpossibleCase = Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing
doCase :: [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> Value
-> [CaseAlt' (TT Name)]
-> Eval (Maybe Value)
doCase [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap Value
v [CaseAlt' (TT Name)]
alts =
do Maybe ([(Name, Value)], SC)
c <- [(Name, Value)]
-> Value
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt [(Name, Value)]
env Value
v (Value -> (Value, [Value])
getValArgs Value
v) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
case Maybe ([(Name, Value)], SC)
c of
Just ([(Name, Value)]
altmap, SC
sc) -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> SC
-> Eval (Maybe Value)
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
altmap SC
sc
Maybe ([(Name, Value)], SC)
_ -> do Maybe ([(Name, Value)], SC)
c' <- [(Name, Int)]
-> [Name]
-> [(Name, Value)]
-> Value
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
forall {p}.
[(Name, Int)]
-> [Name]
-> [(Name, Value)]
-> p
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt' [(Name, Int)]
ntimes [Name]
stk [(Name, Value)]
env Value
v (Value -> (Value, [Value])
getValArgs Value
v) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
case Maybe ([(Name, Value)], SC)
c' of
Just ([(Name, Value)]
altmap, SC
sc) -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> SC
-> Eval (Maybe Value)
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
altmap SC
sc
Maybe ([(Name, Value)], SC)
_ -> Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing
conHeaded :: TT n -> Bool
conHeaded tm :: TT n
tm@(App AppStatus n
_ TT n
_ TT n
_)
| (P (DCon Int
_ Int
_ Bool
_) n
_ TT n
_, [TT n]
args) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = Bool
True
conHeaded TT n
t = Bool
False
chooseAlt' :: [(Name, Int)]
-> [Name]
-> [(Name, Value)]
-> p
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt' [(Name, Int)]
ntimes [Name]
stk [(Name, Value)]
env p
_ (Value
f, [Value]
args) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
= do Value
f' <- [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> Value
-> [Value]
-> Eval Value
apply [(Name, Int)]
ntimes [Name]
stk Bool
True [(Name, Value)]
env Value
f [Value]
args
[(Name, Value)]
-> Value
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt [(Name, Value)]
env Value
f' (Value -> (Value, [Value])
getValArgs Value
f')
[CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
chooseAlt :: [(Name, Value)] -> Value -> (Value, [Value]) -> [CaseAlt] ->
[(Name, Value)] ->
Eval (Maybe ([(Name, Value)], SC))
chooseAlt :: [(Name, Value)]
-> Value
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt [(Name, Value)]
env Value
_ (VP (DCon Int
i Int
a Bool
_) Name
_ Value
_, [Value]
args) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
| Just ([Name]
ns, SC
sc) <- Int -> [CaseAlt' (TT Name)] -> Maybe ([Name], SC)
forall {t}. Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [CaseAlt' (TT Name)]
alts = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args) [(Name, Value)]
amap, SC
sc)
| Just SC
v <- [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
chooseAlt [(Name, Value)]
env Value
_ (VP (TCon Int
i Int
a) Name
_ Value
_, [Value]
args) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
| Just ([Name]
ns, SC
sc) <- Int -> [CaseAlt' (TT Name)] -> Maybe ([Name], SC)
forall {t}. Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [CaseAlt' (TT Name)]
alts
= Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args) [(Name, Value)]
amap, SC
sc)
| Just SC
v <- [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
chooseAlt [(Name, Value)]
env Value
_ (VConstant Const
c, []) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
| Just SC
v <- Const -> [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [CaseAlt' (TT Name)]
alts = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
| Just (Name
n', Value
sub, SC
sc) <- Const -> [CaseAlt' (TT Name)] -> Maybe (Name, Value, SC)
forall {t}. Const -> [CaseAlt' t] -> Maybe (Name, Value, SC' t)
findSuc Const
c [CaseAlt' (TT Name)]
alts
= Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap [(Name
n',Value
sub)] [(Name, Value)]
amap, SC
sc)
| Just SC
v <- [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
chooseAlt [(Name, Value)]
env Value
_ (VP NameType
_ Name
n Value
_, [Value]
args) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
| Just ([Name]
ns, SC
sc) <- Name -> [CaseAlt' (TT Name)] -> Maybe ([Name], SC)
forall {t}. Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn Name
n [CaseAlt' (TT Name)]
alts = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args) [(Name, Value)]
amap, SC
sc)
chooseAlt [(Name, Value)]
env Value
_ (VBind Bool
_ Name
_ (Pi RigCount
_ Maybe ImplicitInfo
i Value
s Value
k) Value -> Eval Value
t, []) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
| Just ([Name]
ns, SC
sc) <- Name -> [CaseAlt' (TT Name)] -> Maybe ([Name], SC)
forall {t}. Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn (String -> Name
sUN String
"->") [CaseAlt' (TT Name)]
alts
= do Value
t' <- Value -> Eval Value
t (Int -> Value
VV Int
0)
Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value
s, Value
t']) [(Name, Value)]
amap, SC
sc)
chooseAlt [(Name, Value)]
_ Value
_ (Value, [Value])
_ [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
| Just SC
v <- [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts
= if ((CaseAlt' (TT Name) -> Bool) -> [CaseAlt' (TT Name)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CaseAlt' (TT Name) -> Bool
forall {t}. CaseAlt' t -> Bool
fnCase [CaseAlt' (TT Name)]
alts)
then Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
else Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(Name, Value)], SC)
forall a. Maybe a
Nothing
| Bool
otherwise = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(Name, Value)], SC)
forall a. Maybe a
Nothing
fnCase :: CaseAlt' t -> Bool
fnCase (FnCase Name
_ [Name]
_ SC' t
_) = Bool
True
fnCase CaseAlt' t
_ = Bool
False
updateAmap :: [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap [(a, b)]
newm [(a, b)]
amap
= [(a, b)]
newm [(a, b)] -> [(a, b)] -> [(a, b)]
forall a. [a] -> [a] -> [a]
++ ((a, b) -> Bool) -> [(a, b)] -> [(a, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (a
x, b
_) -> Bool -> Bool
not (a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
x (((a, b) -> a) -> [(a, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> a
forall a b. (a, b) -> a
fst [(a, b)]
newm))) [(a, b)]
amap
findTag :: Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [] = Maybe ([Name], SC' t)
forall a. Maybe a
Nothing
findTag Int
i (ConCase Name
n Int
j [Name]
ns SC' t
sc : [CaseAlt' t]
xs) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = ([Name], SC' t) -> Maybe ([Name], SC' t)
forall a. a -> Maybe a
Just ([Name]
ns, SC' t
sc)
findTag Int
i (CaseAlt' t
_ : [CaseAlt' t]
xs) = Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [CaseAlt' t]
xs
findFn :: Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn Name
fn [] = Maybe ([Name], SC' t)
forall a. Maybe a
Nothing
findFn Name
fn (FnCase Name
n [Name]
ns SC' t
sc : [CaseAlt' t]
xs) | Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = ([Name], SC' t) -> Maybe ([Name], SC' t)
forall a. a -> Maybe a
Just ([Name]
ns, SC' t
sc)
findFn Name
fn (CaseAlt' t
_ : [CaseAlt' t]
xs) = Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn Name
fn [CaseAlt' t]
xs
findDefault :: [CaseAlt' t] -> Maybe (SC' t)
findDefault [] = Maybe (SC' t)
forall a. Maybe a
Nothing
findDefault (DefaultCase SC' t
sc : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
sc
findDefault (CaseAlt' t
_ : [CaseAlt' t]
xs) = [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' t]
xs
findSuc :: Const -> [CaseAlt' t] -> Maybe (Name, Value, SC' t)
findSuc Const
c [] = Maybe (Name, Value, SC' t)
forall a. Maybe a
Nothing
findSuc (BI Integer
val) (SucCase Name
n SC' t
sc : [CaseAlt' t]
_)
| Integer
val Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 = (Name, Value, SC' t) -> Maybe (Name, Value, SC' t)
forall a. a -> Maybe a
Just (Name
n, Const -> Value
VConstant (Integer -> Const
BI (Integer
val Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)), SC' t
sc)
findSuc Const
c (CaseAlt' t
_ : [CaseAlt' t]
xs) = Const -> [CaseAlt' t] -> Maybe (Name, Value, SC' t)
findSuc Const
c [CaseAlt' t]
xs
findConst :: Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [] = Maybe (SC' t)
forall a. Maybe a
Nothing
findConst Const
c (ConstCase Const
c' SC' t
v : [CaseAlt' t]
xs) | Const
c Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
c' = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
findConst (AType (ATInt IntTy
ITNative)) (ConCase Name
n Int
1 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
findConst (AType ArithTy
ATFloat) (ConCase Name
n Int
2 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
findConst (AType (ATInt IntTy
ITChar)) (ConCase Name
n Int
3 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
findConst Const
StrType (ConCase Name
n Int
4 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
findConst (AType (ATInt IntTy
ITBig)) (ConCase Name
n Int
6 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
findConst (AType (ATInt (ITFixed NativeTy
ity))) (ConCase Name
n Int
tag [] SC' t
v : [CaseAlt' t]
xs)
| Int
tag Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
7 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ NativeTy -> Int
forall a. Enum a => a -> Int
fromEnum NativeTy
ity = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
findConst Const
c (CaseAlt' t
_ : [CaseAlt' t]
xs) = Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [CaseAlt' t]
xs
getValArgs :: Value -> (Value, [Value])
getValArgs Value
tm = Value -> [Value] -> (Value, [Value])
getValArgs' Value
tm []
getValArgs' :: Value -> [Value] -> (Value, [Value])
getValArgs' (VApp Value
f Value
a) [Value]
as = Value -> [Value] -> (Value, [Value])
getValArgs' Value
f (Value
aValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
as)
getValArgs' Value
f [Value]
as = (Value
f, [Value]
as)
instance Eq Value where
== :: Value -> Value -> Bool
(==) Value
x Value
y = Value -> TT Name
forall {a}. Quote a => a -> TT Name
getTT Value
x TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== Value -> TT Name
forall {a}. Quote a => a -> TT Name
getTT Value
y
where getTT :: a -> TT Name
getTT a
v = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (Int -> a -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 a
v) EvalState
initEval
class Quote a where
quote :: Int -> a -> Eval (TT Name)
instance Quote Value where
quote :: Int -> Value -> State EvalState (TT Name)
quote Int
i (VP NameType
nt Name
n Value
v) = (TT Name -> TT Name)
-> State EvalState (TT Name) -> State EvalState (TT Name)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n) (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
v)
quote Int
i (VV Int
x) = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> State EvalState (TT Name))
-> TT Name -> State EvalState (TT Name)
forall a b. (a -> b) -> a -> b
$ Int -> TT Name
forall n. Int -> TT n
V Int
x
quote Int
i (VBind Bool
_ Name
n Binder Value
b Value -> Eval Value
sc) = do Value
sc' <- Value -> Eval Value
sc (Int -> Value
VTmp Int
i)
Binder (TT Name)
b' <- Binder Value -> StateT EvalState Identity (Binder (TT Name))
forall {a}.
Quote a =>
Binder a -> StateT EvalState Identity (Binder (TT Name))
quoteB Binder Value
b
(TT Name -> TT Name)
-> State EvalState (TT Name) -> State EvalState (TT Name)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder (TT Name)
b') (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Value
sc')
where quoteB :: Binder a -> StateT EvalState Identity (Binder (TT Name))
quoteB Binder a
t = (a -> State EvalState (TT Name))
-> Binder a -> StateT EvalState Identity (Binder (TT Name))
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder a -> m (Binder b)
fmapMB (Int -> a -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i) Binder a
t
quote Int
i (VBLet RigCount
c Int
vd Name
n Value
t Value
v Value
sc)
= do TT Name
sc' <- Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
sc
TT Name
t' <- Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
t
TT Name
v' <- Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
v
let sc'' :: TT Name
sc'' = Name -> TT Name -> TT Name
forall n. Eq n => n -> TT n -> TT n
pToV (Int -> String -> Name
sMN Int
vd String
"vlet") (TT Name -> TT Name
forall n. TT n -> TT n
addBinder TT Name
sc')
TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
c TT Name
t' TT Name
v') TT Name
sc'')
quote Int
i (VApp Value
f Value
a) = (TT Name -> TT Name -> TT Name)
-> State EvalState (TT Name)
-> State EvalState (TT Name)
-> State EvalState (TT Name)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
MaybeHoles) (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
f) (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
a)
quote Int
i (VType UExp
u) = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> TT Name
forall n. UExp -> TT n
TType UExp
u)
quote Int
i (VUType Universe
u) = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe -> TT Name
forall n. Universe -> TT n
UType Universe
u)
quote Int
i Value
VErased = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Erased
quote Int
i Value
VImpossible = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Impossible
quote Int
i (VProj Value
v Int
j) = do TT Name
v' <- Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
v
TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Int -> TT Name
forall n. TT n -> Int -> TT n
Proj TT Name
v' Int
j)
quote Int
i (VConstant Const
c) = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> State EvalState (TT Name))
-> TT Name -> State EvalState (TT Name)
forall a b. (a -> b) -> a -> b
$ Const -> TT Name
forall n. Const -> TT n
Constant Const
c
quote Int
i (VTmp Int
x) = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> State EvalState (TT Name))
-> TT Name -> State EvalState (TT Name)
forall a b. (a -> b) -> a -> b
$ Int -> TT Name
forall n. Int -> TT n
V (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
wknV :: Int -> Value -> Eval Value
wknV :: Int -> Value -> Eval Value
wknV Int
i (VV Int
x) | Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
i = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Int -> Value
VV (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
wknV Int
i (VBind Bool
red Name
n Binder Value
b Value -> Eval Value
sc) = do Binder Value
b' <- (Value -> Eval Value)
-> Binder Value -> StateT EvalState Identity (Binder Value)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder a -> m (Binder b)
fmapMB (Int -> Value -> Eval Value
wknV Int
i) Binder Value
b
Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Binder Value -> (Value -> Eval Value) -> Value
VBind Bool
red Name
n Binder Value
b' (\Value
x -> do Value
x' <- Value -> Eval Value
sc Value
x
Int -> Value -> Eval Value
wknV (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Value
x')
wknV Int
i (VApp Value
f Value
a) = (Value -> Value -> Value) -> Eval Value -> Eval Value -> Eval Value
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Value -> Value -> Value
VApp (Int -> Value -> Eval Value
wknV Int
i Value
f) (Int -> Value -> Eval Value
wknV Int
i Value
a)
wknV Int
i Value
t = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
t
isUniverse :: Term -> Bool
isUniverse :: TT Name -> Bool
isUniverse (TType UExp
_) = Bool
True
isUniverse (UType Universe
_) = Bool
True
isUniverse TT Name
_ = Bool
False
isUsableUniverse :: Term -> Bool
isUsableUniverse :: TT Name -> Bool
isUsableUniverse (UType Universe
NullType) = Bool
False
isUsableUniverse TT Name
x = TT Name -> Bool
isUniverse TT Name
x
convEq' :: Context -> [Name] -> TT Name -> TT Name -> TC Bool
convEq' Context
ctxt [Name]
hs TT Name
x TT Name
y = StateT UCs TC Bool -> UCs -> TC Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq Context
ctxt [Name]
hs TT Name
x TT Name
y) (Int
0, [])
convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq Context
ctxt [Name]
holes TT Name
topx TT Name
topy = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [] TT Name
topx TT Name
topy where
ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps (P NameType
xt Name
x TT Name
_) (P NameType
yt Name
y TT Name
_)
| Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
| Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y Bool -> Bool -> Bool
|| (Name
x, Name
y) (Name, Name) -> [(Name, Name)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, Name)]
ps Bool -> Bool -> Bool
|| (Name
y,Name
x) (Name, Name) -> [(Name, Name)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, Name)]
ps = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
| Bool
otherwise = [(Name, Name)] -> Name -> Name -> StateT UCs TC Bool
sameDefs [(Name, Name)]
ps Name
x Name
y
ceq [(Name, Name)]
ps (Bind Name
n (PVar RigCount
_ TT Name
t) TT Name
sc) TT Name
y = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
sc TT Name
y
ceq [(Name, Name)]
ps TT Name
x (Bind Name
n (PVar RigCount
_ TT Name
t) TT Name
sc) = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
sc
ceq [(Name, Name)]
ps (Bind Name
n (PVTy TT Name
t) TT Name
sc) TT Name
y = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
sc TT Name
y
ceq [(Name, Name)]
ps TT Name
x (Bind Name
n (PVTy TT Name
t) TT Name
sc) = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
sc
ceq [(Name, Name)]
ps (V Int
x) (V Int
y) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y)
ceq [(Name, Name)]
ps (V Int
x) (P NameType
_ Name
y TT Name
_)
| Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& [(Name, Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
x = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, Name) -> Name
forall a b. (a, b) -> a
fst ([(Name, Name)]
ps[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
x) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y)
| Bool
otherwise = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
ceq [(Name, Name)]
ps (P NameType
_ Name
x TT Name
_) (V Int
y)
| Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& [(Name, Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
y = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== (Name, Name) -> Name
forall a b. (a, b) -> b
snd ([(Name, Name)]
ps[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
y))
| Bool
otherwise = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
ceq [(Name, Name)]
ps (Bind Name
n Binder (TT Name)
xb TT Name
xs) (Bind Name
n' Binder (TT Name)
yb TT Name
ys)
= (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)]
-> Binder (TT Name) -> Binder (TT Name) -> StateT UCs TC Bool
ceqB [(Name, Name)]
ps Binder (TT Name)
xb Binder (TT Name)
yb) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq ((Name
n,Name
n')(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) TT Name
xs TT Name
ys)
where
ceqB :: [(Name, Name)]
-> Binder (TT Name) -> Binder (TT Name) -> StateT UCs TC Bool
ceqB [(Name, Name)]
ps (Let RigCount
c TT Name
v TT Name
t) (Let RigCount
c' TT Name
v' TT Name
t') = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
v TT Name
v') ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
t TT Name
t')
ceqB [(Name, Name)]
ps (Guess TT Name
v TT Name
t) (Guess TT Name
v' TT Name
t') = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
v TT Name
v') ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
t TT Name
t')
ceqB [(Name, Name)]
ps (Pi RigCount
r Maybe ImplicitInfo
i TT Name
v TT Name
t) (Pi RigCount
r' Maybe ImplicitInfo
i' TT Name
v' TT Name
t') = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
v TT Name
v') ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
t TT Name
t')
ceqB [(Name, Name)]
ps Binder (TT Name)
b Binder (TT Name)
b' = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b) (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b')
ceq [(Name, Name)]
ps TT Name
x (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
y (V Int
0)))
= [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x (TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
t) TT Name
y)
ceq [(Name, Name)]
ps (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
x (V Int
0))) TT Name
y
= [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps (TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
t) TT Name
x) TT Name
y
ceq [(Name, Name)]
ps TT Name
x (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
y (P NameType
Bound Name
n' TT Name
_)))
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
y
ceq [(Name, Name)]
ps (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
x (P NameType
Bound Name
n' TT Name
_))) TT Name
y
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
y
ceq [(Name, Name)]
ps x :: TT Name
x@(App AppStatus Name
_ TT Name
_ TT Name
_) y :: TT Name
y@(App AppStatus Name
_ TT Name
_ TT Name
_)
| (P NameType
_ Name
cx TT Name
_, [TT Name]
xargs) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
x,
(P NameType
_ Name
cy TT Name
_, [TT Name]
yargs) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
y,
Name -> Bool
caseName Name
cx Bool -> Bool -> Bool
&& Name -> Bool
caseName Name
cy = [(Name, Name)]
-> Name -> Name -> [TT Name] -> [TT Name] -> StateT UCs TC Bool
sameCase [(Name, Name)]
ps Name
cx Name
cy [TT Name]
xargs [TT Name]
yargs
ceq [(Name, Name)]
ps (App AppStatus Name
_ TT Name
fx TT Name
ax) (App AppStatus Name
_ TT Name
fy TT Name
ay) = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
fx TT Name
fy) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
ax TT Name
ay)
ceq [(Name, Name)]
ps (Constant Const
x) (Constant Const
y) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const
x Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
y)
ceq [(Name, Name)]
ps (TType UExp
x) (TType UExp
y) | UExp
x UExp -> UExp -> Bool
forall a. Eq a => a -> a -> Bool
== UExp
y = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
ceq [(Name, Name)]
ps (TType (UVal Int
0)) (TType UExp
y) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
ceq [(Name, Name)]
ps (TType UExp
x) (TType UExp
y) = do (Int
v, [UConstraint]
cs) <- StateT UCs TC UCs
forall s (m :: * -> *). MonadState s m => m s
get
UCs -> StateT UCs TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
v, UExp -> UExp -> UConstraint
ULE UExp
x UExp
y UConstraint -> [UConstraint] -> [UConstraint]
forall a. a -> [a] -> [a]
: [UConstraint]
cs)
Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
ceq [(Name, Name)]
ps (UType Universe
AllTypes) TT Name
x = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Bool
isUsableUniverse TT Name
x)
ceq [(Name, Name)]
ps TT Name
x (UType Universe
AllTypes) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Bool
isUsableUniverse TT Name
x)
ceq [(Name, Name)]
ps (UType Universe
u) (UType Universe
v) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe
u Universe -> Universe -> Bool
forall a. Eq a => a -> a -> Bool
== Universe
v)
ceq [(Name, Name)]
ps TT Name
Erased TT Name
_ = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
ceq [(Name, Name)]
ps TT Name
_ TT Name
Erased = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
ceq [(Name, Name)]
ps TT Name
x TT Name
y = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
caseeq :: [(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq [(Name, Name)]
ps (Case CaseType
_ Name
n [CaseAlt' (TT Name)]
cs) (Case CaseType
_ Name
n' [CaseAlt' (TT Name)]
cs') = [(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA ((Name
n,Name
n')(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) [CaseAlt' (TT Name)]
cs [CaseAlt' (TT Name)]
cs'
where
caseeqA :: [(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA [(Name, Name)]
ps (ConCase Name
x Int
i [Name]
as SC
sc : [CaseAlt' (TT Name)]
rest) (ConCase Name
x' Int
i' [Name]
as' SC
sc' : [CaseAlt' (TT Name)]
rest')
= do Bool
q1 <- [(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq ([Name] -> [Name] -> [(Name, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
as [Name]
as' [(Name, Name)] -> [(Name, Name)] -> [(Name, Name)]
forall a. [a] -> [a] -> [a]
++ [(Name, Name)]
ps) SC
sc SC
sc'
Bool
q2 <- [(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA [(Name, Name)]
ps [CaseAlt' (TT Name)]
rest [CaseAlt' (TT Name)]
rest'
Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> StateT UCs TC Bool) -> Bool -> StateT UCs TC Bool
forall a b. (a -> b) -> a -> b
$ Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i' Bool -> Bool -> Bool
&& Bool
q1 Bool -> Bool -> Bool
&& Bool
q2
caseeqA [(Name, Name)]
ps (ConstCase Const
x SC
sc : [CaseAlt' (TT Name)]
rest) (ConstCase Const
x' SC
sc' : [CaseAlt' (TT Name)]
rest')
= do Bool
q1 <- [(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq [(Name, Name)]
ps SC
sc SC
sc'
Bool
q2 <- [(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA [(Name, Name)]
ps [CaseAlt' (TT Name)]
rest [CaseAlt' (TT Name)]
rest'
Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> StateT UCs TC Bool) -> Bool -> StateT UCs TC Bool
forall a b. (a -> b) -> a -> b
$ Const
x Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
x' Bool -> Bool -> Bool
&& Bool
q1 Bool -> Bool -> Bool
&& Bool
q2
caseeqA [(Name, Name)]
ps (DefaultCase SC
sc : [CaseAlt' (TT Name)]
rest) (DefaultCase SC
sc' : [CaseAlt' (TT Name)]
rest')
= (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq [(Name, Name)]
ps SC
sc SC
sc') ([(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA [(Name, Name)]
ps [CaseAlt' (TT Name)]
rest [CaseAlt' (TT Name)]
rest')
caseeqA [(Name, Name)]
ps [] [] = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
caseeqA [(Name, Name)]
ps [CaseAlt' (TT Name)]
_ [CaseAlt' (TT Name)]
_ = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
caseeq [(Name, Name)]
ps (STerm TT Name
x) (STerm TT Name
y) = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
y
caseeq [(Name, Name)]
ps (UnmatchedCase String
_) (UnmatchedCase String
_) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
caseeq [(Name, Name)]
ps SC
_ SC
_ = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
sameDefs :: [(Name, Name)] -> Name -> Name -> StateT UCs TC Bool
sameDefs [(Name, Name)]
ps Name
x Name
y = case (Name -> Context -> [Def]
lookupDef Name
x Context
ctxt, Name -> Context -> [Def]
lookupDef Name
y Context
ctxt) of
([Function TT Name
_ TT Name
xdef], [Function TT Name
_ TT Name
ydef])
-> [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq ((Name
x,Name
y)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) TT Name
xdef TT Name
ydef
([CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
xd],
[CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
yd])
-> let ([Name]
_, SC
xdef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
xd
([Name]
_, SC
ydef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
yd in
[(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq ((Name
x,Name
y)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) SC
xdef SC
ydef
([Def], [Def])
_ -> Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] ->
StateT UCs TC Bool
sameCase :: [(Name, Name)]
-> Name -> Name -> [TT Name] -> [TT Name] -> StateT UCs TC Bool
sameCase [(Name, Name)]
ps Name
x Name
y [TT Name]
xargs [TT Name]
yargs
= case (Name -> Context -> [Def]
lookupDef Name
x Context
ctxt, Name -> Context -> [Def]
lookupDef Name
y Context
ctxt) of
([Function TT Name
_ TT Name
xdef], [Function TT Name
_ TT Name
ydef])
-> [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq ((Name
x,Name
y)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) TT Name
xdef TT Name
ydef
([CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
xd],
[CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
yd])
-> let ([Name]
xin, SC
xdef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
xd
([Name]
yin, SC
ydef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
yd in
do (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&)
(do [Bool]
ok <- (TT Name -> TT Name -> StateT UCs TC Bool)
-> [TT Name] -> [TT Name] -> StateT UCs TC [Bool]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps)
(Int -> [TT Name] -> [TT Name]
forall a. Int -> [a] -> [a]
drop ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
xin) [TT Name]
xargs)
(Int -> [TT Name] -> [TT Name]
forall a. Int -> [a] -> [a]
drop ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
yin) [TT Name]
yargs)
Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
ok))
([(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq ((Name
x,Name
y)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) SC
xdef SC
ydef)
([Def], [Def])
_ -> Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
data Def = Function !Type !Term
| TyDecl NameType !Type
| Operator Type Int ([Value] -> Maybe Value)
| CaseOp CaseInfo
!Type
![(Type, Bool)]
![Either Term (Term, Term)]
![([Name], Term, Term)]
!CaseDefs
deriving (forall x. Def -> Rep Def x)
-> (forall x. Rep Def x -> Def) -> Generic Def
forall x. Rep Def x -> Def
forall x. Def -> Rep Def x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Def -> Rep Def x
from :: forall x. Def -> Rep Def x
$cto :: forall x. Rep Def x -> Def
to :: forall x. Rep Def x -> Def
Generic
data CaseDefs = CaseDefs {
CaseDefs -> ([Name], SC)
cases_compiletime :: !([Name], SC),
CaseDefs -> ([Name], SC)
cases_runtime :: !([Name], SC)
}
deriving (forall x. CaseDefs -> Rep CaseDefs x)
-> (forall x. Rep CaseDefs x -> CaseDefs) -> Generic CaseDefs
forall x. Rep CaseDefs x -> CaseDefs
forall x. CaseDefs -> Rep CaseDefs x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CaseDefs -> Rep CaseDefs x
from :: forall x. CaseDefs -> Rep CaseDefs x
$cto :: forall x. Rep CaseDefs x -> CaseDefs
to :: forall x. Rep CaseDefs x -> CaseDefs
Generic
data CaseInfo = CaseInfo {
CaseInfo -> Bool
case_inlinable :: Bool,
CaseInfo -> Bool
case_alwaysinline :: Bool,
CaseInfo -> Bool
tc_dictionary :: Bool
}
deriving (forall x. CaseInfo -> Rep CaseInfo x)
-> (forall x. Rep CaseInfo x -> CaseInfo) -> Generic CaseInfo
forall x. Rep CaseInfo x -> CaseInfo
forall x. CaseInfo -> Rep CaseInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CaseInfo -> Rep CaseInfo x
from :: forall x. CaseInfo -> Rep CaseInfo x
$cto :: forall x. Rep CaseInfo x -> CaseInfo
to :: forall x. Rep CaseInfo x -> CaseInfo
Generic
instance Show Def where
show :: Def -> String
show (Function TT Name
ty TT Name
tm) = String
"Function: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (TT Name, TT Name) -> String
forall a. Show a => a -> String
show (TT Name
ty, TT Name
tm)
show (TyDecl NameType
nt TT Name
ty) = String
"TyDecl: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NameType -> String
forall a. Show a => a -> String
show NameType
nt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
ty
show (Operator TT Name
ty Int
_ [Value] -> Maybe Value
_) = String
"Operator: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
ty
show (CaseOp (CaseInfo Bool
inlc Bool
inla Bool
inlr) TT Name
ty [(TT Name, Bool)]
atys [Either (TT Name) (TT Name, TT Name)]
ps_in [([Name], TT Name, TT Name)]
ps CaseDefs
cd)
= let ([Name]
ns, SC
sc) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd
([Name]
ns', SC
sc') = CaseDefs -> ([Name], SC)
cases_runtime CaseDefs
cd in
String
"Case: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [([Name], TT Name, TT Name)] -> String
forall a. Show a => a -> String
show [([Name], TT Name, TT Name)]
ps String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"COMPILE TIME:\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
[Name] -> String
forall a. Show a => a -> String
show [Name]
ns String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
sc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"RUN TIME:\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
[Name] -> String
forall a. Show a => a -> String
show [Name]
ns' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
sc' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
if Bool
inlc then String
"Inlinable" else String
"Not inlinable" String -> ShowS
forall a. [a] -> [a] -> [a]
++
if Bool
inla then String
" Aggressively\n" else String
"\n"
data Accessibility = Hidden | Public | Frozen | Private
deriving (Accessibility -> Accessibility -> Bool
(Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Bool) -> Eq Accessibility
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Accessibility -> Accessibility -> Bool
== :: Accessibility -> Accessibility -> Bool
$c/= :: Accessibility -> Accessibility -> Bool
/= :: Accessibility -> Accessibility -> Bool
Eq, Eq Accessibility
Eq Accessibility =>
(Accessibility -> Accessibility -> Ordering)
-> (Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Accessibility)
-> (Accessibility -> Accessibility -> Accessibility)
-> Ord Accessibility
Accessibility -> Accessibility -> Bool
Accessibility -> Accessibility -> Ordering
Accessibility -> Accessibility -> Accessibility
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Accessibility -> Accessibility -> Ordering
compare :: Accessibility -> Accessibility -> Ordering
$c< :: Accessibility -> Accessibility -> Bool
< :: Accessibility -> Accessibility -> Bool
$c<= :: Accessibility -> Accessibility -> Bool
<= :: Accessibility -> Accessibility -> Bool
$c> :: Accessibility -> Accessibility -> Bool
> :: Accessibility -> Accessibility -> Bool
$c>= :: Accessibility -> Accessibility -> Bool
>= :: Accessibility -> Accessibility -> Bool
$cmax :: Accessibility -> Accessibility -> Accessibility
max :: Accessibility -> Accessibility -> Accessibility
$cmin :: Accessibility -> Accessibility -> Accessibility
min :: Accessibility -> Accessibility -> Accessibility
Ord, (forall x. Accessibility -> Rep Accessibility x)
-> (forall x. Rep Accessibility x -> Accessibility)
-> Generic Accessibility
forall x. Rep Accessibility x -> Accessibility
forall x. Accessibility -> Rep Accessibility x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Accessibility -> Rep Accessibility x
from :: forall x. Accessibility -> Rep Accessibility x
$cto :: forall x. Rep Accessibility x -> Accessibility
to :: forall x. Rep Accessibility x -> Accessibility
Generic)
instance Show Accessibility where
show :: Accessibility -> String
show Accessibility
Public = String
"public export"
show Accessibility
Frozen = String
"export"
show Accessibility
Private = String
"private"
show Accessibility
Hidden = String
"hidden"
type Injectivity = Bool
data Totality = Total [Int]
| Productive
| Partial PReason
| Unchecked
| Generated
deriving (Totality -> Totality -> Bool
(Totality -> Totality -> Bool)
-> (Totality -> Totality -> Bool) -> Eq Totality
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Totality -> Totality -> Bool
== :: Totality -> Totality -> Bool
$c/= :: Totality -> Totality -> Bool
/= :: Totality -> Totality -> Bool
Eq, (forall x. Totality -> Rep Totality x)
-> (forall x. Rep Totality x -> Totality) -> Generic Totality
forall x. Rep Totality x -> Totality
forall x. Totality -> Rep Totality x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Totality -> Rep Totality x
from :: forall x. Totality -> Rep Totality x
$cto :: forall x. Rep Totality x -> Totality
to :: forall x. Rep Totality x -> Totality
Generic)
data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
| ExternalIO | BelieveMe | Mutual [Name] | NotProductive
deriving (Int -> PReason -> ShowS
[PReason] -> ShowS
PReason -> String
(Int -> PReason -> ShowS)
-> (PReason -> String) -> ([PReason] -> ShowS) -> Show PReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PReason -> ShowS
showsPrec :: Int -> PReason -> ShowS
$cshow :: PReason -> String
show :: PReason -> String
$cshowList :: [PReason] -> ShowS
showList :: [PReason] -> ShowS
Show, PReason -> PReason -> Bool
(PReason -> PReason -> Bool)
-> (PReason -> PReason -> Bool) -> Eq PReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PReason -> PReason -> Bool
== :: PReason -> PReason -> Bool
$c/= :: PReason -> PReason -> Bool
/= :: PReason -> PReason -> Bool
Eq, (forall x. PReason -> Rep PReason x)
-> (forall x. Rep PReason x -> PReason) -> Generic PReason
forall x. Rep PReason x -> PReason
forall x. PReason -> Rep PReason x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PReason -> Rep PReason x
from :: forall x. PReason -> Rep PReason x
$cto :: forall x. Rep PReason x -> PReason
to :: forall x. Rep PReason x -> PReason
Generic)
instance Show Totality where
show :: Totality -> String
show (Total [Int]
args)= String
"Total"
show Totality
Productive = String
"Productive"
show Totality
Unchecked = String
"not yet checked for totality"
show (Partial PReason
Itself) = String
"possibly not total as it is not well founded"
show (Partial PReason
NotCovering) = String
"not total as there are missing cases"
show (Partial PReason
NotPositive) = String
"not strictly positive"
show (Partial PReason
ExternalIO) = String
"an external IO primitive"
show (Partial PReason
NotProductive) = String
"not productive"
show (Partial PReason
BelieveMe) = String
"not total due to use of believe_me in proof"
show (Partial (Other [Name]
ns)) = String
"possibly not total due to: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
", " ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
forall a. Show a => a -> String
show [Name]
ns)
show (Partial (Mutual [Name]
ns)) = String
"possibly not total due to recursive path " String -> ShowS
forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
showSep String
" --> " ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
forall a. Show a => a -> String
show [Name]
ns)
show (Partial (UseUndef Name
n)) = String
"possibly not total because it uses the undefined name " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
show Totality
Generated = String
"auto-generated"
data MetaInformation =
EmptyMI
| DataMI [Int]
deriving (MetaInformation -> MetaInformation -> Bool
(MetaInformation -> MetaInformation -> Bool)
-> (MetaInformation -> MetaInformation -> Bool)
-> Eq MetaInformation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaInformation -> MetaInformation -> Bool
== :: MetaInformation -> MetaInformation -> Bool
$c/= :: MetaInformation -> MetaInformation -> Bool
/= :: MetaInformation -> MetaInformation -> Bool
Eq, Int -> MetaInformation -> ShowS
[MetaInformation] -> ShowS
MetaInformation -> String
(Int -> MetaInformation -> ShowS)
-> (MetaInformation -> String)
-> ([MetaInformation] -> ShowS)
-> Show MetaInformation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaInformation -> ShowS
showsPrec :: Int -> MetaInformation -> ShowS
$cshow :: MetaInformation -> String
show :: MetaInformation -> String
$cshowList :: [MetaInformation] -> ShowS
showList :: [MetaInformation] -> ShowS
Show, (forall x. MetaInformation -> Rep MetaInformation x)
-> (forall x. Rep MetaInformation x -> MetaInformation)
-> Generic MetaInformation
forall x. Rep MetaInformation x -> MetaInformation
forall x. MetaInformation -> Rep MetaInformation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaInformation -> Rep MetaInformation x
from :: forall x. MetaInformation -> Rep MetaInformation x
$cto :: forall x. Rep MetaInformation x -> MetaInformation
to :: forall x. Rep MetaInformation x -> MetaInformation
Generic)
data Context = MkContext {
Context -> Int
next_tvar :: Int,
Context -> Ctxt TTDecl
definitions :: Ctxt TTDecl
} deriving (Int -> Context -> ShowS
[Context] -> ShowS
Context -> String
(Int -> Context -> ShowS)
-> (Context -> String) -> ([Context] -> ShowS) -> Show Context
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Context -> ShowS
showsPrec :: Int -> Context -> ShowS
$cshow :: Context -> String
show :: Context -> String
$cshowList :: [Context] -> ShowS
showList :: [Context] -> ShowS
Show, (forall x. Context -> Rep Context x)
-> (forall x. Rep Context x -> Context) -> Generic Context
forall x. Rep Context x -> Context
forall x. Context -> Rep Context x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Context -> Rep Context x
from :: forall x. Context -> Rep Context x
$cto :: forall x. Rep Context x -> Context
to :: forall x. Rep Context x -> Context
Generic)
type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
initContext :: Context
initContext = Int -> Ctxt TTDecl -> Context
MkContext Int
0 Ctxt TTDecl
forall {k} {a}. Map k a
emptyContext
mapDefCtxt :: (Def -> Def) -> Context -> Context
mapDefCtxt :: (Def -> Def) -> Context -> Context
mapDefCtxt Def -> Def
f (MkContext Int
t !Ctxt TTDecl
defs) = Int -> Ctxt TTDecl -> Context
MkContext Int
t ((TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a b. (a -> b) -> Ctxt a -> Ctxt b
mapCtxt TTDecl -> TTDecl
forall {b} {c} {d} {e} {f} {t}. (Def, b, c, d, e, f) -> t
f' Ctxt TTDecl
defs)
where f' :: (Def, b, c, d, e, f) -> t
f' (!Def
d, b
r, c
i, d
a, e
t, f
m) = (Def, b, c, d, e, f) -> t
f' (Def -> Def
f Def
d, b
r, c
i, d
a, e
t, f
m)
ctxtAlist :: Context -> [(Name, Def)]
ctxtAlist :: Context -> [(Name, Def)]
ctxtAlist Context
ctxt = ((Name, TTDecl) -> (Name, Def))
-> [(Name, TTDecl)] -> [(Name, Def)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) -> (Name
n, Def
d)) ([(Name, TTDecl)] -> [(Name, Def)])
-> [(Name, TTDecl)] -> [(Name, Def)]
forall a b. (a -> b) -> a -> b
$ Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Ctxt a -> [(Name, a)]
toAlist (Context -> Ctxt TTDecl
definitions Context
ctxt)
veval :: Context -> Env -> TT Name -> Value
veval Context
ctxt Env
env TT Name
t = Eval Value -> EvalState -> Value
forall s a. State s a -> s -> a
evalState (Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [] Env
env TT Name
t []) EvalState
initEval
addToCtxt :: Name -> Term -> Type -> Context -> Context
addToCtxt :: Name -> TT Name -> TT Name -> Context -> Context
addToCtxt Name
n TT Name
tm TT Name
ty Context
uctxt
= let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
!ctxt' :: Ctxt TTDecl
ctxt' = Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (TT Name -> TT Name -> Def
Function TT Name
ty TT Name
tm, RigCount
RigW, Bool
False, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt in
Context
uctxt { definitions = ctxt' }
setAccess :: Name -> Accessibility -> Context -> Context
setAccess :: Name -> Accessibility -> Context -> Context
setAccess Name
n Accessibility
a Context
uctxt
= let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
!ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
r, Bool
i, Accessibility
_, Totality
t, MetaInformation
m) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
Context
uctxt { definitions = ctxt' }
setInjective :: Name -> Injectivity -> Context -> Context
setInjective :: Name -> Bool -> Context -> Context
setInjective Name
n Bool
i Context
uctxt
= let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
!ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
r, Bool
_, Accessibility
a, Totality
t, MetaInformation
m) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
Context
uctxt { definitions = ctxt' }
setTotal :: Name -> Totality -> Context -> Context
setTotal :: Name -> Totality -> Context -> Context
setTotal Name
n Totality
t Context
uctxt
= let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
!ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
_, MetaInformation
m) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
Context
uctxt { definitions = ctxt' }
setRigCount :: Name -> RigCount -> Context -> Context
setRigCount :: Name -> RigCount -> Context -> Context
setRigCount Name
n RigCount
rc Context
uctxt
= let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
!ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
_, Bool
i, Accessibility
a, Totality
t, MetaInformation
m) -> (Def
d, RigCount
rc, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
Context
uctxt { definitions = ctxt' }
setMetaInformation :: Name -> MetaInformation -> Context -> Context
setMetaInformation :: Name -> MetaInformation -> Context -> Context
setMetaInformation Name
n MetaInformation
m Context
uctxt
= let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
!ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
_) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
Context
uctxt { definitions = ctxt' }
addCtxtDef :: Name -> Def -> Context -> Context
addCtxtDef :: Name -> Def -> Context -> Context
addCtxtDef Name
n Def
d Context
c = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
c
!ctxt' :: Ctxt TTDecl
ctxt' = Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (Def
d, RigCount
RigW, Bool
False, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) (Ctxt TTDecl -> Ctxt TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a b. (a -> b) -> a -> b
$! Ctxt TTDecl
ctxt in
Context
c { definitions = ctxt' }
addTyDecl :: Name -> NameType -> Type -> Context -> Context
addTyDecl :: Name -> NameType -> TT Name -> Context -> Context
addTyDecl Name
n NameType
nt TT Name
ty Context
uctxt
= let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
!ctxt' :: Ctxt TTDecl
ctxt' = Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (NameType -> TT Name -> Def
TyDecl NameType
nt TT Name
ty, RigCount
RigW, Bool
False, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt in
Context
uctxt { definitions = ctxt' }
addDatatype :: Datatype Name -> Context -> Context
addDatatype :: Datatype Name -> Context -> Context
addDatatype (Data Name
n Int
tag TT Name
ty Bool
unique [(Name, TT Name)]
cons) Context
uctxt
= let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
ty' :: TT Name
ty' = Context -> Env -> TT Name -> TT Name
normalise Context
uctxt [] TT Name
ty
!ctxt' :: Ctxt TTDecl
ctxt' = Int -> [(Name, TT Name)] -> Ctxt TTDecl -> Ctxt TTDecl
addCons Int
0 [(Name, TT Name)]
cons (Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n
(NameType -> TT Name -> Def
TyDecl (Int -> Int -> NameType
TCon Int
tag (TT Name -> Int
forall n. TT n -> Int
arity TT Name
ty')) TT Name
ty, RigCount
RigW, Bool
True, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt) in
Context
uctxt { definitions = ctxt' }
where
addCons :: Int -> [(Name, TT Name)] -> Ctxt TTDecl -> Ctxt TTDecl
addCons Int
tag [] Ctxt TTDecl
ctxt = Ctxt TTDecl
ctxt
addCons Int
tag ((Name
n, TT Name
ty) : [(Name, TT Name)]
cons) Ctxt TTDecl
ctxt
= let ty' :: TT Name
ty' = Context -> Env -> TT Name -> TT Name
normalise Context
uctxt [] TT Name
ty in
Int -> [(Name, TT Name)] -> Ctxt TTDecl -> Ctxt TTDecl
addCons (Int
tagInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [(Name, TT Name)]
cons (Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n
(NameType -> TT Name -> Def
TyDecl (Int -> Int -> Bool -> NameType
DCon Int
tag (TT Name -> Int
forall n. TT n -> Int
arity TT Name
ty') Bool
unique) TT Name
ty, RigCount
RigW, Bool
True, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt)
addCasedef :: Name -> ErasureInfo -> CaseInfo ->
Bool -> SC ->
Bool -> Bool ->
[(Type, Bool)] ->
[Int] ->
[Either Term (Term, Term)] ->
[([Name], Term, Term)] ->
[([Name], Term, Term)] ->
Type -> Context -> TC Context
addCasedef :: Name
-> ErasureInfo
-> CaseInfo
-> Bool
-> SC
-> Bool
-> Bool
-> [(TT Name, Bool)]
-> [Int]
-> [Either (TT Name) (TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
-> TT Name
-> Context
-> TC Context
addCasedef Name
n ErasureInfo
ei ci :: CaseInfo
ci@(CaseInfo Bool
inline Bool
alwaysInline Bool
tcdict)
Bool
tcase SC
covering Bool
reflect Bool
asserted [(TT Name, Bool)]
argtys [Int]
inacc
[Either (TT Name) (TT Name, TT Name)]
ps_in [([Name], TT Name, TT Name)]
ps_ct [([Name], TT Name, TT Name)]
ps_rt TT Name
ty Context
uctxt
= do let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
access :: Accessibility
access = case Name -> Bool -> Context -> [(Def, Accessibility)]
lookupDefAcc Name
n Bool
False Context
uctxt of
[(Def
_, Accessibility
acc)] -> Accessibility
acc
[(Def, Accessibility)]
_ -> Accessibility
Public
CaseDef
compileTime <- Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(TT Name, Bool)]
-> [([Name], TT Name, TT Name)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
tcase SC
covering Bool
reflect Phase
CompileTime FC
emptyFC [Int]
inacc [(TT Name, Bool)]
argtys [([Name], TT Name, TT Name)]
ps_ct ErasureInfo
ei
CaseDef
runtime <- Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(TT Name, Bool)]
-> [([Name], TT Name, TT Name)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
tcase SC
covering Bool
reflect Phase
RunTime FC
emptyFC [Int]
inacc [(TT Name, Bool)]
argtys [([Name], TT Name, TT Name)]
ps_rt ErasureInfo
ei
Ctxt TTDecl
ctxt' <- case (CaseDef
compileTime, CaseDef
runtime) of
( CaseDef [Name]
args_ct SC
sc_ct [TT Name]
_,
CaseDef [Name]
args_rt SC
sc_rt [TT Name]
_) ->
let inl :: Bool
inl = Bool
alwaysInline
inlc :: Bool
inlc = (Bool
inl Bool -> Bool -> Bool
|| Name -> [Name] -> SC -> Bool
small Name
n [Name]
args_rt SC
sc_rt) Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
asserted)
cdef :: CaseDefs
cdef = ([Name], SC) -> ([Name], SC) -> CaseDefs
CaseDefs ([Name]
args_ct, SC
sc_ct)
([Name]
args_rt, SC
sc_rt)
op :: TTDecl
op = (CaseInfo
-> TT Name
-> [(TT Name, Bool)]
-> [Either (TT Name) (TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
-> CaseDefs
-> Def
CaseOp (CaseInfo
ci { case_inlinable = inlc })
TT Name
ty [(TT Name, Bool)]
argtys [Either (TT Name) (TT Name, TT Name)]
ps_in [([Name], TT Name, TT Name)]
ps_ct CaseDefs
cdef,
RigCount
RigW, Bool
False, Accessibility
access, Totality
Unchecked, MetaInformation
EmptyMI)
in Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ctxt TTDecl -> TC (Ctxt TTDecl))
-> Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a b. (a -> b) -> a -> b
$ Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n TTDecl
op Ctxt TTDecl
ctxt
Context -> TC Context
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Context
uctxt { definitions = ctxt' }
simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
simplifyCasedef Name
n [Name]
ufnames [[Name]]
umethss ErasureInfo
ei Context
uctxt
= do let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
Ctxt TTDecl
ctxt' <- case Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n Ctxt TTDecl
ctxt of
[(CaseOp CaseInfo
ci TT Name
ty [(TT Name, Bool)]
atys [] [([Name], TT Name, TT Name)]
ps CaseDefs
_, RigCount
rc, Bool
inj, Accessibility
acc, Totality
tot, MetaInformation
metainf)] ->
Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Ctxt TTDecl
ctxt
[(CaseOp CaseInfo
ci TT Name
ty [(TT Name, Bool)]
atys [Either (TT Name) (TT Name, TT Name)]
ps_in [([Name], TT Name, TT Name)]
ps CaseDefs
cd, RigCount
rc, Bool
inj, Accessibility
acc, Totality
tot, MetaInformation
metainf)] ->
do let ps_in' :: [Either (TT Name) (TT Name, TT Name)]
ps_in' = (Either (TT Name) (TT Name, TT Name)
-> Either (TT Name) (TT Name, TT Name))
-> [Either (TT Name) (TT Name, TT Name)]
-> [Either (TT Name) (TT Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map Either (TT Name) (TT Name, TT Name)
-> Either (TT Name) (TT Name, TT Name)
forall {a} {a}. Either a (a, TT Name) -> Either a (a, TT Name)
simpl [Either (TT Name) (TT Name, TT Name)]
ps_in
pdef :: [([Name], TT Name, TT Name)]
pdef = (Either (TT Name) (TT Name, TT Name) -> ([Name], TT Name, TT Name))
-> [Either (TT Name) (TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map Either (TT Name) (TT Name, TT Name) -> ([Name], TT Name, TT Name)
forall {n} {n}. Either (TT n) (TT n, TT n) -> ([n], TT n, TT n)
debind [Either (TT Name) (TT Name, TT Name)]
ps_in'
CaseDef [Name]
args SC
sc [TT Name]
_ <- Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(TT Name, Bool)]
-> [([Name], TT Name, TT Name)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
False (TT Name -> SC
forall t. t -> SC' t
STerm TT Name
forall n. TT n
Erased) Bool
False Phase
CompileTime FC
emptyFC [] [(TT Name, Bool)]
atys [([Name], TT Name, TT Name)]
pdef ErasureInfo
ei
Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ctxt TTDecl -> TC (Ctxt TTDecl))
-> Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a b. (a -> b) -> a -> b
$ Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (CaseInfo
-> TT Name
-> [(TT Name, Bool)]
-> [Either (TT Name) (TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
-> CaseDefs
-> Def
CaseOp CaseInfo
ci
TT Name
ty [(TT Name, Bool)]
atys [Either (TT Name) (TT Name, TT Name)]
ps_in' [([Name], TT Name, TT Name)]
ps (CaseDefs
cd { cases_compiletime = (args, sc) }),
RigCount
rc, Bool
inj, Accessibility
acc, Totality
tot, MetaInformation
metainf) Ctxt TTDecl
ctxt
[TTDecl]
_ -> Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Ctxt TTDecl
ctxt
Context -> TC Context
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Context
uctxt { definitions = ctxt' }
where
depat :: [n] -> TT n -> ([n], TT n)
depat [n]
acc (Bind n
n (PVar RigCount
_ TT n
t) TT n
sc)
= [n] -> TT n -> ([n], TT n)
depat (n
n n -> [n] -> [n]
forall a. a -> [a] -> [a]
: [n]
acc) (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
instantiate (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n TT n
t) TT n
sc)
depat [n]
acc TT n
x = ([n]
acc, TT n
x)
debind :: Either (TT n) (TT n, TT n) -> ([n], TT n, TT n)
debind (Right (TT n
x, TT n
y)) = let ([n]
vs, TT n
x') = [n] -> TT n -> ([n], TT n)
forall {n}. [n] -> TT n -> ([n], TT n)
depat [] TT n
x
([n]
_, TT n
y') = [n] -> TT n -> ([n], TT n)
forall {n}. [n] -> TT n -> ([n], TT n)
depat [] TT n
y in
([n]
vs, TT n
x', TT n
y')
debind (Left TT n
x) = let ([n]
vs, TT n
x') = [n] -> TT n -> ([n], TT n)
forall {n}. [n] -> TT n -> ([n], TT n)
depat [] TT n
x in
([n]
vs, TT n
x', TT n
forall n. TT n
Impossible)
simpl :: Either a (a, TT Name) -> Either a (a, TT Name)
simpl (Right (a
x, TT Name
y))
= if [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
ufnames then (a, TT Name) -> Either a (a, TT Name)
forall a b. b -> Either a b
Right (a
x, TT Name
y)
else (a, TT Name) -> Either a (a, TT Name)
forall a b. b -> Either a b
Right (a
x, Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
unfold Context
uctxt [] ((Name -> (Name, Int)) -> [Name] -> [(Name, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, Int
1)) (TT Name -> [Name]
uns TT Name
y)) TT Name
y)
simpl Either a (a, TT Name)
t = Either a (a, TT Name)
t
uns :: TT Name -> [Name]
uns TT Name
tm = [Name] -> [[Name]] -> TT Name -> [Name]
getNamesToUnfold [Name]
ufnames [[Name]]
umethss TT Name
tm
getNamesToUnfold :: [Name] -> [[Name]] -> Term -> [Name]
getNamesToUnfold :: [Name] -> [[Name]] -> TT Name -> [Name]
getNamesToUnfold [Name]
inames [[Name]]
ms TT Name
tm = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name]
inames [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
tm [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Name]]
ms
where
getNames :: Maybe Name -> TT Name -> [Name]
getNames Maybe Name
under fn :: TT Name
fn@(App AppStatus Name
_ TT Name
_ TT Name
_)
| (TT Name
f, [TT Name]
args) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
fn
= let under' :: Maybe Name
under' = case TT Name
f of
P NameType
_ Name
fn TT Name
_ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
fn
TT Name
_ -> Maybe Name
forall a. Maybe a
Nothing
in
Maybe Name -> TT Name -> [Name]
getNames Maybe Name
under TT Name
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (TT Name -> [Name]) -> [TT Name] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Maybe Name -> TT Name -> [Name]
getNames Maybe Name
under') [TT Name]
args
getNames (Just Name
under) (P NameType
_ Name
ref TT Name
_)
= if Name
ref Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inames then [Name
under] else []
getNames Maybe Name
under (Bind Name
n (Let RigCount
c TT Name
t TT Name
v) TT Name
sc)
= Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
v [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
sc
getNames Maybe Name
under (Bind Name
n Binder (TT Name)
b TT Name
sc) = Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
sc
getNames Maybe Name
_ TT Name
_ = []
addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
Context -> Context
addOperator :: Name
-> TT Name -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
n TT Name
ty Int
a [Value] -> Maybe Value
op Context
uctxt
= let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
ctxt' :: Ctxt TTDecl
ctxt' = Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (TT Name -> Int -> ([Value] -> Maybe Value) -> Def
Operator TT Name
ty Int
a [Value] -> Maybe Value
op, RigCount
RigW, Bool
False, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt in
Context
uctxt { definitions = ctxt' }
tfst :: (a, b, c, d, e, f) -> a
tfst (a
a, b
_, c
_, d
_, e
_, f
_) = a
a
lookupNames :: Name -> Context -> [Name]
lookupNames :: Name -> Context -> [Name]
lookupNames Name
n Context
ctxt
= let ns :: [(Name, TTDecl)]
ns = Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt) in
((Name, TTDecl) -> Name) -> [(Name, TTDecl)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TTDecl) -> Name
forall a b. (a, b) -> a
fst [(Name, TTDecl)]
ns
lookupTyName :: Name -> Context -> [(Name, Type)]
lookupTyName :: Name -> Context -> [(Name, TT Name)]
lookupTyName Name
n Context
ctxt = do
(Name
name, TTDecl
def) <- Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
TT Name
ty <- case TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst TTDecl
def of
(Function TT Name
ty TT Name
_) -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
(TyDecl NameType
_ TT Name
ty) -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
(Operator TT Name
ty Int
_ [Value] -> Maybe Value
_) -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
(CaseOp CaseInfo
_ TT Name
ty [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
_) -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
(Name, TT Name) -> [(Name, TT Name)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
name, TT Name
ty)
lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)
lookupTyNameExact :: Name -> Context -> Maybe (Name, TT Name)
lookupTyNameExact Name
n Context
ctxt = [(Name, TT Name)] -> Maybe (Name, TT Name)
forall a. [a] -> Maybe a
listToMaybe [ (Name
nm, TT Name
v) | (Name
nm, TT Name
v) <- Name -> Context -> [(Name, TT Name)]
lookupTyName Name
n Context
ctxt, Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n ]
lookupTy :: Name -> Context -> [Type]
lookupTy :: Name -> Context -> [TT Name]
lookupTy Name
n Context
ctxt = ((Name, TT Name) -> TT Name) -> [(Name, TT Name)] -> [TT Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TT Name) -> TT Name
forall a b. (a, b) -> b
snd (Name -> Context -> [(Name, TT Name)]
lookupTyName Name
n Context
ctxt)
lookupTyExact :: Name -> Context -> Maybe Type
lookupTyExact :: Name -> Context -> Maybe (TT Name)
lookupTyExact Name
n Context
ctxt = ((Name, TT Name) -> TT Name)
-> Maybe (Name, TT Name) -> Maybe (TT Name)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, TT Name) -> TT Name
forall a b. (a, b) -> b
snd (Name -> Context -> Maybe (Name, TT Name)
lookupTyNameExact Name
n Context
ctxt)
isCanonical :: Type -> Context -> Bool
isCanonical :: TT Name -> Context -> Bool
isCanonical TT Name
t Context
ctxt
= case TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t of
(P NameType
_ Name
n TT Name
_, [TT Name]
_) -> Name -> Context -> Bool
isConName Name
n Context
ctxt
(Constant Const
_, [TT Name]
_) -> Bool
True
(TT Name, [TT Name])
_ -> Bool
False
isConName :: Name -> Context -> Bool
isConName :: Name -> Context -> Bool
isConName Name
n Context
ctxt = Name -> Context -> Bool
isTConName Name
n Context
ctxt Bool -> Bool -> Bool
|| Name -> Context -> Bool
isDConName Name
n Context
ctxt
isTConName :: Name -> Context -> Bool
isTConName :: Name -> Context -> Bool
isTConName Name
n Context
ctxt
= case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
Just (TyDecl (TCon Int
_ Int
_) TT Name
_) -> Bool
True
Maybe Def
_ -> Bool
False
isDConName :: Name -> Context -> Bool
isDConName :: Name -> Context -> Bool
isDConName Name
n Context
ctxt
= case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
Just (TyDecl (DCon Int
_ Int
_ Bool
_) TT Name
_) -> Bool
True
Maybe Def
_ -> Bool
False
canBeDConName :: Name -> Context -> Bool
canBeDConName :: Name -> Context -> Bool
canBeDConName Name
n Context
ctxt
= [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ do TTDecl
def <- Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
case TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst TTDecl
def of
(TyDecl (DCon Int
_ Int
_ Bool
_) TT Name
_) -> Bool -> [Bool]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Def
_ -> Bool -> [Bool]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isFnName :: Name -> Context -> Bool
isFnName :: Name -> Context -> Bool
isFnName Name
n Context
ctxt
= case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
Just (Function TT Name
_ TT Name
_) -> Bool
True
Just (Operator TT Name
_ Int
_ [Value] -> Maybe Value
_) -> Bool
True
Just (CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
_) -> Bool
True
Maybe Def
_ -> Bool
False
isTCDict :: Name -> Context -> Bool
isTCDict :: Name -> Context -> Bool
isTCDict Name
n Context
ctxt
= case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
Just (Function TT Name
_ TT Name
_) -> Bool
False
Just (Operator TT Name
_ Int
_ [Value] -> Maybe Value
_) -> Bool
False
Just (CaseOp CaseInfo
ci TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
_) -> CaseInfo -> Bool
tc_dictionary CaseInfo
ci
Maybe Def
_ -> Bool
False
conGuarded :: Context -> Name -> Term -> Bool
conGuarded :: Context -> Name -> TT Name -> Bool
conGuarded Context
ctxt Name
n TT Name
tm = Name -> TT Name -> Bool
guarded Name
n TT Name
tm
where
guarded :: Name -> TT Name -> Bool
guarded Name
n (P NameType
_ Name
n' TT Name
_) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
guarded Name
n ap :: TT Name
ap@(App AppStatus Name
_ TT Name
_ TT Name
_)
| (P NameType
_ Name
f TT Name
_, [TT Name]
as) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
ap,
Name -> Context -> Bool
isConName Name
f Context
ctxt = (TT Name -> Bool) -> [TT Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> TT Name -> Bool
guarded Name
n) [TT Name]
as
guarded Name
_ TT Name
_ = Bool
False
visibleDefinitions :: Context -> Ctxt TTDecl
visibleDefinitions :: Context -> Ctxt TTDecl
visibleDefinitions Context
ctxt =
(Map Name TTDecl -> Bool) -> Ctxt TTDecl -> Ctxt TTDecl
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\Map Name TTDecl
m -> Map Name TTDecl -> Int
forall a. Map Name a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name TTDecl
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Ctxt TTDecl -> Ctxt TTDecl)
-> (Context -> Ctxt TTDecl) -> Context -> Ctxt TTDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Name TTDecl -> Map Name TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Map Name TTDecl -> Map Name TTDecl
forall {k} {a} {b} {c} {e} {f}.
Map k (a, b, c, Accessibility, e, f)
-> Map k (a, b, c, Accessibility, e, f)
onlyVisible (Ctxt TTDecl -> Ctxt TTDecl)
-> (Context -> Ctxt TTDecl) -> Context -> Ctxt TTDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Ctxt TTDecl
definitions (Context -> Ctxt TTDecl) -> Context -> Ctxt TTDecl
forall a b. (a -> b) -> a -> b
$ Context
ctxt
where
onlyVisible :: Map k (a, b, c, Accessibility, e, f)
-> Map k (a, b, c, Accessibility, e, f)
onlyVisible = ((a, b, c, Accessibility, e, f) -> Bool)
-> Map k (a, b, c, Accessibility, e, f)
-> Map k (a, b, c, Accessibility, e, f)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (a, b, c, Accessibility, e, f) -> Bool
forall {a} {b} {c} {e} {f}. (a, b, c, Accessibility, e, f) -> Bool
visible
visible :: (a, b, c, Accessibility, e, f) -> Bool
visible (a
_def, b
_rigCount, c
_injectivity, Accessibility
accessibility, e
_totality, f
_metaInformation) =
Accessibility
accessibility Accessibility -> [Accessibility] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Accessibility
Hidden, Accessibility
Private]
lookupP :: Name -> Context -> [Term]
lookupP :: Name -> Context -> [TT Name]
lookupP = Bool -> Bool -> Name -> Context -> [TT Name]
lookupP_all Bool
False Bool
False
lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
lookupP_all :: Bool -> Bool -> Name -> Context -> [TT Name]
lookupP_all Bool
all Bool
exact Name
n Context
ctxt
= do (Name
n', TTDecl
def) <- [(Name, TTDecl)]
names
(TT Name, Accessibility)
p <- case TTDecl
def of
(Function TT Name
ty TT Name
tm, RigCount
_, Bool
inj, Accessibility
a, Totality
_, MetaInformation
_) -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n' TT Name
ty, Accessibility
a)
(TyDecl NameType
nt TT Name
ty, RigCount
_, Bool
_, Accessibility
a, Totality
_, MetaInformation
_) -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n' TT Name
ty, Accessibility
a)
(CaseOp CaseInfo
_ TT Name
ty [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
_, RigCount
_, Bool
inj, Accessibility
a, Totality
_, MetaInformation
_) -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n' TT Name
ty, Accessibility
a)
(Operator TT Name
ty Int
_ [Value] -> Maybe Value
_, RigCount
_, Bool
inj, Accessibility
a, Totality
_, MetaInformation
_) -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n' TT Name
ty, Accessibility
a)
case (TT Name, Accessibility) -> Accessibility
forall a b. (a, b) -> b
snd (TT Name, Accessibility)
p of
Accessibility
Hidden -> if Bool
all then TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((TT Name, Accessibility) -> TT Name
forall a b. (a, b) -> a
fst (TT Name, Accessibility)
p) else []
Accessibility
Private -> if Bool
all then TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((TT Name, Accessibility) -> TT Name
forall a b. (a, b) -> a
fst (TT Name, Accessibility)
p) else []
Accessibility
_ -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((TT Name, Accessibility) -> TT Name
forall a b. (a, b) -> a
fst (TT Name, Accessibility)
p)
where
names :: [(Name, TTDecl)]
names = let ns :: [(Name, TTDecl)]
ns = Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt) in
if Bool
exact
then ((Name, TTDecl) -> Bool) -> [(Name, TTDecl)] -> [(Name, TTDecl)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', TTDecl
d) -> Name
n' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n) [(Name, TTDecl)]
ns
else [(Name, TTDecl)]
ns
lookupDefExact :: Name -> Context -> Maybe Def
lookupDefExact :: Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt = TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst (TTDecl -> Def) -> Maybe TTDecl -> Maybe Def
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
lookupDef :: Name -> Context -> [Def]
lookupDef :: Name -> Context -> [Def]
lookupDef Name
n Context
ctxt = TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst (TTDecl -> Def) -> [TTDecl] -> [Def]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
lookupNameDef :: Name -> Context -> [(Name, Def)]
lookupNameDef :: Name -> Context -> [(Name, Def)]
lookupNameDef Name
n Context
ctxt = (TTDecl -> Def) -> [(Name, TTDecl)] -> [(Name, Def)]
forall {t} {b} {a}. (t -> b) -> [(a, t)] -> [(a, b)]
mapSnd TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst ([(Name, TTDecl)] -> [(Name, Def)])
-> [(Name, TTDecl)] -> [(Name, Def)]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where mapSnd :: (t -> b) -> [(a, t)] -> [(a, b)]
mapSnd t -> b
f [] = []
mapSnd t -> b
f ((a
x,t
y):[(a, t)]
xys) = (a
x, t -> b
f t
y) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: (t -> b) -> [(a, t)] -> [(a, b)]
mapSnd t -> b
f [(a, t)]
xys
lookupDefAcc :: Name -> Bool -> Context ->
[(Def, Accessibility)]
lookupDefAcc :: Name -> Bool -> Context -> [(Def, Accessibility)]
lookupDefAcc Name
n Bool
mkpublic Context
ctxt
= (TTDecl -> (Def, Accessibility))
-> [TTDecl] -> [(Def, Accessibility)]
forall a b. (a -> b) -> [a] -> [b]
map TTDecl -> (Def, Accessibility)
forall {a} {b} {c} {e} {f}.
(a, b, c, Accessibility, e, f) -> (a, Accessibility)
mkp ([TTDecl] -> [(Def, Accessibility)])
-> [TTDecl] -> [(Def, Accessibility)]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where mkp :: (a, b, c, Accessibility, e, f) -> (a, Accessibility)
mkp (a
d, b
_, c
inj, Accessibility
a, e
_, f
_) = if Bool
mkpublic Bool -> Bool -> Bool
&& (Bool -> Bool
not (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_bind" Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_pure"))
then (a
d, Accessibility
Public) else (a
d, Accessibility
a)
lookupTotalAccessibility :: Name -> Context -> [(Totality,Accessibility)]
lookupTotalAccessibility :: Name -> Context -> [(Totality, Accessibility)]
lookupTotalAccessibility Name
n Context
ctxt = (TTDecl -> (Totality, Accessibility))
-> [TTDecl] -> [(Totality, Accessibility)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> (Totality, Accessibility)
forall {a} {b} {c} {b} {a} {f}. (a, b, c, b, a, f) -> (a, b)
unpack ([TTDecl] -> [(Totality, Accessibility)])
-> [TTDecl] -> [(Totality, Accessibility)]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where
unpack :: (a, b, c, b, a, f) -> (a, b)
unpack ((a
_,b
_,c
_,b
a,a
t,f
_)) = (a
t,b
a)
lookupDefAccExact :: Name -> Bool -> Context ->
Maybe (Def, Accessibility)
lookupDefAccExact :: Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
mkpublic Context
ctxt
= (TTDecl -> (Def, Accessibility))
-> Maybe TTDecl -> Maybe (Def, Accessibility)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> (Def, Accessibility)
forall {a} {b} {c} {e} {f}.
(a, b, c, Accessibility, e, f) -> (a, Accessibility)
mkp (Maybe TTDecl -> Maybe (Def, Accessibility))
-> Maybe TTDecl -> Maybe (Def, Accessibility)
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where mkp :: (a, b, c, Accessibility, e, f) -> (a, Accessibility)
mkp (a
d, b
_, c
inj, Accessibility
a, e
_, f
_) = if Bool
mkpublic Bool -> Bool -> Bool
&& (Bool -> Bool
not (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_bind" Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_pure"))
then (a
d, Accessibility
Public) else (a
d, Accessibility
a)
lookupTotal :: Name -> Context -> [Totality]
lookupTotal :: Name -> Context -> [Totality]
lookupTotal Name
n Context
ctxt = (TTDecl -> Totality) -> [TTDecl] -> [Totality]
forall a b. (a -> b) -> [a] -> [b]
map TTDecl -> Totality
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> e
mkt ([TTDecl] -> [Totality]) -> [TTDecl] -> [Totality]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where mkt :: (a, b, c, d, e, f) -> e
mkt (a
d, b
_, c
inj, d
a, e
t, f
m) = e
t
lookupTotalExact :: Name -> Context -> Maybe Totality
lookupTotalExact :: Name -> Context -> Maybe Totality
lookupTotalExact Name
n Context
ctxt = (TTDecl -> Totality) -> Maybe TTDecl -> Maybe Totality
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> Totality
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> e
mkt (Maybe TTDecl -> Maybe Totality) -> Maybe TTDecl -> Maybe Totality
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where mkt :: (a, b, c, d, e, f) -> e
mkt (a
d, b
_, c
inj, d
a, e
t, f
m) = e
t
lookupRigCount :: Name -> Context -> [Totality]
lookupRigCount :: Name -> Context -> [Totality]
lookupRigCount Name
n Context
ctxt = (TTDecl -> Totality) -> [TTDecl] -> [Totality]
forall a b. (a -> b) -> [a] -> [b]
map TTDecl -> Totality
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> e
mkt ([TTDecl] -> [Totality]) -> [TTDecl] -> [Totality]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where mkt :: (a, b, c, d, e, f) -> e
mkt (a
d, b
_, c
inj, d
a, e
t, f
m) = e
t
lookupRigCountExact :: Name -> Context -> Maybe RigCount
lookupRigCountExact :: Name -> Context -> Maybe RigCount
lookupRigCountExact Name
n Context
ctxt = (TTDecl -> RigCount) -> Maybe TTDecl -> Maybe RigCount
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> RigCount
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> b
mkt (Maybe TTDecl -> Maybe RigCount) -> Maybe TTDecl -> Maybe RigCount
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where mkt :: (a, b, c, d, e, f) -> b
mkt (a
d, b
rc, c
inj, d
a, e
t, f
m) = b
rc
lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
lookupInjectiveExact :: Name -> Context -> Maybe Bool
lookupInjectiveExact Name
n Context
ctxt = (TTDecl -> Bool) -> Maybe TTDecl -> Maybe Bool
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> Bool
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> c
mkt (Maybe TTDecl -> Maybe Bool) -> Maybe TTDecl -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where mkt :: (a, b, c, d, e, f) -> c
mkt (a
d, b
_, c
inj, d
a, e
t, f
m) = c
inj
linearCheck :: Context -> Type -> TC ()
linearCheck :: Context -> TT Name -> TC ()
linearCheck Context
ctxt TT Name
t = TT Name -> TC ()
checkArgs TT Name
t
where
checkArgs :: TT Name -> TC ()
checkArgs (Bind Name
n (Pi RigCount
RigW Maybe ImplicitInfo
_ TT Name
ty TT Name
_) TT Name
sc)
= do Context -> TT Name -> TC ()
linearCheckArg Context
ctxt TT Name
ty
TT Name -> TC ()
checkArgs (TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
forall n. TT n
Erased) TT Name
sc)
checkArgs (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
sc)
= TT Name -> TC ()
checkArgs (TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
forall n. TT n
Erased) TT Name
sc)
checkArgs TT Name
_ = () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
linearCheckArg :: Context -> Type -> TC ()
linearCheckArg :: Context -> TT Name -> TC ()
linearCheckArg Context
ctxt TT Name
ty = (Name -> TC ()) -> [Name] -> TC ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> TC ()
checkNameOK (TT Name -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames TT Name
ty)
where
checkNameOK :: Name -> TC ()
checkNameOK Name
f
= case Name -> Context -> Maybe RigCount
lookupRigCountExact Name
f Context
ctxt of
Just RigCount
Rig1 ->
Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> Err -> TC ()
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> String -> Err
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" can only appear in a linear binding"
Maybe RigCount
_ -> () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
tcReducible :: Name -> Context -> Bool
tcReducible :: Name -> Context -> Bool
tcReducible Name
n Context
ctxt = case Name -> Context -> Maybe Totality
lookupTotalExact Name
n Context
ctxt of
Maybe Totality
Nothing -> Bool
True
Just (Partial PReason
_) -> Bool
False
Maybe Totality
_ -> Bool
True
lookupMetaInformation :: Name -> Context -> [MetaInformation]
lookupMetaInformation :: Name -> Context -> [MetaInformation]
lookupMetaInformation Name
n Context
ctxt = (TTDecl -> MetaInformation) -> [TTDecl] -> [MetaInformation]
forall a b. (a -> b) -> [a] -> [b]
map TTDecl -> MetaInformation
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> f
mkm ([TTDecl] -> [MetaInformation]) -> [TTDecl] -> [MetaInformation]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
where mkm :: (a, b, c, d, e, f) -> f
mkm (a
d, b
_, c
inj, d
a, e
t, f
m) = f
m
lookupNameTotal :: Name -> Context -> [(Name, Totality)]
lookupNameTotal :: Name -> Context -> [(Name, Totality)]
lookupNameTotal Name
n = ((Name, TTDecl) -> (Name, Totality))
-> [(Name, TTDecl)] -> [(Name, Totality)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, (Def
_, RigCount
_, Bool
_, Accessibility
_, Totality
t, MetaInformation
_)) -> (Name
n, Totality
t)) ([(Name, TTDecl)] -> [(Name, Totality)])
-> (Context -> [(Name, TTDecl)]) -> Context -> [(Name, Totality)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Ctxt TTDecl -> [(Name, TTDecl)])
-> (Context -> Ctxt TTDecl) -> Context -> [(Name, TTDecl)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Ctxt TTDecl
definitions
lookupVal :: Name -> Context -> [Value]
lookupVal :: Name -> Context -> [Value]
lookupVal Name
n Context
ctxt
= do TTDecl
def <- Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
case TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst TTDecl
def of
(Function TT Name
_ TT Name
htm) -> Value -> [Value]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Context -> Env -> TT Name -> Value
veval Context
ctxt [] TT Name
htm)
(TyDecl NameType
nt TT Name
ty) -> Value -> [Value]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> Value -> Value
VP NameType
nt Name
n (Context -> Env -> TT Name -> Value
veval Context
ctxt [] TT Name
ty))
Def
_ -> []
lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, Type)
lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, TT Name)
lookupTyEnv Name
n Env
env = Name -> Int -> Env -> Maybe (Int, RigCount, TT Name)
forall {t} {t} {b} {c}.
(Eq t, Num t) =>
t -> t -> [(t, b, Binder c)] -> Maybe (t, b, c)
li Name
n Int
0 Env
env where
li :: t -> t -> [(t, b, Binder c)] -> Maybe (t, b, c)
li t
n t
i [] = Maybe (t, b, c)
forall a. Maybe a
Nothing
li t
n t
i ((t
x, b
r, Binder c
b): [(t, b, Binder c)]
xs)
| t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
x = (t, b, c) -> Maybe (t, b, c)
forall a. a -> Maybe a
Just (t
i, b
r, Binder c -> c
forall b. Binder b -> b
binderTy Binder c
b)
| Bool
otherwise = t -> t -> [(t, b, Binder c)] -> Maybe (t, b, c)
li t
n (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1) [(t, b, Binder c)]
xs
uniqueNameCtxt :: Context -> Name -> [Name] -> Name
uniqueNameCtxt :: Context -> Name -> [Name] -> Name
uniqueNameCtxt Context
ctxt Name
n [Name]
hs
| Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs = Context -> Name -> [Name] -> Name
uniqueNameCtxt Context
ctxt (Name -> Name
nextName Name
n) [Name]
hs
| [TT Name
_] <- Name -> Context -> [TT Name]
lookupTy Name
n Context
ctxt = Context -> Name -> [Name] -> Name
uniqueNameCtxt Context
ctxt (Name -> Name
nextName Name
n) [Name]
hs
| Bool
otherwise = Name
n
uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt [Name]
ns (Bind Name
n Binder (TT Name)
b TT Name
sc)
= let n' :: Name
n' = Context -> Name -> [Name] -> Name
uniqueNameCtxt Context
ctxt Name
n [Name]
ns in
Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' ((TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt (Name
n'Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns)) Binder (TT Name)
b) (Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt [Name]
ns TT Name
sc)
uniqueBindersCtxt Context
ctxt [Name]
ns (App AppStatus Name
s TT Name
f TT Name
a) = AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt [Name]
ns TT Name
f) (Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt [Name]
ns TT Name
a)
uniqueBindersCtxt Context
ctxt [Name]
ns TT Name
t = TT Name
t