HaRe-0.6: refactorer/PwPf/GlobalPW.hs
-----------------------------------------------------------------------------
-- |
-- Module : GlobalPW
-- Copyright : (c) Jose Proenca 2005
-- License : GPL
--
-- Maintainer : jproenca@di.uminho.pt
-- Stability : experimental
-- Portability : portable
--
-- A global pointwise syntax and its relation with:
--
-- * An expression in programatica's abstract syntax tree;
--
-- * A pointwise core - "PWCore".
--
-----------------------------------------------------------------------------
module GlobalPW (
-- * Data Type
{-| Represents a pointwise language that:
(1) is very similar to the way we are used to program in haskell;
(2) not the most general one, since it only deals with booleans, natural numbers and lists.
-}
GLTerm (..),
-- * Conversion of an haskell expression to a GlobalPW term
exp2Global,
-- * Conversion of a GlobalPW term to a "PWCore" term
global2core
) where
import PWCore
import RefacUtils
import PrettyPrint
--------------------------------
----- Global definition --------
--------------------------------
data GLTerm
= Star -- ^Unit
| V String -- ^Variable
| GLTerm:-:GLTerm -- ^Aplication
| Lam String GLTerm -- ^Abstraction
| GLTerm:&:GLTerm -- ^Pair
| Pi1 GLTerm -- ^Point-wise first
| Pi2 GLTerm -- ^Point-wise second
| Inl' GLTerm -- ^Point-wise left injection
| Inr' GLTerm -- ^Point-wise right injection
| Case' GLTerm (String,GLTerm) (String,GLTerm)
-- ^Case of
| In' HsExpP GLTerm -- ^Injection on a specified type
| Out' HsExpP GLTerm -- ^Extraction of the functor of a specified type
| Fix' GLTerm -- ^Fixed-point
---------------- from PCF ---------------------
| T' -- ^Constant True
| F' -- ^Constant False
| Z' -- ^Constant Zero
| Suc GLTerm -- ^Successor
| Pred GLTerm -- ^Predecessor
| IsZ GLTerm -- ^is zero?
| Ite GLTerm GLTerm GLTerm -- ^if then else
| N' -- ^Empty list
| GLTerm ::: GLTerm -- ^Constructor for lists
| Hd GLTerm -- ^Head of a list
| Tl GLTerm -- ^Tail of a list
| IsN GLTerm -- ^is the list empty?
| Letrec String GLTerm GLTerm
-- ^recursive let
---------------- from BNL ---------------------
| RecNat GLTerm GLTerm GLTerm
-- ^Primitive recursion on Nat's
| RecList GLTerm GLTerm GLTerm
-- ^Primitive recursion on List's
deriving Show
{- | Applies a simple transformation from an expression of programatica's
abstract syntax tree to 'GLTerm'.
The recognized grammar is:
[G, G1, G2, G3 @::=@]
(G) | @undefined@ | @()@ | @_L@ | @inN (_L::@/type/@) @G |@ ouT (_L::@/type/@)@
|@ True @|@ False @|@ 0 @|@ [] @|@ /n, n>0/ @|@ [@G1@, @G2@, ... ] @| G1@ : @G2 |@ succ @G |@ pred @G
|@ (==0) @G |@ @G@ == 0 @|@ head @G@ @|@ tail @G@ @|@ null @
|@ recNat @G1@ @G2@ @G3@ @|@ recList @G1@ @G2@ @G3
|@ fix @G@ @|@ if @G1@ then @G2@ else @G3@ @|@ /var/ @|@ (@G1@,@G2@) @|@ fst @|@ snd @|@ Left @|@ Right @
|@ @G1@ /infixOp/ @G2@ @|@ \\/var1 var2 .../ -> @G
|@ case @G1@ of Left /var1/ -> @G2@; Right /var2/ ->@G3
|@ let /var/ = @G1@ in @G2@
@
where types are read as the pretty print string, and /var/, /var1/ and /var2/ are variables that are read as strings also.
-}
exp2Global :: Monad m => HsExpI PNT -> m GLTerm
-- parentisis
exp2Global (Exp (HsParen e)) = exp2Global e
-- unit -> "()" or "undefined" or "_L"
exp2Global (Exp (HsId (HsCon (PNT (PN (Qual (PlainModule "Prelude") "()") (G (PlainModule "Prelude") "()" (N (Just _)))) (ConstrOf (PN "()" (G (PlainModule "Prelude") "()" (N (Just _)))) (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "()" (G (PlainModule "Prelude") "()" (N (Just _))), conArity = 0, conFields = Nothing}], fields = []})) (N (Just loc))))))
= return Star
exp2Global (Exp (HsId (HsVar (PNT (PN (UnQual "undefined") (G (PlainModule "Prelude") "undefined" (N (Just _)))) _ (N (Just _))))))
= return Star
exp2Global (Exp (HsId (HsVar (PNT (PN (UnQual "_L") _) _ _))))
= return Star
-- Constants (inN,ouT, True, False,[],int)
-- inN (_L::typ) exp
exp2Global (Exp (HsApp (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "inN") _) _ (N (Just _)))))) (Exp (HsParen typ@(Exp (HsExpTypeSig _ (Exp (HsId (HsVar (PNT (PN (UnQual "_L") _) _ (N (Just _)))))) []
typ'
)))))) exp2))
= exp2Global exp2 >>= return . In' typ--(pp typ)
-- ouT (_L::typ) exp
exp2Global (Exp (HsApp (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "ouT") _) _ (N (Just _)))))) (Exp (HsParen typ@(Exp (HsExpTypeSig _ (Exp (HsId (HsVar (PNT (PN (UnQual "_L") _) _ (N (Just _)))))) []
typ'
)))))) exp2))
= exp2Global exp2 >>= return . Out' typ --(pp typ)
-- True
exp2Global (Exp (HsId (HsCon (PNT (PN (UnQual "True") (G (PlainModule "Prelude") "True" (N (Just _)))) (ConstrOf (PN "Bool" (G (PlainModule "Prelude") "Bool" (N (Just _)))) (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "False" (G (PlainModule "Prelude") "False" (N (Just _))), conArity = 0, conFields = Nothing},ConInfo {conName = PN "True" (G (PlainModule "Prelude") "True" (N (Just _))), conArity = 0, conFields = Nothing}], fields = []})) (N (Just _))))))
= return T'
-- False
exp2Global (Exp (HsId (HsCon (PNT (PN (UnQual "False") (G (PlainModule "Prelude") "False" (N (Just _)))) (ConstrOf (PN "Bool" (G (PlainModule "Prelude") "Bool" (N (Just _)))) (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "False" (G (PlainModule "Prelude") "False" (N (Just _))), conArity = 0, conFields = Nothing},ConInfo {conName = PN "True" (G (PlainModule "Prelude") "True" (N (Just _))), conArity = 0, conFields = Nothing}], fields = []})) (N (Just _))))))
= return F'
-- Zero
exp2Global (Exp (HsLit _ (HsInt 0)))
= return Z'
-- []
exp2Global ((Exp (HsList [])))
= return N'
-- n>0
exp2Global (Exp (HsLit _ (HsInt n)))
| n > 0 = exp2Global (Exp $ HsLit loc0 $ HsInt (n-1)) >>= return . Suc
------ recursion
-- recNat
exp2Global (Exp (HsApp (Exp (HsApp (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "recNat") _) _ _)))) exp1)) exp2)) exp3))
= do term1 <- exp2Global exp1
term2 <- exp2Global exp2
term3 <- exp2Global exp3
return $ RecNat term1 term2 term3
-- recList
exp2Global (Exp (HsApp (Exp (HsApp (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "recList") _) _ _)))) exp1)) exp2)) exp3))
= do term1 <- exp2Global exp1
term2 <- exp2Global exp2
term3 <- exp2Global exp3
return $ RecList term1 term2 term3
-- fix exp
exp2Global (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "fix") _) _ _)))) exp))
= do term1 <- exp2Global exp
return $ Fix' term1
-- let var = exp1 -> exp2
exp2Global (Exp (HsLet [Dec (HsPatBind _ (Pat (HsPId (HsVar (PNT (PN (UnQual str) _) _ _)))) (HsBody exp1) [])] exp2))
= do t1 <- exp2Global exp1
t2 <- exp2Global exp2
return $ Letrec str t1 t2
------ remaining operators
-- succ exp
exp2Global (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "succ") _) _ (N (Just _)))))) e))
= do t <- exp2Global e
return $ Suc t
-- pred exp
exp2Global (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "pred") _) _ (N (Just _)))))) e))
= do t <- exp2Global e
return $ Pred t
-- (== 0) exp
exp2Global (Exp (HsApp (Exp (HsRightSection (HsVar (PNT (PN (UnQual "==") (G (PlainModule "Prelude") "==" (N (Just _)))) (MethodOf (PN "Eq" (G (PlainModule "Prelude") "Eq" (N (Just _)))) _ [PN "==" (G (PlainModule "Prelude") "==" (N (Just _))),PN "/=" (G (PlainModule "Prelude") "/=" (N (Just _)))]) _)) (Exp (HsLit _ (HsInt 0))))) exp))
= do t <- exp2Global exp
return $ IsZ t
-- exp == 0
exp2Global (Exp (HsInfixApp exp (HsVar (PNT (PN (UnQual "==") (G (PlainModule "Prelude") "==" (N (Just _)))) (MethodOf (PN "Eq" (G (PlainModule "Prelude") "Eq" (N (Just _)))) _ [PN "==" (G (PlainModule "Prelude") "==" (N (Just _))),PN "/=" (G (PlainModule "Prelude") "/=" (N (Just _)))]) (N (Just _)))) (Exp (HsLit _ (HsInt 0)))))
= do t <- exp2Global exp
return $ IsZ t
-- [exp1, exp2, ... ]
exp2Global (Exp (HsList (e1:e2)))
= do t1 <- exp2Global e1
t2 <- exp2Global (Exp (HsList e2))
return $ t1 ::: t2
-- x : xs
exp2Global (Exp (HsInfixApp e1 (HsCon (PNT (PN (UnQual ":") (G (PlainModule "Prelude") ":" (N (Just _)))) (ConstrOf (PN "[]" (G (PlainModule "Prelude") "[]" (N (Just _)))) (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "[]" (G (PlainModule "Prelude") "[]" (N (Just _))), conArity = 0, conFields = Nothing},ConInfo {conName = PN ":" (G (PlainModule "Prelude") ":" (N (Just _))), conArity = 2, conFields = Nothing}], fields = []})) (N (Just _)))) e2))
= do t1 <- exp2Global e1
t2 <- exp2Global e2
return $ t1 ::: t2
-- head exp
exp2Global (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "head") _) _ (N (Just _)))))) e))
= do t <- exp2Global e
return $ Hd t
-- tail exp
exp2Global (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "tail") _) _ (N (Just _)))))) e))
= do t <- exp2Global e
return $ Tl t
-- null exp
exp2Global (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "null") _) _ (N (Just _)))))) e))
= do t <- exp2Global e
return $ IsN t
-- if exp1 then exp2 else exp3
exp2Global (Exp (HsIf e1 e2 e3)) =
do t1 <- exp2Global e1
t2 <- exp2Global e2
t3 <- exp2Global e3
return $ Ite t1 t2 t3
-- var
exp2Global (Exp (HsId (HsVar (PNT (PN (UnQual str) _) _ (N (Just _))))))
= return $ V str
-- pairs
exp2Global (Exp (HsTuple [e1,e2]))
= do t1 <- exp2Global e1
t2 <- exp2Global e2
return $ t1 :&: t2
-- fst exp
exp2Global (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "fst") _) _ (N (Just _)))))) e))
= do t <- exp2Global e
return $ Pi1 t
-- snd exp
exp2Global (Exp (HsApp (Exp (HsId (HsVar (PNT (PN (UnQual "snd") _) _ (N (Just _)))))) e))
= do t <- exp2Global e
return $ Pi2 t
-- Left exp
exp2Global (Exp (HsApp (Exp (HsId (HsCon (PNT (PN (UnQual "Left") (G (PlainModule "Prelude") "Left" (N (Just _)))) (ConstrOf (PN "Either" (G (PlainModule "Prelude") "Either" (N (Just _)))) (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "Left" (G (PlainModule "Prelude") "Left" (N (Just _))), conArity = 1, conFields = Nothing},ConInfo {conName = PN "Right" (G (PlainModule "Prelude") "Right" (N (Just _))), conArity = 1, conFields = Nothing}], fields = []})) _)))) e))
= do t <- exp2Global e
return $ Inl' t
-- Right exp
exp2Global (Exp (HsApp (Exp (HsId (HsCon (PNT (PN (UnQual "Right") (G (PlainModule "Prelude") "Right" (N (Just _)))) (ConstrOf (PN "Either" (G (PlainModule "Prelude") "Either" (N (Just _)))) (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "Left" (G (PlainModule "Prelude") "Left" (N (Just _))), conArity = 1, conFields = Nothing},ConInfo {conName = PN "Right" (G (PlainModule "Prelude") "Right" (N (Just _))), conArity = 1, conFields = Nothing}], fields = []})) _)))) e))
= do t <- exp2Global e
return $ Inr' t
-- application
exp2Global (Exp (HsApp e1 e2)) =
do t1 <- exp2Global e1
t2 <- exp2Global e2
return $ t1 :-: t2
-- infix application
exp2Global (Exp (HsInfixApp e1 op e2)) =
do t1 <- exp2Global e1
t2 <- exp2Global e2
return $ (getOpName op) :-: t1 :-: t2
where getOpName ((HsVar (PNT (PN (UnQual op) _) _ _))) = V op
-- \ var -> exp
exp2Global (Exp (HsLambda [Pat (HsPId (HsVar (PNT (PN (UnQual str) _) _ _)))] e))
= do t <- exp2Global e
return $ Lam str t
-- \ var1 var2 ... -> exp
exp2Global (Exp (HsLambda (h@((Pat (HsPId (HsVar _)))):t) e))
= exp2Global (Exp (HsLambda [h] (Exp (HsLambda t e))))
-- case exp1 of Left var2 -> exp2; Right var3 -> exp3
exp2Global (Exp (HsCase exp1
[HsAlt _ (Pat (HsPApp (PNT (PN (UnQual "Left") (G (PlainModule "Prelude") "Left" (N (Just _)))) (ConstrOf (PN "Either" (G (PlainModule "Prelude") "Either" (N (Just _)))) (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "Left" (G (PlainModule "Prelude") "Left" (N (Just _))), conArity = 1, conFields = Nothing},ConInfo {conName = PN "Right" (G (PlainModule "Prelude") "Right" (N (Just _))), conArity = 1, conFields = Nothing}], fields = []})) (N (Just _))) [Pat (HsPId (HsVar (PNT (PN (UnQual str2) _) _ _)))])) (HsBody exp2) []
,HsAlt _ (Pat (HsPApp (PNT (PN (UnQual "Right") (G (PlainModule "Prelude") "Right" (N (Just _)))) (ConstrOf (PN "Either" (G (PlainModule "Prelude") "Either" (N (Just _)))) (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "Left" (G (PlainModule "Prelude") "Left" (N (Just _))), conArity = 1, conFields = Nothing},ConInfo {conName = PN "Right" (G (PlainModule "Prelude") "Right" (N (Just _))), conArity = 1, conFields = Nothing}], fields = []})) (N (Just _))) [Pat (HsPId (HsVar (PNT (PN (UnQual str3) _) _ _)))])) (HsBody exp3) []]))
= do t1 <- exp2Global exp1
t2 <- exp2Global exp2
t3 <- exp2Global exp3
return $ Case' t1 (str2,t2) (str3,t3)
exp2Global x = --mzero
--fail
error $ "not a Global term: "++ pp x
--------------------------------
------- global to core ---------
{- | Converts a 'GLTerm' to a 'PWTerm', which is a more general representation for
pointwise terms, but with less pratical constructors (in "PWCore").
-}
global2core :: GLTerm -> PWTerm
global2core Star = Unit
global2core (V str) = Var' str
global2core (Lam str t) = Abstr str (global2core t)
global2core (t1 :-: t2) = (global2core t1) :@: (global2core t2)
global2core (t1 :&: t2) = (global2core t1) :><: (global2core t2)
global2core (Pi1 t) = Fst (global2core t)
global2core (Pi2 t) = Snd (global2core t)
global2core T' = In boolT (Inl Unit)
global2core F' = In boolT (Inr Unit)
global2core Z' = In intT (Inl Unit)
global2core (Suc t) = In intT (Inr $ global2core t)
global2core (Pred t) =
Case (Out intT$ global2core t) ("_",In intT (Inl Unit))
("x", (Var' "x"))
global2core (IsZ t) =
Case (Out intT$ global2core t) ("_", In boolT (Inl Unit))
("_", In boolT (Inr Unit))
global2core (Ite t1 t2 t3) =
Case (Out boolT$ global2core t1) ("_", global2core t2)
("_", global2core t3)
global2core (Fix' t) = Fix (global2core t)
global2core N' = In listT (Inl Unit)
global2core (t1 ::: t2) = In listT (Inr ((global2core t1):><:(global2core t2)))
global2core (IsN t) =
Case (Out listT$ global2core t) ("_", In boolT (Inl Unit))
("_", In boolT (Inr Unit))
global2core (Hd t) =
Case (Out listT$ global2core t) ("_", Var' "undefined")
("x", Fst $ Var' "x")
global2core (Tl t) =
Case (Out listT$ global2core t) ("_", In listT (Inl Unit))
("x", Snd $ Var' "x")
global2core (Letrec str t1 t2) =
let func = (Fix (Abstr str (global2core t1)))
in (Abstr str (global2core t2)) :@: func
global2core (Inl' t) = Inl (global2core t)
global2core (Inr' t) = Inr (global2core t)
global2core (Case' a (s1,b) (s2,c)) =
Case (global2core a) (s1,global2core b) (s2,global2core c)
global2core (In' s t) = In s (global2core t)
global2core (Out' s t) = Out s (global2core t)
global2core (RecNat t1 t2 t3) =
(Fix $ Abstr "r" $ Abstr "n" $ Abstr "f" $ Abstr "z" $
Case (Out intT (Var' "n"))
("x", Var' "z")
("y", (Var' "f") :@: (Var' "y") :@:
((Var' "r"):@:(Var' "y"):@:(Var' "f"):@:(Var' "z"))))
:@: (global2core t1) :@: (global2core t2) :@: (global2core t3)
global2core (RecList t1 t2 t3) =
(Fix $ Abstr "r" $ Abstr "l" $ Abstr "f" $ Abstr "z" $
Case (Out listT (Var' "l"))
("x", Var' "z")
("y", (Var' "f") :@: (Fst$Var' "y") :@: (Snd$Var' "y") :@:
((Var' "r"):@:(Snd$Var' "y"):@:(Var' "f"):@:(Var' "z"))))
:@: (global2core t1) :@: (global2core t2) :@: (global2core t3)
---- expressions for (_L::Int)
-- (_L::Bool)
-- (_L::[a])
intT = mkType (Typ (HsTyCon (PNT (PN (UnQual "Int") (G (PlainModule "Prelude") "Int" (N (Just loc0)))) (Type (TypeInfo {defType = Just Primitive, constructors = [], fields = []})) (N (Just loc0)))))
boolT = mkType (Typ (HsTyCon (PNT (PN (UnQual "Bool") (G (PlainModule "Prelude") "Bool" (N (Just loc0)))) (Type (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "False" (G (PlainModule "Prelude") "False" (N (Just loc0))), conArity = 0, conFields = Nothing},ConInfo {conName = PN "True" (G (PlainModule "Prelude") "True" (N (Just loc0))), conArity = 0, conFields = Nothing}], fields = []})) (N (Just loc0)))))
listT = mkType (Typ (HsTyApp (Typ $ HsTyCon (PNT (PN (Qual (PlainModule "Prelude") "[]") (G (PlainModule "Prelude") "[]" (N (Just loc0)))) (Type (TypeInfo {defType = Just Data, constructors = [ConInfo {conName = PN "[]" (G (PlainModule "Prelude") "[]" (N (Just loc0))), conArity = 0, conFields = Nothing},ConInfo {conName = PN ":" (G (PlainModule "Prelude") ":" (N (Just loc0))), conArity = 2, conFields = Nothing}], fields = []})) (N (Just loc0)))) (Typ $ HsTyVar (PNT (PN (UnQual "a") (S loc0)) (Type (TypeInfo {defType = Nothing, constructors = [], fields = []})) (N (Just loc0))))))
mkType typ = Exp $ HsParen $ typedExp "_L" typ
typedExp strVar typ = Exp (HsExpTypeSig loc0 (nameToExp strVar) [] typ)