Carry types with functions
[darcs-mirror-polyfix.git] / Expr.hs
1 {-# LANGUAGE PatternGuards  #-}
2 module Expr where
3
4 import Data.List
5 import ParseType
6
7 data TypedExpr = TypedExpr
8         { unTypeExpr    :: Expr
9         , typeOf        :: Typ
10         , onRightSide   :: Bool
11         } deriving (Eq)
12
13 data Expr
14         = Var String
15         | App Expr Expr
16         | Conc [Expr] -- Conc [] is Id
17         | Lambda String Expr
18         | Pair Expr Expr
19         | Map
20             deriving (Eq)
21
22 data BoolExpr 
23         = BETrue
24         | Equal Expr Expr
25         | And BoolExpr BoolExpr
26         | AllZipWith String String BoolExpr Expr Expr
27         | Condition TypedExpr TypedExpr  BoolExpr BoolExpr
28         | UnpackPair String String Expr Bool Typ BoolExpr
29         | UnCond String Bool Typ BoolExpr
30         | TypeVarInst Int BoolExpr
31             deriving (Eq)
32
33 -- Smart constructors
34
35 -- Left or right side of a relation (affects type variables)
36 typedLeft e t = TypedExpr e t False
37 typedRight e t = TypedExpr e t True
38
39 equal = Equal
40
41 unpackPair = UnpackPair
42
43 allZipWith v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
44                                 e1 `equal` app (app Map (lambda v2 v1')) e2
45                            | Just v2' <- defFor v2 rel =
46                                 app (app Map (lambda v1 v2')) e1 `equal` e2
47                            | otherwise =
48                                 AllZipWith v1 v2 rel e1 e2
49
50 -- | Is inside the term a definition for the variable?
51 defFor v (e1 `Equal` e2) | (Var v) == e1 = Just e2
52                          | (Var v) == e2 = Just e1
53 defFor v (e1 `And` e2)   | Just d  <- defFor v e1
54                          , Nothing <- defFor v e2 = Just d
55 defFor v (e1 `And` e2)   | Just d  <- defFor v e2
56                          , Nothing <- defFor v e1 = Just d
57 defFor _ _                               = Nothing
58
59 app Map (Conc []) = Conc []
60 app (Conc []) v   = v
61 app f v           = App f v
62
63 unCond v b t (Equal l r) | (Just l') <- isApplOn v l 
64                          , (Just r') <- isApplOn v r = 
65         if hasVar v l' || hasVar v r'
66         then UnCond v b t (Equal l' r')
67         else (Equal l' r')
68 unCond v b t e = UnCond v b t e
69
70 lambda v e | (Just e') <- isApplOn v e, not (hasVar v e') = e'
71            | Var v == e                                   = Conc []
72            | otherwise                                    = Lambda v e
73
74
75 conc f (Conc fs) = Conc (f:fs)
76
77 -- Helpers
78
79 isApplOn v (Var _)                                         = Nothing
80 isApplOn v (App f (Var v')) | v == v'                      = Just (Conc [f])
81 isApplOn v (App f e)        | (Just inner) <- isApplOn v e = Just (conc f inner)
82 isApplOn _ _                                               = Nothing
83
84 hasVar v (Var v')     = v == v'
85 hasVar v (App e1 e2)  = hasVar v e1 && hasVar v e2
86 hasVar v (Conc es)    = any (hasVar v) es
87 hasVar v (Lambda _ e) = hasVar v e
88 hasVar v Map          = False
89
90 isTuple (TPair _ _) = True
91 isTuple _           = False
92
93
94 -- showing
95
96 -- Precedences:
97 -- 10 fun app
98 --  9 (.)
99 --  8 ==
100 --  7 ==>
101 --  6 forall
102
103 instance Show Expr where
104         showsPrec d (Var s)     = showString s
105         showsPrec d (App e1 e2) = showParen (d>10) $
106                 showsPrec 10 e1 . showChar ' ' . showsPrec 11 e2
107         showsPrec d (Conc [])   = showString "id"
108         showsPrec d (Conc [e])  = showsPrec d e
109         showsPrec d (Conc es)   = showParen (d>9) $
110                 showIntercalate (showString " . ") (map (showsPrec 10) es)
111         showsPrec d (Lambda v e) = showParen True $ 
112                                    showString "\\" .
113                                    showString v .
114                                    showString " -> ".
115                                    showsPrec 0 e 
116         showsPrec _ (Pair e1 e2) = showParen True $ 
117                                    showsPrec 0 e1 .
118                                    showString "," .
119                                    showsPrec 0 e2
120         showsPrec _ Map           = showString "map"
121
122 showIntercalate i []  = id
123 showIntercalate i [x] = x
124 showIntercalate i (x:xs) = x . i . showIntercalate i xs
125
126 instance Show TypedExpr where
127         showsPrec d (TypedExpr e t rightSide) = 
128                 showParen (d>10) $
129                         showsPrec 0 e .
130                         showString " :: " .
131                         showString (arrowInstType rightSide t)
132
133 instance Show BoolExpr where
134         show (Equal e1 e2) = showsPrec 9 e1 $
135                              showString " == " $
136                              showsPrec 9 e2 ""
137         show (And be1 be2) = show be1 ++
138                              " && " ++
139                              show be2 
140         show (AllZipWith v1 v2 be e1 e2) =
141                         "allZipWith " ++
142                         "( " ++
143                         "\\" ++
144                         v1 ++
145                         " " ++
146                         v2 ++
147                         " -> " ++
148                         show be ++
149                         ")" ++
150                         " " ++
151                         showsPrec 11 e1 "" ++
152                         " " ++
153                         showsPrec 11 e2 ""
154         show (Condition tv1 tv2 be1 be2) = 
155                         "forall " ++
156                         showsPrec 0 tv1 "" ++
157                         ", " ++
158                         showsPrec 0 tv2 "" ++
159                         ".\n" ++
160                         (if be1 /= BETrue then indent 2 (show be1) ++ "==>\n" else "") ++
161                         indent 2 (show be2)
162         show (UnpackPair v1 v2 e b t be) = 
163                         "let (" ++
164                         v1 ++
165                         "," ++
166                         v2 ++
167                         ") = " ++
168                         showsPrec 0 e "" ++
169                         " :: " ++
170                         arrowInstType b t ++
171                         " in\n" ++
172                         indent 2 (show be)
173         show (UnCond v1 b t be1) = 
174                         "forall " ++
175                         v1 ++
176                         " :: " ++
177                         arrowInstType b t ++
178                         ".\n" ++
179                         indent 2 (show be1)
180         show (TypeVarInst i be) = 
181                         "forall types t" ++
182                         show (2*i-1) ++
183                         ", t" ++
184                         show (2*i) ++
185                         ", function g" ++
186                         show i ++
187                         " :: t" ++
188                         show (2*i-1) ++
189                         " -> t" ++
190                         show (2*i) ++ 
191                         ".\n" ++
192                         indent 2 (show be)
193
194 indent n = unlines . map (replicate n ' ' ++) . lines
195
196 arrowInstType :: Bool -> Typ -> String
197 arrowInstType b = ait 0
198   where 
199         ait _ Int                       = "Int" 
200         ait _ (TVar (TypVar i)) | not b = "t" ++  show (2*i-1)
201                                 |     b = "t" ++  show (2*i)
202         ait d (Arrow t1 t2)             = paren (d>9) $ 
203                                                   ait 10 t1 ++ " -> " ++ ait 9 t2 
204         ait d (List t)                  = "[" ++ ait 0 t ++ "]"
205         ait d (TEither t1 t2)           = "Either " ++ ait 11 t1 ++ 
206                                                 " " ++ ait 11 t2
207         ait d (TPair t1 t2)             = "(" ++ ait 0 t1 ++ "," ++ ait 0 t2 ++ ")"
208
209 paren b p   =  if b then "(" ++ p ++ ")" else p