MiniAgda-0.2025.7.23: 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)
#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 msg a = a
traceRew :: String -> a -> a
traceRew msg a = a -- trace msg a
traceRewM :: Monad m => String -> m ()
traceRewM msg = return () -- traceM msg
{-
traceRew msg a = trace msg a
traceRewM msg = traceM msg
-}
-- metavariables and constraints
traceMeta :: String -> a -> a
traceMeta msg a = a -- trace msg a
traceMetaM :: Monad m => String -> m ()
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
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 :: MetaVars
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 :: 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 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 :: Rewrites
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
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) }
-- 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 :: 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 :: TypeCheck a -> TypeCheck a
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 :: Signature
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) = return $ Just $ arc (Flex i) (m-n) (Flex j)
mkConstraint (VMeta i rho n) VInfty = return $ Just $ arc (Flex i) 0 (Rigid (RConst Infinite))
mkConstraint (VMeta i rho n) v = return $ Just $ arc (Flex i) (m-n) (Rigid (RVar j))
where (j,m) = vGenSuccs v 0
mkConstraint VInfty (VMeta i rho n) = return $ Just $ arc (Rigid (RConst Infinite)) 0 (Flex i)
mkConstraint v (VMeta j rho m) = return $ Just $ 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 :: Val -> Int -> (Int, Int)
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
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'')
-}