From: pimjager Date: Thu, 28 Apr 2016 18:39:23 +0000 (+0200) Subject: Started working on algorithm M X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=296f3451766b91f1c6ea0d51ae05e71db011935d;p=cc1516.git Started working on algorithm M --- diff --git a/sem.icl b/sem.icl index 16a426c..8cc3df9 100644 --- a/sem.icl +++ b/sem.icl @@ -99,19 +99,6 @@ where _ = Left $ SanityError p "main has to return Void") isNiceMain _ = pure () -instance toString Scheme where - toString (Forall x t) = - concat ["Forall ": map ((+++) "\n") x] +++ toString t - -instance toString Gamma where - toString mp = - concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp] - -instance toString SemError where - toString (SanityError p e) = concat [toString p, - "SemError: SanityError: ", e] - toString se = "SemError: " - class Typeable a where ftv :: a -> [TVar] subst :: Substitution a -> a @@ -147,8 +134,8 @@ instance Typeable Gamma where instance zero Substitution where zero = 'Map'.newMap compose :: Substitution Substitution -> Substitution -compose s1 s2 = 'Map'.union (Mapmap (subst s1) s2) s1 -//Note: unlike function composition, compose is left biased! +compose s1 s2 = 'Map'.union (Mapmap (subst s2) s1) s2 +//Note: just like function compositon compose does snd first occurs :: TVar a -> Bool | Typeable a occurs tvar a = elem tvar (ftv a) @@ -177,13 +164,19 @@ gamma :: Typing Gamma gamma = gets fst putGamma :: Gamma -> Typing () putGamma g = modify (appFst $ const g) >>| pure () -withGamma :: (Gamma -> Gamma) -> Typing () -withGamma f = modify (appFst f) >>| pure () +changeGamma :: (Gamma -> Gamma) -> Typing () +changeGamma f = modify (appFst f) >>| pure () +withGamma :: (Gamma -> a) -> Typing a +withGamma f = f <$> gamma fresh :: Typing Type fresh = gets snd >>= \vars-> modify (appSnd $ const $ tail vars) >>| pure (IdType (head vars)) +lift :: (Either SemError a) -> Typing a +lift (Left e) = liftT $ Left e +lift (Right v) = pure v + //instantiate maps a schemes type variables to variables with fresh names //and drops the quantification: i.e. forall a,b.a->[b] becomes c->[d] instantiate :: Scheme -> Typing Type @@ -191,13 +184,67 @@ instantiate (Forall bound t) = mapM (const fresh) bound >>= \newVars-> let s = 'Map'.fromList (zip (bound,newVars)) in pure (subst s t) + //generalize quentifies all free type variables in a type which are not //in the gamma generalize :: Type -> Typing Scheme generalize t = gamma >>= \g-> pure $ Forall (difference (ftv t) (ftv g)) t - - +lookup :: String -> Typing Scheme +lookup k = gamma >>= \g-> case 'Map'.member k g of + False = liftT (Left $ UndeclaredVariableError zero k) + True = pure ('Map'.find k g) + +//The inference class +//When tying it all together we will treat the program is a big +//let x=e1 in let y=e2 in .... +class infer a :: a -> Typing (Substitution, Type) + +instance infer Expr where + infer e = case e of + VarExpr _ (VarDef k fs) = (\t->(zero,t)) <$> (lookup k >>= instantiate) + //instantiate is key for the let polymorphism! + + Op2Expr _ e1 op e2 = + infer e1 >>= \(s1, t1) -> + infer e2 >>= \(s2, t2) -> + fresh >>= \tv -> + let given = t1 ->> t2 ->> tv in + op2Type op >>= \expected -> + lift (unify expected given) >>= \s3 -> + pure ((compose s1 $ compose s2 s3), subst s3 tv) + + Op1Expr _ op e1 = + infer e1 >>= \(s1, t1) -> + fresh >>= \tv -> + let given = t1 ->> tv in + op1Type op >>= \expected -> + lift (unify expected given) >>= \s2 -> + pure ((compose s1 s2), subst s2 tv) + + + + IntExpr _ _ = pure $ (zero, IntType) + BoolExpr _ _ = pure $ (zero, BoolType) + CharExpr _ _ = pure $ (zero, CharType) + + +op2Type :: Op2 -> Typing Type +op2Type op +| elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod] + = pure (IntType ->> IntType ->> IntType) +| elem op [BiEquals, BiUnEqual] + = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType) +| elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq] + = pure (IntType ->> IntType ->> BoolType) +| elem op [BiAnd, BiOr] + = pure (BoolType ->> BoolType ->> BoolType) +| op == BiCons + = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1) + +op1Type :: Op1 -> Typing Type +op1Type UnNegation = pure $ (BoolType ->> BoolType) +op1Type UnMinus = pure $ (IntType ->> IntType) Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b) @@ -206,6 +253,22 @@ Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v) (Mapmap f ml) (Mapmap f mr) +instance toString Scheme where + toString (Forall x t) = + concat ["Forall ": map ((+++) "\n") x] +++ toString t + +instance toString Gamma where + toString mp = + concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp] + +instance toString SemError where + toString (SanityError p e) = concat [toString p, + "SemError: SanityError: ", e] + toString se = "SemError: " + +instance MonadTrans (StateT (Gamma, [TVar])) where + liftT m = StateT \s-> m >>= \a-> return (a, s) + //// ------------------------ //// First step: Inference //// ------------------------//