From 7db4b641ce6abe90dd404459cd5eccb6e67f618c Mon Sep 17 00:00:00 2001 From: krasimir Date: Wed, 20 May 2009 21:03:56 +0000 Subject: refactor the PGF.Expr type and the evaluation of abstract expressions --- src/PGF/AbsCompute.hs | 106 ---------------------------------- src/PGF/Binary.hs | 21 ++++++- src/PGF/Data.hs | 2 +- src/PGF/Expr.hs | 157 +++++++++++++++++++++++++++++++++----------------- src/PGF/Expr.hs-boot | 13 +++++ src/PGF/Macros.hs | 12 ++-- src/PGF/Paraphrase.hs | 17 +++--- src/PGF/Type.hs | 2 +- src/PGF/TypeCheck.hs | 45 +++------------ 9 files changed, 157 insertions(+), 218 deletions(-) delete mode 100644 src/PGF/AbsCompute.hs create mode 100644 src/PGF/Expr.hs-boot (limited to 'src/PGF') diff --git a/src/PGF/AbsCompute.hs b/src/PGF/AbsCompute.hs deleted file mode 100644 index 0997ca952..000000000 --- a/src/PGF/AbsCompute.hs +++ /dev/null @@ -1,106 +0,0 @@ ----------------------------------------------------------------------- --- | --- Module : AbsCompute --- Maintainer : AR --- Stability : (stable) --- Portability : (portable) --- --- computation in abstract syntax with def definitions. --- --- modified from src GF computation ------------------------------------------------------------------------------ - -module PGF.AbsCompute ( - compute - ) where - -import PGF.Data -import PGF.Macros (lookDef,isData) -import PGF.Expr -import PGF.CId - -compute :: PGF -> Tree -> Tree -compute pgf = computeAbsTermIn pgf [] - -computeAbsTermIn :: PGF -> [CId] -> Tree -> Tree -computeAbsTermIn pgf vv = expr2tree . compt vv . tree2expr where - compt vv t = - let - t' = beta vv t - (yy,f,aa) = exprForm t' - vv' = yy ++ vv - aa' = map (compt vv') aa - in - mkAbs yy $ case look f of - Left (EEq eqs) -> case match eqs aa' of - Just (d,g) -> compt vv' $ subst vv' g d - _ -> mkApp f aa' - Left (EMeta _) -> mkApp f aa' -- canonical or primitive - Left d -> compt vv' $ mkApp d aa' - _ -> mkApp f aa' -- literal - look f = case f of - EVar c -> Left $ lookDef pgf c - _ -> Right f - match = findMatch pgf - -beta :: [CId] -> Expr -> Expr -beta vv c = case c of - EApp f a -> - let (a',f') = (beta vv a, beta vv f) in - case f' of - EAbs x b -> beta vv $ subst vv [(x,a')] (beta (x:vv) b) - _ -> (if a'==a && f'==f then id else beta vv) $ EApp f' a' - EAbs x b -> EAbs x (beta (x:vv) b) - _ -> c - - -subst :: [CId] -> Subst -> Expr -> Expr -subst xs g e = case e of - EAbs x b -> EAbs x (subst (x:xs) g e) ---- TODO: refresh variables - EApp f a -> EApp (substg f) (substg a) - EVar x -> maybe e id $ lookup x g - _ -> e - where - substg = subst xs g - -type Subst = [(CId,Expr)] -type Patt = Expr - - -exprForm :: Expr -> ([CId],Expr,[Expr]) -exprForm exp = upd ([],exp,[]) where - upd (xs,f,es) = case f of - EAbs x b -> upd (x:xs,b,es) - EApp c a -> upd (xs,c,a:es) - _ -> (reverse xs,f,es) - -mkAbs xs b = foldr EAbs b xs -mkApp f es = foldl EApp f es - --- special version of pattern matching, to deal with comp under lambda - -findMatch :: PGF -> [Equation] -> [Expr] -> Maybe (Expr, Subst) -findMatch pgf cases terms = case cases of - [] -> Nothing - (Equ patts _):_ | length patts /= length terms -> Nothing - (Equ patts val):cc -> case mapM tryMatch (zip patts terms) of - Just substs -> return (val, concat substs) - _ -> findMatch pgf cc terms - where - - tryMatch (p,t) = case (exprForm p, exprForm t) of - (([],EVar c,[]),_) | constructor c -> if p==t then return [] else Nothing - (([],EVar x,[]),_) | notMeta t -> return [(x,t)] - (([],p, pp), ([], f, tt)) | p == f && length pp == length tt -> do - matches <- mapM tryMatch (zip pp tt) - return (concat matches) - _ -> if p==t then return [] else Nothing - - notMeta e = case e of - EMeta _ -> False - EApp f a -> notMeta f && notMeta a - EAbs _ b -> notMeta b - _ -> True - - constructor = isData pgf - diff --git a/src/PGF/Binary.hs b/src/PGF/Binary.hs index 9df9be146..2a96f0c91 100644 --- a/src/PGF/Binary.hs +++ b/src/PGF/Binary.hs @@ -109,7 +109,6 @@ instance Binary Expr where put (ELit (LFlt d)) = putWord8 4 >> put d put (ELit (LInt i)) = putWord8 5 >> put i put (EMeta i) = putWord8 6 >> put i - put (EEq eqs) = putWord8 7 >> put eqs get = do tag <- getWord8 case tag of 0 -> liftM2 EAbs get get @@ -119,9 +118,25 @@ instance Binary Expr where 4 -> liftM (ELit . LFlt) get 5 -> liftM (ELit . LInt) get 6 -> liftM EMeta get - 7 -> liftM EEq get _ -> decodingError - + +instance Binary Patt where + put (PApp f ps) = putWord8 0 >> put (f,ps) + put (PVar x) = putWord8 1 >> put x + put PWild = putWord8 2 + put (PLit (LStr s)) = putWord8 3 >> put s + put (PLit (LFlt d)) = putWord8 4 >> put d + put (PLit (LInt i)) = putWord8 5 >> put i + get = do tag <- getWord8 + case tag of + 0 -> liftM2 PApp get get + 1 -> liftM PVar get + 2 -> return PWild + 3 -> liftM (PLit . LStr) get + 4 -> liftM (PLit . LFlt) get + 5 -> liftM (PLit . LInt) get + _ -> decodingError + instance Binary Equation where put (Equ ps e) = put (ps,e) get = liftM2 Equ get get diff --git a/src/PGF/Data.hs b/src/PGF/Data.hs index 5aba8cdfa..58952dc7d 100644 --- a/src/PGF/Data.hs +++ b/src/PGF/Data.hs @@ -24,7 +24,7 @@ data PGF = PGF { data Abstr = Abstr { aflags :: Map.Map CId String, -- value of a flag - funs :: Map.Map CId (Type,Expr), -- type and def of a fun + funs :: Map.Map CId (Type,[Equation]), -- type and def of a fun cats :: Map.Map CId [Hypo], -- context of a cat catfuns :: Map.Map CId [CId] -- funs to a cat (redundant, for fast lookup) } diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs index eee489100..79c88303d 100644 --- a/src/PGF/Expr.hs +++ b/src/PGF/Expr.hs @@ -1,13 +1,13 @@ module PGF.Expr(Tree(..), Literal(..), readTree, showTree, pTree, ppTree, - Expr(..), Equation(..), - readExpr, showExpr, pExpr, ppExpr, + Expr(..), Patt(..), Equation(..), + readExpr, showExpr, pExpr, ppExpr, ppPatt, tree2expr, expr2tree, -- needed in the typechecker - Value(..), Env, eval, apply, + Value(..), Env, eval, apply, eqValue, -- helpers pStr,pFactor, @@ -17,6 +17,7 @@ module PGF.Expr(Tree(..), Literal(..), ) where import PGF.CId +import PGF.Type import Data.Char import Data.Maybe @@ -29,7 +30,7 @@ data Literal = LStr String -- ^ string constant | LInt Integer -- ^ integer constant | LFlt Double -- ^ floating point constant - deriving (Eq,Ord,Show) + deriving (Eq,Ord) -- | The tree is an evaluated expression in the abstract syntax -- of the grammar. The type is especially restricted to not @@ -53,17 +54,24 @@ data Expr = | ELit Literal -- ^ literal | EMeta Int -- ^ meta variable | EVar CId -- ^ variable or function reference - | EEq [Equation] -- ^ lambda function defined as a set of equations with pattern matching | EPi CId Expr Expr -- ^ dependent function type deriving (Eq,Ord) +-- | The pattern is used to define equations in the abstract syntax of the grammar. +data Patt = + PApp CId [Patt] -- ^ application. The identifier should be constructor i.e. defined with 'data' + | PLit Literal -- ^ literal + | PVar CId -- ^ variable + | PWild -- ^ wildcard + deriving (Eq,Ord) + -- | The equation is used to define lambda function as a sequence -- of equations with pattern matching. The list of 'Expr' represents -- the patterns and the second 'Expr' is the function body for this -- equation. data Equation = - Equ [Expr] Expr - deriving (Eq,Ord,Show) + Equ [Patt] Expr + deriving (Eq,Ord) -- | parses 'String' as an expression readTree :: String -> Maybe Tree @@ -120,24 +128,13 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li return (Meta n) pExpr :: RP.ReadP Expr -pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm RP.<++ pEqs) +pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm) where pTerm = fmap (foldl1 EApp) (RP.sepBy1 pFactor RP.skipSpaces) pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')) e <- pExpr return (foldr EAbs e xs) - - pEqs = fmap EEq $ - RP.between (RP.skipSpaces >> RP.char '{') - (RP.skipSpaces >> RP.char '}') - (RP.sepBy1 (RP.skipSpaces >> pEq) - (RP.skipSpaces >> RP.string ";")) - - pEq = do pats <- (RP.sepBy1 pExpr RP.skipSpaces) - RP.skipSpaces >> RP.string "=>" - e <- pExpr - return (Equ pats e) pFactor = fmap EVar pCId RP.<++ fmap ELit pLit @@ -176,6 +173,7 @@ ppTree d (Meta n) = PP.char '?' PP.<> PP.int n ppTree d (Var id) = PP.text (prCId id) +ppExpr :: Int -> Expr -> PP.Doc ppExpr d (EAbs x e) = let (xs,e1) = getVars (EAbs x e) in ppParens (d > 0) (PP.char '\\' PP.<> PP.hsep (PP.punctuate PP.comma (map (PP.text . prCId) xs)) PP.<+> @@ -188,9 +186,11 @@ ppExpr d (EApp e1 e2) = ppParens (d > 1) ((ppExpr 1 e1) PP.<+> (ppExpr 2 e2)) ppExpr d (ELit l) = ppLit l ppExpr d (EMeta n) = PP.char '?' PP.<+> PP.int n ppExpr d (EVar f) = PP.text (prCId f) -ppExpr d (EEq eqs) = PP.braces (PP.sep (PP.punctuate PP.semi (map ppEquation eqs))) -ppEquation (Equ pats e) = PP.hsep (map (ppExpr 2) pats) PP.<+> PP.text "=>" PP.<+> ppExpr 0 e +ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps)) +ppPatt d (PLit l) = ppLit l +ppPatt d (PVar f) = PP.text (prCId f) +ppPatt d PWild = PP.char '_' ppLit (LStr s) = PP.text (show s) ppLit (LInt n) = PP.integer n @@ -212,46 +212,97 @@ tree2expr (Meta n) = EMeta n tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs tree2expr (Var x) = EVar x --- | Converts an expression to tree. If the expression --- contains unevaluated applications they will be applied. -expr2tree :: Expr -> Tree -expr2tree e = value2tree (eval Map.empty e) [] [] +-- | Converts an expression to tree. The expression +-- is first reduced to beta-eta-alfa normal form and +-- after that converted to tree. +expr2tree :: Funs -> Expr -> Tree +expr2tree funs e = value2tree [] (eval funs Map.empty e) where - value2tree (VApp v1 v2) xs ts = value2tree v1 xs (value2tree v2 [] []:ts) - value2tree (VVar x) xs ts = ret xs (fun xs x ts) - value2tree (VMeta n) xs [] = ret xs (Meta n) - value2tree (VLit l) xs [] = ret xs (Lit l) - value2tree (VClosure env (EAbs x e)) xs [] = value2tree (eval (Map.insert x (VVar x) env) e) (x:xs) [] - - fun xs x ts - | x `elem` xs = Var x - | otherwise = Fun x ts + value2tree xs (VApp f vs) = case Map.lookup f funs of + Just (DTyp hyps _ _,_) -> -- eta conversion + let a1 = length hyps + a2 = length vs + a = a1 - a2 + i = length xs + xs' = [var i | i <- [i..i+a-1]] + in ret (reverse xs'++xs) + (Fun f (map (value2tree []) vs++map Var xs')) + Nothing -> error ("unknown variable "++prCId f) + value2tree xs (VGen i) = ret xs (Var (var i)) + value2tree xs (VMeta n) = ret xs (Meta n) + value2tree xs (VLit l) = ret xs (Lit l) + value2tree xs (VClosure env (EAbs x e)) = let i = length xs + in value2tree (var i:xs) (eval funs (Map.insert x (VGen i) env) e) + + var i = mkCId ('v':show i) ret [] t = t ret xs t = Abs (reverse xs) t data Value - = VGen Int - | VApp Value Value - | VVar CId - | VMeta Int + = VApp CId [Value] | VLit Literal + | VMeta Int + | VGen Int | VClosure Env Expr - deriving (Show,Eq,Ord) - -type Env = Map.Map CId Value - -eval :: Env -> Expr -> Value -eval env (EVar x) = fromMaybe (VVar x) (Map.lookup x env) -eval env (EApp e1 e2) = apply (eval env e1) (eval env e2) -eval env (EAbs x e) = VClosure env (EAbs x e) -eval env (EMeta k) = VMeta k -eval env (ELit l) = VLit l -eval env e = VClosure env e - -apply :: Value -> Value -> Value -apply (VClosure env (EAbs x e)) v = eval (Map.insert x v env) e -apply v0 v = VApp v0 v + deriving (Eq,Ord) + +type Funs = Map.Map CId (Type,[Equation]) -- type and def of a fun +type Env = Map.Map CId Value + +eval :: Funs -> Env -> Expr -> Value +eval funs env (EVar x) = case Map.lookup x env of + Just v -> v + Nothing -> case Map.lookup x funs of + Just (_,eqs) -> case eqs of + Equ [] e : _ -> eval funs env e + [] -> VApp x [] + Nothing -> error ("unknown variable "++prCId x) +eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2] +eval funs env (EAbs x e) = VClosure env (EAbs x e) +eval funs env (EMeta k) = VMeta k +eval funs env (ELit l) = VLit l + +apply :: Funs -> Env -> Expr -> [Value] -> Value +apply funs env e [] = eval funs env e +apply funs env (EVar x) vs = case Map.lookup x env of + Just v -> case (v,vs) of + (VClosure env (EAbs x e),v:vs) -> apply funs (Map.insert x v env) e vs + Nothing -> case Map.lookup x funs of + Just (_,eqs) -> case match eqs vs of + Just (e,vs,env) -> apply funs env e vs + Nothing -> VApp x vs + Nothing -> error ("unknown variable "++prCId x) +apply funs env (EAbs x e) (v:vs) = apply funs (Map.insert x v env) e vs +apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs) + +match :: [Equation] -> [Value] -> Maybe (Expr, [Value], Env) +match eqs vs = + case eqs of + [] -> Nothing + (Equ ps res):eqs -> let (as,vs') = splitAt (length ps) vs + in case zipWithM tryMatch ps as of + Just envs -> Just (res, vs', Map.unions envs) + Nothing -> match eqs vs + where + tryMatch p v = case (p, v) of + (PVar x, _ ) -> Just (Map.singleton x v) + (PApp f ps, VApp fe vs) | f == fe -> do envs <- zipWithM tryMatch ps vs + return (Map.unions envs) + (PLit l, VLit le ) | l == le -> Just Map.empty + _ -> Nothing + +eqValue :: Int -> Value -> Value -> [(Value,Value)] +eqValue k v1 v2 = + case (v1,v2) of + (VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue k) vs1 vs2) + (VLit l1, VLit l2 ) | l1 == l2 -> [] + (VMeta i, VMeta j ) | i == j -> [] + (VGen i, VGen j ) | i == j -> [] + (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) -> + let v = VGen k + in eqValue (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2) + _ -> [(v1,v2)] --- use composOp and state monad... newMetas :: Expr -> Expr diff --git a/src/PGF/Expr.hs-boot b/src/PGF/Expr.hs-boot new file mode 100644 index 000000000..0369be173 --- /dev/null +++ b/src/PGF/Expr.hs-boot @@ -0,0 +1,13 @@ +module PGF.Expr where + +import qualified Text.PrettyPrint as PP +import qualified Text.ParserCombinators.ReadP as RP + +data Expr + +instance Eq Expr +instance Ord Expr + +pFactor :: RP.ReadP Expr + +ppExpr :: Int -> Expr -> PP.Doc diff --git a/src/PGF/Macros.hs b/src/PGF/Macros.hs index 22b96df92..462fa9cba 100644 --- a/src/PGF/Macros.hs +++ b/src/PGF/Macros.hs @@ -37,14 +37,15 @@ lookType :: PGF -> CId -> Type lookType pgf f = fst $ lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf)) -lookDef :: PGF -> CId -> Expr +lookDef :: PGF -> CId -> [Equation] lookDef pgf f = snd $ lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf)) isData :: PGF -> CId -> Bool -isData pgf f = case Map.lookup f (funs (abstract pgf)) of - Just (_,EMeta 0) -> True ---- the encoding of data constrs - _ -> False +isData pgf f = + case Map.lookup f (funs (abstract pgf)) of + Just (_,[]) -> True -- the encoding of data constrs + _ -> False lookValCat :: PGF -> CId -> CId lookValCat pgf = valCat . lookType pgf @@ -120,9 +121,6 @@ contextLength :: Type -> Int contextLength ty = case ty of DTyp hyps _ _ -> length hyps -primNotion :: Expr -primNotion = EEq [] - term0 :: CId -> Term term0 = TM . prCId diff --git a/src/PGF/Paraphrase.hs b/src/PGF/Paraphrase.hs index 9e0123605..ff718a785 100644 --- a/src/PGF/Paraphrase.hs +++ b/src/PGF/Paraphrase.hs @@ -49,13 +49,8 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where [(ps,p) | (p,d@(Fun g ps)) <- equs, g==f, isClosed d || (length equs == 1 && isLinear d)] - equss = [(f,[(Fun f (map expr2tree ps), expr2tree d) | (Equ ps d) <- eqs]) | - (f,(_,d)) <- Map.assocs (funs (abstract pgf)), eqs <- defs d] - - defs d = case d of - EEq eqs -> [eqs] - EMeta _ -> [] - _ -> [[Equ [] d]] + equss = [(f,[(Fun f (map patt2tree ps), expr2tree (funs (abstract pgf)) d) | (Equ ps d) <- eqs]) | + (f,(_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)] trequ s f e = True ----trace (s ++ ": " ++ show f ++ " " ++ show e) True @@ -86,8 +81,6 @@ isLinear = nodup . vars where nodup = all ((<2) . length) . group . sort --- special version of AbsCompute.findMatch, working on Tree - match :: [([Tree],Tree)] -> [Tree] -> [(Tree, Subst)] match cases terms = case cases of [] -> [] @@ -108,3 +101,9 @@ match cases terms = case cases of Fun f ts -> all notMeta ts _ -> True +-- | Converts a pattern to tree. +patt2tree :: Patt -> Tree +patt2tree (PApp f ps) = Fun f (map patt2tree ps) +patt2tree (PLit l) = Lit l +patt2tree (PVar x) = Var x +patt2tree PWild = Meta 0 diff --git a/src/PGF/Type.hs b/src/PGF/Type.hs index 8c513ffd4..5b77c8085 100644 --- a/src/PGF/Type.hs +++ b/src/PGF/Type.hs @@ -3,7 +3,7 @@ module PGF.Type ( Type(..), Hypo(..), pType, ppType, ppHypo ) where import PGF.CId -import PGF.Expr +import {-# SOURCE #-} PGF.Expr import Data.Char import qualified Text.PrettyPrint as PP import qualified Text.ParserCombinators.ReadP as RP diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs index 1a2ba334a..7a7a5ccc0 100644 --- a/src/PGF/TypeCheck.hs +++ b/src/PGF/TypeCheck.hs @@ -17,7 +17,6 @@ module PGF.TypeCheck ( import PGF.Data import PGF.Macros (lookDef,isData) import PGF.Expr -import PGF.AbsCompute import PGF.CId import GF.Data.ErrM @@ -29,7 +28,7 @@ import Debug.Trace typecheck :: PGF -> Tree -> [Tree] typecheck pgf t = case inferExpr pgf (newMetas (tree2expr t)) of - Ok t -> [expr2tree t] + Ok t -> [expr2tree (funs (abstract pgf)) t] Bad s -> trace s [] inferExpr :: PGF -> Expr -> Err Expr @@ -50,26 +49,24 @@ infer pgf tenv@(k,rho,gamma) e = case e of -- K i -> return (AStr i, valAbsString, []) EApp f t -> do - (f',w,csf) <- infer pgf tenv f - typ <- whnf w + (f',typ,csf) <- infer pgf tenv f case typ of VClosure env (EPi x a b) -> do (a',csa) <- checkExp pgf tenv t (VClosure env a) - b' <- whnf $ VClosure (eins x (VClosure rho t) env) b + let b' = eval (funs (abstract pgf)) (eins x (VClosure rho t) env) b return $ (EApp f' a', b', csf ++ csa) _ -> Bad ("function type expected for function " ++ show f) _ -> Bad ("cannot infer type of expression" ++ show e) checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)]) -checkExp pgf tenv@(k,rho,gamma) e ty = do - typ <- whnf ty +checkExp pgf tenv@(k,rho,gamma) e typ = do let v = VGen k case e of EMeta m -> return $ (e,[]) EAbs x t -> case typ of VClosure env (EPi y a b) -> do - a' <- whnf $ VClosure env a + let a' = eval (funs (abstract pgf)) env a (t',cs) <- checkExp pgf (k+1,eins x v rho, eins x a' gamma) t (VClosure (eins y v env) b) return (EAbs x t', cs) @@ -79,7 +76,7 @@ checkExp pgf tenv@(k,rho,gamma) e ty = do checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)]) checkInferExp pgf tenv@(k,_,_) e typ = do (e',w,cs1) <- infer pgf tenv e - cs2 <- eqValue k w typ + let cs2 = eqValue k w typ return (e',cs1 ++ cs2) lookupEVar :: PGF -> TCEnv -> CId -> Err Value @@ -100,40 +97,12 @@ eins = Map.insert emptyTCEnv :: TCEnv emptyTCEnv = (0,eempty,eempty) -whnf :: Value -> Err Value -whnf v = case v of - VApp u w -> do - u' <- whnf u - w' <- whnf w - return $ apply u' w' - VClosure env e -> return $ eval env e - _ -> return v - -eqValue :: Int -> Value -> Value -> Err [(Value,Value)] -eqValue k u1 u2 = do - w1 <- whnf u1 - w2 <- whnf u2 - let v = VGen k - case (w1,w2) of - (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqValue k f1 f2) (eqValue k a1 a2) - (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) -> - eqValue (k+1) (VClosure (eins x1 v env1) e1) (VClosure (eins x2 v env2) e2) - (VClosure env1 (EPi x1 a1 b1), VClosure env2 (EPi x2 a2 b2)) -> - liftM2 (++) - (eqValue k (VClosure env1 a1) (VClosure env2 a2)) - (eqValue (k+1) (VClosure (eins x1 v env1) b1) (VClosure (eins x2 v env2) b2)) - (VGen i, VGen j) -> return [(w1,w2) | i /= j] - (VVar i, VVar j) -> return [(w1,w2) | i /= j] - _ -> return [(w1,w2) | w1 /= w2] --- invariant: constraints are in whnf - -- this is not given in Expr prValue = showExpr . value2expr value2expr v = case v of - VApp v u -> EApp (value2expr v) (value2expr u) - VVar x -> EVar x + VApp f vs -> foldl EApp (EVar f) (map value2expr vs) VMeta i -> EMeta i VClosure g e -> e ---- VLit l -> ELit l -- cgit v1.2.3