module Expr where
import Data.List
+import ParseType
data Expr
= Var String
| App Expr Expr
- | Conc [Expr]
+ | Conc [Expr] -- Conc [] is Id
| Lambda String Expr
| Map
deriving (Eq)
data BoolExpr
= Equal Expr Expr
| Pairwise String String BoolExpr Expr Expr
- | Condition String String BoolExpr BoolExpr
- | UnCond String BoolExpr
+ | Condition String String Typ BoolExpr BoolExpr
+ | UnCond String Bool Typ BoolExpr
| TypeVarInst Int BoolExpr
deriving (Eq)
-- Smart constructors
-unCond v (Equal l r) | (Just l') <- isApplOn v l
- , (Just r') <- isApplOn v r =
+equal = Equal
+
+pairwise v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
+ e1 `equal` app (app Map (lambda v2 v1')) e2
+ | Just v2' <- defFor v2 rel =
+ app (app Map (lambda v1 v2')) e1 `equal` e2
+ | otherwise =
+ Pairwise v1 v2 rel e1 e2
+
+defFor v (e1 `Equal` e2) | (Var v) == e1 = Just e2
+ | (Var v) == e2 = Just e1
+defFor _ _ = Nothing
+
+app Map (Conc []) = Conc []
+app (Conc []) v = v
+app f v = App f v
+
+unCond v b t (Equal l r) | (Just l') <- isApplOn v l
+ , (Just r') <- isApplOn v r =
if hasVar v l' || hasVar v r'
- then UnCond v (Equal l' r')
+ then UnCond v b t (Equal l' r')
else (Equal l' r')
-unCond v e = UnCond v e
+unCond v b t e = UnCond v b t e
lambda v e | (Just e') <- isApplOn v e, not (hasVar v e') = e'
+ | Var v == e = Conc []
| otherwise = Lambda v e
hasVar v (Var v') = v == v'
hasVar v (App e1 e2) = hasVar v e1 && hasVar v e2
hasVar v (Conc es) = any (hasVar v) es
+hasVar v (Lambda _ e) = hasVar v e
+hasVar v Map = False
-- showing
showsPrec d (Var s) = showString s
showsPrec d (App e1 e2) = showParen (d>10) $
showsPrec 10 e1 . showChar ' ' . showsPrec 11 e2
+ showsPrec d (Conc []) = showString "id"
+ showsPrec d (Conc [e]) = showsPrec d e
showsPrec d (Conc es) = showParen (d>9) $
showIntercalate (showString " . ") (map (showsPrec 10) es)
showsPrec d (Lambda v e) = showParen True $
showParen (d>10) $
showString "allZipWith " .
showParen True (
- showString "(\\" .
+ showString "\\" .
showString v1 .
showChar ' ' .
showString v2 .
showString " -> " .
- showsPrec 0 e1
+ showsPrec 0 be
) .
showChar ' ' .
+ showsPrec 11 e1 .
+ showChar ' ' .
showsPrec 11 e2
- showsPrec d (Condition v1 v2 be1 be2) =
+ showsPrec d (Condition v1 v2 t be1 be2) =
showParen (d>6) $
showString "forall " .
showString v1 .
- showChar ' ' .
+ showString " :: " .
+ arrowInstType False t .
+ showString ", " .
showString v2 .
- showString ". " .
+ showString " :: " .
+ arrowInstType True t .
+ showString ".\n" .
showsPrec 9 be1 .
showString " ==> " .
showsPrec 6 be2
- showsPrec d (UnCond v1 be1) =
+ showsPrec d (UnCond v1 b t be1) =
showParen (d>6) $
showString "forall " .
showString v1 .
- showString ". " .
+ showString " :: " .
+ arrowInstType b t .
+ showString ".\n" .
showsPrec 6 be1
showsPrec d (TypeVarInst i be) =
showParen (d>6) $
showString ".\n" .
showsPrec 6 be
+arrowInstType :: Bool -> Typ -> ShowS
+arrowInstType b Int = showString "Int"
+arrowInstType False (TVar (TypVar i)) = showString "t" . shows (2*i-1)
+arrowInstType True (TVar (TypVar i)) = showString "t" . shows (2*i)
+arrowInstType b (Arrow t1 t2) = arrowInstType b t1 .
+ showString " -> " .
+ arrowInstType b t2
[v1,v2] <- asks (take 2)
local (drop 2) $ do
map <- freeTheorem' (Var v1) (Var v2) t
- return $ case map of
- (Equal (Var v1') ev1) | v1' == v1 ->
- if ev1 == (Var v2)
- then Equal e1 e2
- else Equal e1 (App (App (Var "map") (lambda v2 ev1)) e2)
- _ -> Pairwise v1 v2 map e1 e2
+ return $ pairwise v1 v2 map e1 e2
freeTheorem' e1 e2 (Arrow t1 t2) = do
[v1,v2] <- asks (take 2)
local (drop 2) $ do
cond <- freeTheorem' (Var v1) (Var v2) t1
- case cond of
- (Equal (Var v1') ev1) | v1' == v1 -> do
- concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
- return $ unCond v2 concl
+ case (defFor v1 cond, defFor v2 cond) of
+ (Just ev1, _) -> do
+ concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
+ return $ unCond v2 True t1 concl
+ (Nothing,Just ev2) -> do
+ concl <- freeTheorem' (App e1 (Var v1)) (App e2 ev2) t2
+ return $ unCond v1 False t1 concl
_ -> do
concl <- freeTheorem' (App e1 (Var v1)) (App e2 (Var v2)) t2
- return $ Condition v1 v2 cond concl
+ return $ Condition v1 v2 t1 cond concl
freeTheorem' e1 e2 (TVar (TypVar i)) = return $
- Equal e1 (App (Var ("g"++show i)) e2)
+ Equal (App (Var ("g"++show i)) e1) e2
freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
freeTheorem' e1 e2 (All (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t