{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, PatternGuards, FlexibleContexts, NamedFieldPuns, DeriveFunctor, DeriveFoldable, DeriveTraversable, TupleSections #-}
module TCM where
import Prelude hiding (null)
import Control.Monad
import Control.Monad.State (StateT, get, gets, put)
import Control.Monad.Except (ExceptT, MonadError)
import Control.Monad.Reader (ReaderT, ask, asks, local)
#if !MIN_VERSION_base(4,8,0)
import Control.Applicative
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
#endif
import qualified Data.Traversable as Traversable
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Maybe as Maybe
import Abstract
import Polarity
import Value
import {-# SOURCE #-} Eval
import PrettyTCM
import TraceError
import TreeShapedOrder (TSO)
import qualified TreeShapedOrder as TSO
import Util
import Warshall
traceSig :: String -> a -> a
traceSig :: forall a. String -> a -> a
traceSig String
msg a
a = a
a
traceRew :: String -> a -> a
traceRew :: forall a. String -> a -> a
traceRew String
msg a
a = a
a
traceRewM :: Monad m => String -> m ()
traceRewM :: forall (m :: * -> *). Monad m => String -> m ()
traceRewM String
msg = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
traceMeta :: String -> a -> a
traceMeta :: forall a. String -> a -> a
traceMeta String
msg a
a = a
a
traceMetaM :: Monad m => String -> m ()
traceMetaM :: forall (m :: * -> *). Monad m => String -> m ()
traceMetaM String
msg = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
class (MonadCxt m, MonadSig m, MonadMeta m, MonadError TraceError m) =>
MonadTCM m where
data OneOrTwo a = One a | Two a a deriving (OneOrTwo a -> OneOrTwo a -> Bool
(OneOrTwo a -> OneOrTwo a -> Bool)
-> (OneOrTwo a -> OneOrTwo a -> Bool) -> Eq (OneOrTwo a)
forall a. Eq a => OneOrTwo a -> OneOrTwo a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => OneOrTwo a -> OneOrTwo a -> Bool
== :: OneOrTwo a -> OneOrTwo a -> Bool
$c/= :: forall a. Eq a => OneOrTwo a -> OneOrTwo a -> Bool
/= :: OneOrTwo a -> OneOrTwo a -> Bool
Eq, Eq (OneOrTwo a)
Eq (OneOrTwo a) =>
(OneOrTwo a -> OneOrTwo a -> Ordering)
-> (OneOrTwo a -> OneOrTwo a -> Bool)
-> (OneOrTwo a -> OneOrTwo a -> Bool)
-> (OneOrTwo a -> OneOrTwo a -> Bool)
-> (OneOrTwo a -> OneOrTwo a -> Bool)
-> (OneOrTwo a -> OneOrTwo a -> OneOrTwo a)
-> (OneOrTwo a -> OneOrTwo a -> OneOrTwo a)
-> Ord (OneOrTwo a)
OneOrTwo a -> OneOrTwo a -> Bool
OneOrTwo a -> OneOrTwo a -> Ordering
OneOrTwo a -> OneOrTwo a -> OneOrTwo a
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
forall a. Ord a => Eq (OneOrTwo a)
forall a. Ord a => OneOrTwo a -> OneOrTwo a -> Bool
forall a. Ord a => OneOrTwo a -> OneOrTwo a -> Ordering
forall a. Ord a => OneOrTwo a -> OneOrTwo a -> OneOrTwo a
$ccompare :: forall a. Ord a => OneOrTwo a -> OneOrTwo a -> Ordering
compare :: OneOrTwo a -> OneOrTwo a -> Ordering
$c< :: forall a. Ord a => OneOrTwo a -> OneOrTwo a -> Bool
< :: OneOrTwo a -> OneOrTwo a -> Bool
$c<= :: forall a. Ord a => OneOrTwo a -> OneOrTwo a -> Bool
<= :: OneOrTwo a -> OneOrTwo a -> Bool
$c> :: forall a. Ord a => OneOrTwo a -> OneOrTwo a -> Bool
> :: OneOrTwo a -> OneOrTwo a -> Bool
$c>= :: forall a. Ord a => OneOrTwo a -> OneOrTwo a -> Bool
>= :: OneOrTwo a -> OneOrTwo a -> Bool
$cmax :: forall a. Ord a => OneOrTwo a -> OneOrTwo a -> OneOrTwo a
max :: OneOrTwo a -> OneOrTwo a -> OneOrTwo a
$cmin :: forall a. Ord a => OneOrTwo a -> OneOrTwo a -> OneOrTwo a
min :: OneOrTwo a -> OneOrTwo a -> OneOrTwo a
Ord, (forall a b. (a -> b) -> OneOrTwo a -> OneOrTwo b)
-> (forall a b. a -> OneOrTwo b -> OneOrTwo a) -> Functor OneOrTwo
forall a b. a -> OneOrTwo b -> OneOrTwo a
forall a b. (a -> b) -> OneOrTwo a -> OneOrTwo b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> OneOrTwo a -> OneOrTwo b
fmap :: forall a b. (a -> b) -> OneOrTwo a -> OneOrTwo b
$c<$ :: forall a b. a -> OneOrTwo b -> OneOrTwo a
<$ :: forall a b. a -> OneOrTwo b -> OneOrTwo a
Functor, (forall m. Monoid m => OneOrTwo m -> m)
-> (forall m a. Monoid m => (a -> m) -> OneOrTwo a -> m)
-> (forall m a. Monoid m => (a -> m) -> OneOrTwo a -> m)
-> (forall a b. (a -> b -> b) -> b -> OneOrTwo a -> b)
-> (forall a b. (a -> b -> b) -> b -> OneOrTwo a -> b)
-> (forall b a. (b -> a -> b) -> b -> OneOrTwo a -> b)
-> (forall b a. (b -> a -> b) -> b -> OneOrTwo a -> b)
-> (forall a. (a -> a -> a) -> OneOrTwo a -> a)
-> (forall a. (a -> a -> a) -> OneOrTwo a -> a)
-> (forall a. OneOrTwo a -> [a])
-> (forall a. OneOrTwo a -> Bool)
-> (forall a. OneOrTwo a -> Int)
-> (forall a. Eq a => a -> OneOrTwo a -> Bool)
-> (forall a. Ord a => OneOrTwo a -> a)
-> (forall a. Ord a => OneOrTwo a -> a)
-> (forall a. Num a => OneOrTwo a -> a)
-> (forall a. Num a => OneOrTwo a -> a)
-> Foldable OneOrTwo
forall a. Eq a => a -> OneOrTwo a -> Bool
forall a. Num a => OneOrTwo a -> a
forall a. Ord a => OneOrTwo a -> a
forall m. Monoid m => OneOrTwo m -> m
forall a. OneOrTwo a -> Bool
forall a. OneOrTwo a -> Int
forall a. OneOrTwo a -> [a]
forall a. (a -> a -> a) -> OneOrTwo a -> a
forall m a. Monoid m => (a -> m) -> OneOrTwo a -> m
forall b a. (b -> a -> b) -> b -> OneOrTwo a -> b
forall a b. (a -> b -> b) -> b -> OneOrTwo a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => OneOrTwo m -> m
fold :: forall m. Monoid m => OneOrTwo m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> OneOrTwo a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> OneOrTwo a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> OneOrTwo a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> OneOrTwo a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> OneOrTwo a -> b
foldr :: forall a b. (a -> b -> b) -> b -> OneOrTwo a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> OneOrTwo a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> OneOrTwo a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> OneOrTwo a -> b
foldl :: forall b a. (b -> a -> b) -> b -> OneOrTwo a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> OneOrTwo a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> OneOrTwo a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> OneOrTwo a -> a
foldr1 :: forall a. (a -> a -> a) -> OneOrTwo a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> OneOrTwo a -> a
foldl1 :: forall a. (a -> a -> a) -> OneOrTwo a -> a
$ctoList :: forall a. OneOrTwo a -> [a]
toList :: forall a. OneOrTwo a -> [a]
$cnull :: forall a. OneOrTwo a -> Bool
null :: forall a. OneOrTwo a -> Bool
$clength :: forall a. OneOrTwo a -> Int
length :: forall a. OneOrTwo a -> Int
$celem :: forall a. Eq a => a -> OneOrTwo a -> Bool
elem :: forall a. Eq a => a -> OneOrTwo a -> Bool
$cmaximum :: forall a. Ord a => OneOrTwo a -> a
maximum :: forall a. Ord a => OneOrTwo a -> a
$cminimum :: forall a. Ord a => OneOrTwo a -> a
minimum :: forall a. Ord a => OneOrTwo a -> a
$csum :: forall a. Num a => OneOrTwo a -> a
sum :: forall a. Num a => OneOrTwo a -> a
$cproduct :: forall a. Num a => OneOrTwo a -> a
product :: forall a. Num a => OneOrTwo a -> a
Foldable, Functor OneOrTwo
Foldable OneOrTwo
(Functor OneOrTwo, Foldable OneOrTwo) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> OneOrTwo a -> f (OneOrTwo b))
-> (forall (f :: * -> *) a.
Applicative f =>
OneOrTwo (f a) -> f (OneOrTwo a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> OneOrTwo a -> m (OneOrTwo b))
-> (forall (m :: * -> *) a.
Monad m =>
OneOrTwo (m a) -> m (OneOrTwo a))
-> Traversable OneOrTwo
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => OneOrTwo (m a) -> m (OneOrTwo a)
forall (f :: * -> *) a.
Applicative f =>
OneOrTwo (f a) -> f (OneOrTwo a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> OneOrTwo a -> m (OneOrTwo b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> OneOrTwo a -> f (OneOrTwo b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> OneOrTwo a -> f (OneOrTwo b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> OneOrTwo a -> f (OneOrTwo b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
OneOrTwo (f a) -> f (OneOrTwo a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
OneOrTwo (f a) -> f (OneOrTwo a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> OneOrTwo a -> m (OneOrTwo b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> OneOrTwo a -> m (OneOrTwo b)
$csequence :: forall (m :: * -> *) a. Monad m => OneOrTwo (m a) -> m (OneOrTwo a)
sequence :: forall (m :: * -> *) a. Monad m => OneOrTwo (m a) -> m (OneOrTwo a)
Traversable)
instance Show a => Show (OneOrTwo a) where
show :: OneOrTwo a -> String
show (One a
a) = a -> String
forall a. Show a => a -> String
show a
a
show (Two a
a a
b) = a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"||" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
b
name12 :: OneOrTwo Name -> Name
name12 :: OneOrTwo Name -> Name
name12 (One Name
n) = Name
n
name12 (Two Name
n1 Name
n2)
| String -> Bool
forall a. Null a => a -> Bool
null (Name -> String
suggestion Name
n2) = Name
n1
| String -> Bool
forall a. Null a => a -> Bool
null (Name -> String
suggestion Name
n1) = Name
n2
| Name -> String
suggestion Name
n1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
suggestion Name
n2 = Name
n1
| Bool
otherwise = String -> Name
fresh (Name -> String
suggestion Name
n1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"||" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
suggestion Name
n2)
oneOrTwo :: (a -> b) -> (a -> a -> b) -> OneOrTwo a -> b
oneOrTwo :: forall a b. (a -> b) -> (a -> a -> b) -> OneOrTwo a -> b
oneOrTwo a -> b
f a -> a -> b
g (One a
a) = a -> b
f a
a
oneOrTwo a -> b
f a -> a -> b
g (Two a
a1 a
a2) = a -> a -> b
g a
a1 a
a2
fromOne :: OneOrTwo a -> a
fromOne :: forall a. OneOrTwo a -> a
fromOne (One a
a) = a
a
toTwo :: OneOrTwo a -> OneOrTwo a
toTwo :: forall a. OneOrTwo a -> OneOrTwo a
toTwo = (a -> OneOrTwo a)
-> (a -> a -> OneOrTwo a) -> OneOrTwo a -> OneOrTwo a
forall a b. (a -> b) -> (a -> a -> b) -> OneOrTwo a -> b
oneOrTwo (\ a
a -> a -> a -> OneOrTwo a
forall a. a -> a -> OneOrTwo a
Two a
a a
a) a -> a -> OneOrTwo a
forall a. a -> a -> OneOrTwo a
Two
first12 :: OneOrTwo a -> a
first12 :: forall a. OneOrTwo a -> a
first12 (One a
a) = a
a
first12 (Two a
a1 a
a2) = a
a1
second12 :: OneOrTwo a -> a
second12 :: forall a. OneOrTwo a -> a
second12 (One a
a) = a
a
second12 (Two a
a1 a
a2) = a
a2
mapSecond12 :: (a -> a) -> OneOrTwo a -> OneOrTwo a
mapSecond12 :: forall a. (a -> a) -> OneOrTwo a -> OneOrTwo a
mapSecond12 a -> a
f (One a
a) = a -> OneOrTwo a
forall a. a -> OneOrTwo a
One (a -> a
f a
a)
mapSecond12 a -> a
f (Two a
a1 a
a2) = a -> a -> OneOrTwo a
forall a. a -> a -> OneOrTwo a
Two a
a1 (a -> a
f a
a2)
zipWith12 :: (a -> b -> c) -> OneOrTwo a -> OneOrTwo b -> OneOrTwo c
zipWith12 :: forall a b c.
(a -> b -> c) -> OneOrTwo a -> OneOrTwo b -> OneOrTwo c
zipWith12 a -> b -> c
f (One a
a) (One b
b) = c -> OneOrTwo c
forall a. a -> OneOrTwo a
One (a -> b -> c
f a
a b
b)
zipWith12 a -> b -> c
f (Two a
a a
a') (Two b
b b
b') = c -> c -> OneOrTwo c
forall a. a -> a -> OneOrTwo a
Two (a -> b -> c
f a
a b
b) (a -> b -> c
f a
a' b
b')
zipWith123 :: (a -> b -> c -> d) ->
OneOrTwo a -> OneOrTwo b -> OneOrTwo c -> OneOrTwo d
zipWith123 :: forall a b c d.
(a -> b -> c -> d)
-> OneOrTwo a -> OneOrTwo b -> OneOrTwo c -> OneOrTwo d
zipWith123 a -> b -> c -> d
f (One a
a) (One b
b) (One c
c) = d -> OneOrTwo d
forall a. a -> OneOrTwo a
One (a -> b -> c -> d
f a
a b
b c
c)
zipWith123 a -> b -> c -> d
f (Two a
a a
a') (Two b
b b
b') (Two c
c c
c') = d -> d -> OneOrTwo d
forall a. a -> a -> OneOrTwo a
Two (a -> b -> c -> d
f a
a b
b c
c) (a -> b -> c -> d
f a
a' b
b' c
c')
toList12 :: OneOrTwo a -> [a]
toList12 :: forall a. OneOrTwo a -> [a]
toList12 (One a
a) = [a
a]
toList12 (Two a
a1 a
a2) = [a
a1,a
a2]
fromList12 :: Show a => [a] -> OneOrTwo a
fromList12 :: forall a. Show a => [a] -> OneOrTwo a
fromList12 [a
a] = a -> OneOrTwo a
forall a. a -> OneOrTwo a
One a
a
fromList12 [a
a1,a
a2] = a -> a -> OneOrTwo a
forall a. a -> a -> OneOrTwo a
Two a
a1 a
a2
fromList12 [a]
l = String -> OneOrTwo a
forall a. HasCallStack => String -> a
error (String -> OneOrTwo a) -> String -> OneOrTwo a
forall a b. (a -> b) -> a -> b
$ String
"fromList12 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
l
toMaybe12 :: Show a => [a] -> Maybe (OneOrTwo a)
toMaybe12 :: forall a. Show a => [a] -> Maybe (OneOrTwo a)
toMaybe12 [] = Maybe (OneOrTwo a)
forall a. Maybe a
Nothing
toMaybe12 [a
a] = OneOrTwo a -> Maybe (OneOrTwo a)
forall a. a -> Maybe a
Just (OneOrTwo a -> Maybe (OneOrTwo a))
-> OneOrTwo a -> Maybe (OneOrTwo a)
forall a b. (a -> b) -> a -> b
$ a -> OneOrTwo a
forall a. a -> OneOrTwo a
One a
a
toMaybe12 [a
a1,a
a2] = OneOrTwo a -> Maybe (OneOrTwo a)
forall a. a -> Maybe a
Just (OneOrTwo a -> Maybe (OneOrTwo a))
-> OneOrTwo a -> Maybe (OneOrTwo a)
forall a b. (a -> b) -> a -> b
$ a -> a -> OneOrTwo a
forall a. a -> a -> OneOrTwo a
Two a
a1 a
a2
toMaybe12 [a]
l = String -> Maybe (OneOrTwo a)
forall a. HasCallStack => String -> a
error (String -> Maybe (OneOrTwo a)) -> String -> Maybe (OneOrTwo a)
forall a b. (a -> b) -> a -> b
$ String
"toMaybe12 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
l
data TCContext = TCContext
{ TCContext -> SemCxt
context :: SemCxt
, TCContext -> Ren
renaming :: Ren
, TCContext -> Map Int Name
naming :: Map Int Name
, TCContext -> Env2
environ :: Env2
, TCContext -> Rewrites
rewrites :: Rewrites
, TCContext -> TSO Int
sizeRels :: TSO Int
, TCContext -> [Int]
belowInfty:: [Int]
, TCContext -> [Bound Val]
bounds :: [Bound Val]
, TCContext -> Bool
consistencyCheck :: Bool
, TCContext -> Bool
checkingConType :: Bool
, TCContext -> AssertionHandling
assertionHandling :: AssertionHandling
, TCContext -> Bool
impredicative :: Bool
, TCContext -> Map Name (Kinded Fun)
funsTemplate :: Map Name (Kinded Fun)
, TCContext -> Map Name SigDef
mutualFuns :: Map Name SigDef
, TCContext -> Co
mutualCo :: Co
, TCContext -> [Name]
mutualNames :: [Name]
, TCContext -> Maybe DefId
checkingMutualName :: Maybe DefId
, TCContext -> [QName]
callStack :: [QName]
}
instance Show TCContext where
show :: TCContext -> String
show TCContext
ce = Env2 -> String
forall a. Show a => a -> String
show (TCContext -> Env2
environ TCContext
ce) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"; " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SemCxt -> String
forall a. Show a => a -> String
show (TCContext -> SemCxt
context TCContext
ce)
emptyContext :: TCContext
emptyContext :: TCContext
emptyContext = TCContext
{ context :: SemCxt
context = SemCxt
cxtEmpty
, renaming :: Ren
renaming = Ren
forall k a. Map k a
Map.empty
, naming :: Map Int Name
naming = Map Int Name
forall k a. Map k a
Map.empty
, environ :: Env2
environ = Env2
forall a. Environ a
emptyEnv
, rewrites :: Rewrites
rewrites = Rewrites
emptyRewrites
, sizeRels :: TSO Int
sizeRels = TSO Int
forall a. TSO a
TSO.empty
, belowInfty :: [Int]
belowInfty = []
, bounds :: [Bound Val]
bounds = []
, consistencyCheck :: Bool
consistencyCheck = Bool
False
, checkingConType :: Bool
checkingConType = Bool
False
, assertionHandling :: AssertionHandling
assertionHandling = AssertionHandling
Failure
, impredicative :: Bool
impredicative = Bool
False
, funsTemplate :: Map Name (Kinded Fun)
funsTemplate = Map Name (Kinded Fun)
forall k a. Map k a
Map.empty
, mutualFuns :: Map Name SigDef
mutualFuns = Map Name SigDef
forall k a. Map k a
Map.empty
, mutualCo :: Co
mutualCo = Co
Ind
, mutualNames :: [Name]
mutualNames = []
, checkingMutualName :: Maybe DefId
checkingMutualName = Maybe DefId
forall a. Maybe a
Nothing
, callStack :: [QName]
callStack = []
}
data TCState = TCState
{ TCState -> Signature
signature :: Signature
, TCState -> MetaVars
metaVars :: MetaVars
, TCState -> Constraints
constraints :: Constraints
, TCState -> PositivityGraph
positivityGraph :: PositivityGraph
}
type MetaVars = Map MVar MetaVar
emptyMetaVars :: MetaVars
emptyMetaVars :: MetaVars
emptyMetaVars = MetaVars
forall k a. Map k a
Map.empty
type MScope = [Name]
data MetaVar = MetaVar
{ MetaVar -> [Name]
mscope :: MScope
, MetaVar -> Maybe Val
solution :: Maybe Val
}
type PosConstrnt = Constrnt PPoly DefId ()
type PositivityGraph = [PosConstrnt]
emptyPosGraph :: PositivityGraph
emptyPosGraph :: PositivityGraph
emptyPosGraph = []
type TypeCheck = StateT TCState (ReaderT TCContext (ExceptT TraceError IO))
instance MonadAssert TypeCheck where
assert :: Bool -> String -> TypeCheck ()
assert Bool
b String
s = do
h <- (TCContext -> AssertionHandling)
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
AssertionHandling
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCContext -> AssertionHandling
assertionHandling
assert' h b s
newAssertionHandling :: forall a. AssertionHandling -> TypeCheck a -> TypeCheck a
newAssertionHandling AssertionHandling
h = (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ( \ TCContext
ce -> TCContext
ce { assertionHandling = h })
data Rewrite = Rewrite { Rewrite -> Val
lhs :: Val, Rewrite -> Val
rhs :: Val }
type Rewrites = [Rewrite]
emptyRewrites :: Rewrites
emptyRewrites :: Rewrites
emptyRewrites = []
instance Show Rewrite where
show :: Rewrite -> String
show Rewrite
rr = Val -> String
forall a. Show a => a -> String
show (Rewrite -> Val
lhs Rewrite
rr) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" --> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show (Rewrite -> Val
rhs Rewrite
rr)
type Ren = Map Name Int
type Env2 = Environ (OneOrTwo Val)
type Context a = Map Int a
type Context2 a = Context (OneOrTwo a)
data CxtE a = CxtEntry { forall a. CxtE a -> a
domain :: a, forall a. CxtE a -> UDec
upperDec :: UDec }
type CxtEntry = CxtE (OneOrTwo Domain)
type CxtEntry1 = CxtE Domain
data SemCxt = SemCxt
{ SemCxt -> Int
len :: Int
, SemCxt -> Context2 Domain
cxt :: Context2 Domain
, SemCxt -> Context UDec
upperDecs :: Context UDec
}
instance Show SemCxt where
show :: SemCxt -> String
show SemCxt
delta =
[(OneOrTwo Domain, UDec)] -> String
forall a. Show a => a -> String
show ([(OneOrTwo Domain, UDec)] -> String)
-> [(OneOrTwo Domain, UDec)] -> String
forall a b. (a -> b) -> a -> b
$ [OneOrTwo Domain] -> [UDec] -> [(OneOrTwo Domain, UDec)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Context2 Domain -> [OneOrTwo Domain]
forall k a. Map k a -> [a]
Map.elems (SemCxt -> Context2 Domain
cxt SemCxt
delta))
(Context UDec -> [UDec]
forall k a. Map k a -> [a]
Map.elems (SemCxt -> Context UDec
upperDecs SemCxt
delta))
cxtEmpty :: SemCxt
cxtEmpty :: SemCxt
cxtEmpty = SemCxt
{ len :: Int
len = Int
0
, cxt :: Context2 Domain
cxt = Context2 Domain
forall k a. Map k a
Map.empty
, upperDecs :: Context UDec
upperDecs = Context UDec
forall k a. Map k a
Map.empty
}
cxtPush' :: OneOrTwo Domain -> SemCxt -> SemCxt
cxtPush' :: OneOrTwo Domain -> SemCxt -> SemCxt
cxtPush' OneOrTwo Domain
entry SemCxt
delta =
SemCxt
delta { len = k + 1
, cxt = Map.insert k entry (cxt delta)
, upperDecs = Map.insert k defaultUpperDec (upperDecs delta)
}
where k :: Int
k = SemCxt -> Int
len SemCxt
delta
cxtPushEntry :: OneOrTwo Domain -> SemCxt -> (Int, SemCxt)
cxtPushEntry :: OneOrTwo Domain -> SemCxt -> (Int, SemCxt)
cxtPushEntry OneOrTwo Domain
ce SemCxt
delta = (SemCxt -> Int
len SemCxt
delta, OneOrTwo Domain -> SemCxt -> SemCxt
cxtPush' OneOrTwo Domain
ce SemCxt
delta)
cxtPush :: Domain -> SemCxt -> (Int, SemCxt)
cxtPush :: Domain -> SemCxt -> (Int, SemCxt)
cxtPush Domain
dom SemCxt
delta = OneOrTwo Domain -> SemCxt -> (Int, SemCxt)
cxtPushEntry (Domain -> OneOrTwo Domain
forall a. a -> OneOrTwo a
One Domain
dom) SemCxt
delta
cxtPush2 :: Domain -> Domain -> SemCxt -> (Int, SemCxt)
cxtPush2 :: Domain -> Domain -> SemCxt -> (Int, SemCxt)
cxtPush2 Domain
doml Domain
domr SemCxt
delta = OneOrTwo Domain -> SemCxt -> (Int, SemCxt)
cxtPushEntry (Domain -> Domain -> OneOrTwo Domain
forall a. a -> a -> OneOrTwo a
Two Domain
doml Domain
domr) SemCxt
delta
cxtPushGen :: Name -> SemCxt -> (Int, SemCxt)
cxtPushGen :: Name -> SemCxt -> (Int, SemCxt)
cxtPushGen Name
x SemCxt
delta = Domain -> SemCxt -> (Int, SemCxt)
cxtPush Domain
forall {b}. b
bot SemCxt
delta
where bot :: b
bot = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"IMPOSSIBLE: name " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not bound to any type"
cxtSetType :: Int -> Domain -> SemCxt -> SemCxt
cxtSetType :: Int -> Domain -> SemCxt -> SemCxt
cxtSetType Int
k Domain
dom SemCxt
delta =
SemCxt
delta { cxt = Map.insert k (One dom) (cxt delta)
}
lookupM :: (MonadError TraceError m, Show k, Ord k) => k -> Map k v -> m v
lookupM :: forall (m :: * -> *) k v.
(MonadError TraceError m, Show k, Ord k) =>
k -> Map k v -> m v
lookupM k
k Map k v
m = m v -> (v -> m v) -> Maybe v -> m v
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> m v
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m v) -> String -> m v
forall a b. (a -> b) -> a -> b
$ String
"lookupM: unbound key " String -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k) v -> m v
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe v -> m v) -> Maybe v -> m v
forall a b. (a -> b) -> a -> b
$ k -> Map k v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k v
m
cxtLookupGen :: MonadError TraceError m => SemCxt -> Int -> m CxtEntry
cxtLookupGen :: forall (m :: * -> *).
MonadError TraceError m =>
SemCxt -> Int -> m CxtEntry
cxtLookupGen SemCxt
delta Int
k = do
dom12 <- Int -> Context2 Domain -> m (OneOrTwo Domain)
forall (m :: * -> *) k v.
(MonadError TraceError m, Show k, Ord k) =>
k -> Map k v -> m v
lookupM Int
k (SemCxt -> Context2 Domain
cxt SemCxt
delta)
udec <- lookupM k (upperDecs delta)
return $ CxtEntry dom12 udec
cxtLookupName :: MonadError TraceError m => SemCxt -> Ren -> Name -> m CxtEntry
cxtLookupName :: forall (m :: * -> *).
MonadError TraceError m =>
SemCxt -> Ren -> Name -> m CxtEntry
cxtLookupName SemCxt
delta Ren
ren Name
x = do
i <- Name -> Ren -> m Int
forall (m :: * -> *) k v.
(MonadError TraceError m, Show k, Ord k) =>
k -> Map k v -> m v
lookupM Name
x Ren
ren
cxtLookupGen delta i
cxtApplyDec :: Dec -> SemCxt -> SemCxt
cxtApplyDec :: Dec -> SemCxt -> SemCxt
cxtApplyDec Dec
dec SemCxt
delta = SemCxt
delta { upperDecs = Map.map (compDec dec) (upperDecs delta) }
class Monad m => MonadCxt m where
newVar :: Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> m a) -> m a
newWithGen :: Name -> Domain -> (Int -> Val -> m a) -> m a
newWithGen Name
x Domain
d Int -> Val -> m a
k = Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> m a) -> m a
forall a.
Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> m a) -> m a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> m a) -> m a
newVar Name
x (Domain -> OneOrTwo Domain
forall a. a -> OneOrTwo a
One Domain
d)
(\ Int
i (One Val
v) -> Int -> Val -> m a
k Int
i Val
v)
new2WithGen:: Name -> (Domain, Domain) -> (Int -> (Val, Val) -> m a) -> m a
new2WithGen Name
x (Domain
doml, Domain
domr) Int -> (Val, Val) -> m a
k = Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> m a) -> m a
forall a.
Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> m a) -> m a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> m a) -> m a
newVar Name
x (Domain -> Domain -> OneOrTwo Domain
forall a. a -> a -> OneOrTwo a
Two Domain
doml Domain
domr)
(\ Int
i (Two Val
vl Val
vr) -> Int -> (Val, Val) -> m a
k Int
i (Val
vl, Val
vr))
new :: Name -> Domain -> (Val -> m a) -> m a
new Name
x Domain
d Val -> m a
cont = Name -> Domain -> (Int -> Val -> m a) -> m a
forall a. Name -> Domain -> (Int -> Val -> m a) -> m a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> Domain -> (Int -> Val -> m a) -> m a
newWithGen Name
x Domain
d (\ Int
_ -> Val -> m a
cont)
new2 :: Name -> (Domain, Domain) -> ((Val, Val) -> m a) -> m a
new2 Name
x (Domain, Domain)
d (Val, Val) -> m a
cont = Name -> (Domain, Domain) -> (Int -> (Val, Val) -> m a) -> m a
forall a.
Name -> (Domain, Domain) -> (Int -> (Val, Val) -> m a) -> m a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> (Domain, Domain) -> (Int -> (Val, Val) -> m a) -> m a
new2WithGen Name
x (Domain, Domain)
d (\ Int
_ -> (Val, Val) -> m a
cont)
new' :: Name -> Domain -> m a -> m a
new' Name
x Domain
d m a
cont = Name -> Domain -> (Val -> m a) -> m a
forall a. Name -> Domain -> (Val -> m a) -> m a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> Domain -> (Val -> m a) -> m a
new Name
x Domain
d (\ Val
_ -> m a
cont)
newIrr :: Name -> m a -> m a
addName :: Name -> (Val -> m a) -> m a
addKindedTypeSigs :: [Kinded (TySig TVal)] -> m a -> m a
addKindedTypeSigs [] m a
k = m a
k
addKindedTypeSigs (Kinded Kind
ki (TypeSig Name
n Val
tv) : [Kinded (TySig Val)]
ktss) m a
k =
Name -> Domain -> m a -> m a
forall a. Name -> Domain -> m a -> m a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
new' Name
n (Val -> Kind -> Dec -> Domain
forall a. a -> Kind -> Dec -> Dom a
Domain Val
tv Kind
ki Dec
defaultDec) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ [Kinded (TySig Val)] -> m a -> m a
forall a. [Kinded (TySig Val)] -> m a -> m a
forall (m :: * -> *) a.
MonadCxt m =>
[Kinded (TySig Val)] -> m a -> m a
addKindedTypeSigs [Kinded (TySig Val)]
ktss m a
k
setType :: Int -> Domain -> m a -> m a
setTypeOfName :: Name -> Domain -> m a -> m a
genOfName :: Name -> m Int
nameOfGen :: Int -> m Name
uniqueName :: Name -> Int -> m Name
uniqueName Name
x Int
_ = Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
lookupGen :: Int -> m CxtEntry
lookupGenType2 :: Int -> m (TVal, TVal)
lookupGenType2 Int
i = do
entry <- Int -> m CxtEntry
forall (m :: * -> *). MonadCxt m => Int -> m CxtEntry
lookupGen Int
i
case domain entry of
One Domain
d1 -> (Val, Val) -> m (Val, Val)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Domain -> Val
forall a. Dom a -> a
typ Domain
d1, Domain -> Val
forall a. Dom a -> a
typ Domain
d1)
Two Domain
d1 Domain
d2 -> (Val, Val) -> m (Val, Val)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Domain -> Val
forall a. Dom a -> a
typ Domain
d1, Domain -> Val
forall a. Dom a -> a
typ Domain
d2)
lookupName :: Name -> m CxtEntry
lookupName1 :: Name -> m CxtEntry1
lookupName1 Name
x = do
e <- Name -> m CxtEntry
forall (m :: * -> *). MonadCxt m => Name -> m CxtEntry
lookupName Name
x
return $ CxtEntry (fromOne (domain e)) (upperDec e)
getContextTele :: m TeleVal
getLen :: m Int
getEnv :: m Env
getRen :: m Ren
applyDec :: Dec -> m a -> m a
resurrect :: m a -> m a
resurrect = Dec -> m a -> m a
forall a. Dec -> m a -> m a
forall (m :: * -> *) a. MonadCxt m => Dec -> m a -> m a
applyDec Dec
irrelevantDec
addRewrite :: Rewrite -> [Val] -> ([Val] -> m a) -> m a
addPattern :: TVal -> Pattern -> Env -> (TVal -> Val -> Env -> m a) -> m a
addPatterns:: TVal -> [Pattern] -> Env -> (TVal -> [Val] -> Env -> m a) -> m a
addSizeRel :: Int -> Int -> Int -> m a -> m a
addBelowInfty :: Int -> m a -> m a
addBoundHyp :: Bound Val -> m a -> m a
isBelowInfty :: Int -> m Bool
sizeVarBelow :: Int -> Int -> m (Maybe Int)
getMinSize :: Int -> m (Maybe Int)
getSizeVarsInScope :: m [Name]
checkingCon :: Bool -> m a -> m a
checkingDom :: m a -> m a
setCo :: Co -> m a -> m a
installFuns :: Co -> [Kinded Fun] -> m a -> m a
setMeasure :: Measure Val -> m a -> m a
activateFuns :: m a -> m a
goImpredicative :: m a -> m a
checkingMutual :: Maybe DefId -> m a -> m a
dontCare :: a
dontCare :: forall {b}. b
dontCare = String -> a
forall a. HasCallStack => String -> a
error String
"Internal error: tried to retrieve unassigned type of variable"
instance MonadCxt TypeCheck where
newIrr :: forall a. Name -> TypeCheck a -> TypeCheck a
newIrr Name
x = (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
ce -> TCContext
ce { environ = update (environ ce) x (One VIrr) })
addName :: forall a. Name -> (Val -> TypeCheck a) -> TypeCheck a
addName Name
x Val -> TypeCheck a
f = String -> TypeCheck a -> TypeCheck a
forall (m :: * -> *) a.
MonadError TraceError m =>
String -> m a -> m a
enter (String
"new " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : _") (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ do
cxtenv <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
let (k, delta) = cxtPushGen x (context cxtenv)
let v = Int -> Val
VGen Int
k
let rho = Env2 -> Name -> OneOrTwo Val -> Env2
forall a. Environ a -> Name -> a -> Environ a
update (TCContext -> Env2
environ TCContext
cxtenv) Name
x (Val -> OneOrTwo Val
forall a. a -> OneOrTwo a
One Val
v)
x' <- uniqueName x k
local (\ TCContext
cxt -> TCContext
cxt { context = delta
, renaming = Map.insert x k (renaming cxtenv)
, naming = Map.insert k x' (naming cxt)
, environ = rho }) (f v)
newVar :: forall a.
Name
-> OneOrTwo Domain
-> (Int -> OneOrTwo Val -> TypeCheck a)
-> TypeCheck a
newVar Name
x dom12 :: OneOrTwo Domain
dom12@(One (Domain (VBelow LtLe
ltle Val
v) Kind
ki Dec
dec)) Int -> OneOrTwo Val -> TypeCheck a
f = do
String -> TypeCheck a -> TypeCheck a
forall (m :: * -> *) a.
MonadError TraceError m =>
String -> m a -> m a
enter (String
"new " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ LtLe -> String
forall a. Show a => a -> String
show LtLe
ltle String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v) (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ do
cxtenv <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
let (k, delta) = cxtPushEntry (One (Domain vSize kSize dec)) (context cxtenv)
let xv = Int -> Val
VGen Int
k
let v12 = Val -> OneOrTwo Val
forall a. a -> OneOrTwo a
One Val
xv
let rho = Env2 -> Name -> OneOrTwo Val -> Env2
forall a. Environ a -> Name -> a -> Environ a
update (TCContext -> Env2
environ TCContext
cxtenv) Name
x OneOrTwo Val
v12
let beta = LtLe -> Measure Val -> Measure Val -> Bound Val
forall a. LtLe -> Measure a -> Measure a -> Bound a
Bound LtLe
ltle ([Val] -> Measure Val
forall a. [a] -> Measure a
Measure [Val
xv]) ([Val] -> Measure Val
forall a. [a] -> Measure a
Measure [Val
v])
x' <- uniqueName x k
local (\ TCContext
cxt -> TCContext
cxt { context = delta
, renaming = Map.insert x k (renaming cxtenv)
, naming = Map.insert k x' (naming cxtenv)
, environ = rho }) $
addBoundHyp beta $ (f k v12)
newVar Name
x OneOrTwo Domain
dom12 Int -> OneOrTwo Val -> TypeCheck a
f = do
let tv12 :: OneOrTwo Val
tv12 = (Domain -> Val) -> OneOrTwo Domain -> OneOrTwo Val
forall a b. (a -> b) -> OneOrTwo a -> OneOrTwo b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Domain -> Val
forall a. Dom a -> a
typ OneOrTwo Domain
dom12
String -> TypeCheck a -> TypeCheck a
forall (m :: * -> *) a.
MonadError TraceError m =>
String -> m a -> m a
enter (String
"new " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ OneOrTwo Val -> String
forall a. Show a => a -> String
show OneOrTwo Val
tv12) (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ do
cxtenv <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
let (k, delta) = cxtPushEntry dom12 (context cxtenv)
v12 <- Traversable.mapM (up False (VGen k)) tv12
let rho = Env2 -> Name -> OneOrTwo Val -> Env2
forall a. Environ a -> Name -> a -> Environ a
update (TCContext -> Env2
environ TCContext
cxtenv) Name
x OneOrTwo Val
v12
x' <- uniqueName x k
local (\ TCContext
cxt -> TCContext
cxt { context = delta
, renaming = Map.insert x k (renaming cxtenv)
, naming = Map.insert k x' (naming cxtenv)
, environ = rho }) (f k v12)
setType :: forall a. Int -> Domain -> TypeCheck a -> TypeCheck a
setType Int
k Domain
dom =
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
ce -> TCContext
ce { context = cxtSetType k dom (context ce) })
setTypeOfName :: forall a. Name -> Domain -> TypeCheck a -> TypeCheck a
setTypeOfName Name
x Domain
dom TypeCheck a
cont = do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
let Just k = Map.lookup x (renaming ce)
setType k dom cont
genOfName :: Name -> TypeCheck Int
genOfName Name
x = do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
case Map.lookup x (renaming ce) of
Maybe Int
Nothing -> String -> TypeCheck Int
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck Int) -> String -> TypeCheck Int
forall a b. (a -> b) -> a -> b
$ String
"internal error: variable not bound: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x
Just Int
k -> Int -> TypeCheck Int
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
k
nameOfGen :: Int -> TypeCheck Name
nameOfGen Int
k = do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
case Map.lookup k (naming ce) of
Maybe Name
Nothing -> Name -> TypeCheck Name
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> TypeCheck Name) -> Name -> TypeCheck Name
forall a b. (a -> b) -> a -> b
$ String -> Name
fresh (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"error_unnamed_gen" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
Just Name
x -> Name -> TypeCheck Name
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
lookupGen :: Int -> TypeCheck CxtEntry
lookupGen Int
k = do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
cxtLookupGen (context ce) k
lookupName :: Name -> TypeCheck CxtEntry
lookupName Name
x = do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
cxtLookupName (context ce) (renaming ce) x
getContextTele :: TypeCheck TeleVal
getContextTele = do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
let cxt = TCContext -> SemCxt
context TCContext
ce
let ren = TCContext -> Ren
renaming TCContext
ce
let env = Env2 -> [(Name, OneOrTwo Val)]
forall a. Environ a -> [(Name, a)]
envMap (Env2 -> [(Name, OneOrTwo Val)]) -> Env2 -> [(Name, OneOrTwo Val)]
forall a b. (a -> b) -> a -> b
$ TCContext -> Env2
environ TCContext
ce
let mkTBind (Name
x,b
_) = (Name -> Domain -> TBinding Val
forall a. Name -> Dom a -> TBinding a
TBind Name
x (Domain -> TBinding Val)
-> (CxtEntry -> Domain) -> CxtEntry -> TBinding Val
forall b c a. (b -> c) -> (a -> b) -> a -> c
.OneOrTwo Domain -> Domain
forall a. OneOrTwo a -> a
fromOne (OneOrTwo Domain -> Domain)
-> (CxtEntry -> OneOrTwo Domain) -> CxtEntry -> Domain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtEntry -> OneOrTwo Domain
forall a. CxtE a -> a
domain) (CxtEntry -> TBinding Val) -> f CxtEntry -> f (TBinding Val)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SemCxt -> Ren -> Name -> f CxtEntry
forall (m :: * -> *).
MonadError TraceError m =>
SemCxt -> Ren -> Name -> m CxtEntry
cxtLookupName SemCxt
cxt Ren
ren Name
x
mapM mkTBind env
getLen :: TypeCheck Int
getLen = do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
return $ len (context ce)
getRen :: TypeCheck Ren
getRen = do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
return $ renaming ce
getEnv :: TypeCheck Env
getEnv = do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
let (Environ rho mmeas) = environ ce
return $ Environ (map (\ (Name
x, One Val
v) -> (Name
x, Val
v)) rho) mmeas
applyDec :: forall a. Dec -> TypeCheck a -> TypeCheck a
applyDec Dec
dec = (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
ce -> TCContext
ce { context = cxtApplyDec dec (context ce) })
addRewrite :: forall a. Rewrite -> [Val] -> ([Val] -> TypeCheck a) -> TypeCheck a
addRewrite Rewrite
rew [Val]
vs [Val] -> TypeCheck a
cont = String -> TypeCheck a -> TypeCheck a
forall a. String -> a -> a
traceRew (String
"adding rewrite " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rewrite -> String
forall a. Show a => a -> String
show Rewrite
rew) (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$
(TCContext -> TCContext) -> TypeCheck a -> TypeCheck a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
cxt -> TCContext
cxt { rewrites = rew : (rewrites cxt) }) (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ do
ce <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
traceRewM "normalizing types in context"
cx' <- mapMapM (Traversable.mapM (Traversable.mapM reval)) (cxt (context ce))
traceRewM "normalizing environment"
let Environ rho mmeas = environ ce
rho' <- mapM (\ (Name
x,OneOrTwo Val
v12) -> (Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> OneOrTwo Val
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (OneOrTwo Val)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> OneOrTwo a -> m (OneOrTwo b)
Traversable.mapM Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall a. Reval a => a -> TypeCheck a
reval OneOrTwo Val
v12 StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (OneOrTwo Val)
-> (OneOrTwo Val
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
(Name, OneOrTwo Val))
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
(Name, OneOrTwo Val)
forall a b.
StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> (a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) b)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ OneOrTwo Val
v12' -> (Name, OneOrTwo Val)
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
(Name, OneOrTwo Val)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x, OneOrTwo Val
v12')) rho
let en' = [(Name, OneOrTwo Val)] -> Maybe (Measure Val) -> Env2
forall a. [(Name, a)] -> Maybe (Measure Val) -> Environ a
Environ [(Name, OneOrTwo Val)]
rho' Maybe (Measure Val)
mmeas
vs' <- mapM reval vs
local (\ TCContext
ce -> TCContext
ce { context = (context ce) { cxt = cx' }
, environ = en' }) $ cont vs'
addPattern :: forall a.
Val
-> Pattern
-> Env
-> (Val -> Val -> Env -> TypeCheck a)
-> TypeCheck a
addPattern tv :: Val
tv@(VQuant PiSigma
Pi Name
x Domain
dom Val
fv) Pattern
p Env
rho Val -> Val -> Env -> TypeCheck a
cont =
case Pattern
p of
VarP Name
y -> Name
-> Domain
-> Val
-> (Int -> Val -> Val -> TypeCheck a)
-> TypeCheck a
forall a.
Name
-> Domain
-> Val
-> (Int -> Val -> Val -> TypeCheck a)
-> TypeCheck a
underAbs Name
y Domain
dom Val
fv ((Int -> Val -> Val -> TypeCheck a) -> TypeCheck a)
-> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Int
_ Val
xv Val
bv -> do
Val -> Val -> Env -> TypeCheck a
cont Val
bv Val
xv (Env -> Name -> Val -> Env
forall a. Environ a -> Name -> a -> Environ a
update Env
rho Name
y Val
xv)
SizeP Expr
e Name
y -> Name
-> Domain
-> Val
-> (Int -> Val -> Val -> TypeCheck a)
-> TypeCheck a
forall a.
Name
-> Domain
-> Val
-> (Int -> Val -> Val -> TypeCheck a)
-> TypeCheck a
underAbs Name
y Domain
dom Val
fv ((Int -> Val -> Val -> TypeCheck a) -> TypeCheck a)
-> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Int
j Val
xv Val
bv -> do
ve <- Expr
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
whnf' Expr
e
addBoundHyp (Bound Lt (Measure [xv]) (Measure [ve])) $
cont bv xv (update rho y xv)
ConP PatternInfo
pi QName
n [Pattern]
pl -> do
sige <- QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
n
vc <- conLType n (typ dom)
addPatterns vc pl rho $ \ Val
vc' [Val]
vpl Env
rho -> do
pv0 <- Dotted
-> ConK
-> QName
-> [Val]
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
mkConVal Dotted
notDotted (PatternInfo -> ConK
coPat PatternInfo
pi) QName
n [Val]
vpl Val
vc
pv <- up False pv0 (typ dom)
vb <- app fv pv
cont vb pv rho
SuccP Pattern
p2 -> do
Val
-> Pattern
-> Env
-> (Val -> Val -> Env -> TypeCheck a)
-> TypeCheck a
forall a.
Val
-> Pattern
-> Env
-> (Val -> Val -> Env -> TypeCheck a)
-> TypeCheck a
forall (m :: * -> *) a.
MonadCxt m =>
Val -> Pattern -> Env -> (Val -> Val -> Env -> m a) -> m a
addPattern (Val
vSize Val -> Val -> Val
`arrow` Val
vSize) Pattern
p2 Env
rho ((Val -> Val -> Env -> TypeCheck a) -> TypeCheck a)
-> (Val -> Val -> Env -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Val
_ Val
vp2 Env
rho -> do
let pv :: Val
pv = Val -> Val
succSize Val
vp2
vb <- Val
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
app Val
fv Val
pv
cont vb pv rho
ErasedP Pattern
p -> Val
-> Pattern
-> Env
-> (Val -> Val -> Env -> TypeCheck a)
-> TypeCheck a
forall a.
Val
-> Pattern
-> Env
-> (Val -> Val -> Env -> TypeCheck a)
-> TypeCheck a
forall (m :: * -> *) a.
MonadCxt m =>
Val -> Pattern -> Env -> (Val -> Val -> Env -> m a) -> m a
addPattern Val
tv Pattern
p Env
rho Val -> Val -> Env -> TypeCheck a
cont
DotP Expr
e -> do
v <- Env
-> Expr
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
whnf Env
rho Expr
e
vb <- app fv v
cont vb v rho
addPatterns :: forall a.
Val
-> [Pattern]
-> Env
-> (Val -> [Val] -> Env -> TypeCheck a)
-> TypeCheck a
addPatterns Val
tv [] Env
rho Val -> [Val] -> Env -> TypeCheck a
cont = Val -> [Val] -> Env -> TypeCheck a
cont Val
tv [] Env
rho
addPatterns Val
tv (Pattern
p:[Pattern]
ps) Env
rho Val -> [Val] -> Env -> TypeCheck a
cont =
Val
-> Pattern
-> Env
-> (Val -> Val -> Env -> TypeCheck a)
-> TypeCheck a
forall a.
Val
-> Pattern
-> Env
-> (Val -> Val -> Env -> TypeCheck a)
-> TypeCheck a
forall (m :: * -> *) a.
MonadCxt m =>
Val -> Pattern -> Env -> (Val -> Val -> Env -> m a) -> m a
addPattern Val
tv Pattern
p Env
rho ((Val -> Val -> Env -> TypeCheck a) -> TypeCheck a)
-> (Val -> Val -> Env -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Val
tv' Val
v Env
env ->
Val
-> [Pattern]
-> Env
-> (Val -> [Val] -> Env -> TypeCheck a)
-> TypeCheck a
forall a.
Val
-> [Pattern]
-> Env
-> (Val -> [Val] -> Env -> TypeCheck a)
-> TypeCheck a
forall (m :: * -> *) a.
MonadCxt m =>
Val -> [Pattern] -> Env -> (Val -> [Val] -> Env -> m a) -> m a
addPatterns Val
tv' [Pattern]
ps Env
env ((Val -> [Val] -> Env -> TypeCheck a) -> TypeCheck a)
-> (Val -> [Val] -> Env -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Val
tv'' [Val]
vs Env
env' ->
Val -> [Val] -> Env -> TypeCheck a
cont Val
tv'' (Val
vVal -> [Val] -> [Val]
forall a. a -> [a] -> [a]
:[Val]
vs) Env
env'
addSizeRel :: forall a. Int -> Int -> Int -> TypeCheck a -> TypeCheck a
addSizeRel Int
son Int
dist Int
father TypeCheck a
k = do
let s :: String
s = String
"v" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
son String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
dist String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <= v" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
father
String -> TypeCheck a -> TypeCheck a
forall (m :: * -> *) a.
MonadError TraceError m =>
String -> m a -> m a
enter
(String
"adding size rel. " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ do
let modBI :: [Int] -> [Int]
modBI [Int]
belowInfty = if Int
father Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
belowInfty Bool -> Bool -> Bool
|| Int
dist Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Int
son Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
belowInfty else [Int]
belowInfty
TypeCheck Bool -> TypeCheck () -> TypeCheck ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((TCContext -> Bool) -> TypeCheck Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCContext -> Bool
consistencyCheck TypeCheck Bool -> TypeCheck Bool -> TypeCheck Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`andLazy` do
Int -> (Int, Int) -> TSO Int -> Bool
forall a. (Ord a, Eq a) => a -> (Int, a) -> TSO a -> Bool
TSO.increasesHeight Int
son (Int
dist, Int
father) (TSO Int -> Bool)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (TSO Int)
-> TypeCheck Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCContext -> TSO Int)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (TSO Int)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCContext -> TSO Int
sizeRels) (TypeCheck () -> TypeCheck ()) -> TypeCheck () -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$ do
String -> TypeCheck ()
forall (m :: * -> *). MonadAssert m => String -> m ()
recoverFail (String -> TypeCheck ()) -> String -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$ String
"cannot add hypothesis " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" because it is not satisfyable under all possible valuations of the current hypotheses"
TypeCheck (Maybe Int) -> (Int -> TypeCheck ()) -> TypeCheck ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (Int -> Int -> TSO Int -> Maybe Int
forall a. (Ord a, Eq a) => a -> a -> TSO a -> Maybe Int
TSO.isAncestor Int
father Int
son (TSO Int -> Maybe Int)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (TSO Int)
-> TypeCheck (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCContext -> TSO Int)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (TSO Int)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCContext -> TSO Int
sizeRels) ((Int -> TypeCheck ()) -> TypeCheck ())
-> (Int -> TypeCheck ()) -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$ \ Int
n ->
Bool -> TypeCheck () -> TypeCheck ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
dist Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> - Int
n) (TypeCheck () -> TypeCheck ()) -> TypeCheck () -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$
String -> TypeCheck ()
forall (m :: * -> *). MonadAssert m => String -> m ()
recoverFail(String -> TypeCheck ()) -> String -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$ String
"cannot add hypothesis " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" because it makes the set of hyptheses unsatisfiable"
(TCContext -> TCContext) -> TypeCheck a -> TypeCheck a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
cxt -> TCContext
cxt
{ sizeRels = TSO.insert son (dist, father) (sizeRels cxt)
, belowInfty = modBI (belowInfty cxt)
}) TypeCheck a
k
addBelowInfty :: forall a. Int -> TypeCheck a -> TypeCheck a
addBelowInfty Int
i = (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a)
-> (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a b. (a -> b) -> a -> b
$ \ TCContext
cxt -> TCContext
cxt { belowInfty = i : belowInfty cxt }
addBoundHyp :: forall a. Bound Val -> TypeCheck a -> TypeCheck a
addBoundHyp beta :: Bound Val
beta@(Bound LtLe
ltle (Measure [Val]
mu) (Measure [Val]
mu')) TypeCheck a
cont =
case (LtLe
ltle, [Val]
mu, [Val]
mu') of
(LtLe
Le, [Val]
_, [Val
VInfty]) -> TypeCheck a
cont
(LtLe
ltle, [Val
v], [Val
v']) -> Int -> Val -> Val -> TypeCheck a
loop (if LtLe
ltleLtLe -> LtLe -> Bool
forall a. Eq a => a -> a -> Bool
==LtLe
Lt then Int
1 else Int
0) Val
v Val
v'
(LtLe, [Val], [Val])
_ -> TypeCheck a
failure
where failure :: TypeCheck a
failure = do
AssertionHandling -> Bool -> TypeCheck Doc -> TypeCheck ()
forall (m :: * -> *).
(MonadError TraceError m, MonadIO m) =>
AssertionHandling -> Bool -> m Doc -> m ()
assertDoc' AssertionHandling
Warning Bool
False (String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text String
"hypothetical constraint" TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> Bound Val -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM Bound Val
beta TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text String
"ignored")
TypeCheck a
cont
loop :: Int -> Val -> Val -> TypeCheck a
loop Int
n (VGen Int
i) Val
VInfty = Int -> TypeCheck a -> TypeCheck a
forall a. Int -> TypeCheck a -> TypeCheck a
forall (m :: * -> *) a. MonadCxt m => Int -> m a -> m a
addBelowInfty Int
i TypeCheck a
cont
loop Int
n (VGen Int
i) (VGen Int
j) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Int -> Int -> Int -> TypeCheck a -> TypeCheck a
forall a. Int -> Int -> Int -> TypeCheck a -> TypeCheck a
forall (m :: * -> *) a.
MonadCxt m =>
Int -> Int -> Int -> m a -> m a
addSizeRel Int
i Int
n Int
j TypeCheck a
cont
| Bool
otherwise = Int -> Int -> Int -> TypeCheck a -> TypeCheck a
forall {m :: * -> *} {a}.
MonadReader TCContext m =>
Int -> Int -> Int -> m a -> m a
addIrregularBound Int
i Int
j (-Int
n) TypeCheck a
cont
loop Int
n (VSucc Val
v) Val
v' = Int -> Val -> Val -> TypeCheck a
loop (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Val
v Val
v'
loop Int
n Val
v (VSucc Val
v') = Int -> Val -> Val -> TypeCheck a
loop (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Val
v Val
v'
loop Int
_ Val
_ Val
_ = TypeCheck a
failure
addIrregularBound :: Int -> Int -> Int -> m a -> m a
addIrregularBound Int
i Int
j Int
n = (TCContext -> TCContext) -> m a -> m a
forall a. (TCContext -> TCContext) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
ce -> TCContext
ce { bounds = beta : bounds ce }) where
v' :: Val
v' = (Val -> Val) -> Val -> [Val]
forall a. (a -> a) -> a -> [a]
iterate Val -> Val
VSucc (Int -> Val
VGen Int
j) [Val] -> Int -> Val
forall a. HasCallStack => [a] -> Int -> a
!! Int
n
beta :: Bound Val
beta = LtLe -> Measure Val -> Measure Val -> Bound Val
forall a. LtLe -> Measure a -> Measure a -> Bound a
Bound LtLe
Le ([Val] -> Measure Val
forall a. [a] -> Measure a
Measure [Int -> Val
VGen Int
i]) ([Val] -> Measure Val
forall a. [a] -> Measure a
Measure [Val
v'])
isBelowInfty :: Int -> TypeCheck Bool
isBelowInfty Int
i = (Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([Int] -> Bool)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Int]
-> TypeCheck Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCContext -> [Int])
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Int]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCContext -> [Int]
belowInfty
sizeVarBelow :: Int -> Int -> TypeCheck (Maybe Int)
sizeVarBelow Int
son Int
ancestor = do
cxt <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
return $ TSO.isAncestor son ancestor (sizeRels cxt)
getMinSize :: Int -> TypeCheck (Maybe Int)
getMinSize Int
parent = do
cxt <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
return $ TSO.height parent (sizeRels cxt)
getSizeVarsInScope :: TypeCheck [Name]
getSizeVarsInScope = do
TCContext { context = delta, naming = nam } <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
let fSize (a
i, OneOrTwo Domain
tv12) =
case OneOrTwo Domain
tv12 of
One Domain
dom -> Val -> Bool
isVSize (Val -> Bool) -> Val -> Bool
forall a b. (a -> b) -> a -> b
$ Domain -> Val
forall a. Dom a -> a
typ Domain
dom
OneOrTwo Domain
_ ->
Bool
False
let idl = ((Int, OneOrTwo Domain) -> Bool)
-> [(Int, OneOrTwo Domain)] -> [(Int, OneOrTwo Domain)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int, OneOrTwo Domain) -> Bool
forall {a}. (a, OneOrTwo Domain) -> Bool
fSize ([(Int, OneOrTwo Domain)] -> [(Int, OneOrTwo Domain)])
-> [(Int, OneOrTwo Domain)] -> [(Int, OneOrTwo Domain)]
forall a b. (a -> b) -> a -> b
$ Context2 Domain -> [(Int, OneOrTwo Domain)]
forall k a. Map k a -> [(k, a)]
Map.toAscList (SemCxt -> Context2 Domain
cxt SemCxt
delta)
let udecs = SemCxt -> Context UDec
upperDecs SemCxt
delta
let fPos (Int
i, One Dom a
dom) =
case PProd -> Maybe Pol
fromPProd (UDec -> PProd
forall pol. Polarity pol => Decoration pol -> pol
polarity (Maybe UDec -> UDec
forall a. HasCallStack => Maybe a -> a
Maybe.fromJust (Int -> Context UDec -> Maybe UDec
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i Context UDec
udecs))) of
Just Pol
p -> Pol -> Pol -> Bool
leqPol (Dec -> Pol
forall pol. Polarity pol => Decoration pol -> pol
polarity (Dom a -> Dec
forall a. Dom a -> Dec
decor Dom a
dom)) Pol
p
Maybe Pol
Nothing -> Bool
False
let fName (Int
i, b
_) = Maybe Name -> Name
forall a. HasCallStack => Maybe a -> a
Maybe.fromJust (Maybe Name -> Name) -> Maybe Name -> Name
forall a b. (a -> b) -> a -> b
$ Int -> Map Int Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i Map Int Name
nam
return $ map fName $ filter fPos idl
checkingCon :: forall a. Bool -> TypeCheck a -> TypeCheck a
checkingCon Bool
b = (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
cxt -> TCContext
cxt { checkingConType = b})
checkingDom :: forall a. TypeCheck a -> TypeCheck a
checkingDom TypeCheck a
k = do
b <- (TCContext -> Bool) -> TypeCheck Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TCContext -> Bool
checkingConType
if b then k else applyDec (Dec Neg) k
setCo :: forall a. Co -> TypeCheck a -> TypeCheck a
setCo Co
co = (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
cxt -> TCContext
cxt { mutualCo = co })
installFuns :: forall a. Co -> [Kinded Fun] -> TypeCheck a -> TypeCheck a
installFuns Co
co [Kinded Fun]
kfuns TypeCheck a
k = do
let funt :: Map Name (Kinded Fun)
funt = (Map Name (Kinded Fun) -> Kinded Fun -> Map Name (Kinded Fun))
-> Map Name (Kinded Fun) -> [Kinded Fun] -> Map Name (Kinded Fun)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ Map Name (Kinded Fun)
m fun :: Kinded Fun
fun@(Kinded Kind
_ (Fun (TypeSig Name
n Expr
_) Name
n' Arity
_ [Clause]
_)) -> Name
-> Kinded Fun -> Map Name (Kinded Fun) -> Map Name (Kinded Fun)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n Kinded Fun
fun Map Name (Kinded Fun)
m)
Map Name (Kinded Fun)
forall k a. Map k a
Map.empty
[Kinded Fun]
kfuns
(TCContext -> TCContext) -> TypeCheck a -> TypeCheck a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
cxt -> TCContext
cxt { mutualCo = co, funsTemplate = funt }) TypeCheck a
k
setMeasure :: forall a. Measure Val -> TypeCheck a -> TypeCheck a
setMeasure Measure Val
mu TypeCheck a
k = do
rho0 <- TypeCheck Env
forall (m :: * -> *). MonadCxt m => m Env
getEnv
let rho = Env
rho0 { envBound = Just mu }
local (\ TCContext
cxt -> TCContext
cxt
{ environ = (environ cxt) { envBound = Just mu }
}) k
activateFuns :: forall a. TypeCheck a -> TypeCheck a
activateFuns TypeCheck a
k = do
rho <- TypeCheck Env
forall (m :: * -> *). MonadCxt m => m Env
getEnv
case (envBound rho) of
Maybe (Measure Val)
Nothing -> TypeCheck a
k
Just Measure Val
mu ->
(TCContext -> TCContext) -> TypeCheck a -> TypeCheck a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
cxt -> TCContext
cxt
{ mutualFuns =
Map.map (boundFun rho (mutualCo cxt)) (funsTemplate cxt)
}) TypeCheck a
k
where boundFun :: Env -> Co -> Kinded Fun -> SigDef
boundFun :: Env -> Co -> Kinded Fun -> SigDef
boundFun Env
rho Co
co (Kinded Kind
ki (Fun (TypeSig Name
n Expr
t) Name
n' Arity
ar [Clause]
cls)) =
Co -> Val -> Kind -> Arity -> [Clause] -> Bool -> Expr -> SigDef
FunSig Co
co (Env -> Expr -> Val
VClos Env
rho Expr
t) Kind
ki Arity
ar [Clause]
cls Bool
False Expr
forall a. HasCallStack => a
undefined
goImpredicative :: forall a. TypeCheck a -> TypeCheck a
goImpredicative = (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
cxt -> TCContext
cxt { impredicative = True })
checkingMutual :: forall a. Maybe DefId -> TypeCheck a -> TypeCheck a
checkingMutual Maybe DefId
mn = (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ TCContext
cxt -> TCContext
cxt { checkingMutualName = mn })
underAbs :: Name -> Domain -> FVal -> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a
underAbs :: forall a.
Name
-> Domain
-> Val
-> (Int -> Val -> Val -> TypeCheck a)
-> TypeCheck a
underAbs Name
x Domain
dom Val
fv Int -> Val -> Val -> TypeCheck a
cont = Name -> Domain -> (Int -> Val -> TypeCheck a) -> TypeCheck a
forall a.
Name -> Domain -> (Int -> Val -> TypeCheck a) -> TypeCheck a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> Domain -> (Int -> Val -> m a) -> m a
newWithGen Name
x Domain
dom ((Int -> Val -> TypeCheck a) -> TypeCheck a)
-> (Int -> Val -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Int
i Val
xv -> Int -> Val -> Val -> TypeCheck a
cont Int
i Val
xv (Val -> TypeCheck a)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> TypeCheck a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Val
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
app Val
fv Val
xv
underAbs_ :: Name -> Domain -> FVal -> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a
underAbs_ :: forall a.
Name
-> Domain
-> Val
-> (Int -> Val -> Val -> TypeCheck a)
-> TypeCheck a
underAbs_ Name
x Domain
dom Val
fv Int -> Val -> Val -> TypeCheck a
cont = TypeCheck a -> TypeCheck a
forall a. TypeCheck a -> TypeCheck a
noConsistencyChecking (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ Name
-> Domain
-> Val
-> (Int -> Val -> Val -> TypeCheck a)
-> TypeCheck a
forall a.
Name
-> Domain
-> Val
-> (Int -> Val -> Val -> TypeCheck a)
-> TypeCheck a
underAbs Name
x Domain
dom Val
fv Int -> Val -> Val -> TypeCheck a
cont
noConsistencyChecking :: TypeCheck a -> TypeCheck a
noConsistencyChecking :: forall a. TypeCheck a -> TypeCheck a
noConsistencyChecking = (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a.
(TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a)
-> (TCContext -> TCContext)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a b. (a -> b) -> a -> b
$ \ TCContext
cxt -> TCContext
cxt { consistencyCheck = False }
underAbs' :: Name -> FVal -> (Val -> Val -> TypeCheck a) -> TypeCheck a
underAbs' :: forall a. Name -> Val -> (Val -> Val -> TypeCheck a) -> TypeCheck a
underAbs' Name
x Val
fv Val -> Val -> TypeCheck a
cont = Name -> (Val -> TypeCheck a) -> TypeCheck a
forall a. Name -> (Val -> TypeCheck a) -> TypeCheck a
forall (m :: * -> *) a. MonadCxt m => Name -> (Val -> m a) -> m a
addName Name
x ((Val -> TypeCheck a) -> TypeCheck a)
-> (Val -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Val
xv -> Val -> Val -> TypeCheck a
cont Val
xv (Val -> TypeCheck a)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> TypeCheck a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Val
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
app Val
fv Val
xv
addBind :: TBind -> TypeCheck a -> TypeCheck a
addBind :: forall a. TBind -> TypeCheck a -> TypeCheck a
addBind (TBind Name
x Dom Expr
dom) TypeCheck a
cont = do
dom' <- ((Expr
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> Dom Expr
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) Domain
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom a -> m (Dom b)
Traversable.mapM Expr
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
whnf' Dom Expr
dom)
new' x dom' cont
addBinds :: Telescope -> TypeCheck a -> TypeCheck a
addBinds :: forall a. Telescope -> TypeCheck a -> TypeCheck a
addBinds Telescope
tel TypeCheck a
k0 = (TBind -> TypeCheck a -> TypeCheck a)
-> TypeCheck a -> [TBind] -> TypeCheck a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TBind -> TypeCheck a -> TypeCheck a
forall a. TBind -> TypeCheck a -> TypeCheck a
addBind TypeCheck a
k0 ([TBind] -> TypeCheck a) -> [TBind] -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ Telescope -> [TBind]
telescope Telescope
tel
introPatterns :: [Pattern] -> TVal -> ([(Pattern,Val)] -> TVal -> TypeCheck a) -> TypeCheck a
introPatterns :: forall a.
[Pattern]
-> Val -> ([(Pattern, Val)] -> Val -> TypeCheck a) -> TypeCheck a
introPatterns [Pattern]
ps Val
tv [(Pattern, Val)] -> Val -> TypeCheck a
cont =
[Pattern] -> TypeCheck a -> TypeCheck a
forall a. [Pattern] -> TypeCheck a -> TypeCheck a
introPatVars [Pattern]
ps (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ do
vs <- (Pattern
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> [Pattern]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Val]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Expr
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
whnf' (Expr
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> (Pattern -> Expr)
-> Pattern
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> Expr
patternToExpr) [Pattern]
ps
let pvs = [Pattern] -> [Val] -> [(Pattern, Val)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Pattern]
ps [Val]
vs
introPatTypes pvs tv (cont pvs)
introPatVar :: Pattern -> TypeCheck a -> TypeCheck a
introPatVar :: forall a. Pattern -> TypeCheck a -> TypeCheck a
introPatVar Pattern
p TypeCheck a
cont =
case Pattern
p of
VarP Name
n -> Name -> (Val -> TypeCheck a) -> TypeCheck a
forall a. Name -> (Val -> TypeCheck a) -> TypeCheck a
forall (m :: * -> *) a. MonadCxt m => Name -> (Val -> m a) -> m a
addName Name
n ((Val -> TypeCheck a) -> TypeCheck a)
-> (Val -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Val
_ -> TypeCheck a
cont
SizeP Expr
m Name
n -> Name -> (Val -> TypeCheck a) -> TypeCheck a
forall a. Name -> (Val -> TypeCheck a) -> TypeCheck a
forall (m :: * -> *) a. MonadCxt m => Name -> (Val -> m a) -> m a
addName Name
n ((Val -> TypeCheck a) -> TypeCheck a)
-> (Val -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Val
_ -> TypeCheck a
cont
ConP PatternInfo
co QName
n [Pattern]
pl -> [Pattern] -> TypeCheck a -> TypeCheck a
forall a. [Pattern] -> TypeCheck a -> TypeCheck a
introPatVars [Pattern]
pl TypeCheck a
cont
PairP Pattern
p1 Pattern
p2 -> [Pattern] -> TypeCheck a -> TypeCheck a
forall a. [Pattern] -> TypeCheck a -> TypeCheck a
introPatVars [Pattern
p1,Pattern
p2] TypeCheck a
cont
SuccP Pattern
p -> Pattern -> TypeCheck a -> TypeCheck a
forall a. Pattern -> TypeCheck a -> TypeCheck a
introPatVar Pattern
p TypeCheck a
cont
ProjP{} -> TypeCheck a
cont
DotP Expr
e -> TypeCheck a
cont
Pattern
AbsurdP -> TypeCheck a
cont
ErasedP Pattern
p -> Pattern -> TypeCheck a -> TypeCheck a
forall a. Pattern -> TypeCheck a -> TypeCheck a
introPatVar Pattern
p TypeCheck a
cont
introPatVars :: [Pattern] -> TypeCheck a -> TypeCheck a
introPatVars :: forall a. [Pattern] -> TypeCheck a -> TypeCheck a
introPatVars [] TypeCheck a
cont = TypeCheck a
cont
introPatVars (Pattern
p:[Pattern]
ps) TypeCheck a
cont = Pattern -> TypeCheck a -> TypeCheck a
forall a. Pattern -> TypeCheck a -> TypeCheck a
introPatVar Pattern
p (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ [Pattern] -> TypeCheck a -> TypeCheck a
forall a. [Pattern] -> TypeCheck a -> TypeCheck a
introPatVars [Pattern]
ps (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ TypeCheck a
cont
introPatType :: (Pattern,Val) -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a
introPatType :: forall a.
(Pattern, Val) -> Val -> (Val -> TypeCheck a) -> TypeCheck a
introPatType (Pattern
p,Val
v) Val
tv Val -> TypeCheck a
cont = do
case Val
tv of
VGuard Bound Val
beta Val
bv -> Bound Val -> TypeCheck a -> TypeCheck a
forall a. Bound Val -> TypeCheck a -> TypeCheck a
forall (m :: * -> *) a. MonadCxt m => Bound Val -> m a -> m a
addBoundHyp Bound Val
beta (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ (Pattern, Val) -> Val -> (Val -> TypeCheck a) -> TypeCheck a
forall a.
(Pattern, Val) -> Val -> (Val -> TypeCheck a) -> TypeCheck a
introPatType (Pattern
p,Val
v) Val
bv Val -> TypeCheck a
cont
VApp (VDef (DefId IdKind
DatK QName
d)) [Val]
vl ->
case Pattern
p of
ProjP Name
n -> Val -> TypeCheck a
cont (Val -> TypeCheck a)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> TypeCheck a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Val
-> Name
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
projectType Val
tv Name
n Val
VIrr
Pattern
_ -> String -> TypeCheck a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck a) -> String -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ String
"introPatType: internal error, expected projection pattern, found " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern -> String
forall a. Show a => a -> String
show Pattern
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" at type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
tv
VQuant PiSigma
Pi Name
x Domain
dom Val
fv -> do
v <- Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
whnfClos Val
v
matchPatType (p,v) dom . cont =<< app fv v
Val
_ -> String -> TypeCheck a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck a) -> String -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ String
"introPatType: internal error, expected Pi-type, found " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
tv
introPatTypes :: [(Pattern,Val)] -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a
introPatTypes :: forall a.
[(Pattern, Val)] -> Val -> (Val -> TypeCheck a) -> TypeCheck a
introPatTypes [(Pattern, Val)]
pvs Val
tv Val -> TypeCheck a
f = do
case [(Pattern, Val)]
pvs of
[] -> Val -> TypeCheck a
f Val
tv
((Pattern, Val)
pv:[(Pattern, Val)]
pvs') -> (Pattern, Val) -> Val -> (Val -> TypeCheck a) -> TypeCheck a
forall a.
(Pattern, Val) -> Val -> (Val -> TypeCheck a) -> TypeCheck a
introPatType (Pattern, Val)
pv Val
tv ((Val -> TypeCheck a) -> TypeCheck a)
-> (Val -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Val
tv' -> [(Pattern, Val)] -> Val -> (Val -> TypeCheck a) -> TypeCheck a
forall a.
[(Pattern, Val)] -> Val -> (Val -> TypeCheck a) -> TypeCheck a
introPatTypes [(Pattern, Val)]
pvs' Val
tv' Val -> TypeCheck a
f
matchPatType :: (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
matchPatType :: forall a. (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
matchPatType (Pattern
p,Val
v) Domain
dom TypeCheck a
cont =
case (Pattern
p,Val
v) of
(VarP Name
y, VGen Int
k) -> Int -> Domain -> TypeCheck a -> TypeCheck a
forall a. Int -> Domain -> TypeCheck a -> TypeCheck a
forall (m :: * -> *) a. MonadCxt m => Int -> Domain -> m a -> m a
setType Int
k Domain
dom (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ TypeCheck a
cont
(SizeP Expr
z Name
y, VGen Int
k) -> Int -> Domain -> TypeCheck a -> TypeCheck a
forall a. Int -> Domain -> TypeCheck a -> TypeCheck a
forall (m :: * -> *) a. MonadCxt m => Int -> Domain -> m a -> m a
setType Int
k Domain
dom (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ TypeCheck a
cont
(ConP PatternInfo
co QName
n [], Val
_) -> TypeCheck a
cont
(ConP PatternInfo
co QName
n [Pattern]
pl, VApp (VDef (DefId ConK{} QName
_)) [Val]
vl) -> do
vc <- QName
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
conType QName
n (Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
force (Domain -> Val
forall a. Dom a -> a
typ Domain
dom)
introPatTypes (zip pl vl) vc $ \ Val
_ -> TypeCheck a
cont
(SuccP Pattern
p2, VSucc Val
v2) -> (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
forall a. (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
matchPatType (Pattern
p2, Val
v2) (Val -> Domain
forall a. a -> Dom a
defaultDomain Val
vSize) (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ TypeCheck a
cont
(PairP Pattern
p1 Pattern
p2, VPair Val
v1 Val
v2) -> do
av <- Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
force (Domain -> Val
forall a. Dom a -> a
typ Domain
dom)
case av of
VQuant PiSigma
Sigma Name
x dom1 :: Domain
dom1@(Domain Val
av1 Kind
ki Dec
dec) Val
fv -> do
(Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
forall a. (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
matchPatType (Pattern
p1,Val
v1) Domain
dom1 (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ do
bv <- Val
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
app Val
fv Val
v1
matchPatType (p2,v2) (Domain bv ki dec) cont
Val
_ -> String -> TypeCheck a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck a) -> String -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ String
"matchPatType: IMPOSSIBLE " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern -> String
forall a. Show a => a -> String
show Pattern
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Domain -> String
forall a. Show a => a -> String
show Domain
dom
(DotP Expr
e, Val
_) -> TypeCheck a
cont
(Pattern
AbsurdP, Val
_) -> TypeCheck a
cont
(ErasedP Pattern
p,Val
_) -> (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
forall a. (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
matchPatType (Pattern
p,Val
v) Domain
dom TypeCheck a
cont
(Pattern, Val)
_ -> String -> TypeCheck a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck a) -> String -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ String
"matchPatType: IMPOSSIBLE " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Pattern, Val) -> String
forall a. Show a => a -> String
show (Pattern
p,Val
v)
type Signature = Map QName SigDef
data SigDef
= FunSig { SigDef -> Co
isCo :: Co
, SigDef -> Val
symbTyp :: TVal
, SigDef -> Kind
symbolKind :: Kind
, SigDef -> Arity
arity :: Arity
, SigDef -> [Clause]
clauses :: [Clause]
, SigDef -> Bool
isTypeChecked :: Bool
, SigDef -> Expr
extrTyp :: Expr
}
| LetSig { symbTyp :: TVal
, symbolKind :: Kind
, SigDef -> Val
definingVal :: Val
, extrTyp :: Expr
}
| PatSig { SigDef -> [Name]
patVars :: [Name]
, SigDef -> Pattern
definingPat :: Pattern
, definingVal :: Val
}
| ConSig { SigDef -> ConPars
conPars :: ConPars
, SigDef -> LHSType
lhsTyp :: LHSType
, SigDef -> [Bool]
recOccs :: [Bool]
, symbTyp :: TVal
, SigDef -> Name
dataName :: Name
, SigDef -> Int
dataPars :: Int
, extrTyp :: Expr
}
| DataSig { SigDef -> Int
numPars :: Int
, SigDef -> [Pol]
positivity :: [Pol]
, SigDef -> Sized
isSized :: Sized
, isCo :: Co
, symbTyp :: TVal
, symbolKind :: Kind
, SigDef -> [ConstructorInfo]
constructors :: [ConstructorInfo]
, SigDef -> Bool
etaExpand :: Bool
, SigDef -> Bool
isTuple :: Bool
, extrTyp :: Expr
}
deriving (Int -> SigDef -> ShowS
[SigDef] -> ShowS
SigDef -> String
(Int -> SigDef -> ShowS)
-> (SigDef -> String) -> ([SigDef] -> ShowS) -> Show SigDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SigDef -> ShowS
showsPrec :: Int -> SigDef -> ShowS
$cshow :: SigDef -> String
show :: SigDef -> String
$cshowList :: [SigDef] -> ShowS
showList :: [SigDef] -> ShowS
Show)
type ConPars = Maybe ([Name], [Pattern])
type LHSType = Maybe (Name, TVal)
isEmptyData :: QName -> TypeCheck Bool
isEmptyData :: QName -> TypeCheck Bool
isEmptyData QName
n = do
sig <- QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
n
case sig of
DataSig { [ConstructorInfo]
constructors :: SigDef -> [ConstructorInfo]
constructors :: [ConstructorInfo]
constructors } -> Bool -> TypeCheck Bool
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TypeCheck Bool) -> Bool -> TypeCheck Bool
forall a b. (a -> b) -> a -> b
$ [ConstructorInfo] -> Bool
forall a. Null a => a -> Bool
null [ConstructorInfo]
constructors
SigDef
_ -> String -> TypeCheck Bool
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck Bool) -> String -> TypeCheck Bool
forall a b. (a -> b) -> a -> b
$ String
"internal error: isEmptyData " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": name of data type expected"
isUnitData :: QName -> TypeCheck Bool
isUnitData :: QName -> TypeCheck Bool
isUnitData QName
n = do
sig <- QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
n
case sig of
DataSig { constructors :: SigDef -> [ConstructorInfo]
constructors = [ConstructorInfo
c], Bool
isTuple :: SigDef -> Bool
isTuple :: Bool
isTuple } -> Bool -> TypeCheck Bool
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TypeCheck Bool) -> Bool -> TypeCheck Bool
forall a b. (a -> b) -> a -> b
$
Bool
isTuple Bool -> Bool -> Bool
&& [FieldInfo] -> Bool
forall a. Null a => a -> Bool
null (ConstructorInfo -> [FieldInfo]
cFields ConstructorInfo
c) Bool -> Bool -> Bool
&& ConstructorInfo -> (PatternsType, [Pattern])
cPatFam ConstructorInfo
c (PatternsType, [Pattern]) -> (PatternsType, [Pattern]) -> Bool
forall a. Eq a => a -> a -> Bool
== (PatternsType
LinearPatterns, [])
DataSig { [ConstructorInfo]
constructors :: SigDef -> [ConstructorInfo]
constructors :: [ConstructorInfo]
constructors } -> Bool -> TypeCheck Bool
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
SigDef
_ -> String -> TypeCheck Bool
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck Bool) -> String -> TypeCheck Bool
forall a b. (a -> b) -> a -> b
$ String
"internal error: isUnitData " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": name of data type expected"
undefinedFType :: QName -> Expr
undefinedFType :: QName -> Expr
undefinedFType QName
n = Expr
Irr
symbKind :: SigDef -> Kind
symbKind :: SigDef -> Kind
symbKind ConSig{} = Kind
kTerm
symbKind SigDef
d = SigDef -> Kind
symbolKind SigDef
d
emptySig :: Signature
emptySig :: Signature
emptySig = Signature
forall k a. Map k a
Map.empty
data DataView
= Data Name [Clos]
| NoData
dataView :: TVal -> TypeCheck DataView
dataView :: Val -> TypeCheck DataView
dataView Val
tv = do
tv <- Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
force Val
tv
case tv of
VApp (VDef (DefId IdKind
DatK QName
n)) [Val]
vs -> DataView -> TypeCheck DataView
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DataView -> TypeCheck DataView) -> DataView -> TypeCheck DataView
forall a b. (a -> b) -> a -> b
$ Name -> [Val] -> DataView
Data (QName -> Name
unqual QName
n) [Val]
vs
VSing Val
v Val
dv -> Val -> TypeCheck DataView
dataView (Val -> TypeCheck DataView)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> TypeCheck DataView
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
whnfClos Val
dv
Val
_ -> DataView -> TypeCheck DataView
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DataView -> TypeCheck DataView) -> DataView -> TypeCheck DataView
forall a b. (a -> b) -> a -> b
$ DataView
NoData
disambigCon :: QName -> TVal -> TypeCheck QName
disambigCon :: QName -> Val -> TypeCheck QName
disambigCon QName
c Val
tv =
case QName
c of
Qual{} -> QName -> TypeCheck QName
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
c
QName Name
n -> do
dv <- Val -> TypeCheck DataView
dataView Val
tv
case dv of
Data Name
d [Val]
_ -> QName -> TypeCheck QName
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> TypeCheck QName) -> QName -> TypeCheck QName
forall a b. (a -> b) -> a -> b
$ Name -> Name -> QName
Qual Name
d Name
n
DataView
_ -> String -> TypeCheck QName
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck QName) -> String -> TypeCheck QName
forall a b. (a -> b) -> a -> b
$ String
"cannot resolve constructor " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
conType :: QName -> TVal -> TypeCheck TVal
conType :: QName
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
conType QName
c Val
tv = do
c <- QName -> Val -> TypeCheck QName
disambigCon QName
c Val
tv
ConSig { conPars, symbTyp, dataName, dataPars } <- lookupSymbQ c
instConType c conPars symbTyp dataName dataPars tv
conLType :: QName -> TVal -> TypeCheck TVal
conLType :: QName
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
conLType QName
c Val
tv = do
c <- QName -> Val -> TypeCheck QName
disambigCon QName
c Val
tv
ConSig { conPars, lhsTyp, symbTyp, dataName, dataPars } <- lookupSymbQ c
case lhsTyp of
LHSType
Nothing -> QName
-> ConPars
-> Val
-> Name
-> Int
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
instConType QName
c ConPars
conPars Val
symbTyp Name
dataName Int
dataPars Val
tv
Just (Name
x, Val
lTyp) -> QName
-> ConPars
-> Val
-> Name
-> Int
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
instConType QName
c ((([Name], [Pattern]) -> ([Name], [Pattern])) -> ConPars -> ConPars
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> ([Name], [Pattern]) -> ([Name], [Pattern])
forall {e}. Name -> ([Name], [Pat e]) -> ([Name], [Pat e])
inc Name
x) ConPars
conPars) Val
lTyp Name
dataName (Int
dataParsInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Val
tv
where inc :: Name -> ([Name], [Pat e]) -> ([Name], [Pat e])
inc Name
x ([Name]
xs, [Pat e]
ps) = ([Name]
xs [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
x], [Pat e]
ps [Pat e] -> [Pat e] -> [Pat e]
forall a. [a] -> [a] -> [a]
++ [Name -> Pat e
forall e. Name -> Pat e
VarP Name
x])
instConType :: QName -> ConPars -> TVal -> Name -> Int -> TVal -> TypeCheck TVal
instConType :: QName
-> ConPars
-> Val
-> Name
-> Int
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
instConType QName
c ConPars
conPars Val
symbTyp Name
dataName Int
dataPars Val
tv =
QName
-> ConPars
-> Val
-> Maybe ((Name, Val), Val -> Bool)
-> Maybe Name
-> Int
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
instConLType' QName
c ConPars
conPars Val
symbTyp Maybe ((Name, Val), Val -> Bool)
forall a. Maybe a
Nothing (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
dataName) Int
dataPars Val
tv
instConLType :: QName -> ConPars -> TVal -> LHSType -> (Val -> Bool) -> Int -> TVal -> TypeCheck TVal
instConLType :: QName
-> ConPars
-> Val
-> LHSType
-> (Val -> Bool)
-> Int
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
instConLType QName
c ConPars
conPars Val
rhsTyp LHSType
lhsTyp Val -> Bool
isFlex Int
dataPars Val
dataTyp =
QName
-> ConPars
-> Val
-> Maybe ((Name, Val), Val -> Bool)
-> Maybe Name
-> Int
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
instConLType' QName
c ConPars
conPars Val
rhsTyp (((Name, Val) -> ((Name, Val), Val -> Bool))
-> LHSType -> Maybe ((Name, Val), Val -> Bool)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Val -> Bool
isFlex) LHSType
lhsTyp) Maybe Name
forall a. Maybe a
Nothing Int
dataPars Val
dataTyp
instConLType' :: QName -> ConPars -> TVal -> Maybe ((Name, TVal), Val -> Bool) -> Maybe Name -> Int -> TVal -> TypeCheck TVal
instConLType' :: QName
-> ConPars
-> Val
-> Maybe ((Name, Val), Val -> Bool)
-> Maybe Name
-> Int
-> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
instConLType' QName
c ConPars
conPars Val
symbTyp Maybe ((Name, Val), Val -> Bool)
isSized Maybe Name
md Int
dataPars Val
tv =
String
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall (m :: * -> *) a.
MonadError TraceError m =>
String -> m a -> m a
enter (String
"instConLType'") (StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall a b. (a -> b) -> a -> b
$ do
let failure :: StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
failure = TypeCheck Doc
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadError TraceError m => m Doc -> m a
failDoc (String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text (String
"conType " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": expected")
TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> Val -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM Val
tv
TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text (String
"to be a data type applied to all of its " String -> ShowS
forall a. [a] -> [a] -> [a]
++
Int -> String
forall a. Show a => a -> String
show Int
dataPars String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" parameters"))
dv <- Val -> TypeCheck DataView
dataView Val
tv
case dv of
DataView
NoData -> TypeCheck Doc
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall (m :: * -> *) a. MonadError TraceError m => m Doc -> m a
failDoc (String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text (String
"conType " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": expected")
TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> Val -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM Val
tv TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text String
"to be a data type")
Data Name
d [Val]
vs -> do
Maybe Name -> (Name -> TypeCheck ()) -> TypeCheck ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Name
md ((Name -> TypeCheck ()) -> TypeCheck ())
-> (Name -> TypeCheck ()) -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$ \ Name
d' ->
Bool -> TypeCheck () -> TypeCheck ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Name
d Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
d') (TypeCheck () -> TypeCheck ()) -> TypeCheck () -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$ String -> TypeCheck ()
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck ()) -> String -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$ String
"expected constructor of datatype " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", but found one of datatype " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
d'
let ([Val]
pars, [Val]
inds) = Int -> [Val] -> ([Val], [Val])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
dataPars [Val]
vs
Bool -> TypeCheck () -> TypeCheck ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Val] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
pars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
dataPars) TypeCheck ()
forall {a}.
StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
failure
case (Maybe ((Name, Val), Val -> Bool)
isSized, [Val]
inds) of
(Just ((Name, Val), Val -> Bool)
_, []) -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall {a}.
StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
failure
(Just ((Name
x,Val
ltv), Val -> Bool
isFlex), Val
sizeInd:[Val]
_) | Bool -> Bool
not (Val -> Bool
isFlex Val
sizeInd) ->
Name
-> [Name]
-> Val
-> [Val]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
continue Name
d [Name
x] Val
ltv ([Val]
pars [Val] -> [Val] -> [Val]
forall a. [a] -> [a] -> [a]
++ [Val
sizeInd])
(Maybe ((Name, Val), Val -> Bool), [Val])
_ -> Name
-> [Name]
-> Val
-> [Val]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
continue Name
d [] Val
symbTyp [Val]
pars
where
continue :: Name
-> [Name]
-> Val
-> [Val]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
continue Name
d [Name]
ys Val
tv [Val]
pars = case ConPars
conPars of
ConPars
Nothing -> Val
-> [Val]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
piApps Val
tv [Val]
pars
Just ([Name]
xs, [Pattern]
ps) -> do
let failure :: StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
failure = TypeCheck Doc
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadError TraceError m => m Doc -> m a
failDoc (TypeCheck Doc
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a)
-> TypeCheck Doc
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall a b. (a -> b) -> a -> b
$ [TypeCheck Doc] -> TypeCheck Doc
forall {f :: * -> *}. Monad f => [f Doc] -> f Doc
sep
[ String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text String
"instConType:"
, String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text String
"cannot match parameters" TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> [TypeCheck Doc] -> TypeCheck Doc
forall {f :: * -> *}. Monad f => [f Doc] -> f Doc
prettyList ((Val -> TypeCheck Doc) -> [Val] -> [TypeCheck Doc]
forall a b. (a -> b) -> [a] -> [b]
map Val -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM [Val]
pars)
, String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text String
"against patterns" TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> [TypeCheck Doc] -> TypeCheck Doc
forall {f :: * -> *}. Monad f => [f Doc] -> f Doc
prettyList ((Pattern -> TypeCheck Doc) -> [Pattern] -> [TypeCheck Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM [Pattern]
ps)
, String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text String
"when instantiating type" TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> Val -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM Val
tv
, String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text (String
"of constructor " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
c)
]
mst <- Bool
-> Bool
-> MatchState
-> [Pattern]
-> [Val]
-> Val
-> TypeCheck (Maybe MatchState)
nonLinMatchList' Bool
True Bool
True (Env
forall a. Environ a
emptyEnv, []) [Pattern]
ps [Val]
pars (Val -> TypeCheck (Maybe MatchState))
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> TypeCheck (Maybe MatchState)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall (m :: * -> *). MonadSig m => Name -> m Val
lookupSymbTyp Name
d
case mst of
Maybe MatchState
Nothing -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall {a}.
StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
failure
Just (Environ{ envMap :: forall a. Environ a -> [(Name, a)]
envMap = [(Name, Val)]
env0 }, [(Int, Pattern)]
psub) -> do
let env :: [(Name, Val)]
env = [(Name, Val)]
env0 [(Name, Val)] -> [(Name, Val)] -> [(Name, Val)]
forall a. [a] -> [a] -> [a]
++ [ (Name
x, Int -> Val
VGen Int
i) | (Int
i, VarP Name
x) <- [(Int, Pattern)]
psub ]
vs <- [Name]
-> (Name
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Val]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Name]
xs [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
ys) ((Name
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Val])
-> (Name
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Val]
forall a b. (a -> b) -> a -> b
$ \ Name
x -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
-> (Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> Maybe Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall b a. b -> (a -> b) -> Maybe a -> b
maybe StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall {a}.
StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
failure Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val)
-> Maybe Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall a b. (a -> b) -> a -> b
$ Name -> [(Name, Val)] -> Maybe Val
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x [(Name, Val)]
env
piApps tv vs
class MonadCxt m => MonadSig m where
lookupSymbTypQ :: QName -> m TVal
lookupSymbQ :: QName -> m SigDef
addSigQ :: QName -> SigDef -> m ()
modifySigQ :: QName -> (SigDef -> SigDef) -> m ()
setExtrTypQ :: QName -> Expr -> m ()
lookupSymbTyp :: Name -> m TVal
lookupSymbTyp = QName -> m Val
forall (m :: * -> *). MonadSig m => QName -> m Val
lookupSymbTypQ (QName -> m Val) -> (Name -> QName) -> Name -> m Val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
QName
lookupSymb :: Name -> m SigDef
lookupSymb = QName -> m SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ (QName -> m SigDef) -> (Name -> QName) -> Name -> m SigDef
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
QName
addSig :: Name -> SigDef -> m ()
addSig = QName -> SigDef -> m ()
forall (m :: * -> *). MonadSig m => QName -> SigDef -> m ()
addSigQ (QName -> SigDef -> m ())
-> (Name -> QName) -> Name -> SigDef -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
QName
modifySig :: Name -> (SigDef -> SigDef) -> m ()
modifySig = QName -> (SigDef -> SigDef) -> m ()
forall (m :: * -> *).
MonadSig m =>
QName -> (SigDef -> SigDef) -> m ()
modifySigQ (QName -> (SigDef -> SigDef) -> m ())
-> (Name -> QName) -> Name -> (SigDef -> SigDef) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
QName
setExtrTyp :: Name -> Expr -> m ()
setExtrTyp = QName -> Expr -> m ()
forall (m :: * -> *). MonadSig m => QName -> Expr -> m ()
setExtrTypQ (QName -> Expr -> m ()) -> (Name -> QName) -> Name -> Expr -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
QName
instance MonadSig TypeCheck where
lookupSymbTyp :: Name
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
lookupSymbTyp Name
n = do
mdom <- TypeCheck CxtEntry1
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
(Maybe CxtEntry1)
forall e (m :: * -> *) a. MonadError e m => m a -> m (Maybe a)
errorToMaybe (TypeCheck CxtEntry1
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
(Maybe CxtEntry1))
-> TypeCheck CxtEntry1
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
(Maybe CxtEntry1)
forall a b. (a -> b) -> a -> b
$ Name -> TypeCheck CxtEntry1
forall (m :: * -> *). MonadCxt m => Name -> m CxtEntry1
lookupName1 Name
n
case mdom of
Just (CxtEntry Domain
dom UDec
udec) -> Val
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Domain -> Val
forall a. Dom a -> a
typ Domain
dom)
Maybe CxtEntry1
Nothing -> SigDef -> Val
symbTyp (SigDef -> Val)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => Name -> m SigDef
lookupSymb Name
n
lookupSymbTypQ :: QName
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
lookupSymbTypQ (QName Name
n) = Name
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall (m :: * -> *). MonadSig m => Name -> m Val
lookupSymbTyp Name
n
lookupSymbTypQ n :: QName
n@Qual{} = SigDef -> Val
symbTyp (SigDef -> Val)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Val
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
n
lookupSymb :: Name
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
lookupSymb Name
n = do
cxt <- StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) TCContext
forall r (m :: * -> *). MonadReader r m => m r
ask
case Map.lookup n (mutualFuns cxt) of
Just SigDef
k -> SigDef
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SigDef
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef)
-> SigDef
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall a b. (a -> b) -> a -> b
$ SigDef
k
Maybe SigDef
Nothing -> QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
lookupSymbInSig (Name -> QName
QName Name
n)
lookupSymbQ :: QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
lookupSymbQ (QName Name
n) = Name
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => Name -> m SigDef
lookupSymb Name
n
lookupSymbQ n :: QName
n@Qual{} = QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
lookupSymbInSig QName
n
addSigQ :: QName -> SigDef -> TypeCheck ()
addSigQ QName
n SigDef
def = String -> TypeCheck () -> TypeCheck ()
forall a. String -> a -> a
traceSig (String
"addSig: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is bound to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SigDef -> String
forall a. Show a => a -> String
show SigDef
def) (TypeCheck () -> TypeCheck ()) -> TypeCheck () -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$ do
st <- StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) TCState
forall s (m :: * -> *). MonadState s m => m s
get
put $ st { signature = Map.insert n def $ signature st }
modifySigQ :: QName -> (SigDef -> SigDef) -> TypeCheck ()
modifySigQ QName
n SigDef -> SigDef
f = do
st <- StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) TCState
forall s (m :: * -> *). MonadState s m => m s
get
put $ st { signature = Map.adjust f n $ signature st }
setExtrTypQ :: QName -> Expr -> TypeCheck ()
setExtrTypQ QName
n Expr
t = QName -> (SigDef -> SigDef) -> TypeCheck ()
forall (m :: * -> *).
MonadSig m =>
QName -> (SigDef -> SigDef) -> m ()
modifySigQ QName
n (\ SigDef
d -> SigDef
d { extrTyp = t })
lookupSymbInSig :: QName -> TypeCheck SigDef
lookupSymbInSig :: QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
lookupSymbInSig QName
n = QName
-> Signature
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall {k} {m :: * -> *} {a}.
(Ord k, MonadError TraceError m, Show k) =>
k -> Map k a -> m a
lookupSig QName
n (Signature
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) Signature
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCState -> Signature)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) Signature
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TCState -> Signature
signature
where
lookupSig :: k -> Map k a -> m a
lookupSig k
n Map k a
sig =
case (k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
n Map k a
sig) of
Maybe a
Nothing -> String -> m a
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"identifier " String -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in signature " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [k] -> String
forall a. Show a => a -> String
show (Map k a -> [k]
forall k a. Map k a -> [k]
Map.keys Map k a
sig)
Just a
k -> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
k
initSt :: TCState
initSt :: TCState
initSt = Signature -> MetaVars -> Constraints -> PositivityGraph -> TCState
TCState Signature
emptySig MetaVars
emptyMetaVars Constraints
emptyConstraints PositivityGraph
emptyPosGraph
initWithSig :: Signature -> TCState
initWithSig :: Signature -> TCState
initWithSig Signature
sig = TCState
initSt { signature = sig }
class Monad m => MonadMeta m where
resetConstraints :: m ()
mkConstraint :: Val -> Val -> m (Maybe Constraint)
addMeta :: Ren -> MVar -> m ()
addLeq :: Val -> Val -> m ()
addLe :: LtLe -> Val -> Val -> m ()
addLe LtLe
Le Val
v1 Val
v2 = Val -> Val -> m ()
forall (m :: * -> *). MonadMeta m => Val -> Val -> m ()
addLeq Val
v1 Val
v2
addLe LtLe
Lt Val
v1 Val
v2 = Val -> Val -> m ()
forall (m :: * -> *). MonadMeta m => Val -> Val -> m ()
addLeq (Val -> Val
succSize Val
v1) Val
v2
solveConstraints :: m Solution
solveAndModify :: [Expr] -> Env -> m [Expr]
solveAndModify [Expr]
es Env
rho = do
sol <- m Solution
forall (m :: * -> *). MonadMeta m => m Solution
solveConstraints
let es' = (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Expr -> Expr
forall a. Substitute a => Subst -> a -> a
subst (Solution -> Env -> Subst
solToSubst Solution
sol Env
rho)) [Expr]
es
resetConstraints
return es'
instance MonadMeta TypeCheck where
resetConstraints :: TypeCheck ()
resetConstraints = do
st <- StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) TCState
forall s (m :: * -> *). MonadState s m => m s
get
put $ st { constraints = emptyConstraints }
mkConstraint :: Val -> Val -> TypeCheck (Maybe Constraint)
mkConstraint Val
v (VMax [Val]
vs) = do
bs <- (Val -> TypeCheck Bool)
-> [Val]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (TypeCheck () -> TypeCheck Bool
forall e (m :: * -> *). MonadError e m => m () -> m Bool
errorToBool (TypeCheck () -> TypeCheck Bool)
-> (Val -> TypeCheck ()) -> Val -> TypeCheck Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Val -> Val -> TypeCheck ()
leqSize' Val
v) [Val]
vs
if any id bs then return Nothing else
throwErrorMsg $ "cannot handle constraint " ++ show v ++ " <= " ++ show (VMax vs)
mkConstraint w :: Val
w@(VMax [Val]
vs) Val
v = String -> TypeCheck (Maybe Constraint)
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck (Maybe Constraint))
-> String -> TypeCheck (Maybe Constraint)
forall a b. (a -> b) -> a -> b
$ String
"cannot handle constraint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v
mkConstraint (VMeta Int
i Env
rho Int
n) (VMeta Int
j Env
rho' Int
m) = Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Constraint -> TypeCheck (Maybe Constraint))
-> Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a b. (a -> b) -> a -> b
$ Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just (Constraint -> Maybe Constraint) -> Constraint -> Maybe Constraint
forall a b. (a -> b) -> a -> b
$ Node Rigid -> Int -> Node Rigid -> Constraint
arc (Int -> Node Rigid
forall rigid. Int -> Node rigid
Flex Int
i) (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
n) (Int -> Node Rigid
forall rigid. Int -> Node rigid
Flex Int
j)
mkConstraint (VMeta Int
i Env
rho Int
n) Val
VInfty = Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Constraint -> TypeCheck (Maybe Constraint))
-> Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a b. (a -> b) -> a -> b
$ Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just (Constraint -> Maybe Constraint) -> Constraint -> Maybe Constraint
forall a b. (a -> b) -> a -> b
$ Node Rigid -> Int -> Node Rigid -> Constraint
arc (Int -> Node Rigid
forall rigid. Int -> Node rigid
Flex Int
i) Int
0 (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid (Weight -> Rigid
RConst Weight
Infinite))
mkConstraint (VMeta Int
i Env
rho Int
n) Val
v = Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Constraint -> TypeCheck (Maybe Constraint))
-> Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a b. (a -> b) -> a -> b
$ Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just (Constraint -> Maybe Constraint) -> Constraint -> Maybe Constraint
forall a b. (a -> b) -> a -> b
$ Node Rigid -> Int -> Node Rigid -> Constraint
arc (Int -> Node Rigid
forall rigid. Int -> Node rigid
Flex Int
i) (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
n) (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid (Int -> Rigid
RVar Int
j))
where (Int
j,Int
m) = Val -> Int -> (Int, Int)
vGenSuccs Val
v Int
0
mkConstraint Val
VInfty (VMeta Int
i Env
rho Int
n) = Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Constraint -> TypeCheck (Maybe Constraint))
-> Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a b. (a -> b) -> a -> b
$ Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just (Constraint -> Maybe Constraint) -> Constraint -> Maybe Constraint
forall a b. (a -> b) -> a -> b
$ Node Rigid -> Int -> Node Rigid -> Constraint
arc (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid (Weight -> Rigid
RConst Weight
Infinite)) Int
0 (Int -> Node Rigid
forall rigid. Int -> Node rigid
Flex Int
i)
mkConstraint Val
v (VMeta Int
j Env
rho Int
m) = Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Constraint -> TypeCheck (Maybe Constraint))
-> Maybe Constraint -> TypeCheck (Maybe Constraint)
forall a b. (a -> b) -> a -> b
$ Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just (Constraint -> Maybe Constraint) -> Constraint -> Maybe Constraint
forall a b. (a -> b) -> a -> b
$ Node Rigid -> Int -> Node Rigid -> Constraint
arc (Rigid -> Node Rigid
forall rigid. rigid -> Node rigid
Rigid (Int -> Rigid
RVar Int
i)) (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
n) (Int -> Node Rigid
forall rigid. Int -> Node rigid
Flex Int
j)
where (Int
i,Int
n) = Val -> Int -> (Int, Int)
vGenSuccs Val
v Int
0
mkConstraint Val
v1 Val
v2 = String -> TypeCheck (Maybe Constraint)
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck (Maybe Constraint))
-> String -> TypeCheck (Maybe Constraint)
forall a b. (a -> b) -> a -> b
$ String
"mkConstraint undefined for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Val, Val) -> String
forall a. Show a => a -> String
show (Val
v1,Val
v2)
addMeta :: Ren -> Int -> TypeCheck ()
addMeta Ren
ren Int
i = do
scope <- TypeCheck [Name]
forall (m :: * -> *). MonadCxt m => m [Name]
getSizeVarsInScope
traceMetaM ("addMeta " ++ show i ++ " scope " ++ show scope)
st <- get
put $ st { metaVars = Map.insert i (MetaVar scope Nothing) (metaVars st)
, constraints = NewFlex i (\ Int
k' -> Bool
True)
: constraints st }
addLeq :: Val -> Val -> TypeCheck ()
addLeq Val
v1 Val
v2 = String -> TypeCheck () -> TypeCheck ()
forall a. String -> a -> a
traceMeta (String
"Constraint: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v2) (TypeCheck () -> TypeCheck ()) -> TypeCheck () -> TypeCheck ()
forall a b. (a -> b) -> a -> b
$
do mc <- Val -> Val -> TypeCheck (Maybe Constraint)
forall (m :: * -> *).
MonadMeta m =>
Val -> Val -> m (Maybe Constraint)
mkConstraint Val
v1 Val
v2
case mc of
Maybe Constraint
Nothing -> () -> TypeCheck ()
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Constraint
c -> do
st <- StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) TCState
forall s (m :: * -> *). MonadState s m => m s
get
put $ st { constraints = c : constraints st }
solveConstraints :: TypeCheck Solution
solveConstraints = do
cs <- (TCState -> Constraints)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) Constraints
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TCState -> Constraints
constraints
if null cs then return emptySolution
else case solve cs of
Just Solution
subst -> String -> TypeCheck Solution -> TypeCheck Solution
forall a. String -> a -> a
traceMeta (String
"solution" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Solution -> String
forall a. Show a => a -> String
show Solution
subst) (TypeCheck Solution -> TypeCheck Solution)
-> TypeCheck Solution -> TypeCheck Solution
forall a b. (a -> b) -> a -> b
$
Solution -> TypeCheck Solution
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Solution
subst
Maybe Solution
Nothing -> String -> TypeCheck Solution
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck Solution) -> String -> TypeCheck Solution
forall a b. (a -> b) -> a -> b
$ String
"size constraints " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Constraints -> String
forall a. Show a => a -> String
show Constraints
cs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" unsolvable"
nameOf :: EnvMap -> Int -> Maybe Name
nameOf :: [(Name, Val)] -> Int -> Maybe Name
nameOf [] Int
j = Maybe Name
forall a. Maybe a
Nothing
nameOf ((Name
x,VGen Int
i):[(Name, Val)]
rho) Int
j | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
nameOf ((Name, Val)
_:[(Name, Val)]
rho) Int
j = [(Name, Val)] -> Int -> Maybe Name
nameOf [(Name, Val)]
rho Int
j
vGenSuccs :: Val -> Int -> (Int, Int)
vGenSuccs :: Val -> Int -> (Int, Int)
vGenSuccs (VGen Int
k) Int
m = (Int
k,Int
m)
vGenSuccs (VSucc Val
v) Int
m = Val -> Int -> (Int, Int)
vGenSuccs Val
v (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
vGenSuccs Val
v Int
m = String -> (Int, Int)
forall a. HasCallStack => String -> a
error (String -> (Int, Int)) -> String -> (Int, Int)
forall a b. (a -> b) -> a -> b
$ String
"vGenSuccs fails on " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
Util.parens (Val -> String
forall a. Show a => a -> String
show Val
v) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
m
sizeExprToExpr :: Env -> SizeExpr -> Expr
sizeExprToExpr :: Env -> SizeExpr -> Expr
sizeExprToExpr Env
rho (SizeConst Weight
Infinite) = Expr
Infty
sizeExprToExpr Env
rho (SizeVar Int
i Int
n) | Just Name
x <- [(Name, Val)] -> Int -> Maybe Name
nameOf (Env -> [(Name, Val)]
forall a. Environ a -> [(Name, a)]
envMap Env
rho) Int
i = Expr -> Int -> Expr
forall {t}. (Ord t, Num t) => Expr -> t -> Expr
add (Name -> Expr
Var Name
x) Int
n
where add :: Expr -> t -> Expr
add Expr
e t
n | t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
0 = Expr
e
| Bool
otherwise = Expr -> t -> Expr
add (Expr -> Expr
Succ Expr
e) (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1)
sizeExprToExpr Env
rho e :: SizeExpr
e@(SizeVar Int
i Int
n) | Maybe Name
Nothing <- [(Name, Val)] -> Int -> Maybe Name
nameOf (Env -> [(Name, Val)]
forall a. Environ a -> [(Name, a)]
envMap Env
rho) Int
i = String -> Expr
forall a. HasCallStack => String -> a
error (String -> Expr) -> String -> Expr
forall a b. (a -> b) -> a -> b
$ String
"panic: sizeExprToExpr " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
Util.parens (SizeExpr -> String
forall a. Show a => a -> String
show SizeExpr
e) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": variable v" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in scope " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Val)] -> String
forall a. Show a => a -> String
show (Env -> [(Name, Val)]
forall a. Environ a -> [(Name, a)]
envMap Env
rho)
maxExpr :: [Expr] -> Expr
maxExpr :: [Expr] -> Expr
maxExpr [] = Expr
Infty
maxExpr [Expr
e] = Expr
e
maxExpr [Expr]
l = if Expr
Infty Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
l then Expr
Infty else [Expr] -> Expr
Max [Expr]
l
solToSubst :: Solution -> Env -> Subst
solToSubst :: Solution -> Env -> Subst
solToSubst Solution
sol Env
rho = ([SizeExpr] -> Expr) -> Solution -> Subst
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ([Expr] -> Expr
maxExpr ([Expr] -> Expr) -> ([SizeExpr] -> [Expr]) -> [SizeExpr] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SizeExpr -> Expr) -> [SizeExpr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> SizeExpr -> Expr
sizeExprToExpr Env
rho)) Solution
sol