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 Data.Generics hiding (typeOf)
   9 import Data.Generics.Schemes
  10
  11 data TypedExpr = TypedExpr
  12         { unTypeExpr    :: Expr
  13         , typeOf        :: Typ
  14         } deriving (Eq, Typeable, Data)
  15
  16 typedLeft, typedRight :: Expr -> Typ -> TypedExpr
  17 typedLeft  e t = TypedExpr e (instType False t)
  18 typedRight e t = TypedExpr e (instType True t)
  19
  20 data Expr
  21         = Var String
  22         | App Expr Expr
  23         | Conc [Expr] -- Conc [] is Id
  24         | Lambda TypedExpr Expr
  25         | Pair Expr Expr
  26         | Map
  27             deriving (Eq, Typeable, Data)
  28
  29 data BoolExpr
  30         = Equal Expr Expr
  31         | And [BoolExpr] -- And [] is True
  32         | AllZipWith TypedExpr TypedExpr BoolExpr Expr Expr
  33         | Condition [TypedExpr] BoolExpr BoolExpr
  34         | UnpackPair TypedExpr TypedExpr TypedExpr BoolExpr
  35         | TypeVarInst Int BoolExpr
  36             deriving (Eq, Typeable, Data)
  37
  38 -- Smart constructors
  39
  40 equal te1 te2 | typeOf te1 /= typeOf te2 = error "Type mismatch in equal"
  41               | otherwise                = Equal (unTypeExpr te1) (unTypeExpr te2)
  42
  43 unpackPair = UnpackPair
  44
  45 allZipWith :: TypedExpr -> TypedExpr -> BoolExpr -> TypedExpr -> TypedExpr -> BoolExpr
  46 allZipWith v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
  47                                 e1 `equal` amap (lambda v2 v1') e2
  48                            | Just v2' <- defFor v2 rel =
  49                                 amap (lambda v1 v2') e1 `equal` e2
  50                            | otherwise =
  51                                 AllZipWith v1 v2 rel (unTypeExpr e1) (unTypeExpr e2)
  52
  53 amap tf tl | Arrow t1 t2 <- typeOf tf
  54            , List t      <- typeOf tl
  55            , t1 == t
  56            = let tMap = TypedExpr Map (Arrow (Arrow t1 t2) (Arrow (List t1) (List t2)))
  57              in app (app tMap tf) tl
  58 amap tf tl | otherwise = error "Type error in map"
  59
  60 -- Float out foralls
  61 aand (Condition vars beTrue concl) be = Condition vars beTrue (aand concl be)
  62 aand (And xs) (And ys) = And (xs  ++ ys)
  63 aand (And xs) y        = And (xs  ++ [y])
  64 aand x        (And ys) = And ([x] ++ ys)
  65 aand x        y        = And ([x,y])
  66
  67 beTrue = And []
  68
  69 -- | Is any var (or part of var) defined in cond, and can be replaced in concl?
  70 condition :: [TypedExpr] -> BoolExpr -> BoolExpr -> BoolExpr
  71 condition vars cond concl | ((vars',cond',concl'):_) <- mapMaybe try vars
  72                           = condition vars' cond' concl'
  73                           | otherwise
  74                           = Condition vars cond concl
  75   where try v = do subst <- findReplacer v cond --Maybe Monad
  76                    return (delete v vars, subst cond, subst concl)
  77
  78 -- | Replaces a Term in a BoolExpr
  79 replaceTermBE :: Expr -> Expr -> BoolExpr -> BoolExpr
  80 replaceTermBE d r = go
  81   where go (e1 `Equal` e2) | d == e1 && r == e2 = beTrue
  82                            | d == e2 && r == e1 = beTrue
  83                            | otherwise          = go' e1 `Equal` go' e2
  84         go (And es)        = foldr aand beTrue (map go es)
  85         go (AllZipWith v1 v2 be e1 e2)
  86                            = AllZipWith v1 v2 (go be) (go' e1) (go' e2)
  87         go (Condition vs cond concl)
  88                            = condition vs (go cond) (go concl)
  89         go (UnpackPair v1 v2 e be)
  90                            = unpackPair v1 v2 (go' e) (go be)
  91         go (TypeVarInst _ _) = error "TypeVarInst not expected here"
  92         go' :: Data a => a -> a
  93         go' = replaceExpr d r
  94
  95 replaceExpr :: Data a => Expr -> Expr -> a -> a
  96 replaceExpr d r = everywhere (mkT go)
  97   where go e | e == d    = r
  98              | otherwise = e
  99
 100 -- | Is inside the term a definition for the variable?
 101 findReplacer :: TypedExpr -> BoolExpr -> Maybe (BoolExpr -> BoolExpr)
 102 findReplacer tv be = findReplacer' (unTypeExpr tv) be
 103
 104 -- | Find a definition, and return a substitution
 105 findReplacer' :: Expr -> BoolExpr -> Maybe (BoolExpr -> BoolExpr)
 106 -- For combined types, look up the components
 107 findReplacer' (Pair x y) e | Just (delX) <- findReplacer' x e
 108                            , Just (delY) <- findReplacer' y e
 109                     = Just (delX . delY)
 110 -- Find the definition
 111 findReplacer' e (e1 `Equal` e2) | e == e1    = Just (replaceTermBE e e2)
 112                                 | e == e2    = Just (replaceTermBE e e1)
 113 findReplacer' e (And es)        = listToMaybe (mapMaybe (findReplacer' e) es)
 114                                   -- assuming no two definitions can exist
 115 findReplacer' _ _               = Nothing
 116
 117 -- | Is inside the term a definition for the variable?
 118 defFor :: TypedExpr -> BoolExpr -> Maybe (TypedExpr)
 119 defFor tv be | Just (e') <- defFor' (unTypeExpr tv) be
 120                          = Just (TypedExpr e' (typeOf tv))
 121              | otherwise = Nothing
 122
 123 -- | Find a definition, and return it along the definition remover
 124 defFor' :: Expr -> BoolExpr -> Maybe (Expr)
 125 defFor' e (e1 `Equal` e2) | e == e1                 = Just (e2)
 126                           | e == e2                 = Just (e1)
 127 defFor' e (And es)        | [d]  <- mapMaybe (defFor' e) es -- exactly one definition
 128                                                     = Just d
 129 defFor' _ _                                         = Nothing
 130
 131 app te1 te2 | Arrow t1 t2 <- typeOf te1
 132             , t3          <- typeOf te2
 133             , t1 == t3
 134             = TypedExpr (app' (unTypeExpr te1) (unTypeExpr te2)) t2
 135  where app' Map (Conc []) = Conc []
 136        app' (Conc []) v   = v
 137        app' f v           = App f v
 138 app te1 te2 | otherwise                          = error $ "Type mismatch in app: " ++
 139                                                            show te1 ++ " " ++ show te2
 140
 141 unCond v (Equal l r) | (Just l') <- isApplOn (unTypeExpr v) l
 142                      , (Just r') <- isApplOn (unTypeExpr v) r =
 143         if v `occursIn` l' || v `occursIn` r'
 144         then Condition [v] beTrue (Equal l' r')
 145         else (Equal l' r')
 146 unCond v e = Condition [v] beTrue e
 147
 148 lambda tv e = TypedExpr inner (Arrow (typeOf tv) (typeOf e))
 149   where inner | (Just e') <- isApplOn (unTypeExpr tv) (unTypeExpr e)
 150               , not (unTypeExpr tv `occursIn` e')
 151                           = e'
 152               | tv == e   = Conc []
 153               | otherwise = Lambda tv (unTypeExpr e)
 154
 155 conc f (Conc fs) = Conc (f:fs)
 156
 157 -- Helpers
 158
 159 isApplOn e e'         | e == e'                       = Nothing
 160 isApplOn e (App f e') | e == e'                       = Just (Conc [f])
 161 isApplOn e (App f e') | (Just inner) <- isApplOn e e' = Just (conc f inner)
 162 isApplOn _ _                                          = Nothing
 163
 164 hasVar v (Var v')     = v == v'
 165 hasVar v (App e1 e2)  = hasVar v e1 && hasVar v e2
 166 hasVar v (Conc es)    = any (hasVar v) es
 167 hasVar v (Lambda _ e) = hasVar v e
 168 hasVar v Map          = False
 169
 170 e `occursIn` e'       = not (null (listify (==e) e'))
 171
 172 isTuple (TPair _ _) = True
 173 isTuple _           = False
 174
 175
 176 -- showing
 177
 178 -- Precedences:
 179 -- 10 fun app
 180 --  9 (.)
 181 --  8 ==
 182 --  7 ==>
 183 --  6 forall
 184
 185 instance Show Expr where
 186         showsPrec d (Var s)     = showString s
 187         showsPrec d (App e1 e2) = showParen (d>10) $
 188                 showsPrec 10 e1 . showChar ' ' . showsPrec 11 e2
 189         showsPrec d (Conc [])   = showString "id"
 190         showsPrec d (Conc [e])  = showsPrec d e
 191         showsPrec d (Conc es)   = showParen (d>9) $
 192                 showIntercalate (showString " . ") (map (showsPrec 10) es)
 193         showsPrec d (Lambda tv e) = showParen True $
 194                                     showString "\\" .
 195                                     showsPrec 0 tv .
 196                                     showString " -> ".
 197                                     showsPrec 0 e
 198         showsPrec _ (Pair e1 e2) = showParen True $
 199                                    showsPrec 0 e1 .
 200                                    showString "," .
 201                                    showsPrec 0 e2
 202         showsPrec _ Map           = showString "map"
 203
 204 showIntercalate i []  = id
 205 showIntercalate i [x] = x
 206 showIntercalate i (x:xs) = x . i . showIntercalate i xs
 207
 208 instance Show TypedExpr where
 209         showsPrec d (TypedExpr e t) =
 210                 showParen (d>10) $
 211                         showsPrec 0 e .
 212                         showString " :: " .
 213                         showString (showTypePrec 0 t)
 214
 215 instance Show BoolExpr where
 216         show (Equal e1 e2) = showsPrec 9 e1 $
 217                              showString " == " $
 218                              showsPrec 9 e2 ""
 219         show (And [])      = show "True"
 220         show (And bes)     = intercalate " && " $ map show bes
 221         show (AllZipWith v1 v2 be e1 e2) =
 222                         "allZipWith " ++
 223                         "( " ++
 224                         "\\" ++
 225                         showsPrec 11 v1 "" ++
 226                         " " ++
 227                         showsPrec 11 v2 "" ++
 228                         " -> " ++
 229                         show be ++
 230                         ")" ++
 231                         " " ++
 232                         showsPrec 11 e1 "" ++
 233                         " " ++
 234                         showsPrec 11 e2 ""
 235         show (Condition tvars be1 be2) =
 236                         "forall " ++
 237                         intercalate ", " (map show tvars) ++
 238                         ".\n" ++
 239                         (if be1 /= beTrue then indent 2 (show be1) ++ "==>\n" else "") ++
 240                         indent 2 (show be2)
 241         show (UnpackPair v1 v2 e be) =
 242                         "let (" ++
 243                         showsPrec 0 v1 "" ++
 244                         "," ++
 245                         showsPrec 0 v2 "" ++
 246                         ") = " ++
 247                         showsPrec 0 e "" ++
 248                         " in\n" ++
 249                         indent 2 (show be)
 250         show (TypeVarInst i be) =
 251                         "forall types t" ++
 252                         show (2*i-1) ++
 253                         ", t" ++
 254                         show (2*i) ++
 255                         ", function g" ++
 256                         show i ++
 257                         " :: t" ++
 258                         show (2*i-1) ++
 259                         " -> t" ++
 260                         show (2*i) ++
 261                         ".\n" ++
 262                         indent 2 (show be)
 263
 264 indent n = unlines . map (replicate n ' ' ++) . lines
 265
 266 showTypePrec :: Int -> Typ -> String
 267 showTypePrec _ Int                          = "Int"
 268 showTypePrec _ (TVar (TypVar i))            = "a"++show i
 269 showTypePrec _ (TVar (TypInst i b)) | not b = "t" ++  show (2*i-1)
 270                                     |     b = "t" ++  show (2*i)
 271 showTypePrec d (Arrow t1 t2)                = paren (d>9) $
 272                                   showTypePrec 10 t1 ++ " -> " ++ showTypePrec 9 t2
 273 showTypePrec d (List t)                     = "[" ++ showTypePrec 0 t ++ "]"
 274 showTypePrec d (TEither t1 t2)              = "Either " ++ showTypePrec 11 t1 ++
 275                                                     " " ++ showTypePrec 11 t2
 276 showTypePrec d (TPair t1 t2)                = "(" ++ showTypePrec 0 t1 ++
 277                                               "," ++ showTypePrec 0 t2 ++ ")"
 278
 279 paren b p   =  if b then "(" ++ p ++ ")" else p