From 7420b2778565ed8d9cbba1329828c20598e82a7c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 2 Dec 2014 14:47:01 -0800 Subject: [PATCH] Add Parser AST constructor EInfFrom to represent [x...] and [x,y...] As a result, parsed terms including [x...] or [x,y...] now pretty-print back out using the same syntax. --- src/Cryptol/ModuleSystem/Renamer.hs | 1 + src/Cryptol/Parser.y | 4 ++-- src/Cryptol/Parser/AST.hs | 4 ++++ src/Cryptol/Parser/Names.hs | 2 ++ src/Cryptol/Parser/NoPat.hs | 2 ++ src/Cryptol/TypeCheck/Infer.hs | 7 +++++++ 6 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 3268e3a1..72a232b8 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -377,6 +377,7 @@ instance Rename Expr where ESel e' s -> ESel <$> rename e' <*> pure s EList es -> EList <$> rename es EFromTo s n e'-> EFromTo <$> rename s <*> rename n <*> rename e' + EInfFrom e e' -> EInfFrom<$> rename e <*> rename e' EComp e' bs -> do bs' <- mapM renameMatch bs shadowNames (namingEnv bs') (EComp <$> rename e' <*> pure bs') diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index 04deca43..411f3139 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -510,8 +510,8 @@ list_expr :: { Expr } | expr ',' expr '..' {% eFromTo $4 $1 (Just $3) Nothing } | expr ',' expr '..' expr {% eFromTo $4 $1 (Just $3) (Just $5) } - | expr '...' { EApp (ECon ECInfFrom) $1 } - | expr ',' expr '...' { EApp (EApp (ECon ECInfFromThen) $1) $3 } + | expr '...' { EInfFrom $1 Nothing } + | expr ',' expr '...' { EInfFrom $1 (Just $3) } list_alts :: { [[Match]] } diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 4abf7ec8..33b8d026 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -253,6 +253,7 @@ data Expr = EVar QName -- ^ @ x @ | ESel Expr Selector -- ^ @ e.l @ | EList [Expr] -- ^ @ [1,2,3] @ | EFromTo Type (Maybe Type) (Maybe Type) -- ^ @[1, 5 .. 117 ] @ + | EInfFrom Expr (Maybe Expr) -- ^ @ [1, 3 ...] @ | EComp Expr [[Match]] -- ^ @ [ 1 | x <- xs ] @ | EApp Expr Expr -- ^ @ f x @ | EAppT Expr [TypeInst] -- ^ @ f `{x = 8}, f`{8} @ @@ -665,6 +666,8 @@ instance PP Expr where EFromTo e1 e2 e3 -> brackets (pp e1 <> step <+> text ".." <+> end) where step = maybe empty (\e -> comma <+> pp e) e2 end = maybe empty pp e3 + EInfFrom e1 e2 -> brackets (pp e1 <> step <+> text "...") + where step = maybe empty (\e -> comma <+> pp e) e2 EComp e mss -> brackets (pp e <+> vcat (map arm mss)) where arm ms = text "|" <+> commaSep (map pp ms) ETypeVal t -> text "`" <> ppPrec 5 t -- XXX @@ -893,6 +896,7 @@ instance NoPos Expr where ESel x y -> ESel (noPos x) y EList x -> EList (noPos x) EFromTo x y z -> EFromTo (noPos x) (noPos y) (noPos z) + EInfFrom x y -> EInfFrom (noPos x) (noPos y) EComp x y -> EComp (noPos x) (noPos y) EApp x y -> EApp (noPos x) (noPos y) EAppT x y -> EAppT (noPos x) (noPos y) diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index daa8a75d..6b7fb72d 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -84,6 +84,7 @@ namesE expr = ESel e _ -> namesE e EList es -> Set.unions (map namesE es) EFromTo _ _ _ -> Set.empty + EInfFrom e e' -> Set.union (namesE e) (maybe Set.empty namesE e') EComp e arms -> let (dss,uss) = unzip (map namesArm arms) in Set.union (boundNames (concat dss) (namesE e)) (Set.unions uss) @@ -194,6 +195,7 @@ tnamesE expr = EList es -> Set.unions (map tnamesE es) EFromTo a b c -> Set.union (tnamesT a) (Set.union (maybe Set.empty tnamesT b) (maybe Set.empty tnamesT c)) + EInfFrom e e' -> Set.union (tnamesE e) (maybe Set.empty tnamesE e') EComp e mss -> Set.union (tnamesE e) (Set.unions (map tnamesM (concat mss))) EApp e1 e2 -> Set.union (tnamesE e1) (tnamesE e2) EAppT e fs -> Set.union (tnamesE e) (Set.unions (map tnamesTI fs)) diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index a3ffd223..117591fb 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -25,6 +25,7 @@ import Control.Applicative(Applicative(..),(<$>)) import Data.Maybe(maybeToList) import Data.Either(partitionEithers) import qualified Data.Map as Map +import Data.Traversable(traverse) class RemovePatterns t where @@ -147,6 +148,7 @@ noPatE expr = ESel e s -> ESel <$> noPatE e <*> return s EList es -> EList <$> mapM noPatE es EFromTo {} -> return expr + EInfFrom e e' -> EInfFrom <$> noPatE e <*> traverse noPatE e' EComp e mss -> EComp <$> noPatE e <*> mapM noPatArm mss EApp e1 e2 -> EApp <$> noPatE e1 <*> noPatE e2 EAppT e ts -> EAppT <$> noPatE e <*> return ts diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index d1320bdf..7a7ef927 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -133,6 +133,7 @@ appTys expr ts = P.ESel {} -> mono P.EList {} -> mono P.EFromTo {} -> mono + P.EInfFrom {} -> mono P.EComp {} -> mono P.EApp {} -> mono P.EIf {} -> mono @@ -249,6 +250,12 @@ inferE expr = | (x,y) <- ("first",t1) : fs ] + P.EInfFrom e1 Nothing -> + inferE $ P.EApp (P.ECon ECInfFrom) e1 + + P.EInfFrom e1 (Just e2) -> + inferE $ P.EApp (P.EApp (P.ECon ECInfFromThen) e1) e2 + P.EComp e mss -> do (mss', dss, ts) <- unzip3 `fmap` zipWithM inferCArm [ 1 .. ] mss w <- smallest ts