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 EVar = F
  23           | FromTypVar Int
  24           | FromParam Int Bool
  25             deriving (Eq, Typeable, Data)
  26
  27 data Expr
  28         = Var EVar
  29         | TheOneFunc
  30         | App Expr Expr
  31         | Conc [Expr] -- Conc [] is Id
  32         | Lambda TypedExpr Expr
  33         | Pair Expr Expr
  34         | Map
  35         | ConstUnit
  36         | EitherMap
  37         | EUnit
  38             deriving (Eq, Typeable, Data)
  39
  40 data LambdaBE = CurriedEquals Typ
  41               | LambdaBE TypedExpr TypedExpr BoolExpr
  42             deriving (Eq, Typeable, Data)
  43
  44 data BoolExpr
  45         = Equal Expr Expr
  46         | And [BoolExpr] -- And [] is True
  47         | AllZipWith LambdaBE Expr Expr
  48         | AndEither  LambdaBE LambdaBE Expr Expr
  49         | Condition [TypedExpr] BoolExpr BoolExpr
  50         | UnpackPair TypedExpr TypedExpr TypedExpr BoolExpr
  51         | TypeVarInst Bool Int BoolExpr
  52             deriving (Eq, Typeable, Data)
  53
  54 -- Smart constructors
  55
  56 -- | Try eta reduction
  57 equal :: TypedExpr -> TypedExpr -> BoolExpr
  58 equal te1 te2 | typeOf te1 /= typeOf te2 = error "Type mismatch in equal"
  59               | otherwise                = equal' (unTypeExpr te1) (unTypeExpr te2)
  60
  61 equal' :: Expr -> Expr -> BoolExpr
  62 equal' e1 e2  | (Just (lf,lv)) <- isFunctionApplication e1
  63               , (Just (rf,rv)) <- isFunctionApplication e2
  64               , lv == rv
  65                                          = equal' lf rf
  66               -- This makes it return True...
  67               | e1 == e2                 = beTrue
  68               | otherwise                = Equal e1 e2
  69
  70 -- | If e is of the type (app f1 (app f2 .. (app fn x)..)),
  71 --   return Just (f1 . f2. ... . fn, x)
  72 isFunctionApplication :: Expr -> Maybe (Expr, Expr)
  73 isFunctionApplication (App f e') | (Just (inner,v)) <- isFunctionApplication e'
  74                                  = Just (conc f inner, v)
  75                                  | otherwise
  76                                  = Just (f, e')
  77 isFunctionApplication _          = Nothing
  78
  79
  80 -- | If both bound variables are just functions, we can replace this
  81 --   by a comparison
  82 unpackPair :: TypedExpr -> TypedExpr -> TypedExpr -> BoolExpr -> BoolExpr
  83 unpackPair v1 v2 te be | Just subst1 <- findReplacer v1 be
  84                        , Just subst2 <- findReplacer v2 be
  85                        = subst1. subst2 $ (pair v1 v2 `equal` te) `aand` be
  86
  87 -- | If the whole tuple is a function, we can replace this
  88 --   by a comparison
  89 unpackPair v1 v2 te be | Just subst <- findReplacer (pair v1 v2) be
  90                        = subst $ (pair v1 v2 `equal` te) `aand` be
  91
  92 -- | Nothing to optimize
  93 unpackPair v1 v2 te be = UnpackPair v1 v2 te be
  94
  95 pair :: TypedExpr -> TypedExpr -> TypedExpr
  96 pair (TypedExpr e1 t1) (TypedExpr e2 t2) = TypedExpr (Pair e1 e2) (TPair t1 t2)
  97
  98 lambdaBE :: TypedExpr -> TypedExpr -> BoolExpr -> LambdaBE
  99 lambdaBE v1 v2 rel | typeOf v1 == typeOf v2
 100                    , rel == v1 `equal` v2    = CurriedEquals (typeOf v1)
 101                    | otherwise               = LambdaBE v1 v2 rel
 102
 103 andEither :: LambdaBE -> LambdaBE -> TypedExpr -> TypedExpr -> BoolExpr
 104 andEither (CurriedEquals _) (CurriedEquals _) e1 e2 = e1 `equal` e2
 105 andEither lbe1 lbe2 e1 e2 | Just f1 <- arg1IsFunc lbe1
 106                           , Just f2 <- arg1IsFunc lbe2
 107                           = e1 `equal` eitherE f1 f2 e2
 108                           | Just f1 <- arg2IsFunc lbe1
 109                           , Just f2 <- arg2IsFunc lbe2
 110                           = eitherE f1 f2 e1 `equal` e2
 111                           | otherwise
 112                           = AndEither lbe1 lbe2 (unTypeExpr e1) (unTypeExpr e2)
 113
 114 arg1IsFunc (CurriedEquals t)    = Just $ TypedExpr (Conc []) (Arrow t t)
 115 arg1IsFunc (LambdaBE v1 v2 rel) | Just v1' <- defFor v1 rel
 116                                 = Just (lambda v2 v1')
 117                                 | otherwise = Nothing
 118
 119 arg2IsFunc (CurriedEquals t)    = Just $ TypedExpr (Conc []) (Arrow t t)
 120 arg2IsFunc (LambdaBE v1 v2 rel) | Just v2' <- defFor v2 rel
 121                                 = Just (lambda v1 v2')
 122                                 | otherwise = Nothing
 123
 124 allZipWith :: TypedExpr -> TypedExpr -> BoolExpr -> TypedExpr -> TypedExpr -> BoolExpr
 125 allZipWith v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
 126                                 e1 `equal` amap (lambda v2 v1') e2
 127                            | Just v2' <- defFor v2 rel =
 128                                 amap (lambda v1 v2') e1 `equal` e2
 129                            | otherwise =
 130                                 AllZipWith (LambdaBE v1 v2 rel) (unTypeExpr e1) (unTypeExpr e2)
 131
 132 eitherE :: TypedExpr -> TypedExpr -> TypedExpr -> TypedExpr
 133 eitherE f1 f2 e | Arrow lt1 lt2 <- typeOf f1
 134                 , Arrow rt1 rt2 <- typeOf f2
 135                 , TEither lt rt <- typeOf e
 136                 , lt1 == lt
 137                 , rt1 == rt
 138         = let tEither = TypedExpr EitherMap (Arrow (typeOf f1) (Arrow (typeOf f2) (Arrow (typeOf e) (TEither lt2 rt2))))
 139           in  app (app (app tEither f1) f2) e
 140                 | otherwise = error $ "Type error in eitherE\n" ++ show (f1, f2, e)
 141
 142 amap :: TypedExpr -> TypedExpr -> TypedExpr
 143 amap tf tl | Arrow t1 t2 <- typeOf tf
 144            , List t      <- typeOf tl
 145            , t1 == t
 146            = let tMap = TypedExpr Map (Arrow (Arrow t1 t2) (Arrow (List t1) (List t2)))
 147              in app (app tMap tf) tl
 148            | otherwise = error "Type error in map"
 149
 150 aand :: BoolExpr -> BoolExpr -> BoolExpr
 151 aand (And xs) (And ys) = And (xs  ++ ys)
 152 aand (And xs) y        = And (xs  ++ [y])
 153 aand x        (And ys) = And ([x] ++ ys)
 154 aand x        y        = And ([x,y])
 155
 156 beTrue :: BoolExpr
 157 beTrue = And []
 158
 159 -- | Optimize a forall condition
 160 condition :: [TypedExpr] -> BoolExpr -> BoolExpr -> BoolExpr
 161 -- empty condition
 162 condition [] cond concl   | cond == beTrue
 163                           = concl
 164 -- float out conditions on the right
 165 condition vars cond (Condition vars' cond' concl')
 166                           = condition (vars ++ vars') (cond `aand` cond') concl'
 167
 168 -- Try to find variables that are functions of other variables, and remove them
 169 condition vars cond concl | True -- set to false to disable
 170                           , ((vars',cond',concl'):_) <- mapMaybe try vars
 171                           = condition vars' cond' concl'
 172               -- A variable which can be replaced
 173   where try v | Just subst <- findReplacer v cond
 174               = -- trace ("Tested " ++ show v ++ ", can be replaced") $
 175                 Just (delete v vars, subst cond, subst concl)
 176
 177               -- A variable with can be removed
 178               | not (unTypeExpr v `occursIn` cond || unTypeExpr v `occursIn` concl)
 179               = -- trace ("Tested " ++ show v ++ ", can be reased") $
 180                 Just (delete v vars, cond, concl)
 181
 182               -- Nothing to do with this variable
 183               | otherwise
 184               = -- trace ("Tested " ++ show v ++ " without success") $
 185                 Nothing
 186
 187 -- Nothing left to optizmize
 188 condition vars cond concl = Condition vars cond concl
 189
 190 -- | Replaces a Term in a BoolExpr
 191 replaceTermBE :: Expr -> Expr -> BoolExpr -> BoolExpr
 192 replaceTermBE d r = go
 193   where go (e1 `Equal` e2) | d == e1 && r == e2 = beTrue
 194                            | d == e2 && r == e1 = beTrue
 195                            | otherwise          = go' e1 `equal'` go' e2
 196         go (And es)        = foldr aand beTrue (map go es)
 197         go (AllZipWith lbe e1 e2)
 198                            = AllZipWith (goL lbe) (go' e1) (go' e2)
 199         go (AndEither lbe1 lbe2 e1 e2)
 200                            = AndEither (goL lbe1) (goL lbe2) (go' e1) (go' e2)
 201         go (Condition vs cond concl)
 202                            = condition vs (go cond) (go concl)
 203         go (UnpackPair v1 v2 e be)
 204                            = unpackPair v1 v2 (goT e) (go be)
 205         go (TypeVarInst _ _ _) = error "TypeVarInst not expected here"
 206
 207         go' = replaceExpr d r
 208
 209         goT te = te { unTypeExpr = go' (unTypeExpr te) }
 210
 211         goL (CurriedEquals t)   = (CurriedEquals t)
 212         goL (LambdaBE v1 v2 be) = lambdaBE v1 v2 (go be)
 213
 214
 215 replaceExpr :: Expr -> Expr -> Expr -> Expr
 216 replaceExpr d r = go
 217   where go e | e == d    = r
 218         go (App e1 e2)   = app' (go e1) (go e2)
 219         go (Conc es)     = foldr conc (Conc []) (map go es)
 220         go (Lambda te e) = lambda' te (go e)
 221         go (Pair e1 e2)  = Pair (go e1) (go e2)
 222         go e             = e
 223
 224
 225 -- | Is inside the term a definition for the variable?
 226 findReplacer :: TypedExpr -> BoolExpr -> Maybe (BoolExpr -> BoolExpr)
 227 findReplacer tv be = findReplacer' (unTypeExpr tv) be
 228
 229 -- | Find a definition, and return a substitution
 230 findReplacer' :: Expr -> BoolExpr -> Maybe (BoolExpr -> BoolExpr)
 231 -- For combined types, look up the components
 232 findReplacer' (Pair x y) e | Just (delX) <- findReplacer' x e
 233                            , Just (delY) <- findReplacer' y e
 234                     = Just (delX . delY)
 235 -- Find the definition
 236 findReplacer' e (e1 `Equal` e2) | e == e1    = Just (replaceTermBE e e2)
 237                                 | e == e2    = Just (replaceTermBE e e1)
 238 findReplacer' e (And es)        = listToMaybe (mapMaybe (findReplacer' e) es)
 239                                   -- assuming no two definitions can exist
 240 findReplacer' _ _               = Nothing
 241
 242 -- | Is inside the term a definition for the variable?
 243 defFor :: TypedExpr -> BoolExpr -> Maybe (TypedExpr)
 244 defFor tv be | Just (e') <- defFor' (unTypeExpr tv) be
 245                          = Just (TypedExpr e' (typeOf tv))
 246              | otherwise = Nothing
 247
 248 -- | Find a definition, and return it along the definition remover
 249 defFor' :: Expr -> BoolExpr -> Maybe (Expr)
 250 defFor' e (e1 `Equal` e2) | e == e1                 = Just (e2)
 251                           | e == e2                 = Just (e1)
 252 defFor' e (And es)        | [d]  <- mapMaybe (defFor' e) es -- exactly one definition
 253                                                     = Just d
 254 defFor' _ _                                         = Nothing
 255
 256 app :: TypedExpr -> TypedExpr -> TypedExpr
 257 app te1 te2 | Arrow t1 t2 <- typeOf te1
 258             , t3          <- typeOf te2
 259             , t1 == t3
 260             = TypedExpr (app' (unTypeExpr te1) (unTypeExpr te2)) t2
 261 app te1 te2 | otherwise                          = error $ "Type mismatch in app: " ++
 262                                                            show te1 ++ " " ++ show te2
 263
 264 app' :: Expr -> Expr -> Expr
 265 app' Map (Conc []) = Conc []   -- map id = id
 266 app' ConstUnit v   = EUnit     -- id x   = x
 267 app' (Conc []) v   = v         -- id x   = x
 268 app' f v           = App f v
 269
 270 lambda :: TypedExpr -> TypedExpr -> TypedExpr
 271 lambda tv e = TypedExpr (lambda' tv (unTypeExpr e)) (Arrow (typeOf tv) (typeOf e))
 272
 273 lambda' :: TypedExpr -> Expr -> Expr
 274 lambda' tv e  | (Just e') <- isApplOn (unTypeExpr tv) e
 275               , not (unTypeExpr tv `occursIn` e')
 276                                      = e'
 277               | unTypeExpr tv == e   = Conc []
 278               | otherwise            = Lambda tv e
 279
 280 conc :: Expr -> Expr -> Expr
 281 conc (Conc xs) (Conc ys) = Conc (xs  ++ ys)
 282 conc (Conc xs)  y        = Conc (xs  ++ [y])
 283 conc x         (Conc ys) = Conc ([x] ++ ys)
 284 conc x          y        = Conc ([x,y])
 285
 286
 287 -- Specialization of g'
 288
 289 specialize (TypeVarInst strict i be') =
 290                 replaceTermBE (Var (FromTypVar i)) (if strict then Conc [] else ConstUnit) .
 291                 everywhere (mkT $ go) $
 292                 be
 293         where be = specialize be'
 294               go (TypInst i' _) | i' == i = TUnit
 295               go tv                       = tv
 296 -- No need to go further once we are through the quantors
 297 specialize be = be
 298
 299 -- Helpers
 300
 301 isApplOn :: Expr -> Expr -> Maybe Expr
 302 isApplOn e e'         | e == e'                       = Nothing
 303 isApplOn e (App f e') | e == e'                       = Just (Conc [f])
 304 isApplOn e (App f e') | (Just inner) <- isApplOn e e' = Just (conc f inner)
 305 isApplOn _ _                                          = Nothing
 306
 307 occursIn :: (Typeable a, Data a1, Eq a) => a -> a1 -> Bool
 308 e `occursIn` e'       = not (null (listify (==e) e'))
 309
 310 isTuple :: Typ -> Bool
 311 isTuple (TPair _ _) = True
 312 isTuple _           = False
 313
 314
 315 -- showing
 316
 317 -- Precedences:
 318 -- 10 fun app
 319 --  9 (.)
 320 --  8 ==
 321 --  7 ==>
 322 --  6 forall
 323
 324 instance Show EVar where
 325         show F               = "f"
 326         show (FromTypVar i)  = "g" ++ show i
 327         show (FromParam i b) = "x" ++ show i ++ if b then "'" else ""
 328
 329
 330 instance Show Expr where
 331         showsPrec _ (Var v)     = showsPrec 11 v
 332         showsPrec d (App e1 e2) = showParen (d>10) $
 333                 showsPrec 10 e1 . showChar ' ' . showsPrec 11 e2
 334         showsPrec _ (Conc [])   = showString "id"
 335         showsPrec d (Conc [e])  = showsPrec d e
 336         showsPrec d (Conc es)   = showParen (d>9) $
 337                 showIntercalate (showString " . ") (map (showsPrec 10) es)
 338         showsPrec _ (Lambda tv e) = showParen True $
 339                                     showString "\\" .
 340                                     showsPrec 0 tv .
 341                                     showString " -> ".
 342                                     showsPrec 0 e
 343         showsPrec _ (Pair e1 e2) = showParen True $
 344                                    showsPrec 0 e1 .
 345                                    showString "," .
 346                                    showsPrec 0 e2
 347         showsPrec _ Map           = showString "map"
 348         showsPrec d ConstUnit     = showParen (d>10) $ showString "const ()"
 349         showsPrec _ EitherMap     = showString "eitherMap"
 350
 351 showIntercalate :: ShowS -> [ShowS] -> ShowS
 352 showIntercalate _ []  = id
 353 showIntercalate _ [x] = x
 354 showIntercalate i (x:xs) = x . i . showIntercalate i xs
 355
 356 instance Show TypedExpr where
 357         showsPrec d (TypedExpr e t) =
 358                 showParen (d>10) $
 359                         showsPrec 0 e .
 360                         showString " :: " .
 361                         showString (showTypePrec 0 t)
 362
 363 instance Show LambdaBE where
 364         show (CurriedEquals _) =
 365                         "(==)"
 366         show (LambdaBE v1 v2 be) =
 367                         "(" ++
 368                         "\\" ++
 369                         showsPrec 11 (unTypeExpr v1) "" ++
 370                         " " ++
 371                         showsPrec 11 (unTypeExpr v2) "" ++
 372                         " -> " ++
 373                         show be ++
 374                         ")"
 375
 376 instance Show BoolExpr where
 377         show (Equal e1 e2) = showsPrec 9 e1 $
 378                              showString " == " $
 379                              showsPrec 9 e2 ""
 380         show (And [])      = "True"
 381         show (And bes)     = intercalate " && " $ map show bes
 382         show (AllZipWith lbe e1 e2) =
 383                         "allZipWith " ++
 384                         show lbe ++
 385                         " " ++
 386                         showsPrec 11 e1 "" ++
 387                         " " ++
 388                         showsPrec 11 e2 ""
 389         show (AndEither lbe1 lbe2 e1 e2) =
 390                         "andEither " ++
 391                         show lbe1 ++
 392                         " " ++
 393                         show lbe2 ++
 394                         " " ++
 395                         showsPrec 11 e1 "" ++
 396                         " " ++
 397                         showsPrec 11 e2 ""
 398         show (Condition tvars be1 be2) =
 399                         "forall " ++
 400                         intercalate ", " (map show tvars) ++
 401                         ".\n" ++
 402                         (if be1 /= beTrue then indent 2 (show be1) ++ "==>\n" else "") ++
 403                         indent 2 (show be2)
 404         show (UnpackPair v1 v2 e be) =
 405                         "let (" ++
 406                         showsPrec 0 v1 "" ++
 407                         "," ++
 408                         showsPrec 0 v2 "" ++
 409                         ") = " ++
 410                         showsPrec 0 e "" ++
 411                         " in\n" ++
 412                         indent 2 (show be)
 413         show (TypeVarInst strict i be) =
 414                         "forall types t" ++
 415                         show (2*i-1) ++
 416                         ", t" ++
 417                         show (2*i) ++
 418                         ", " ++
 419                         (if strict then "strict " else "(strict) ") ++
 420                         "functions " ++
 421                         show i ++
 422                         " :: t" ++
 423                         show (2*i-1) ++
 424                         " -> t" ++
 425                         show (2*i) ++
 426                         ".\n" ++
 427                         indent 2 (show be)
 428
 429 indent :: Int -> String -> String
 430 indent n = unlines . map (replicate n ' ' ++) . lines
 431
 432 showTypePrec :: Int -> Typ -> String
 433 showTypePrec _ Int                          = "Int"
 434 showTypePrec _ (TVar (TypVar i))            = "a"++show i
 435 showTypePrec _ (TVar (TypInst i b)) | not b = "t" ++  show (2*i-1)
 436                                     |     b = "t" ++  show (2*i)
 437 showTypePrec _ (TVar (TUnit))               = "()"
 438 showTypePrec d (Arrow t1 t2)                = paren (d>9) $
 439                                                 showTypePrec 10 t1 ++
 440                                                 " -> " ++
 441                                                 showTypePrec 9 t2
 442 showTypePrec _ (List t)                     = "[" ++ showTypePrec 0 t ++ "]"
 443 showTypePrec _ (TEither t1 t2)              = "Either " ++ showTypePrec 11 t1 ++
 444                                                     " " ++ showTypePrec 11 t2
 445 showTypePrec _ (TPair t1 t2)                = "(" ++ showTypePrec 0 t1 ++
 446                                               "," ++ showTypePrec 0 t2 ++ ")"
 447 showTypePrec _ t                            = error $ "Did not expect to show " ++ show t
 448
 449 paren :: Bool -> String -> String
 450 paren b p   =  if b then "(" ++ p ++ ")" else p