Initial check in
authorJoachim Breitner <mail@joachim-breitner.de>
Mon, 13 Oct 2008 14:59:41 +0000 (14:59 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Mon, 13 Oct 2008 14:59:41 +0000 (14:59 +0000)
Expr.hs [new file with mode: 0644]
ParseType.hs [new file with mode: 0644]
SimpleFT.hs [new file with mode: 0644]

diff --git a/Expr.hs b/Expr.hs
new file mode 100644 (file)
index 0000000..0c44f7a
--- /dev/null
+++ b/Expr.hs
@@ -0,0 +1,123 @@
+{-# LANGUAGE PatternGuards  #-}
+module Expr where
+
+import Data.List
+
+data Expr
+       = Var String
+       | App Expr Expr
+       | Conc [Expr]
+       | Lambda String Expr
+       | Map
+            deriving (Eq)
+
+data BoolExpr 
+       = Equal Expr Expr
+       | Pairwise String String BoolExpr Expr Expr
+       | Condition String String BoolExpr BoolExpr
+       | UnCond String BoolExpr
+       | TypeVarInst Int BoolExpr
+            deriving (Eq)
+
+-- Smart constructors
+
+unCond v (Equal l r) | (Just l') <- isApplOn v l 
+                    , (Just r') <- isApplOn v r = 
+       if hasVar v l' || hasVar v r'
+       then UnCond v (Equal l' r')
+       else (Equal l' r')
+unCond v e = UnCond v e
+
+lambda v e | (Just e') <- isApplOn v e, not (hasVar v e') = e'
+           | otherwise                                    = Lambda v e
+
+
+conc f (Conc fs) = Conc (f:fs)
+
+-- Helpers
+
+isApplOn v (Var _)                                         = Nothing
+isApplOn v (App f (Var v')) | v == v'                      = Just (Conc [f])
+isApplOn v (App f e)        | (Just inner) <- isApplOn v e = Just (conc f inner)
+isApplOn _ _                                               = Nothing
+
+hasVar v (Var v')     = v == v'
+hasVar v (App e1 e2)  = hasVar v e1 && hasVar v e2
+hasVar v (Conc es)    = any (hasVar v) es
+
+
+-- showing
+
+-- Precedences:
+-- 10 fun app
+--  9 (.)
+--  8 ==
+--  7 ==>
+--  6 forall
+
+instance Show Expr where
+       showsPrec d (Var s)     = showString s
+       showsPrec d (App e1 e2) = showParen (d>10) $
+               showsPrec 10 e1 . showChar ' ' . showsPrec 11 e2
+       showsPrec d (Conc es)   = showParen (d>9) $
+               showIntercalate (showString " . ") (map (showsPrec 10) es)
+       showsPrec d (Lambda v e) = showParen True $ 
+                                  showString "\\" .
+                                   showString v .
+                                   showString " -> ".
+                                  showsPrec 0 e 
+       showsPrec _ Map           = showString "map"
+
+showIntercalate i []  = id
+showIntercalate i [x] = x
+showIntercalate i (x:xs) = x . i . showIntercalate i xs
+
+instance Show BoolExpr where
+       showsPrec d (Equal e1 e2) = showParen (d>8) $
+                                   showsPrec 9 e1 .
+                                   showString " == " .
+                                   showsPrec 9 e2 
+       showsPrec d (Pairwise v1 v2 be e1 e2) =
+                       showParen (d>10) $
+                       showString "allZipWith " .
+                       showParen True ( 
+                               showString "(\\" .
+                               showString v1 .
+                               showChar ' ' .
+                               showString v2 . 
+                               showString " -> " .
+                               showsPrec 0 e1
+                       ) .
+                       showChar ' ' .
+                       showsPrec 11 e2
+       showsPrec d (Condition v1 v2 be1 be2) = 
+                       showParen (d>6) $
+                       showString "forall " . 
+                       showString v1 . 
+                       showChar ' ' .
+                       showString v2 . 
+                       showString ". " .
+                       showsPrec 9 be1 .
+                       showString " ==> " .
+                       showsPrec 6 be2
+       showsPrec d (UnCond v1 be1) = 
+                       showParen (d>6) $
+                       showString "forall " . 
+                       showString v1 . 
+                       showString ". " .
+                       showsPrec 6 be1
+       showsPrec d (TypeVarInst i be) = 
+                       showParen (d>6) $
+                       showString "forall types t" .
+                       shows (2*i-1) .
+                       showString ", t" .
+                       shows (2*i) . 
+                       showString ", function g" .
+                       shows i .
+                       showString " :: t" .
+                       shows (2*i-1) .
+                       showString " -> t" .
+                       shows (2*i) . 
+                       showString ".\n" .
+                       showsPrec 6 be
+
diff --git a/ParseType.hs b/ParseType.hs
new file mode 100644 (file)
index 0000000..824ffbd
--- /dev/null
@@ -0,0 +1,82 @@
+{-# LANGUAGE FlexibleContexts, PatternSignatures, DeriveDataTypeable #-}
+module ParseType (
+         parseType
+       , TypVar(..)
+       , Typ(..)
+       ) where
+
+import Language.Haskell.Parser (parseModule, ParseResult(..))
+import Language.Haskell.Syntax
+
+import Control.Monad
+import Control.Monad.Error
+import Control.Monad.Reader
+import Data.List
+import qualified Data.Map as M
+
+import Data.Generics
+import Data.Generics.Schemes
+import Data.Char
+
+newtype TypVar = TypVar Int deriving (Show, Eq, Typeable, Data)
+
+data Typ    = TVar    TypVar
+            | Arrow   Typ     Typ
+            | All     TypVar  Typ       --wir geben Typen ohne Quantifier an
+            | AllStar TypVar  Typ
+            | List    Typ
+            --Extensions
+            | Int
+            | TPair    Typ     Typ
+            | TEither  Typ     Typ
+            deriving (Show, Eq, Typeable, Data)
+
+parseType = either error id . parseType'
+
+-- | A simple type parser.
+--
+-- >  parseType "Int -> [Either a b] -> (a,b)" :: Either String Typ
+--
+--  Right (All (TypVar 3) (All (TypVar 4) (Arrow Int (Arrow (List (TEither (TVar (TypVar 3)) (TVar (TypVar 4)))) (TPair (TVar (TypVar 3)) (TVar (TypVar 4)))))))
+--
+parseType' :: (MonadError String t) => String -> t Typ
+parseType' s = case parseModule ("x :: " ++ s) of
+  ParseOk hsModule -> do
+                       hstype <- extractTheOneType hsModule
+                       let varmap = createVarMap hstype
+                       typ <- runReaderT (simplifiyType hstype) varmap
+                       return (quantify typ)
+  ParseFailed l _  -> do throwError ("Parse error at (" ++ show (srcLine l) ++ ":" ++ show (srcColumn l) ++ ").")
+
+extractTheOneType :: (MonadError String m) => HsModule -> m HsType
+extractTheOneType (HsModule _ _ _ _ [HsTypeSig _ _ (HsQualType [] t)]) = return t
+extractTheOneType _  = throwError "parseModule gave unexpected result"
+
+createVarMap :: HsType -> M.Map HsName TypVar
+createVarMap hstype = M.fromList $ zip
+                       (nub (listify isVar hstype))
+                       (map TypVar [1..])
+  where isVar (HsIdent (x:xs)) | isLower x  = True
+        isVar _                            =  False
+
+
+simplifiyType :: (MonadReader (M.Map HsName TypVar) m, MonadError String m) =>
+                 HsType -> m Typ
+simplifiyType (HsTyFun t1 t2)
+                               = liftM2 Arrow (simplifiyType t1) (simplifiyType t2)
+simplifiyType (HsTyTuple [t1,t2])
+                               = liftM2 TPair (simplifiyType t1) (simplifiyType t2)
+simplifiyType (HsTyTuple _)    = throwError "Tuple with more than one type not supported."
+simplifiyType (HsTyVar name)    = do Just tv <- asks (M.lookup name)
+                                     return (TVar tv)
+simplifiyType (HsTyCon (UnQual (HsIdent "Int")))
+                               = return Int
+simplifiyType (HsTyApp (HsTyApp (HsTyCon (UnQual (HsIdent "Either"))) t1) t2)
+                               = liftM2 TEither (simplifiyType t1) (simplifiyType t2)
+simplifiyType (HsTyApp (HsTyCon (Special HsListCon)) t)
+                               = liftM  List (simplifiyType t)
+simplifiyType t
+                               = throwError ("Unsupported type " ++ show t)
+
+quantify :: Typ -> Typ
+quantify t = foldr All t (nub (listify (\(_::TypVar) -> True) t))
diff --git a/SimpleFT.hs b/SimpleFT.hs
new file mode 100644 (file)
index 0000000..9589bcf
--- /dev/null
@@ -0,0 +1,47 @@
+{-# LANGUAGE PatternGuards  #-}
+
+module SimpleFT where
+
+import ParseType
+import Expr
+import Control.Monad.Reader
+
+test = putStrLn . show . freeTheorem . parseType
+
+freeTheorem t = runReader (freeTheorem' (Var "f") (Var "f") t) freeVars
+
+freeVars = (map (:"") ['a'..])
+
+
+freeTheorem' :: Expr -> Expr -> Typ -> Reader [String] BoolExpr
+
+freeTheorem' e1 e2 Int = return $
+       Equal e1 e2
+
+freeTheorem' e1 e2 (List t) = do
+       [v1,v2] <- asks (take 2)
+       local (drop 2) $ do
+               map <- freeTheorem' (Var v1) (Var v2) t
+               case map of
+                 (Equal (Var v1') ev1) | v1' == v1 -> do
+                       return $ Equal e1 (App (App (Var "map") (lambda v2 ev1)) e2)
+                 _ -> do
+                       return $ Pairwise v1 v2 map e1 e2
+
+freeTheorem' e1 e2 (Arrow t1 t2) = do
+       [v1,v2] <- asks (take 2)
+       local (drop 2) $ do
+               cond  <- freeTheorem' (Var v1) (Var v2) t1
+               case cond of
+                 (Equal (Var v1') ev1) | v1' == v1 -> do
+                       concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
+                       return $ unCond v2 concl
+                 _ -> do
+                       concl <- freeTheorem' (App e1 (Var v1)) (App e2 (Var v2)) t2
+                       return $ Condition v1 v2 cond concl
+
+freeTheorem' e1 e2 (TVar (TypVar i)) = return $
+       Equal e1 (App (Var ("g"++show i)) e2)
+
+freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
+freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t