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