{-|
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
import Control.Monad.State
import Data.List
import Data.Maybe (listToMaybe)
import GHC.Generics (Generic)

import qualified Data.Map.Strict as Map

data EvalState = ES { EvalState -> [(Name, Int)]
limited :: [(Name, Int)],
                      EvalState -> Int
nexthole :: Int,
                      EvalState -> Bool
blocking :: Bool }
  deriving Int -> EvalState -> ShowS
[EvalState] -> ShowS
EvalState -> String
(Int -> EvalState -> ShowS)
-> (EvalState -> String)
-> ([EvalState] -> ShowS)
-> Show EvalState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EvalState -> ShowS
showsPrec :: Int -> EvalState -> ShowS
$cshow :: EvalState -> String
show :: EvalState -> String
$cshowList :: [EvalState] -> ShowS
showList :: [EvalState] -> ShowS
Show

type Eval a = State EvalState a

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

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

-- 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 = TT Name -> String
forall a. Show a => a -> String
show (TT Name -> String) -> TT Name -> String
forall a b. (a -> b) -> a -> b
$ State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
100 Value
x) EvalState
initEval

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

-- 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
   = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [] (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) TT Name
t []
                   Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | 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
   = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [] (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) TT Name
t [EvalOpt
AtREPL]
                   Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | 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
   = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt ((Name -> (Name, Int)) -> [Name] -> [(Name, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, Int
0)) [Name]
blocked)
                                          (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) TT Name
t [EvalOpt
AtREPL]
                   Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval

normalise :: Context -> Env -> TT Name -> TT Name
normalise :: Context -> Env -> TT Name -> TT Name
normalise = Bool -> Context -> Env -> TT Name -> TT Name
normaliseTrace Bool
False

normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
normaliseTrace Bool
tr Context
ctxt Env
env TT Name
t
   = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
tr Context
ctxt [] (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t) []
                   Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval

toValue :: Context -> Env -> TT Name -> Value
toValue :: Context -> Env -> TT Name -> Value
toValue Context
ctxt Env
env TT Name
t
  = Eval Value -> EvalState -> Value
forall s a. State s a -> s -> a
evalState (Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [] (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) TT Name
t []) EvalState
initEval

quoteTerm :: Value -> TT Name
quoteTerm :: Value -> TT Name
quoteTerm Value
val = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- 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) =
          State EvalState (TT Name) -> EvalState -> (TT Name, EvalState)
forall s a. State s a -> s -> (a, s)
runState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt []
                                 (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                                 [EvalOpt
Spec]
                       Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) (EvalState
initEval { limited = limits }) in
         (TT Name
tm, EvalState -> [(Name, Int)]
limited EvalState
st)

-- | 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
   = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [(String -> Name
sUN String
"lazy", Int
0),
                                           (String -> Name
sUN String
"force", Int
0),
                                           (String -> Name
sUN String
"Force", Int
0),
                                           (String -> Name
sUN String
"assert_smaller", Int
0),
                                           (String -> Name
sUN String
"assert_total", Int
0),
                                           (String -> Name
sUN String
"par", Int
0),
                                           (String -> Name
sUN String
"prim__syntactic_eq", Int
0),
                                           (String -> Name
sUN String
"fork", Int
0)]
                                 (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                                 [Bool -> EvalOpt
Simplify Bool
True]
                   Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | 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
   = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt []
                                 (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                                 [Bool -> EvalOpt
Simplify Bool
False]
                   Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | 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
   = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [(String -> Name
sUN String
"lazy", Int
0),
                                           (String -> Name
sUN String
"force", Int
0),
                                           (String -> Name
sUN String
"Force", Int
0),
                                           (String -> Name
sUN String
"par", Int
0),
                                           (String -> Name
sUN String
"prim__syntactic_eq", Int
0),
                                           (String -> Name
sUN String
"prim_fork", Int
0)]
                                 (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                                 [EvalOpt
RunTT]
                   Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval

-- | Unfold 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
   = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (do Value
val <- Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [(Name, Int)]
ns
                               (((Name, RigCount, Binder (TT Name))
 -> (Name, RigCount, Binder (TT Name)))
-> Env -> Env
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name))
-> (Name, RigCount, Binder (TT Name))
finalEntry Env
env) (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                               [EvalOpt
Unfold]
                   Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 Value
val) EvalState
initEval


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

usable :: Bool -- 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 [] = (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [])
usable Bool
True Bool
uf Int
depthlimit Name
n [(Name, Int)]
ns
  = do ES [(Name, Int)]
ls Int
num Bool
b <- StateT EvalState Identity EvalState
forall s (m :: * -> *). MonadState s m => m s
get
       if Bool
b then (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
            else case Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
ls of
                    Just Int
0 -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
                    Just Int
i -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [(Name, Int)]
ns)
                    Maybe Int
_ -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
usable Bool
False Bool
uf Int
depthlimit Name
n [(Name, Int)]
ns
  = case Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
ns of
         Just Int
0 -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
         Just Int
i -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)]))
-> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a b. (a -> b) -> a -> b
$ (Bool
True, (Name
n, Int -> Int
forall a. Num a => a -> a
abs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
: ((Name, Int) -> Bool) -> [(Name, Int)] -> [(Name, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', Int
_) -> Name
nName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ns)
         Maybe Int
_ -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)]))
-> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall a b. (a -> b) -> a -> b
$ if Bool
uf
                          then (Bool
False, [(Name, Int)]
ns)
                          else (Bool
True, (Name
n, Int
depthlimit) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
: ((Name, Int) -> Bool) -> [(Name, Int)] -> [(Name, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', Int
_) -> Name
nName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ns)


fnCount :: Int -> Name -> Eval ()
fnCount :: Int -> Name -> Eval ()
fnCount Int
inc Name
n
         = do ES [(Name, Int)]
ls Int
num Bool
b <- StateT EvalState Identity EvalState
forall s (m :: * -> *). MonadState s m => m s
get
              case Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
ls of
                  Just Int
i -> do EvalState -> Eval ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalState -> Eval ()) -> EvalState -> Eval ()
forall a b. (a -> b) -> a -> b
$ [(Name, Int)] -> Int -> Bool -> EvalState
ES ((Name
n, (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
inc)) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
:
                                           ((Name, Int) -> Bool) -> [(Name, Int)] -> [(Name, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', Int
_) -> Name
nName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ls) Int
num Bool
b
                  Maybe Int
_ -> () -> Eval ()
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

setBlock :: Bool -> Eval ()
setBlock :: Bool -> Eval ()
setBlock Bool
b = do ES [(Name, Int)]
ls Int
num Bool
_ <- StateT EvalState Identity EvalState
forall s (m :: * -> *). MonadState s m => m s
get
                EvalState -> Eval ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([(Name, Int)] -> Int -> Bool -> EvalState
ES [(Name, Int)]
ls Int
num Bool
b)

deduct :: Name -> Eval ()
deduct = Int -> Name -> Eval ()
fnCount Int
1
reinstate :: Name -> Eval ()
reinstate = Int -> Name -> Eval ()
fnCount (-Int
1)

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

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

    -- 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
|| Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
n t Name
stk
       | Bool
simpl
           = (Bool -> Bool
not Bool
inl Bool -> Bool -> Bool
|| Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
n t Name
stk)
             Bool -> Bool -> Bool
|| (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"prim__syntactic_eq")
       | Bool
otherwise = Bool
False

    getCases :: CaseDefs -> ([Name], SC)
getCases CaseDefs
cd | Bool
simpl = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd
                | Bool
runtime = CaseDefs -> ([Name], SC)
cases_runtime CaseDefs
cd
                | Bool
otherwise = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd

    ev :: [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (P NameType
_ Name
n TT Name
ty)
        | Just (Let RigCount
_ TT Name
t TT Name
v) <- Name -> Env -> Maybe (Binder (TT Name))
forall n. Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
lookupBinder Name
n Env
genv = [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
v
    ev [(Name, Int)]
ntimes_in [Name]
stk Bool
top [(Name, Value)]
env (P NameType
Ref Name
n TT Name
ty)
         = do let limit :: Int
limit = if Bool
simpl then Int
100 else Int
10000
              (Bool
u, [(Name, Int)]
ntimes) <- Bool
-> Bool
-> Int
-> Name
-> [(Name, Int)]
-> Eval (Bool, [(Name, Int)])
usable Bool
spec Bool
unfold Int
limit Name
n [(Name, Int)]
ntimes_in
              let red :: Bool
red = Bool
u Bool -> Bool -> Bool
&& (Name -> Context -> Bool
tcReducible Name
n Context
ctxt Bool -> Bool -> Bool
|| Bool
spec Bool -> Bool -> Bool
|| (Bool
atRepl Bool -> Bool -> Bool
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env)
                                Bool -> Bool -> Bool
|| Bool
runtime Bool -> Bool -> Bool
|| Bool
unfold
                                Bool -> Bool -> Bool
|| String -> Name
sUN String
"assert_total" Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
stk)
              if Bool
red then
               do let val :: Maybe (Def, Accessibility)
val = Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n (Bool
spec Bool -> Bool -> Bool
|| Bool
unfold Bool -> Bool -> Bool
|| (Bool
atRepl Bool -> Bool -> Bool
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env) Bool -> Bool -> Bool
|| Bool
runtime) Context
ctxt
                  case Maybe (Def, Accessibility)
val of
                    Just (Function TT Name
_ TT Name
tm, Accessibility
Public) ->
                           [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
stk) Bool
True [(Name, Value)]
env TT Name
tm
                    Just (TyDecl NameType
nt TT Name
ty, Accessibility
_) -> do Value
vty <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
True [(Name, Value)]
env TT Name
ty
                                                 Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ NameType -> Name -> Value -> Value
VP NameType
nt Name
n Value
vty
                    Just (CaseOp CaseInfo
ci TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
cd, Accessibility
acc)
                         | (Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Public Bool -> Bool -> Bool
|| Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Hidden) Bool -> Bool -> Bool
&&
--                                || sUN "assert_total" `elem` stk) &&
                             [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (([Name], SC) -> [Name]
forall a b. (a, b) -> a
fst (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd)) -> -- unoptimised version
                       let ([Name]
ns, SC
tree) = CaseDefs -> ([Name], SC)
getCases CaseDefs
cd in
                         if CaseInfo -> Name -> [Name] -> Bool
forall {t :: * -> *}.
Foldable t =>
CaseInfo -> Name -> t Name -> Bool
blockSimplify CaseInfo
ci Name
n [Name]
stk
                            then (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
                            else -- 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
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
stk) Bool
top [(Name, Value)]
env [Name]
ns [] SC
tree
                                    case (Maybe Value, [Value])
c of
                                        (Maybe Value
Nothing, [Value]
_) -> (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
                                        (Just Value
v, [Value]
_)  -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
                    Maybe (Def, Accessibility)
_ -> (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
               else (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (P NameType
nt Name
n TT Name
ty)
        = (Value -> Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> Value -> Value
VP NameType
nt Name
n) ([(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
ty)
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (V Int
i)
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Value)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Value)]
env Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ (Name, Value) -> Value
forall a b. (a, b) -> b
snd ([(Name, Value)]
env [(Name, Value)] -> Int -> (Name, Value)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
        | Bool
otherwise      = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Int -> Value
VV Int
i
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Bind Name
n (Let RigCount
c TT Name
t TT Name
v) TT Name
sc)
        | (Bool -> Bool
not (Bool
runtime Bool -> Bool -> Bool
|| Bool
simpl_inline Bool -> Bool -> Bool
|| Bool
unfold)) Bool -> Bool -> Bool
|| Name -> TT Name -> Int
forall n. Eq n => n -> TT n -> Int
occurrences Name
n TT Name
sc Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2
           = do Value
v' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
v --(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') (Name, Value) -> [(Name, Value)] -> [(Name, Value)]
forall a. a -> [a] -> [a]
: [(Name, Value)]
env) TT Name
sc
                Int -> Value -> Eval Value
wknV (-Int
1) Value
sc'
        | Bool
otherwise
           = do Value
t' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
t
                Value
v' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
v --(finalise v)
                -- use Tmp as a placeholder, then make it a variable reference
                -- again when evaluation finished
                EvalState
hs <- StateT EvalState Identity EvalState
forall s (m :: * -> *). MonadState s m => m s
get
                let vd :: Int
vd = EvalState -> Int
nexthole EvalState
hs
                EvalState -> Eval ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalState
hs { nexthole = vd + 1 })
                Value
sc' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top ((Name
n, NameType -> Name -> Value -> Value
VP NameType
Bound (Int -> String -> Name
sMN Int
vd String
"vlet") Value
VErased) (Name, Value) -> [(Name, Value)] -> [(Name, Value)]
forall a. a -> [a] -> [a]
: [(Name, Value)]
env) TT Name
sc
                Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ RigCount -> Int -> Name -> Value -> Value -> Value -> Value
VBLet RigCount
c Int
vd Name
n Value
t' Value
v' Value
sc'
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Bind Name
n (NLet TT Name
t TT Name
v) TT Name
sc)
           = do Value
t' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
t)
                Value
v' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
v)
                Value
sc' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top ((Name
n, Value
v') (Name, Value) -> [(Name, Value)] -> [(Name, Value)]
forall a. a -> [a] -> [a]
: [(Name, Value)]
env) TT Name
sc
                Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Binder Value -> (Value -> Eval Value) -> Value
VBind Bool
True Name
n (RigCount -> Value -> Value -> Binder Value
forall b. RigCount -> b -> b -> Binder b
Let RigCount
RigW Value
t' Value
v') (\Value
x -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
sc')
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Bind Name
n Binder (TT Name)
b TT Name
sc)
           = do Binder Value
b' <- [(Name, Value)]
-> Binder (TT Name) -> StateT EvalState Identity (Binder Value)
vbind [(Name, Value)]
env Binder (TT Name)
b
                let n' :: Name
n' = Name -> [Name] -> Name
uniqueName Name
n (((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
genv [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ((Name, Value) -> Name) -> [(Name, Value)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Value) -> Name
forall a b. (a, b) -> a
fst [(Name, Value)]
env)
                Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Binder Value -> (Value -> Eval Value) -> Value
VBind Bool
True -- (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)(Name, Value) -> [(Name, Value)] -> [(Name, Value)]
forall a. a -> [a] -> [a]
:[(Name, Value)]
env) TT Name
sc)
       where vbind :: [(Name, Value)]
-> Binder (TT Name) -> StateT EvalState Identity (Binder Value)
vbind [(Name, Value)]
env Binder (TT Name)
t
                     = (TT Name -> Eval Value)
-> Binder (TT Name) -> StateT EvalState Identity (Binder Value)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder a -> m (Binder b)
fmapMB (\TT Name
tm -> [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
tm)) Binder (TT Name)
t
    -- 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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" Bool -> Bool -> Bool
&& Text
lco Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Infinite" Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
unfold Bool -> Bool -> Bool
|| Bool
simpl)
            = do let (TT Name
f, [TT Name]
_) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
arg
                 let ntimes' :: [(Name, Int)]
ntimes' = case TT Name
f of
                                    P NameType
_ Name
fn TT Name
_ -> (Name
fn, Int
0) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
: [(Name, Int)]
ntimes
                                    TT Name
_ -> [(Name, Int)]
ntimes
                 Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec (Eval () -> Eval ()) -> Eval () -> Eval ()
forall a b. (a -> b) -> a -> b
$ Bool -> Eval ()
setBlock Bool
True
                 Value
d' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes' [Name]
stk Bool
False [(Name, Value)]
env TT Name
d
                 Value
l' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes' [Name]
stk Bool
False [(Name, Value)]
env TT Name
l
                 Value
t' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes' [Name]
stk Bool
False [(Name, Value)]
env TT Name
t
                 Value
arg' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes' [Name]
stk Bool
False [(Name, Value)]
env TT Name
arg
                 Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec (Eval () -> Eval ()) -> Eval () -> Eval ()
forall a b. (a -> b) -> a -> b
$ Bool -> Eval ()
setBlock Bool
False
                 [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes' [Name]
stk Bool
top [(Name, Value)]
env [Value
l',Value
t',Value
arg'] Value
d'
    -- 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
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env)Bool -> Bool -> Bool
|| Bool
runtime) Context
ctxt,
         Text
at Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"assert_total" Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
simpl Bool -> Bool -> Bool
|| Bool
unfold)
            = [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
stk) Bool
top [(Name, Value)]
env TT Name
arg
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (App AppStatus Name
_ TT Name
f TT Name
a)
           = do Value
f' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
False [(Name, Value)]
env TT Name
f
                Value
a' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
False [(Name, Value)]
env TT Name
a
                [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [Value
a'] Value
f'
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Proj TT Name
t Int
i)
           = do -- 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' []
                Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> (Value, [Value]) -> Value
doProj Value
t' (Value -> (Value, [Value])
getValArgs Value
t'))
       where doProj :: Value -> (Value, [Value]) -> Value
doProj Value
t' (VP (DCon Int
_ Int
_ Bool
_) Name
_ Value
_, [Value]
args)
                  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Value] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args = [Value]
args[Value] -> Int -> Value
forall a. HasCallStack => [a] -> Int -> a
!!Int
i
             doProj Value
t' (Value, [Value])
_ = Value -> Int -> Value
VProj Value
t' Int
i

    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Constant Const
c) = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Const -> Value
VConstant Const
c
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
Erased    = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
VErased
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
Impossible  = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
VImpossible
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Inferred TT Name
tm) = [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
tm
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (TType UExp
i)   = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ UExp -> Value
VType UExp
i
    ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (UType Universe
u)   = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Universe -> Value
VUType Universe
u

    evApply :: [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [Value]
args (VApp Value
f Value
a)
          = [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Value
aValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
args) Value
f
    evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [Value]
args Value
f
          = [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> Value
-> [Value]
-> Eval Value
apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env Value
f [Value]
args

    apply :: [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> Value
-> [Value]
-> Eval Value
apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (VBind Bool
True Name
n (Lam RigCount
_ Value
t) Value -> Eval Value
sc) (Value
a:[Value]
as)
         = do Value
a' <- Value -> Eval Value
sc Value
a
              Value
app <- [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> Value
-> [Value]
-> Eval Value
apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env Value
a' [Value]
as
              Int -> Value -> Eval Value
wknV Int
1 Value
app
    apply [(Name, Int)]
ntimes_in [Name]
stk Bool
top [(Name, Value)]
env f :: Value
f@(VP NameType
Ref Name
n Value
ty) [Value]
args
         = do let limit :: Int
limit = if Bool
simpl then Int
100 else Int
10000
              (Bool
u, [(Name, Int)]
ntimes) <- Bool
-> Bool
-> Int
-> Name
-> [(Name, Int)]
-> Eval (Bool, [(Name, Int)])
usable Bool
spec Bool
unfold Int
limit Name
n [(Name, Int)]
ntimes_in
              let red :: Bool
red = Bool
u Bool -> Bool -> Bool
&& (Name -> Context -> Bool
tcReducible Name
n Context
ctxt Bool -> Bool -> Bool
|| Bool
spec Bool -> Bool -> Bool
|| (Bool
atRepl Bool -> Bool -> Bool
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env)
                                Bool -> Bool -> Bool
|| Bool
unfold Bool -> Bool -> Bool
|| Bool
runtime
                                Bool -> Bool -> Bool
|| String -> Name
sUN String
"assert_total" Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
stk)
              if Bool
red then
                 do let val :: Maybe (Def, Accessibility)
val = Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n (Bool
spec Bool -> Bool -> Bool
|| Bool
unfold Bool -> Bool -> Bool
|| (Bool
atRepl Bool -> Bool -> Bool
&& [(Name, Value)] -> Bool
forall {a}. [(a, Value)] -> Bool
noFree [(Name, Value)]
env) Bool -> Bool -> Bool
|| Bool
runtime) Context
ctxt
                    case Maybe (Def, Accessibility)
val of
                      Just (CaseOp CaseInfo
ci TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
cd, Accessibility
acc)
                           | Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Public Bool -> Bool -> Bool
|| Accessibility
acc Accessibility -> Accessibility -> Bool
forall a. Eq a => a -> a -> Bool
== Accessibility
Hidden ->
                           -- unoptimised version
                       let ([Name]
ns, SC
tree) = CaseDefs -> ([Name], SC)
getCases CaseDefs
cd in
                         if CaseInfo -> Name -> [Name] -> Bool
forall {t :: * -> *}.
Foldable t =>
CaseInfo -> Name -> t Name -> Bool
blockSimplify CaseInfo
ci Name
n [Name]
stk
                           then Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n Value
ty) [Value]
args
                           else -- 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
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
stk) Bool
top [(Name, Value)]
env [Name]
ns [Value]
args SC
tree
                                   case (Maybe Value, [Value])
c of
                                      (Maybe Value
Nothing, [Value]
_) -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n Value
ty) [Value]
args
                                      (Just Value
v, [Value]
rest) -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [Value]
rest Value
v
                      Just (Operator TT Name
_ Int
i [Value] -> Maybe Value
op, Accessibility
_)  ->
                        if (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Value] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args)
                           then case [Value] -> Maybe Value
op (Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
take Int
i [Value]
args) of
                              Maybe Value
Nothing -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n Value
ty) [Value]
args
                              Just Value
v  -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [Value]
-> Value
-> Eval Value
evApply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env (Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
drop Int
i [Value]
args) Value
v
                           else Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env (NameType -> Name -> Value -> Value
VP NameType
Ref Name
n Value
ty) [Value]
args
                      Maybe (Def, Accessibility)
_ -> case [Value]
args of
                              [] -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
f
                              [Value]
_ -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env Value
f [Value]
args
                 else case [Value]
args of
                           (Value
a : [Value]
as) -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env Value
f (Value
aValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
as)
                           [] -> Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
f
    apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env Value
f (Value
a:[Value]
as) = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Name, Value)] -> Value -> [Value] -> Value
unload [(Name, Value)]
env Value
f (Value
aValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
as)
    apply [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env Value
f []     = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
f

--     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
        | [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Value] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args
             = do let args' :: [Value]
args' = Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
take ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns) [Value]
args
                  let rest :: [Value]
rest  = Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
drop ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns) [Value]
args
                  Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec (Eval () -> Eval ()) -> Eval () -> Eval ()
forall a b. (a -> b) -> a -> b
$ Name -> Eval ()
deduct Name
n
                  Maybe Value
t <- [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> SC
-> Eval (Maybe Value)
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args') SC
tree
                  Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
spec (Eval () -> Eval ()) -> Eval () -> Eval ()
forall a b. (a -> b) -> a -> b
$ case Maybe Value
t of
                                   Maybe Value
Nothing -> Name -> Eval ()
reinstate Name
n -- Blocked, count n again
                                   Just Value
_ -> () -> Eval ()
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
--                                 (zipWith (\n , t) -> (n, t)) ns args') tree
                  (Maybe Value, [Value])
-> StateT EvalState Identity (Maybe Value, [Value])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Value
t, [Value]
rest)
        | Bool
otherwise = (Maybe Value, [Value])
-> StateT EvalState Identity (Maybe Value, [Value])
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Value
forall a. Maybe a
Nothing, [Value]
args)

    evTree :: [(Name, Int)] -> [Name] -> Bool ->
              [(Name, Value)] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
    evTree :: [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> SC
-> Eval (Maybe Value)
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap (UnmatchedCase String
str) = Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing
    evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap (STerm TT Name
tm)
        = do let etm :: TT Name
etm = [Name] -> TT Name -> TT Name
forall n. Eq n => [n] -> TT n -> TT n
pToVs (((Name, Value) -> Name) -> [(Name, Value)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Value) -> Name
forall a b. (a, b) -> a
fst [(Name, Value)]
amap) TT Name
tm
             Value
etm' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk (Bool -> Bool
not (TT Name -> Bool
forall {n}. TT n -> Bool
conHeaded TT Name
tm))
                                   ([(Name, Value)]
amap [(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall a. [a] -> [a] -> [a]
++ [(Name, Value)]
env) TT Name
etm
             Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Value -> Eval (Maybe Value))
-> Maybe Value -> Eval (Maybe Value)
forall a b. (a -> b) -> a -> b
$ Value -> Maybe Value
forall a. a -> Maybe a
Just Value
etm'
    evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap (ProjCase TT Name
t [CaseAlt' (TT Name)]
alts)
        = do Value
t' <- [(Name, Int)]
-> [Name] -> Bool -> [(Name, Value)] -> TT Name -> Eval Value
ev [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env TT Name
t
             [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> Value
-> [CaseAlt' (TT Name)]
-> Eval (Maybe Value)
doCase [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap Value
t' [CaseAlt' (TT Name)]
alts
    evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap (Case CaseType
_ Name
n [CaseAlt' (TT Name)]
alts)
        = case Name -> [(Name, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Value)]
amap of
            Just Value
v -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> Value
-> [CaseAlt' (TT Name)]
-> Eval (Maybe Value)
doCase [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap Value
v [CaseAlt' (TT Name)]
alts
            Maybe Value
_ -> Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing
    evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap SC
ImpossibleCase = Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing

    doCase :: [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> Value
-> [CaseAlt' (TT Name)]
-> Eval (Maybe Value)
doCase [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
amap Value
v [CaseAlt' (TT Name)]
alts =
            do Maybe ([(Name, Value)], SC)
c <- [(Name, Value)]
-> Value
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt [(Name, Value)]
env Value
v (Value -> (Value, [Value])
getValArgs Value
v) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
               case Maybe ([(Name, Value)], SC)
c of
                    Just ([(Name, Value)]
altmap, SC
sc) -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> SC
-> Eval (Maybe Value)
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
altmap SC
sc
                    Maybe ([(Name, Value)], SC)
_ -> do Maybe ([(Name, Value)], SC)
c' <- [(Name, Int)]
-> [Name]
-> [(Name, Value)]
-> Value
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
forall {p}.
[(Name, Int)]
-> [Name]
-> [(Name, Value)]
-> p
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt' [(Name, Int)]
ntimes [Name]
stk [(Name, Value)]
env Value
v (Value -> (Value, [Value])
getValArgs Value
v) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
                            case Maybe ([(Name, Value)], SC)
c' of
                                 Just ([(Name, Value)]
altmap, SC
sc) -> [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> [(Name, Value)]
-> SC
-> Eval (Maybe Value)
evTree [(Name, Int)]
ntimes [Name]
stk Bool
top [(Name, Value)]
env [(Name, Value)]
altmap SC
sc
                                 Maybe ([(Name, Value)], SC)
_ -> Maybe Value -> Eval (Maybe Value)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing

    conHeaded :: TT n -> Bool
conHeaded tm :: TT n
tm@(App AppStatus n
_ TT n
_ TT n
_)
        | (P (DCon Int
_ Int
_ Bool
_) n
_ TT n
_, [TT n]
args) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = Bool
True
    conHeaded TT n
t = Bool
False

    chooseAlt' :: [(Name, Int)]
-> [Name]
-> [(Name, Value)]
-> p
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt' [(Name, Int)]
ntimes  [Name]
stk [(Name, Value)]
env p
_ (Value
f, [Value]
args) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
        = do Value
f' <- [(Name, Int)]
-> [Name]
-> Bool
-> [(Name, Value)]
-> Value
-> [Value]
-> Eval Value
apply [(Name, Int)]
ntimes [Name]
stk Bool
True [(Name, Value)]
env Value
f [Value]
args
             [(Name, Value)]
-> Value
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt [(Name, Value)]
env Value
f' (Value -> (Value, [Value])
getValArgs Value
f')
                       [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap

    chooseAlt :: [(Name, Value)] -> Value -> (Value, [Value]) -> [CaseAlt] ->
                 [(Name, Value)] ->
                 Eval (Maybe ([(Name, Value)], SC))
    chooseAlt :: [(Name, Value)]
-> Value
-> (Value, [Value])
-> [CaseAlt' (TT Name)]
-> [(Name, Value)]
-> Eval (Maybe ([(Name, Value)], SC))
chooseAlt [(Name, Value)]
env Value
_ (VP (DCon Int
i Int
a Bool
_) Name
_ Value
_, [Value]
args) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
        | Just ([Name]
ns, SC
sc) <- Int -> [CaseAlt' (TT Name)] -> Maybe ([Name], SC)
forall {t}. Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [CaseAlt' (TT Name)]
alts = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args) [(Name, Value)]
amap, SC
sc)
        | Just SC
v <- [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts      = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
    chooseAlt [(Name, Value)]
env Value
_ (VP (TCon Int
i Int
a) Name
_ Value
_, [Value]
args) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
        | Just ([Name]
ns, SC
sc) <- Int -> [CaseAlt' (TT Name)] -> Maybe ([Name], SC)
forall {t}. Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [CaseAlt' (TT Name)]
alts
                            = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args) [(Name, Value)]
amap, SC
sc)
        | Just SC
v <- [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts      = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
    chooseAlt [(Name, Value)]
env Value
_ (VConstant Const
c, []) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
        | Just SC
v <- Const -> [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [CaseAlt' (TT Name)]
alts      = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
        | Just (Name
n', Value
sub, SC
sc) <- Const -> [CaseAlt' (TT Name)] -> Maybe (Name, Value, SC)
forall {t}. Const -> [CaseAlt' t] -> Maybe (Name, Value, SC' t)
findSuc Const
c [CaseAlt' (TT Name)]
alts
                            = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap [(Name
n',Value
sub)] [(Name, Value)]
amap, SC
sc)
        | Just SC
v <- [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts      = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
    chooseAlt [(Name, Value)]
env Value
_ (VP NameType
_ Name
n Value
_, [Value]
args) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
        | Just ([Name]
ns, SC
sc) <- Name -> [CaseAlt' (TT Name)] -> Maybe ([Name], SC)
forall {t}. Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn Name
n [CaseAlt' (TT Name)]
alts  = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value]
args) [(Name, Value)]
amap, SC
sc)
    chooseAlt [(Name, Value)]
env Value
_ (VBind Bool
_ Name
_ (Pi RigCount
_ Maybe ImplicitInfo
i Value
s Value
k) Value -> Eval Value
t, []) [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
        | Just ([Name]
ns, SC
sc) <- Name -> [CaseAlt' (TT Name)] -> Maybe ([Name], SC)
forall {t}. Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn (String -> Name
sUN String
"->") [CaseAlt' (TT Name)]
alts
           = do Value
t' <- Value -> Eval Value
t (Int -> Value
VV Int
0) -- we know it's not in scope or it's not a pattern
                Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)] -> [(Name, Value)] -> [(Name, Value)]
forall {a} {b}. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
updateAmap ([Name] -> [Value] -> [(Name, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [Value
s, Value
t']) [(Name, Value)]
amap, SC
sc)
    chooseAlt [(Name, Value)]
_ Value
_ (Value, [Value])
_ [CaseAlt' (TT Name)]
alts [(Name, Value)]
amap
        | Just SC
v <- [CaseAlt' (TT Name)] -> Maybe SC
forall {t}. [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' (TT Name)]
alts
             = if ((CaseAlt' (TT Name) -> Bool) -> [CaseAlt' (TT Name)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CaseAlt' (TT Name) -> Bool
forall {t}. CaseAlt' t -> Bool
fnCase [CaseAlt' (TT Name)]
alts)
                  then Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC)))
-> Maybe ([(Name, Value)], SC)
-> Eval (Maybe ([(Name, Value)], SC))
forall a b. (a -> b) -> a -> b
$ ([(Name, Value)], SC) -> Maybe ([(Name, Value)], SC)
forall a. a -> Maybe a
Just ([(Name, Value)]
amap, SC
v)
                  else Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(Name, Value)], SC)
forall a. Maybe a
Nothing
        | Bool
otherwise = Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(Name, Value)], SC)
forall a. Maybe a
Nothing

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

    -- 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 [(a, b)] -> [(a, b)] -> [(a, b)]
forall a. [a] -> [a] -> [a]
++ ((a, b) -> Bool) -> [(a, b)] -> [(a, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (a
x, b
_) -> Bool -> Bool
not (a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
x (((a, b) -> a) -> [(a, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> a
forall a b. (a, b) -> a
fst [(a, b)]
newm))) [(a, b)]
amap
    findTag :: Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [] = Maybe ([Name], SC' t)
forall a. Maybe a
Nothing
    findTag Int
i (ConCase Name
n Int
j [Name]
ns SC' t
sc : [CaseAlt' t]
xs) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = ([Name], SC' t) -> Maybe ([Name], SC' t)
forall a. a -> Maybe a
Just ([Name]
ns, SC' t
sc)
    findTag Int
i (CaseAlt' t
_ : [CaseAlt' t]
xs) = Int -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findTag Int
i [CaseAlt' t]
xs

    findFn :: Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn Name
fn [] = Maybe ([Name], SC' t)
forall a. Maybe a
Nothing
    findFn Name
fn (FnCase Name
n [Name]
ns SC' t
sc : [CaseAlt' t]
xs) | Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = ([Name], SC' t) -> Maybe ([Name], SC' t)
forall a. a -> Maybe a
Just ([Name]
ns, SC' t
sc)
    findFn Name
fn (CaseAlt' t
_ : [CaseAlt' t]
xs) = Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn Name
fn [CaseAlt' t]
xs

    findDefault :: [CaseAlt' t] -> Maybe (SC' t)
findDefault [] = Maybe (SC' t)
forall a. Maybe a
Nothing
    findDefault (DefaultCase SC' t
sc : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
sc
    findDefault (CaseAlt' t
_ : [CaseAlt' t]
xs) = [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' t]
xs

    findSuc :: Const -> [CaseAlt' t] -> Maybe (Name, Value, SC' t)
findSuc Const
c [] = Maybe (Name, Value, SC' t)
forall a. Maybe a
Nothing
    findSuc (BI Integer
val) (SucCase Name
n SC' t
sc : [CaseAlt' t]
_)
         | Integer
val Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 = (Name, Value, SC' t) -> Maybe (Name, Value, SC' t)
forall a. a -> Maybe a
Just (Name
n, Const -> Value
VConstant (Integer -> Const
BI (Integer
val Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)), SC' t
sc)
    findSuc Const
c (CaseAlt' t
_ : [CaseAlt' t]
xs) = Const -> [CaseAlt' t] -> Maybe (Name, Value, SC' t)
findSuc Const
c [CaseAlt' t]
xs

    findConst :: Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [] = Maybe (SC' t)
forall a. Maybe a
Nothing
    findConst Const
c (ConstCase Const
c' SC' t
v : [CaseAlt' t]
xs) | Const
c Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
c' = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt IntTy
ITNative)) (ConCase Name
n Int
1 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType ArithTy
ATFloat) (ConCase Name
n Int
2 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt IntTy
ITChar))  (ConCase Name
n Int
3 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst Const
StrType (ConCase Name
n Int
4 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt IntTy
ITBig)) (ConCase Name
n Int
6 [] SC' t
v : [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt (ITFixed NativeTy
ity))) (ConCase Name
n Int
tag [] SC' t
v : [CaseAlt' t]
xs)
        | Int
tag Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
7 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ NativeTy -> Int
forall a. Enum a => a -> Int
fromEnum NativeTy
ity = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst Const
c (CaseAlt' t
_ : [CaseAlt' t]
xs) = Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [CaseAlt' t]
xs

    getValArgs :: Value -> (Value, [Value])
getValArgs Value
tm = Value -> [Value] -> (Value, [Value])
getValArgs' Value
tm []
    getValArgs' :: Value -> [Value] -> (Value, [Value])
getValArgs' (VApp Value
f Value
a) [Value]
as = Value -> [Value] -> (Value, [Value])
getValArgs' Value
f (Value
aValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
as)
    getValArgs' Value
f [Value]
as = (Value
f, [Value]
as)

-- 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 = Value -> TT Name
forall {a}. Quote a => a -> TT Name
getTT Value
x TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== Value -> TT Name
forall {a}. Quote a => a -> TT Name
getTT Value
y
      where getTT :: a -> TT Name
getTT a
v = State EvalState (TT Name) -> EvalState -> TT Name
forall s a. State s a -> s -> a
evalState (Int -> a -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
0 a
v) EvalState
initEval

class Quote a where
    quote :: Int -> a -> Eval (TT Name)

instance Quote Value where
    quote :: Int -> Value -> State EvalState (TT Name)
quote Int
i (VP NameType
nt Name
n Value
v)      = (TT Name -> TT Name)
-> State EvalState (TT Name) -> State EvalState (TT Name)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n) (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
v)
    quote Int
i (VV Int
x)           = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> State EvalState (TT Name))
-> TT Name -> State EvalState (TT Name)
forall a b. (a -> b) -> a -> b
$ Int -> TT Name
forall n. Int -> TT n
V Int
x
    quote Int
i (VBind Bool
_ Name
n Binder Value
b Value -> Eval Value
sc) = do Value
sc' <- Value -> Eval Value
sc (Int -> Value
VTmp Int
i)
                                  Binder (TT Name)
b' <- Binder Value -> StateT EvalState Identity (Binder (TT Name))
forall {a}.
Quote a =>
Binder a -> StateT EvalState Identity (Binder (TT Name))
quoteB Binder Value
b
                                  (TT Name -> TT Name)
-> State EvalState (TT Name) -> State EvalState (TT Name)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder (TT Name)
b') (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Value
sc')
       where quoteB :: Binder a -> StateT EvalState Identity (Binder (TT Name))
quoteB Binder a
t = (a -> State EvalState (TT Name))
-> Binder a -> StateT EvalState Identity (Binder (TT Name))
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder a -> m (Binder b)
fmapMB (Int -> a -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i) Binder a
t
    quote Int
i (VBLet RigCount
c Int
vd Name
n Value
t Value
v Value
sc)
                           = do TT Name
sc' <- Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
sc
                                TT Name
t' <- Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
t
                                TT Name
v' <- Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
v
                                let sc'' :: TT Name
sc'' = Name -> TT Name -> TT Name
forall n. Eq n => n -> TT n -> TT n
pToV (Int -> String -> Name
sMN Int
vd String
"vlet") (TT Name -> TT Name
forall n. TT n -> TT n
addBinder TT Name
sc')
                                TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
c TT Name
t' TT Name
v') TT Name
sc'')
    quote Int
i (VApp Value
f Value
a)     = (TT Name -> TT Name -> TT Name)
-> State EvalState (TT Name)
-> State EvalState (TT Name)
-> State EvalState (TT Name)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
MaybeHoles) (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
f) (Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
a)
    quote Int
i (VType UExp
u)      = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> TT Name
forall n. UExp -> TT n
TType UExp
u)
    quote Int
i (VUType Universe
u)     = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe -> TT Name
forall n. Universe -> TT n
UType Universe
u)
    quote Int
i Value
VErased        = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Erased
    quote Int
i Value
VImpossible    = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Impossible
    quote Int
i (VProj Value
v Int
j)    = do TT Name
v' <- Int -> Value -> State EvalState (TT Name)
forall a. Quote a => Int -> a -> State EvalState (TT Name)
quote Int
i Value
v
                                TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Int -> TT Name
forall n. TT n -> Int -> TT n
Proj TT Name
v' Int
j)
    quote Int
i (VConstant Const
c)  = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> State EvalState (TT Name))
-> TT Name -> State EvalState (TT Name)
forall a b. (a -> b) -> a -> b
$ Const -> TT Name
forall n. Const -> TT n
Constant Const
c
    quote Int
i (VTmp Int
x)       = TT Name -> State EvalState (TT Name)
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> State EvalState (TT Name))
-> TT Name -> State EvalState (TT Name)
forall a b. (a -> b) -> a -> b
$ Int -> TT Name
forall n. Int -> TT n
V (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

wknV :: Int -> Value -> Eval Value
wknV :: Int -> Value -> Eval Value
wknV Int
i (VV Int
x) | Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
i = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Int -> Value
VV (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
wknV Int
i (VBind Bool
red Name
n Binder Value
b Value -> Eval Value
sc) = do Binder Value
b' <- (Value -> Eval Value)
-> Binder Value -> StateT EvalState Identity (Binder Value)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder a -> m (Binder b)
fmapMB (Int -> Value -> Eval Value
wknV Int
i) Binder Value
b
                               Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Binder Value -> (Value -> Eval Value) -> Value
VBind Bool
red Name
n Binder Value
b' (\Value
x -> do Value
x' <- Value -> Eval Value
sc Value
x
                                                                 Int -> Value -> Eval Value
wknV (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Value
x')
wknV Int
i (VApp Value
f Value
a)     = (Value -> Value -> Value) -> Eval Value -> Eval Value -> Eval Value
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Value -> Value -> Value
VApp (Int -> Value -> Eval Value
wknV Int
i Value
f) (Int -> Value -> Eval Value
wknV Int
i Value
a)
wknV Int
i Value
t              = Value -> Eval Value
forall a. a -> StateT EvalState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
t

isUniverse :: Term -> Bool
isUniverse :: TT Name -> Bool
isUniverse (TType UExp
_) = Bool
True
isUniverse (UType Universe
_) = Bool
True
isUniverse TT Name
_ = Bool
False

isUsableUniverse :: Term -> Bool
isUsableUniverse :: TT Name -> Bool
isUsableUniverse (UType Universe
NullType) = Bool
False
isUsableUniverse TT Name
x = TT Name -> Bool
isUniverse TT Name
x

convEq' :: Context -> [Name] -> TT Name -> TT Name -> TC Bool
convEq' Context
ctxt [Name]
hs TT Name
x TT Name
y = StateT UCs TC Bool -> UCs -> TC Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq Context
ctxt [Name]
hs TT Name
x TT Name
y) (Int
0, [])

convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq Context
ctxt [Name]
holes TT Name
topx TT Name
topy = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [] TT Name
topx TT Name
topy where
    ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
    ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps (P NameType
xt Name
x TT Name
_) (P NameType
yt Name
y TT Name
_)
        | Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y Bool -> Bool -> Bool
|| (Name
x, Name
y) (Name, Name) -> [(Name, Name)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, Name)]
ps Bool -> Bool -> Bool
|| (Name
y,Name
x) (Name, Name) -> [(Name, Name)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, Name)]
ps = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        | Bool
otherwise = [(Name, Name)] -> Name -> Name -> StateT UCs TC Bool
sameDefs [(Name, Name)]
ps Name
x Name
y

    ceq [(Name, Name)]
ps (Bind Name
n (PVar RigCount
_ TT Name
t) TT Name
sc) TT Name
y = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
sc TT Name
y
    ceq [(Name, Name)]
ps TT Name
x (Bind Name
n (PVar RigCount
_ TT Name
t) TT Name
sc) = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
sc
    ceq [(Name, Name)]
ps (Bind Name
n (PVTy TT Name
t) TT Name
sc) TT Name
y = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
sc TT Name
y
    ceq [(Name, Name)]
ps TT Name
x (Bind Name
n (PVTy TT Name
t) TT Name
sc) = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
sc

    ceq [(Name, Name)]
ps (V Int
x)      (V Int
y)      = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y)
    ceq [(Name, Name)]
ps (V Int
x)      (P NameType
_ Name
y TT Name
_)
        | Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& [(Name, Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
x = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, Name) -> Name
forall a b. (a, b) -> a
fst ([(Name, Name)]
ps[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
x) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y)
        | Bool
otherwise = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    ceq [(Name, Name)]
ps (P NameType
_ Name
x TT Name
_)  (V Int
y)
        | Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& [(Name, Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
y = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== (Name, Name) -> Name
forall a b. (a, b) -> b
snd ([(Name, Name)]
ps[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
y))
        | Bool
otherwise = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    ceq [(Name, Name)]
ps (Bind Name
n Binder (TT Name)
xb TT Name
xs) (Bind Name
n' Binder (TT Name)
yb TT Name
ys)
                             = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)]
-> Binder (TT Name) -> Binder (TT Name) -> StateT UCs TC Bool
ceqB [(Name, Name)]
ps Binder (TT Name)
xb Binder (TT Name)
yb) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq ((Name
n,Name
n')(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) TT Name
xs TT Name
ys)
        where
            ceqB :: [(Name, Name)]
-> Binder (TT Name) -> Binder (TT Name) -> StateT UCs TC Bool
ceqB [(Name, Name)]
ps (Let RigCount
c TT Name
v TT Name
t) (Let RigCount
c' TT Name
v' TT Name
t') = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
v TT Name
v') ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
t TT Name
t')
            ceqB [(Name, Name)]
ps (Guess TT Name
v TT Name
t) (Guess TT Name
v' TT Name
t') = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
v TT Name
v') ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
t TT Name
t')
            ceqB [(Name, Name)]
ps (Pi RigCount
r Maybe ImplicitInfo
i TT Name
v TT Name
t) (Pi RigCount
r' Maybe ImplicitInfo
i' TT Name
v' TT Name
t') = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
v TT Name
v') ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
t TT Name
t')
            ceqB [(Name, Name)]
ps Binder (TT Name)
b Binder (TT Name)
b' = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b) (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b')

    ceq [(Name, Name)]
ps TT Name
x (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
y (V Int
0)))
          = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x (TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
t) TT Name
y)
    ceq [(Name, Name)]
ps (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
x (V Int
0))) TT Name
y
          = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps (TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
t) TT Name
x) TT Name
y
    ceq [(Name, Name)]
ps TT Name
x (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
y (P NameType
Bound Name
n' TT Name
_)))
        | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
y
    ceq [(Name, Name)]
ps (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
x (P NameType
Bound Name
n' TT Name
_))) TT Name
y
        | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
y

    -- 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) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
x,
          (P NameType
_ Name
cy TT Name
_, [TT Name]
yargs) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
y,
          Name -> Bool
caseName Name
cx Bool -> Bool -> Bool
&& Name -> Bool
caseName Name
cy = [(Name, Name)]
-> Name -> Name -> [TT Name] -> [TT Name] -> StateT UCs TC Bool
sameCase [(Name, Name)]
ps Name
cx Name
cy [TT Name]
xargs [TT Name]
yargs

    ceq [(Name, Name)]
ps (App AppStatus Name
_ TT Name
fx TT Name
ax) (App AppStatus Name
_ TT Name
fy TT Name
ay) = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
fx TT Name
fy) ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
ax TT Name
ay)
    ceq [(Name, Name)]
ps (Constant Const
x) (Constant Const
y) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const
x Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
y)
    ceq [(Name, Name)]
ps (TType UExp
x) (TType UExp
y) | UExp
x UExp -> UExp -> Bool
forall a. Eq a => a -> a -> Bool
== UExp
y = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq [(Name, Name)]
ps (TType (UVal Int
0)) (TType UExp
y) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq [(Name, Name)]
ps (TType UExp
x) (TType UExp
y) = do (Int
v, [UConstraint]
cs) <- StateT UCs TC UCs
forall s (m :: * -> *). MonadState s m => m s
get
                                    UCs -> StateT UCs TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
v, UExp -> UExp -> UConstraint
ULE UExp
x UExp
y UConstraint -> [UConstraint] -> [UConstraint]
forall a. a -> [a] -> [a]
: [UConstraint]
cs)
                                    Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq [(Name, Name)]
ps (UType Universe
AllTypes) TT Name
x = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Bool
isUsableUniverse TT Name
x)
    ceq [(Name, Name)]
ps TT Name
x (UType Universe
AllTypes) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Bool
isUsableUniverse TT Name
x)
    ceq [(Name, Name)]
ps (UType Universe
u) (UType Universe
v) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe
u Universe -> Universe -> Bool
forall a. Eq a => a -> a -> Bool
== Universe
v)
    ceq [(Name, Name)]
ps TT Name
Erased TT Name
_ = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq [(Name, Name)]
ps TT Name
_ TT Name
Erased = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq [(Name, Name)]
ps TT Name
x TT Name
y = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    caseeq :: [(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq [(Name, Name)]
ps (Case CaseType
_ Name
n [CaseAlt' (TT Name)]
cs) (Case CaseType
_ Name
n' [CaseAlt' (TT Name)]
cs') = [(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA ((Name
n,Name
n')(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) [CaseAlt' (TT Name)]
cs [CaseAlt' (TT Name)]
cs'
      where
        caseeqA :: [(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA [(Name, Name)]
ps (ConCase Name
x Int
i [Name]
as SC
sc : [CaseAlt' (TT Name)]
rest) (ConCase Name
x' Int
i' [Name]
as' SC
sc' : [CaseAlt' (TT Name)]
rest')
            = do Bool
q1 <- [(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq ([Name] -> [Name] -> [(Name, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
as [Name]
as' [(Name, Name)] -> [(Name, Name)] -> [(Name, Name)]
forall a. [a] -> [a] -> [a]
++ [(Name, Name)]
ps) SC
sc SC
sc'
                 Bool
q2 <- [(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA [(Name, Name)]
ps [CaseAlt' (TT Name)]
rest [CaseAlt' (TT Name)]
rest'
                 Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> StateT UCs TC Bool) -> Bool -> StateT UCs TC Bool
forall a b. (a -> b) -> a -> b
$ Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i' Bool -> Bool -> Bool
&& Bool
q1 Bool -> Bool -> Bool
&& Bool
q2
        caseeqA [(Name, Name)]
ps (ConstCase Const
x SC
sc : [CaseAlt' (TT Name)]
rest) (ConstCase Const
x' SC
sc' : [CaseAlt' (TT Name)]
rest')
            = do Bool
q1 <- [(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq [(Name, Name)]
ps SC
sc SC
sc'
                 Bool
q2 <- [(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA [(Name, Name)]
ps [CaseAlt' (TT Name)]
rest [CaseAlt' (TT Name)]
rest'
                 Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> StateT UCs TC Bool) -> Bool -> StateT UCs TC Bool
forall a b. (a -> b) -> a -> b
$ Const
x Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
x' Bool -> Bool -> Bool
&& Bool
q1 Bool -> Bool -> Bool
&& Bool
q2
        caseeqA [(Name, Name)]
ps (DefaultCase SC
sc : [CaseAlt' (TT Name)]
rest) (DefaultCase SC
sc' : [CaseAlt' (TT Name)]
rest')
            = (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) ([(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq [(Name, Name)]
ps SC
sc SC
sc') ([(Name, Name)]
-> [CaseAlt' (TT Name)]
-> [CaseAlt' (TT Name)]
-> StateT UCs TC Bool
caseeqA [(Name, Name)]
ps [CaseAlt' (TT Name)]
rest [CaseAlt' (TT Name)]
rest')
        caseeqA [(Name, Name)]
ps [] [] = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        caseeqA [(Name, Name)]
ps [CaseAlt' (TT Name)]
_ [CaseAlt' (TT Name)]
_ = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    caseeq [(Name, Name)]
ps (STerm TT Name
x) (STerm TT Name
y) = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
y
    caseeq [(Name, Name)]
ps (UnmatchedCase String
_) (UnmatchedCase String
_) = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    caseeq [(Name, Name)]
ps SC
_ SC
_ = Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    sameDefs :: [(Name, Name)] -> Name -> Name -> StateT UCs TC Bool
sameDefs [(Name, Name)]
ps Name
x Name
y = case (Name -> Context -> [Def]
lookupDef Name
x Context
ctxt, Name -> Context -> [Def]
lookupDef Name
y Context
ctxt) of
                        ([Function TT Name
_ TT Name
xdef], [Function TT Name
_ TT Name
ydef])
                              -> [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq ((Name
x,Name
y)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) TT Name
xdef TT Name
ydef
                        ([CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
xd],
                         [CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
yd])
                              -> let ([Name]
_, SC
xdef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
xd
                                     ([Name]
_, SC
ydef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
yd in
                                       [(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq ((Name
x,Name
y)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) SC
xdef SC
ydef
                        ([Def], [Def])
_ -> Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] ->
                StateT UCs TC Bool
    sameCase :: [(Name, Name)]
-> Name -> Name -> [TT Name] -> [TT Name] -> StateT UCs TC Bool
sameCase [(Name, Name)]
ps Name
x Name
y [TT Name]
xargs [TT Name]
yargs
          = case (Name -> Context -> [Def]
lookupDef Name
x Context
ctxt, Name -> Context -> [Def]
lookupDef Name
y Context
ctxt) of
                 ([Function TT Name
_ TT Name
xdef], [Function TT Name
_ TT Name
ydef])
                       -> [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq ((Name
x,Name
y)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) TT Name
xdef TT Name
ydef
                 ([CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
xd],
                  [CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
yd])
                       -> let ([Name]
xin, SC
xdef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
xd
                              ([Name]
yin, SC
ydef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
yd in
                            do (Bool -> Bool -> Bool)
-> StateT UCs TC Bool -> StateT UCs TC Bool -> StateT UCs TC Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&)
                                  (do [Bool]
ok <- (TT Name -> TT Name -> StateT UCs TC Bool)
-> [TT Name] -> [TT Name] -> StateT UCs TC [Bool]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps)
                                              (Int -> [TT Name] -> [TT Name]
forall a. Int -> [a] -> [a]
drop ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
xin) [TT Name]
xargs)
                                              (Int -> [TT Name] -> [TT Name]
forall a. Int -> [a] -> [a]
drop ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
yin) [TT Name]
yargs)
                                      Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
ok))
                                  ([(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq ((Name
x,Name
y)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
ps) SC
xdef SC
ydef)
                 ([Def], [Def])
_ -> Bool -> StateT UCs TC Bool
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- 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. Def -> Rep Def x)
-> (forall x. Rep Def x -> Def) -> Generic Def
forall x. Rep Def x -> Def
forall x. Def -> Rep Def x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Def -> Rep Def x
from :: forall x. Def -> Rep Def x
$cto :: forall x. Rep Def x -> Def
to :: forall x. Rep Def x -> Def
Generic
--                   [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. CaseDefs -> Rep CaseDefs x)
-> (forall x. Rep CaseDefs x -> CaseDefs) -> Generic CaseDefs
forall x. Rep CaseDefs x -> CaseDefs
forall x. CaseDefs -> Rep CaseDefs x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CaseDefs -> Rep CaseDefs x
from :: forall x. CaseDefs -> Rep CaseDefs x
$cto :: forall x. Rep CaseDefs x -> CaseDefs
to :: forall x. Rep CaseDefs x -> CaseDefs
Generic

data CaseInfo = CaseInfo {
                  CaseInfo -> Bool
case_inlinable :: Bool, -- decided by machine
                  CaseInfo -> Bool
case_alwaysinline :: Bool, -- decided by %inline flag
                  CaseInfo -> Bool
tc_dictionary :: Bool
                }
  deriving (forall x. CaseInfo -> Rep CaseInfo x)
-> (forall x. Rep CaseInfo x -> CaseInfo) -> Generic CaseInfo
forall x. Rep CaseInfo x -> CaseInfo
forall x. CaseInfo -> Rep CaseInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CaseInfo -> Rep CaseInfo x
from :: forall x. CaseInfo -> Rep CaseInfo x
$cto :: forall x. Rep CaseInfo x -> CaseInfo
to :: forall x. Rep CaseInfo x -> CaseInfo
Generic

{-!
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: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (TT Name, TT Name) -> String
forall a. Show a => a -> String
show (TT Name
ty, TT Name
tm)
    show (TyDecl NameType
nt TT Name
ty) = String
"TyDecl: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NameType -> String
forall a. Show a => a -> String
show NameType
nt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
ty
    show (Operator TT Name
ty Int
_ [Value] -> Maybe Value
_) = String
"Operator: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
ty
    show (CaseOp (CaseInfo Bool
inlc Bool
inla Bool
inlr) TT Name
ty [(TT Name, Bool)]
atys [Either (TT Name) (TT Name, TT Name)]
ps_in [([Name], TT Name, TT Name)]
ps CaseDefs
cd)
      = let ([Name]
ns, SC
sc) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd
            ([Name]
ns', SC
sc') = CaseDefs -> ([Name], SC)
cases_runtime CaseDefs
cd in
          String
"Case: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [([Name], TT Name, TT Name)] -> String
forall a. Show a => a -> String
show [([Name], TT Name, TT Name)]
ps String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                        String
"COMPILE TIME:\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                        [Name] -> String
forall a. Show a => a -> String
show [Name]
ns String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
sc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                        String
"RUN TIME:\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                        [Name] -> String
forall a. Show a => a -> String
show [Name]
ns' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
sc' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
            if Bool
inlc then String
"Inlinable" else String
"Not inlinable" String -> ShowS
forall a. [a] -> [a] -> [a]
++
            if Bool
inla then String
" Aggressively\n" else String
"\n"

-------

-- 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
(Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Bool) -> Eq Accessibility
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Accessibility -> Accessibility -> Bool
== :: Accessibility -> Accessibility -> Bool
$c/= :: Accessibility -> Accessibility -> Bool
/= :: Accessibility -> Accessibility -> Bool
Eq, Eq Accessibility
Eq Accessibility =>
(Accessibility -> Accessibility -> Ordering)
-> (Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Bool)
-> (Accessibility -> Accessibility -> Accessibility)
-> (Accessibility -> Accessibility -> Accessibility)
-> Ord Accessibility
Accessibility -> Accessibility -> Bool
Accessibility -> Accessibility -> Ordering
Accessibility -> Accessibility -> Accessibility
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Accessibility -> Accessibility -> Ordering
compare :: Accessibility -> Accessibility -> Ordering
$c< :: Accessibility -> Accessibility -> Bool
< :: Accessibility -> Accessibility -> Bool
$c<= :: Accessibility -> Accessibility -> Bool
<= :: Accessibility -> Accessibility -> Bool
$c> :: Accessibility -> Accessibility -> Bool
> :: Accessibility -> Accessibility -> Bool
$c>= :: Accessibility -> Accessibility -> Bool
>= :: Accessibility -> Accessibility -> Bool
$cmax :: Accessibility -> Accessibility -> Accessibility
max :: Accessibility -> Accessibility -> Accessibility
$cmin :: Accessibility -> Accessibility -> Accessibility
min :: Accessibility -> Accessibility -> Accessibility
Ord, (forall x. Accessibility -> Rep Accessibility x)
-> (forall x. Rep Accessibility x -> Accessibility)
-> Generic Accessibility
forall x. Rep Accessibility x -> Accessibility
forall x. Accessibility -> Rep Accessibility x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Accessibility -> Rep Accessibility x
from :: forall x. Accessibility -> Rep Accessibility x
$cto :: forall x. Rep Accessibility x -> Accessibility
to :: forall x. Rep Accessibility x -> Accessibility
Generic)

instance Show Accessibility where
  show :: Accessibility -> String
show Accessibility
Public = String
"public export"
  show Accessibility
Frozen = String
"export"
  show Accessibility
Private = String
"private"
  show Accessibility
Hidden = String
"hidden"

type Injectivity = Bool

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

-- | 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
(Int -> PReason -> ShowS)
-> (PReason -> String) -> ([PReason] -> ShowS) -> Show PReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PReason -> ShowS
showsPrec :: Int -> PReason -> ShowS
$cshow :: PReason -> String
show :: PReason -> String
$cshowList :: [PReason] -> ShowS
showList :: [PReason] -> ShowS
Show, PReason -> PReason -> Bool
(PReason -> PReason -> Bool)
-> (PReason -> PReason -> Bool) -> Eq PReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PReason -> PReason -> Bool
== :: PReason -> PReason -> Bool
$c/= :: PReason -> PReason -> Bool
/= :: PReason -> PReason -> Bool
Eq, (forall x. PReason -> Rep PReason x)
-> (forall x. Rep PReason x -> PReason) -> Generic PReason
forall x. Rep PReason x -> PReason
forall x. PReason -> Rep PReason x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PReason -> Rep PReason x
from :: forall x. PReason -> Rep PReason x
$cto :: forall x. Rep PReason x -> PReason
to :: forall x. Rep PReason x -> PReason
Generic)

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

{-!
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
(MetaInformation -> MetaInformation -> Bool)
-> (MetaInformation -> MetaInformation -> Bool)
-> Eq MetaInformation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaInformation -> MetaInformation -> Bool
== :: MetaInformation -> MetaInformation -> Bool
$c/= :: MetaInformation -> MetaInformation -> Bool
/= :: MetaInformation -> MetaInformation -> Bool
Eq, Int -> MetaInformation -> ShowS
[MetaInformation] -> ShowS
MetaInformation -> String
(Int -> MetaInformation -> ShowS)
-> (MetaInformation -> String)
-> ([MetaInformation] -> ShowS)
-> Show MetaInformation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaInformation -> ShowS
showsPrec :: Int -> MetaInformation -> ShowS
$cshow :: MetaInformation -> String
show :: MetaInformation -> String
$cshowList :: [MetaInformation] -> ShowS
showList :: [MetaInformation] -> ShowS
Show, (forall x. MetaInformation -> Rep MetaInformation x)
-> (forall x. Rep MetaInformation x -> MetaInformation)
-> Generic MetaInformation
forall x. Rep MetaInformation x -> MetaInformation
forall x. MetaInformation -> Rep MetaInformation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaInformation -> Rep MetaInformation x
from :: forall x. MetaInformation -> Rep MetaInformation x
$cto :: forall x. Rep MetaInformation x -> MetaInformation
to :: forall x. Rep MetaInformation x -> MetaInformation
Generic)

-- | 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
(Int -> Context -> ShowS)
-> (Context -> String) -> ([Context] -> ShowS) -> Show Context
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Context -> ShowS
showsPrec :: Int -> Context -> ShowS
$cshow :: Context -> String
show :: Context -> String
$cshowList :: [Context] -> ShowS
showList :: [Context] -> ShowS
Show, (forall x. Context -> Rep Context x)
-> (forall x. Rep Context x -> Context) -> Generic Context
forall x. Rep Context x -> Context
forall x. Context -> Rep Context x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Context -> Rep Context x
from :: forall x. Context -> Rep Context x
$cto :: forall x. Rep Context x -> Context
to :: forall x. Rep Context x -> Context
Generic)

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

-- | The initial empty context
initContext :: Context
initContext = Int -> Ctxt TTDecl -> Context
MkContext Int
0 Ctxt TTDecl
forall {k} {a}. Map k a
emptyContext


mapDefCtxt :: (Def -> Def) -> Context -> Context
mapDefCtxt :: (Def -> Def) -> Context -> Context
mapDefCtxt Def -> Def
f (MkContext Int
t !Ctxt TTDecl
defs) = Int -> Ctxt TTDecl -> Context
MkContext Int
t ((TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a b. (a -> b) -> Ctxt a -> Ctxt b
mapCtxt TTDecl -> TTDecl
forall {b} {c} {d} {e} {f} {t}. (Def, b, c, d, e, f) -> t
f' Ctxt TTDecl
defs)
   where f' :: (Def, b, c, d, e, f) -> t
f' (!Def
d, b
r, c
i, d
a, e
t, f
m) = (Def, b, c, d, e, f) -> t
f' (Def -> Def
f Def
d, b
r, c
i, d
a, e
t, f
m)

-- | Get the definitions from a context
ctxtAlist :: Context -> [(Name, Def)]
ctxtAlist :: Context -> [(Name, Def)]
ctxtAlist Context
ctxt = ((Name, TTDecl) -> (Name, Def))
-> [(Name, TTDecl)] -> [(Name, Def)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) -> (Name
n, Def
d)) ([(Name, TTDecl)] -> [(Name, Def)])
-> [(Name, TTDecl)] -> [(Name, Def)]
forall a b. (a -> b) -> a -> b
$ Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Ctxt a -> [(Name, a)]
toAlist (Context -> Ctxt TTDecl
definitions Context
ctxt)

veval :: Context -> Env -> TT Name -> Value
veval Context
ctxt Env
env TT Name
t = Eval Value -> EvalState -> Value
forall s a. State s a -> s -> a
evalState (Bool
-> Context
-> [(Name, Int)]
-> Env
-> TT Name
-> [EvalOpt]
-> Eval Value
eval Bool
False Context
ctxt [] Env
env TT Name
t []) EvalState
initEval

addToCtxt :: Name -> Term -> Type -> Context -> Context
addToCtxt :: Name -> TT Name -> TT Name -> Context -> Context
addToCtxt Name
n TT Name
tm TT Name
ty Context
uctxt
    = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
          !ctxt' :: Ctxt TTDecl
ctxt' = Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (TT Name -> TT Name -> Def
Function TT Name
ty TT Name
tm, RigCount
RigW, Bool
False, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions = ctxt' }

setAccess :: Name -> Accessibility -> Context -> Context
setAccess :: Name -> Accessibility -> Context -> Context
setAccess Name
n Accessibility
a Context
uctxt
    = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
          !ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
r, Bool
i, Accessibility
_, Totality
t, MetaInformation
m) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions = ctxt' }

setInjective :: Name -> Injectivity -> Context -> Context
setInjective :: Name -> Bool -> Context -> Context
setInjective Name
n Bool
i Context
uctxt
    = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
          !ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
r, Bool
_, Accessibility
a, Totality
t, MetaInformation
m) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions = ctxt' }

setTotal :: Name -> Totality -> Context -> Context
setTotal :: Name -> Totality -> Context -> Context
setTotal Name
n Totality
t Context
uctxt
    = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
          !ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
_, MetaInformation
m) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions = ctxt' }

setRigCount :: Name -> RigCount -> Context -> Context
setRigCount :: Name -> RigCount -> Context -> Context
setRigCount Name
n RigCount
rc Context
uctxt
    = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
          !ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
_, Bool
i, Accessibility
a, Totality
t, MetaInformation
m) -> (Def
d, RigCount
rc, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions = ctxt' }

setMetaInformation :: Name -> MetaInformation -> Context -> Context
setMetaInformation :: Name -> MetaInformation -> Context -> Context
setMetaInformation Name
n MetaInformation
m Context
uctxt
    = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
          !ctxt' :: Ctxt TTDecl
ctxt' = Name -> (TTDecl -> TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef Name
n (\ (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
_) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions = ctxt' }

addCtxtDef :: Name -> Def -> Context -> Context
addCtxtDef :: Name -> Def -> Context -> Context
addCtxtDef Name
n Def
d Context
c = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
c
                       !ctxt' :: Ctxt TTDecl
ctxt' = Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (Def
d, RigCount
RigW, Bool
False, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) (Ctxt TTDecl -> Ctxt TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a b. (a -> b) -> a -> b
$! Ctxt TTDecl
ctxt in
                       Context
c { definitions = ctxt' }

addTyDecl :: Name -> NameType -> Type -> Context -> Context
addTyDecl :: Name -> NameType -> TT Name -> Context -> Context
addTyDecl Name
n NameType
nt TT Name
ty Context
uctxt
    = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
          !ctxt' :: Ctxt TTDecl
ctxt' = Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (NameType -> TT Name -> Def
TyDecl NameType
nt TT Name
ty, RigCount
RigW, Bool
False, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions = ctxt' }

addDatatype :: Datatype Name -> Context -> Context
addDatatype :: Datatype Name -> Context -> Context
addDatatype (Data Name
n Int
tag TT Name
ty Bool
unique [(Name, TT Name)]
cons) Context
uctxt
    = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
          ty' :: TT Name
ty' = Context -> Env -> TT Name -> TT Name
normalise Context
uctxt [] TT Name
ty
          !ctxt' :: Ctxt TTDecl
ctxt' = Int -> [(Name, TT Name)] -> Ctxt TTDecl -> Ctxt TTDecl
addCons Int
0 [(Name, TT Name)]
cons (Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n
                     (NameType -> TT Name -> Def
TyDecl (Int -> Int -> NameType
TCon Int
tag (TT Name -> Int
forall n. TT n -> Int
arity TT Name
ty')) TT Name
ty, RigCount
RigW, Bool
True, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt) in
          Context
uctxt { definitions = ctxt' }
  where
    addCons :: Int -> [(Name, TT Name)] -> Ctxt TTDecl -> Ctxt TTDecl
addCons Int
tag [] Ctxt TTDecl
ctxt = Ctxt TTDecl
ctxt
    addCons Int
tag ((Name
n, TT Name
ty) : [(Name, TT Name)]
cons) Ctxt TTDecl
ctxt
        = let ty' :: TT Name
ty' = Context -> Env -> TT Name -> TT Name
normalise Context
uctxt [] TT Name
ty in
              Int -> [(Name, TT Name)] -> Ctxt TTDecl -> Ctxt TTDecl
addCons (Int
tagInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [(Name, TT Name)]
cons (Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n
                  (NameType -> TT Name -> Def
TyDecl (Int -> Int -> Bool -> NameType
DCon Int
tag (TT Name -> Int
forall n. TT n -> Int
arity TT Name
ty') Bool
unique) TT Name
ty, RigCount
RigW, Bool
True, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt)

-- 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 = inlc })
                                                TT Name
ty [(TT Name, Bool)]
argtys [Either (TT Name) (TT Name, TT Name)]
ps_in [([Name], TT Name, TT Name)]
ps_ct CaseDefs
cdef,
                                 RigCount
RigW, Bool
False, Accessibility
access, Totality
Unchecked, MetaInformation
EmptyMI)
                       in Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ctxt TTDecl -> TC (Ctxt TTDecl))
-> Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a b. (a -> b) -> a -> b
$ Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n TTDecl
op Ctxt TTDecl
ctxt
--                    other -> tfail (Msg $ "Error adding case def: " ++ show other)
         Context -> TC Context
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Context
uctxt { definitions = 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 Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n Ctxt TTDecl
ctxt of
                   [(CaseOp CaseInfo
ci TT Name
ty [(TT Name, Bool)]
atys [] [([Name], TT Name, TT Name)]
ps CaseDefs
_, RigCount
rc, Bool
inj, Accessibility
acc, Totality
tot, MetaInformation
metainf)] ->
                      Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Ctxt TTDecl
ctxt -- 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' = (Either (TT Name) (TT Name, TT Name)
 -> Either (TT Name) (TT Name, TT Name))
-> [Either (TT Name) (TT Name, TT Name)]
-> [Either (TT Name) (TT Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map Either (TT Name) (TT Name, TT Name)
-> Either (TT Name) (TT Name, TT Name)
forall {a} {a}. Either a (a, TT Name) -> Either a (a, TT Name)
simpl [Either (TT Name) (TT Name, TT Name)]
ps_in
                             pdef :: [([Name], TT Name, TT Name)]
pdef = (Either (TT Name) (TT Name, TT Name) -> ([Name], TT Name, TT Name))
-> [Either (TT Name) (TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map Either (TT Name) (TT Name, TT Name) -> ([Name], TT Name, TT Name)
forall {n} {n}. Either (TT n) (TT n, TT n) -> ([n], TT n, TT n)
debind [Either (TT Name) (TT Name, TT Name)]
ps_in'
                         CaseDef [Name]
args SC
sc [TT Name]
_ <- Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(TT Name, Bool)]
-> [([Name], TT Name, TT Name)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
False (TT Name -> SC
forall t. t -> SC' t
STerm TT Name
forall n. TT n
Erased) Bool
False Phase
CompileTime FC
emptyFC [] [(TT Name, Bool)]
atys [([Name], TT Name, TT Name)]
pdef ErasureInfo
ei
                         Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ctxt TTDecl -> TC (Ctxt TTDecl))
-> Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a b. (a -> b) -> a -> b
$ Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (CaseInfo
-> TT Name
-> [(TT Name, Bool)]
-> [Either (TT Name) (TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
-> CaseDefs
-> Def
CaseOp CaseInfo
ci
                                              TT Name
ty [(TT Name, Bool)]
atys [Either (TT Name) (TT Name, TT Name)]
ps_in' [([Name], TT Name, TT Name)]
ps (CaseDefs
cd { cases_compiletime = (args, sc) }),
                                              RigCount
rc, Bool
inj, Accessibility
acc, Totality
tot, MetaInformation
metainf) Ctxt TTDecl
ctxt

                   [TTDecl]
_ -> Ctxt TTDecl -> TC (Ctxt TTDecl)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Ctxt TTDecl
ctxt
        Context -> TC Context
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Context
uctxt { definitions = ctxt' }
  where
    depat :: [n] -> TT n -> ([n], TT n)
depat [n]
acc (Bind n
n (PVar RigCount
_ TT n
t) TT n
sc)
        = [n] -> TT n -> ([n], TT n)
depat (n
n n -> [n] -> [n]
forall a. a -> [a] -> [a]
: [n]
acc) (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
instantiate (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n TT n
t) TT n
sc)
    depat [n]
acc TT n
x = ([n]
acc, TT n
x)
    debind :: Either (TT n) (TT n, TT n) -> ([n], TT n, TT n)
debind (Right (TT n
x, TT n
y)) = let ([n]
vs, TT n
x') = [n] -> TT n -> ([n], TT n)
forall {n}. [n] -> TT n -> ([n], TT n)
depat [] TT n
x
                                ([n]
_, TT n
y') = [n] -> TT n -> ([n], TT n)
forall {n}. [n] -> TT n -> ([n], TT n)
depat [] TT n
y in
                                ([n]
vs, TT n
x', TT n
y')
    debind (Left TT n
x)       = let ([n]
vs, TT n
x') = [n] -> TT n -> ([n], TT n)
forall {n}. [n] -> TT n -> ([n], TT n)
depat [] TT n
x in
                                ([n]
vs, TT n
x', TT n
forall n. TT n
Impossible)
    simpl :: Either a (a, TT Name) -> Either a (a, TT Name)
simpl (Right (a
x, TT Name
y))
         = if [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
ufnames then (a, TT Name) -> Either a (a, TT Name)
forall a b. b -> Either a b
Right (a
x, TT Name
y)
              else (a, TT Name) -> Either a (a, TT Name)
forall a b. b -> Either a b
Right (a
x, Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
unfold Context
uctxt [] ((Name -> (Name, Int)) -> [Name] -> [(Name, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, Int
1)) (TT Name -> [Name]
uns TT Name
y)) TT Name
y)
    simpl Either a (a, TT Name)
t = Either a (a, TT Name)
t

    -- 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 = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name]
inames [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
tm [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Name]]
ms
      where
        getNames :: Maybe Name -> TT Name -> [Name]
getNames Maybe Name
under fn :: TT Name
fn@(App AppStatus Name
_ TT Name
_ TT Name
_)
            | (TT Name
f, [TT Name]
args) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
fn
                 = let under' :: Maybe Name
under' = case TT Name
f of
                                     P NameType
_ Name
fn TT Name
_ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
fn
                                     TT Name
_ -> Maybe Name
forall a. Maybe a
Nothing
                                  in
                       Maybe Name -> TT Name -> [Name]
getNames Maybe Name
under TT Name
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (TT Name -> [Name]) -> [TT Name] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Maybe Name -> TT Name -> [Name]
getNames Maybe Name
under') [TT Name]
args
        getNames (Just Name
under) (P NameType
_ Name
ref TT Name
_)
            = if Name
ref Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inames then [Name
under] else []
        getNames Maybe Name
under (Bind Name
n (Let RigCount
c TT Name
t TT Name
v) TT Name
sc)
            = Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
              Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
v [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
              Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
sc
        getNames Maybe Name
under (Bind Name
n Binder (TT Name)
b TT Name
sc) = Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
                                       Maybe Name -> TT Name -> [Name]
getNames Maybe Name
forall a. Maybe a
Nothing TT Name
sc
        getNames Maybe Name
_ TT Name
_ = []

addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
               Context -> Context
addOperator :: Name
-> TT Name -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
n TT Name
ty Int
a [Value] -> Maybe Value
op Context
uctxt
    = let ctxt :: Ctxt TTDecl
ctxt = Context -> Ctxt TTDecl
definitions Context
uctxt
          ctxt' :: Ctxt TTDecl
ctxt' = Name -> TTDecl -> Ctxt TTDecl -> Ctxt TTDecl
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n (TT Name -> Int -> ([Value] -> Maybe Value) -> Def
Operator TT Name
ty Int
a [Value] -> Maybe Value
op, RigCount
RigW, Bool
False, Accessibility
Public, Totality
Unchecked, MetaInformation
EmptyMI) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions = ctxt' }

tfst :: (a, b, c, d, e, f) -> a
tfst (a
a, b
_, c
_, d
_, e
_, f
_) = a
a

lookupNames :: Name -> Context -> [Name]
lookupNames :: Name -> Context -> [Name]
lookupNames Name
n Context
ctxt
                = let ns :: [(Name, TTDecl)]
ns = Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt) in
                      ((Name, TTDecl) -> Name) -> [(Name, TTDecl)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TTDecl) -> Name
forall a b. (a, b) -> a
fst [(Name, TTDecl)]
ns

-- | 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) <- Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  TT Name
ty <- case TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst TTDecl
def of
                       (Function TT Name
ty TT Name
_) -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
                       (TyDecl NameType
_ TT Name
ty) -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
                       (Operator TT Name
ty Int
_ [Value] -> Maybe Value
_) -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
                       (CaseOp CaseInfo
_ TT Name
ty [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
_) -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
  (Name, TT Name) -> [(Name, TT Name)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
name, TT Name
ty)

-- | 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 = [(Name, TT Name)] -> Maybe (Name, TT Name)
forall a. [a] -> Maybe a
listToMaybe [ (Name
nm, TT Name
v) | (Name
nm, TT Name
v) <- Name -> Context -> [(Name, TT Name)]
lookupTyName Name
n Context
ctxt, Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n ]

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

-- | 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 = ((Name, TT Name) -> TT Name)
-> Maybe (Name, TT Name) -> Maybe (TT Name)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, TT Name) -> TT Name
forall a b. (a, b) -> b
snd (Name -> Context -> Maybe (Name, TT Name)
lookupTyNameExact Name
n Context
ctxt)

-- | 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 TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t of
            (P NameType
_ Name
n TT Name
_, [TT Name]
_) -> Name -> Context -> Bool
isConName Name
n Context
ctxt
            (Constant Const
_, [TT Name]
_) -> Bool
True
            (TT Name, [TT Name])
_ -> Bool
False

isConName :: Name -> Context -> Bool
isConName :: Name -> Context -> Bool
isConName Name
n Context
ctxt = Name -> Context -> Bool
isTConName Name
n Context
ctxt Bool -> Bool -> Bool
|| Name -> Context -> Bool
isDConName Name
n Context
ctxt

isTConName :: Name -> Context -> Bool
isTConName :: Name -> Context -> Bool
isTConName Name
n Context
ctxt
     = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
         Just (TyDecl (TCon Int
_ Int
_) TT Name
_) -> Bool
True
         Maybe Def
_                          -> Bool
False

-- | 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
     = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ do TTDecl
def <- Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
               case TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst TTDecl
def of
                 (TyDecl (DCon Int
_ Int
_ Bool
_) TT Name
_) -> Bool -> [Bool]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                 Def
_ -> Bool -> [Bool]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

isFnName :: Name -> Context -> Bool
isFnName :: Name -> Context -> Bool
isFnName Name
n Context
ctxt
     = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
         Just (Function TT Name
_ TT Name
_)       -> Bool
True
         Just (Operator TT Name
_ Int
_ [Value] -> Maybe Value
_)     -> Bool
True
         Just (CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
_) -> Bool
True
         Maybe Def
_                         -> Bool
False

isTCDict :: Name -> Context -> Bool
isTCDict :: Name -> Context -> Bool
isTCDict Name
n Context
ctxt
     = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
         Just (Function TT Name
_ TT Name
_)        -> Bool
False
         Just (Operator TT Name
_ Int
_ [Value] -> Maybe Value
_)      -> Bool
False
         Just (CaseOp CaseInfo
ci TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
_) -> CaseInfo -> Bool
tc_dictionary CaseInfo
ci
         Maybe Def
_                          -> Bool
False

-- 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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
    guarded Name
n ap :: TT Name
ap@(App AppStatus Name
_ TT Name
_ TT Name
_)
        | (P NameType
_ Name
f TT Name
_, [TT Name]
as) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
ap,
          Name -> Context -> Bool
isConName Name
f Context
ctxt = (TT Name -> Bool) -> [TT Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> TT Name -> Bool
guarded Name
n) [TT Name]
as
    guarded Name
_ TT Name
_ = Bool
False

visibleDefinitions :: Context -> Ctxt TTDecl
visibleDefinitions :: Context -> Ctxt TTDecl
visibleDefinitions Context
ctxt =
  (Map Name TTDecl -> Bool) -> Ctxt TTDecl -> Ctxt TTDecl
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\Map Name TTDecl
m -> Map Name TTDecl -> Int
forall a. Map Name a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name TTDecl
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Ctxt TTDecl -> Ctxt TTDecl)
-> (Context -> Ctxt TTDecl) -> Context -> Ctxt TTDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Name TTDecl -> Map Name TTDecl) -> Ctxt TTDecl -> Ctxt TTDecl
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Map Name TTDecl -> Map Name TTDecl
forall {k} {a} {b} {c} {e} {f}.
Map k (a, b, c, Accessibility, e, f)
-> Map k (a, b, c, Accessibility, e, f)
onlyVisible (Ctxt TTDecl -> Ctxt TTDecl)
-> (Context -> Ctxt TTDecl) -> Context -> Ctxt TTDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Ctxt TTDecl
definitions (Context -> Ctxt TTDecl) -> Context -> Ctxt TTDecl
forall a b. (a -> b) -> a -> b
$ Context
ctxt
  where
    onlyVisible :: Map k (a, b, c, Accessibility, e, f)
-> Map k (a, b, c, Accessibility, e, f)
onlyVisible = ((a, b, c, Accessibility, e, f) -> Bool)
-> Map k (a, b, c, Accessibility, e, f)
-> Map k (a, b, c, Accessibility, e, f)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (a, b, c, Accessibility, e, f) -> Bool
forall {a} {b} {c} {e} {f}. (a, b, c, Accessibility, e, f) -> Bool
visible
    visible :: (a, b, c, Accessibility, e, f) -> Bool
visible (a
_def, b
_rigCount, c
_injectivity, Accessibility
accessibility, e
_totality, f
_metaInformation) =
      Accessibility
accessibility Accessibility -> [Accessibility] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Accessibility
Hidden, Accessibility
Private]

lookupP :: Name -> Context -> [Term]
lookupP :: Name -> Context -> [TT Name]
lookupP = Bool -> Bool -> Name -> Context -> [TT Name]
lookupP_all Bool
False Bool
False

lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
lookupP_all :: Bool -> Bool -> Name -> Context -> [TT Name]
lookupP_all Bool
all Bool
exact Name
n Context
ctxt
   = do (Name
n', TTDecl
def) <- [(Name, TTDecl)]
names
        (TT Name, Accessibility)
p <- case TTDecl
def of
          (Function TT Name
ty TT Name
tm, RigCount
_, Bool
inj, Accessibility
a, Totality
_, MetaInformation
_)      -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n' TT Name
ty, Accessibility
a)
          (TyDecl NameType
nt TT Name
ty, RigCount
_, Bool
_, Accessibility
a, Totality
_, MetaInformation
_)        -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n' TT Name
ty, Accessibility
a)
          (CaseOp CaseInfo
_ TT Name
ty [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ CaseDefs
_, RigCount
_, Bool
inj, Accessibility
a, Totality
_, MetaInformation
_) -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n' TT Name
ty, Accessibility
a)
          (Operator TT Name
ty Int
_ [Value] -> Maybe Value
_, RigCount
_, Bool
inj, Accessibility
a, Totality
_, MetaInformation
_)     -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n' TT Name
ty, Accessibility
a)
        case (TT Name, Accessibility) -> Accessibility
forall a b. (a, b) -> b
snd (TT Name, Accessibility)
p of
          Accessibility
Hidden -> if Bool
all then TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((TT Name, Accessibility) -> TT Name
forall a b. (a, b) -> a
fst (TT Name, Accessibility)
p) else []
          Accessibility
Private -> if Bool
all then TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((TT Name, Accessibility) -> TT Name
forall a b. (a, b) -> a
fst (TT Name, Accessibility)
p) else []
          Accessibility
_      -> TT Name -> [TT Name]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((TT Name, Accessibility) -> TT Name
forall a b. (a, b) -> a
fst (TT Name, Accessibility)
p)
  where
    names :: [(Name, TTDecl)]
names = let ns :: [(Name, TTDecl)]
ns = Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt) in
                if Bool
exact
                   then ((Name, TTDecl) -> Bool) -> [(Name, TTDecl)] -> [(Name, TTDecl)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n', TTDecl
d) -> Name
n' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n) [(Name, TTDecl)]
ns
                   else [(Name, TTDecl)]
ns

lookupDefExact :: Name -> Context -> Maybe Def
lookupDefExact :: Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt = TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst (TTDecl -> Def) -> Maybe TTDecl -> Maybe Def
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)

lookupDef :: Name -> Context -> [Def]
lookupDef :: Name -> Context -> [Def]
lookupDef Name
n Context
ctxt = TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst (TTDecl -> Def) -> [TTDecl] -> [Def]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)

lookupNameDef :: Name -> Context -> [(Name, Def)]
lookupNameDef :: Name -> Context -> [(Name, Def)]
lookupNameDef Name
n Context
ctxt = (TTDecl -> Def) -> [(Name, TTDecl)] -> [(Name, Def)]
forall {t} {b} {a}. (t -> b) -> [(a, t)] -> [(a, b)]
mapSnd TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst ([(Name, TTDecl)] -> [(Name, Def)])
-> [(Name, TTDecl)] -> [(Name, Def)]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  where mapSnd :: (t -> b) -> [(a, t)] -> [(a, b)]
mapSnd t -> b
f [] = []
        mapSnd t -> b
f ((a
x,t
y):[(a, t)]
xys) = (a
x, t -> b
f t
y) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: (t -> b) -> [(a, t)] -> [(a, b)]
mapSnd t -> b
f [(a, t)]
xys

lookupDefAcc :: Name -> Bool -> Context ->
                [(Def, Accessibility)]
lookupDefAcc :: Name -> Bool -> Context -> [(Def, Accessibility)]
lookupDefAcc Name
n Bool
mkpublic Context
ctxt
    = (TTDecl -> (Def, Accessibility))
-> [TTDecl] -> [(Def, Accessibility)]
forall a b. (a -> b) -> [a] -> [b]
map TTDecl -> (Def, Accessibility)
forall {a} {b} {c} {e} {f}.
(a, b, c, Accessibility, e, f) -> (a, Accessibility)
mkp ([TTDecl] -> [(Def, Accessibility)])
-> [TTDecl] -> [(Def, Accessibility)]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  -- 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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_bind" Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_pure"))
                                      then (a
d, Accessibility
Public) else (a
d, Accessibility
a)

lookupTotalAccessibility :: Name -> Context -> [(Totality,Accessibility)]
lookupTotalAccessibility :: Name -> Context -> [(Totality, Accessibility)]
lookupTotalAccessibility Name
n Context
ctxt = (TTDecl -> (Totality, Accessibility))
-> [TTDecl] -> [(Totality, Accessibility)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> (Totality, Accessibility)
forall {a} {b} {c} {b} {a} {f}. (a, b, c, b, a, f) -> (a, b)
unpack ([TTDecl] -> [(Totality, Accessibility)])
-> [TTDecl] -> [(Totality, Accessibility)]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)

  where
    unpack :: (a, b, c, b, a, f) -> (a, b)
unpack ((a
_,b
_,c
_,b
a,a
t,f
_)) = (a
t,b
a)

lookupDefAccExact :: Name -> Bool -> Context ->
                     Maybe (Def, Accessibility)
lookupDefAccExact :: Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
mkpublic Context
ctxt
    = (TTDecl -> (Def, Accessibility))
-> Maybe TTDecl -> Maybe (Def, Accessibility)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> (Def, Accessibility)
forall {a} {b} {c} {e} {f}.
(a, b, c, Accessibility, e, f) -> (a, Accessibility)
mkp (Maybe TTDecl -> Maybe (Def, Accessibility))
-> Maybe TTDecl -> Maybe (Def, Accessibility)
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  -- 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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_bind" Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"io_pure"))
                                      then (a
d, Accessibility
Public) else (a
d, Accessibility
a)

lookupTotal :: Name -> Context -> [Totality]
lookupTotal :: Name -> Context -> [Totality]
lookupTotal Name
n Context
ctxt = (TTDecl -> Totality) -> [TTDecl] -> [Totality]
forall a b. (a -> b) -> [a] -> [b]
map TTDecl -> Totality
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> e
mkt ([TTDecl] -> [Totality]) -> [TTDecl] -> [Totality]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  where mkt :: (a, b, c, d, e, f) -> e
mkt (a
d, b
_, c
inj, d
a, e
t, f
m) = e
t

lookupTotalExact :: Name -> Context -> Maybe Totality
lookupTotalExact :: Name -> Context -> Maybe Totality
lookupTotalExact Name
n Context
ctxt = (TTDecl -> Totality) -> Maybe TTDecl -> Maybe Totality
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> Totality
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> e
mkt (Maybe TTDecl -> Maybe Totality) -> Maybe TTDecl -> Maybe Totality
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  where mkt :: (a, b, c, d, e, f) -> e
mkt (a
d, b
_, c
inj, d
a, e
t, f
m) = e
t

lookupRigCount :: Name -> Context -> [Totality]
lookupRigCount :: Name -> Context -> [Totality]
lookupRigCount Name
n Context
ctxt = (TTDecl -> Totality) -> [TTDecl] -> [Totality]
forall a b. (a -> b) -> [a] -> [b]
map TTDecl -> Totality
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> e
mkt ([TTDecl] -> [Totality]) -> [TTDecl] -> [Totality]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  where mkt :: (a, b, c, d, e, f) -> e
mkt (a
d, b
_, c
inj, d
a, e
t, f
m) = e
t

lookupRigCountExact :: Name -> Context -> Maybe RigCount
lookupRigCountExact :: Name -> Context -> Maybe RigCount
lookupRigCountExact Name
n Context
ctxt = (TTDecl -> RigCount) -> Maybe TTDecl -> Maybe RigCount
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> RigCount
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> b
mkt (Maybe TTDecl -> Maybe RigCount) -> Maybe TTDecl -> Maybe RigCount
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  where mkt :: (a, b, c, d, e, f) -> b
mkt (a
d, b
rc, c
inj, d
a, e
t, f
m) = b
rc

lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
lookupInjectiveExact :: Name -> Context -> Maybe Bool
lookupInjectiveExact Name
n Context
ctxt = (TTDecl -> Bool) -> Maybe TTDecl -> Maybe Bool
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TTDecl -> Bool
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> c
mkt (Maybe TTDecl -> Maybe Bool) -> Maybe TTDecl -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  where mkt :: (a, b, c, d, e, f) -> c
mkt (a
d, b
_, c
inj, d
a, e
t, f
m) = c
inj

-- 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 (TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
forall n. TT n
Erased) TT Name
sc)
    checkArgs (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
sc)
          = TT Name -> TC ()
checkArgs (TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
forall n. TT n
Erased) TT Name
sc)
    checkArgs TT Name
_ = () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

linearCheckArg :: Context -> Type -> TC ()
linearCheckArg :: Context -> TT Name -> TC ()
linearCheckArg Context
ctxt TT Name
ty = (Name -> TC ()) -> [Name] -> TC ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> TC ()
checkNameOK (TT Name -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames TT Name
ty)
  where
    checkNameOK :: Name -> TC ()
checkNameOK Name
f
       = case Name -> Context -> Maybe RigCount
lookupRigCountExact Name
f Context
ctxt of
              Just RigCount
Rig1 ->
                  Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> Err -> TC ()
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> String -> Err
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" can only appear in a linear binding"
              Maybe RigCount
_ -> () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- 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 = (TTDecl -> MetaInformation) -> [TTDecl] -> [MetaInformation]
forall a b. (a -> b) -> [a] -> [b]
map TTDecl -> MetaInformation
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> f
mkm ([TTDecl] -> [MetaInformation]) -> [TTDecl] -> [MetaInformation]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
  where mkm :: (a, b, c, d, e, f) -> f
mkm (a
d, b
_, c
inj, d
a, e
t, f
m) = f
m

lookupNameTotal :: Name -> Context -> [(Name, Totality)]
lookupNameTotal :: Name -> Context -> [(Name, Totality)]
lookupNameTotal Name
n = ((Name, TTDecl) -> (Name, Totality))
-> [(Name, TTDecl)] -> [(Name, Totality)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, (Def
_, RigCount
_, Bool
_, Accessibility
_, Totality
t, MetaInformation
_)) -> (Name
n, Totality
t)) ([(Name, TTDecl)] -> [(Name, Totality)])
-> (Context -> [(Name, TTDecl)]) -> Context -> [(Name, Totality)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Ctxt TTDecl -> [(Name, TTDecl)])
-> (Context -> Ctxt TTDecl) -> Context -> [(Name, TTDecl)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Ctxt TTDecl
definitions


lookupVal :: Name -> Context -> [Value]
lookupVal :: Name -> Context -> [Value]
lookupVal Name
n Context
ctxt
   = do TTDecl
def <- Name -> Ctxt TTDecl -> [TTDecl]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (Context -> Ctxt TTDecl
definitions Context
ctxt)
        case TTDecl -> Def
forall {a} {b} {c} {d} {e} {f}. (a, b, c, d, e, f) -> a
tfst TTDecl
def of
          (Function TT Name
_ TT Name
htm) -> Value -> [Value]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Context -> Env -> TT Name -> Value
veval Context
ctxt [] TT Name
htm)
          (TyDecl NameType
nt TT Name
ty) -> Value -> [Value]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> Value -> Value
VP NameType
nt Name
n (Context -> Env -> TT Name -> Value
veval Context
ctxt [] TT Name
ty))
          Def
_ -> []

lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, Type)
lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, TT Name)
lookupTyEnv Name
n Env
env = Name -> Int -> Env -> Maybe (Int, RigCount, TT Name)
forall {t} {t} {b} {c}.
(Eq t, Num t) =>
t -> t -> [(t, b, Binder c)] -> Maybe (t, b, c)
li Name
n Int
0 Env
env where
  li :: t -> t -> [(t, b, Binder c)] -> Maybe (t, b, c)
li t
n t
i []           = Maybe (t, b, c)
forall a. Maybe a
Nothing
  li t
n t
i ((t
x, b
r, Binder c
b): [(t, b, Binder c)]
xs)
             | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
x = (t, b, c) -> Maybe (t, b, c)
forall a. a -> Maybe a
Just (t
i, b
r, Binder c -> c
forall b. Binder b -> b
binderTy Binder c
b)
             | Bool
otherwise = t -> t -> [(t, b, Binder c)] -> Maybe (t, b, c)
li t
n (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1) [(t, b, Binder c)]
xs

-- | 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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs = Context -> Name -> [Name] -> Name
uniqueNameCtxt Context
ctxt (Name -> Name
nextName Name
n) [Name]
hs
    | [TT Name
_] <- Name -> Context -> [TT Name]
lookupTy Name
n Context
ctxt = Context -> Name -> [Name] -> Name
uniqueNameCtxt Context
ctxt (Name -> Name
nextName Name
n) [Name]
hs
    | Bool
otherwise = Name
n

uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt [Name]
ns (Bind Name
n Binder (TT Name)
b TT Name
sc)
    = let n' :: Name
n' = Context -> Name -> [Name] -> Name
uniqueNameCtxt Context
ctxt Name
n [Name]
ns in
          Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' ((TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt (Name
n'Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns)) Binder (TT Name)
b) (Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt [Name]
ns TT Name
sc)
uniqueBindersCtxt Context
ctxt [Name]
ns (App AppStatus Name
s TT Name
f TT Name
a) = AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt [Name]
ns TT Name
f) (Context -> [Name] -> TT Name -> TT Name
uniqueBindersCtxt Context
ctxt [Name]
ns TT Name
a)
uniqueBindersCtxt Context
ctxt [Name]
ns TT Name
t = TT Name
t