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

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,
             MultiParamTypeClasses, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}

module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
                normaliseAll, normaliseBlocking, toValue, quoteTerm,
                rt_simplify, simplify, inlineSmall,
                specialise, unfold, convEq, convEq',
                Def(..), CaseInfo(..), CaseDefs(..),
                Accessibility(..), Injectivity, Totality(..), TTDecl, PReason(..), MetaInformation(..),
                Context, initContext, ctxtAlist, next_tvar,
                addToCtxt, setAccess, setInjective, setTotal, setRigCount,
                setMetaInformation, addCtxtDef, addTyDecl,
                addDatatype, addCasedef, simplifyCasedef, addOperator,
                lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
                lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
                mapDefCtxt, tcReducible,
                lookupTotalAccessibility,
                lookupTotal, lookupTotalExact, lookupInjectiveExact,
                lookupRigCount, lookupRigCountExact,
                lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
                isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
                conGuarded,
                Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
                visibleDefinitions,
                isUniverse, linearCheck, linearCheckArg) where

import Idris.Core.CaseTree
import Idris.Core.TT

import Control.Monad.State
import Data.List
import Data.Maybe (listToMaybe)
import GHC.Generics (Generic)

import qualified Data.Map.Strict as Map

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

type Eval a = State EvalState a

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

initEval :: EvalState
initEval = [(Name, Int)] -> Int -> Bool -> EvalState
ES [] 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 _ _ _) _ _) = Bool
True
canonical (VP (TCon _ _) _ _) = Bool
True
canonical (VApp f :: Value
f a :: Value
a) = Value -> Bool
canonical Value
f
canonical (VConstant _) = Bool
True
canonical (VType _) = Bool
True
canonical (VUType _) = Bool
True
canonical VErased = Bool
True
canonical _ = Bool
False


instance Show Value where
    show :: Value -> String
show x :: 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 100 Value
x) EvalState
initEval

instance Show (a -> b) where
    show :: (a -> b) -> String
show x :: a -> b
x = "<<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 ctxt :: Context
ctxt env :: Env
env t :: 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 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 ctxt :: Context
ctxt env :: Env
env t :: 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 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 ctxt :: Context
ctxt env :: Env
env blocked :: [Name]
blocked t :: 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 (\n :: Name
n -> (Name
n, 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 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 tr :: Bool
tr ctxt :: Context
ctxt env :: Env
env t :: 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 0 Value
val) EvalState
initEval

toValue :: Context -> Env -> TT Name -> Value
toValue :: Context -> Env -> TT Name -> Value
toValue ctxt :: Context
ctxt env :: Env
env t :: 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 val :: 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 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 ctxt :: Context
ctxt env :: Env
env limits :: [(Name, Int)]
limits t :: TT Name
t
   = let (tm :: TT Name
tm, st :: 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 0 Value
val) (EvalState
initEval { limited :: [(Name, Int)]
limited = [(Name, Int)]
limits }) in
         (TT Name
tm, EvalState -> [(Name, Int)]
limited EvalState
st)

-- | Like normalise, but we only reduce functions that are marked as okay to
-- inline, and lets
simplify :: Context -> Env -> TT Name -> TT Name
simplify :: Context -> Env -> TT Name -> TT Name
simplify ctxt :: Context
ctxt env :: Env
env t :: 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 "lazy", 0),
                                           (String -> Name
sUN "force", 0),
                                           (String -> Name
sUN "Force", 0),
                                           (String -> Name
sUN "assert_smaller", 0),
                                           (String -> Name
sUN "assert_total", 0),
                                           (String -> Name
sUN "par", 0),
                                           (String -> Name
sUN "prim__syntactic_eq", 0),
                                           (String -> Name
sUN "fork", 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 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 ctxt :: Context
ctxt env :: Env
env t :: 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 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 ctxt :: Context
ctxt env :: Env
env t :: 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 "lazy", 0),
                                           (String -> Name
sUN "force", 0),
                                           (String -> Name
sUN "Force", 0),
                                           (String -> Name
sUN "par", 0),
                                           (String -> Name
sUN "prim__syntactic_eq", 0),
                                           (String -> Name
sUN "prim_fork", 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 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 ctxt :: Context
ctxt env :: Env
env ns :: [(Name, Int)]
ns t :: 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 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 (n :: Name
n, r :: RigCount
r, b :: Binder (TT Name)
b) = (Name
n, RigCount
r, (TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
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 False uf :: Bool
uf depthlimit :: Int
depthlimit n :: Name
n [] = (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [])
usable True uf :: Bool
uf depthlimit :: Int
depthlimit n :: Name
n ns :: [(Name, Int)]
ns
  = do ES ls :: [(Name, Int)]
ls num :: Int
num b :: 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 (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 0 -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
                    Just i :: Int
i -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [(Name, Int)]
ns)
                    _ -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
usable False uf :: Bool
uf depthlimit :: Int
depthlimit n :: Name
n ns :: [(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 0 -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [(Name, Int)]
ns)
         Just i :: Int
i -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
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
-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 (\ (n' :: Name
n', _) -> Name
nName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ns)
         _ -> (Bool, [(Name, Int)]) -> Eval (Bool, [(Name, Int)])
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 (\ (n' :: Name
n', _) -> 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 inc :: Int
inc n :: Name
n
         = do ES ls :: [(Name, Int)]
ls num :: Int
num b :: 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 i :: 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 (\ (n' :: Name
n', _) -> Name
nName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n') [(Name, Int)]
ls) Int
num Bool
b
                  _ -> () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

setBlock :: Bool -> Eval ()
setBlock :: Bool -> Eval ()
setBlock b :: Bool
b = do ES ls :: [(Name, Int)]
ls num :: Int
num _ <- 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 1
reinstate :: Name -> Eval ()
reinstate = Int -> Name -> Eval ()
fnCount (-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 traceon :: Bool
traceon ctxt :: Context
ctxt ntimes :: [(Name, Int)]
ntimes genv :: Env
genv tm :: TT Name
tm opts :: [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 (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 (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 (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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
    runtime :: Bool
runtime = EvalOpt
RunTT EvalOpt -> [EvalOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
    atRepl :: Bool
atRepl = EvalOpt
AtREPL EvalOpt -> [EvalOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [EvalOpt]
opts
    unfold :: Bool
unfold = EvalOpt
Unfold EvalOpt -> [EvalOpt] -> 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 inl :: Bool
inl always :: Bool
always dict :: Bool
dict) n :: Name
n stk :: 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 (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 (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 "prim__syntactic_eq")
       | Bool
otherwise = Bool
False

    getCases :: CaseDefs -> ([Name], SC)
getCases cd :: 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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (P _ n :: Name
n ty :: TT Name
ty)
        | Just (Let _ t :: TT Name
t v :: 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 ntimes_in :: [(Name, Int)]
ntimes_in stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (P Ref n :: Name
n ty :: TT Name
ty)
         = do let limit :: Int
limit = if Bool
simpl then 100 else 10000
              (u :: Bool
u, ntimes :: [(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 "assert_total" Name -> [Name] -> 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 _ tm :: TT Name
tm, 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 nt :: NameType
nt ty :: TT Name
ty, _) -> 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 (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 ci :: CaseInfo
ci _ _ _ _ cd :: CaseDefs
cd, acc :: 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 (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 (ns :: [Name]
ns, tree :: 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
                                        (Nothing, _) -> (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 v :: Value
v, _)  -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
                    _ -> (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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (P nt :: NameType
nt n :: Name
n ty :: 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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (V i :: Int
i)
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Value)] -> 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
>= 0 = Value -> Eval Value
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. [a] -> Int -> a
!! Int
i)
        | Bool
otherwise      = Value -> Eval Value
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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (Bind n :: Name
n (Let c :: RigCount
c t :: TT Name
t v :: TT Name
v) sc :: 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
< 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 (-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 :: Int
nexthole = Int
vd Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 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 "vlet") Value
VErased) (Name, Value) -> [(Name, Value)] -> [(Name, Value)]
forall a. a -> [a] -> [a]
: [(Name, Value)]
env) TT Name
sc
                Value -> Eval Value
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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (Bind n :: Name
n (NLet t :: TT Name
t v :: TT Name
v) sc :: 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 (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') (\x :: Value
x -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
sc')
    ev ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (Bind n :: Name
n b :: Binder (TT Name)
b sc :: 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 (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' (\x :: 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 env :: [(Name, Value)]
env t :: 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 (\tm :: 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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env
              (App _ (App _ (App _ d :: TT Name
d@(P _ (UN dly :: Text
dly) _) l :: TT Name
l@(P _ (UN lco :: Text
lco) _)) t :: TT Name
t) arg :: TT Name
arg)
       | Text
dly Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Delay" Bool -> Bool -> Bool
&& Text
lco Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Infinite" Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
unfold Bool -> Bool -> Bool
|| Bool
simpl)
            = do let (f :: TT Name
f, _) = 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 _ fn :: Name
fn _ -> (Name
fn, 0) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
: [(Name, Int)]
ntimes
                                    _ -> [(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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (App _ (App _ (P _ n :: Name
n@(UN at :: Text
at) _) _) arg :: TT Name
arg)
       | Just (CaseOp _ _ _ _ _ _, _) <- 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 "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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (App _ f :: TT Name
f a :: 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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (Proj t :: TT Name
t i :: 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 (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 t' :: Value
t' (VP (DCon _ _ _) _ _, args :: [Value]
args)
                  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Value] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
args = [Value]
args[Value] -> Int -> Value
forall a. [a] -> Int -> a
!!Int
i
             doProj t' :: Value
t' _ = Value -> Int -> Value
VProj Value
t' Int
i

    ev ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (Constant c :: Const
c) = Value -> Eval Value
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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env Erased    = Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
VErased
    ev ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env Impossible  = Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
VImpossible
    ev ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (Inferred tm :: 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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (TType i :: UExp
i)   = Value -> Eval Value
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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (UType u :: Universe
u)   = Value -> Eval Value
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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env args :: [Value]
args (VApp f :: Value
f a :: 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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env args :: [Value]
args f :: 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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env (VBind True n :: Name
n (Lam _ t :: Value
t) sc :: Value -> Eval Value
sc) (a :: Value
a:as :: [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 1 Value
app
    apply ntimes_in :: [(Name, Int)]
ntimes_in stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env f :: Value
f@(VP Ref n :: Name
n ty :: Value
ty) args :: [Value]
args
         = do let limit :: Int
limit = if Bool
simpl then 100 else 10000
              (u :: Bool
u, ntimes :: [(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 "assert_total" Name -> [Name] -> 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 ci :: CaseInfo
ci _ _ _ _ cd :: CaseDefs
cd, acc :: 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 (ns :: [Name]
ns, tree :: 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 (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
                                      (Nothing, _) -> Value -> Eval Value
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 v :: Value
v, rest :: [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 _ i :: Int
i op :: [Value] -> Maybe Value
op, _)  ->
                        if (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Value] -> 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
                              Nothing -> Value -> Eval Value
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 v :: 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 (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
                      _ -> case [Value]
args of
                              [] -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
f
                              _ -> Value -> Eval Value
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
                           (a :: Value
a : as :: [Value]
as) -> Value -> Eval Value
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 (m :: * -> *) a. Monad m => a -> m a
return Value
f
    apply ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env f :: Value
f (a :: Value
a:as :: [Value]
as) = Value -> Eval Value
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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env f :: Value
f []     = Value -> Eval Value
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 env :: [(Name, Value)]
env f :: Value
f [] = Value
f
    unload env :: [(Name, Value)]
env f :: Value
f (a :: Value
a:as :: [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 ntimes :: [(Name, Int)]
ntimes n :: Name
n stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env ns :: [Name]
ns args :: [Value]
args tree :: SC
tree
        | [Name] -> 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 (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 (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 (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
                                   Nothing -> Name -> Eval ()
reinstate Name
n -- Blocked, count n again
                                   Just _ -> () -> Eval ()
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 (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 (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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env amap :: [(Name, Value)]
amap (UnmatchedCase str :: String
str) = Maybe Value -> Eval (Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing
    evTree ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env amap :: [(Name, Value)]
amap (STerm tm :: 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 (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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env amap :: [(Name, Value)]
amap (ProjCase t :: TT Name
t alts :: [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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env amap :: [(Name, Value)]
amap (Case _ n :: Name
n alts :: [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 v :: 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 -> Eval (Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Value
forall a. Maybe a
Nothing
    evTree ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env amap :: [(Name, Value)]
amap ImpossibleCase = Maybe Value -> Eval (Maybe Value)
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 ntimes :: [(Name, Int)]
ntimes stk :: [Name]
stk top :: Bool
top env :: [(Name, Value)]
env amap :: [(Name, Value)]
amap v :: Value
v alts :: [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 (altmap :: [(Name, Value)]
altmap, sc :: 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
                    _ -> 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 (altmap :: [(Name, Value)]
altmap, sc :: 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 Value -> Eval (Maybe Value)
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 _ _ _)
        | (P (DCon _ _ _) _ _, args :: [TT n]
args) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = Bool
True
    conHeaded t :: 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' ntimes :: [(Name, Int)]
ntimes  stk :: [Name]
stk env :: [(Name, Value)]
env _ (f :: Value
f, args :: [Value]
args) alts :: [CaseAlt' (TT Name)]
alts amap :: [(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 env :: [(Name, Value)]
env _ (VP (DCon i :: Int
i a :: Int
a _) _ _, args :: [Value]
args) alts :: [CaseAlt' (TT Name)]
alts amap :: [(Name, Value)]
amap
        | Just (ns :: [Name]
ns, sc :: 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 (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 v :: 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 (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 env :: [(Name, Value)]
env _ (VP (TCon i :: Int
i a :: Int
a) _ _, args :: [Value]
args) alts :: [CaseAlt' (TT Name)]
alts amap :: [(Name, Value)]
amap
        | Just (ns :: [Name]
ns, sc :: 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 (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 v :: 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 (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 env :: [(Name, Value)]
env _ (VConstant c :: Const
c, []) alts :: [CaseAlt' (TT Name)]
alts amap :: [(Name, Value)]
amap
        | Just v :: 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 (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 (n' :: Name
n', sub :: Value
sub, sc :: 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 (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 v :: 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 (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 env :: [(Name, Value)]
env _ (VP _ n :: Name
n _, args :: [Value]
args) alts :: [CaseAlt' (TT Name)]
alts amap :: [(Name, Value)]
amap
        | Just (ns :: [Name]
ns, sc :: 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 (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 env :: [(Name, Value)]
env _ (VBind _ _ (Pi _ i :: Maybe ImplicitInfo
i s :: Value
s k :: Value
k) t :: Value -> Eval Value
t, []) alts :: [CaseAlt' (TT Name)]
alts amap :: [(Name, Value)]
amap
        | Just (ns :: [Name]
ns, sc :: SC
sc) <- Name -> [CaseAlt' (TT Name)] -> Maybe ([Name], SC)
forall t. Name -> [CaseAlt' t] -> Maybe ([Name], SC' t)
findFn (String -> Name
sUN "->") [CaseAlt' (TT Name)]
alts
           = do Value
t' <- Value -> Eval Value
t (Int -> Value
VV 0) -- we know it's not in scope or it's not a pattern
                Maybe ([(Name, Value)], SC) -> Eval (Maybe ([(Name, Value)], SC))
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 _ _ _ alts :: [CaseAlt' (TT Name)]
alts amap :: [(Name, Value)]
amap
        | Just v :: 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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(Name, Value)], SC)
forall a. Maybe a
Nothing

    fnCase :: CaseAlt' t -> Bool
fnCase (FnCase _ _ _) = Bool
True
    fnCase _ = 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 newm :: [(a, b)]
newm amap :: [(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 (\ (x :: a
x, _) -> Bool -> Bool
not (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 i :: Int
i [] = Maybe ([Name], SC' t)
forall a. Maybe a
Nothing
    findTag i :: Int
i (ConCase n :: Name
n j :: Int
j ns :: [Name]
ns sc :: SC' t
sc : xs :: [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 i :: Int
i (_ : xs :: [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 fn :: Name
fn [] = Maybe ([Name], SC' t)
forall a. Maybe a
Nothing
    findFn fn :: Name
fn (FnCase n :: Name
n ns :: [Name]
ns sc :: SC' t
sc : xs :: [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 fn :: Name
fn (_ : xs :: [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 :: SC' t
sc : xs :: [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
sc
    findDefault (_ : xs :: [CaseAlt' t]
xs) = [CaseAlt' t] -> Maybe (SC' t)
findDefault [CaseAlt' t]
xs

    findSuc :: Const -> [CaseAlt' t] -> Maybe (Name, Value, SC' t)
findSuc c :: Const
c [] = Maybe (Name, Value, SC' t)
forall a. Maybe a
Nothing
    findSuc (BI val :: Integer
val) (SucCase n :: Name
n sc :: SC' t
sc : _)
         | Integer
val Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 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
- 1)), SC' t
sc)
    findSuc c :: Const
c (_ : xs :: [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 c :: Const
c [] = Maybe (SC' t)
forall a. Maybe a
Nothing
    findConst c :: Const
c (ConstCase c' :: Const
c' v :: SC' t
v : xs :: [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 ITNative)) (ConCase n :: Name
n 1 [] v :: SC' t
v : xs :: [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType ATFloat) (ConCase n :: Name
n 2 [] v :: SC' t
v : xs :: [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt ITChar))  (ConCase n :: Name
n 3 [] v :: SC' t
v : xs :: [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst StrType (ConCase n :: Name
n 4 [] v :: SC' t
v : xs :: [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt ITBig)) (ConCase n :: Name
n 6 [] v :: SC' t
v : xs :: [CaseAlt' t]
xs) = SC' t -> Maybe (SC' t)
forall a. a -> Maybe a
Just SC' t
v
    findConst (AType (ATInt (ITFixed ity :: NativeTy
ity))) (ConCase n :: Name
n tag :: Int
tag [] v :: SC' t
v : xs :: [CaseAlt' t]
xs)
        | Int
tag Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 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 c :: Const
c (_ : xs :: [CaseAlt' t]
xs) = Const -> [CaseAlt' t] -> Maybe (SC' t)
findConst Const
c [CaseAlt' t]
xs

    getValArgs :: Value -> (Value, [Value])
getValArgs tm :: Value
tm = Value -> [Value] -> (Value, [Value])
getValArgs' Value
tm []
    getValArgs' :: Value -> [Value] -> (Value, [Value])
getValArgs' (VApp f :: Value
f a :: Value
a) as :: [Value]
as = Value -> [Value] -> (Value, [Value])
getValArgs' Value
f (Value
aValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
as)
    getValArgs' f :: Value
f as :: [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
(==) x :: Value
x y :: 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 v :: 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 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 i :: Int
i (VP nt :: NameType
nt n :: Name
n v :: 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 i :: Int
i (VV x :: Int
x)           = TT Name -> State EvalState (TT Name)
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 i :: Int
i (VBind _ n :: Name
n b :: Binder Value
b sc :: 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
+1) Value
sc')
       where quoteB :: Binder a -> StateT EvalState Identity (Binder (TT Name))
quoteB t :: 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 i :: Int
i (VBLet c :: RigCount
c vd :: Int
vd n :: Name
n t :: Value
t v :: Value
v sc :: 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 "vlet") (TT Name -> TT Name
forall n. TT n -> TT n
addBinder TT Name
sc')
                                TT Name -> State EvalState (TT Name)
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 i :: Int
i (VApp f :: Value
f a :: 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 i :: Int
i (VType u :: UExp
u)      = TT Name -> State EvalState (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> TT Name
forall n. UExp -> TT n
TType UExp
u)
    quote i :: Int
i (VUType u :: Universe
u)     = TT Name -> State EvalState (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe -> TT Name
forall n. Universe -> TT n
UType Universe
u)
    quote i :: Int
i VErased        = TT Name -> State EvalState (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Erased
    quote i :: Int
i VImpossible    = TT Name -> State EvalState (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Impossible
    quote i :: Int
i (VProj v :: Value
v j :: 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 (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 i :: Int
i (VConstant c :: Const
c)  = TT Name -> State EvalState (TT Name)
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 i :: Int
i (VTmp x :: Int
x)       = TT Name -> State EvalState (TT Name)
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
- 1)

wknV :: Int -> Value -> Eval Value
wknV :: Int -> Value -> Eval Value
wknV i :: Int
i (VV x :: Int
x) | Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
i = Value -> Eval Value
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
- 1)
wknV i :: Int
i (VBind red :: Bool
red n :: Name
n b :: Binder Value
b sc :: 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 (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' (\x :: 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
+ 1) Value
x')
wknV i :: Int
i (VApp f :: Value
f a :: 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 i :: Int
i t :: Value
t              = Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
t

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

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

convEq' :: Context -> [Name] -> TT Name -> TT Name -> TC Bool
convEq' ctxt :: Context
ctxt hs :: [Name]
hs x :: TT Name
x y :: 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) (0, [])

convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq ctxt :: Context
ctxt holes :: [Name]
holes topx :: TT Name
topx topy :: 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 ps :: [(Name, Name)]
ps (P xt :: NameType
xt x :: Name
x _) (P yt :: NameType
yt y :: Name
y _)
        | Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes = Bool -> StateT UCs TC Bool
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 (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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, Name)]
ps = Bool -> StateT UCs TC Bool
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 ps :: [(Name, Name)]
ps (Bind n :: Name
n (PVar _ t :: TT Name
t) sc :: TT Name
sc) y :: TT Name
y = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
sc TT Name
y
    ceq ps :: [(Name, Name)]
ps x :: TT Name
x (Bind n :: Name
n (PVar _ t :: TT Name
t) sc :: TT Name
sc) = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
sc
    ceq ps :: [(Name, Name)]
ps (Bind n :: Name
n (PVTy t :: TT Name
t) sc :: TT Name
sc) y :: TT Name
y = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
sc TT Name
y
    ceq ps :: [(Name, Name)]
ps x :: TT Name
x (Bind n :: Name
n (PVTy t :: TT Name
t) sc :: TT Name
sc) = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
sc

    ceq ps :: [(Name, Name)]
ps (V x :: Int
x)      (V y :: Int
y)      = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y)
    ceq ps :: [(Name, Name)]
ps (V x :: Int
x)      (P _ y :: Name
y _)
        | Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& [(Name, Name)] -> 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 (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. [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 (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    ceq ps :: [(Name, Name)]
ps (P _ x :: Name
x _)  (V y :: Int
y)
        | Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& [(Name, Name)] -> 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 (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. [a] -> Int -> a
!!Int
y))
        | Bool
otherwise = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    ceq ps :: [(Name, Name)]
ps (Bind n :: Name
n xb :: Binder (TT Name)
xb xs :: TT Name
xs) (Bind n' :: Name
n' yb :: Binder (TT Name)
yb ys :: 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 ps :: [(Name, Name)]
ps (Let c :: RigCount
c v :: TT Name
v t :: TT Name
t) (Let c' :: RigCount
c' v' :: TT Name
v' t' :: 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 ps :: [(Name, Name)]
ps (Guess v :: TT Name
v t :: TT Name
t) (Guess v' :: TT Name
v' t' :: 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 ps :: [(Name, Name)]
ps (Pi r :: RigCount
r i :: Maybe ImplicitInfo
i v :: TT Name
v t :: TT Name
t) (Pi r' :: RigCount
r' i' :: Maybe ImplicitInfo
i' v' :: TT Name
v' t' :: 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 ps :: [(Name, Name)]
ps b :: Binder (TT Name)
b 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 ps :: [(Name, Name)]
ps x :: TT Name
x (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ y :: TT Name
y (V 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 ps :: [(Name, Name)]
ps (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ x :: TT Name
x (V 0))) y :: 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 ps :: [(Name, Name)]
ps x :: TT Name
x (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ y :: TT Name
y (P Bound n' :: Name
n' _)))
        | 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 ps :: [(Name, Name)]
ps (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ x :: TT Name
x (P Bound n' :: Name
n' _))) y :: 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 ps :: [(Name, Name)]
ps x :: TT Name
x@(App _ _ _) y :: TT Name
y@(App _ _ _)
        | (P _ cx :: Name
cx _, xargs :: [TT Name]
xargs) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
x,
          (P _ cy :: Name
cy _, yargs :: [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 ps :: [(Name, Name)]
ps (App _ fx :: TT Name
fx ax :: TT Name
ax) (App _ fy :: TT Name
fy ay :: 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 ps :: [(Name, Name)]
ps (Constant x :: Const
x) (Constant y :: Const
y) = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Const
x Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
y)
    ceq ps :: [(Name, Name)]
ps (TType x :: UExp
x) (TType y :: UExp
y) | UExp
x UExp -> UExp -> Bool
forall a. Eq a => a -> a -> Bool
== UExp
y = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq ps :: [(Name, Name)]
ps (TType (UVal 0)) (TType y :: UExp
y) = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq ps :: [(Name, Name)]
ps (TType x :: UExp
x) (TType y :: UExp
y) = do (v :: Int
v, cs :: [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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq ps :: [(Name, Name)]
ps (UType AllTypes) x :: TT Name
x = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Bool
isUsableUniverse TT Name
x)
    ceq ps :: [(Name, Name)]
ps x :: TT Name
x (UType AllTypes) = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Bool
isUsableUniverse TT Name
x)
    ceq ps :: [(Name, Name)]
ps (UType u :: Universe
u) (UType v :: Universe
v) = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe
u Universe -> Universe -> Bool
forall a. Eq a => a -> a -> Bool
== Universe
v)
    ceq ps :: [(Name, Name)]
ps Erased _ = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq ps :: [(Name, Name)]
ps _ Erased = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    ceq ps :: [(Name, Name)]
ps x :: TT Name
x y :: TT Name
y = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    caseeq :: [(Name, Name)] -> SC -> SC -> StateT UCs TC Bool
caseeq ps :: [(Name, Name)]
ps (Case _ n :: Name
n cs :: [CaseAlt' (TT Name)]
cs) (Case _ n' :: Name
n' cs' :: [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 ps :: [(Name, Name)]
ps (ConCase x :: Name
x i :: Int
i as :: [Name]
as sc :: SC
sc : rest :: [CaseAlt' (TT Name)]
rest) (ConCase x' :: Name
x' i' :: Int
i' as' :: [Name]
as' sc' :: SC
sc' : rest' :: [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 (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 ps :: [(Name, Name)]
ps (ConstCase x :: Const
x sc :: SC
sc : rest :: [CaseAlt' (TT Name)]
rest) (ConstCase x' :: Const
x' sc' :: SC
sc' : rest' :: [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 (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 ps :: [(Name, Name)]
ps (DefaultCase sc :: SC
sc : rest :: [CaseAlt' (TT Name)]
rest) (DefaultCase sc' :: SC
sc' : rest' :: [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 ps :: [(Name, Name)]
ps [] [] = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        caseeqA ps :: [(Name, Name)]
ps _ _ = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    caseeq ps :: [(Name, Name)]
ps (STerm x :: TT Name
x) (STerm y :: TT Name
y) = [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
ceq [(Name, Name)]
ps TT Name
x TT Name
y
    caseeq ps :: [(Name, Name)]
ps (UnmatchedCase _) (UnmatchedCase _) = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    caseeq ps :: [(Name, Name)]
ps _ _ = Bool -> StateT UCs TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    sameDefs :: [(Name, Name)] -> Name -> Name -> StateT UCs TC Bool
sameDefs ps :: [(Name, Name)]
ps x :: Name
x y :: Name
y = case (Name -> Context -> [Def]
lookupDef Name
x Context
ctxt, Name -> Context -> [Def]
lookupDef Name
y Context
ctxt) of
                        ([Function _ xdef :: TT Name
xdef], [Function _ ydef :: 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 _ _ _ _ _ xd :: CaseDefs
xd],
                         [CaseOp _ _ _ _ _ yd :: CaseDefs
yd])
                              -> let (_, xdef :: SC
xdef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
xd
                                     (_, ydef :: 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
                        _ -> Bool -> StateT UCs TC Bool
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 ps :: [(Name, Name)]
ps x :: Name
x y :: Name
y xargs :: [TT Name]
xargs yargs :: [TT Name]
yargs
          = case (Name -> Context -> [Def]
lookupDef Name
x Context
ctxt, Name -> Context -> [Def]
lookupDef Name
y Context
ctxt) of
                 ([Function _ xdef :: TT Name
xdef], [Function _ ydef :: 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 _ _ _ _ _ xd :: CaseDefs
xd],
                  [CaseOp _ _ _ _ _ yd :: CaseDefs
yd])
                       -> let (xin :: [Name]
xin, xdef :: SC
xdef) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
xd
                              (yin :: [Name]
yin, ydef :: 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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
yin) [TT Name]
yargs)
                                      Bool -> StateT UCs TC Bool
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)
                 _ -> Bool -> StateT UCs TC Bool
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
$cto :: forall x. Rep Def x -> Def
$cfrom :: forall x. Def -> Rep Def x
Generic
--                   [Name] SC -- Compile time case definition
--                   [Name] SC -- Run time cae definitions

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

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

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

instance Show Def where
    show :: Def -> String
show (Function ty :: TT Name
ty tm :: TT Name
tm) = "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 nt :: NameType
nt ty :: TT Name
ty) = "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 -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
ty
    show (Operator ty :: TT Name
ty _ _) = "Operator: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
ty
    show (CaseOp (CaseInfo inlc :: Bool
inlc inla :: Bool
inla inlr :: Bool
inlr) ty :: TT Name
ty atys :: [(TT Name, Bool)]
atys ps_in :: [Either (TT Name) (TT Name, TT Name)]
ps_in ps :: [([Name], TT Name, TT Name)]
ps cd :: CaseDefs
cd)
      = let (ns :: [Name]
ns, sc :: SC
sc) = CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cd
            (ns' :: [Name]
ns', sc' :: SC
sc') = CaseDefs -> ([Name], SC)
cases_runtime CaseDefs
cd in
          "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 -> 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]
++ "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                        "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 -> ShowS
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
sc String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                        "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 -> ShowS
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
sc' String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
            if Bool
inlc then "Inlinable" else "Not inlinable" String -> ShowS
forall a. [a] -> [a] -> [a]
++
            if Bool
inla then " Aggressively\n" else "\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
/= :: Accessibility -> Accessibility -> Bool
$c/= :: Accessibility -> Accessibility -> Bool
== :: Accessibility -> Accessibility -> Bool
$c== :: 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
min :: Accessibility -> Accessibility -> Accessibility
$cmin :: Accessibility -> Accessibility -> Accessibility
max :: Accessibility -> Accessibility -> Accessibility
$cmax :: Accessibility -> Accessibility -> Accessibility
>= :: Accessibility -> Accessibility -> Bool
$c>= :: Accessibility -> Accessibility -> Bool
> :: Accessibility -> Accessibility -> Bool
$c> :: Accessibility -> Accessibility -> Bool
<= :: Accessibility -> Accessibility -> Bool
$c<= :: Accessibility -> Accessibility -> Bool
< :: Accessibility -> Accessibility -> Bool
$c< :: Accessibility -> Accessibility -> Bool
compare :: Accessibility -> Accessibility -> Ordering
$ccompare :: Accessibility -> Accessibility -> Ordering
$cp1Ord :: Eq 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
$cto :: forall x. Rep Accessibility x -> Accessibility
$cfrom :: forall x. Accessibility -> Rep Accessibility x
Generic)

instance Show Accessibility where
  show :: Accessibility -> String
show Public = "public export"
  show Frozen = "export"
  show Private = "private"
  show Hidden = "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
/= :: Totality -> Totality -> Bool
$c/= :: Totality -> Totality -> Bool
== :: Totality -> Totality -> Bool
$c== :: 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
$cto :: forall x. Rep Totality x -> Totality
$cfrom :: forall x. Totality -> Rep Totality x
Generic)

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

instance Show Totality where
    show :: Totality -> String
show (Total args :: [Int]
args)= "Total" -- ++ show args ++ " decreasing arguments"
    show Productive = "Productive" -- ++ show args ++ " decreasing arguments"
    show Unchecked = "not yet checked for totality"
    show (Partial Itself) = "possibly not total as it is not well founded"
    show (Partial NotCovering) = "not total as there are missing cases"
    show (Partial NotPositive) = "not strictly positive"
    show (Partial ExternalIO) = "an external IO primitive"
    show (Partial NotProductive) = "not productive"
    show (Partial BelieveMe) = "not total due to use of believe_me in proof"
    show (Partial (Other ns :: [Name]
ns)) = "possibly not total due to: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep ", " ((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 ns :: [Name]
ns)) = "possibly not total due to recursive path " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                 String -> [String] -> String
showSep " --> " ((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 n :: Name
n)) = "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 Generated = "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
/= :: MetaInformation -> MetaInformation -> Bool
$c/= :: MetaInformation -> MetaInformation -> Bool
== :: MetaInformation -> MetaInformation -> Bool
$c== :: 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
showList :: [MetaInformation] -> ShowS
$cshowList :: [MetaInformation] -> ShowS
show :: MetaInformation -> String
$cshow :: MetaInformation -> String
showsPrec :: Int -> MetaInformation -> ShowS
$cshowsPrec :: Int -> 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
$cto :: forall x. Rep MetaInformation x -> MetaInformation
$cfrom :: forall x. MetaInformation -> Rep MetaInformation x
Generic)

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

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

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


mapDefCtxt :: (Def -> Def) -> Context -> Context
mapDefCtxt :: (Def -> Def) -> Context -> Context
mapDefCtxt f :: Def -> Def
f (MkContext t :: 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, r :: b
r, i :: c
i, a :: d
a, t :: e
t, m :: 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 ctxt :: Context
ctxt = ((Name, TTDecl) -> (Name, Def))
-> [(Name, TTDecl)] -> [(Name, Def)]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n, (d :: Def
d, r :: RigCount
r, i :: Bool
i, a :: Accessibility
a, t :: Totality
t, m :: 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 ctxt :: Context
ctxt env :: Env
env t :: 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 n :: Name
n tm :: TT Name
tm ty :: TT Name
ty uctxt :: 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 TTDecl
definitions = Ctxt TTDecl
ctxt' }

setAccess :: Name -> Accessibility -> Context -> Context
setAccess :: Name -> Accessibility -> Context -> Context
setAccess n :: Name
n a :: Accessibility
a uctxt :: 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 (\ (d :: Def
d, r :: RigCount
r, i :: Bool
i, _, t :: Totality
t, m :: MetaInformation
m) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
ctxt' }

setInjective :: Name -> Injectivity -> Context -> Context
setInjective :: Name -> Bool -> Context -> Context
setInjective n :: Name
n i :: Bool
i uctxt :: 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 (\ (d :: Def
d, r :: RigCount
r, _, a :: Accessibility
a, t :: Totality
t, m :: MetaInformation
m) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
ctxt' }

setTotal :: Name -> Totality -> Context -> Context
setTotal :: Name -> Totality -> Context -> Context
setTotal n :: Name
n t :: Totality
t uctxt :: 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 (\ (d :: Def
d, r :: RigCount
r, i :: Bool
i, a :: Accessibility
a, _, m :: MetaInformation
m) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
ctxt' }

setRigCount :: Name -> RigCount -> Context -> Context
setRigCount :: Name -> RigCount -> Context -> Context
setRigCount n :: Name
n rc :: RigCount
rc uctxt :: 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 (\ (d :: Def
d, _, i :: Bool
i, a :: Accessibility
a, t :: Totality
t, m :: MetaInformation
m) -> (Def
d, RigCount
rc, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
ctxt' }

setMetaInformation :: Name -> MetaInformation -> Context -> Context
setMetaInformation :: Name -> MetaInformation -> Context -> Context
setMetaInformation n :: Name
n m :: MetaInformation
m uctxt :: 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 (\ (d :: Def
d, r :: RigCount
r, i :: Bool
i, a :: Accessibility
a, t :: Totality
t, _) -> (Def
d, RigCount
r, Bool
i, Accessibility
a, Totality
t, MetaInformation
m)) Ctxt TTDecl
ctxt in
          Context
uctxt { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
ctxt' }

addCtxtDef :: Name -> Def -> Context -> Context
addCtxtDef :: Name -> Def -> Context -> Context
addCtxtDef n :: Name
n d :: Def
d c :: 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 TTDecl
definitions = Ctxt TTDecl
ctxt' }

addTyDecl :: Name -> NameType -> Type -> Context -> Context
addTyDecl :: Name -> NameType -> TT Name -> Context -> Context
addTyDecl n :: Name
n nt :: NameType
nt ty :: TT Name
ty uctxt :: 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 TTDecl
definitions = Ctxt TTDecl
ctxt' }

addDatatype :: Datatype Name -> Context -> Context
addDatatype :: Datatype Name -> Context -> Context
addDatatype (Data n :: Name
n tag :: Int
tag ty :: TT Name
ty unique :: Bool
unique cons :: [(Name, TT Name)]
cons) uctxt :: 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 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 TTDecl
definitions = Ctxt TTDecl
ctxt' }
  where
    addCons :: Int -> [(Name, TT Name)] -> Ctxt TTDecl -> Ctxt TTDecl
addCons tag :: Int
tag [] ctxt :: Ctxt TTDecl
ctxt = Ctxt TTDecl
ctxt
    addCons tag :: Int
tag ((n :: Name
n, ty :: TT Name
ty) : cons :: [(Name, TT Name)]
cons) ctxt :: 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
+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 n :: Name
n ei :: ErasureInfo
ei ci :: CaseInfo
ci@(CaseInfo inline :: Bool
inline alwaysInline :: Bool
alwaysInline tcdict :: Bool
tcdict)
           tcase :: Bool
tcase covering :: SC
covering reflect :: Bool
reflect asserted :: Bool
asserted argtys :: [(TT Name, Bool)]
argtys inacc :: [Int]
inacc
           ps_in :: [Either (TT Name) (TT Name, TT Name)]
ps_in ps_ct :: [([Name], TT Name, TT Name)]
ps_ct ps_rt :: [([Name], TT Name, TT Name)]
ps_rt ty :: TT Name
ty uctxt :: 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
                           [(_, acc :: Accessibility
acc)] -> Accessibility
acc
                           _ -> 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 args_ct :: [Name]
args_ct sc_ct :: SC
sc_ct _,
                     CaseDef args_rt :: [Name]
args_rt sc_rt :: SC
sc_rt _) ->
                       let inl :: Bool
inl = Bool
alwaysInline -- tcdict
                           inlc :: Bool
inlc = (Bool
inl Bool -> Bool -> Bool
|| Name -> [Name] -> SC -> Bool
small Name
n [Name]
args_rt SC
sc_rt) Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
asserted)
                           cdef :: CaseDefs
cdef = ([Name], SC) -> ([Name], SC) -> CaseDefs
CaseDefs ([Name]
args_ct, SC
sc_ct)
                                           ([Name]
args_rt, SC
sc_rt)
                           op :: TTDecl
op = (CaseInfo
-> TT Name
-> [(TT Name, Bool)]
-> [Either (TT Name) (TT Name, TT Name)]
-> [([Name], TT Name, TT Name)]
-> CaseDefs
-> Def
CaseOp (CaseInfo
ci { case_inlinable :: Bool
case_inlinable = Bool
inlc })
                                                TT Name
ty [(TT Name, Bool)]
argtys [Either (TT Name) (TT Name, TT Name)]
ps_in [([Name], TT Name, TT Name)]
ps_ct CaseDefs
cdef,
                                 RigCount
RigW, Bool
False, Accessibility
access, Totality
Unchecked, MetaInformation
EmptyMI)
                       in Ctxt TTDecl -> TC (Ctxt TTDecl)
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 (m :: * -> *) a. Monad m => a -> m a
return Context
uctxt { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
ctxt' }

-- simplify a definition by unfolding interface methods
-- We need this for totality checking, because functions which use interfaces
-- in an implementation definition themselves need to have the implementation
-- inlined or it'll be treated as a higher order function that will potentially
-- loop.
simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
simplifyCasedef n :: Name
n ufnames :: [Name]
ufnames umethss :: [[Name]]
umethss ei :: ErasureInfo
ei uctxt :: 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 ci :: CaseInfo
ci ty :: TT Name
ty atys :: [(TT Name, Bool)]
atys [] ps :: [([Name], TT Name, TT Name)]
ps _, rc :: RigCount
rc, inj :: Bool
inj, acc :: Accessibility
acc, tot :: Totality
tot, metainf :: MetaInformation
metainf)] ->
                      Ctxt TTDecl -> TC (Ctxt TTDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return Ctxt TTDecl
ctxt -- nothing to simplify (or already done...)
                   [(CaseOp ci :: CaseInfo
ci ty :: TT Name
ty atys :: [(TT Name, Bool)]
atys ps_in :: [Either (TT Name) (TT Name, TT Name)]
ps_in ps :: [([Name], TT Name, TT Name)]
ps cd :: CaseDefs
cd, rc :: RigCount
rc, inj :: Bool
inj, acc :: Accessibility
acc, tot :: Totality
tot, metainf :: 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 args :: [Name]
args sc :: SC
sc _ <- 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 (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 :: ([Name], SC)
cases_compiletime = ([Name]
args, SC
sc) }),
                                              RigCount
rc, Bool
inj, Accessibility
acc, Totality
tot, MetaInformation
metainf) Ctxt TTDecl
ctxt

                   _ -> Ctxt TTDecl -> TC (Ctxt TTDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return Ctxt TTDecl
ctxt
        Context -> TC Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
uctxt { definitions :: Ctxt TTDecl
definitions = Ctxt TTDecl
ctxt' }
  where
    depat :: [n] -> TT n -> ([n], TT n)
depat acc :: [n]
acc (Bind n :: n
n (PVar _ t :: TT n
t) sc :: 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 acc :: [n]
acc x :: TT n
x = ([n]
acc, TT n
x)
    debind :: Either (TT n) (TT n, TT n) -> ([n], TT n, TT n)
debind (Right (x :: TT n
x, y :: TT n
y)) = let (vs :: [n]
vs, x' :: TT n
x') = [n] -> TT n -> ([n], TT n)
forall n. [n] -> TT n -> ([n], TT n)
depat [] TT n
x
                                (_, y' :: 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 x :: TT n
x)       = let (vs :: [n]
vs, x' :: 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 (x :: a
x, y :: TT Name
y))
         = if [Name] -> 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 (\n :: Name
n -> (Name
n, 1)) (TT Name -> [Name]
uns TT Name
y)) TT Name
y)
    simpl t :: 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 tm :: 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 inames :: [Name]
inames ms :: [[Name]]
ms tm :: 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 under :: Maybe Name
under fn :: TT Name
fn@(App _ _ _)
            | (f :: TT Name
f, args :: [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 _ fn :: Name
fn _ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
fn
                                     _ -> 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 under :: Name
under) (P _ ref :: Name
ref _)
            = if Name
ref Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inames then [Name
under] else []
        getNames under :: Maybe Name
under (Bind n :: Name
n (Let c :: RigCount
c t :: TT Name
t v :: TT Name
v) sc :: 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 under :: Maybe Name
under (Bind n :: Name
n b :: Binder (TT Name)
b sc :: 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 _ _ = []

addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
               Context -> Context
addOperator :: Name
-> TT Name -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator n :: Name
n ty :: TT Name
ty a :: Int
a op :: [Value] -> Maybe Value
op uctxt :: 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 TTDecl
definitions = Ctxt TTDecl
ctxt' }

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

lookupNames :: Name -> Context -> [Name]
lookupNames :: Name -> Context -> [Name]
lookupNames n :: Name
n ctxt :: 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 n :: Name
n ctxt :: Context
ctxt = do
  (name :: Name
name, def :: 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 ty :: TT Name
ty _) -> TT Name -> [TT Name]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
                       (TyDecl _ ty :: TT Name
ty) -> TT Name -> [TT Name]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
                       (Operator ty :: TT Name
ty _ _) -> TT Name -> [TT Name]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
                       (CaseOp _ ty :: TT Name
ty _ _ _ _) -> TT Name -> [TT Name]
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
ty
  (Name, TT Name) -> [(Name, TT Name)]
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 n :: Name
n ctxt :: Context
ctxt = [(Name, TT Name)] -> Maybe (Name, TT Name)
forall a. [a] -> Maybe a
listToMaybe [ (Name
nm, TT Name
v) | (nm :: Name
nm, v :: 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 n :: Name
n ctxt :: 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 n :: Name
n ctxt :: Context
ctxt = ((Name, TT Name) -> TT Name)
-> Maybe (Name, TT Name) -> Maybe (TT Name)
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 t :: TT Name
t ctxt :: Context
ctxt
     = case TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t of
            (P _ n :: Name
n _, _) -> Name -> Context -> Bool
isConName Name
n Context
ctxt
            (Constant _, _) -> Bool
True
            _ -> Bool
False

isConName :: Name -> Context -> Bool
isConName :: Name -> Context -> Bool
isConName n :: Name
n ctxt :: 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 n :: Name
n ctxt :: Context
ctxt
     = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
         Just (TyDecl (TCon _ _) _) -> Bool
True
         _                          -> Bool
False

-- | Check whether a resolved name is certainly a data constructor
isDConName :: Name -> Context -> Bool
isDConName :: Name -> Context -> Bool
isDConName n :: Name
n ctxt :: Context
ctxt
     = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
         Just (TyDecl (DCon _ _ _) _) -> Bool
True
         _                            -> Bool
False

-- | Check whether any overloading of a name is a data constructor
canBeDConName :: Name -> Context -> Bool
canBeDConName :: Name -> Context -> Bool
canBeDConName n :: Name
n ctxt :: 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 _ _ _) _) -> Bool -> [Bool]
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                 _ -> Bool -> [Bool]
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

isFnName :: Name -> Context -> Bool
isFnName :: Name -> Context -> Bool
isFnName n :: Name
n ctxt :: Context
ctxt
     = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
         Just (Function _ _)       -> Bool
True
         Just (Operator _ _ _)     -> Bool
True
         Just (CaseOp _ _ _ _ _ _) -> Bool
True
         _                         -> Bool
False

isTCDict :: Name -> Context -> Bool
isTCDict :: Name -> Context -> Bool
isTCDict n :: Name
n ctxt :: Context
ctxt
     = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
         Just (Function _ _)        -> Bool
False
         Just (Operator _ _ _)      -> Bool
False
         Just (CaseOp ci :: CaseInfo
ci _ _ _ _ _) -> CaseInfo -> Bool
tc_dictionary CaseInfo
ci
         _                          -> 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 ctxt :: Context
ctxt n :: Name
n tm :: TT Name
tm = Name -> TT Name -> Bool
guarded Name
n TT Name
tm
  where
    guarded :: Name -> TT Name -> Bool
guarded n :: Name
n (P _ n' :: Name
n' _) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
    guarded n :: Name
n ap :: TT Name
ap@(App _ _ _)
        | (P _ f :: Name
f _, as :: [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 _ _ = Bool
False

visibleDefinitions :: Context -> Ctxt TTDecl
visibleDefinitions :: Context -> Ctxt TTDecl
visibleDefinitions ctxt :: Context
ctxt =
  (Map Name TTDecl -> Bool) -> Ctxt TTDecl -> Ctxt TTDecl
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\m :: Map Name TTDecl
m -> Map Name TTDecl -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name TTDecl
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 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 (_def :: a
_def, _rigCount :: b
_rigCount, _injectivity :: c
_injectivity, accessibility :: Accessibility
accessibility, _totality :: e
_totality, _metaInformation :: 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 all :: Bool
all exact :: Bool
exact n :: Name
n ctxt :: Context
ctxt
   = do (n' :: Name
n', def :: TTDecl
def) <- [(Name, TTDecl)]
names
        (TT Name, Accessibility)
p <- case TTDecl
def of
          (Function ty :: TT Name
ty tm :: TT Name
tm, _, inj :: Bool
inj, a :: Accessibility
a, _, _)      -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
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 nt :: NameType
nt ty :: TT Name
ty, _, _, a :: Accessibility
a, _, _)        -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
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 _ ty :: TT Name
ty _ _ _ _, _, inj :: Bool
inj, a :: Accessibility
a, _, _) -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
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 ty :: TT Name
ty _ _, _, inj :: Bool
inj, a :: Accessibility
a, _, _)     -> (TT Name, Accessibility) -> [(TT Name, Accessibility)]
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
          Hidden -> if Bool
all then TT Name -> [TT Name]
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 []
          Private -> if Bool
all then TT Name -> [TT Name]
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 []
          _      -> TT Name -> [TT Name]
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 (\ (n' :: Name
n', d :: 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 n :: Name
n ctxt :: 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 n :: Name
n ctxt :: 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 n :: Name
n ctxt :: 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 f :: t -> b
f [] = []
        mapSnd f :: t -> b
f ((x :: a
x,y :: t
y):xys :: [(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 n :: Name
n mkpublic :: Bool
mkpublic ctxt :: 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 (d :: a
d, _, inj :: c
inj, a :: Accessibility
a, _, _) = if Bool
mkpublic Bool -> Bool -> Bool
&& (Bool -> Bool
not (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "io_bind" Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "io_pure"))
                                      then (a
d, Accessibility
Public) else (a
d, Accessibility
a)

lookupTotalAccessibility :: Name -> Context -> [(Totality,Accessibility)]
lookupTotalAccessibility :: Name -> Context -> [(Totality, Accessibility)]
lookupTotalAccessibility n :: Name
n ctxt :: Context
ctxt = (TTDecl -> (Totality, Accessibility))
-> [TTDecl] -> [(Totality, Accessibility)]
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
a,t :: a
t,_)) = (a
t,b
a)

lookupDefAccExact :: Name -> Bool -> Context ->
                     Maybe (Def, Accessibility)
lookupDefAccExact :: Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact n :: Name
n mkpublic :: Bool
mkpublic ctxt :: Context
ctxt
    = (TTDecl -> (Def, Accessibility))
-> Maybe TTDecl -> Maybe (Def, Accessibility)
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 (d :: a
d, _, inj :: c
inj, a :: Accessibility
a, _, _) = if Bool
mkpublic Bool -> Bool -> Bool
&& (Bool -> Bool
not (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "io_bind" Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "io_pure"))
                                      then (a
d, Accessibility
Public) else (a
d, Accessibility
a)

lookupTotal :: Name -> Context -> [Totality]
lookupTotal :: Name -> Context -> [Totality]
lookupTotal n :: Name
n ctxt :: 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 (d :: a
d, _, inj :: c
inj, a :: d
a, t :: e
t, m :: f
m) = e
t

lookupTotalExact :: Name -> Context -> Maybe Totality
lookupTotalExact :: Name -> Context -> Maybe Totality
lookupTotalExact n :: Name
n ctxt :: Context
ctxt = (TTDecl -> Totality) -> Maybe TTDecl -> Maybe Totality
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 (d :: a
d, _, inj :: c
inj, a :: d
a, t :: e
t, m :: f
m) = e
t

lookupRigCount :: Name -> Context -> [Totality]
lookupRigCount :: Name -> Context -> [Totality]
lookupRigCount n :: Name
n ctxt :: 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 (d :: a
d, _, inj :: c
inj, a :: d
a, t :: e
t, m :: f
m) = e
t

lookupRigCountExact :: Name -> Context -> Maybe RigCount
lookupRigCountExact :: Name -> Context -> Maybe RigCount
lookupRigCountExact n :: Name
n ctxt :: Context
ctxt = (TTDecl -> RigCount) -> Maybe TTDecl -> Maybe RigCount
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 (d :: a
d, rc :: b
rc, inj :: c
inj, a :: d
a, t :: e
t, m :: f
m) = b
rc

lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
lookupInjectiveExact :: Name -> Context -> Maybe Bool
lookupInjectiveExact n :: Name
n ctxt :: Context
ctxt = (TTDecl -> Bool) -> Maybe TTDecl -> Maybe Bool
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 (d :: a
d, _, inj :: c
inj, a :: d
a, t :: e
t, m :: f
m) = c
inj

-- Assume type is at least in whnfArgs form
linearCheck :: Context -> Type -> TC ()
linearCheck :: Context -> TT Name -> TC ()
linearCheck ctxt :: Context
ctxt t :: TT Name
t = TT Name -> TC ()
checkArgs TT Name
t
  where
    checkArgs :: TT Name -> TC ()
checkArgs (Bind n :: Name
n (Pi RigW _ ty :: TT Name
ty _) sc :: 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 n :: Name
n (Pi _ _ _ _) sc :: 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 _ = () -> TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

linearCheckArg :: Context -> Type -> TC ()
linearCheckArg :: Context -> TT Name -> TC ()
linearCheckArg ctxt :: Context
ctxt ty :: 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 f :: Name
f
       = case Name -> Context -> Maybe RigCount
lookupRigCountExact Name
f Context
ctxt of
              Just 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]
++ " can only appear in a linear binding"
              _ -> () -> TC ()
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 n :: Name
n ctxt :: Context
ctxt = case Name -> Context -> Maybe Totality
lookupTotalExact Name
n Context
ctxt of
                          Nothing -> Bool
True
                          Just (Partial _) -> Bool
False
                          _ -> Bool
True

lookupMetaInformation :: Name -> Context -> [MetaInformation]
lookupMetaInformation :: Name -> Context -> [MetaInformation]
lookupMetaInformation n :: Name
n ctxt :: 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 (d :: a
d, _, inj :: c
inj, a :: d
a, t :: e
t, m :: f
m) = f
m

lookupNameTotal :: Name -> Context -> [(Name, Totality)]
lookupNameTotal :: Name -> Context -> [(Name, Totality)]
lookupNameTotal n :: Name
n = ((Name, TTDecl) -> (Name, Totality))
-> [(Name, TTDecl)] -> [(Name, Totality)]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n, (_, _, _, _, t :: Totality
t, _)) -> (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 n :: Name
n ctxt :: 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 _ htm :: TT Name
htm) -> Value -> [Value]
forall (m :: * -> *) a. Monad m => a -> m a
return (Context -> Env -> TT Name -> Value
veval Context
ctxt [] TT Name
htm)
          (TyDecl nt :: NameType
nt ty :: TT Name
ty) -> Value -> [Value]
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))
          _ -> []

lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, Type)
lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, TT Name)
lookupTyEnv n :: Name
n env :: 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 0 Env
env where
  li :: t -> t -> [(t, b, Binder c)] -> Maybe (t, b, c)
li n :: t
n i :: t
i []           = Maybe (t, b, c)
forall a. Maybe a
Nothing
  li n :: t
n i :: t
i ((x :: t
x, r :: b
r, b :: Binder c
b): xs :: [(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
+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 ctxt :: Context
ctxt n :: Name
n hs :: [Name]
hs
    | Name
n Name -> [Name] -> 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
    | [_] <- 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 ctxt :: Context
ctxt ns :: [Name]
ns (Bind n :: Name
n b :: Binder (TT Name)
b sc :: 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 (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 ctxt :: Context
ctxt ns :: [Name]
ns (App s :: AppStatus Name
s f :: TT Name
f a :: 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 ctxt :: Context
ctxt ns :: [Name]
ns t :: TT Name
t = TT Name
t