GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-21 00:52:51 -06:00
Code Issues Packages Projects Releases Wiki Activity

syntax for implicit arguments in GF

Browse Source
This commit is contained in:
krasimir
2009-09-20 13:47:08 +00:00
parent a29a8e4f60
commit 96786c1136
20 changed files with 309 additions and 339 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
src/GF/Compile/AbsCompute.hs
View File

@@ -53,7 +53,7 @@ computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unquali
_ -> do
let t' = beta vv t
(yy,f,aa) <- termForm t'
let vv' = yy ++ vv
let vv' = map snd yy ++ vv
aa' <- mapM (compt vv') aa
case look f of
Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 f) $
@@ -84,10 +84,10 @@ beta vv c = case c of
App f a ->
let (a',f') = (beta vv a, beta vv f) in
case f' of
Abs x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b)
Abs _ x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b)
_ -> (if a'==a && f'==f then id else beta vv) $ App f' a'
Prod x a b -> Prod x (beta vv a) (beta (x:vv) b)
Abs x b -> Abs x (beta (x:vv) b)
Prod b x a t -> Prod b x (beta vv a) (beta (x:vv) t)
Abs b x t -> Abs b x (beta (x:vv) t)
_ -> c
-- special version of pattern matching, to deal with comp under lambda
@@ -133,7 +133,7 @@ tryMatch (p,t) = do
notMeta e = case e of
Meta _ -> False
App f a -> notMeta f && notMeta a
Abs _ b -> notMeta b
Abs _ _ b -> notMeta b
_ -> True
prtm p g =

84
src/GF/Compile/CheckGrammar.hs
View File

@@ -134,11 +134,11 @@ checkAbsInfo st m mo c info = do
Let (x,(_,a)) b -> do
a' <- compAbsTyp g a
compAbsTyp ((x, a'):g) b
Prod x a b -> do
Prod b x a t -> do
a' <- compAbsTyp g a
b' <- compAbsTyp ((x,Vr x):g) b
return $ Prod x a' b'
Abs _ _ -> return t
t' <- compAbsTyp ((x,Vr x):g) t
return $ Prod b x a' t'
Abs _ _ _ -> return t
_ -> composOp (compAbsTyp g) t
checkCompleteGrammar :: SourceGrammar -> SourceModInfo -> SourceModInfo -> Check (BinTree Ident Info)
@@ -170,7 +170,7 @@ checkCompleteGrammar gr abs cnc = do
return info
_ -> return info
case info of
CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs identW) (R []) cxt)
CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt)
_ -> Bad "no def lin"
case lookupIdent c js of
Ok (CncFun _ (Just _) _ ) -> return js
@@ -224,7 +224,7 @@ checkResInfo gr mo mm c info = do
--- this can only be a partial guarantee, since matching
--- with value type is only possible if expected type is given
checkUniq $
sort [t : map snd xs | (_,x) <- tysts1, Ok (xs,t) <- [typeFormCnc x]]
sort [t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1, Ok (xs,t) <- [typeFormCnc x]]
return (ResOverload os [(y,x) | (x,y) <- tysts'])
ResParam (Just (pcs,_)) -> chIn "parameter type" $ do
@@ -257,7 +257,7 @@ checkCncInfo gr m mo (a,abs) c info = do
typ <- checkErr $ lookupFunType gr a c
cat0 <- checkErr $ valCat typ
(cont,val) <- linTypeOfType gr m typ -- creates arg vars
(trm',_) <- check trm (mkFunType (map snd cont) val) -- erases arg vars
(trm',_) <- check trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
checkPrintname gr mpr
cat <- return $ snd cat0
return (CncFun (Just (cat,(cont,val))) (Just trm') mpr)
@@ -286,7 +286,7 @@ checkCncInfo gr m mo (a,abs) c info = do
computeLType :: SourceGrammar -> Type -> Check Type
computeLType gr t = do
g0 <- checkGetContext
let g = [(x, Vr x) | (x,_) <- g0]
let g = [(b,x, Vr x) | (b,x,_) <- g0]
checkInContext g $ comp t
where
comp ty = case ty of
@@ -303,17 +303,17 @@ computeLType gr t = do
f' <- comp f
a' <- comp a
case f' of
Abs x b -> checkInContext [(x,a')] $ comp b
Abs b x t -> checkInContext [(b,x,a')] $ comp t
_ -> return $ App f' a'
Prod x a b -> do
Prod bt x a b -> do
a' <- comp a
b' <- checkInContext [(x,Vr x)] $ comp b
return $ Prod x a' b'
b' <- checkInContext [(bt,x,Vr x)] $ comp b
return $ Prod bt x a' b'
Abs x b -> do
b' <- checkInContext [(x,Vr x)] $ comp b
return $ Abs x b'
Abs bt x b -> do
b' <- checkInContext [(bt,x,Vr x)] $ comp b
return $ Abs bt x b'
ExtR r s -> do
r' <- comp r
@@ -387,11 +387,11 @@ inferLType gr trm = case trm of
(f',fty) <- infer f
fty' <- comp fty
case fty' of
Prod z arg val -> do
Prod bt z arg val -> do
a' <- justCheck a arg
ty <- if isWildIdent z
then return val
else substituteLType [(z,a')] val
else substituteLType [(bt,z,a')] val
return (App f' a',ty)
_ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType env fty)
@@ -502,10 +502,10 @@ inferLType gr trm = case trm of
Sort _ ->
termWith trm $ return typeType
Prod x a b -> do
Prod bt x a b -> do
a' <- justCheck a typeType
b' <- checkInContext [(x,a')] $ justCheck b typeType
return (Prod x a' b', typeType)
b' <- checkInContext [(bt,x,a')] $ justCheck b typeType
return (Prod bt x a' b', typeType)
Table p t -> do
p' <- justCheck p typeType --- check p partype!
@@ -655,7 +655,7 @@ getOverload env@gr mt ot = case appForm ot of
noProds vfs = [(v,f) | (v,f) <- vfs, noProd v]
noProd ty = case ty of
Prod _ _ _ -> False
Prod _ _ _ _ -> False
_ -> True
checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
@@ -665,17 +665,17 @@ checkLType env trm typ0 = do
case trm of
Abs x c -> do
Abs bt x c -> do
case typ of
Prod z a b -> do
checkUpdate (x,a)
Prod bt' z a b -> do
checkUpdate (bt,x,a)
(c',b') <- if isWildIdent z
then check c b
else do
b' <- checkIn (text "abs") $ substituteLType [(z,Vr x)] b
b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
check c b'
checkReset
return $ (Abs x c', Prod x a b')
return $ (Abs bt x c', Prod bt' x a b')
_ -> checkError $ text "function type expected instead of" <+> ppType env typ
App f a -> do
@@ -774,7 +774,7 @@ checkLType env trm typ0 = do
Let (x,(mty,def)) body -> case mty of
Just ty -> do
(def',ty') <- check def ty
checkUpdate (x,ty')
checkUpdate (Explicit,x,ty')
body' <- justCheck body typ
checkReset
return (Let (x,(Just ty',def')) body', typ)
@@ -827,14 +827,14 @@ checkLType env trm typ0 = do
pattContext :: LTEnv -> Type -> Patt -> Check Context
pattContext env typ p = case p of
PV x -> return [(x,typ)]
PV x -> return [(Explicit,x,typ)]
PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
t <- checkErr $ lookupResType cnc q c
(cont,v) <- checkErr $ typeFormCnc t
checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
(length cont == length ps)
checkEqLType env typ v (patt2term p)
mapM (uncurry (pattContext env)) (zip (map snd cont) ps) >>= return . concat
mapM (\((_,_,ty),p) -> pattContext env ty p) (zip cont ps) >>= return . concat
PR r -> do
typ' <- computeLType env typ
case typ' of
@@ -849,12 +849,12 @@ pattContext env typ p = case p of
PAs x p -> do
g <- pattContext env typ p
return $ (x,typ):g
return $ (Explicit,x,typ):g
PAlt p' q -> do
g1 <- pattContext env typ p'
g2 <- pattContext env typ q
let pts = nub ([fst pt | pt <- g1, notElem pt g2] ++ [fst pt | pt <- g2, notElem pt g1])
let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
checkCond
(text "incompatible bindings of" <+>
fsep (map ppIdent pts) <+>
@@ -889,7 +889,7 @@ termWith t ct = do
-- | light-weight substitution for dep. types
substituteLType :: Context -> Type -> Check Type
substituteLType g t = case t of
Vr x -> return $ maybe t id $ lookup x g
Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g]
_ -> composOp (substituteLType g) t
-- | compositional check\/infer of binary operations
@@ -933,7 +933,7 @@ checkIfEqLType env t u trm = do
(_,u) | u == typeError -> True
-- contravariance
(Prod x a b, Prod y c d) -> alpha g c a && alpha ((x,y):g) b d
(Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d
-- record subtyping
(RecType rs, RecType ts) -> all (\ (l,a) ->
@@ -975,7 +975,7 @@ checkIfEqLType env t u trm = do
_:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others)))
_ -> return locks
-- contravariance
(Prod x a b, Prod y c d) -> do
(Prod _ x a b, Prod _ y c d) -> do
ls1 <- missingLock g c a
ls2 <- missingLock g b d
return $ ls1 ++ ls2
@@ -989,11 +989,11 @@ checkIfEqLType env t u trm = do
ppType :: LTEnv -> Type -> Doc
ppType env ty =
case ty of
RecType fs -> case filter isLockLabel $ map fst fs of
[lock] -> text (drop 5 (showIdent (label2ident lock)))
_ -> ppTerm Unqualified 0 ty
Prod x a b -> ppType env a <+> text "->" <+> ppType env b
_ -> ppTerm Unqualified 0 ty
RecType fs -> case filter isLockLabel $ map fst fs of
[lock] -> text (drop 5 (showIdent (label2ident lock)))
_ -> ppTerm Unqualified 0 ty
Prod _ x a b -> ppType env a <+> text "->" <+> ppType env b
_ -> ppTerm Unqualified 0 ty
-- | linearization types and defaults
linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
@@ -1013,7 +1013,7 @@ linTypeOfType cnc m typ = do
text "with" $$
nest 2 (ppTerm Unqualified 0 val))) $
plusRecType vars val
return (symb,rec)
return (Explicit,symb,rec)
lookLin (_,c) = checks [ --- rather: update with defLinType ?
checkErr (lookupLincat cnc m c) >>= computeLType cnc
,return defLinType
@@ -1036,11 +1036,11 @@ allDependencies ism b =
opty _ = []
pts i = case i of
ResOper pty pt -> [pty,pt]
ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,t) <- cont]
ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,_,t) <- cont]
CncCat pty _ _ -> [pty]
CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type))
AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual
AbsCat (Just co) _ -> [Just ty | (_,ty) <- co]
AbsCat (Just co) _ -> [Just ty | (_,_,ty) <- co]
_ -> []
topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]

20
src/GF/Compile/Compute.hs
View File

@@ -62,22 +62,22 @@ computeTermOpt rec gr = comput True where
_ -> comp g t'
-- Abs x@(IA _) b -> do
Abs x b | full -> do
Abs _ _ _ | full -> do
let (xs,b1) = termFormCnc t
b' <- comp ([(x,Vr x) | x <- xs] ++ g) b1
b' <- comp ([(x,Vr x) | (_,x) <- xs] ++ g) b1
return $ mkAbs xs b'
-- b' <- comp (ext x (Vr x) g) b
-- return $ Abs x b'
Abs _ _ -> return t -- hnf
Abs _ _ _ -> return t -- hnf
Let (x,(_,a)) b -> do
a' <- comp g a
comp (ext x a' g) b
Prod x a b -> do
Prod b x a t -> do
a' <- comp g a
b' <- comp (ext x (Vr x) g) b
return $ Prod x a' b'
t' <- comp (ext x (Vr x) g) t
return $ Prod b x a' t'
-- beta-convert
App f a -> case appForm t of
@@ -92,9 +92,9 @@ computeTermOpt rec gr = comput True where
(t',b) <- appPredefined (mkApp h' as')
if b then return t' else comp g t'
Abs _ _ -> do
Abs _ _ _ -> do
let (xs,b) = termFormCnc h'
let g' = (zip xs as') ++ g
let g' = (zip (map snd xs) as') ++ g
let as2 = drop (length xs) as'
let xs2 = drop (length as') xs
b' <- comp g' (mkAbs xs2 b)
@@ -234,11 +234,11 @@ computeTermOpt rec gr = comput True where
f' <- hnf g f
a' <- comp g a
case (f',a') of
(Abs x b, FV as) ->
(Abs _ x b, FV as) ->
mapM (\c -> comp (ext x c g) b) as >>= return . variants
(_, FV as) -> mapM (\c -> comp g (App f' c)) as >>= return . variants
(FV fs, _) -> mapM (\c -> comp g (App c a')) fs >>= return . variants
(Abs x b,_) -> comp (ext x a' g) b
(Abs _ x b,_) -> comp (ext x a' g) b
(QC _ _,_) -> returnC $ App f' a'

24
src/GF/Compile/GrammarToGFCC.hs
View File

@@ -119,6 +119,10 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
i2i :: Ident -> CId
i2i = CId . ident2bs
b2b :: A.BindType -> C.BindType
b2b A.Explicit = C.Explicit
b2b A.Implicit = C.Implicit
mkType :: [Ident] -> A.Type -> C.Type
mkType scope t =
case GM.typeForm t of
@@ -127,9 +131,9 @@ mkType scope t =
mkExp :: [Ident] -> A.Term -> C.Expr
mkExp scope t = case GM.termForm t of
Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args))
Ok (xs,c,args) -> mkAbs xs (mkApp (map snd (reverse xs)++scope) c (map (mkExp scope) args))
where
mkAbs xs t = foldr (C.EAbs C.Explicit . i2i) t xs
mkAbs xs t = foldr (\(b,v) -> C.EAbs (b2b b) (i2i v)) t xs
mkApp scope c args = case c of
Q _ c -> foldl C.EApp (C.EFun (i2i c)) args
QC _ c -> foldl C.EApp (C.EFun (i2i c)) args
@@ -154,10 +158,10 @@ mkPatt scope p =
mkContext :: [Ident] -> A.Context -> ([Ident],[C.Hypo])
mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty
in if x == identW
then ( scope,(C.Explicit,i2i x,ty'))
else (x:scope,(C.Explicit,i2i x,ty'))) scope hyps
mkContext scope hyps = mapAccumL (\scope (bt,x,ty) -> let ty' = mkType scope ty
in if x == identW
then ( scope,(b2b bt,i2i x,ty'))
else (x:scope,(b2b bt,i2i x,ty'))) scope hyps
mkTerm :: Term -> C.Term
mkTerm tr = case tr of
@@ -179,7 +183,7 @@ mkTerm tr = case tr of
----- K (KP ss _) -> C.K (C.KP ss []) ---- TODO: prefix variants
Empty -> C.S []
App _ _ -> prtTrace tr $ C.C 66661 ---- for debugging
Abs _ t -> mkTerm t ---- only on toplevel
Abs _ _ t -> mkTerm t ---- only on toplevel
Alts (td,tvs) ->
C.K (C.KP (strings td) [C.Alt (strings u) (strings v) | (u,v) <- tvs])
_ -> prtTrace tr $ C.S [C.K (C.KS (render (A.ppTerm Unqualified 0 tr <+> int 66662)))] ---- for debugging
@@ -309,9 +313,9 @@ canon2canon opts abs cg0 =
ResParam (Just (ps,v)) ->
ResParam (Just ([(c,concatMap unRec cont) | (c,cont) <- ps],Nothing))
_ -> j
unRec (x,ty) = case ty of
RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (identW,typ)]
_ -> [(x,ty)]
unRec (bt,x,ty) = case ty of
RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (Explicit,identW,typ)]
_ -> [(bt,x,ty)]
----
trs v = traceD (render (tr v)) v

14
src/GF/Compile/Optimize.hs
View File

@@ -117,9 +117,9 @@ evalCncInfo opts gr cnc abs (c,info) = do
CncCat ptyp pde ppr -> do
pde' <- case (ptyp,pde) of
(Just typ, Just de) ->
liftM Just $ pEval ([(varStr, typeStr)], typ) de
liftM Just $ pEval ([(Explicit, varStr, typeStr)], typ) de
(Just typ, Nothing) ->
liftM Just $ mkLinDefault gr typ >>= partEval noOptions gr ([(varStr, typeStr)],typ)
liftM Just $ mkLinDefault gr typ >>= partEval noOptions gr ([(Explicit, varStr, typeStr)],typ)
_ -> return pde -- indirection
ppr' <- liftM Just $ evalPrintname gr c ppr (Just $ K $ showIdent c)
@@ -142,7 +142,7 @@ evalCncInfo opts gr cnc abs (c,info) = do
-- | the main function for compiling linearizations
partEval :: Options -> SourceGrammar -> (Context,Type) -> Term -> Err Term
partEval opts gr (context, val) trm = errIn (render (text "parteval" <+> ppTerm Qualified 0 trm)) $ do
let vars = map fst context
let vars = map (\(bt,x,t) -> x) context
args = map Vr vars
subst = [(v, Vr v) | v <- vars]
trm1 = mkApp trm args
@@ -150,7 +150,7 @@ partEval opts gr (context, val) trm = errIn (render (text "parteval" <+> ppTerm
trm3 <- if rightType trm2
then computeTerm gr subst trm2
else recordExpand val trm2 >>= computeTerm gr subst
return $ mkAbs vars trm3
return $ mkAbs [(Explicit,v) | v <- vars] trm3
where
-- don't eta expand records of right length (correct by type checking)
rightType (R rs) = case val of
@@ -178,8 +178,8 @@ recordExpand typ trm = case typ of
mkLinDefault :: SourceGrammar -> Type -> Err Term
mkLinDefault gr typ = do
case typ of
RecType lts -> mapPairsM mkDefField lts >>= (return . Abs varStr . R . mkAssign)
_ -> liftM (Abs varStr) $ mkDefField typ
RecType lts -> mapPairsM mkDefField lts >>= (return . Abs Explicit varStr . R . mkAssign)
_ -> liftM (Abs Explicit varStr) $ mkDefField typ
---- _ -> prtBad "linearization type must be a record type, not" typ
where
mkDefField typ = case typ of
@@ -211,7 +211,7 @@ evalPrintname gr c ppr lin =
comp = computeConcrete gr
oneBranch t = case t of
Abs _ b -> oneBranch b
Abs _ _ b -> oneBranch b
R (r:_) -> oneBranch $ snd $ snd r
T _ (c:_) -> oneBranch $ snd c
V _ (c:_) -> oneBranch c

8
src/GF/Compile/Refresh.hs
View File

@@ -37,13 +37,13 @@ refresh :: Term -> STM IdState Term
refresh e = case e of
Vr x -> liftM Vr (lookVar x)
Abs x b -> liftM2 Abs (refVarPlus x) (refresh b)
Abs b x t -> liftM2 (Abs b) (refVarPlus x) (refresh t)
Prod x a b -> do
Prod b x a t -> do
a' <- refresh a
x' <- refVar x
b' <- refresh b
return $ Prod x' a' b'
t' <- refresh t
return $ Prod b x' a' t'
Let (x,(mt,a)) b -> do
a' <- refresh a

10
src/GF/Compile/Rename.hs
View File

@@ -178,8 +178,8 @@ renPerh ren Nothing = return Nothing
renameTerm :: Status -> [Ident] -> Term -> Err Term
renameTerm env vars = ren vars where
ren vs trm = case trm of
Abs x b -> liftM (Abs x) (ren (x:vs) b)
Prod x a b -> liftM2 (Prod x) (ren vs a) (ren (x:vs) b)
Abs b x t -> liftM (Abs b x) (ren (x:vs) t)
Prod bt x a b -> liftM2 (Prod bt x) (ren vs a) (ren (x:vs) b)
Typed a b -> liftM2 Typed (ren vs a) (ren vs b)
Vr x
| elem x vs -> return trm
@@ -301,16 +301,16 @@ renameParam env (c,co) = do
renameContext :: Status -> Context -> Err Context
renameContext b = renc [] where
renc vs cont = case cont of
(x,t) : xts
(bt,x,t) : xts
| isWildIdent x -> do
t' <- ren vs t
xts' <- renc vs xts
return $ (x,t') : xts'
return $ (bt,x,t') : xts'
| otherwise -> do
t' <- ren vs t
let vs' = x:vs
xts' <- renc vs' xts
return $ (x,t') : xts'
return $ (bt,x,t') : xts'
_ -> return cont
ren = renameTerm b

18
src/GF/Compile/TC.hs
View File

@@ -77,7 +77,7 @@ whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
app :: Val -> Val -> Err Val
app u v = case u of
VClos env (Abs x e) -> eval ((x,v):env) e
VClos env (Abs _ x e) -> eval ((x,v):env) e
_ -> return $ VApp u v
eval :: Env -> Exp -> Err Val
@@ -100,9 +100,9 @@ eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
let v = VGen k
case (w1,w2) of
(VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
(VClos env1 (Abs x1 e1), VClos env2 (Abs x2 e2)) ->
(VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) ->
eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
(VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
(VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) ->
liftM2 (++)
(eqVal k (VClos env1 a1) (VClos env2 a2))
(eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
@@ -123,15 +123,15 @@ checkExp th tenv@(k,rho,gamma) e ty = do
case e of
Meta m -> return $ (AMeta m typ,[])
Abs x t -> case typ of
VClos env (Prod y a b) -> do
Abs _ x t -> case typ of
VClos env (Prod _ y a b) -> do
a' <- whnf $ VClos env a ---
(t',cs) <- checkExp th
(k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
return (AAbs x a' t', cs)
_ -> Bad (render (text "function type expected for" <+> ppTerm Unqualified 0 e <+> text "instead of" <+> ppValue Unqualified 0 typ))
Prod x a b -> do
Prod _ x a b -> do
testErr (typ == vType) "expected Type"
(a',csa) <- checkType th tenv a
(b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
@@ -176,7 +176,7 @@ inferExp th tenv@(k,rho,gamma) e = case e of
(f',w,csf) <- inferExp th tenv f
typ <- whnf w
case typ of
VClos env (Prod x a b) -> do
VClos env (Prod _ x a b) -> do
(a',csa) <- checkExp th tenv t (VClos env a)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)
@@ -217,7 +217,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
p:ps2 -> do
typ <- whnf ty
case typ of
VClos env (Prod y a b) -> do
VClos env (Prod _ y a b) -> do
a' <- whnf $ VClos env a
(p', sigma, binds, cs1) <- checkP tenv p y a'
let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
@@ -275,7 +275,7 @@ checkPatt th tenv exp val = do
(f',w,csf) <- checkExpP tenv f val
typ <- whnf w
case typ of
VClos env (Prod x a b) -> do
VClos env (Prod _ x a b) -> do
(a',_,csa) <- checkExpP tenv t (VClos env a)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)