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