MiniAgda-0.2022.3.11: src/TCM.hs
{-# 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)
import Control.Applicative
import Data.Foldable (Foldable)
import qualified Data.Foldable as Foldable
import Data.Traversable (Traversable)
import qualified Data.Traversable as Traversable
import Data.Monoid
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 msg a = trace msg a
traceSig msg a = a
traceRew msg a = a -- trace msg a
traceRewM msg = return () -- traceM msg
{-
traceRew msg a = trace msg a
traceRewM msg = traceM msg
-}
-- metavariables and constraints
traceMeta msg a = a -- trace msg a
traceMetaM msg = 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 (Eq, Ord, Functor, Foldable, Traversable)
instance Show a => Show (OneOrTwo a) where
show (One a) = show a
show (Two a b) = show a ++ "||" ++ show b
name12 :: OneOrTwo Name -> Name
name12 (One n) = n
name12 (Two n1 n2)
| null (suggestion n2) = n1
| null (suggestion n1) = n2
| suggestion n1 == suggestion n2 = n1
| otherwise = fresh (suggestion n1 ++ "||" ++ suggestion 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 f g (One a) = f a
oneOrTwo f g (Two a1 a2) = g a1 a2
fromOne :: OneOrTwo a -> a
fromOne (One a) = a
toTwo :: OneOrTwo a -> OneOrTwo a
toTwo = oneOrTwo (\ a -> Two a a) Two
first12 :: OneOrTwo a -> a
first12 (One a) = a
first12 (Two a1 a2) = a1
second12 :: OneOrTwo a -> a
second12 (One a) = a
second12 (Two a1 a2) = a2
mapSecond12 :: (a -> a) -> OneOrTwo a -> OneOrTwo a
mapSecond12 f (One a) = One (f a)
mapSecond12 f (Two a1 a2) = Two a1 (f a2)
zipWith12 :: (a -> b -> c) -> OneOrTwo a -> OneOrTwo b -> OneOrTwo c
zipWith12 f (One a) (One b) = One (f a b)
zipWith12 f (Two a a') (Two b b') = Two (f a b) (f a' b')
zipWith123 :: (a -> b -> c -> d) ->
OneOrTwo a -> OneOrTwo b -> OneOrTwo c -> OneOrTwo d
zipWith123 f (One a) (One b) (One c) = One (f a b c)
zipWith123 f (Two a a') (Two b b') (Two c c') = Two (f a b c) (f a' b' c')
toList12 :: OneOrTwo a -> [a]
toList12 (One a) = [a]
toList12 (Two a1 a2) = [a1,a2]
fromList12 :: Show a => [a] -> OneOrTwo a
fromList12 [a] = One a
fromList12 [a1,a2] = Two a1 a2
fromList12 l = error $ "fromList12 " ++ show l
toMaybe12 :: Show a => [a] -> Maybe (OneOrTwo a)
toMaybe12 [] = Nothing
toMaybe12 [a] = Just $ One a
toMaybe12 [a1,a2] = Just $ Two a1 a2
toMaybe12 l = error $ "toMaybe12 " ++ show l
-- reader monad for local environment
data TCContext = TCContext
{ context :: SemCxt
, renaming :: Ren -- assigning de Bruijn Levels to names
, naming :: Map Int Name -- assigning names to de Bruijn levels
-- , nameVariants :: Map Name Int -- how many variants of the name
, environ :: Env2
, rewrites :: Rewrites
, sizeRels :: TSO Int -- relations of universal (rigid) size variables
-- collected from size patterns (x > y)
, belowInfty:: [Int] -- list of size variables < #
, bounds :: [Bound Val] -- bound hyps that do not fit in sizeRels
, consistencyCheck :: Bool -- ^ Do we need to check that new size relations are consistent with every valuation of the current @sizeRels@? [See ICFP 2013 paper]
, checkingConType :: Bool -- different PTS rules for constructor types (parametric function space!)
, assertionHandling :: AssertionHandling -- recover from errors?
, impredicative :: Bool -- use impredicative PTS rules
-- checking measured functions
, funsTemplate :: Map Name (Kinded Fun) -- types of mutual funs with measures checking body
, mutualFuns :: Map Name SigDef -- types of mutual funs while checking body
, mutualCo :: Co -- mutual block (co)recursive ?
, mutualNames :: [Name] -- ^ The defined names of the current mutual block (and parents).
, checkingMutualName :: Maybe DefId -- which body of a mutual block am I checking?
, callStack :: [QName] -- ^ Used to avoid looping when going into recursive data definitions.
}
instance Show TCContext where
show ce = show (environ ce) ++ "; " ++ show (context ce)
emptyContext = TCContext
{ context = cxtEmpty
, renaming = Map.empty
, naming = Map.empty
, environ = emptyEnv
, rewrites = emptyRewrites
, sizeRels = TSO.empty
, belowInfty = []
, bounds = []
, consistencyCheck = False -- initially, no consistency check, turned on when entering rhs
, checkingConType = False
, assertionHandling = Failure -- default is not to ignore any errors
, impredicative = False
, funsTemplate = Map.empty
, mutualFuns = Map.empty
, mutualCo = Ind
, mutualNames = []
, checkingMutualName = Nothing
, callStack = []
}
-- state monad for global signature
data TCState = TCState
{ signature :: Signature
, metaVars :: MetaVars
, constraints :: Constraints
, positivityGraph :: PositivityGraph
-- , dots :: Dots -- UNUSED
}
type MetaVars = Map MVar MetaVar
emptyMetaVars = Map.empty
type MScope = [Name] -- ^ names of size variables which are in scope of mvar
data MetaVar = MetaVar
{ mscope :: MScope
, solution :: Maybe Val
}
type PosConstrnt = Constrnt PPoly DefId ()
type PositivityGraph = [PosConstrnt]
emptyPosGraph = []
-- type TypeCheck = StateT TCState (ReaderT TCContext (CallStackT String IO))
type TypeCheck = StateT TCState (ReaderT TCContext (ExceptT TraceError IO))
instance MonadAssert TypeCheck where
assert b s = do
h <- asks assertionHandling
assert' h b s
newAssertionHandling h = local ( \ ce -> 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 { lhs :: Val, rhs :: Val }
type Rewrites = [Rewrite]
emptyRewrites = []
instance Show Rewrite where
show rr = show (lhs rr) ++ " --> " ++ show (rhs 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 { domain :: a, upperDec :: UDec }
type CxtEntry = CxtE (OneOrTwo Domain)
type CxtEntry1 = CxtE Domain
data SemCxt = SemCxt
{ len :: Int
, cxt :: Context2 Domain -- fixed part of context
, 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 delta =
show $ zip (Map.elems (cxt delta))
(Map.elems (upperDecs 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
{ len = 0
, cxt = Map.empty
-- , kinds = Map.empty
-- , decs = Map.empty
, upperDecs = Map.empty
}
-- push a new type declaration on context
cxtPush' :: OneOrTwo Domain -> SemCxt -> SemCxt
cxtPush' entry delta =
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 = len 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 ce delta = (len delta, cxtPush' ce delta)
cxtPush :: Domain -> SemCxt -> (Int, SemCxt)
cxtPush dom delta = cxtPushEntry (One dom) 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 doml domr delta = cxtPushEntry (Two doml domr) 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 x delta = cxtPush bot delta
where bot = error $ "IMPOSSIBLE: name " ++ show x ++ " is not bound to any type"
-- only defined for single bindings
cxtSetType :: Int -> Domain -> SemCxt -> SemCxt
cxtSetType k dom delta =
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 k m = maybe (throwErrorMsg $ "lookupM: unbound key " ++ show k) return $ Map.lookup k m
cxtLookupGen :: MonadError TraceError m => SemCxt -> Int -> m CxtEntry
cxtLookupGen delta k = do
dom12 <- lookupM k (cxt delta)
udec <- lookupM k (upperDecs delta)
return $ CxtEntry dom12 udec
cxtLookupName :: MonadError TraceError m => SemCxt -> Ren -> Name -> m CxtEntry
cxtLookupName delta ren x = do
i <- lookupM x 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 delta = delta { upperDecs = Map.map (compDec dec) (upperDecs delta) }
-- cxtApplyDec dec delta = delta { decs = Map.map (fmap $ invCompDec dec) (decs delta) }
{- RETIRED, use cxtApplyDec instead
-- clear all "erased" flags (see Pfenning, LICS 2001)
-- UPDATE: resurrection sets "target" status to erased
-- (as opposed to setting "source" status to non-erased)
cxtResurrect :: SemCxt -> SemCxt
cxtResurrect delta = delta { upperDecs = Map.map (\ dec -> dec { erased = True}) (upperDecs delta) }
-- cxtResurrect delta = delta { decs = Map.map (fmap resurrectDec) (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 x d k = newVar x (One d)
(\ i (One v) -> k i v)
new2WithGen:: Name -> (Domain, Domain) -> (Int -> (Val, Val) -> m a) -> m a
new2WithGen x (doml, domr) k = newVar x (Two doml domr)
(\ i (Two vl vr) -> k i (vl, vr))
new :: Name -> Domain -> (Val -> m a) -> m a
new x d cont = newWithGen x d (\ _ -> cont)
new2 :: Name -> (Domain, Domain) -> ((Val, Val) -> m a) -> m a
new2 x d cont = new2WithGen x d (\ _ -> 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' x d cont = new x d (\ _ -> 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 [] k = k
addKindedTypeSigs (Kinded ki (TypeSig n tv) : ktss) k =
new' n (Domain tv ki defaultDec) $ addKindedTypeSigs ktss 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 x _ = return 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 i = do
entry <- lookupGen i
case domain entry of
One d1 -> return (typ d1, typ d1)
Two d1 d2 -> return (typ d1, typ d2)
lookupName :: Name -> m CxtEntry
lookupName1 :: Name -> m CxtEntry1
lookupName1 x = do
e <- lookupName 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 = applyDec 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 = error "Internal error: tried to retrieve unassigned type of variable"
instance MonadCxt TypeCheck where
newIrr x = local (\ ce -> ce { environ = update (environ ce) x (One VIrr) })
-- UPDATE to 2?
addName x f = enter ("new " ++ show x ++ " : _") $ do
cxtenv <- ask
let (k, delta) = cxtPushGen x (context cxtenv)
let v = VGen k
let rho = update (environ cxtenv) x (One v)
x' <- uniqueName x k
local (\ cxt -> cxt { context = delta
, renaming = Map.insert x k (renaming cxtenv)
, naming = Map.insert k x' (naming cxt)
, environ = rho }) (f v)
newVar x dom12@(One (Domain (VBelow ltle v) ki dec)) f = do
enter ("new " ++ show x ++ " " ++ show ltle ++ " " ++ show v) $ do
cxtenv <- ask
let (k, delta) = cxtPushEntry (One (Domain vSize kSize dec)) (context cxtenv)
let xv = VGen k
let v12 = One xv
let rho = update (environ cxtenv) x v12
let beta = Bound ltle (Measure [xv]) (Measure [v])
x' <- uniqueName x k
local (\ cxt -> 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 x dom12 f = do
let tv12 = fmap typ dom12
enter ("new " ++ show x ++ " : " ++ show tv12) $ do
cxtenv <- ask
let (k, delta) = cxtPushEntry dom12 (context cxtenv)
v12 <- Traversable.mapM (up False (VGen k)) tv12
let rho = update (environ cxtenv) x v12
x' <- uniqueName x k
local (\ cxt -> 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 k dom =
local (\ ce -> ce { context = cxtSetType k dom (context ce) })
setTypeOfName x dom cont = do
ce <- ask
let Just k = Map.lookup x (renaming ce)
setType k dom cont
genOfName x = do
ce <- ask
case Map.lookup x (renaming ce) of
Nothing -> throwErrorMsg $ "internal error: variable not bound: " ++ show x
Just k -> return k
nameOfGen k = do
ce <- ask
case Map.lookup k (naming ce) of
Nothing -> return $ fresh $ "error_unnamed_gen" ++ show k
-- throwErrorMsg $ "internal error: no name for variable " ++ show k
Just x -> return x
{-
nameTaken "" = return True
nameTaken x = do
ce <- ask
st <- get
return (Map.member x (renaming ce) || Map.member x (signature st))
-}
lookupGen k = do
ce <- ask
cxtLookupGen (context ce) k
lookupName x = do
ce <- ask
cxtLookupName (context ce) (renaming ce) x
-- does not work with shadowing!
getContextTele = do
ce <- ask
let cxt = context ce
let ren = renaming ce
let env = envMap $ environ ce
let mkTBind (x,_) = (TBind x .fromOne . domain) <$> cxtLookupName cxt ren x
mapM mkTBind env
getLen = do
ce <- ask
return $ len (context ce)
getRen = do
ce <- ask
return $ renaming ce
-- since we only use getEnv during type checking, no case for Two
-- (during equality/subtype checking, we have values)
getEnv = do
ce <- ask
let (Environ rho mmeas) = environ ce
return $ Environ (map (\ (x, One v) -> (x, v)) rho) mmeas
applyDec dec = local (\ ce -> 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 rew vs cont = traceRew ("adding rewrite " ++ show rew) $
-- add rewriting rule
local (\ cxt -> cxt { rewrites = rew : (rewrites cxt) }) $ do
ce <- 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 (\ (x,v12) -> Traversable.mapM reval v12 >>= \ v12' -> return (x, v12')) rho
let en' = Environ rho' mmeas -- no need to rewrite in measure since only size expressions
-- normalize given values
vs' <- mapM reval vs
-- continue in updated context
local (\ ce -> ce { context = (context ce) { cxt = cx' }
, environ = en' }) $ cont vs'
-- addPattern :: TVal -> Pattern -> (TVal -> Val -> Env -> m a) -> m a
addPattern tv@(VQuant Pi x dom fv) p rho cont =
case p of
VarP y -> underAbs y dom fv $ \ _ xv bv -> do
cont bv xv (update rho y xv)
SizeP e y -> underAbs y dom fv $ \ j xv bv -> do
ve <- whnf' 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 pi n pl -> do
sige <- lookupSymbQ n
vc <- conLType n (typ dom)
addPatterns vc pl rho $ \ vc' vpl rho -> do -- apply dom to pl?
pv0 <- mkConVal notDotted (coPat pi) n vpl 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 p2 -> do
addPattern (vSize `arrow` vSize) p2 rho $ \ _ vp2 rho -> do
let pv = succSize vp2
vb <- app fv pv
cont vb pv rho
ErasedP p -> addPattern tv p rho 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 e -> do
v <- whnf rho e
vb <- app fv v
cont vb v rho -- [(x,v)]
addPatterns tv [] rho cont = cont tv [] rho
addPatterns tv (p:ps) rho cont =
addPattern tv p rho $ \ tv' v env ->
addPatterns tv' ps env $ \ tv'' vs env' ->
cont tv'' (v:vs) env' -- (env' ++ env)
addSizeRel son dist father k = do
let s = "v" ++ show son ++ " + " ++ show dist ++ " <= v" ++ show father
enter -- enterTrace
("adding size rel. " ++ s) $ do
let modBI belowInfty = if father `elem` belowInfty || dist > 0 then son : belowInfty else belowInfty
whenM (asks consistencyCheck `andLazy` do
TSO.increasesHeight son (dist, father) <$> asks sizeRels) $ do
recoverFail $ "cannot add hypothesis " ++ s ++ " 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
whenJustM (TSO.isAncestor father son <$> asks sizeRels) $ \ n -> -- n steps from father up to son
when (dist > - n) $ -- still ok if dist == n == 0, otherwise fail
recoverFail$ "cannot add hypothesis " ++ s ++ " because it makes the set of hyptheses unsatisfiable"
local (\ cxt -> cxt
{ sizeRels = TSO.insert son (dist, father) (sizeRels cxt)
, belowInfty = modBI (belowInfty cxt)
}) k
addBelowInfty i = local $ \ cxt -> cxt { belowInfty = i : belowInfty cxt }
addBoundHyp beta@(Bound ltle (Measure mu) (Measure mu')) cont =
case (ltle, mu, mu') of
(Le, _, [VInfty]) -> cont
-- (Lt, _, [VInfty]) -> failure -- handle j < #
(ltle, [v], [v']) -> loop (if ltle==Lt then 1 else 0) v v'
_ -> failure
where failure = do
-- recoverFail $ "adding hypothetical constraint " ++ show beta ++ " not supported"
assertDoc' Warning False (text "hypothetical constraint" <+> prettyTCM beta <+> text "ignored")
cont
loop n (VGen i) VInfty = addBelowInfty i cont
loop n (VGen i) (VGen j) | n >= 0 = addSizeRel i n j cont
| otherwise = addIrregularBound i j (-n) cont
loop n (VSucc v) v' = loop (n + 1) v v'
loop n v (VSucc v') = loop (n - 1) v v'
loop _ _ _ = failure
addIrregularBound i j n = local (\ ce -> ce { bounds = beta : bounds ce }) where
v' = iterate VSucc (VGen j) !! n
beta = Bound Le (Measure [VGen i]) (Measure [v'])
isBelowInfty i = (i `elem`) <$> asks 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 son ancestor = do
cxt <- ask
return $ TSO.isAncestor son ancestor (sizeRels cxt)
{-
getSizeDiff son ancestor = do
cxt <- ask
return $ TSO.diff son ancestor (sizeRels cxt)
-}
getMinSize parent = do
cxt <- ask
return $ TSO.height parent (sizeRels cxt)
getSizeVarsInScope = do
TCContext { context = delta, naming = nam } <- ask
-- get all the size variables with positive or mixed polarity
let fSize (i, tv12) =
case tv12 of
One dom -> isVSize $ typ dom
_ -> -- trace ("not a size variable " ++ show i ++ " : " ++ show tv12) $
False
-- create a list of key (gen) and Domain pairs for the size variables
let idl = filter fSize $ Map.toAscList (cxt delta)
let udecs = upperDecs delta
let fPos (i, One dom) =
case fromPProd (polarity (Maybe.fromJust (Map.lookup i udecs))) of
Just p -> leqPol (polarity (decor dom)) p
Nothing -> False
let fName (i, _) = Maybe.fromJust $ Map.lookup i nam
return $ map fName $ filter fPos idl
checkingCon b = local (\ cxt -> 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 k = do
b <- asks checkingConType
if b then k else applyDec (Dec Neg) k
setCo co = local (\ cxt -> cxt { mutualCo = co })
-- install functions for checking function clauses
-- ==> use internal names
installFuns co kfuns k = do
let funt = foldl (\ m fun@(Kinded _ (Fun (TypeSig n _) n' _ _)) -> Map.insert n fun m)
Map.empty
kfuns
local (\ cxt -> cxt { mutualCo = co, funsTemplate = funt }) k
setMeasure mu k = do
rho0 <- getEnv
let rho = rho0 { envBound = Just mu }
local (\ cxt -> cxt
{ environ = (environ cxt) { envBound = Just mu }
}) k
activateFuns k = do
rho <- getEnv
case (envBound rho) of
Nothing -> k
Just mu ->
local (\ cxt -> cxt
{ mutualFuns =
Map.map (boundFun rho (mutualCo cxt)) (funsTemplate cxt)
}) k
where boundFun :: Env -> Co -> Kinded Fun -> SigDef
boundFun rho co (Kinded ki (Fun (TypeSig n t) n' ar cls)) =
FunSig co (VClos rho t) ki ar cls False 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 = local (\ cxt -> cxt { impredicative = True })
checkingMutual mn = local (\ cxt -> 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 x dom fv cont = newWithGen x dom $ \ i xv -> cont i xv =<< app fv xv
-- | Do not check consistency preservation of context.
underAbs_ :: Name -> Domain -> FVal -> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a
underAbs_ x dom fv cont = noConsistencyChecking $ underAbs x dom fv cont
noConsistencyChecking = local $ \ cxt -> cxt { consistencyCheck = False }
-- | No eta, no hypotheses. First returned val is a @VGen i@.
underAbs' :: Name -> FVal -> (Val -> Val -> TypeCheck a) -> TypeCheck a
underAbs' x fv cont = addName x $ \ xv -> cont xv =<< app fv xv
-- addBind :: MonadTCM m => TBind -> m a -> m a
addBind :: TBind -> TypeCheck a -> TypeCheck a
addBind (TBind x dom) cont = do
dom' <- (Traversable.mapM whnf' dom)
new' x dom' cont
addBinds :: Telescope -> TypeCheck a -> TypeCheck a
addBinds tel k0 = foldr addBind k0 $ telescope tel
-- introduce patterns into context and environment -------------------
-- DOES NOT ETA-EXPAND VARIABLES!! -----------------------------------
introPatterns :: [Pattern] -> TVal -> ([(Pattern,Val)] -> TVal -> TypeCheck a) -> TypeCheck a
introPatterns ps tv cont = -- Problem: NO ETA EXPANSION!
introPatVars ps $ do -- first bind pattern variables
vs <- mapM (whnf' . patternToExpr) ps -- now we can evaluate patterns
let pvs = zip ps 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 p cont =
case p of
VarP n -> addName n $ \ _ -> cont
SizeP m n -> addName n $ \ _ -> cont
ConP co n pl -> introPatVars pl cont
PairP p1 p2 -> introPatVars [p1,p2] cont
SuccP p -> introPatVar p cont
ProjP{} -> cont
DotP e -> cont
AbsurdP -> cont
ErasedP p -> introPatVar p cont
introPatVars :: [Pattern] -> TypeCheck a -> TypeCheck a
introPatVars [] cont = cont
introPatVars (p:ps) cont = introPatVar p $ introPatVars ps $ 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 (p,v) tv cont = do
case tv of
VGuard beta bv -> addBoundHyp beta $ introPatType (p,v) bv cont
VApp (VDef (DefId DatK d)) vl ->
case p of
ProjP n -> cont =<< projectType tv n VIrr -- no record value here
_ -> throwErrorMsg $ "introPatType: internal error, expected projection pattern, found " ++ show p ++ " at type " ++ show tv
VQuant Pi x dom fv -> do
v <- whnfClos v
matchPatType (p,v) dom . cont =<< app fv v
_ -> throwErrorMsg $ "introPatType: internal error, expected Pi-type, found " ++ show tv
introPatTypes :: [(Pattern,Val)] -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a
introPatTypes pvs tv f = do
case pvs of
[] -> f tv
(pv:pvs') -> introPatType pv tv $ \ tv' -> introPatTypes pvs' tv' f
matchPatType :: (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
matchPatType (p,v) dom cont =
case (p,v) of
-- erasure does not matter!
(VarP y, VGen k) -> setType k dom $ cont
(SizeP z y, VGen k) -> setType k dom $ cont
(ConP co n [], _) -> cont
(ConP co n pl, VApp (VDef (DefId ConK{} _)) vl) -> do
{-
sige <- lookupSymb n
let vc = symbTyp sige
-}
vc <- conType n =<< force (typ dom)
introPatTypes (zip pl vl) vc $ \ _ -> cont
(SuccP p2, VSucc v2) -> matchPatType (p2, v2) (defaultDomain vSize) $ cont
(PairP p1 p2, VPair v1 v2) -> do
av <- force (typ dom)
case av of
VQuant Sigma x dom1@(Domain av1 ki dec) fv -> do
matchPatType (p1,v1) dom1 $ do
bv <- app fv v1
matchPatType (p2,v2) (Domain bv ki dec) cont
_ -> throwErrorMsg $ "matchPatType: IMPOSSIBLE " ++ show p ++ " : " ++ show dom
(DotP e, _) -> cont
(AbsurdP, _) -> cont
(ErasedP p,_) -> matchPatType (p,v) dom cont
_ -> throwErrorMsg $ "matchPatType: IMPOSSIBLE " ++ show (p,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 { isCo :: Co
, symbTyp :: TVal
, symbolKind :: Kind
, arity :: Arity
, clauses :: [Clause]
, isTypeChecked :: Bool
, extrTyp :: Expr -- ^ Fomega type.
}
| LetSig { symbTyp :: TVal
, symbolKind :: Kind
, definingVal :: Val
-- , definingExpr :: Expr
, extrTyp :: Expr -- ^ Fomega type.
}
| PatSig { patVars :: [Name]
, definingPat :: Pattern
, definingVal :: Val
}
| ConSig { conPars :: ConPars
-- ^ Parameter patterns and no. of variable they bind.
-- @Nothing@ if old-style parameters.
, 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.
, recOccs :: [Bool]
-- ^ @True@ if argument contains rec.occs.of the (co)data type?
, symbTyp :: TVal -- ^ (RHS) type, includs parameter tel.
, dataName :: Name -- ^ Its datatype.
, dataPars :: Int -- ^ No. of parameters of its datatype.
, extrTyp :: Expr -- ^ Fomega type.
}
| DataSig { numPars :: Int
, positivity :: [Pol]
, 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.
, constructors :: [ConstructorInfo]
, etaExpand :: Bool -- non-overlapping pattern inductive family
-- with at least one eta-expandable constructor
, 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 (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 n = do
sig <- lookupSymbQ n
case sig of
DataSig { constructors } -> return $ null constructors
_ -> throwErrorMsg $ "internal error: isEmptyData " ++ show n ++ ": name of data type expected"
isUnitData :: QName -> TypeCheck Bool
isUnitData n = do
sig <- lookupSymbQ n
case sig of
DataSig { constructors = [c], isTuple } -> return $
isTuple && null (cFields c) && cPatFam c == (LinearPatterns, [])
DataSig { constructors } -> return False
_ -> throwErrorMsg $ "internal error: isUnitData " ++ show n ++ ": name of data type expected"
undefinedFType :: QName -> Expr
undefinedFType n = Irr
-- undefinedFType n = error $ "no extracted type for " ++ show n
symbKind :: SigDef -> Kind
symbKind ConSig{} = kTerm -- constructors are always terms
symbKind d = symbolKind d -- else: lookup
{- Data types can be big!!
symbKind DataSig{} = kType -- data types are never universes
-}
emptySig = 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 tv = do
tv <- force 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 DatK n)) vs -> return $ Data (unqual n) vs
VSing v dv -> dataView =<< whnfClos dv
_ -> return $ NoData
-- | Disambiguate possibly overloaded constructor @c@ at given type @tv@.
disambigCon :: QName -> TVal -> TypeCheck QName
disambigCon c tv =
case c of
Qual{} -> return c
QName n -> do
dv <- dataView tv
case dv of
Data d _ -> return $ Qual d n
_ -> throwErrorMsg $ "cannot resolve constructor " ++ show n
-- | @conType c tv@ returns the type of constructor @c@ at datatype @tv@
-- with parameters instantiated.
conType :: QName -> TVal -> TypeCheck TVal
conType c tv = do
c <- disambigCon c 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 c tv = do
c <- disambigCon c tv
ConSig { conPars, lhsTyp, symbTyp, dataName, dataPars } <- lookupSymbQ c
case lhsTyp of
Nothing -> instConType c conPars symbTyp dataName dataPars tv
Just (x, lTyp) -> instConType c (fmap (inc x) conPars) lTyp dataName (dataPars+1) tv
where inc x (xs, ps) = (xs ++ [x], ps ++ [VarP 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 c conPars symbTyp dataName dataPars tv =
instConLType' c conPars symbTyp Nothing (Just dataName) dataPars 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 c conPars rhsTyp lhsTyp isFlex dataPars dataTyp =
instConLType' c conPars rhsTyp (fmap (,isFlex) lhsTyp) Nothing dataPars dataTyp
-- | The common pattern behind @instConType@ and @instConLType@.
instConLType' :: QName -> ConPars -> TVal -> Maybe ((Name, TVal), Val -> Bool) -> Maybe Name -> Int -> TVal -> TypeCheck TVal
instConLType' c conPars symbTyp isSized md dataPars tv =
enter ("instConLType'") $ do
let failure = failDoc (text ("conType " ++ show c ++ ": expected")
<+> prettyTCM tv
<+> text ("to be a data type applied to all of its " ++
show dataPars ++ " parameters"))
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
whenJust md $ \ d' ->
unless (d == d') $ throwErrorMsg $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show d'
-- whenJust conPars $ throwErrorMsg $ "NYI: constructor with pattern parameters"
let (pars, inds) = splitAt dataPars vs
unless (length pars == dataPars) failure
case (isSized, inds) of
(Just _, []) -> failure
-- if size index not flexible, use lhs type
(Just ((x,ltv), isFlex), sizeInd:_) | not (isFlex sizeInd) ->
continue d [x] ltv (pars ++ [sizeInd])
-- otherwise, use rhs type
_ -> continue d [] symbTyp pars
where
continue d ys tv pars = case conPars of
Nothing -> piApps tv pars
Just (xs, ps) -> do
let failure = failDoc $ sep
[ text "instConType:"
, text "cannot match parameters" <+> prettyList (map prettyTCM pars)
, text "against patterns" <+> prettyList (map prettyTCM ps)
, text "when instantiating type" <+> prettyTCM tv
, text ("of constructor " ++ show c)
]
-- clear dots here:
mst <- nonLinMatchList' True True (emptyEnv, []) ps pars =<< lookupSymbTyp d
case mst of
Nothing -> failure
Just (Environ{ envMap = env0 }, psub) -> do
let env = env0 ++ [ (x, VGen i) | (i, VarP x) <- psub ]
-- if length env /= length xs then failure else do
vs <- forM (xs ++ ys) $ \ x -> maybe failure return $ lookup x 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 = lookupSymbTypQ . QName
lookupSymb :: Name -> m SigDef
lookupSymb = lookupSymbQ . QName
addSig :: Name -> SigDef -> m ()
addSig = addSigQ . QName
modifySig :: Name -> (SigDef -> SigDef) -> m ()
modifySig = modifySigQ . QName
setExtrTyp :: Name -> Expr -> m ()
setExtrTyp = setExtrTypQ . QName
-- Signature implementation ------------------------------------------
instance MonadSig TypeCheck where
-- first in context, then in signature
-- lookupSymbTyp :: Name -> TypeCheck TVal
lookupSymbTyp n = do
mdom <- errorToMaybe $ lookupName1 n
case mdom of
Just (CxtEntry dom udec) -> return (typ dom)
Nothing -> symbTyp <$> lookupSymb n
lookupSymbTypQ (QName n) = lookupSymbTyp n
lookupSymbTypQ n@Qual{} = symbTyp <$> lookupSymbQ n
-- lookupSymb :: Name -> TypeCheck SigDef
lookupSymb n = do
cxt <- ask
case Map.lookup n (mutualFuns cxt) of
Just k -> return $ k
Nothing -> lookupSymbInSig (QName n)
lookupSymbQ (QName n) = lookupSymb n
lookupSymbQ n@Qual{} = lookupSymbInSig n
-- addSig :: Name -> SigDef -> TypeCheck ()
addSigQ n def = traceSig ("addSig: " ++ show n ++ " is bound to " ++ show def) $ do
st <- get
put $ st { signature = Map.insert n def $ signature st }
-- modifySig :: Name -> (SigDef -> SigDef) -> TypeCheck ()
modifySigQ n f = do
st <- get
put $ st { signature = Map.adjust f n $ signature st }
-- setExtrTyp :: Name -> Expr -> TypeCheck ()
setExtrTypQ n t = modifySigQ n (\ d -> d { extrTyp = t })
lookupSymbInSig :: QName -> TypeCheck SigDef
lookupSymbInSig n = lookupSig n =<< gets signature
where
-- lookupSig :: Name -> Signature -> TypeCheck SigDef
lookupSig n sig =
case (Map.lookup n sig) of
Nothing -> throwErrorMsg $ "identifier " ++ show n ++ " not in signature " ++ show (Map.keys sig)
Just k -> return k
-- more on the type checking monad -------------------------------
initSt :: TCState
initSt = TCState emptySig emptyMetaVars emptyConstraints emptyPosGraph -- emptyDots
initWithSig :: Signature -> TCState
initWithSig sig = 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 Le v1 v2 = addLeq v1 v2
addLe Lt v1 v2 = addLeq (succSize v1) v2 -- broken for #
solveConstraints :: m Solution
-- solve constraints and substitute solution into the analyzed expressions
solveAndModify :: [Expr] -> Env -> m [Expr]
solveAndModify es rho = do
sol <- solveConstraints
let es' = map (subst (solToSubst sol rho)) es
resetConstraints
return es'
-- Constraints implementation ----------------------------------------
instance MonadMeta TypeCheck where
--resetConstraints :: TypeCheck ()
resetConstraints = do
st <- get
put $ st { constraints = emptyConstraints }
-- mkConstraint :: Val -> Val -> TypeCheck (Maybe Constraint)
mkConstraint v (VMax vs) = do
bs <- mapM (errorToBool . leqSize' v) vs
if any id bs then return Nothing else
throwErrorMsg $ "cannot handle constraint " ++ show v ++ " <= " ++ show (VMax vs)
mkConstraint w@(VMax vs) v = throwErrorMsg $ "cannot handle constraint " ++ show w ++ " <= " ++ show v
mkConstraint (VMeta i rho n) (VMeta j rho' m) = retret $ arc (Flex i) (m-n) (Flex j)
mkConstraint (VMeta i rho n) VInfty = retret $ arc (Flex i) 0 (Rigid (RConst Infinite))
mkConstraint (VMeta i rho n) v = retret $ arc (Flex i) (m-n) (Rigid (RVar j))
where (j,m) = vGenSuccs v 0
mkConstraint VInfty (VMeta i rho n) = retret $ arc (Rigid (RConst Infinite)) 0 (Flex i)
mkConstraint v (VMeta j rho m) = retret $ arc (Rigid (RVar i)) (m-n) (Flex j)
where (i,n) = vGenSuccs v 0
mkConstraint v1 v2 = throwErrorMsg $ "mkConstraint undefined for " ++ show (v1,v2)
-- addMeta k x adds a metavariable which can refer to VGens < k
-- addMeta :: Ren -> MVar -> TypeCheck ()
addMeta ren i = do
scope <- getSizeVarsInScope
traceMetaM ("addMeta " ++ show i ++ " scope " ++ show scope)
st <- get
put $ st { metaVars = Map.insert i (MetaVar scope Nothing) (metaVars st)
, constraints = NewFlex i (\ k' -> True) -- k' < k)
-- DO NOT ADD constraints of form <= infty !!
-- : arc (Flex i) 0 (Rigid (RConst Infinite))
: constraints st }
-- addLeq :: Val -> Val -> TypeCheck ()
addLeq v1 v2 = traceMeta ("Constraint: " ++ show v1 ++ " <= " ++ show v2) $
do mc <- mkConstraint v1 v2
case mc of
Nothing -> return ()
Just c -> do
st <- get
put $ st { constraints = c : constraints st }
-- solveConstraints :: TypeCheck Solution
solveConstraints = do
cs <- gets constraints
if null cs then return emptySolution
else case solve cs of
Just subst -> traceMeta ("solution" ++ show subst) $
return subst
Nothing -> throwErrorMsg $ "size constraints " ++ show cs ++ " unsolvable"
nameOf :: EnvMap -> Int -> Maybe Name
nameOf [] j = Nothing
nameOf ((x,VGen i):rho) j | i == j = Just x
nameOf (_:rho) j = nameOf rho j
vGenSuccs (VGen k) m = (k,m)
vGenSuccs (VSucc v) m = vGenSuccs v (m+1)
vGenSuccs v m = error $ "vGenSuccs fails on " ++ Util.parens (show v) ++ " " ++ show m
retret = return . return
sizeExprToExpr :: Env -> SizeExpr -> Expr
sizeExprToExpr rho (SizeConst Infinite) = Infty
sizeExprToExpr rho (SizeVar i n) | Just x <- nameOf (envMap rho) i = add (Var x) n
where add e n | n <= 0 = e
| otherwise = add (Succ e) (n-1)
sizeExprToExpr rho e@(SizeVar i n) | Nothing <- nameOf (envMap rho) i = error $ "panic: sizeExprToExpr " ++ Util.parens (show e) ++ ": variable v" ++ show i ++ " not in scope " ++ show (envMap rho)
maxExpr :: [Expr] -> Expr
maxExpr [] = Infty
maxExpr [e] = e
maxExpr l = if Infty `elem` l then Infty else Max l
solToSubst :: Solution -> Env -> Subst
solToSubst sol rho = Map.map (maxExpr . map (sizeExprToExpr rho)) 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'')
-}