And as list
[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 inside the term a definition for the variable?
67 defFor :: TypedExpr -> BoolExpr -> Maybe TypedExpr
68 defFor tv be | Just e' <- defFor' (unTypeExpr tv) be
69                          = Just (TypedExpr e' (typeOf tv))
70              | otherwise = Nothing
71         
72 defFor' v (e1 `Equal` e2) | v == e1                 = Just e2
73                           | v == e2                 = Just e1
74 defFor' v (And es)        | [d]  <- mapMaybe (defFor' v) es -- exactly one definition
75                                                     = Just d
76 defFor' _ _                                         = Nothing
77
78 app te1 te2 | Arrow t1 t2 <- typeOf te1
79             , t3          <- typeOf te2 
80             , t1 == t3 
81             = TypedExpr (app' (unTypeExpr te1) (unTypeExpr te2)) t2
82  where app' Map (Conc []) = Conc []
83        app' (Conc []) v   = v
84        app' f v           = App f v
85 app te1 te2 | otherwise                          = error $ "Type mismatch in app: " ++
86                                                            show te1 ++ " " ++ show te2
87
88 unCond v (Equal l r) | (Just l') <- isApplOn (unTypeExpr v) l 
89                      , (Just r') <- isApplOn (unTypeExpr v) r = 
90         if v `occursIn` l' || v `occursIn` r'
91         then Condition [v] beTrue (Equal l' r')
92         else (Equal l' r')
93 unCond v e = Condition [v] beTrue e
94
95 lambda tv e = TypedExpr inner (Arrow (typeOf tv) (typeOf e))
96   where inner | (Just e') <- isApplOn (unTypeExpr tv) (unTypeExpr e)
97               , not (unTypeExpr tv `occursIn` e')
98                           = e'
99               | tv == e   = Conc []
100               | otherwise = Lambda tv (unTypeExpr e)
101
102 conc f (Conc fs) = Conc (f:fs)
103
104 -- Helpers
105
106 isApplOn e e'         | e == e'                       = Nothing
107 isApplOn e (App f e') | e == e'                       = Just (Conc [f])
108 isApplOn e (App f e') | (Just inner) <- isApplOn e e' = Just (conc f inner)
109 isApplOn _ _                                          = Nothing
110
111 hasVar v (Var v')     = v == v'
112 hasVar v (App e1 e2)  = hasVar v e1 && hasVar v e2
113 hasVar v (Conc es)    = any (hasVar v) es
114 hasVar v (Lambda _ e) = hasVar v e
115 hasVar v Map          = False
116
117 e `occursIn` e'       = not (null (listify (==e) e'))
118
119 isTuple (TPair _ _) = True
120 isTuple _           = False
121
122
123 -- showing
124
125 -- Precedences:
126 -- 10 fun app
127 --  9 (.)
128 --  8 ==
129 --  7 ==>
130 --  6 forall
131
132 instance Show Expr where
133         showsPrec d (Var s)     = showString s
134         showsPrec d (App e1 e2) = showParen (d>10) $
135                 showsPrec 10 e1 . showChar ' ' . showsPrec 11 e2
136         showsPrec d (Conc [])   = showString "id"
137         showsPrec d (Conc [e])  = showsPrec d e
138         showsPrec d (Conc es)   = showParen (d>9) $
139                 showIntercalate (showString " . ") (map (showsPrec 10) es)
140         showsPrec d (Lambda tv e) = showParen True $ 
141                                     showString "\\" .
142                                     showsPrec 0 tv .
143                                     showString " -> ".
144                                     showsPrec 0 e 
145         showsPrec _ (Pair e1 e2) = showParen True $ 
146                                    showsPrec 0 e1 .
147                                    showString "," .
148                                    showsPrec 0 e2
149         showsPrec _ Map           = showString "map"
150
151 showIntercalate i []  = id
152 showIntercalate i [x] = x
153 showIntercalate i (x:xs) = x . i . showIntercalate i xs
154
155 instance Show TypedExpr where
156         showsPrec d (TypedExpr e t) = 
157                 showParen (d>10) $
158                         showsPrec 0 e .
159                         showString " :: " .
160                         showString (showTypePrec 0 t)
161
162 instance Show BoolExpr where
163         show (Equal e1 e2) = showsPrec 9 e1 $
164                              showString " == " $
165                              showsPrec 9 e2 ""
166         show (And [])      = show "True"
167         show (And bes)     = intercalate " && " $ map show bes
168         show (AllZipWith v1 v2 be e1 e2) =
169                         "allZipWith " ++
170                         "( " ++
171                         "\\" ++
172                         showsPrec 11 v1 "" ++
173                         " " ++
174                         showsPrec 11 v2 "" ++
175                         " -> " ++
176                         show be ++
177                         ")" ++
178                         " " ++
179                         showsPrec 11 e1 "" ++
180                         " " ++
181                         showsPrec 11 e2 ""
182         show (Condition tvars be1 be2) = 
183                         "forall " ++
184                         intercalate ", " (map show tvars) ++
185                         ".\n" ++
186                         (if be1 /= beTrue then indent 2 (show be1) ++ "==>\n" else "") ++
187                         indent 2 (show be2)
188         show (UnpackPair v1 v2 e be) = 
189                         "let (" ++
190                         showsPrec 0 v1 "" ++
191                         "," ++
192                         showsPrec 0 v2 "" ++
193                         ") = " ++
194                         showsPrec 0 e "" ++
195                         " in\n" ++
196                         indent 2 (show be)
197         show (TypeVarInst i be) = 
198                         "forall types t" ++
199                         show (2*i-1) ++
200                         ", t" ++
201                         show (2*i) ++
202                         ", function g" ++
203                         show i ++
204                         " :: t" ++
205                         show (2*i-1) ++
206                         " -> t" ++
207                         show (2*i) ++ 
208                         ".\n" ++
209                         indent 2 (show be)
210
211 indent n = unlines . map (replicate n ' ' ++) . lines
212
213 showTypePrec :: Int -> Typ -> String
214 showTypePrec _ Int                          = "Int" 
215 showTypePrec _ (TVar (TypVar i))            = "a"++show i
216 showTypePrec _ (TVar (TypInst i b)) | not b = "t" ++  show (2*i-1)
217                                     |     b = "t" ++  show (2*i)
218 showTypePrec d (Arrow t1 t2)                = paren (d>9) $ 
219                                   showTypePrec 10 t1 ++ " -> " ++ showTypePrec 9 t2 
220 showTypePrec d (List t)                     = "[" ++ showTypePrec 0 t ++ "]"
221 showTypePrec d (TEither t1 t2)              = "Either " ++ showTypePrec 11 t1 ++ 
222                                                     " " ++ showTypePrec 11 t2
223 showTypePrec d (TPair t1 t2)                = "(" ++ showTypePrec 0 t1 ++
224                                               "," ++ showTypePrec 0 t2 ++ ")"
225
226 paren b p   =  if b then "(" ++ p ++ ")" else p