diff options
Diffstat (limited to 'src/compiler/GF/Compile/Abstract')
| -rw-r--r-- | src/compiler/GF/Compile/Abstract/Compute.hs | 138 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/Abstract/TC.hs | 297 | ||||
| -rw-r--r-- | src/compiler/GF/Compile/Abstract/TypeCheck.hs | 82 |
3 files changed, 0 insertions, 517 deletions
diff --git a/src/compiler/GF/Compile/Abstract/Compute.hs b/src/compiler/GF/Compile/Abstract/Compute.hs deleted file mode 100644 index 3ca9fe432..000000000 --- a/src/compiler/GF/Compile/Abstract/Compute.hs +++ /dev/null @@ -1,138 +0,0 @@ ----------------------------------------------------------------------- --- | --- 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 deleted file mode 100644 index 68b1691ec..000000000 --- a/src/compiler/GF/Compile/Abstract/TC.hs +++ /dev/null @@ -1,297 +0,0 @@ ----------------------------------------------------------------------- --- | --- 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 Int - | 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 c -> return $ VCn c - QC c -> return $ VCn 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 c -> mkAnnot (ACn c) $ noConstr $ lookupConst th 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) - PAs x p -> p2t p (ps,i,g,k) - 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 c xs -> (mkApp (Q c) xss : ps, j, g',k') - where (xss,j,g',k') = foldr p2t ([],i,g,k) xs - PImplArg p -> p2t p (ps,i,g,k) - PTilde t -> (t : ps, i, g, k) - _ -> 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 c -> do - typ <- lookupConst th c - return $ (ACn c typ, typ, []) - QC c -> do - typ <- lookupConst th c - return $ (ACn 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 deleted file mode 100644 index 74804983d..000000000 --- a/src/compiler/GF/Compile/Abstract/TypeCheck.hs +++ /dev/null @@ -1,82 +0,0 @@ ----------------------------------------------------------------------- --- | --- 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 eq = err (\x -> [text x]) ppConstrs $ do - (b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2val typ) - (constrs,_) <- unifyVal cs - return $ filter notJustMeta constrs - -checkConstrs :: SourceGrammar -> Cat -> [Ident] -> [String] -checkConstrs gr cat _ = [] ---- check constructors! |