diff options
Diffstat (limited to 'src/GF/Compile')
| -rw-r--r-- | src/GF/Compile/AbsCompute.hs | 10 | ||||
| -rw-r--r-- | src/GF/Compile/CheckGrammar.hs | 84 | ||||
| -rw-r--r-- | src/GF/Compile/Compute.hs | 20 | ||||
| -rw-r--r-- | src/GF/Compile/GrammarToGFCC.hs | 24 | ||||
| -rw-r--r-- | src/GF/Compile/Optimize.hs | 14 | ||||
| -rw-r--r-- | src/GF/Compile/Refresh.hs | 8 | ||||
| -rw-r--r-- | src/GF/Compile/Rename.hs | 10 | ||||
| -rw-r--r-- | src/GF/Compile/TC.hs | 18 |
8 files changed, 96 insertions, 92 deletions
diff --git a/src/GF/Compile/AbsCompute.hs b/src/GF/Compile/AbsCompute.hs index 48499eb74..3f4c6d061 100644 --- a/src/GF/Compile/AbsCompute.hs +++ b/src/GF/Compile/AbsCompute.hs @@ -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 = diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs index 6e6e27c74..98cd17f23 100644 --- a/src/GF/Compile/CheckGrammar.hs +++ b/src/GF/Compile/CheckGrammar.hs @@ -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] diff --git a/src/GF/Compile/Compute.hs b/src/GF/Compile/Compute.hs index f764acc52..f4bc61a5b 100644 --- a/src/GF/Compile/Compute.hs +++ b/src/GF/Compile/Compute.hs @@ -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' diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs index aa84f820c..18e262de7 100644 --- a/src/GF/Compile/GrammarToGFCC.hs +++ b/src/GF/Compile/GrammarToGFCC.hs @@ -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 diff --git a/src/GF/Compile/Optimize.hs b/src/GF/Compile/Optimize.hs index 9122b6e5f..e83f0e912 100644 --- a/src/GF/Compile/Optimize.hs +++ b/src/GF/Compile/Optimize.hs @@ -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 diff --git a/src/GF/Compile/Refresh.hs b/src/GF/Compile/Refresh.hs index ba6142ddd..04800fcce 100644 --- a/src/GF/Compile/Refresh.hs +++ b/src/GF/Compile/Refresh.hs @@ -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 diff --git a/src/GF/Compile/Rename.hs b/src/GF/Compile/Rename.hs index 8c563eeed..7d61e8a7d 100644 --- a/src/GF/Compile/Rename.hs +++ b/src/GF/Compile/Rename.hs @@ -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 diff --git a/src/GF/Compile/TC.hs b/src/GF/Compile/TC.hs index 3999c223b..8cc2ff45b 100644 --- a/src/GF/Compile/TC.hs +++ b/src/GF/Compile/TC.hs @@ -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) |