summaryrefslogtreecommitdiff
path: root/src/GF/Compile
diff options
context:
space:
mode:
authorkrasimir <krasimir@chalmers.se>2009-03-15 17:59:49 +0000
committerkrasimir <krasimir@chalmers.se>2009-03-15 17:59:49 +0000
commit3ac05b4f613a037265b14c381305fd859cc13263 (patch)
treec850a673d53ed7f40ef292beaa4da4e9b3da4198 /src/GF/Compile
parent3afe18dc576bbb71b124126ebdf2a9155fe1fb8d (diff)
some more refactoring
Diffstat (limited to 'src/GF/Compile')
-rw-r--r--src/GF/Compile/TC.hs41
1 files changed, 1 insertions, 40 deletions
diff --git a/src/GF/Compile/TC.hs b/src/GF/Compile/TC.hs
index f6e15b175..4eb078109 100644
--- a/src/GF/Compile/TC.hs
+++ b/src/GF/Compile/TC.hs
@@ -16,7 +16,6 @@ module GF.Compile.TC (AExp(..),
Theory,
checkExp,
inferExp,
- checkEqs,
eqVal,
whnf
) where
@@ -122,12 +121,11 @@ checkExp th tenv@(k,rho,gamma) e ty = do
return (AAbs x a' t', cs)
_ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
--- {- --- to get deprec when checkEqs works (15/9/2005)
Eqs es -> do
bcs <- mapM (\b -> checkBranch th tenv b typ) es
let (bs,css) = unzip bcs
return (AEqs bs, concat css)
--- - }
+
Prod x a b -> do
testErr (typ == vType) "expected Type"
(a',csa) <- checkType th tenv a
@@ -164,43 +162,6 @@ inferExp th tenv@(k,rho,gamma) e = case e of
_ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
_ -> prtBad "cannot infer type of expression" e
-checkEqs :: Theory -> TCEnv -> (Fun,Term) -> Val -> Err [(Val,Val)]
-checkEqs th tenv@(k,rho,gamma) (fun@(m,f),def) val = case def of
- Eqs es -> liftM concat $ mapM checkBranch es
- _ -> liftM snd $ checkExp th tenv def val
- where
- checkBranch (ps,df) =
- let
- (ps',_,vars) = foldr p2t ([],0,[]) ps
- fps = mkApp (Q m f) ps'
- in errIn ("branch" +++ prt fps) $ do
- (aexp, typ, cs1) <- inferExp th tenv fps
- let
- bds = binds vars aexp
- tenv' = (k, rho, bds ++ gamma)
- (_,cs2) <- errIn (show bds) $ checkExp th tenv' df typ
- return $ (cs1 ++ cs2)
- p2t p (ps,i,g) = case p of
- PW -> (Meta (MetaSymb i) : ps, i+1, g)
- PV IW -> (Meta (MetaSymb i) : ps, i+1, g)
- PV x -> (Meta (MetaSymb i) : ps, i+1,upd x i g)
- PString s -> ( K s : ps, i, g)
- PInt n -> (EInt n : ps, i, g)
- PFloat n -> (EFloat n : ps, i, g)
- PP m c xs -> (mkApp (qq (m,c)) xss : ps, i', g')
- where (xss,i',g') = foldr p2t ([],i,g) xs
- _ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
- upd x i g = (x,i) : g --- to annotate pattern variables: treat as metas
-
- -- notice: in vars, the sequence 0.. is sorted. In subst aexp, all
- -- this occurs and nothing else.
- binds vars aexp = [(x,v) | ((x,_),v) <- zip vars metas] where
- metas = map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ subst aexp
- subst aexp = case aexp of
- AMeta (MetaSymb i) v -> [(i,v)]
- AApp c a _ -> subst c ++ subst a
- _ -> [] -- never matter in patterns
-
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