module Language.Pointwise.Parser where import Language.Pointwise.Syntax as Pointwise import Language.Haskell.Exts.Syntax as Exts import Language.Haskell.Exts.Pretty import Data.Char {- Parsing of a Exp to a pointwise term. It recognizes: G, G1, G2 ::= (G) | undefined | _L | inn G | out G | 'literal' | 'var' | fix G | (G1,G2) | fst G | snd G | Left G | RightG | G1 G2 | \ 'var' -> G | case G of Left var1 -> G1 ; Right var2 -> G2 | case G of Right var1 -> G1 ; Left var2 -> G2 | case G of ... -} mkVar = Exts.Var . UnQual . Ident hs2pw :: Exp -> Maybe Term hs2pw (Paren e) = hs2pw e -- unit -> "undefined" or "_L" hs2pw (Exts.Var(UnQual(Ident "undefined"))) = return $ Unit hs2pw (Exts.Var(UnQual(Ident "_L"))) = return $ Unit -- Constants hs2pw (App (Exts.Var (UnQual (Ident "inn"))) exp) = hs2pw exp >>= return . In hs2pw (App (Exts.Var (UnQual (Ident "out"))) exp) = hs2pw exp >>= return . Out hs2pw (Lit lit) = return $ Const $ prettyPrint lit hs2pw (Exts.Var(UnQual(Ident str))) = return $ Pointwise.Var str hs2pw (InfixApp e1 (QConOp (Special Cons)) e2) = do t1 <- hs2pw e1 t2 <- hs2pw e2 return $ ((Const ":") :@: t1) :@: t2 hs2pw (List []) = return $ Const "[]" hs2pw (List (x:xs)) = do e <- hs2pw x es <- hs2pw (List xs) return $ ((Const ":") :@: e) :@: es -- Recursion hs2pw (App (Exts.Var (UnQual (Ident "fix"))) exp) = do term <- hs2pw exp return $ Fix term -- remaining hs2pw (Tuple [e1,e2]) = do t1 <- hs2pw e1 t2 <- hs2pw e2 return $ t1 :&: t2 hs2pw (App (Exts.Var (UnQual (Ident "fst"))) e) = do t <- hs2pw e return $ Fst t hs2pw (App (Exts.Var (UnQual (Ident "snd"))) e) = do t <- hs2pw e return $ Snd t hs2pw (App (Con (UnQual (Ident "Left"))) e) = do t <- hs2pw e return $ Inl t hs2pw (App (Con (UnQual (Ident "Right"))) e) = do t <- hs2pw e return $ Inr t hs2pw (App e1 e2) = do t1 <- hs2pw e1 t2 <- hs2pw e2 return $ t1 :@: t2 hs2pw (Lambda _ [PVar(Ident str)] e) = do t <- hs2pw e return $ Lam str t -- in "case of"'s, guards fail and declarations are lost hs2pw (Exts.Case e1 [Alt _ (PApp (UnQual(Ident "Left")) [PVar(Ident str2)]) (UnGuardedAlt e2) _, Alt _ (PApp (UnQual(Ident "Right")) [PVar(Ident str3)]) (UnGuardedAlt e3) _]) = do t1 <- hs2pw e1 t2 <- hs2pw e2 t3 <- hs2pw e3 return $ Pointwise.Case t1 (Lam str2 t2) (Lam str3 t3) hs2pw (Exts.Case e1 [Alt _ (PApp (UnQual(Ident "Right")) [PVar(Ident str3)]) (UnGuardedAlt e3) _, Alt _ (PApp (UnQual(Ident "Left")) [PVar(Ident str2)]) (UnGuardedAlt e2) _]) = do t1 <- hs2pw e1 t2 <- hs2pw e2 t3 <- hs2pw e3 return $ Pointwise.Case t1 (Lam str2 t2) (Lam str3 t3) hs2pw (Exts.Case e alts) = do t1 <- hs2pw e ts <- mapM alt2pws alts return $ Pointwise.Match t1 ts where alt2pws (Alt _ pat (UnGuardedAlt e) _) = do tp <- pat2pw pat te <- hs2pw e return (tp,te) alt2pws _ = fail "No guards allowed." hs2pw (Con (UnQual (Ident x))) = return $ Const x hs2pw t = fail $ "'"++prettyPrint t++ "' is not a valid pointwise term." hsPat2Exp :: Pat -> Exp hsPat2Exp (Exts.PVar hsName) = Exts.Var $ UnQual hsName hsPat2Exp (PLit hsLiteral) = Lit hsLiteral hsPat2Exp (PNeg hsPat) = NegApp . hsPat2Exp $ hsPat hsPat2Exp (PInfixApp hsPat1 hsQName hsPat2) = let hsExp1 = hsPat2Exp hsPat1 hsExp2 = hsPat2Exp hsPat2 hsQOp = (if f hsQName then QConOp else QVarOp) hsQName in InfixApp hsExp1 hsQOp hsExp2 where f (Qual _ name) = g name f (UnQual name) = g name f (Special _ ) = True g (Ident name) = isUpper $ head name g (Symbol str) = isUpper $ head str hsPat2Exp (PApp hsQName []) = Con hsQName hsPat2Exp (PApp hsQName lPat) = foldl App (Con hsQName) . map hsPat2Exp $ lPat hsPat2Exp (PTuple lPat) = Tuple $ map hsPat2Exp lPat hsPat2Exp (PList lPat) = List $ map hsPat2Exp lPat hsPat2Exp (PParen hsPat) = Paren $ hsPat2Exp hsPat hsPat2Exp (PRec hsQName lPatField) = RecConstr hsQName (map f lPatField) where f (PFieldPat hsQName hsPat) = FieldUpdate hsQName $ hsPat2Exp hsPat --hsPat2Exp (PAsPat hsName hsPat) = AsPat hsName (hsPat2Exp hsPat) hsPat2Exp (PWildCard) = mkVar "_L" --hsPat2Exp (PIrrPat hsPat) = IrrPat $ hsPat2Exp hsPat -- this approach may be changed... pat2pw = hs2pw . hsPat2Exp