summaryrefslogtreecommitdiff
path: root/src/compiler/GF/Compile/Abstract
diff options
context:
space:
mode:
authorkrasimir <krasimir@chalmers.se>2009-12-13 18:50:29 +0000
committerkrasimir <krasimir@chalmers.se>2009-12-13 18:50:29 +0000
commitf85232947e74ee7ef8c7b0ad2338212e7e68f1be (patch)
tree667b886a5e3a4b026a63d4e3597f32497d824761 /src/compiler/GF/Compile/Abstract
parentd88a865faff59c98fc91556ff8700b10ee5f2df8 (diff)
reorganize the directories under src, and rescue the JavaScript interpreter from deprecated
Diffstat (limited to 'src/compiler/GF/Compile/Abstract')
-rw-r--r--src/compiler/GF/Compile/Abstract/Compute.hs138
-rw-r--r--src/compiler/GF/Compile/Abstract/TC.hs294
-rw-r--r--src/compiler/GF/Compile/Abstract/TypeCheck.hs83
3 files changed, 515 insertions, 0 deletions
diff --git a/src/compiler/GF/Compile/Abstract/Compute.hs b/src/compiler/GF/Compile/Abstract/Compute.hs
new file mode 100644
index 000000000..d5c9a163c
--- /dev/null
+++ b/src/compiler/GF/Compile/Abstract/Compute.hs
@@ -0,0 +1,138 @@
+----------------------------------------------------------------------
+-- |
+-- Module : GF.Compile.Abstract.Compute
+-- Maintainer : AR
+-- Stability : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/02 20:50:19 $
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.8 $
+--
+-- computation in abstract syntax w.r.t. explicit definitions.
+--
+-- old GF computation; to be updated
+-----------------------------------------------------------------------------
+
+module GF.Compile.Abstract.Compute (LookDef,
+ compute,
+ computeAbsTerm,
+ computeAbsTermIn,
+ beta
+ ) where
+
+import GF.Data.Operations
+
+import GF.Grammar
+import GF.Grammar.Lookup
+
+import Debug.Trace
+import Data.List(intersperse)
+import Control.Monad (liftM, liftM2)
+import Text.PrettyPrint
+
+-- for debugging
+tracd m t = t
+-- tracd = trace
+
+compute :: SourceGrammar -> Exp -> Err Exp
+compute = computeAbsTerm
+
+computeAbsTerm :: SourceGrammar -> Exp -> Err Exp
+computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []
+
+-- | a hack to make compute work on source grammar as well
+type LookDef = Ident -> Ident -> Err (Maybe Int,Maybe [Equation])
+
+computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
+computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unqualified 0 e)) $ compt xs e where
+ compt vv t = case t of
+-- Prod x a b -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
+-- Abs x b -> liftM (Abs x) (compt (x:vv) b)
+ _ -> do
+ let t' = beta vv t
+ (yy,f,aa) <- termForm t'
+ let vv' = map snd yy ++ vv
+ aa' <- mapM (compt vv') aa
+ case look f of
+ Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 f) $
+ case findMatch eqs aa' of
+ Ok (d,g) -> do
+ --- let (xs,ts) = unzip g
+ --- ts' <- alphaFreshAll vv' ts
+ let g' = g --- zip xs ts'
+ d' <- compt vv' $ substTerm vv' g' d
+ tracd (text "by Egs:" <+> ppTerm Unqualified 0 d') $ return $ mkAbs yy $ d'
+ _ -> tracd (text "no match" <+> ppTerm Unqualified 0 t') $
+ do
+ let v = mkApp f aa'
+ return $ mkAbs yy $ v
+ _ -> do
+ let t2 = mkAbs yy $ mkApp f aa'
+ tracd (text "not defined" <+> ppTerm Unqualified 0 t2) $ return t2
+
+ look t = case t of
+ (Q m f) -> case lookd m f of
+ Ok (_,md) -> md
+ _ -> Nothing
+ _ -> Nothing
+
+beta :: [Ident] -> Exp -> Exp
+beta vv c = case c of
+ Let (x,(_,a)) b -> beta vv $ substTerm vv [(x,beta vv a)] (beta (x:vv) b)
+ 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)
+ _ -> (if a'==a && f'==f then id else beta vv) $ App f' a'
+ 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
+
+findMatch :: [([Patt],Term)] -> [Term] -> Err (Term, Substitution)
+findMatch cases terms = case cases of
+ [] -> Bad $ render (text "no applicable case for" <+> hcat (punctuate comma (map (ppTerm Unqualified 0) terms)))
+ (patts,_):_ | length patts /= length terms ->
+ Bad (render (text "wrong number of args for patterns :" <+>
+ hsep (map (ppPatt Unqualified 0) patts) <+> text "cannot take" <+> hsep (map (ppTerm Unqualified 0) terms)))
+ (patts,val):cc -> case mapM tryMatch (zip patts terms) of
+ Ok substs -> return (tracd (text "value" <+> ppTerm Unqualified 0 val) val, concat substs)
+ _ -> findMatch cc terms
+
+tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
+tryMatch (p,t) = do
+ t' <- termForm t
+ trym p t'
+ where
+
+ trym p t' = err (\s -> tracd s (Bad s)) (\t -> tracd (prtm p t) (return t)) $ ----
+ case (p,t') of
+ (PW, _) | notMeta t -> return [] -- optimization with wildcard
+ (PV x, _) | notMeta t -> return [(x,t)]
+ (PString s, ([],K i,[])) | s==i -> return []
+ (PInt s, ([],EInt i,[])) | s==i -> return []
+ (PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding?
+ (PP q p pp, ([], QC r f, tt)) |
+ p `eqStrIdent` f && length pp == length tt -> do
+ matches <- mapM tryMatch (zip pp tt)
+ return (concat matches)
+ (PP q p pp, ([], Q r f, tt)) |
+ p `eqStrIdent` f && length pp == length tt -> do
+ matches <- mapM tryMatch (zip pp tt)
+ return (concat matches)
+ (PT _ p',_) -> trym p' t'
+ (PAs x p',_) -> do
+ subst <- trym p' t'
+ return $ (x,t) : subst
+ _ -> Bad (render (text "no match in pattern" <+> ppPatt Unqualified 0 p <+> text "for" <+> ppTerm Unqualified 0 t))
+
+ notMeta e = case e of
+ Meta _ -> False
+ App f a -> notMeta f && notMeta a
+ Abs _ _ b -> notMeta b
+ _ -> True
+
+ prtm p g =
+ ppPatt Unqualified 0 p <+> colon $$ hsep (punctuate semi [ppIdent x <+> char '=' <+> ppTerm Unqualified 0 y | (x,y) <- g])
diff --git a/src/compiler/GF/Compile/Abstract/TC.hs b/src/compiler/GF/Compile/Abstract/TC.hs
new file mode 100644
index 000000000..163301838
--- /dev/null
+++ b/src/compiler/GF/Compile/Abstract/TC.hs
@@ -0,0 +1,294 @@
+----------------------------------------------------------------------
+-- |
+-- Module : TC
+-- Maintainer : AR
+-- Stability : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/02 20:50:19 $
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.11 $
+--
+-- Thierry Coquand's type checking algorithm that creates a trace
+-----------------------------------------------------------------------------
+
+module GF.Compile.Abstract.TC (AExp(..),
+ Theory,
+ checkExp,
+ inferExp,
+ checkBranch,
+ eqVal,
+ whnf
+ ) where
+
+import GF.Data.Operations
+import GF.Grammar
+import GF.Grammar.Predef
+
+import Control.Monad
+import Data.List (sortBy)
+import Data.Maybe
+import Text.PrettyPrint
+
+data AExp =
+ AVr Ident Val
+ | ACn QIdent Val
+ | AType
+ | AInt Integer
+ | AFloat Double
+ | AStr String
+ | AMeta MetaId Val
+ | AApp AExp AExp Val
+ | AAbs Ident Val AExp
+ | AProd Ident AExp AExp
+ | AEqs [([Exp],AExp)] --- not used
+ | ARecType [ALabelling]
+ | AR [AAssign]
+ | AP AExp Label Val
+ | AData Val
+ deriving (Eq,Show)
+
+type ALabelling = (Label, AExp)
+type AAssign = (Label, (Val, AExp))
+
+type Theory = QIdent -> Err Val
+
+lookupConst :: Theory -> QIdent -> Err Val
+lookupConst th f = th f
+
+lookupVar :: Env -> Ident -> Err Val
+lookupVar g x = maybe (Bad (render (text "unknown variable" <+> ppIdent x))) return $ lookup x ((IW,uVal):g)
+-- wild card IW: no error produced, ?0 instead.
+
+type TCEnv = (Int,Env,Env)
+
+emptyTCEnv :: TCEnv
+emptyTCEnv = (0,[],[])
+
+whnf :: Val -> Err Val
+whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
+ case v of
+ VApp u w -> do
+ u' <- whnf u
+ w' <- whnf w
+ app u' w'
+ VClos env e -> eval env e
+ _ -> return v
+
+app :: Val -> Val -> Err Val
+app u v = case u of
+ VClos env (Abs _ x e) -> eval ((x,v):env) e
+ _ -> return $ VApp u v
+
+eval :: Env -> Exp -> Err Val
+eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
+ case e of
+ Vr x -> lookupVar env x
+ Q m c -> return $ VCn (m,c)
+ QC m c -> return $ VCn (m,c) ---- == Q ?
+ Sort c -> return $ VType --- the only sort is Type
+ App f a -> join $ liftM2 app (eval env f) (eval env a)
+ RecType xs -> do xs <- mapM (\(l,e) -> eval env e >>= \e -> return (l,e)) xs
+ return (VRecType xs)
+ _ -> return $ VClos env e
+
+eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
+eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
+ do
+ w1 <- whnf u1
+ w2 <- whnf 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)) ->
+ 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)) ->
+ liftM2 (++)
+ (eqVal k (VClos env1 a1) (VClos env2 a2))
+ (eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
+ (VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
+ (VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
+ --- thus ignore qualifications; valid because inheritance cannot
+ --- be qualified. Simplifies annotation. AR 17/3/2005
+ _ -> return [(w1,w2) | w1 /= w2]
+-- invariant: constraints are in whnf
+
+checkType :: Theory -> TCEnv -> Exp -> Err (AExp,[(Val,Val)])
+checkType th tenv e = checkExp th tenv e vType
+
+checkExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkExp th tenv@(k,rho,gamma) e ty = do
+ typ <- whnf ty
+ let v = VGen k
+ case e of
+ Meta m -> return $ (AMeta m typ,[])
+
+ 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
+ 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
+ return (AProd x a' b', csa ++ csb)
+
+ R xs ->
+ case typ of
+ VRecType ys -> do case [l | (l,_) <- ys, isNothing (lookup l xs)] of
+ [] -> return ()
+ ls -> fail (render (text "no value given for label:" <+> fsep (punctuate comma (map ppLabel ls))))
+ r <- mapM (checkAssign th tenv ys) xs
+ let (xs,css) = unzip r
+ return (AR xs, concat css)
+ _ -> Bad (render (text "record type expected for" <+> ppTerm Unqualified 0 e <+> text "instead of" <+> ppValue Unqualified 0 typ))
+
+ P r l -> do (r',cs) <- checkExp th tenv r (VRecType [(l,typ)])
+ return (AP r' l typ,cs)
+
+ _ -> checkInferExp th tenv e typ
+
+checkInferExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkInferExp th tenv@(k,_,_) e typ = do
+ (e',w,cs1) <- inferExp th tenv e
+ cs2 <- eqVal k w typ
+ return (e',cs1 ++ cs2)
+
+inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
+inferExp th tenv@(k,rho,gamma) e = case e of
+ Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
+ Q m c | m == cPredefAbs && isPredefCat c
+ -> return (ACn (m,c) vType, vType, [])
+ | otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
+ QC m c -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) ----
+ EInt i -> return (AInt i, valAbsInt, [])
+ EFloat i -> return (AFloat i, valAbsFloat, [])
+ K i -> return (AStr i, valAbsString, [])
+ Sort _ -> return (AType, vType, [])
+ RecType xs -> do r <- mapM (checkLabelling th tenv) xs
+ let (xs,css) = unzip r
+ return (ARecType xs, vType, concat css)
+ App f t -> do
+ (f',w,csf) <- inferExp th tenv f
+ typ <- whnf w
+ case typ of
+ 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)
+ _ -> Bad (render (text "Prod expected for function" <+> ppTerm Unqualified 0 f <+> text "instead of" <+> ppValue Unqualified 0 typ))
+ _ -> Bad (render (text "cannot infer type of expression" <+> ppTerm Unqualified 0 e))
+
+checkLabelling :: Theory -> TCEnv -> Labelling -> Err (ALabelling, [(Val,Val)])
+checkLabelling th tenv (lbl,typ) = do
+ (atyp,cs) <- checkType th tenv typ
+ return ((lbl,atyp),cs)
+
+checkAssign :: Theory -> TCEnv -> [(Label,Val)] -> Assign -> Err (AAssign, [(Val,Val)])
+checkAssign th tenv@(k,rho,gamma) typs (lbl,(Just typ,exp)) = do
+ (atyp,cs1) <- checkType th tenv typ
+ val <- eval rho typ
+ cs2 <- case lookup lbl typs of
+ Nothing -> return []
+ Just val0 -> eqVal k val val0
+ (aexp,cs3) <- checkExp th tenv exp val
+ return ((lbl,(val,aexp)),cs1++cs2++cs3)
+checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
+ case lookup lbl typs of
+ Nothing -> do (aexp,val,cs) <- inferExp th tenv exp
+ return ((lbl,(val,aexp)),cs)
+ Just val -> do (aexp,cs) <- checkExp th tenv exp val
+ return ((lbl,(val,aexp)),cs)
+
+checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
+checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
+ chB tenv' ps' ty
+ where
+
+ (ps',_,rho2,k') = ps2ts k ps
+ tenv' = (k, rho2++rho, gamma) ---- k' ?
+ (k,rho,gamma) = tenv
+
+ chB tenv@(k,rho,gamma) ps ty = case ps of
+ p:ps2 -> do
+ typ <- whnf ty
+ case typ of
+ 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)
+ ((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
+ return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
+ _ -> Bad (render (text "Product expected for definiens" <+> ppTerm Unqualified 0 t <+> text "instead of" <+> ppValue Unqualified 0 typ))
+ [] -> do
+ (e,cs) <- checkExp th tenv t ty
+ return (([],e),cs)
+ checkP env@(k,rho,gamma) t x a = do
+ (delta,cs) <- checkPatt th env t a
+ let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
+ return (VClos sigma t, sigma, delta, cs)
+
+ ps2ts k = foldr p2t ([],0,[],k)
+ p2t p (ps,i,g,k) = case p of
+ PW -> (Meta i : ps, i+1,g,k)
+ PV x -> (Vr x : ps, i, upd x k g,k+1)
+ PString s -> (K s : ps, i, g, k)
+ PInt n -> (EInt n : ps, i, g, k)
+ PFloat n -> (EFloat n : ps, i, g, k)
+ PP m c xs -> (mkApp (Q m c) xss : ps, j, g',k')
+ where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
+ _ -> error $ render (text "undefined p2t case" <+> ppPatt Unqualified 0 p <+> text "in checkBranch")
+
+ upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
+
+
+checkPatt :: Theory -> TCEnv -> Exp -> Val -> Err (Binds,[(Val,Val)])
+checkPatt th tenv exp val = do
+ (aexp,_,cs) <- checkExpP tenv exp val
+ let binds = extrBinds aexp
+ return (binds,cs)
+ where
+ extrBinds aexp = case aexp of
+ AVr i v -> [(i,v)]
+ AApp f a _ -> extrBinds f ++ extrBinds a
+ _ -> [] -- no other cases are possible
+
+--- ad hoc, to find types of variables
+ checkExpP tenv@(k,rho,gamma) exp val = case exp of
+ Meta m -> return $ (AMeta m val, val, [])
+ Vr x -> return $ (AVr x val, val, [])
+ EInt i -> return (AInt i, valAbsInt, [])
+ EFloat i -> return (AFloat i, valAbsFloat, [])
+ K s -> return (AStr s, valAbsString, [])
+
+ Q m c -> do
+ typ <- lookupConst th (m,c)
+ return $ (ACn (m,c) typ, typ, [])
+ QC m c -> do
+ typ <- lookupConst th (m,c)
+ return $ (ACn (m,c) typ, typ, []) ----
+ App f t -> do
+ (f',w,csf) <- checkExpP tenv f val
+ typ <- whnf w
+ case typ of
+ 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)
+ _ -> Bad (render (text "Prod expected for function" <+> ppTerm Unqualified 0 f <+> text "instead of" <+> ppValue Unqualified 0 typ))
+ _ -> Bad (render (text "cannot typecheck pattern" <+> ppTerm Unqualified 0 exp))
+
+-- auxiliaries
+
+noConstr :: Err Val -> Err (Val,[(Val,Val)])
+noConstr er = er >>= (\v -> return (v,[]))
+
+mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
+mkAnnot a ti = do
+ (v,cs) <- ti
+ return (a v, v, cs)
+
diff --git a/src/compiler/GF/Compile/Abstract/TypeCheck.hs b/src/compiler/GF/Compile/Abstract/TypeCheck.hs
new file mode 100644
index 000000000..2632c54dd
--- /dev/null
+++ b/src/compiler/GF/Compile/Abstract/TypeCheck.hs
@@ -0,0 +1,83 @@
+----------------------------------------------------------------------
+-- |
+-- Module : TypeCheck
+-- Maintainer : AR
+-- Stability : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/09/15 16:22:02 $
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.16 $
+--
+-- (Description of the module)
+-----------------------------------------------------------------------------
+
+module GF.Compile.Abstract.TypeCheck (-- * top-level type checking functions; TC should not be called directly.
+ checkContext,
+ checkTyp,
+ checkDef,
+ checkConstrs,
+ ) where
+
+import GF.Data.Operations
+
+import GF.Infra.CheckM
+import GF.Grammar
+import GF.Grammar.Lookup
+import GF.Grammar.Unify
+import GF.Compile.Refresh
+import GF.Compile.Abstract.Compute
+import GF.Compile.Abstract.TC
+
+import Text.PrettyPrint
+import Control.Monad (foldM, liftM, liftM2)
+
+-- | invariant way of creating TCEnv from context
+initTCEnv gamma =
+ (length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma)
+
+-- interface to TC type checker
+
+type2val :: Type -> Val
+type2val = VClos []
+
+cont2exp :: Context -> Exp
+cont2exp c = mkProd c eType [] -- to check a context
+
+cont2val :: Context -> Val
+cont2val = type2val . cont2exp
+
+-- some top-level batch-mode checkers for the compiler
+
+justTypeCheck :: SourceGrammar -> Exp -> Val -> Err Constraints
+justTypeCheck gr e v = do
+ (_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
+ (constrs1,_) <- unifyVal constrs0
+ return $ filter notJustMeta constrs1
+
+notJustMeta (c,k) = case (c,k) of
+ (VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
+ _ -> True
+
+grammar2theory :: SourceGrammar -> Theory
+grammar2theory gr (m,f) = case lookupFunType gr m f of
+ Ok t -> return $ type2val t
+ Bad s -> case lookupCatContext gr m f of
+ Ok cont -> return $ cont2val cont
+ _ -> Bad s
+
+checkContext :: SourceGrammar -> Context -> [Message]
+checkContext st = checkTyp st . cont2exp
+
+checkTyp :: SourceGrammar -> Type -> [Message]
+checkTyp gr typ = err (\x -> [text x]) ppConstrs $ justTypeCheck gr typ vType
+
+checkDef :: SourceGrammar -> Fun -> Type -> [Equation] -> [Message]
+checkDef gr (m,fun) typ eqs = err (\x -> [text x]) ppConstrs $ do
+ bcs <- mapM (\b -> checkBranch (grammar2theory gr) (initTCEnv []) b (type2val typ)) eqs
+ let (bs,css) = unzip bcs
+ (constrs,_) <- unifyVal (concat css)
+ return $ filter notJustMeta constrs
+
+checkConstrs :: SourceGrammar -> Cat -> [Ident] -> [String]
+checkConstrs gr cat _ = [] ---- check constructors!