{-|
Module      : Idris.Core.Evaluate
Description : Evaluate Idris expressions.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# 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.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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EvalState] -> ShowS
$cshowList :: [EvalState] -> ShowS
show :: EvalState -> String
$cshow :: EvalState -> String
showsPrec :: Int -> EvalState -> ShowS
$cshowsPrec :: Int -> EvalState -> ShowS
Show

type Eval a = State EvalState a

data EvalOpt = Spec
             | Simplify Bool -- ^ whether to expand lets or not
             | AtREPL
             | RunTT
             | Unfold
  deriving (Int -> EvalOpt -> ShowS
[EvalOpt] -> ShowS
EvalOpt -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EvalOpt] -> ShowS
$cshowList :: [EvalOpt] -> ShowS
show :: EvalOpt -> String
$cshow :: EvalOpt -> String
showsPrec :: Int -> EvalOpt -> ShowS
$cshowsPrec :: Int -> EvalOpt -> ShowS
Show, EvalOpt -> EvalOpt -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EvalOpt -> EvalOpt -> Bool
$c/= :: EvalOpt -> EvalOpt -> Bool
== :: EvalOpt -> EvalOpt -> Bool
$c== :: EvalOpt -> EvalOpt -> Bool
Eq)

initEval :: EvalState
initEval = [(Name, Int)] -> Int -> Bool -> EvalState
ES [] Int
0 Bool
False

-- VALUES (as HOAS) ---------------------------------------------------------
-- | A HOAS representation of values
data Value = VP NameType Name Value
           | VV Int
             -- True for Bool indicates safe to reduce
           | VBind Bool Name (Binder Value) (Value -> Eval Value)
             -- For frozen let bindings when simplifying
           | VBLet RigCount Int Name Value Value Value
           | VApp Value Value
           | VType UExp
           | VUType Universe
           | VErased
           | VImpossible
           | VConstant Const
           | VProj Value Int
--            | VLazy Env [Value] Term
           | 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 = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall s a. State s a -> s -> a
evalState (forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
100 Value
x) EvalState
initEval

instance Show (a -> b) where
    show :: (a -> b) -> String
show a -> b
x = String
"<<fn>>"

-- THE EVALUATOR ------------------------------------------------------------

-- The environment is assumed to be "locally named" - i.e., not de Bruijn
-- indexed.
-- i.e. it's an intermediate environment that we have while type checking or
-- while building a proof.

-- | Normalise fully type checked terms (so, assume all names/let bindings resolved)
normaliseC :: Context -> Env -> TT Name -> TT Name
normaliseC :: Context -> Env -> TT Name -> TT Name
normaliseC Context
ctxt Env
env TT Name
t
   = 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 [] (forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) TT Name
t []
                   forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | Normalise everything, whether abstract, private or public
normaliseAll :: Context -> Env -> TT Name -> TT Name
normaliseAll :: Context -> Env -> TT Name -> TT Name
normaliseAll Context
ctxt Env
env TT Name
t
   = 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 [] (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]
                   forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | As normaliseAll, but with an explicit list of names *not* to reduce
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
   = 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 (forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, Int
0)) [Name]
blocked)
                                          (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]
                   forall a. Quote a => Int -> a -> Eval (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
   = 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 [] (forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (forall n. Eq n => TT n -> TT n
finalise TT Name
t) []
                   forall a. Quote a => Int -> a -> Eval (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
  = forall s a. State s a -> s -> a
evalState (Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [] (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 = forall s a. State s a -> s -> a
evalState (forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- Return a specialised name, and an updated list of reductions available,
-- so that the caller can tell how much specialisation was achieved.
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) =
          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 []
                                 (forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                                 [EvalOpt
Spec]
                       forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
0 Value
val) (EvalState
initEval { limited :: [(Name, Int)]
limited = [(Name, Int)]
limits }) in
         (TT Name
tm, EvalState -> [(Name, Int)]
limited EvalState
st)

-- | Like normalise, but we only reduce functions that are marked as okay to
-- inline, and lets
simplify :: Context -> Env -> TT Name -> TT Name
simplify :: Context -> Env -> TT Name -> TT Name
simplify Context
ctxt Env
env TT Name
t
   = 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)]
                                 (forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                                 [Bool -> EvalOpt
Simplify Bool
True]
                   forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | Like simplify, but we only reduce functions that are marked as okay to
-- inline, and don't reduce lets
inlineSmall :: Context -> Env -> TT Name -> TT Name
inlineSmall :: Context -> Env -> TT Name -> TT Name
inlineSmall Context
ctxt Env
env TT Name
t
   = 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 []
                                 (forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                                 [Bool -> EvalOpt
Simplify Bool
False]
                   forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | Simplify for run-time (i.e. basic inlining)
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
   = 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)]
                                 (forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                                 [EvalOpt
RunTT]
                   forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | Unfold the given names in a term, the given number of times in a stack.
-- Preserves 'let'.
-- This is primarily to support inlining of the given names, and can also
-- help with partial evaluation by allowing a rescursive definition to be
-- unfolded once only.
-- Specifically used to unfold definitions using interfaces before going to
-- the totality checker (otherwise mutually recursive definitions in
-- implementations will not work...)
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
   = 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
                               (forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                               [EvalOpt
Unfold]
                   forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
0 Value
val) EvalState
initEval


-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))

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, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall n. Eq n => TT n -> TT n
finalise Binder (TT Name)
b)

usable :: Bool -- specialising
          -> Bool -- unfolding only
          -> Int -- Reduction depth limit (when simplifying/at REPL)
          -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
usable :: Bool
-> Bool
-> Int
-> Name
-> [(Name, Int)]
-> Eval (Bool, [(Name, Int)])
usable Bool
False Bool
uf Int
depthlimit Name
n [] = 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 <- forall s (m :: * -> *). MonadState s m => m s
get
       if Bool
b then forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
            else case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
ls of
                    Just Int
0 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
                    Just Int
i -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [(Name, Int)]
ns)
                    Maybe Int
_ -> 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 forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
ns of
         Just Int
0 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
         Just Int
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Bool
True, (Name
n, forall a. Num a => a -> a
abs (Int
iforall a. Num a => a -> a -> a
-Int
1)) forall a. a -> [a] -> [a]
: forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', Int
_) -> Name
nforall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ns)
         Maybe Int
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
uf
                          then (Bool
False, [(Name, Int)]
ns)
                          else (Bool
True, (Name
n, Int
depthlimit) forall a. a -> [a] -> [a]
: forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', Int
_) -> Name
nforall 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 <- forall s (m :: * -> *). MonadState s m => m s
get
              case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
ls of
                  Just Int
i -> do forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ [(Name, Int)] -> Int -> Bool -> EvalState
ES ((Name
n, (Int
i forall a. Num a => a -> a -> a
- Int
inc)) forall a. a -> [a] -> [a]
:
                                           forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', Int
_) -> Name
nforall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ls) Int
num Bool
b
                  Maybe Int
_ -> 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
_ <- forall s (m :: * -> *). MonadState s m => m s
get
                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)

-- | Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
-- such as we might have during construction of a proof)

-- The (Name, Int) pair in the arguments is the maximum depth of unfolding of
-- a name. The corresponding pair in the state is the maximum number of
-- unfoldings overall.

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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
    simpl :: Bool
simpl = Bool -> EvalOpt
Simplify Bool
True forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts Bool -> Bool -> Bool
|| Bool -> EvalOpt
Simplify Bool
False forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
    simpl_inline :: Bool
simpl_inline = Bool -> EvalOpt
Simplify Bool
False forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
    runtime :: Bool
runtime = EvalOpt
RunTT forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
    atRepl :: Bool
atRepl = EvalOpt
AtREPL forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
    unfold :: Bool
unfold = EvalOpt
Unfold forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts

    noFree :: [(a, Value)] -> Bool
noFree = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Value -> Bool
canonical forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd

    -- returns 'True' if the function should block
    -- normal evaluation should return false
    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
|| 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
|| forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
n t Name
stk)
             Bool -> Bool -> Bool
|| (Name
n 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) <- 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
&& 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" 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
&& 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
nforall 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
                                                 forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a. Eq a => a -> a -> Bool
== Accessibility
Public Bool -> Bool -> Bool
|| Accessibility
acc forall a. Eq a => a -> a -> Bool
== Accessibility
Hidden) Bool -> Bool -> Bool
&&
--                                || sUN "assert_total" `elem` stk) &&
                             forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a b. (a, b) -> a
fst (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd)) -> -- unoptimised version
                       let ([Name]
ns, SC
tree) = CaseDefs -> ([Name], SC)
getCases CaseDefs
cd in
                         if forall {t :: * -> *}.
Foldable t =>
CaseInfo -> Name -> t Name -> Bool
blockSimplify CaseInfo
ci Name
n [Name]
stk
                            then 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 -- traceWhen runtime (show (n, ns, tree)) $
                                 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
nforall 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]
_) -> 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]
_)  -> forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
                    Maybe (Def, Accessibility)
_ -> 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 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)
        = 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 forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Value)]
env Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
>= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd ([(Name, Value)]
env forall a. [a] -> Int -> a
!! Int
i)
        | Bool
otherwise      = forall (m :: * -> *) a. Monad m => a -> m a
return 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
|| forall n. Eq n => n -> TT n -> Int
occurrences Name
n TT Name
sc 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 --(finalise 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') 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 --(finalise v)
                -- use Tmp as a placeholder, then make it a variable reference
                -- again when evaluation finished
                EvalState
hs <- forall s (m :: * -> *). MonadState s m => m s
get
                let vd :: Int
vd = EvalState -> Int
nexthole EvalState
hs
                forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalState
hs { nexthole :: Int
nexthole = Int
vd forall a. Num a => a -> a -> a
+ Int
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) forall a. a -> [a] -> [a]
: [(Name, Value)]
env) TT Name
sc
                forall (m :: * -> *) a. Monad m => a -> m a
return 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 (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 (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') forall a. a -> [a] -> [a]
: [(Name, Value)]
env) TT Name
sc
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Binder Value -> (Value -> Eval Value) -> Value
VBind Bool
True Name
n (forall b. RigCount -> b -> b -> Binder b
Let RigCount
RigW Value
t' Value
v') (\Value
x -> 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 (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
genv forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Value)]
env)
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Binder Value -> (Value -> Eval Value) -> Value
VBind Bool
True -- (vinstances 0 sc < 2)
                               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)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
                     = 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 (forall n. Eq n => TT n -> TT n
finalise TT Name
tm)) Binder (TT Name)
t
    -- block reduction immediately under codata (and not forced)
    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 forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" Bool -> Bool -> Bool
&& Text
lco 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]
_) = 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) forall a. a -> [a] -> [a]
: [(Name, Int)]
ntimes
                                    TT Name
_ -> [(Name, Int)]
ntimes
                 forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec 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
                 forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec 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'
    -- Treat "assert_total" specially, as long as it's defined!
    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
&& forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env)Bool -> Bool -> Bool
|| Bool
runtime) Context
ctxt,
         Text
at 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 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 -- evaluate dictionaries if it means the projection works
                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
--                 tfull' <- reapply ntimes stk top env t' []
                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 forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args = [Value]
argsforall a. [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) = forall (m :: * -> *) a. Monad m => a -> m a
return 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    = 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  = 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)   = forall (m :: * -> *) a. Monad m => a -> m a
return 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)   = forall (m :: * -> *) a. Monad m => a -> m a
return 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
aforall 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
&& 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" 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
&& 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 forall a. Eq a => a -> a -> Bool
== Accessibility
Public Bool -> Bool -> Bool
|| Accessibility
acc forall a. Eq a => a -> a -> Bool
== Accessibility
Hidden ->
                           -- unoptimised version
                       let ([Name]
ns, SC
tree) = CaseDefs -> ([Name], SC)
getCases CaseDefs
cd in
                         if forall {t :: * -> *}.
Foldable t =>
CaseInfo -> Name -> t Name -> Bool
blockSimplify CaseInfo
ci Name
n [Name]
stk
                           then forall (m :: * -> *) a. Monad m => a -> m a
return 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 -- traceWhen runtime (show (n, ns, tree)) $
                                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
nforall 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]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args)
                           then case [Value] -> Maybe Value
op (forall a. Int -> [a] -> [a]
take Int
i [Value]
args) of
                              Maybe Value
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 (forall a. Int -> [a] -> [a]
drop Int
i [Value]
args) Value
v
                           else forall (m :: * -> *) a. Monad m => a -> m a
return 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
                              [] -> forall (m :: * -> *) a. Monad m => a -> m a
return Value
f
                              [Value]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return 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) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env Value
f (Value
aforall a. a -> [a] -> [a]
:[Value]
as)
                           [] -> 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) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env Value
f (Value
aforall a. a -> [a] -> [a]
:[Value]
as)
    apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env Value
f []     = forall (m :: * -> *) a. Monad m => a -> m a
return Value
f

--     specApply stk env f@(VP Ref n ty) args
--         = case lookupCtxt n statics of
--                 [as] -> if or as
--                           then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
--                                 return $ unload env f args
--                           else return $ unload env f args
--                 _ -> return $ unload env f args
--     specApply stk env f args = return $ unload env f args

    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
        | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args
             = do let args' :: [Value]
args' = forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns) [Value]
args
                  let rest :: [Value]
rest  = forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns) [Value]
args
                  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec 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 (forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args') SC
tree
                  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec forall a b. (a -> b) -> a -> b
$ case Maybe Value
t of
                                   Maybe Value
Nothing -> Name -> Eval ()
reinstate Name
n -- Blocked, count n again
                                   Just Value
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
--                                 (zipWith (\n , t) -> (n, t)) ns args') tree
                  forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Value
t, [Value]
rest)
        | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return (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) = forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall n. Eq n => [n] -> TT n -> TT n
pToVs (forall a b. (a -> b) -> [a] -> [b]
map 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 (forall {n}. TT n -> Bool
conHeaded TT Name
tm))
                                   ([(Name, Value)]
amap forall a. [a] -> [a] -> [a]
++ [(Name, Value)]
env) TT Name
etm
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap SC
ImpossibleCase = forall (m :: * -> *) a. Monad m => a -> m a
return 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' <- 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)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return 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) <- 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) <- forall {t}. Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [CaseAlt' (TT Name)]
alts = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap (forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args) [(Name, Value)]
amap, SC
sc)
        | Just SC
v <- forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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) <- forall {t}. Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [CaseAlt' (TT Name)]
alts
                            = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap (forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args) [(Name, Value)]
amap, SC
sc)
        | Just SC
v <- forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall {t}. Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [CaseAlt' (TT Name)]
alts      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
        | Just (Name
n', Value
sub, SC
sc) <- forall {t}. Const -> [CaseAlt' t] -> Maybe (Name, Value, SC' t)
findSuc Const
c [CaseAlt' (TT Name)]
alts
                            = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap [(Name
n',Value
sub)] [(Name, Value)]
amap, SC
sc)
        | Just SC
v <- forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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) <- forall {t}. Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn Name
n [CaseAlt' (TT Name)]
alts  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap (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) <- 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) -- we know it's not in scope or it's not a pattern
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap (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 <- forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts
             = if (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall {t}. CaseAlt' t -> Bool
fnCase [CaseAlt' (TT Name)]
alts)
                  then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
                  else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

    fnCase :: CaseAlt' t -> Bool
fnCase (FnCase Name
_ [Name]
_ SC' t
_) = Bool
True
    fnCase CaseAlt' t
_ = Bool
False

    -- Replace old variable names in the map with new matches
    -- (This is possibly unnecessary since we make unique names and don't
    -- allow repeated variables...?)
    updateAmap :: [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap [(a, b)]
newm [(a, b)]
amap
       = [(a, b)]
newm forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter (\ (a
x, b
_) -> Bool -> Bool
not (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
x (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(a, b)]
newm))) [(a, b)]
amap
    findTag :: Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [] = forall a. Maybe a
Nothing
    findTag Int
i (ConCase Name
n Int
j [Name]
ns SC' t
sc : [CaseAlt' t]
xs) | Int
i forall a. Eq a => a -> a -> Bool
== Int
j = 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 [] = forall a. Maybe a
Nothing
    findFn Name
fn (FnCase Name
n [Name]
ns SC' t
sc : [CaseAlt' t]
xs) | Name
fn forall a. Eq a => a -> a -> Bool
== Name
n = 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 [] = forall a. Maybe a
Nothing
    findDefault (DefaultCase SC' t
sc : [CaseAlt' t]
xs) = 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 [] = forall a. Maybe a
Nothing
    findSuc (BI Integer
val) (SucCase Name
n SC' t
sc : [CaseAlt' t]
_)
         | Integer
val forall a. Eq a => a -> a -> Bool
/= Integer
0 = forall a. a -> Maybe a
Just (Name
n, Const -> Value
VConstant (Integer -> Const
BI (Integer
val 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 [] = forall a. Maybe a
Nothing
    findConst Const
c (ConstCase Const
c' SC' t
v : [CaseAlt' t]
xs) | Const
c forall a. Eq a => a -> a -> Bool
== Const
c' = 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) = forall a. a -> Maybe a
Just SC' t
v
    findConst (AType ArithTy
ATFloat) (ConCase Name
n Int
2 [] SC' t
v : [CaseAlt' t]
xs) = 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) = forall a. a -> Maybe a
Just SC' t
v
    findConst Const
StrType (ConCase Name
n Int
4 [] SC' t
v : [CaseAlt' t]
xs) = 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) = 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 forall a. Eq a => a -> a -> Bool
== Int
7 forall a. Num a => a -> a -> a
+ forall a. Enum a => a -> Int
fromEnum NativeTy
ity = 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
aforall a. a -> [a] -> [a]
:[Value]
as)
    getValArgs' Value
f [Value]
as = (Value
f, [Value]
as)

-- tmpToV i vd (VLetHole j) | vd == j = return $ VV i
-- tmpToV i vd (VP nt n v) = liftM (VP nt n) (tmpToV i vd v)
-- tmpToV i vd (VBind n b sc) = do b' <- fmapMB (tmpToV i vd) b
--                                 let sc' = \x -> do x' <- sc x
--                                                    tmpToV (i + 1) vd x'
--                                 return (VBind n b' sc')
-- tmpToV i vd (VApp f a) = liftM2 VApp (tmpToV i vd f) (tmpToV i vd a)
-- tmpToV i vd x = return x

instance Eq Value where
    == :: Value -> Value -> Bool
(==) Value
x Value
y = forall {a}. Quote a => a -> TT Name
getTT Value
x forall a. Eq a => a -> a -> Bool
== forall {a}. Quote a => a -> TT Name
getTT Value
y
      where getTT :: a -> TT Name
getTT a
v = forall s a. State s a -> s -> a
evalState (forall a. Quote a => Int -> a -> Eval (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 -> Eval (TT Name)
quote Int
i (VP NameType
nt Name
n Value
v)      = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n) (forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
i Value
v)
    quote Int
i (VV Int
x)           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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' <- forall {a}.
Quote a =>
Binder a -> StateT EvalState Identity (Binder (TT Name))
quoteB Binder Value
b
                                  forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder (TT Name)
b') (forall a. Quote a => Int -> a -> Eval (TT Name)
quote (Int
iforall a. Num a => a -> a -> a
+Int
1) Value
sc')
       where quoteB :: Binder a -> StateT EvalState Identity (Binder (TT Name))
quoteB Binder a
t = forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder a -> m (Binder b)
fmapMB (forall a. Quote a => Int -> a -> Eval (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' <- forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
i Value
sc
                                TT Name
t' <- forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
i Value
t
                                TT Name
v' <- forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
i Value
v
                                let sc'' :: TT Name
sc'' = forall n. Eq n => n -> TT n -> TT n
pToV (Int -> String -> Name
sMN Int
vd String
"vlet") (forall n. TT n -> TT n
addBinder TT Name
sc')
                                forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (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)     = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (forall n. AppStatus n -> TT n -> TT n -> TT n
App forall n. AppStatus n
MaybeHoles) (forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
i Value
f) (forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
i Value
a)
    quote Int
i (VType UExp
u)      = forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. UExp -> TT n
TType UExp
u)
    quote Int
i (VUType Universe
u)     = forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. Universe -> TT n
UType Universe
u)
    quote Int
i Value
VErased        = forall (m :: * -> *) a. Monad m => a -> m a
return forall n. TT n
Erased
    quote Int
i Value
VImpossible    = forall (m :: * -> *) a. Monad m => a -> m a
return forall n. TT n
Impossible
    quote Int
i (VProj Value
v Int
j)    = do TT Name
v' <- forall a. Quote a => Int -> a -> Eval (TT Name)
quote Int
i Value
v
                                forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. TT n -> Int -> TT n
Proj TT Name
v' Int
j)
    quote Int
i (VConstant Const
c)  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. Const -> TT n
Constant Const
c
    quote Int
i (VTmp Int
x)       = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. Int -> TT n
V (Int
i forall a. Num a => a -> a -> a
- Int
x 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 forall a. Ord a => a -> a -> Bool
>= Int
i = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Value
VV (Int
x 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' <- 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
                               forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a. Num a => a -> a -> a
+ Int
1) Value
x')
wknV Int
i (VApp Value
f Value
a)     = 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              = 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 = 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes Bool -> Bool -> Bool
|| Name
y forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        | Name
x forall a. Eq a => a -> a -> Bool
== Name
y Bool -> Bool -> Bool
|| (Name
x, Name
y) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, Name)]
ps Bool -> Bool -> Bool
|| (Name
y,Name
x) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, Name)]
ps = 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)      = forall (m :: * -> *) a. Monad m => a -> m a
return (Int
x forall a. Eq a => a -> a -> Bool
== Int
y)
    ceq [(Name, Name)]
ps (V Int
x)      (P NameType
_ Name
y TT Name
_)
        | Int
x forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
ps forall a. Ord a => a -> a -> Bool
> Int
x = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a, b) -> a
fst ([(Name, Name)]
psforall a. [a] -> Int -> a
!!Int
x) forall a. Eq a => a -> a -> Bool
== Name
y)
        | Bool
otherwise = 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 forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
ps forall a. Ord a => a -> a -> Bool
> Int
y = forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x forall a. Eq a => a -> a -> Bool
== forall a b. (a, b) -> b
snd ([(Name, Name)]
psforall a. [a] -> Int -> a
!!Int
y))
        | Bool
otherwise = 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)
                             = 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')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') = 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') = 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') = 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 (forall b. Binder b -> b
binderTy Binder (TT Name)
b) (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 (forall n. TT n -> TT n -> TT n
substV (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 (forall n. TT n -> TT n -> TT n
substV (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 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 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

    -- Special case for 'case' blocks - size of scope causes complications,
    -- we only want to check the blocks themselves are valid and identical
    -- in the current scope. So, just check the bodies, and the additional
    -- arguments the case blocks are applied to.
    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) <- forall n. TT n -> (TT n, [TT n])
unApply TT Name
x,
          (P NameType
_ Name
cy TT Name
_, [TT Name]
yargs) <- 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) = 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) = forall (m :: * -> *) a. Monad m => a -> m a
return (Const
x forall a. Eq a => a -> a -> Bool
== Const
y)
    ceq [(Name, Name)]
ps (TType UExp
x) (TType UExp
y) | UExp
x forall a. Eq a => a -> a -> Bool
== UExp
y = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq [(Name, Name)]
ps (TType (UVal Int
0)) (TType UExp
y) = 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) <- forall s (m :: * -> *). MonadState s m => m s
get
                                    forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
v, UExp -> UExp -> UConstraint
ULE UExp
x UExp
y forall a. a -> [a] -> [a]
: [UConstraint]
cs)
                                    forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq [(Name, Name)]
ps (UType Universe
AllTypes) TT Name
x = 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) = 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) = forall (m :: * -> *) a. Monad m => a -> m a
return (Universe
u forall a. Eq a => a -> a -> Bool
== Universe
v)
    ceq [(Name, Name)]
ps TT Name
Erased TT Name
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq [(Name, Name)]
ps TT Name
_ TT Name
Erased = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq [(Name, Name)]
ps TT Name
x TT Name
y = 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')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 (forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
as [Name]
as' 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'
                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name
x forall a. Eq a => a -> a -> Bool
== Name
x' Bool -> Bool -> Bool
&& Int
i 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'
                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Const
x 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')
            = 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 [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        caseeqA [(Name, Name)]
ps [CaseAlt' (TT Name)]
_ [CaseAlt' (TT Name)]
_ = 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
_) = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    caseeq [(Name, Name)]
ps SC
_ SC
_ = 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)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)forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) SC
xdef SC
ydef
                        ([Def], [Def])
_ -> 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)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 forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&)
                                  (do [Bool]
ok <- 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)
                                              (forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
xin) [TT Name]
xargs)
                                              (forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
yin) [TT Name]
yargs)
                                      forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
ok))
                                  ([(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq ((Name
x,Name
y)forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) SC
xdef SC
ydef)
                 ([Def], [Def])
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- CONTEXTS -----------------------------------------------------------------

{-| A definition is either a simple function (just an expression with a type),
   a constant, which could be a data or type constructor, an axiom or as an
   yet undefined function, or an Operator.
   An Operator is a function which explains how to reduce.
   A CaseOp is a function defined by a simple case tree -}

data Def = Function !Type !Term
         | TyDecl NameType !Type
         | Operator Type Int ([Value] -> Maybe Value)
         | CaseOp CaseInfo
                  !Type
                  ![(Type, Bool)] -- argument types, whether canonical
                  ![Either Term (Term, Term)] -- original definition
                  ![([Name], Term, Term)] -- simplified for totality check definition
                  !CaseDefs
  deriving 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
$cto :: forall x. Rep Def x -> Def
$cfrom :: forall x. Def -> Rep Def x
Generic
--                   [Name] SC -- Compile time case definition
--                   [Name] SC -- Run time cae definitions

data CaseDefs = CaseDefs {
                  CaseDefs -> ([Name], SC)
cases_compiletime :: !([Name], SC),
                  CaseDefs -> ([Name], SC)
cases_runtime :: !([Name], SC)
                }
  deriving 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
$cto :: forall x. Rep CaseDefs x -> CaseDefs
$cfrom :: forall x. CaseDefs -> Rep CaseDefs x
Generic

data CaseInfo = CaseInfo {
                  CaseInfo -> Bool
case_inlinable :: Bool, -- decided by machine
                  CaseInfo -> Bool
case_alwaysinline :: Bool, -- decided by %inline flag
                  CaseInfo -> Bool
tc_dictionary :: Bool
                }
  deriving 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
$cto :: forall x. Rep CaseInfo x -> CaseInfo
$cfrom :: forall x. CaseInfo -> Rep CaseInfo x
Generic

{-!
deriving instance Binary Def
!-}
{-!
deriving instance Binary CaseInfo
!-}
{-!
deriving instance Binary CaseDefs
!-}

instance Show Def where
    show :: Def -> String
show (Function TT Name
ty TT Name
tm) = String
"Function: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (TT Name
ty, TT Name
tm)
    show (TyDecl NameType
nt TT Name
ty) = String
"TyDecl: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NameType
nt forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TT Name
ty
    show (Operator TT Name
ty Int
_ [Value] -> Maybe Value
_) = String
"Operator: " forall a. [a] -> [a] -> [a]
++ 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: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TT Name
ty forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [([Name], TT Name, TT Name)]
ps forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++
                                        String
"COMPILE TIME:\n\n" forall a. [a] -> [a] -> [a]
++
                                        forall a. Show a => a -> String
show [Name]
ns forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SC
sc forall a. [a] -> [a] -> [a]
++ String
"\n\n" forall a. [a] -> [a] -> [a]
++
                                        String
"RUN TIME:\n\n" forall a. [a] -> [a] -> [a]
++
                                        forall a. Show a => a -> String
show [Name]
ns' forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SC
sc' forall a. [a] -> [a] -> [a]
++ String
"\n\n" forall a. [a] -> [a] -> [a]
++
            if Bool
inlc then String
"Inlinable" else String
"Not inlinable" forall a. [a] -> [a] -> [a]
++
            if Bool
inla then String
" Aggressively\n" else String
"\n"

-------

-- Hidden => Programs can't access the name at all
-- Public => Programs can access the name and use at will
-- Frozen => Programs can access the name, which doesn't reduce
-- Private => Programs can't access the name, doesn't reduce internally

data Accessibility = Hidden | Public | Frozen | Private
    deriving (Accessibility -> Accessibility -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Accessibility -> Accessibility -> Bool
$c/= :: Accessibility -> Accessibility -> Bool
== :: Accessibility -> Accessibility -> Bool
$c== :: Accessibility -> Accessibility -> Bool
Eq, Eq 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
min :: Accessibility -> Accessibility -> Accessibility
$cmin :: Accessibility -> Accessibility -> Accessibility
max :: Accessibility -> Accessibility -> Accessibility
$cmax :: Accessibility -> Accessibility -> Accessibility
>= :: Accessibility -> Accessibility -> Bool
$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
compare :: Accessibility -> Accessibility -> Ordering
$ccompare :: Accessibility -> Accessibility -> Ordering
Ord, 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
$cto :: forall x. Rep Accessibility x -> Accessibility
$cfrom :: forall x. Accessibility -> Rep Accessibility x
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

-- | The result of totality checking
data Totality = Total [Int] -- ^ well-founded arguments
              | Productive -- ^ productive
              | Partial PReason
              | Unchecked
              | Generated
    deriving (Totality -> Totality -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Totality -> Totality -> Bool
$c/= :: Totality -> Totality -> Bool
== :: Totality -> Totality -> Bool
$c== :: Totality -> Totality -> Bool
Eq, 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
$cto :: forall x. Rep Totality x -> Totality
$cfrom :: forall x. Totality -> Rep Totality x
Generic)

-- | Reasons why a function may not be total
data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
             | ExternalIO | BelieveMe | Mutual [Name] | NotProductive
    deriving (Int -> PReason -> ShowS
[PReason] -> ShowS
PReason -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PReason] -> ShowS
$cshowList :: [PReason] -> ShowS
show :: PReason -> String
$cshow :: PReason -> String
showsPrec :: Int -> PReason -> ShowS
$cshowsPrec :: Int -> PReason -> ShowS
Show, PReason -> PReason -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PReason -> PReason -> Bool
$c/= :: PReason -> PReason -> Bool
== :: PReason -> PReason -> Bool
$c== :: PReason -> PReason -> Bool
Eq, 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
$cto :: forall x. Rep PReason x -> PReason
$cfrom :: forall x. PReason -> Rep PReason x
Generic)

instance Show Totality where
    show :: Totality -> String
show (Total [Int]
args)= String
"Total" -- ++ show args ++ " decreasing arguments"
    show Totality
Productive = String
"Productive" -- ++ show args ++ " decreasing arguments"
    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: " forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Name]
ns)
    show (Partial (Mutual [Name]
ns)) = String
"possibly not total due to recursive path " forall a. [a] -> [a] -> [a]
++
                                 String -> [String] -> String
showSep String
" --> " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Name]
ns)
    show (Partial (UseUndef Name
n)) = String
"possibly not total because it uses the undefined name " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
    show Totality
Generated = String
"auto-generated"

{-!
deriving instance Binary Accessibility
!-}

{-!
deriving instance Binary Totality
!-}

{-!
deriving instance Binary PReason
!-}

-- Possible attached meta-information for a definition in context
data MetaInformation =
      EmptyMI -- ^ No meta-information
    | DataMI [Int] -- ^ Meta information for a data declaration with position of parameters
  deriving (MetaInformation -> MetaInformation -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MetaInformation -> MetaInformation -> Bool
$c/= :: MetaInformation -> MetaInformation -> Bool
== :: MetaInformation -> MetaInformation -> Bool
$c== :: MetaInformation -> MetaInformation -> Bool
Eq, Int -> MetaInformation -> ShowS
[MetaInformation] -> ShowS
MetaInformation -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MetaInformation] -> ShowS
$cshowList :: [MetaInformation] -> ShowS
show :: MetaInformation -> String
$cshow :: MetaInformation -> String
showsPrec :: Int -> MetaInformation -> ShowS
$cshowsPrec :: Int -> MetaInformation -> ShowS
Show, 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
$cto :: forall x. Rep MetaInformation x -> MetaInformation
$cfrom :: forall x. MetaInformation -> Rep MetaInformation x
Generic)

-- | Contexts used for global definitions and for proof state. They contain
-- universe constraints and existing definitions.
-- Also store maximum RigCount of the name (can't bind a name at multiplicity
-- 1 in a RigW, for example)
data Context = MkContext {
                  Context -> Int
next_tvar       :: Int,
                  Context -> Ctxt TTDecl
definitions     :: Ctxt TTDecl
                } deriving (Int -> Context -> ShowS
[Context] -> ShowS
Context -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Context] -> ShowS
$cshowList :: [Context] -> ShowS
show :: Context -> String
$cshow :: Context -> String
showsPrec :: Int -> Context -> ShowS
$cshowsPrec :: Int -> Context -> ShowS
Show, 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
$cto :: forall x. Rep Context x -> Context
$cfrom :: forall x. Context -> Rep Context x
Generic)

type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)

-- | The initial empty context
initContext :: Context
initContext = Int -> Ctxt TTDecl -> Context
MkContext Int
0 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 (forall a b. (a -> b) -> Ctxt a -> Ctxt b
mapCtxt 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)

-- | Get the definitions from a context
ctxtAlist :: Context -> [(Name, Def)]
ctxtAlist :: Context -> [(Name, Def)]
ctxtAlist Context
ctxt = 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)) forall a b. (a -> b) -> a -> b
$ 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 = 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' = 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 TTDecl
definitions = Ctxt TTDecl
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' = 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 TTDecl
definitions = Ctxt TTDecl
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' = 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 TTDecl
definitions = Ctxt TTDecl
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' = 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 TTDecl
definitions = Ctxt TTDecl
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' = 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 TTDecl
definitions = Ctxt TTDecl
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' = 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 TTDecl
definitions = Ctxt TTDecl
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' = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (Def
d, RigCount
RigW, Bool
False, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) forall a b. (a -> b) -> a -> b
$! Ctxt TTDecl
ctxt in
                       Context
c { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
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' = 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 TTDecl
definitions = Ctxt TTDecl
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 (forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n
                     (NameType -> TT Name -> Def
TyDecl (Int -> Int -> NameType
TCon Int
tag (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 TTDecl
definitions = Ctxt TTDecl
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
tagforall a. Num a => a -> a -> a
+Int
1) [(Name, TT Name)]
cons (forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n
                  (NameType -> TT Name -> Def
TyDecl (Int -> Int -> Bool -> NameType
DCon Int
tag (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)

-- FIXME: Too many arguments! Refactor all these Bools.
--
-- Issue #1724 on the issue tracker.
-- https://github.com/idris-lang/Idris-dev/issues/1724
addCasedef :: Name -> ErasureInfo -> CaseInfo ->
              Bool -> SC -> -- default case
              Bool -> Bool ->
              [(Type, Bool)] -> -- argument types, whether canonical
              [Int] ->  -- inaccessible arguments
              [Either Term (Term, Term)] ->
              [([Name], Term, Term)] -> -- compile time
              [([Name], Term, Term)] -> -- run time
              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 -- tcdict
                           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 :: Bool
case_inlinable = Bool
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 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n TTDecl
op Ctxt TTDecl
ctxt
--                    other -> tfail (Msg $ "Error adding case def: " ++ show other)
         forall (m :: * -> *) a. Monad m => a -> m a
return Context
uctxt { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
ctxt' }

-- simplify a definition by unfolding interface methods
-- We need this for totality checking, because functions which use interfaces
-- in an implementation definition themselves need to have the implementation
-- inlined or it'll be treated as a higher order function that will potentially
-- loop.
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 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)] ->
                      forall (m :: * -> *) a. Monad m => a -> m a
return Ctxt TTDecl
ctxt -- nothing to simplify (or already done...)
                   [(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' = forall a b. (a -> b) -> [a] -> [b]
map 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 = forall a b. (a -> b) -> [a] -> [b]
map 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 (forall t. t -> SC' t
STerm forall n. TT n
Erased) Bool
False Phase
CompileTime FC
emptyFC [] [(TT Name, Bool)]
atys [([Name], TT Name, TT Name)]
pdef ErasureInfo
ei
                         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 :: ([Name], SC)
cases_compiletime = ([Name]
args, SC
sc) }),
                                              RigCount
rc, Bool
inj, Accessibility
acc, Totality
tot, MetaInformation
metainf) Ctxt TTDecl
ctxt

                   [TTDecl]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Ctxt TTDecl
ctxt
        forall (m :: * -> *) a. Monad m => a -> m a
return Context
uctxt { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
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 forall a. a -> [a] -> [a]
: [n]
acc) (forall n. TT n -> TT n -> TT n
instantiate (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') = forall {n}. [n] -> TT n -> ([n], TT n)
depat [] TT n
x
                                ([n]
_, TT n
y') = 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') = forall {n}. [n] -> TT n -> ([n], TT n)
depat [] TT n
x in
                                ([n]
vs, TT n
x', forall n. TT n
Impossible)
    simpl :: Either a (a, TT Name) -> Either a (a, TT Name)
simpl (Right (a
x, TT Name
y))
         = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
ufnames then forall a b. b -> Either a b
Right (a
x, TT Name
y)
              else forall a b. b -> Either a b
Right (a
x, Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
unfold Context
uctxt [] (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

    -- Unfold the given name, interface methdods, and any function which uses it as
    -- an argument directly. This is specifically for finding applications of
    -- interface dictionaries and inlining them both for totality checking and for
    -- a small performance gain.
    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 = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ [Name]
inames forall a. [a] -> [a] -> [a]
++ Maybe Name -> TT Name -> [Name]
getNames forall a. Maybe a
Nothing TT Name
tm forall a. [a] -> [a] -> [a]
++ 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) <- 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
_ -> forall a. a -> Maybe a
Just Name
fn
                                     TT Name
_ -> forall a. Maybe a
Nothing
                                  in
                       Maybe Name -> TT Name -> [Name]
getNames Maybe Name
under TT Name
f forall a. [a] -> [a] -> [a]
++ 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 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 forall a. Maybe a
Nothing TT Name
t forall a. [a] -> [a] -> [a]
++
              Maybe Name -> TT Name -> [Name]
getNames forall a. Maybe a
Nothing TT Name
v forall a. [a] -> [a] -> [a]
++
              Maybe Name -> TT Name -> [Name]
getNames 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 forall a. Maybe a
Nothing (forall b. Binder b -> b
binderTy Binder (TT Name)
b) forall a. [a] -> [a] -> [a]
++
                                       Maybe Name -> TT Name -> [Name]
getNames 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' = 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 TTDecl
definitions = Ctxt TTDecl
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 = forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt) in
                      forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, TTDecl)]
ns

-- | Get the list of pairs of fully-qualified names and their types that match some name
lookupTyName :: Name -> Context -> [(Name, Type)]
lookupTyName :: Name -> Context -> [(Name, TT Name)]
lookupTyName Name
n Context
ctxt = do
  (Name
name, TTDecl
def) <- forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  TT Name
ty <- case forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst TTDecl
def of
                       (Function TT Name
ty TT Name
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
                       (TyDecl NameType
_ TT Name
ty) -> forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
                       (Operator TT Name
ty Int
_ [Value] -> Maybe Value
_) -> 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
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return (Name
name, TT Name
ty)

-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.
lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)
lookupTyNameExact :: Name -> Context -> Maybe (Name, TT Name)
lookupTyNameExact Name
n Context
ctxt = 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 forall a. Eq a => a -> a -> Bool
== Name
n ]

-- | Get the types that match some name
lookupTy :: Name -> Context -> [Type]
lookupTy :: Name -> Context -> [TT Name]
lookupTy Name
n Context
ctxt = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (Name -> Context -> [(Name, TT Name)]
lookupTyName Name
n Context
ctxt)

-- | Get the single type that matches some name precisely
lookupTyExact :: Name -> Context -> Maybe Type
lookupTyExact :: Name -> Context -> Maybe (TT Name)
lookupTyExact Name
n Context
ctxt = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd (Name -> Context -> Maybe (Name, TT Name)
lookupTyNameExact Name
n Context
ctxt)

-- | Return true if the given type is a concrete type familyor primitive
-- False it it's a function to compute a type or a variable
isCanonical :: Type -> Context -> Bool
isCanonical :: TT Name -> Context -> Bool
isCanonical TT Name
t Context
ctxt
     = case 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

-- | Check whether a resolved name is certainly a data constructor
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

-- | Check whether any overloading of a name is a data constructor
canBeDConName :: Name -> Context -> Bool
canBeDConName :: Name -> Context -> Bool
canBeDConName Name
n Context
ctxt
     = forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall a b. (a -> b) -> a -> b
$ do TTDecl
def <- forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
               case 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
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                 Def
_ -> 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

-- Is the name guarded by constructors in the term?
-- We assume the term is normalised, so no looking under 'let' for example.
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 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) <- forall n. TT n -> (TT n, [TT n])
unApply TT Name
ap,
          Name -> Context -> Bool
isConName Name
f Context
ctxt = 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 =
  forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\Map Name TTDecl
m -> forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name TTDecl
m forall a. Ord a => a -> a -> Bool
> Int
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall {k} {a} {b} {c} {e} {f}.
Map k (a, b, c, Accessibility, e, f)
-> Map k (a, b, c, Accessibility, e, f)
onlyVisible forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Ctxt TTDecl
definitions 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 = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter 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 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
_)      -> forall (m :: * -> *) a. Monad m => a -> m a
return (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
_)        -> forall (m :: * -> *) a. Monad m => a -> m a
return (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
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (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
_)     -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n' TT Name
ty, Accessibility
a)
        case forall a b. (a, b) -> b
snd (TT Name, Accessibility)
p of
          Accessibility
Hidden -> if Bool
all then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a, b) -> a
fst (TT Name, Accessibility)
p) else []
          Accessibility
Private -> if Bool
all then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a, b) -> a
fst (TT Name, Accessibility)
p) else []
          Accessibility
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a, b) -> a
fst (TT Name, Accessibility)
p)
  where
    names :: [(Name, TTDecl)]
names = let ns :: [(Name, TTDecl)]
ns = forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt) in
                if Bool
exact
                   then forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', TTDecl
d) -> Name
n' 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 = forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall {t} {b} {a}. (t -> b) -> [(a, t)] -> [(a, b)]
mapSnd forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst forall a b. (a -> b) -> a -> b
$ 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) 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
    = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {e} {f}.
(a, b, c, Accessibility, e, f) -> (a, Accessibility)
mkp forall a b. (a -> b) -> a -> b
$ forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  -- io_bind a special case for REPL prettiness
  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 forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_bind" Bool -> Bool -> Bool
|| Name
n 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {b} {c} {b} {a} {f}. (a, b, c, b, a, f) -> (a, b)
unpack forall a b. (a -> b) -> a -> b
$ 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
    = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {b} {c} {e} {f}.
(a, b, c, Accessibility, e, f) -> (a, Accessibility)
mkp forall a b. (a -> b) -> a -> b
$ forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  -- io_bind a special case for REPL prettiness
  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 forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_bind" Bool -> Bool -> Bool
|| Name
n 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 = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> e
mkt forall a b. (a -> b) -> a -> b
$ 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> e
mkt forall a b. (a -> b) -> a -> b
$ 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 = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> e
mkt forall a b. (a -> b) -> a -> b
$ 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> b
mkt forall a b. (a -> b) -> a -> b
$ 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> c
mkt forall a b. (a -> b) -> a -> b
$ 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

-- Assume type is at least in whnfArgs form
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 (forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n 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 (forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n forall n. TT n
Erased) TT Name
sc)
    checkArgs TT Name
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()

linearCheckArg :: Context -> Type -> TC ()
linearCheckArg :: Context -> TT Name -> TC ()
linearCheckArg Context
ctxt TT Name
ty = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> TC ()
checkNameOK (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 ->
                  forall a. Err -> TC a
tfail forall a b. (a -> b) -> a -> b
$ forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
f forall a. [a] -> [a] -> [a]
++ String
" can only appear in a linear binding"
              Maybe RigCount
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- Check if a name is reducible in the type checker. Partial definitions
-- are not reducible (so treated as a constant)
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 = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> f
mkm forall a b. (a -> b) -> a -> b
$ 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 = forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, (Def
_, RigCount
_, Bool
_, Accessibility
_, Totality
t, MetaInformation
_)) -> (Name
n, Totality
t)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n 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 <- forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
        case forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst TTDecl
def of
          (Function TT Name
_ TT Name
htm) -> 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) -> 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 = 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 []           = forall a. Maybe a
Nothing
  li t
n t
i ((t
x, b
r, Binder c
b): [(t, b, Binder c)]
xs)
             | t
n forall a. Eq a => a -> a -> Bool
== t
x = forall a. a -> Maybe a
Just (t
i, b
r, 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
iforall a. Num a => a -> a -> a
+t
1) [(t, b, Binder c)]
xs

-- | Create a unique name given context and other existing names
uniqueNameCtxt :: Context -> Name -> [Name] -> Name
uniqueNameCtxt :: Context -> Name -> [Name] -> Name
uniqueNameCtxt Context
ctxt Name
n [Name]
hs
    | Name
n 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
          forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt (Name
n'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) = 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