diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -1,5 +1,5 @@ name: language-ats -version: 0.2.0.1 +version: 0.2.0.2 synopsis: Parser and pretty-printer for ATS. description: Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex. license: BSD3 diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x --- a/src/Language/ATS/Lexer.x +++ b/src/Language/ATS/Lexer.x @@ -100,10 +100,8 @@ tokens :- $white+ ; - @block_comment { tok (\p s -> CommentLex p s) } - "//".* { tok (\p s -> CommentLex p s) } - -- "//".* ; - -- @block_comment ; + @block_comment { tok (\p s -> CommentLex p s) } + "//".* { tok (\p s -> CommentLex p s) } "#define".* { tok (\p s -> MacroBlock p s) } @if_block { tok (\p s -> MacroBlock p s) } @c_block { tok (\p s -> CBlockLex p s) } @@ -116,6 +114,9 @@ prfun { tok (\p s -> Keyword p KwPrfun) } datatype { tok (\p s -> Keyword p KwDatatype) } data @view type { tok (\p s -> Keyword p KwDatavtype) } + @view type { tok (\p s -> Keyword p (KwVtype None)) } + @view type"+" { tok (\p s -> Keyword p (KwVtype Plus)) } + @view type"-" { tok (\p s -> Keyword p (KwVtype Minus)) } dataview { tok (\p s -> Keyword p KwDataview) } dataprop { tok (\p s -> Keyword p KwDataprop) } assume { tok (\p s -> Keyword p KwAssume) } @@ -238,6 +239,7 @@ get_staload _ = undefined get_addendum (Keyword _ (KwVal a)) = a +get_addendum (Keyword _ (KwVtype a)) = a get_addendum _ = undefined data Keyword = KwFun @@ -248,6 +250,7 @@ | KwAssume | KwTypedef | KwVtypedef + | KwVtype Addendum | KwStaload Bool | KwLet | KwIn @@ -343,6 +346,7 @@ instance Pretty Keyword where pretty KwFun = "fun" + pretty (KwVtype a) = "vtype" <> pretty a pretty KwAnd = "and" pretty KwDatatype = "datatype" pretty KwDatavtype = "datavtype" -- FIXME this wrongly squashes dataviewtype diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y --- a/src/Language/ATS/Parser.y +++ b/src/Language/ATS/Parser.y @@ -90,6 +90,7 @@ sortdef { Keyword $$ KwSortdef } local { Keyword $$ KwLocal } view { Keyword $$ (KwView None) } + vtype { $$@(Keyword _ KwVtype{}) } viewPlusMinus { Keyword _ (KwView $$) } raise { Keyword $$ KwRaise } tkindef { Keyword $$ KwTKind } @@ -439,7 +440,8 @@ | vt0pPlain { Vt0p None } | vt0pCo { Vt0p Plus } | addr { Addr } - | view { View $1 None } + | view { View $1 None } + | vtype { VType (token_posn $1) (get_addendum $1) } | IdentifierOr { NamedSort $1 } QuantifierArgs : IdentifierOr { [$1] } @@ -451,11 +453,15 @@ | openExistential QuantifierArgs colon Sort vbar StaticExpression rsqbracket { Existential $2 True (Just $4) (Just $6) } | lsqbracket StaticExpression rsqbracket { Existential mempty False Nothing (Just $2) } +Predicates : { [] } + | StaticExpression { [$1] } + | Predicates semicolon StaticExpression { $3 : $1 } + -- | Parse a universal quantifier on a type -Universal : lbrace QuantifierArgs rbrace { Universal $2 Nothing Nothing } - | lbrace QuantifierArgs vbar StaticExpression rbrace { Universal $2 Nothing (Just $4) } - | lbrace QuantifierArgs colon Sort rbrace { Universal $2 (Just $4) Nothing } - | lbrace QuantifierArgs colon Sort vbar StaticExpression rbrace { Universal $2 (Just $4) (Just $6) } +Universal : lbrace QuantifierArgs rbrace { Universal $2 Nothing [] } + | lbrace QuantifierArgs vbar Predicates rbrace { Universal $2 Nothing $4 } + | lbrace QuantifierArgs colon Sort rbrace { Universal $2 (Just $4) [] } + | lbrace QuantifierArgs colon Sort vbar Predicates rbrace { Universal $2 (Just $4) $6 } Implicits : lspecial TypeIn rbracket { [$2] } | Implicits lspecial TypeIn rbracket { $3 : $1 } @@ -499,7 +505,7 @@ | dollar tempenver { SpecialName $1 "tempenver" } | dollar extype { SpecialName $1 "effmask_all" } | dollar listVT { SpecialName $1 "list_vt" } - | dollar ldelay { SpecialName $1 "ldelay" } -- FIXME there is probably a better/more efficient way of doing this + | dollar ldelay { SpecialName $1 "ldelay" } -- FIXME there is probably a better way of doing this | dollar {% Left $ Expected $1 "Name" "$" } -- | Parse a list of values in a record @@ -608,13 +614,14 @@ | lsqbracket {% Left $ Expected $1 "Function signature" "[" } -- | Parse affiliated `sortdef`s -AndSort : AndSort and IdentifierOr eq Sort { AndD $1 (SortDef $2 $3 $5) } -- TODO figure out if this is building up the slow way - | sortdef IdentifierOr eq Sort { SortDef $1 $2 $4 } +AndSort : AndSort and IdentifierOr eq Sort { AndD $1 (SortDef $2 $3 (Left $5)) } -- TODO figure out if this is building up the slow way + | sortdef IdentifierOr eq Sort { SortDef $1 $2 (Left $4) } + | sortdef IdentifierOr eq Universal { SortDef $1 $2 (Right $4) } AndStadef : stadef IdentifierOr eq Name { Stadef $2 $4 [] } | stadef IdentifierOr eq identifierSpace { Stadef $2 (Unqualified $ to_string $4) [] } - | AndStadef and stadef IdentifierOr eq identifierSpace { AndD $1 (Stadef $4 (Unqualified $ to_string $6) []) } - | AndStadef and stadef IdentifierOr eq identifier { AndD $1 (Stadef $4 (Unqualified $ to_string $6) []) } + | AndStadef and IdentifierOr eq identifierSpace { AndD $1 (Stadef $3 (Unqualified $ to_string $5) []) } + | AndStadef and IdentifierOr eq identifier { AndD $1 (Stadef $3 (Unqualified $ to_string $5) []) } StafunDecl : prfun PreFunction { Func $1 (PrFun $2) } | prfn PreFunction { Func $1 (PrFn $2) } @@ -667,7 +674,7 @@ | vtypedef IdentifierOr SortArgs eq Type { ViewTypeDef $1 $2 $3 $5 } | datatype IdentifierOr SortArgs eq Leaves { SumType $2 $3 $5 } | datavtype IdentifierOr SortArgs eq Leaves { SumViewType $2 $3 $5 } - | abst0p IdentifierOr eq Type { AbsT0p $1 $2 $4 } + | abst0p IdentifierOr SortArgs MaybeType { AbsT0p $1 $2 $3 $4 } | viewdef IdentifierOr openParen FullArgs closeParen eq Type { ViewDef $1 $2 $4 $7 } | absvt0p IdentifierOr SortArgs eq Type { AbsVT0p $1 $2 $3 (Just $5) } | absview IdentifierOr openParen FullArgs closeParen MaybeType { AbsView $1 $2 $4 $6 } diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -273,6 +273,7 @@ pretty (NamedSort s) = text s pretty Addr = "addr" pretty (View _ t) = "view" <> pretty t + pretty (VType _ a) = "vtype" <> pretty a instance Pretty Type where pretty = cata a where @@ -315,11 +316,11 @@ pretty (Existential bs b st (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan st <> "|" <+> pretty e <+> rbracket instance Pretty Universal where - pretty (Universal [x] Nothing Nothing) = lbrace <> text x <> rbrace - pretty (Universal [x] (Just st) Nothing) = lbrace <> text x <> ":" <> pretty st <> rbrace - pretty (Universal bs Nothing Nothing) = lbrace <> mconcat (punctuate "," (fmap pretty (reverse bs))) <> rbrace - pretty (Universal bs (Just ty) Nothing) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <+> ":" <+> pretty ty <+> rbrace - pretty (Universal bs ty (Just e)) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <> "|" <+> pretty e <+> rbrace + pretty (Universal [x] Nothing []) = lbrace <> text x <> rbrace + pretty (Universal [x] (Just st) []) = lbrace <> text x <> ":" <> pretty st <> rbrace + pretty (Universal bs Nothing []) = lbrace <> mconcat (punctuate "," (fmap pretty (reverse bs))) <> rbrace + pretty (Universal bs (Just ty) []) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <+> ":" <+> pretty ty <+> rbrace + pretty (Universal bs ty es) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <> "|" <+> mconcat (punctuate "; " (fmap pretty es)) <+> rbrace instance Pretty ATS where pretty (ATS xs) = concatSame (fmap rewriteDecl xs) @@ -569,10 +570,10 @@ pretty (AndD d (Stadef i n as)) = pretty d <+> "and" <+> text i <+> pretty n <> prettyArgs as pretty (AbsView _ i as t) = "absview" <+> text i <> prettyArgs as <> prettyMaybeType t pretty (AbsVT0p _ i as t) = "absvt@ype" <+> text i <> prettySortArgs as <> prettyMaybeType t - pretty (AbsT0p _ i t) = "abst@ype" <+> text i <+> "=" <+> pretty t + pretty (AbsT0p _ i as t) = "abst@ype" <+> text i <> prettySortArgs as <> "=" <+> pretty t pretty (ViewDef _ s [] t) = "viewdef" <+> text s <+> "=" <#> pretty t pretty (ViewDef _ s as t) = "viewdef" <+> text s <> prettyArgs as <+> "=" <#> pretty t pretty (TKind _ n s) = pretty n <+> "=" <+> text s - pretty (SortDef _ s t) = "sortdef" <+> text s <+> "=" <+> pretty t - pretty (AndD d (SortDef _ i t)) = pretty d <+> "and" <+> text i <+> "=" <+> pretty t + pretty (SortDef _ s t) = "sortdef" <+> text s <+> "=" <+> either pretty pretty t + pretty (AndD d (SortDef _ i t)) = pretty d <+> "and" <+> text i <+> "=" <+> either pretty pretty t pretty AndD{} = undefined -- probably not valid syntax if we get to this point diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -99,7 +99,7 @@ | AbsViewType AlexPosn String SortArgs (Maybe Type) | AbsView AlexPosn String [Arg] (Maybe Type) | AbsVT0p AlexPosn String SortArgs (Maybe Type) - | AbsT0p AlexPosn String Type + | AbsT0p AlexPosn String SortArgs (Maybe Type) | ViewDef AlexPosn String [Arg] Type | OverloadOp AlexPosn BinOp Name | OverloadIdent AlexPosn String Name (Maybe Int) @@ -107,7 +107,7 @@ | DataProp AlexPosn String SortArgs [DataPropLeaf] | Extern AlexPosn Declaration | Define String - | SortDef AlexPosn String Sort + | SortDef AlexPosn String (Either Sort Universal) | AndD Declaration Declaration | Local AlexPosn ATS ATS | AbsProp AlexPosn String [Arg] @@ -196,12 +196,13 @@ | T0p Addendum -- ^ t@ype | Vt0p Addendum -- ^ vt@ype | Addr + | VType AlexPosn Addendum -- ^ viewtype or vtype | View AlexPosn Addendum -- ^ view deriving (Show, Eq, Generic, NFData) -- FIXME a type for sorts? -- | Wrapper for universal quantifiers (refinement types) -data Universal = Universal { bound :: [String], typeU :: Maybe Sort, prop :: Maybe StaticExpression } -- TODO NonEmpty type? +data Universal = Universal { bound :: [String], typeU :: Maybe Sort, prop :: [StaticExpression] } deriving (Show, Eq, Generic, NFData) -- | Wrapper for existential quantifiers/types