Expr.hs

   1 {-# LANGUAGE PatternGuards, DeriveDataTypeable   #-}
   2 module Expr where
   3
   4 import Data.List
   5 import Data.Maybe
   6 import ParseType
   7
   8 -- import Debug.Trace
   9
  10 import Data.Generics hiding (typeOf)
  11 import Data.Generics.Schemes
  12
  13 data TypedExpr = TypedExpr
  14         { unTypeExpr    :: Expr
  15         , typeOf        :: Typ
  16         } deriving (Eq, Typeable, Data)
  17
  18 typedLeft, typedRight :: Expr -> Typ -> TypedExpr
  19 typedLeft  e t = TypedExpr e (instType False t)
  20 typedRight e t = TypedExpr e (instType True t)
  21
  22 data Expr
  23         = Var String
  24         | App Expr Expr
  25         | Conc [Expr] -- Conc [] is Id
  26         | Lambda TypedExpr Expr
  27         | Pair Expr Expr
  28         | Map
  29             deriving (Eq, Typeable, Data)
  30
  31 data BoolExpr
  32         = Equal Expr Expr
  33         | And [BoolExpr] -- And [] is True
  34         | AllZipWith TypedExpr TypedExpr BoolExpr Expr Expr
  35         | Condition [TypedExpr] BoolExpr BoolExpr
  36         | UnpackPair TypedExpr TypedExpr TypedExpr BoolExpr
  37         | TypeVarInst Int BoolExpr
  38             deriving (Eq, Typeable, Data)
  39
  40 -- Smart constructors
  41
  42 -- | Try eta reduction
  43 equal :: TypedExpr -> TypedExpr -> BoolExpr
  44 equal te1 te2 | typeOf te1 /= typeOf te2 = error "Type mismatch in equal"
  45               | otherwise                = equal' (unTypeExpr te1) (unTypeExpr te2)
  46
  47 equal' :: Expr -> Expr -> BoolExpr
  48 equal' e1 e2  | (Just (lf,lv)) <- isFunctionApplication e1
  49               , (Just (rf,rv)) <- isFunctionApplication e2
  50               , lv == rv
  51                                          = equal' lf rf
  52               -- This makes it return True...
  53               | e1 == e2                 = beTrue
  54               | otherwise                = Equal e1 e2
  55
  56 -- | If e is of the type (app f1 (app f2 .. (app fn x)..)),
  57 --   return Just (f1 . f2. ... . fn, x)
  58 isFunctionApplication :: Expr -> Maybe (Expr, Expr)
  59 isFunctionApplication (App f e') | (Just (inner,v)) <- isFunctionApplication e'
  60                                  = Just (conc f inner, v)
  61                                  | otherwise
  62                                  = Just (f, e')
  63 isFunctionApplication _          = Nothing
  64
  65
  66 -- | If both bound variables are just functions, we can replace this
  67 --   by a comparison
  68 unpackPair :: TypedExpr -> TypedExpr -> TypedExpr -> BoolExpr -> BoolExpr
  69 unpackPair v1 v2 te be | Just subst1 <- findReplacer v1 be
  70                        , Just subst2 <- findReplacer v2 be
  71                        = subst1. subst2 $ (pair v1 v2 `equal` te) `aand` be
  72
  73 -- | If the whole tuple is a function, we can replace this
  74 --   by a comparison
  75 unpackPair v1 v2 te be | Just subst <- findReplacer (pair v1 v2) be
  76                        = subst $ (pair v1 v2 `equal` te) `aand` be
  77
  78 -- | Nothing to optimize
  79 unpackPair v1 v2 te be = UnpackPair v1 v2 te be
  80
  81 pair :: TypedExpr -> TypedExpr -> TypedExpr
  82 pair (TypedExpr e1 t1) (TypedExpr e2 t2) = TypedExpr (Pair e1 e2) (TPair t1 t2)
  83
  84 allZipWith :: TypedExpr -> TypedExpr -> BoolExpr -> TypedExpr -> TypedExpr -> BoolExpr
  85 allZipWith v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
  86                                 e1 `equal` amap (lambda v2 v1') e2
  87                            | Just v2' <- defFor v2 rel =
  88                                 amap (lambda v1 v2') e1 `equal` e2
  89                            | otherwise =
  90                                 AllZipWith v1 v2 rel (unTypeExpr e1) (unTypeExpr e2)
  91
  92 amap :: TypedExpr -> TypedExpr -> TypedExpr
  93 amap tf tl | Arrow t1 t2 <- typeOf tf
  94            , List t      <- typeOf tl
  95            , t1 == t
  96            = let tMap = TypedExpr Map (Arrow (Arrow t1 t2) (Arrow (List t1) (List t2)))
  97              in app (app tMap tf) tl
  98 amap _ _   | otherwise = error "Type error in map"
  99
 100 aand :: BoolExpr -> BoolExpr -> BoolExpr
 101 aand (And xs) (And ys) = And (xs  ++ ys)
 102 aand (And xs) y        = And (xs  ++ [y])
 103 aand x        (And ys) = And ([x] ++ ys)
 104 aand x        y        = And ([x,y])
 105
 106 beTrue :: BoolExpr
 107 beTrue = And []
 108
 109 -- | Optimize a forall condition
 110 condition :: [TypedExpr] -> BoolExpr -> BoolExpr -> BoolExpr
 111 -- empty condition
 112 condition [] cond concl   | cond == beTrue
 113                           = concl
 114 -- float out conditions on the right
 115 condition vars cond (Condition vars' cond' concl')
 116                           = condition (vars ++ vars') (cond `aand` cond') concl'
 117
 118 -- Try to find variables that are functions of other variables, and remove them
 119 condition vars cond concl | True -- set to false to disable
 120                           , ((vars',cond',concl'):_) <- mapMaybe try vars
 121                           = condition vars' cond' concl'
 122               -- A variable which can be replaced
 123   where try v | Just subst <- findReplacer v cond
 124               = -- trace ("Tested " ++ show v ++ ", can be replaced") $
 125                 Just (delete v vars, subst cond, subst concl)
 126
 127               -- A variable with can be removed
 128               | not (unTypeExpr v `occursIn` cond || unTypeExpr v `occursIn` concl)
 129               = -- trace ("Tested " ++ show v ++ ", can be reased") $
 130                 Just (delete v vars, cond, concl)
 131
 132               -- Nothing to do with this variable
 133               | otherwise
 134               = -- trace ("Tested " ++ show v ++ " without success") $
 135                 Nothing
 136
 137 -- Nothing left to optizmize
 138 condition vars cond concl = Condition vars cond concl
 139
 140 -- | Replaces a Term in a BoolExpr
 141 replaceTermBE :: Expr -> Expr -> BoolExpr -> BoolExpr
 142 replaceTermBE d r = go
 143   where go (e1 `Equal` e2) | d == e1 && r == e2 = beTrue
 144                            | d == e2 && r == e1 = beTrue
 145                            | otherwise          = go' e1 `equal'` go' e2
 146         go (And es)        = foldr aand beTrue (map go es)
 147         go (AllZipWith v1 v2 be e1 e2)
 148                            = AllZipWith v1 v2 (go be) (go' e1) (go' e2)
 149         go (Condition vs cond concl)
 150                            = condition vs (go cond) (go concl)
 151         go (UnpackPair v1 v2 e be)
 152                            = unpackPair v1 v2 (go' e) (go be)
 153         go (TypeVarInst _ _) = error "TypeVarInst not expected here"
 154         go' :: Data a => a -> a
 155         go' = replaceExpr d r
 156
 157 replaceExpr :: Data a => Expr -> Expr -> a -> a
 158 replaceExpr d r = everywhere (mkT go)
 159   where go e | e == d    = r
 160              | otherwise = e
 161
 162 -- | Is inside the term a definition for the variable?
 163 findReplacer :: TypedExpr -> BoolExpr -> Maybe (BoolExpr -> BoolExpr)
 164 findReplacer tv be = findReplacer' (unTypeExpr tv) be
 165
 166 -- | Find a definition, and return a substitution
 167 findReplacer' :: Expr -> BoolExpr -> Maybe (BoolExpr -> BoolExpr)
 168 -- For combined types, look up the components
 169 findReplacer' (Pair x y) e | Just (delX) <- findReplacer' x e
 170                            , Just (delY) <- findReplacer' y e
 171                     = Just (delX . delY)
 172 -- Find the definition
 173 findReplacer' e (e1 `Equal` e2) | e == e1    = Just (replaceTermBE e e2)
 174                                 | e == e2    = Just (replaceTermBE e e1)
 175 findReplacer' e (And es)        = listToMaybe (mapMaybe (findReplacer' e) es)
 176                                   -- assuming no two definitions can exist
 177 findReplacer' _ _               = Nothing
 178
 179 -- | Is inside the term a definition for the variable?
 180 defFor :: TypedExpr -> BoolExpr -> Maybe (TypedExpr)
 181 defFor tv be | Just (e') <- defFor' (unTypeExpr tv) be
 182                          = Just (TypedExpr e' (typeOf tv))
 183              | otherwise = Nothing
 184
 185 -- | Find a definition, and return it along the definition remover
 186 defFor' :: Expr -> BoolExpr -> Maybe (Expr)
 187 defFor' e (e1 `Equal` e2) | e == e1                 = Just (e2)
 188                           | e == e2                 = Just (e1)
 189 defFor' e (And es)        | [d]  <- mapMaybe (defFor' e) es -- exactly one definition
 190                                                     = Just d
 191 defFor' _ _                                         = Nothing
 192
 193 app :: TypedExpr -> TypedExpr -> TypedExpr
 194 app te1 te2 | Arrow t1 t2 <- typeOf te1
 195             , t3          <- typeOf te2
 196             , t1 == t3
 197             = TypedExpr (app' (unTypeExpr te1) (unTypeExpr te2)) t2
 198  where app' Map (Conc []) = Conc []   -- map id = id
 199        app' (Conc []) v   = v         -- id x   = x
 200        app' f v           = App f v
 201 app te1 te2 | otherwise                          = error $ "Type mismatch in app: " ++
 202                                                            show te1 ++ " " ++ show te2
 203
 204 lambda :: TypedExpr -> TypedExpr -> TypedExpr
 205 lambda tv e = TypedExpr inner (Arrow (typeOf tv) (typeOf e))
 206   where inner | (Just e') <- isApplOn (unTypeExpr tv) (unTypeExpr e)
 207               , not (unTypeExpr tv `occursIn` e')
 208                           = e'
 209               | tv == e   = Conc []
 210               | otherwise = Lambda tv (unTypeExpr e)
 211
 212 conc :: Expr -> Expr -> Expr
 213 conc (Conc xs) (Conc ys) = Conc (xs  ++ ys)
 214 conc (Conc xs)  y        = Conc (xs  ++ [y])
 215 conc x         (Conc ys) = Conc ([x] ++ ys)
 216 conc x          y        = Conc ([x,y])
 217
 218 -- Helpers
 219
 220 isApplOn :: Expr -> Expr -> Maybe Expr
 221 isApplOn e e'         | e == e'                       = Nothing
 222 isApplOn e (App f e') | e == e'                       = Just (Conc [f])
 223 isApplOn e (App f e') | (Just inner) <- isApplOn e e' = Just (conc f inner)
 224 isApplOn _ _                                          = Nothing
 225
 226 hasVar :: String -> Expr -> Bool
 227 hasVar v (Var v')     = v == v'
 228 hasVar v (App e1 e2)  = hasVar v e1 || hasVar v e2
 229 hasVar v (Conc es)    = any (hasVar v) es
 230 hasVar v (Lambda _ e) = hasVar v e
 231 hasVar v (Pair e1 e2) = hasVar v e1 || hasVar v e2
 232 hasVar _ Map          = False
 233
 234 occursIn :: (Typeable a, Data a1, Eq a) => a -> a1 -> Bool
 235 e `occursIn` e'       = not (null (listify (==e) e'))
 236
 237 isTuple :: Typ -> Bool
 238 isTuple (TPair _ _) = True
 239 isTuple _           = False
 240
 241
 242 -- showing
 243
 244 -- Precedences:
 245 -- 10 fun app
 246 --  9 (.)
 247 --  8 ==
 248 --  7 ==>
 249 --  6 forall
 250
 251 instance Show Expr where
 252         showsPrec _ (Var s)     = showString s
 253         showsPrec d (App e1 e2) = showParen (d>10) $
 254                 showsPrec 10 e1 . showChar ' ' . showsPrec 11 e2
 255         showsPrec _ (Conc [])   = showString "id"
 256         showsPrec d (Conc [e])  = showsPrec d e
 257         showsPrec d (Conc es)   = showParen (d>9) $
 258                 showIntercalate (showString " . ") (map (showsPrec 10) es)
 259         showsPrec _ (Lambda tv e) = showParen True $
 260                                     showString "\\" .
 261                                     showsPrec 0 tv .
 262                                     showString " -> ".
 263                                     showsPrec 0 e
 264         showsPrec _ (Pair e1 e2) = showParen True $
 265                                    showsPrec 0 e1 .
 266                                    showString "," .
 267                                    showsPrec 0 e2
 268         showsPrec _ Map           = showString "map"
 269
 270 showIntercalate :: ShowS -> [ShowS] -> ShowS
 271 showIntercalate _ []  = id
 272 showIntercalate _ [x] = x
 273 showIntercalate i (x:xs) = x . i . showIntercalate i xs
 274
 275 instance Show TypedExpr where
 276         showsPrec d (TypedExpr e t) =
 277                 showParen (d>10) $
 278                         showsPrec 0 e .
 279                         showString " :: " .
 280                         showString (showTypePrec 0 t)
 281
 282 instance Show BoolExpr where
 283         show (Equal e1 e2) = showsPrec 9 e1 $
 284                              showString " == " $
 285                              showsPrec 9 e2 ""
 286         show (And [])      = "True"
 287         show (And bes)     = intercalate " && " $ map show bes
 288         show (AllZipWith v1 v2 be e1 e2) =
 289                         "allZipWith " ++
 290                         "( " ++
 291                         "\\" ++
 292                         showsPrec 11 v1 "" ++
 293                         " " ++
 294                         showsPrec 11 v2 "" ++
 295                         " -> " ++
 296                         show be ++
 297                         ")" ++
 298                         " " ++
 299                         showsPrec 11 e1 "" ++
 300                         " " ++
 301                         showsPrec 11 e2 ""
 302         show (Condition tvars be1 be2) =
 303                         "forall " ++
 304                         intercalate ", " (map show tvars) ++
 305                         ".\n" ++
 306                         (if be1 /= beTrue then indent 2 (show be1) ++ "==>\n" else "") ++
 307                         indent 2 (show be2)
 308         show (UnpackPair v1 v2 e be) =
 309                         "let (" ++
 310                         showsPrec 0 v1 "" ++
 311                         "," ++
 312                         showsPrec 0 v2 "" ++
 313                         ") = " ++
 314                         showsPrec 0 e "" ++
 315                         " in\n" ++
 316                         indent 2 (show be)
 317         show (TypeVarInst i be) =
 318                         "forall types t" ++
 319                         show (2*i-1) ++
 320                         ", t" ++
 321                         show (2*i) ++
 322                         ", function g" ++
 323                         show i ++
 324                         " :: t" ++
 325                         show (2*i-1) ++
 326                         " -> t" ++
 327                         show (2*i) ++
 328                         ".\n" ++
 329                         indent 2 (show be)
 330
 331 indent :: Int -> String -> String
 332 indent n = unlines . map (replicate n ' ' ++) . lines
 333
 334 showTypePrec :: Int -> Typ -> String
 335 showTypePrec _ Int                          = "Int"
 336 showTypePrec _ (TVar (TypVar i))            = "a"++show i
 337 showTypePrec _ (TVar (TypInst i b)) | not b = "t" ++  show (2*i-1)
 338                                     |     b = "t" ++  show (2*i)
 339 showTypePrec d (Arrow t1 t2)                = paren (d>9) $
 340                                                 showTypePrec 10 t1 ++
 341                                                 " -> " ++
 342                                                 showTypePrec 9 t2
 343 showTypePrec _ (List t)                     = "[" ++ showTypePrec 0 t ++ "]"
 344 showTypePrec _ (TEither t1 t2)              = "Either " ++ showTypePrec 11 t1 ++
 345                                                     " " ++ showTypePrec 11 t2
 346 showTypePrec _ (TPair t1 t2)                = "(" ++ showTypePrec 0 t1 ++
 347                                               "," ++ showTypePrec 0 t2 ++ ")"
 348
 349 paren :: Bool -> String -> String
 350 paren b p   =  if b then "(" ++ p ++ ")" else p