{-# 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 Debug.Trace

import Abstract
import Polarity
import Value
import {-# SOURCE #-} Eval -- (up,whnf')
import PrettyTCM

-- import CallStack
import TraceError

import TreeShapedOrder (TSO)
import qualified TreeShapedOrder as TSO

import Util

import Warshall

traceSig :: String -> a -> a
-- traceSig msg a = trace msg 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 -- trace msg 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 () -- traceM msg
{-
traceRew msg a = trace msg a
traceRewM msg = traceM msg
-}

-- metavariables and constraints

traceMeta :: String -> a -> a
traceMeta :: forall a. String -> a -> a
traceMeta String
msg a
a = a
a -- trace msg 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 () -- traceM msg
{-
traceMeta msg a = trace msg a
traceMetaM msg = traceM msg
-}


-- type checking monad -----------------------------------------------

class (MonadCxt m, MonadSig m, MonadMeta m, MonadError TraceError m) =>
  MonadTCM m where


-- lists of exactly one or two elements ------------------------------

-- this would have been better implemented by just lists and a view
--   type OneOrTwo a = [a]
--   data View12 a = One a | Two a a
--   fromList12
-- then one could still get completeness of pattern matching!
-- now we have lots of boilerplate code

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)

{-
instance Functor OneOrTwo where
  fmap f (One a)   = One (f a)
  fmap f (Two a b) = Two (f a) (f b)

instance Foldable OneOrTwo where
  foldMap f (One a) = f a
  foldMap f (Two a b) = f a `mappend` f b

-- traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
instance Traversable OneOrTwo where
  traverse f (One a) = One <$> f a
  traverse f (Two a b) = Two <$> f a <*> f b
-}

-- eliminator
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


-- reader monad for local environment

data TCContext = TCContext
  { TCContext -> SemCxt
context   :: SemCxt
  , TCContext -> Ren
renaming  :: Ren       -- assigning de Bruijn Levels to names
  , TCContext -> Map Int Name
naming    :: Map Int Name  -- assigning names to de Bruijn levels
--  , nameVariants :: Map Name Int -- how many variants of the name
  , TCContext -> Env2
environ   :: Env2
  , TCContext -> Rewrites
rewrites  :: Rewrites
  , TCContext -> TSO Int
sizeRels  :: TSO Int   -- relations of universal (rigid) size variables
                           -- collected from size patterns (x > y)
  , TCContext -> [Int]
belowInfty:: [Int]     -- list of size variables < #
  , TCContext -> [Bound Val]
bounds    :: [Bound Val]  -- bound hyps that do not fit in sizeRels
  , TCContext -> Bool
consistencyCheck :: Bool -- ^ Do we need to check that new size relations are consistent with every valuation of the current @sizeRels@? [See ICFP 2013 paper]
  , TCContext -> Bool
checkingConType :: Bool  -- different PTS rules for constructor types (parametric function space!)
  , TCContext -> AssertionHandling
assertionHandling :: AssertionHandling -- recover from errors?
  , TCContext -> Bool
impredicative :: Bool       -- use impredicative PTS rules
  -- checking measured functions
  , TCContext -> Map Name (Kinded Fun)
funsTemplate :: Map Name (Kinded Fun) -- types of mutual funs with measures checking body
  , TCContext -> Map Name SigDef
mutualFuns :: Map Name SigDef -- types of mutual funs while checking body
  , TCContext -> Co
mutualCo :: Co                -- mutual block (co)recursive ?
  , TCContext -> [Name]
mutualNames :: [Name] -- ^ The defined names of the current mutual block (and parents).
  , TCContext -> Maybe DefId
checkingMutualName :: Maybe DefId -- which body of a mutual block am I checking?
  , TCContext -> [QName]
callStack :: [QName] -- ^ Used to avoid looping when going into recursive data definitions.
  }

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 -- initially, no consistency check, turned on when entering rhs
  , checkingConType :: Bool
checkingConType = Bool
False
  , assertionHandling :: AssertionHandling
assertionHandling = AssertionHandling
Failure  -- default is not to ignore any errors
  , 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 = []
  }

-- state monad for global signature

data TCState = TCState
  { TCState -> Signature
signature   :: Signature
  , TCState -> MetaVars
metaVars    :: MetaVars
  , TCState -> Constraints
constraints :: Constraints
  , TCState -> PositivityGraph
positivityGraph :: PositivityGraph
  -- , dots        :: Dots -- UNUSED
  }

type MetaVars = Map MVar MetaVar

emptyMetaVars :: MetaVars
emptyMetaVars :: MetaVars
emptyMetaVars = MetaVars
forall k a. Map k a
Map.empty

type MScope = [Name] -- ^ names of size variables which are in scope of mvar
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 (CallStackT String IO))
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 })

{- mtl-2 provides these instances
-- TypeCheck is applicative since every monad is.
-- I do not know why this ain't in the libraries...
instance Applicative TypeCheck where
  pure      = return
  mf <*> ma = mf >>= \ f -> ma >>= \ a -> pure (f a)
-}

{- NOT NEEDED

-- | Dotted constructors (the top one in the pattern).
type Dots = [(Dotted,Pattern)]

emptyDots = []

class LensDots a where
  getDots :: a -> Dots
  setDots :: Dots -> a -> a
  setDots = mapDots . const
  mapDots :: (Dots -> Dots) -> a -> a
  mapDots f a = setDots (f (getDots a)) a

instance LensDots TCState where
  getDots = dots
  setDots d st = st { dots = d }

newDotted :: Pattern -> TypeCheck Dotted
newDotted p = do
  d <- mkDotted True
  modify $ mapDots $ ((d,p):)
  return d

clearDots :: TypeCheck ()
clearDots = modify $ setDots emptyDots

openDots :: TypeCheck [Pattern]
openDots = map snd . filter (isDotted . fst) <$> gets dots
-}

-- rewriting rules -----------------------------------------------

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)

{- renaming ------------------------------------------------------

  A renaming maps names to de Bruijn levels (= generic values).
-}

type Ren = Map Name Int

type Env2 = Environ (OneOrTwo Val)

type Context a = Map Int a
type Context2 a = Context (OneOrTwo a)

{- context -------------------------------------------------------

A context maps generic values to their type value.

During type checking, named variables are mapped to
generic values via a renaming.  Thus, looking up the type of a
name involves first looking up the generic value, and then its type.

-}

{-
-- data Domain = Domain { typ :: TVal, decor :: Dec }
data Domain = Domain { typ :: TVal, kind :: Class, decor :: Dec }

mapTyp :: (TVal -> TVal) -> Domain -> Domain
mapTyp f dom = dom { typ = f (typ dom) }

mapTypM :: Monad m => (TVal -> m TVal) -> Domain -> m Domain
mapTypM f dom = do
  t' <- f (typ dom)
  return $ dom { typ = t' }

instance Show Domain where
  show item = (if erased (decor item) then brackets else id) (show (typ item))
-}

-- During heterogeneous equality, a variable might have
-- two different types, one on the left and one on the right.
-- We implement this as Two tl tr.

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  -- fixed part of context
  , SemCxt -> Context UDec
upperDecs :: Context UDec -- the "should be below" decoration for each var.; this is updated by resurrection
  }
{- invariant: length (cxt delta) = length (upperDecs delta) = len
     cxt(i) = Two ... iff  upperDecs(i) = Two ...
 -}

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))
{-
  show delta = show $ zip (
    zipWith3 (zipWith12 Domain)
--    zipWith (\ entry dec -> fmap ((flip Domain) dec) entry)
      (Map.elems (cxt delta))
      (Map.elems (kinds delta))
      (Map.elems (decs delta))
    ) (Map.elems (upperDecs 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
--  , kinds = Map.empty
--  , decs = Map.empty
  , upperDecs :: Context UDec
upperDecs = Context UDec
forall k a. Map k a
Map.empty
  }

-- push a new type declaration on context
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)
--        , cxt  = Map.insert k (fmap typ   entry) (cxt delta)
--        , decs = Map.insert k (fmap decor entry) (decs delta)
        , upperDecs = Map.insert k defaultUpperDec (upperDecs delta)
        }
  where k :: Int
k = SemCxt -> Int
len SemCxt
delta
{-
cxtPush' (tv12, dec) delta =
  delta { len = k + 1
        , cxt  = Map.insert k tv12 (cxt delta)
        , decs = Map.insert k dec (decs delta) }
  where k = len delta
-}
{-
cxtPush :: Dec -> TVal -> SemCxt -> (Int, SemCxt)
cxtPush dec v delta = (len delta, cxtPush' (One (Domain v dec)) delta)
-- cxtPush dec v delta = (len delta, cxtPush' (One v, dec) 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
-- cxtPush dec v delta = (len delta, cxtPush' (One v, dec) delta)

-- push a variable with a left and a right type
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
--  (len delta, cxtPush' (Two doml domr) delta)

{-
-- push a variable with a left and a right type
cxtPush2 :: Dec -> TVal -> TVal -> SemCxt -> (Int, SemCxt)
cxtPush2 dec tvl tvr delta =
  (len delta, cxtPush' (Two tvl tvr, dec) 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"

-- only defined for single bindings
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)
        -- upperDecs need not be updated
        }

-- | Version of 'Map.lookup' that throws 'TraceError'.
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

-- apply decoration, possibly resurrecting (see Pfenning, LICS 2001)
-- and changing polarities (see Abel, MSCS 2008)
cxtApplyDec :: Dec -> SemCxt -> SemCxt
cxtApplyDec :: Dec -> SemCxt -> SemCxt
cxtApplyDec Dec
dec SemCxt
delta = SemCxt
delta { upperDecs = Map.map (compDec dec) (upperDecs delta) }
-- cxtApplyDec dec delta =  delta { decs = Map.map (fmap $ invCompDec dec) (decs delta) }

-- manipulating the context ------------------------------------------

{-
-- | Size decrements in bounded quantification do not count for termination
data LamPi
  = LamBind -- ^ add a lambda binding to the context
  | PiBind  -- ^ add a pi binding to the context
-}

class Monad m => MonadCxt m where
--  bind     :: Name -> Domain -> Val -> m a -> m a
--  new performs eta-expansion "up" of new gen
  -- adding types (Two t1 t2) returns values (Two (Up t1 vi) (Up t2 vi))
  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)
{-
  new2       :: Name -> (TVal, TVal, Dec) -> ((Val, Val) -> m a) -> m a
  new2 x d cont = new2WithGen x d (\ _ -> 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  -- only add binding x = VIrr to env
  addName    :: Name -> (Val -> m a) -> m a
{- RETIRED
  addTypeSigs :: [TySig TVal] -> m a -> m a
  addTypeSigs [] k = k
  addTypeSigs (TypeSig n tv : tss) k =
    new' n (defaultDomain tv) $ addTypeSigs tss k
-}
  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
--  addName x = new x dontCare
  setType    :: Int -> Domain -> m a -> m a
  setTypeOfName :: Name -> Domain -> m a -> m a
  genOfName  :: Name -> m Int
  nameOfGen  :: Int -> m Name
--  nameTaken  :: Name -> m Bool
  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 -- $ freshen x -- TODO!  now freshen causes problems in extraction
{-
  uniqueName x k = ifM (nameTaken x) (return $ show x ++ "~" ++ show k) (return 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  -- return context as telescope of type values
  getLen     :: m Int       -- return length of the context
  getEnv     :: m Env       -- return current environment
  getRen     :: m Ren       -- return current renaming
  applyDec   :: Dec -> m a -> m a  -- resurrect/adjust polarities
  resurrect  :: m a -> m a -- resurrect all erased variables in context
  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 -- step under pat
  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)
--  getSizeDiff :: Int -> Int -> m (Maybe Int)
  getMinSize  :: Int -> m (Maybe Int)
  getSizeVarsInScope :: m [Name]
  checkingCon :: Bool -> m a -> m a
  checkingDom :: m a -> m a  -- check domain A of Pi x:A.B (takes care of polarities)
  setCo :: Co -> m a -> m a -- entering a recursive or corecursive function?
  installFuns :: Co -> [Kinded Fun] -> m a -> m a
  setMeasure  :: Measure Val -> m a -> m a
  activateFuns :: m a -> m a -- create instance of mutually recursive functions bounded by measure
  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) })

  -- UPDATE to 2?
  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)
{-
  newVar x (tv12, dec) f = enter ("new " ++ x ++ " : " ++ show tv12) $ do
    cxtenv <- ask
    let (k, delta) = cxtPushEntry (tv12, dec) (context cxtenv)
    v12 <- Traversable.mapM (up (VGen k)) tv12
    let rho = update (environ cxtenv) x v12
    local (\ cxt -> cxt { context = delta
                        , renaming = Map.insert x k (renaming 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
       -- throwErrorMsg $ "internal error: no name for variable " ++ show 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

{-
  nameTaken "" = return True
  nameTaken x = do
    ce <- ask
    st <- get
    return (Map.member x (renaming ce) || Map.member x (signature st))
-}

  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

  -- does not work with shadowing!
  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

  -- since we only use getEnv during type checking, no case for Two
  -- (during equality/subtype checking, we have values)
  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) })
--  applyDec dec = local (\ ce -> ce { upperDecs = Map.map (compDec dec) (upperDecs ce) })

  -- resurrection sets "target" status to erased
  -- (as opposed to setting "source" status to non-erased)
{-
  resurrect = local (\ ce -> ce { upperDecs =
    Map.map (\ dec -> dec { erased = True }) (upperDecs ce) })
-}
{-
  resurrect = local (\ ce -> ce { context = cxtResurrect (context ce) })
-}


  -- PROBABLY TOO INEFFICIENT
  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
$
    -- add rewriting rule
    (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
      -- normalize all types in context
      traceRewM "normalizing types in context"
      cx' <- mapMapM (Traversable.mapM (Traversable.mapM reval)) (cxt (context ce))  -- LOOP!
      -- normalize environment
      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 -- no need to rewrite in measure since only size expressions
      -- normalize given values
      vs' <- mapM reval vs
      -- continue in updated context
      local (\ TCContext
ce -> TCContext
ce { context = (context ce) { cxt = cx' }
                        , environ = en' }) $ cont vs'

  -- addPattern :: TVal -> Pattern -> (TVal -> Val -> Env -> m a) -> m a
  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)
{-
          SizeP z y -> newWithGen y dom $ \ j xv -> do
              bv <- whnf (update env x xv) b
              VGen k <- whnf' (Var z)
              addSizeRel j 1 k $
                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 -- apply dom to pl?
                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
{-
          ConP pi n pl -> do
              sige <- lookupSymb n
              let vc = symbTyp sige
              addPatterns vc pl rho $ \ vc' vpl rho -> do -- apply dom to pl?
                pv0 <- foldM app (vCon (coPat pi) n) vpl
                pv  <- up False pv0 (typ dom)
                vb  <- whnf (update env x pv) b
                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

-- for dot patterns, we have to do something smart, because they might
-- contain identifiers which are not yet in scope, only after adding
-- other patterns
-- the following trivial solution only works for trivial dot patterns, i.e.,
-- such that do not use yet undeclared identifiers

          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 -- [(x,v)]


  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' -- (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 -- enterTrace
      (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"
    -- if the new son is an ancestor of the father, we are cyclic
    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 -> -- n steps from father up to son
      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
$ -- still ok if dist == n == 0, otherwise fail
        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
--      (Lt, _, [VInfty]) -> failure  -- handle j < #
      (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
--            recoverFail $ "adding hypothetical constraint " ++ show beta ++ " not supported"
            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

{-
  isBelowInfty i = do
    belowInfty <- asks belowInfty
    if (i `elem` belowInfty) then return True else do
      tso <- asks sizeRels
      loop $ parents i tso where
        loop [] = return False
        loop [(_,j)] = return $ j `elem` belowInfty
        loop (x:xs)  = loop xs
-}

  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)
{-
  getSizeDiff son ancestor = do
    cxt <- ask
    return $ TSO.diff 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
    -- get all the size variables with positive or mixed polarity
    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
_ -> -- trace ("not a size variable " ++ show i ++ " : " ++ show tv12) $
                   Bool
False
    -- create a list of key (gen) and Domain pairs for the size variables
    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 = local $ \ cxt ->
    if checkingConType cxt then cxt
     else cxt { context = cxtApplyDec (Dec False Neg) (context cxt) }
-}
  -- check domain A of (x : A) -> 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 })

  -- install functions for checking function clauses
  -- ==> use internal names
  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

{-
  activateFuns mu k = do
      rho0 <- getEnv
      let rho = rho0 { envBound = Just mu }
      local (\ cxt -> cxt
        { environ    = (environ cxt) { envBound = Just mu }
        , mutualFuns =
            Map.map (boundFun rho (mutualCo cxt)) (funsTemplate cxt)
        }) k
    where boundFun :: Env -> Co -> Fun -> SigDef
          boundFun rho co (TypeSig n t, (ar, cls)) =
            FunSig co (VClos rho t) ar cls False
 -}

  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 })

-- | Go into the codomain of a Pi-type or open an abstraction.
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

-- | Do not check consistency preservation of context.
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 }

-- | No eta, no hypotheses.  First returned val is a @VGen i@.
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 :: MonadTCM m => TBind -> m a -> m a
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

-- introduce patterns into context and environment -------------------
-- DOES NOT ETA-EXPAND VARIABLES!! -----------------------------------

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 =                -- Problem: NO ETA EXPANSION!
  [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                    -- first bind pattern variables
    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 -- now we can evaluate patterns
    let pvs = [Pattern] -> [Val] -> [(Pattern, Val)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Pattern]
ps [Val]
vs
    introPatTypes pvs tv (cont pvs)       -- now we can assign types to pvars

-- introduce variables bound in pattern into the environment
-- extend delta by generic values but do not introduce their types
-- this is to deal with dot patterns
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

-- if the bindings name->gen are already in the environment
-- we can now bind the gen to their types
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 -- no record value here
        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
                                                   -- erasure does not matter!
          (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
{-
             sige <- lookupSymb n
             let vc = symbTyp sige
-}
             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)


-- Signature -----------------------------------------------------

-- input to and output of the type-checker

type Signature = Map QName SigDef

-- a signature entry is either
-- - a fun/cofun,
-- - a defined constant,
-- - a constructor, or
-- - a data type id with its kind
-- they share "symbTyp", the type signature of the definition
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   -- ^ Fomega type.
            }
  | LetSig  { symbTyp       :: TVal
            , symbolKind    :: Kind
            , SigDef -> Val
definingVal   :: Val
--            , definingExpr  :: Expr
            , extrTyp       :: Expr   -- ^ Fomega type.
            }
  | PatSig  { SigDef -> [Name]
patVars       :: [Name]
            , SigDef -> Pattern
definingPat   :: Pattern
            , definingVal   :: Val
            }
  | ConSig  { SigDef -> ConPars
conPars       :: ConPars
              -- ^ Parameter patterns and no. of variable they bind.
              --   @Nothing@ if old-style parameters.
            , SigDef -> LHSType
lhsTyp        :: LHSType
              -- ^ LHS type of constructor for pattern matching, e.g.
   -- rhs @cons : [A : Set] [i : Size]         -> A -> List A i -> List A $i@
   -- lhs @cons : [A : Set] [i : Size] [j < i] -> A -> List A j -> List A i@
   -- @Name@ is the name of the size parameter.
            , SigDef -> [Bool]
recOccs       :: [Bool]
              -- ^ @True@ if argument contains rec.occs.of the (co)data type?
            , symbTyp       :: TVal   -- ^ (RHS) type, includs parameter tel.
            , SigDef -> Name
dataName      :: Name   -- ^ Its datatype.
            , SigDef -> Int
dataPars      :: Int    -- ^ No. of parameters of its datatype.
            , extrTyp       :: Expr   -- ^ Fomega type.
            }
  | DataSig { SigDef -> Int
numPars       :: Int
            , SigDef -> [Pol]
positivity    :: [Pol]
            , SigDef -> Sized
isSized       :: Sized
            , isCo          :: Co
            , symbTyp       :: TVal
            , symbolKind    :: Kind
            -- the following information is only needed for eta-expansion
            -- hence it is only provided for suitable ind.fams.
            , SigDef -> [ConstructorInfo]
constructors  :: [ConstructorInfo]
            , SigDef -> Bool
etaExpand     :: Bool -- non-overlapping pattern inductive family
                                    -- with at least one eta-expandable constructor
            , SigDef -> Bool
isTuple       :: Bool -- each constructor is irrefutable
                                    -- must be (NEW: non-overlapping) pattern inductive family
                                    -- qualifies for target of corecursive fun
                                    -- NO LONGER: exactly one constructor
                                    -- NOW: at least one constructor
                                    -- can be recursive
            , extrTyp       :: Expr -- Fomega kind
{-
            , destructors   :: Maybe [Name] -- Nothing if not a record
            , isFamily      :: Bool
-}
            } -- # parameters, positivity of parameters  , sized , co , type
              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)

-- | Parameter patterns and no. of variables they bind.
type ConPars = Maybe ([Name], [Pattern])

-- | LHS type plus name of size index.
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
-- undefinedFType n = error $ "no extracted type for " ++ show n

symbKind :: SigDef -> Kind
symbKind :: SigDef -> Kind
symbKind ConSig{}  = Kind
kTerm          -- constructors are always terms
symbKind SigDef
d         = SigDef -> Kind
symbolKind SigDef
d   -- else: lookup
{- Data types can be big!!
symbKind DataSig{} = kType          -- data types are never universes
-}

emptySig :: Signature
emptySig :: Signature
emptySig = Signature
forall k a. Map k a
Map.empty

-- Handling constructor types  ------------------------------------------

data DataView
  = Data Name [Clos]
  | NoData

-- | Check if type @tv@ is a datatype @D vs@.
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
{- 2012-01-31 EVIL, LEADS TO UNBOUND VARS:
    VQuant Pi x dom env b         -> do
      new x dom $ \ xv -> dataView =<< whnf (update env x xv) b
-}
    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

-- | Disambiguate possibly overloaded constructor @c@ at given type @tv@.
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 c tv@ returns the type of constructor @c@ at datatype @tv@
--   with parameters instantiated.
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

-- | Get LHS type of constructor.
--
--   Constructors or sized data types internally have a lhs type
--   that differs from its rhs type.  E.g.,
--   rhs @suc : [i : Size] -> Nat i -> Nat $i@
--   lhs @suc : [i : Size] [j < i] -> Nat j -> Nat i@.
--   In the lhs type, @i@ turns into an additional parameter.
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])

-- | Instantiate type of constructor to parameters obtained from
--   the data type.
--
--   @instConType c n symbTyp dataName tv@
--   instantiates type @symbTyp@ of constructor @c@ with first @n@ arguments
--   that @dataName@ is applied to in @tv@.
--   @@
--      instConType c n ((x1:A1..xn:An) -> B) d (d v1..vn ws) = B[vs/xs]
--   @@
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
{-
instConType c numPars symbTyp dataName tv = do
  dv <- dataView tv
  case dv of
    NoData    -> failDoc (text ("conType " ++ show c ++ ": expected")
                   <+> prettyTCM tv <+> text "to be a data type")
    Data d vs -> do
      unless (d == dataName) $ throwErrorMsg $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show dataName
      let (pars, inds) = splitAt numPars vs
      unless (length pars == numPars) $
        failDoc (text ("conType " ++ show c ++ ": expected")
                   <+> prettyTCM tv
                   <+> text ("to be a data type applied to all of its " ++
                     show numPars ++ " parameters"))
      piApps symbTyp pars
-}

-- | Get correct lhs type for constructor pattern.
--
--   @instConLType c numPars symbTyp Nothing isFlex tv@ behaves like
--   @instConLType c numPars symbType _ tv@.
--
--   But if the data types is sized and the constructor has a lhs type,
--   @instConLType c numPars symbTyp (Just ltv) isFlex tv@
--   uses the lhs type @ltv@ unless the variable instantiated for
--   the size argument is flexible (because then it wants to be
--   unified with the successor pattern of the rhs type.
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

-- | The common pattern behind @instConType@ and @instConLType@.
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'
      -- whenJust conPars $ throwErrorMsg $ "NYI: constructor with pattern parameters"
      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
        -- if size index not flexible, use lhs type
        (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])
        -- otherwise, use rhs type
        (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)
              ]
        -- clear dots here:
        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 ]
            -- if length env /= length xs then failure else do
            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
{-
        menv <- matchList emptyEnv ps pars
        case menv of
          Nothing  -> failure
          Just Environ{ envMap = env } -> if length env /= length xs then failure else do
            vs <- forM (xs ++ ys) $ \ x -> maybe failure return $ lookup x env
            piApps tv vs
-}

{-
      case isSized of
        Nothing  -> piApps symbTyp pars
        Just ltv -> do
          when (null inds) failure
          let sizeInd = head inds
          if isFlex sizeInd then piApps symbTyp pars else piApps ltv (pars ++ [sizeInd])
-}

-- Signature specification -------------------------------------------

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

-- Signature implementation ------------------------------------------

instance MonadSig TypeCheck where

  -- first in context, then in signature
  -- lookupSymbTyp :: Name -> TypeCheck TVal
  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 -> TypeCheck SigDef
  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

  -- addSig :: Name -> SigDef -> TypeCheck ()
  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 }

  -- modifySig :: Name -> (SigDef -> SigDef) -> TypeCheck ()
  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 }

  -- setExtrTyp :: Name -> Expr -> TypeCheck ()
  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 :: Name -> Signature -> TypeCheck SigDef
      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


-- more on the type checking monad -------------------------------

initSt :: TCState
initSt :: TCState
initSt = Signature -> MetaVars -> Constraints -> PositivityGraph -> TCState
TCState Signature
emptySig MetaVars
emptyMetaVars Constraints
emptyConstraints PositivityGraph
emptyPosGraph -- emptyDots

initWithSig :: Signature -> TCState
initWithSig :: Signature -> TCState
initWithSig Signature
sig = TCState
initSt { signature = sig }

-- Meta-variable and constraint handling specification ---------------

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 -- broken for #

  solveConstraints :: m Solution

  -- solve constraints and substitute solution into the analyzed expressions
  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'

-- Constraints implementation ----------------------------------------

instance MonadMeta TypeCheck where

  --resetConstraints :: TypeCheck ()
  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 -> 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 k x  adds a metavariable which can refer to VGens < k
  -- addMeta :: Ren -> MVar -> TypeCheck ()
  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) -- k' < k)
            -- DO NOT ADD constraints of form <= infty !!
            --               : arc (Flex i) 0 (Rigid (RConst Infinite))
                           : constraints st }

  -- addLeq :: Val -> Val -> TypeCheck ()
  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 :: 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


{-
solToSubst :: Solution -> Env -> Subst
solToSubst sol rho = Map.foldWithKey step Map.empty sol
  where step k (SizeVar i n) sub | Just x <- nameOf rho i =
           Map.insert k (add (Var x) n) sub
        step k (SizeConst Infinite) sub = Map.insert k Infty sub
        step _ _ sub = sub

        add e n | n <= 0 = e
                | otherwise = add (Succ e) (n-1)
-}

-- pattern to Value ----------------------------------------------

{- RETIRED
patternToVal :: Pattern -> TypeCheck Val
patternToVal p = do
  k <- getLen
  return $ fst (p2v k p)

-- turn a pattern into a value
-- dot patterns get variables corresponding to their flexible generic value
p2v :: Int -> Pattern -> (Val,Int)
p2v k p =
    case p of
      VarP n -> (VGen k,k+1)
      ConP co n [] -> (VCon co n,k)
      ConP co n pl -> let (vl,k') = ps2vs k pl
                      in (VApp (VCon co n) vl,k')
      SuccP p -> let (v,k') = p2v k p
                 in (VSucc v,k')
      DotP e -> (VGen k,k+1)

ps2vs :: Int -> [Pattern] -> ([Val],Int)
ps2vs k []  = ([],k)
ps2vs k (p:pl) = let (v,k') = p2v k p
                     (vl,k'') = ps2vs k' pl
                 in
                   (v:vl,k'')
-}