mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
the evaluator and the typechecker now share the same monad
This commit is contained in:
Krasimir Angelov
@@ -6,7 +6,7 @@ module GF.Compile.Compute.Concrete
|
||||
( normalForm
|
||||
, Value(..), Thunk, ThunkState(..), Env, Scope, showValue
|
||||
, MetaThunks
|
||||
, EvalM(..), runEvalM, evalError
|
||||
, EvalM(..), runEvalM, runEvalOneM, evalError, evalWarn
|
||||
, eval, apply, force, value2term, patternMatch
|
||||
, newThunk, newEvaluatedThunk
|
||||
, newResiduation, newNarrowing, getVariables
|
||||
@@ -450,30 +450,30 @@ vtableSelect v0 ty tnks tnk2 vs = do
|
||||
"cannot be evaluated at compile time.")
|
||||
|
||||
|
||||
susp i env ki = EvalM $ \gr k mt d r -> do
|
||||
susp i env ki = EvalM $ \gr k mt d r msgs -> do
|
||||
s <- readSTRef i
|
||||
case s of
|
||||
Narrowing id (QC q) -> case lookupOrigInfo gr q of
|
||||
Ok (m,ResParam (Just (L _ ps)) _) -> bindParam gr k mt d r s m ps
|
||||
Bad msg -> return (Fail (pp msg))
|
||||
Ok (m,ResParam (Just (L _ ps)) _) -> bindParam gr k mt d r msgs s m ps
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
Narrowing id ty
|
||||
| Just max <- isTypeInts ty
|
||||
-> bindInt gr k mt d r s 0 max
|
||||
-> bindInt gr k mt d r msgs s 0 max
|
||||
Evaluated _ v -> case ki v of
|
||||
EvalM f -> f gr k mt d r
|
||||
_ -> k (VSusp i env ki []) mt d r
|
||||
EvalM f -> f gr k mt d r msgs
|
||||
_ -> k (VSusp i env ki []) mt d r msgs
|
||||
where
|
||||
bindParam gr k mt d r s m [] = return (Success r)
|
||||
bindParam gr k mt d r s m ((p, ctxt):ps) = do
|
||||
bindParam gr k mt d r msgs s m [] = return (Success r msgs)
|
||||
bindParam gr k mt d r msgs s m ((p, ctxt):ps) = do
|
||||
(mt',tnks) <- mkArgs mt ctxt
|
||||
let v = VApp (m,p) tnks
|
||||
writeSTRef i (Evaluated (length env) v)
|
||||
res <- case ki v of
|
||||
EvalM f -> f gr k mt' d r
|
||||
EvalM f -> f gr k mt' d r msgs
|
||||
writeSTRef i s
|
||||
case res of
|
||||
Fail msg -> return (Fail msg)
|
||||
Success r -> bindParam gr k mt d r s m ps
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success r msgs -> bindParam gr k mt d r msgs s m ps
|
||||
|
||||
mkArgs mt [] = return (mt,[])
|
||||
mkArgs mt ((_,_,ty):ctxt) = do
|
||||
@@ -484,17 +484,17 @@ susp i env ki = EvalM $ \gr k mt d r -> do
|
||||
(mt,tnks) <- mkArgs (Map.insert i tnk mt) ctxt
|
||||
return (mt,tnk:tnks)
|
||||
|
||||
bindInt gr k mt d r s iv max
|
||||
bindInt gr k mt d r msgs s iv max
|
||||
| iv <= max = do
|
||||
let v = VInt iv
|
||||
writeSTRef i (Evaluated (length env) v)
|
||||
res <- case ki v of
|
||||
EvalM f -> f gr k mt d r
|
||||
EvalM f -> f gr k mt d r msgs
|
||||
writeSTRef i s
|
||||
case res of
|
||||
Fail msg -> return (Fail msg)
|
||||
Success r -> bindInt gr k mt d r s (iv+1) max
|
||||
| otherwise = return (Success r)
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success r msgs -> bindInt gr k mt d r msgs s (iv+1) max
|
||||
| otherwise = return (Success r msgs)
|
||||
|
||||
|
||||
value2term xs (VApp q tnks) =
|
||||
@@ -686,7 +686,7 @@ value2int _ = RunTime
|
||||
-- * Evaluation monad
|
||||
|
||||
type MetaThunks s = Map.Map MetaId (Thunk s)
|
||||
type Cont s r = MetaThunks s -> Int -> r -> ST s (CheckResult r)
|
||||
type Cont s r = MetaThunks s -> Int -> r -> [Message] -> ST s (CheckResult r [Message])
|
||||
newtype EvalM s a = EvalM (forall r . Grammar -> (a -> Cont s r) -> Cont s r)
|
||||
|
||||
instance Functor (EvalM s) where
|
||||
@@ -705,90 +705,101 @@ instance Monad (EvalM s) where
|
||||
#endif
|
||||
|
||||
instance Fail.MonadFail (EvalM s) where
|
||||
fail msg = EvalM (\gr k _ _ r -> return (Fail (pp msg)))
|
||||
fail msg = EvalM (\gr k _ _ r msgs -> return (Fail (pp msg) msgs))
|
||||
|
||||
instance Alternative (EvalM s) where
|
||||
empty = EvalM (\gr k _ _ r -> return (Success r))
|
||||
(EvalM f) <|> (EvalM g) = EvalM $ \gr k mt b r -> do
|
||||
res <- f gr k mt b r
|
||||
empty = EvalM (\gr k _ _ r msgs -> return (Success r msgs))
|
||||
(EvalM f) <|> (EvalM g) = EvalM $ \gr k mt b r msgs -> do
|
||||
res <- f gr k mt b r msgs
|
||||
case res of
|
||||
Fail msg -> return (Fail msg)
|
||||
Success r -> g gr k mt b r
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success r msgs -> g gr k mt b r msgs
|
||||
|
||||
instance MonadPlus (EvalM s) where
|
||||
|
||||
runEvalM :: Grammar -> (forall s . EvalM s a) -> Check [a]
|
||||
runEvalM gr f =
|
||||
runEvalM gr f = Check $ \(es,ws) ->
|
||||
case runST (case f of
|
||||
EvalM f -> f gr (\x mt _ xs -> return (Success (x:xs))) Map.empty maxBound []) of
|
||||
Fail msg -> checkError msg
|
||||
Success xs -> return (reverse xs)
|
||||
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of
|
||||
Fail msg ws -> Fail msg (es,ws)
|
||||
Success xs ws -> Success (reverse xs) (es,ws)
|
||||
|
||||
evalError :: Doc -> EvalM s a
|
||||
evalError msg = EvalM (\gr k _ _ r -> return (Fail msg))
|
||||
runEvalOneM :: Grammar -> (forall s . EvalM s a) -> Check a
|
||||
runEvalOneM gr f = Check $ \(es,ws) ->
|
||||
case runST (case f of
|
||||
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of
|
||||
Fail msg ws -> Fail msg (es,ws)
|
||||
Success [] ws -> Fail (pp "The evaluation produced no results") (es,ws)
|
||||
Success (x:_) ws -> Success x (es,ws)
|
||||
|
||||
evalError :: Message -> EvalM s a
|
||||
evalError msg = EvalM (\gr k _ _ r msgs -> return (Fail msg msgs))
|
||||
|
||||
evalWarn :: Message -> EvalM s ()
|
||||
evalWarn msg = EvalM (\gr k mt d r msgs -> k () mt d r (msg:msgs))
|
||||
|
||||
getResDef :: QIdent -> EvalM s Term
|
||||
getResDef q = EvalM $ \gr k mt d r -> do
|
||||
getResDef q = EvalM $ \gr k mt d r msgs -> do
|
||||
case lookupResDef gr q of
|
||||
Ok t -> k t mt d r
|
||||
Bad msg -> return (Fail (pp msg))
|
||||
Ok t -> k t mt d r msgs
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
|
||||
getInfo :: QIdent -> EvalM s (ModuleName,Info)
|
||||
getInfo q = EvalM $ \gr k mt d r -> do
|
||||
getInfo q = EvalM $ \gr k mt d r msgs -> do
|
||||
case lookupOrigInfo gr q of
|
||||
Ok res -> k res mt d r
|
||||
Bad msg -> return (Fail (pp msg))
|
||||
Ok res -> k res mt d r msgs
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
|
||||
getResType :: QIdent -> EvalM s Type
|
||||
getResType q = EvalM $ \gr k mt d r -> do
|
||||
getResType q = EvalM $ \gr k mt d r msgs -> do
|
||||
case lookupResType gr q of
|
||||
Ok t -> k t mt d r
|
||||
Bad msg -> return (Fail (pp msg))
|
||||
Ok t -> k t mt d r msgs
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
|
||||
getAllParamValues :: Type -> EvalM s [Term]
|
||||
getAllParamValues ty = EvalM $ \gr k mt d r ->
|
||||
getAllParamValues ty = EvalM $ \gr k mt d r msgs ->
|
||||
case allParamValues gr ty of
|
||||
Ok ts -> k ts mt d r
|
||||
Bad msg -> return (Fail (pp msg))
|
||||
Ok ts -> k ts mt d r msgs
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
|
||||
newThunk env t = EvalM $ \gr k mt d r -> do
|
||||
newThunk env t = EvalM $ \gr k mt d r msgs -> do
|
||||
tnk <- newSTRef (Unevaluated env t)
|
||||
k tnk mt d r
|
||||
k tnk mt d r msgs
|
||||
|
||||
newEvaluatedThunk v = EvalM $ \gr k mt d r -> do
|
||||
newEvaluatedThunk v = EvalM $ \gr k mt d r msgs -> do
|
||||
tnk <- newSTRef (Evaluated maxBound v)
|
||||
k tnk mt d r
|
||||
k tnk mt d r msgs
|
||||
|
||||
newHole i = EvalM $ \gr k mt d r ->
|
||||
newHole i = EvalM $ \gr k mt d r msgs ->
|
||||
if i == 0
|
||||
then do tnk <- newSTRef (Hole i)
|
||||
k tnk mt d r
|
||||
k tnk mt d r msgs
|
||||
else case Map.lookup i mt of
|
||||
Just tnk -> k tnk mt d r
|
||||
Just tnk -> k tnk mt d r msgs
|
||||
Nothing -> do tnk <- newSTRef (Hole i)
|
||||
k tnk (Map.insert i tnk mt) d r
|
||||
k tnk (Map.insert i tnk mt) d r msgs
|
||||
|
||||
newResiduation scope ty = EvalM $ \gr k mt d r -> do
|
||||
newResiduation scope ty = EvalM $ \gr k mt d r msgs -> do
|
||||
tnk <- newSTRef (Residuation 0 scope ty)
|
||||
k tnk mt d r
|
||||
k tnk mt d r msgs
|
||||
|
||||
newNarrowing i ty = EvalM $ \gr k mt d r ->
|
||||
newNarrowing i ty = EvalM $ \gr k mt d r msgs ->
|
||||
if i == 0
|
||||
then do tnk <- newSTRef (Narrowing i ty)
|
||||
k tnk mt d r
|
||||
k tnk mt d r msgs
|
||||
else case Map.lookup i mt of
|
||||
Just tnk -> k tnk mt d r
|
||||
Just tnk -> k tnk mt d r msgs
|
||||
Nothing -> do tnk <- newSTRef (Narrowing i ty)
|
||||
k tnk (Map.insert i tnk mt) d r
|
||||
k tnk (Map.insert i tnk mt) d r msgs
|
||||
|
||||
withVar d0 (EvalM f) = EvalM $ \gr k mt d1 r ->
|
||||
withVar d0 (EvalM f) = EvalM $ \gr k mt d1 r msgs ->
|
||||
let !d = min d0 d1
|
||||
in f gr k mt d r
|
||||
in f gr k mt d r msgs
|
||||
|
||||
getVariables :: EvalM s [(LVar,LIndex)]
|
||||
getVariables = EvalM $ \gr k mt d r -> do
|
||||
getVariables = EvalM $ \gr k mt d ws r -> do
|
||||
ps <- metas2params gr (Map.elems mt)
|
||||
k ps mt d r
|
||||
k ps mt d ws r
|
||||
where
|
||||
metas2params gr [] = return []
|
||||
metas2params gr (tnk:tnks) = do
|
||||
@@ -803,65 +814,65 @@ getVariables = EvalM $ \gr k mt d r -> do
|
||||
else return params
|
||||
_ -> metas2params gr tnks
|
||||
|
||||
getRef tnk = EvalM $ \gr k mt d r -> readSTRef tnk >>= \st -> k st mt d r
|
||||
setRef tnk st = EvalM $ \gr k mt d r -> writeSTRef tnk st >>= \st -> k () mt d r
|
||||
getRef tnk = EvalM $ \gr k mt d ws r -> readSTRef tnk >>= \st -> k st mt d ws r
|
||||
setRef tnk st = EvalM $ \gr k mt d ws r -> writeSTRef tnk st >>= \st -> k () mt d ws r
|
||||
|
||||
force tnk = EvalM $ \gr k mt d r -> do
|
||||
force tnk = EvalM $ \gr k mt d r msgs -> do
|
||||
s <- readSTRef tnk
|
||||
case s of
|
||||
Unevaluated env t -> case eval env t [] of
|
||||
EvalM f -> f gr (\v mt b r -> do let d = length env
|
||||
writeSTRef tnk (Evaluated d v)
|
||||
r <- k v mt d r
|
||||
writeSTRef tnk s
|
||||
return r) mt d r
|
||||
Evaluated d v -> k v mt d r
|
||||
Hole _ -> k (VMeta tnk [] []) mt d r
|
||||
Residuation _ _ _ -> k (VMeta tnk [] []) mt d r
|
||||
Narrowing _ _ -> k (VMeta tnk [] []) mt d r
|
||||
EvalM f -> f gr (\v mt b r msgs -> do let d = length env
|
||||
writeSTRef tnk (Evaluated d v)
|
||||
r <- k v mt d r msgs
|
||||
writeSTRef tnk s
|
||||
return r) mt d r msgs
|
||||
Evaluated d v -> k v mt d r msgs
|
||||
Hole _ -> k (VMeta tnk [] []) mt d r msgs
|
||||
Residuation _ _ _ -> k (VMeta tnk [] []) mt d r msgs
|
||||
Narrowing _ _ -> k (VMeta tnk [] []) mt d r msgs
|
||||
|
||||
tnk2term xs tnk = EvalM $ \gr k mt d r ->
|
||||
tnk2term xs tnk = EvalM $ \gr k mt d r msgs ->
|
||||
let join f g = do res <- f
|
||||
case res of
|
||||
Fail msg -> return (Fail msg)
|
||||
Success r -> g r
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success r msgs -> g r msgs
|
||||
|
||||
flush [] k1 mt r = k1 mt r
|
||||
flush [x] k1 mt r = join (k x mt d r) (k1 mt)
|
||||
flush xs k1 mt r = join (k (FV (reverse xs)) mt d r) (k1 mt)
|
||||
flush [] k1 mt r msgs = k1 mt r msgs
|
||||
flush [x] k1 mt r msgs = join (k x mt d r msgs) (k1 mt)
|
||||
flush xs k1 mt r msgs = join (k (FV (reverse xs)) mt d r msgs) (k1 mt)
|
||||
|
||||
acc d0 x mt d (r,!c,xs)
|
||||
| d < d0 = flush xs (\mt r -> join (k x mt d r) (\r -> return (Success (r,c+1,[])))) mt r
|
||||
| otherwise = return (Success (r,c+1,x:xs))
|
||||
acc d0 x mt d (r,!c,xs) msgs
|
||||
| d < d0 = flush xs (\mt r msgs -> join (k x mt d r msgs) (\r msgs -> return (Success (r,c+1,[]) msgs))) mt r msgs
|
||||
| otherwise = return (Success (r,c+1,x:xs) msgs)
|
||||
|
||||
in do s <- readSTRef tnk
|
||||
case s of
|
||||
Unevaluated env t -> do let d0 = length env
|
||||
res <- case eval env t [] of
|
||||
EvalM f -> f gr (\v mt d r -> do writeSTRef tnk (Evaluated d0 v)
|
||||
r <- case value2term xs v of
|
||||
EvalM f -> f gr (acc d0) mt d r
|
||||
writeSTRef tnk s
|
||||
return r) mt maxBound (r,0,[])
|
||||
EvalM f -> f gr (\v mt d msgs r -> do writeSTRef tnk (Evaluated d0 v)
|
||||
r <- case value2term xs v of
|
||||
EvalM f -> f gr (acc d0) mt d msgs r
|
||||
writeSTRef tnk s
|
||||
return r) mt maxBound (r,0,[]) msgs
|
||||
case res of
|
||||
Fail msg -> return (Fail msg)
|
||||
Success (r,0,xs) -> k (FV []) mt d r
|
||||
Success (r,c,xs) -> flush xs (\mt r -> return (Success r)) mt r
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success (r,0,xs) msgs -> k (FV []) mt d r msgs
|
||||
Success (r,c,xs) msgs -> flush xs (\mt msgs r -> return (Success msgs r)) mt r msgs
|
||||
Evaluated d0 v -> do res <- case value2term xs v of
|
||||
EvalM f -> f gr (acc d0) mt maxBound (r,0,[])
|
||||
EvalM f -> f gr (acc d0) mt maxBound (r,0,[]) msgs
|
||||
case res of
|
||||
Fail msg -> return (Fail msg)
|
||||
Success (r,0,xs) -> k (FV []) mt d r
|
||||
Success (r,c,xs) -> flush xs (\mt r -> return (Success r)) mt r
|
||||
Hole i -> k (Meta i) mt d r
|
||||
Residuation i _ _ -> k (Meta i) mt d r
|
||||
Narrowing i _ -> k (Meta i) mt d r
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success (r,0,xs) msgs -> k (FV []) mt d r msgs
|
||||
Success (r,c,xs) msgs -> flush xs (\mt r msgs -> return (Success r msgs)) mt r msgs
|
||||
Hole i -> k (Meta i) mt d r msgs
|
||||
Residuation i _ _ -> k (Meta i) mt d r msgs
|
||||
Narrowing i _ -> k (Meta i) mt d r msgs
|
||||
|
||||
zonk tnk vs = EvalM $ \gr k mt d r -> do
|
||||
zonk tnk vs = EvalM $ \gr k mt d r msgs -> do
|
||||
s <- readSTRef tnk
|
||||
case s of
|
||||
Evaluated _ v -> case apply v vs of
|
||||
EvalM f -> f gr (k . Left) mt d r
|
||||
Hole i -> k (Right i) mt d r
|
||||
Residuation i _ _ -> k (Right i) mt d r
|
||||
Narrowing i _ -> k (Right i) mt d r
|
||||
EvalM f -> f gr (k . Left) mt d r msgs
|
||||
Hole i -> k (Right i) mt d r msgs
|
||||
Residuation i _ _ -> k (Right i) mt d r msgs
|
||||
Narrowing i _ -> k (Right i) mt d r msgs
|
||||
|
||||
@@ -23,20 +23,20 @@ import Data.Maybe(fromMaybe,isNothing)
|
||||
import qualified Control.Monad.Fail as Fail
|
||||
|
||||
checkLType :: Grammar -> Term -> Type -> Check (Term, Type)
|
||||
checkLType gr t ty = runTcM gr $ do
|
||||
vty <- liftEvalM (eval [] ty [])
|
||||
checkLType gr t ty = runEvalOneM gr $ do
|
||||
vty <- eval [] ty []
|
||||
(t,_) <- tcRho [] t (Just vty)
|
||||
t <- zonkTerm t
|
||||
return (t,ty)
|
||||
|
||||
inferLType :: Grammar -> Term -> Check (Term, Type)
|
||||
inferLType gr t = runTcM gr $ do
|
||||
inferLType gr t = runEvalOneM gr $ do
|
||||
(t,ty) <- inferSigma [] t
|
||||
t <- zonkTerm t
|
||||
ty <- zonkTerm =<< liftEvalM (value2term [] ty)
|
||||
ty <- zonkTerm =<< value2term [] ty
|
||||
return (t,ty)
|
||||
|
||||
inferSigma :: Scope s -> Term -> TcM s (Term,Sigma s)
|
||||
inferSigma :: Scope s -> Term -> EvalM s (Term,Sigma s)
|
||||
inferSigma scope t = do -- GEN1
|
||||
(t,ty) <- tcRho scope t Nothing
|
||||
env_tvs <- getMetaVars (scopeTypes scope)
|
||||
@@ -46,13 +46,13 @@ inferSigma scope t = do -- GEN1
|
||||
|
||||
vtypeInt = VApp (cPredef,cInt) []
|
||||
vtypeFloat = VApp (cPredef,cFloat) []
|
||||
vtypeInts i= liftEvalM (newEvaluatedThunk (VInt i)) >>= \tnk -> return (VApp (cPredef,cInts) [tnk])
|
||||
vtypeInts i= newEvaluatedThunk (VInt i) >>= \tnk -> return (VApp (cPredef,cInts) [tnk])
|
||||
vtypeStr = VSort cStr
|
||||
vtypeStrs = VSort cStrs
|
||||
vtypeType = VSort cType
|
||||
vtypePType = VSort cPType
|
||||
|
||||
tcRho :: Scope s -> Term -> Maybe (Rho s) -> TcM s (Term, Rho s)
|
||||
tcRho :: Scope s -> Term -> Maybe (Rho s) -> EvalM s (Term, Rho s)
|
||||
tcRho scope t@(EInt i) mb_ty = vtypeInts i >>= \sigma -> instSigma scope t sigma mb_ty -- INT
|
||||
tcRho scope t@(EFloat _) mb_ty = instSigma scope t vtypeFloat mb_ty -- FLOAT
|
||||
tcRho scope t@(K _) mb_ty = instSigma scope t vtypeStr mb_ty -- STR
|
||||
@@ -60,7 +60,7 @@ tcRho scope t@(Empty) mb_ty = instSigma scope t vtypeStr mb_ty
|
||||
tcRho scope t@(Vr v) mb_ty = do -- VAR
|
||||
case lookup v scope of
|
||||
Just v_sigma -> instSigma scope t v_sigma mb_ty
|
||||
Nothing -> tcError ("Unknown variable" <+> v)
|
||||
Nothing -> evalError ("Unknown variable" <+> v)
|
||||
tcRho scope t@(Q id) mb_ty =
|
||||
runTcA (tcOverloadFailed t) $ \gr ->
|
||||
tcApp gr scope t `bindTcA` \(t,ty) ->
|
||||
@@ -74,7 +74,7 @@ tcRho scope t@(App fun arg) mb_ty = do
|
||||
tcApp gr scope t `bindTcA` \(t,ty) ->
|
||||
instSigma scope t ty mb_ty
|
||||
tcRho scope (Abs bt var body) Nothing = do -- ABS1
|
||||
tnk <- liftEvalM (newResiduation scope vtypeType)
|
||||
tnk <- newResiduation scope vtypeType
|
||||
env <- scopeEnv scope
|
||||
let arg_ty = VMeta tnk env []
|
||||
(body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing
|
||||
@@ -83,7 +83,7 @@ tcRho scope t@(Abs Implicit var body) (Just ty) = do -- ABS2
|
||||
(bt, var_ty, body_ty) <- unifyFun scope ty
|
||||
if bt == Implicit
|
||||
then return ()
|
||||
else tcError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected")
|
||||
else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected")
|
||||
(body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty)
|
||||
return (Abs Implicit var body,ty)
|
||||
tcRho scope (Abs Explicit var body) (Just ty) = do -- ABS3
|
||||
@@ -96,21 +96,21 @@ tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET
|
||||
Nothing -> inferSigma scope rhs
|
||||
Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
|
||||
env <- scopeEnv scope
|
||||
v_ann_ty <- liftEvalM (eval env ann_ty [])
|
||||
v_ann_ty <- eval env ann_ty []
|
||||
(rhs,_) <- tcRho scope rhs (Just v_ann_ty)
|
||||
return (rhs, v_ann_ty)
|
||||
(body, body_ty) <- tcRho ((var,var_ty):scope) body mb_ty
|
||||
var_ty <- liftEvalM (value2term (scopeVars scope) var_ty)
|
||||
var_ty <- value2term (scopeVars scope) var_ty
|
||||
return (Let (var, (Just var_ty, rhs)) body, body_ty)
|
||||
tcRho scope (Typed body ann_ty) mb_ty = do -- ANNOT
|
||||
(ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
|
||||
env <- scopeEnv scope
|
||||
v_ann_ty <- liftEvalM (eval env ann_ty [])
|
||||
v_ann_ty <- eval env ann_ty []
|
||||
(body,_) <- tcRho scope body (Just v_ann_ty)
|
||||
instSigma scope (Typed body ann_ty) v_ann_ty mb_ty
|
||||
tcRho scope (FV ts) mb_ty = do
|
||||
case ts of
|
||||
[] -> do i <- liftEvalM (newResiduation scope vtypeType)
|
||||
[] -> do i <- newResiduation scope vtypeType
|
||||
env <- scopeEnv scope
|
||||
instSigma scope (FV []) (VMeta i env []) mb_ty
|
||||
(t:ts) -> do (t,ty) <- tcRho scope t mb_ty
|
||||
@@ -136,9 +136,9 @@ tcRho scope t@(RecType rs) (Just ty) = do
|
||||
VMeta i env vs -> case rs of
|
||||
[] -> unifyVar scope i env vs vtypePType
|
||||
_ -> return ()
|
||||
ty -> do ty <- zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)
|
||||
tcError ("The record type" <+> ppTerm Unqualified 0 t $$
|
||||
"cannot be of type" <+> ppTerm Unqualified 0 ty)
|
||||
ty -> do ty <- zonkTerm =<< value2term (scopeVars scope) ty
|
||||
evalError ("The record type" <+> ppTerm Unqualified 0 t $$
|
||||
"cannot be of type" <+> ppTerm Unqualified 0 ty)
|
||||
(rs,mb_ty) <- tcRecTypeFields scope rs (Just ty')
|
||||
return (f (RecType rs),ty)
|
||||
tcRho scope t@(Table p res) mb_ty = do
|
||||
@@ -148,14 +148,14 @@ tcRho scope t@(Table p res) mb_ty = do
|
||||
tcRho scope (Prod bt x ty1 ty2) mb_ty = do
|
||||
(ty1,ty1_ty) <- tcRho scope ty1 (Just vtypeType)
|
||||
env <- scopeEnv scope
|
||||
vty1 <- liftEvalM (eval env ty1 [])
|
||||
vty1 <- eval env ty1 []
|
||||
(ty2,ty2_ty) <- tcRho ((x,vty1):scope) ty2 (Just vtypeType)
|
||||
instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty
|
||||
tcRho scope (S t p) mb_ty = do
|
||||
env <- scopeEnv scope
|
||||
p_ty <- fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType)
|
||||
p_ty <- fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypePType
|
||||
res_ty <- case mb_ty of
|
||||
Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType)
|
||||
Nothing -> fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypeType
|
||||
Just ty -> return ty
|
||||
let t_ty = VTable p_ty res_ty
|
||||
(t,t_ty) <- tcRho scope t (Just t_ty)
|
||||
@@ -164,14 +164,14 @@ tcRho scope (S t p) mb_ty = do
|
||||
tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for tables
|
||||
env <- scopeEnv scope
|
||||
p_ty <- case tt of
|
||||
TRaw -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypePType)
|
||||
TRaw -> fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypePType
|
||||
TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType)
|
||||
liftEvalM (eval env ty [])
|
||||
eval env ty []
|
||||
(ps,mb_res_ty) <- tcCases scope ps p_ty Nothing
|
||||
res_ty <- case mb_res_ty of
|
||||
Just res_ty -> return res_ty
|
||||
Nothing -> fmap (\i -> VMeta i env []) $ liftEvalM (newEvaluatedThunk vtypeType)
|
||||
p_ty_t <- liftEvalM (value2term [] p_ty)
|
||||
Nothing -> fmap (\i -> VMeta i env []) $ newEvaluatedThunk vtypeType
|
||||
p_ty_t <- value2term [] p_ty
|
||||
return (T (TTyped p_ty_t) ps, VTable p_ty res_ty)
|
||||
tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
@@ -181,11 +181,11 @@ tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for t
|
||||
TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType)
|
||||
return ()--subsCheckRho ge scope -> Term ty res_ty
|
||||
(ps,Just res_ty) <- tcCases scope ps p_ty (Just res_ty)
|
||||
p_ty_t <- liftEvalM (value2term [] p_ty)
|
||||
p_ty_t <- value2term [] p_ty
|
||||
return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty)
|
||||
tcRho scope (R rs) Nothing = do
|
||||
lttys <- inferRecFields scope rs
|
||||
rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
|
||||
rs <- mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
|
||||
return (R rs,
|
||||
VRecType [(l, ty) | (l,t,ty) <- lttys]
|
||||
)
|
||||
@@ -193,12 +193,12 @@ tcRho scope (R rs) (Just ty) = do
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
case ty' of
|
||||
(VRecType ltys) -> do lttys <- checkRecFields scope rs ltys
|
||||
rs <- liftEvalM (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
|
||||
rs <- mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
|
||||
return ((f . R) rs,
|
||||
VRecType [(l, ty) | (l,t,ty) <- lttys]
|
||||
)
|
||||
ty -> do lttys <- inferRecFields scope rs
|
||||
t <- liftEvalM (liftM (f . R) (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys))
|
||||
t <- liftM (f . R) (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
|
||||
let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys]
|
||||
t <- subsCheckRho scope t ty' ty
|
||||
return (t, ty')
|
||||
@@ -206,7 +206,7 @@ tcRho scope (P t l) mb_ty = do
|
||||
l_ty <- case mb_ty of
|
||||
Just ty -> return ty
|
||||
Nothing -> do env <- scopeEnv scope
|
||||
i <- liftEvalM (newEvaluatedThunk vtypeType)
|
||||
i <- newEvaluatedThunk vtypeType
|
||||
return (VMeta i env [])
|
||||
(t,t_ty) <- tcRho scope t (Just (VRecType [(l,l_ty)]))
|
||||
return (P t l,l_ty)
|
||||
@@ -228,7 +228,7 @@ tcRho scope t@(ExtR t1 t2) mb_ty = do
|
||||
| otherwise = cType
|
||||
in instSigma scope (ExtR t1 t2) (VSort sort) mb_ty
|
||||
(VRecType rs1, VRecType rs2) -> instSigma scope (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty
|
||||
_ -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t)
|
||||
_ -> evalError ("Cannot type check" <+> ppTerm Unqualified 0 t)
|
||||
tcRho scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser
|
||||
tcRho scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
|
||||
tcRho scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser
|
||||
@@ -251,12 +251,12 @@ tcRho scope (EPattType ty) mb_ty = do
|
||||
tcRho scope t@(EPatt min max p) mb_ty = do
|
||||
(scope,f,ty) <- case mb_ty of
|
||||
Nothing -> do env <- scopeEnv scope
|
||||
i <- liftEvalM (newEvaluatedThunk vtypeType)
|
||||
i <- newEvaluatedThunk vtypeType
|
||||
return (scope,id,VMeta i env [])
|
||||
Just ty -> do (scope,f,ty) <- skolemise scope ty
|
||||
case ty of
|
||||
VPattType ty -> return (scope,f,ty)
|
||||
_ -> tcError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected")
|
||||
_ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected")
|
||||
tcPatt scope p ty
|
||||
return (f (EPatt min max p), ty)
|
||||
tcRho scope t _ = unimplemented ("tcRho "++show t)
|
||||
@@ -273,10 +273,10 @@ tcApp gr scope t@(App fun (ImplArg arg)) = do -- APP1
|
||||
do (bt, arg_ty, res_ty) <- unifyFun scope fun_ty
|
||||
if (bt == Implicit)
|
||||
then return ()
|
||||
else tcError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected")
|
||||
else evalError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected")
|
||||
(arg,_) <- tcRho scope arg (Just arg_ty)
|
||||
env <- scopeEnv scope
|
||||
varg <- liftEvalM (eval env arg [])
|
||||
varg <- eval env arg []
|
||||
return (App fun (ImplArg arg), res_ty)
|
||||
tcApp gr scope (App fun arg) = -- APP2
|
||||
tcApp gr scope fun `bindTcA` \(fun,fun_ty) ->
|
||||
@@ -284,24 +284,24 @@ tcApp gr scope (App fun arg) = -- APP2
|
||||
(_, arg_ty, res_ty) <- unifyFun scope fun_ty
|
||||
(arg,_) <- tcRho scope arg (Just arg_ty)
|
||||
env <- scopeEnv scope
|
||||
varg <- liftEvalM (eval env arg [])
|
||||
varg <- eval env arg []
|
||||
return (App fun arg, res_ty)
|
||||
tcApp gr scope (Q id) = do -- VAR (global)
|
||||
mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) ->
|
||||
do ty <- liftEvalM (eval [] ty [])
|
||||
do ty <- eval [] ty []
|
||||
return (t,ty)
|
||||
tcApp gr scope (QC id) = -- VAR (global)
|
||||
mkTcA (lookupOverloadTypes gr id) `bindTcA` \(t,ty) ->
|
||||
do ty <- liftEvalM (eval [] ty [])
|
||||
do ty <- eval [] ty []
|
||||
return (t,ty)
|
||||
tcApp gr scope t =
|
||||
singleTcA (tcRho scope t Nothing)
|
||||
|
||||
|
||||
tcOverloadFailed t ttys =
|
||||
tcError ("Overload resolution failed" $$
|
||||
"of term " <+> pp t $$
|
||||
"with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys])
|
||||
evalError ("Overload resolution failed" $$
|
||||
"of term " <+> pp t $$
|
||||
"with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys])
|
||||
|
||||
|
||||
tcPatt scope PW ty0 =
|
||||
@@ -309,12 +309,12 @@ tcPatt scope PW ty0 =
|
||||
tcPatt scope (PV x) ty0 =
|
||||
return ((x,ty0):scope)
|
||||
tcPatt scope (PP c ps) ty0 = do
|
||||
ty <- liftEvalM (getResType c)
|
||||
ty <- getResType c
|
||||
let go scope ty [] = return (scope,ty)
|
||||
go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun scope ty
|
||||
scope <- tcPatt scope p arg_ty
|
||||
go scope res_ty ps
|
||||
vty <- liftEvalM (eval [] ty [])
|
||||
vty <- eval [] ty []
|
||||
(scope,ty) <- go scope vty ps
|
||||
unify scope ty0 ty
|
||||
return scope
|
||||
@@ -337,7 +337,7 @@ tcPatt scope (PAs x p) ty0 = do
|
||||
tcPatt ((x,ty0):scope) p ty0
|
||||
tcPatt scope (PR rs) ty0 = do
|
||||
let mk_ltys [] = return []
|
||||
mk_ltys ((l,p):rs) = do i <- liftEvalM (newEvaluatedThunk vtypePType)
|
||||
mk_ltys ((l,p):rs) = do i <- newEvaluatedThunk vtypePType
|
||||
ltys <- mk_ltys rs
|
||||
env <- scopeEnv scope
|
||||
return ((l,p,VMeta i env []) : ltys)
|
||||
@@ -352,13 +352,13 @@ tcPatt scope (PAlt p1 p2) ty0 = do
|
||||
tcPatt scope p2 ty0
|
||||
return scope
|
||||
tcPatt scope (PM q) ty0 = do
|
||||
ty <- liftEvalM (getResType q)
|
||||
ty <- getResType q
|
||||
case ty of
|
||||
EPattType ty
|
||||
-> do vty <- liftEvalM (eval [] ty [])
|
||||
-> do vty <- eval [] ty []
|
||||
unify scope ty0 vty
|
||||
return scope
|
||||
ty -> tcError ("Pattern type expected but " <+> pp ty <+> " found.")
|
||||
ty -> evalError ("Pattern type expected but " <+> pp ty <+> " found.")
|
||||
tcPatt scope p ty = unimplemented ("tcPatt "++show p)
|
||||
|
||||
inferRecFields scope rs =
|
||||
@@ -366,13 +366,13 @@ inferRecFields scope rs =
|
||||
|
||||
checkRecFields scope [] ltys
|
||||
| null ltys = return []
|
||||
| otherwise = tcError ("Missing fields:" <+> hsep (map fst ltys))
|
||||
| otherwise = evalError ("Missing fields:" <+> hsep (map fst ltys))
|
||||
checkRecFields scope ((l,t):lts) ltys =
|
||||
case takeIt l ltys of
|
||||
(Just ty,ltys) -> do ltty <- tcRecField scope l t (Just ty)
|
||||
lttys <- checkRecFields scope lts ltys
|
||||
return (ltty : lttys)
|
||||
(Nothing,ltys) -> do tcWarn ("Discarded field:" <+> l)
|
||||
(Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l)
|
||||
ltty <- tcRecField scope l t Nothing
|
||||
lttys <- checkRecFields scope lts ltys
|
||||
return lttys -- ignore the field
|
||||
@@ -387,7 +387,7 @@ tcRecField scope l (mb_ann_ty,t) mb_ty = do
|
||||
(t,ty) <- case mb_ann_ty of
|
||||
Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
|
||||
env <- scopeEnv scope
|
||||
v_ann_ty <- liftEvalM (eval env ann_ty [])
|
||||
v_ann_ty <- eval env ann_ty []
|
||||
(t,_) <- tcRho scope t (Just v_ann_ty)
|
||||
instSigma scope t v_ann_ty mb_ty
|
||||
Nothing -> tcRho scope t mb_ty
|
||||
@@ -401,35 +401,35 @@ tcRecTypeFields scope ((l,ty):rs) mb_ty = do
|
||||
| s == cType -> return (Just sort)
|
||||
| s == cPType -> return mb_ty
|
||||
VMeta _ _ _ -> return mb_ty
|
||||
_ -> do sort <- zonkTerm =<< liftEvalM (value2term (scopeVars scope) sort)
|
||||
tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
|
||||
"cannot be of type" <+> ppTerm Unqualified 0 sort)
|
||||
_ -> do sort <- zonkTerm =<< value2term (scopeVars scope) sort
|
||||
evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
|
||||
"cannot be of type" <+> ppTerm Unqualified 0 sort)
|
||||
(rs,mb_ty) <- tcRecTypeFields scope rs mb_ty
|
||||
return ((l,ty):rs,mb_ty)
|
||||
|
||||
-- | Invariant: if the third argument is (Just rho),
|
||||
-- then rho is in weak-prenex form
|
||||
instSigma :: Scope s -> Term -> Sigma s -> Maybe (Rho s) -> TcM s (Term, Rho s)
|
||||
instSigma :: Scope s -> Term -> Sigma s -> Maybe (Rho s) -> EvalM s (Term, Rho s)
|
||||
instSigma scope t ty1 Nothing = return (t,ty1) -- INST1
|
||||
instSigma scope t ty1 (Just ty2) = do -- INST2
|
||||
t <- subsCheckRho scope t ty1 ty2
|
||||
return (t,ty2)
|
||||
|
||||
-- | Invariant: the second argument is in weak-prenex form
|
||||
subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> TcM s Term
|
||||
subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> EvalM s Term
|
||||
subsCheckRho scope t ty1@(VMeta i env vs) ty2 = do
|
||||
mv <- liftEvalM (getRef i)
|
||||
mv <- getRef i
|
||||
case mv of
|
||||
Residuation _ _ _ -> do unify scope ty1 ty2
|
||||
return t
|
||||
Evaluated _ vty1 -> do vty1 <- liftEvalM (apply vty1 vs)
|
||||
Evaluated _ vty1 -> do vty1 <- apply vty1 vs
|
||||
subsCheckRho scope t vty1 ty2
|
||||
subsCheckRho scope t ty1 ty2@(VMeta i env vs) = do
|
||||
mv <- liftEvalM (getRef i)
|
||||
mv <- getRef i
|
||||
case mv of
|
||||
Residuation _ _ _ -> do unify scope ty1 ty2
|
||||
return t
|
||||
Evaluated _ vty2 -> do vty2 <- liftEvalM (apply vty2 vs)
|
||||
Evaluated _ vty2 -> do vty2 <- apply vty2 vs
|
||||
subsCheckRho scope t ty1 vty2
|
||||
{-subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do -- Rule SPEC
|
||||
i <- newMeta scope ty1
|
||||
@@ -458,7 +458,7 @@ subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j]) -- Rule
|
||||
| predefName p1 == cInts && predefName p2 == cInts =
|
||||
if i <= j
|
||||
then return t
|
||||
else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
|
||||
else evalError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
|
||||
subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
|
||||
let mkAccess scope t =
|
||||
case t of
|
||||
@@ -494,15 +494,15 @@ subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule
|
||||
let fields = [(l,ty2,lookup l rs1) | (l,ty2) <- rs2]
|
||||
case [l | (l,_,Nothing) <- fields] of
|
||||
[] -> return ()
|
||||
missing -> tcError ("In the term" <+> pp t $$
|
||||
"there are no values for fields:" <+> hsep missing)
|
||||
missing -> evalError ("In the term" <+> pp t $$
|
||||
"there are no values for fields:" <+> hsep missing)
|
||||
rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]]
|
||||
return (mkWrap (R rs))
|
||||
subsCheckRho ge scope t tau1 tau2 = do -- Rule EQ
|
||||
unify ge scope tau1 tau2 -- Revert to ordinary unification
|
||||
return t
|
||||
|
||||
subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> Rho) -> TcM Term
|
||||
subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> Rho) -> EvalM Term
|
||||
subsCheckFun ge scope t a1 r1 a2 r2 = do
|
||||
let v = newVar scope
|
||||
vt <- subsCheckRho ge ((v,a2):scope) (Vr v) a2 a1
|
||||
@@ -511,7 +511,7 @@ subsCheckFun ge scope t a1 r1 a2 r2 = do
|
||||
t <- subsCheckRho ge ((v,vtypeType):scope) (App t vt) (r1 val1) (r2 val2)
|
||||
return (Abs Explicit v t)
|
||||
|
||||
subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
|
||||
subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term
|
||||
subsCheckTbl ge scope t p1 r1 p2 r2 = do
|
||||
let x = newVar scope
|
||||
xt <- subsCheckRho ge scope (Vr x) p2 p1
|
||||
@@ -523,25 +523,25 @@ subsCheckTbl ge scope t p1 r1 p2 r2 = do
|
||||
-- Unification
|
||||
-----------------------------------------------------------------------
|
||||
|
||||
unifyFun :: Scope s -> Rho s -> TcM s (BindType, Sigma s, Rho s)
|
||||
unifyFun :: Scope s -> Rho s -> EvalM s (BindType, Sigma s, Rho s)
|
||||
unifyFun scope (VProd bt x arg res) =
|
||||
return (bt,arg,res)
|
||||
unifyFun scope tau = do
|
||||
let mk_val ty = VMeta ty [] []
|
||||
arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType)
|
||||
res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType)
|
||||
arg <- fmap mk_val $ newEvaluatedThunk vtypeType
|
||||
res <- fmap mk_val $ newEvaluatedThunk vtypeType
|
||||
let bt = Explicit
|
||||
unify scope tau (VProd bt identW arg res)
|
||||
return (bt,arg,res)
|
||||
|
||||
unifyTbl :: Scope s -> Rho s -> TcM s (Sigma s, Rho s)
|
||||
unifyTbl :: Scope s -> Rho s -> EvalM s (Sigma s, Rho s)
|
||||
unifyTbl scope (VTable arg res) =
|
||||
return (arg,res)
|
||||
unifyTbl scope tau = do
|
||||
env <- scopeEnv scope
|
||||
let mk_val ty = VMeta ty env []
|
||||
arg <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypePType)
|
||||
res <- liftEvalM (fmap mk_val $ newEvaluatedThunk vtypeType)
|
||||
arg <- fmap mk_val $ newEvaluatedThunk vtypePType
|
||||
res <- fmap mk_val $ newEvaluatedThunk vtypeType
|
||||
unify scope tau (VTable arg res)
|
||||
return (arg,res)
|
||||
|
||||
@@ -570,29 +570,29 @@ unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v
|
||||
unify ge scope v1 v2 = do
|
||||
t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
|
||||
t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
|
||||
tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
|
||||
ppTerm Unqualified 0 t2))
|
||||
evalError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
|
||||
ppTerm Unqualified 0 t2))
|
||||
-}
|
||||
-- | Invariant: tv1 is a flexible type variable
|
||||
unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> TcM s ()
|
||||
unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> EvalM s ()
|
||||
unifyVar scope tnk env vs ty2 = do -- Check whether i is bound
|
||||
mv <- liftEvalM (getRef tnk)
|
||||
mv <- getRef tnk
|
||||
case mv of
|
||||
Unevaluated _ ty1 -> do v <- liftEvalM (eval env ty1 [] >>= \v -> apply v vs)
|
||||
Unevaluated _ ty1 -> do v <- eval env ty1 [] >>= \v -> apply v vs
|
||||
unify scope v ty2
|
||||
Residuation i scope' _ -> do ty2' <- liftEvalM (value2term (scopeVars scope') ty2)
|
||||
Residuation i scope' _ -> do ty2' <- value2term (scopeVars scope') ty2
|
||||
ms2 <- getMetaVars [(scope,ty2)]
|
||||
if i `elem` ms2
|
||||
then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
|
||||
nest 2 (ppTerm Unqualified 0 ty2'))
|
||||
else liftEvalM (setRef tnk (Unevaluated env ty2'))
|
||||
then evalError ("Occurs check for" <+> ppMeta i <+> "in:" $$
|
||||
nest 2 (ppTerm Unqualified 0 ty2'))
|
||||
else setRef tnk (Unevaluated env ty2')
|
||||
|
||||
-----------------------------------------------------------------------
|
||||
-- Instantiation and quantification
|
||||
-----------------------------------------------------------------------
|
||||
|
||||
-- | Instantiate the topmost implicit arguments with metavariables
|
||||
instantiate :: Scope s -> Term -> Sigma s -> TcM s (Term,Rho s)
|
||||
instantiate :: Scope s -> Term -> Sigma s -> EvalM s (Term,Rho s)
|
||||
instantiate scope t (VProd Implicit x ty1 ty2) = undefined {- do
|
||||
i <- newMeta scope ty1
|
||||
instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) -}
|
||||
@@ -600,12 +600,12 @@ instantiate scope t ty = do
|
||||
return (t,ty)
|
||||
|
||||
-- | Build fresh lambda abstractions for the topmost implicit arguments
|
||||
skolemise :: Scope s -> Sigma s -> TcM s (Scope s, Term->Term, Rho s)
|
||||
skolemise :: Scope s -> Sigma s -> EvalM s (Scope s, Term->Term, Rho s)
|
||||
skolemise scope ty@(VMeta i env vs) = undefined {-do
|
||||
mv <- getRef i
|
||||
case mv of
|
||||
Residuation _ _ _ -> return (scope,id,ty) -- guarded constant?
|
||||
Evaluated _ vty -> do vty <- liftEvalM (apply vty vs)
|
||||
Evaluated _ vty -> do vty <- apply vty vs
|
||||
skolemise scope vty
|
||||
skolemise scope (VProd Implicit ty1 x ty2) = do
|
||||
let v = newVar scope
|
||||
@@ -615,7 +615,7 @@ skolemise scope ty = do
|
||||
return (scope,undefined,ty)-}
|
||||
|
||||
-- | Quantify over the specified type variables (all flexible)
|
||||
quantify :: Scope s -> Term -> [MetaId] -> Rho s -> TcM s (Term,Sigma s)
|
||||
quantify :: Scope s -> Term -> [MetaId] -> Rho s -> EvalM s (Term,Sigma s)
|
||||
quantify scope t tvs ty0 = undefined {- do
|
||||
ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
|
||||
let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
|
||||
@@ -636,77 +636,15 @@ allBinders = [ identS [x] | x <- ['a'..'z'] ] ++
|
||||
|
||||
|
||||
-----------------------------------------------------------------------
|
||||
-- The Monad
|
||||
-- Helpers
|
||||
-----------------------------------------------------------------------
|
||||
|
||||
type Sigma s = Value s
|
||||
type Rho s = Value s -- No top-level ForAll
|
||||
type Tau s = Value s -- No ForAlls anywhere
|
||||
|
||||
data TcResult s a
|
||||
= TcOk a (MetaThunks s) [Message]
|
||||
| TcFail [Message] -- First msg is error, the rest are warnings?
|
||||
newtype TcM s a = TcM {unTcM :: Grammar -> MetaThunks s -> [Message] -> ST s (TcResult s a)}
|
||||
|
||||
instance Monad (TcM s) where
|
||||
return x = TcM (\gr ms msgs -> return (TcOk x ms msgs))
|
||||
f >>= g = TcM $ \gr ms msgs -> do
|
||||
res <- unTcM f gr ms msgs
|
||||
case res of
|
||||
TcOk x ms msgs -> unTcM (g x) gr ms msgs
|
||||
TcFail msgs -> return (TcFail msgs)
|
||||
|
||||
#if !(MIN_VERSION_base(4,13,0))
|
||||
-- Monad(fail) will be removed in GHC 8.8+
|
||||
fail = Fail.fail
|
||||
#endif
|
||||
|
||||
instance Fail.MonadFail (TcM s) where
|
||||
fail = tcError . pp
|
||||
|
||||
|
||||
instance Applicative (TcM s) where
|
||||
pure = return
|
||||
(<*>) = ap
|
||||
|
||||
instance Functor (TcM s) where
|
||||
fmap f g = TcM $ \gr ms msgs -> do
|
||||
res <- unTcM g gr ms msgs
|
||||
case res of
|
||||
TcOk x ms msgs -> return (TcOk (f x) ms msgs)
|
||||
TcFail msgs -> return (TcFail msgs)
|
||||
|
||||
instance ErrorMonad (TcM s) where
|
||||
raise = tcError . pp
|
||||
handle f g = TcM $ \gr ms msgs -> do
|
||||
res <- unTcM f gr ms msgs
|
||||
case res of
|
||||
TcFail (msg:msgs) -> unTcM (g (render msg)) gr ms msgs
|
||||
r -> return r
|
||||
|
||||
tcError :: Message -> TcM s a
|
||||
tcError msg = TcM (\gr ms msgs -> return (TcFail (msg : msgs)))
|
||||
|
||||
tcWarn :: Message -> TcM s ()
|
||||
tcWarn msg = TcM (\gr ms msgs -> return (TcOk () ms (msg : msgs)))
|
||||
|
||||
unimplemented str = fail ("Unimplemented: "++str)
|
||||
|
||||
|
||||
runTcM :: Grammar -> (forall s . TcM s a) -> Check a
|
||||
runTcM gr f = Check $ \(errs,wngs) -> runST $ do
|
||||
res <- unTcM f gr Map.empty []
|
||||
case res of
|
||||
TcOk x _ msgs -> return ((errs, wngs++msgs),Success x)
|
||||
TcFail (msg:msgs) -> return ((errs, wngs++msgs),Fail msg)
|
||||
|
||||
liftEvalM :: EvalM s a -> TcM s a
|
||||
liftEvalM (EvalM f) = TcM $ \gr ms msgs -> do
|
||||
res <- f gr (\x ms b r -> return (Success (x,ms))) ms maxBound undefined
|
||||
case res of
|
||||
Success (x,ms) -> return (TcOk x ms [])
|
||||
Fail msg -> return (TcFail [msg])
|
||||
|
||||
newVar :: Scope s -> Ident
|
||||
newVar scope = head [x | i <- [1..],
|
||||
let x = identS ('v':show i),
|
||||
@@ -715,15 +653,15 @@ newVar scope = head [x | i <- [1..],
|
||||
isFree [] x = True
|
||||
isFree ((y,_):scope) x = x /= y && isFree scope x
|
||||
|
||||
scopeEnv scope = zipWithM (\(x,ty) i -> liftEvalM (newEvaluatedThunk (VGen i [])) >>= \tnk -> return (x,tnk)) (reverse scope) [0..]
|
||||
scopeEnv scope = zipWithM (\(x,ty) i -> newEvaluatedThunk (VGen i []) >>= \tnk -> return (x,tnk)) (reverse scope) [0..]
|
||||
scopeVars scope = map fst scope
|
||||
scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope)
|
||||
|
||||
-- | This function takes account of zonking, and returns a set
|
||||
-- (no duplicates) of unbound meta-type variables
|
||||
getMetaVars :: [(Scope s,Sigma s)] -> TcM s [MetaId]
|
||||
getMetaVars :: [(Scope s,Sigma s)] -> EvalM s [MetaId]
|
||||
getMetaVars sc_tys = do
|
||||
tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys
|
||||
tys <- mapM (\(scope,ty) -> zonkTerm =<< value2term (scopeVars scope) ty) sc_tys
|
||||
return (foldr go [] tys)
|
||||
where
|
||||
-- Get the MetaIds from a term; no duplicates in result
|
||||
@@ -742,9 +680,9 @@ getMetaVars sc_tys = do
|
||||
|
||||
-- | This function takes account of zonking, and returns a set
|
||||
-- (no duplicates) of free type variables
|
||||
getFreeVars :: [(Scope s,Sigma s)] -> TcM s [Ident]
|
||||
getFreeVars :: [(Scope s,Sigma s)] -> EvalM s [Ident]
|
||||
getFreeVars sc_tys = do
|
||||
tys <- mapM (\(scope,ty) -> zonkTerm =<< liftEvalM (value2term (scopeVars scope) ty)) sc_tys
|
||||
tys <- mapM (\(scope,ty) -> zonkTerm =<< value2term (scopeVars scope) ty) sc_tys
|
||||
return (foldr (go []) [] tys)
|
||||
where
|
||||
go bound (Vr tv) acc
|
||||
@@ -760,7 +698,7 @@ getFreeVars sc_tys = do
|
||||
go bound (Table p t) acc = go bound p (go bound t acc)
|
||||
|
||||
-- | Eliminate any substitutions in a term
|
||||
zonkTerm :: Term -> TcM s Term
|
||||
zonkTerm :: Term -> EvalM s Term
|
||||
zonkTerm (Meta i) = undefined {- do
|
||||
mv <- getMeta i
|
||||
case mv of
|
||||
@@ -773,34 +711,34 @@ zonkTerm t = composOp zonkTerm t
|
||||
-}
|
||||
|
||||
data TcA s x a
|
||||
= TcSingle (Grammar -> MetaThunks s -> [Message] -> ST s (TcResult s a))
|
||||
= TcSingle (Grammar -> MetaThunks s -> [Message] -> ST s (CheckResult s a))
|
||||
| TcMany [x] (Grammar -> MetaThunks s -> [Message] -> ST s [(a,MetaThunks s,[Message])])
|
||||
|
||||
mkTcA :: Err [a] -> TcA s a a
|
||||
mkTcA f = case f of
|
||||
mkTcA f = undefined {- case f of
|
||||
Bad msg -> TcSingle (\gr ms msgs -> return (TcFail (pp msg : msgs)))
|
||||
Ok [x] -> TcSingle (\gr ms msgs -> return (TcOk x ms msgs))
|
||||
Ok xs -> TcMany xs (\gr ms msgs -> return [(x,ms,msgs) | x <- xs])
|
||||
-}
|
||||
singleTcA :: EvalM s a -> TcA s x a
|
||||
singleTcA = undefined {- TcSingle . unTcM -}
|
||||
|
||||
singleTcA :: TcM s a -> TcA s x a
|
||||
singleTcA = TcSingle . unTcM
|
||||
|
||||
bindTcA :: TcA s x a -> (a -> TcM s b) -> TcA s x b
|
||||
bindTcA f g = case f of
|
||||
TcSingle f -> TcSingle (unTcM (TcM f >>= g))
|
||||
bindTcA :: TcA s x a -> (a -> EvalM s b) -> TcA s x b
|
||||
bindTcA f g = undefined {- case f of
|
||||
TcSingle f -> TcSingle (unTcM (EvalM f >>= g))
|
||||
TcMany xs f -> TcMany xs (\gr ms msgs -> f gr ms msgs >>= foldM (add gr) [])
|
||||
where
|
||||
add gr rs (y,ms,msgs) = do
|
||||
res <- unTcM (g y) gr ms msgs
|
||||
case res of
|
||||
TcFail _ -> return rs
|
||||
TcOk y ms msgs -> return ((y,ms,msgs):rs)
|
||||
|
||||
runTcA :: ([x] -> TcM s a) -> (SourceGrammar -> TcA s x a) -> TcM s a
|
||||
runTcA g f = TcM (\gr ms msgs -> case f gr of
|
||||
TcMany xs f -> do rs <- f gr ms msgs
|
||||
case rs of
|
||||
[(x,ms,msgs)] -> return (TcOk x ms msgs)
|
||||
rs -> unTcM (g xs) gr ms msgs
|
||||
TcSingle f -> f gr ms msgs)
|
||||
|
||||
Fail _ _ -> return rs
|
||||
Success y msgs -> return ((y,ms,msgs):rs)
|
||||
-}
|
||||
runTcA :: ([x] -> EvalM s a) -> (SourceGrammar -> TcA s x a) -> EvalM s a
|
||||
runTcA g f = undefined {- EvalM (\gr ms msgs -> case f gr of
|
||||
TcMany xs f -> do rs <- f gr ms msgs
|
||||
case rs of
|
||||
[(x,ms,msgs)] -> return (Success x msgs)
|
||||
rs -> unTcM (g xs) gr ms msgs
|
||||
TcSingle f -> f gr ms msgs)
|
||||
-}
|
||||
|
||||
@@ -37,22 +37,19 @@ import qualified Control.Monad.Fail as Fail
|
||||
type Message = Doc
|
||||
type Error = Message
|
||||
type Warning = Message
|
||||
--data Severity = Warning | Error
|
||||
--type NonFatal = ([Severity,Message]) -- preserves order
|
||||
type NonFatal = ([Error],[Warning])
|
||||
type Accumulate acc ans = acc -> (acc,ans)
|
||||
data CheckResult a = Fail Error | Success a
|
||||
data CheckResult a b = Fail Error b | Success a b
|
||||
newtype Check a
|
||||
= Check {unCheck :: {-Context ->-} Accumulate NonFatal (CheckResult a)}
|
||||
= Check {unCheck :: NonFatal -> CheckResult a NonFatal}
|
||||
|
||||
instance Functor Check where fmap = liftM
|
||||
|
||||
instance Monad Check where
|
||||
return x = Check $ \{-ctxt-} ws -> (ws,Success x)
|
||||
f >>= g = Check $ \{-ctxt-} ws ->
|
||||
case unCheck f {-ctxt-} ws of
|
||||
(ws,Success x) -> unCheck (g x) {-ctxt-} ws
|
||||
(ws,Fail msg) -> (ws,Fail msg)
|
||||
return x = Check $ \msgs -> Success x msgs
|
||||
f >>= g = Check $ \ws ->
|
||||
case unCheck f ws of
|
||||
Success x msgs -> unCheck (g x) msgs
|
||||
Fail msg msgs -> Fail msg msgs
|
||||
|
||||
instance Fail.MonadFail Check where
|
||||
fail = raise
|
||||
@@ -65,26 +62,26 @@ instance ErrorMonad Check where
|
||||
raise s = checkError (pp s)
|
||||
handle f h = handle' f (h . render)
|
||||
|
||||
handle' f h = Check (\{-ctxt-} msgs -> case unCheck f {-ctxt-} msgs of
|
||||
(ws,Success x) -> (ws,Success x)
|
||||
(ws,Fail msg) -> unCheck (h msg) {-ctxt-} ws)
|
||||
handle' f h = Check (\msgs -> case unCheck f {-ctxt-} msgs of
|
||||
Success x msgs -> Success x msgs
|
||||
Fail msg msgs -> unCheck (h msg) msgs)
|
||||
|
||||
-- | Report a fatal error
|
||||
checkError :: Message -> Check a
|
||||
checkError msg = Check (\{-ctxt-} ws -> (ws,Fail msg))
|
||||
checkError msg = Check (\msgs -> Fail msg msgs)
|
||||
|
||||
checkCond :: Message -> Bool -> Check ()
|
||||
checkCond s b = if b then return () else checkError s
|
||||
|
||||
-- | warnings should be reversed in the end
|
||||
checkWarn :: Message -> Check ()
|
||||
checkWarn msg = Check $ \{-ctxt-} (es,ws) -> ((es,("Warning:" <+> msg) : ws),Success ())
|
||||
checkWarn msg = Check $ \(es,ws) -> Success () (es,("Warning:" <+> msg) : ws)
|
||||
|
||||
checkWarnings ms = mapM_ checkWarn ms
|
||||
|
||||
-- | Report a nonfatal (accumulated) error
|
||||
checkAccumError :: Message -> Check ()
|
||||
checkAccumError msg = Check $ \{-ctxt-} (es,ws) -> ((msg:es,ws),Success ())
|
||||
checkAccumError msg = Check $ \(es,ws) -> Success () (msg:es,ws)
|
||||
|
||||
-- | Turn a fatal error into a nonfatal (accumulated) error
|
||||
accumulateError :: (a -> Check a) -> a -> Check a
|
||||
@@ -94,13 +91,13 @@ accumulateError chk a =
|
||||
-- | Turn accumulated errors into a fatal error
|
||||
commitCheck :: Check a -> Check a
|
||||
commitCheck c =
|
||||
Check $ \ {-ctxt-} msgs0@(es0,ws0) ->
|
||||
case unCheck c {-ctxt-} ([],[]) of
|
||||
(([],ws),Success v) -> ((es0,ws++ws0),Success v)
|
||||
(msgs ,Success _) -> bad msgs0 msgs
|
||||
((es,ws),Fail e) -> bad msgs0 ((e:es),ws)
|
||||
Check $ \msgs0@(es0,ws0) ->
|
||||
case unCheck c ([],[]) of
|
||||
(Success v ([],ws)) -> Success v (es0,ws++ws0)
|
||||
(Success _ msgs) -> bad msgs0 msgs
|
||||
(Fail e (es,ws)) -> bad msgs0 ((e:es),ws)
|
||||
where
|
||||
bad (es0,ws0) (es,ws) = ((es0,ws++ws0),Fail (list es))
|
||||
bad (es0,ws0) (es,ws) = (Fail (list es) (es0,ws++ws0))
|
||||
list = vcat . reverse
|
||||
|
||||
-- | Run an error check, report errors and warnings
|
||||
@@ -109,10 +106,10 @@ runCheck c = runCheck' noOptions c
|
||||
-- | Run an error check, report errors and (optionally) warnings
|
||||
runCheck' :: ErrorMonad m => Options -> Check a -> m (a,String)
|
||||
runCheck' opts c =
|
||||
case unCheck c {-[]-} ([],[]) of
|
||||
(([],ws),Success v) -> return (v,render (wlist ws))
|
||||
(msgs ,Success v) -> bad msgs
|
||||
((es,ws),Fail e) -> bad ((e:es),ws)
|
||||
case unCheck c ([],[]) of
|
||||
Success v ([],ws) -> return (v,render (wlist ws))
|
||||
Success v msgs -> bad msgs
|
||||
Fail e (es,ws) -> bad ((e:es),ws)
|
||||
where
|
||||
bad (es,ws) = raise (render $ wlist ws $$ list es)
|
||||
list = vcat . reverse
|
||||
@@ -128,12 +125,13 @@ checkMapRecover f = fmap Map.fromList . mapM f' . Map.toList
|
||||
where f' (k,v) = fmap ((,)k) (f k v)
|
||||
|
||||
checkIn :: Doc -> Check a -> Check a
|
||||
checkIn msg c = Check $ \{-ctxt-} msgs0 ->
|
||||
case unCheck c {-ctxt-} ([],[]) of
|
||||
(msgs,Fail msg) -> (augment msgs0 msgs,Fail (augment1 msg))
|
||||
(msgs,Success v) -> (augment msgs0 msgs,Success v)
|
||||
checkIn msg c = Check $ \msgs0 ->
|
||||
case unCheck c ([],[]) of
|
||||
Fail msg msgs -> Fail (augment1 msg) (augment msgs0 msgs)
|
||||
Success v msgs -> Success v (augment msgs0 msgs)
|
||||
where
|
||||
augment (es0,ws0) (es,ws) = (augment' es0 es,augment' ws0 ws)
|
||||
|
||||
augment' msgs0 [] = msgs0
|
||||
augment' msgs0 msgs' = (msg $$ nest 3 (vcat (reverse msgs'))):msgs0
|
||||
|
||||
|
||||
Reference in New Issue
Block a user