mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-24 03:52:50 -06:00
some more refactoring
This commit is contained in:
@@ -16,7 +16,6 @@ module GF.Compile.TC (AExp(..),
|
|||||||
Theory,
|
Theory,
|
||||||
checkExp,
|
checkExp,
|
||||||
inferExp,
|
inferExp,
|
||||||
checkEqs,
|
|
||||||
eqVal,
|
eqVal,
|
||||||
whnf
|
whnf
|
||||||
) where
|
) where
|
||||||
@@ -122,12 +121,11 @@ checkExp th tenv@(k,rho,gamma) e ty = do
|
|||||||
return (AAbs x a' t', cs)
|
return (AAbs x a' t', cs)
|
||||||
_ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
|
_ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
|
||||||
|
|
||||||
-- {- --- to get deprec when checkEqs works (15/9/2005)
|
|
||||||
Eqs es -> do
|
Eqs es -> do
|
||||||
bcs <- mapM (\b -> checkBranch th tenv b typ) es
|
bcs <- mapM (\b -> checkBranch th tenv b typ) es
|
||||||
let (bs,css) = unzip bcs
|
let (bs,css) = unzip bcs
|
||||||
return (AEqs bs, concat css)
|
return (AEqs bs, concat css)
|
||||||
-- - }
|
|
||||||
Prod x a b -> do
|
Prod x a b -> do
|
||||||
testErr (typ == vType) "expected Type"
|
testErr (typ == vType) "expected Type"
|
||||||
(a',csa) <- checkType th tenv a
|
(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 ("Prod expected for function" +++ prt f +++ "instead of") typ
|
||||||
_ -> prtBad "cannot infer type of expression" e
|
_ -> 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 :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
|
||||||
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
|
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
|
||||||
chB tenv' ps' ty
|
chB tenv' ps' ty
|
||||||
|
|||||||
Reference in New Issue
Block a user