diff options
Diffstat (limited to 'src/GF/Grammar/TC.hs')
| -rw-r--r-- | src/GF/Grammar/TC.hs | 210 |
1 files changed, 210 insertions, 0 deletions
diff --git a/src/GF/Grammar/TC.hs b/src/GF/Grammar/TC.hs new file mode 100644 index 000000000..ce9da979d --- /dev/null +++ b/src/GF/Grammar/TC.hs @@ -0,0 +1,210 @@ +module TC where + +import Operations +import Abstract +import AbsCompute + +import Monad + +-- Thierry Coquand's type checking algorithm that creates a trace + +data AExp = + AVr Ident Val + | ACn QIdent Val + | AType + | AInt Int + | AStr String + | AMeta MetaSymb Val + | AApp AExp AExp Val + | AAbs Ident Val AExp + | AProd Ident AExp AExp + | AEqs [([Exp],AExp)] --- + deriving (Eq,Show) + +type Theory = QIdent -> Err Val + +lookupConst :: Theory -> QIdent -> Err Val +lookupConst th f = th f + +lookupVar :: Env -> Ident -> Err Val +lookupVar g x = maybe (prtBad "unknown variable" 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) + Sort c -> return $ VType --- the only sort is Type + App f a -> join $ liftM2 app (eval env f) (eval env a) + _ -> 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] + _ -> 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) + _ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ + + 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 + (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b + return (AProd x a' b', csa ++ csb) + + _ -> 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 -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) + Sort _ -> return (AType, vType, []) + 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) + _ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ + _ -> prtBad "cannot infer type of expression" e + +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,_) = ps2ts k ps + tenv' = (k,rho2++rho, gamma) + (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 + _ -> prtBad ("Product expected for definiens" +++prt t +++ "instead of") 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 + PV IW -> (meta (MetaSymb i) : ps, i+1,g,k) + PV x -> (vr x : ps, i, upd x k g,k+1) +---- PL s -> (cn s : ps, i, g, k) + PP m c xs -> (mkApp (qq (m,c)) xss : ps, j, g',k') + where (xss,j,g',k') = foldr p2t ([],i,g,k) xs + _ -> error $ "undefined p2t case" +++ prt p +++ "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, []) + Q 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) + _ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ + _ -> prtBad "cannot typecheck pattern" 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) + |