----------------------------------------------------------------------------- -- | -- 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)