diff --git a/Justfile b/Justfile --- a/Justfile +++ b/Justfile @@ -1,5 +1,6 @@ approve FILE: @atsfmt test/data/{{ FILE }} -o > test/data/$(echo {{ FILE }} | sed 's/\(dats\|sats\)/out/') + sed -i '$d' test/data/$(echo {{ FILE }} | sed 's/\(dats\|sats\)/out/') next: @export VERSION=$(ac ats-format.cabal | grep -P -o '\d+\.\d+\.\d+\.\d+' ats-format.cabal | head -n1 | awk -F. '{$NF+=1; print $0}' | sed 's/ /\./g') && echo $VERSION && sed -i "2s/[0-9]\+\.[0-9]\+\.[0-9]\+\.[0-9]\+/$VERSION/" ats-format.cabal diff --git a/ats-format.cabal b/ats-format.cabal --- a/ats-format.cabal +++ b/ats-format.cabal @@ -1,5 +1,5 @@ name: ats-format -version: 0.1.0.16 +version: 0.1.0.17 synopsis: A source-code formatter for ATS description: An opinionated source-code formatter for ATS (http://www.ats-lang.org/). homepage: https://hub.darcs.net/vmchale/ats-format#readme @@ -41,6 +41,7 @@ , Language.ATS.Parser , Language.ATS.PrettyPrint , Language.ATS.Exec + , Language.ATS.Doc , Paths_ats_format build-depends: base >= 4.8 && < 5 , array @@ -55,6 +56,8 @@ , megaparsec , unordered-containers , text + , blaze-markup + , blaze-html , directory , process , file-embed diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs --- a/src/Language/ATS.hs +++ b/src/Language/ATS.hs @@ -3,6 +3,8 @@ lexATS , parseATS , printATS + -- * Documentation generation + , generateATSDocs -- * Syntax Tree , ATS (..) , Declaration (..) @@ -33,6 +35,7 @@ , exec ) where +import Language.ATS.Doc import Language.ATS.Exec import Language.ATS.Lexer import Language.ATS.Parser diff --git a/src/Language/ATS/Doc.hs b/src/Language/ATS/Doc.hs new file mode 100644 --- /dev/null +++ b/src/Language/ATS/Doc.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Language.ATS.Doc ( generateATSDocs + ) where + +import Language.ATS.Types +import Text.Blaze.Html5 + +generateATSDocs :: ATS -> Html +generateATSDocs = toHtml . markupATS + +markupATS :: ATS -> Markup +markupATS _ = html $ + body $ do + p "First paragraph" + p "Second paragraph" 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 @@ -74,9 +74,9 @@ @ref_call = ($alpha | $digit | "(" | ")" | _ | (","))+ ">" @not_close_c = \% [^\}] -@c_block = \%\{ ("#" | "$" | "^" | "") ([^\%] | @not_close_c | \n)* \%\} -- TODO include %{# and %{$ +@c_block = \%\{ ("#" | "$" | "^" | "") ([^\%] | @not_close_c | \n)* \%\} -@inner_signature = ("!wrt" | "!exn" | "!exnwrt" | "0" | "1" | "!all" | "!laz" | "lin" | "fun" | "clo" | "cloptr" | "cloref" | "!ntm" | "!ref" | "prf" | @block_comment) +@inner_signature = ("!wrt" | "!exn" | "!exnwrt" | "0" | "1" | "!all" | "!laz" | "lin" | "fun" | "clo" | "cloptr" | "cloref" | "!ntm" | "!ref" | "prf" | "fe" | @block_comment) @inner_signature_mult = (@inner_signature (("," | "") @inner_signature)*) | "" @lambda = "=>" | "=>>" | "=<" @inner_signature_mult ">" @@ -96,8 +96,8 @@ tokens :- $white+ ; - ^ @block_comment { tok (\p s -> CommentLex p s) } - ^ "//".* { tok (\p s -> CommentLex p s) } + ^ @block_comment { tok (\p s -> CommentLex p s) } + ^ "//".* { tok (\p s -> CommentLex p s) } "//".* ; @block_comment ; "#define".* { tok (\p s -> MacroBlock p s) } @@ -145,6 +145,7 @@ primplmnt { tok (\p s -> Keyword p KwProofImplement) } primplement { tok (\p s -> Keyword p KwProofImplement) } -- TODO does this squash too much? abst"@"ype { tok (\p s -> Keyword p (KwAbst0p None)) } + abs@view"t@ype" { tok (\p s -> Keyword p (KwAbsvt0p None)) } t"@"ype"+" { tok (\p s -> Keyword p (KwT0p Plus)) } t"@"ype"-" { tok (\p s -> Keyword p (KwT0p Minus)) } t"@"ype { tok (\p s -> Keyword p (KwT0p None)) } @@ -154,11 +155,15 @@ abstype { tok (\p s -> Keyword p KwAbstype) } abs @view type { tok (\p s -> Keyword p KwAbsvtype) } absview { tok (\p s -> Keyword p KwAbsview) } - view { tok (\p s -> Keyword p KwView) } + view { tok (\p s -> Keyword p (KwView None)) } + view"+" { tok (\p s -> Keyword p (KwView Plus)) } + view"-" { tok (\p s -> Keyword p (KwView Minus)) } + viewdef { tok (\p s -> Keyword p KwViewdef) } "#"include { tok (\p s -> Keyword p KwInclude) } when { tok (\p s -> Keyword p KwWhen) } of { tok (\p s -> Keyword p KwOf) } stadef { tok (\p s -> Keyword p KwStadef) } + stacst { tok (\p s -> Keyword p KwStacst) } local { tok (\p s -> Keyword p KwLocal) } praxi { tok (\p s -> Keyword p KwPraxi) } while { tok (\p s -> Keyword p KwWhile) } @@ -177,11 +182,14 @@ "prerrln!" { tok (\p s -> Identifier p s) } "fix@" { tok (\p s -> Keyword p KwFixAt) } "lam@" { tok (\p s -> Keyword p KwLambdaAt) } + "addr" { tok (\p s -> Keyword p KwAddr) } "addr@" { tok (\p s -> Keyword p KwAddrAt) } "view@" { tok (\p s -> Keyword p KwViewAt) } sta { tok (\p s -> Keyword p KwSta) } symintr { tok (\p s -> Keyword p KwSymintr) } absview { tok (\p s -> Keyword p KwAbsview) } + "fold@" { tok (\p s -> Identifier p s) } + "free@" { tok (\p s -> Identifier p s) } @double_parens { tok (\p s -> DoubleParenTok p) } @double_braces { tok (\p s -> DoubleBracesTok p) } @double_brackets { tok (\p s -> DoubleBracketTok p) } @@ -197,6 +205,7 @@ @operator { tok (\p s -> Operator p s) } @signature { tok (\p s -> SignatureTok p (tail s)) } $special { tok (\p s -> Special p s) } + @identifier / " " { tok (\p s -> IdentifierSpace p s) } @identifier { tok (\p s -> Identifier p s) } @string { tok (\p s -> StringTok p s) } @@ -258,10 +267,11 @@ | KwChar | KwDataview | KwDataprop - | KwView + | KwView Addendum | KwAbstype | KwType | KwAbst0p Addendum + | KwAbsvt0p Addendum | KwT0p Addendum | KwVt0p Addendum | KwPrfun @@ -278,14 +288,17 @@ | KwFixAt | KwLambdaAt | KwAddrAt + | KwAddr | KwSta | KwViewAt + | KwViewdef | KwSymintr | KwAbsview | KwFn | KwInfix | KwInfixr | KwInfixl + | KwStacst deriving (Eq, Show, Generic, NFData) data Token = Identifier AlexPosn String @@ -297,6 +310,7 @@ | StringTok AlexPosn String | Special AlexPosn String | CBlockLex AlexPosn String + | IdentifierSpace AlexPosn String | Operator AlexPosn String | Arrow AlexPosn String | FuncType AlexPosn String @@ -359,11 +373,12 @@ pretty KwChar = "char" pretty KwDataview = "dataview" pretty KwDataprop = "dataprop" - pretty KwView = "view" + pretty (KwView c) = "view" <> pretty c pretty KwAbstype = "abstype" pretty KwAbsvtype = "absvtype" pretty KwType = "type" pretty (KwAbst0p c) = "abst@ype" <> pretty c + pretty (KwAbsvt0p c) = "absvt@ype" <> pretty c pretty (KwT0p c) = "t@ype" <> pretty c pretty (KwVt0p c) = "vt@ype" <> pretty c pretty KwPrfun = "prfun" @@ -379,8 +394,11 @@ pretty KwFixAt = "fix@" pretty KwLambdaAt = "lam@" pretty KwAddrAt = "addr@" + pretty KwAddr = "addr" pretty KwSta = "sta" + pretty KwStacst = "stacst" pretty KwViewAt = "view@" + pretty KwViewdef = "viewdef" pretty KwSymintr = "symintr" pretty KwAbsview = "absview" pretty KwFn = "fn" @@ -390,6 +408,7 @@ instance Pretty Token where pretty (Identifier _ s) = string s + pretty (IdentifierSpace _ s) = string s pretty (Keyword _ kw) = pretty kw pretty (BoolTok _ b) = string $ over _head toLower (show b) pretty (IntTok _ i) = pretty i @@ -411,6 +430,7 @@ pretty SpecialBracket{} = "{" token_posn (Identifier p _) = p +token_posn (IdentifierSpace p _) = p token_posn (Keyword p _) = p token_posn (BoolTok p _) = p token_posn (IntTok p _) = p 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 @@ -17,6 +17,7 @@ , token_posn ) +import Data.Char (toLower) import Control.DeepSeq (NFData) import Control.Lens (over, _head) import GHC.Generics (Generic) @@ -50,8 +51,12 @@ let { Keyword $$ KwLet } typedef { Keyword $$ KwTypedef } vtypedef { Keyword $$ KwVtypedef } + absview { Keyword $$ KwAbsview } absvtype { Keyword $$ KwAbsvtype } abstype { Keyword $$ KwAbstype } + abst0p { Keyword $$ (KwAbst0p None) } + absvt0p { Keyword $$ (KwAbsvt0p None) } + viewdef { Keyword $$ KwViewdef } in { Keyword $$ KwIn } end { Keyword $$ KwEnd } stringType { Keyword $$ KwString } @@ -63,6 +68,7 @@ bool { Keyword $$ KwBool } int { Keyword $$ KwInt } nat { Keyword $$ KwNat } + addr { Keyword $$ KwAddr } when { Keyword $$ KwWhen } begin { Keyword $$ KwBegin } case { Keyword _ (KwCase $$) } @@ -85,12 +91,15 @@ absprop { Keyword $$ KwAbsprop } sortdef { Keyword $$ KwSortdef } local { Keyword $$ KwLocal } - view { Keyword $$ KwView } + view { Keyword $$ (KwView None) } + viewPlusMinus { Keyword _ (KwView $$) } raise { Keyword $$ KwRaise } tkindef { Keyword $$ KwTKind } assume { Keyword $$ KwAssume } addrAt { Keyword $$ KwAddrAt } viewAt { Keyword $$ KwViewAt } + symintr { Keyword $$ KwSymintr } + stacst { Keyword $$ KwStacst } boolLit { BoolTok _ $$ } timeLit { TimeTok _ $$ } intLit { IntTok _ $$ } @@ -102,6 +111,7 @@ listVT { Identifier $$ "list_vt" } -- TODO token? raise { Identifier $$ "raise" } identifier { Identifier _ $$ } + identifierSpace { IdentifierSpace _ $$ } closeParen { Special $$ ")" } openParen { Special $$ "(" } signature { SignatureTok _ $$ } @@ -183,9 +193,11 @@ -- | Parse a type Type : Name openParen TypeInExpr closeParen { Dependent $1 $3 } + | identifierSpace openParen TypeInExpr closeParen { Dependent (Unqualified $1) $3 } | bool { Bool } | int { Int } | nat { Nat } + | addr { Addr } | stringType { String } | charType { Char } | voidType { Void } @@ -198,6 +210,7 @@ | int openParen StaticExpression closeParen { DependentInt $3 } | bool openParen StaticExpression closeParen { DependentBool $3 } | identifier { Named $1 } + | identifierSpace { Named $1 } | exclamation Type { Unconsumed $2 } | Type mutateArrow Type { FunctionType "->" $1 $3 } | Type funcArrow Type { FunctionType $2 $1 $3 } @@ -207,11 +220,13 @@ | Type prfTransform Type { AsProof $1 (Just $3) } | Type prfTransform underscore { AsProof $1 Nothing } | view at Type { ViewType $1 $3 } + | viewPlusMinus { ViewLiteral $1 } + | view { ViewLiteral None } | Existential Type { Ex $1 $2 } | Universal Type { ForA $1 $2 } | Type at Type { At $2 $1 $3 } | openParen Type vbar Type closeParen { ProofType $1 $2 $4 } - | Name identifier { Dependent $1 [Named $2] } + | identifierSpace identifier { Dependent (Unqualified $1) [Named $2] } | openParen TypeIn closeParen { Tuple $1 $2 } | openParen Type closeParen { $2 } | int StaticExpression { DependentInt $2 } @@ -227,9 +242,9 @@ -- | A comma-separated list of arguments Args : Arg { [$1] } + | FullArgs comma Arg vbar Arg { PrfArg $3 $5 : $1 } | Args comma Arg { $3 : $1 } | Arg vbar Arg { [ PrfArg $1 $3 ] } - | FullArgs comma Arg vbar Arg { PrfArg $3 $5 : $1 } Arg : identifier { Arg (First $1) } | identifier signature Type { Arg (Both $1 $3) } @@ -252,15 +267,18 @@ -- | Parse a pattern match Pattern : identifier { PName $1 [] } + | identifierSpace { PName $1 [] } | underscore { Wildcard $1 } | identifier doubleParens { PName ($1 ++ "()") [] } | tilde Pattern { Free $2 } | identifier openParen PatternIn closeParen { PName $1 $3 } | identifier Pattern { PSum $1 $2 } + | identifierSpace Pattern { PSum $1 $2 } | openParen PatternIn vbar PatternIn closeParen { Proof $1 $2 $4 } | openParen PatternIn closeParen { TuplePattern $2 } | Literal { PLiteral $1 } | Pattern when Expression { Guarded $2 $3 $1 } + | at Pattern { AtPattern $1 $2 } | minus {% Left $ Expected $1 "Pattern" "-" } | plus {% Left $ Expected $1 "Pattern" "+" } @@ -284,6 +302,7 @@ | spear { Spear $1 } | minus {% Left $ Expected $1 "Arrow" "-" } | eq {% Left $ Expected $1 "Arrow" "=" } + | minus {% Left $ Expected $1 "Arrow" "-" } LambdaArrow : plainArrow { Plain $1 } | cloref1Arrow { Full $1 "cloref1" } -- TODO do this more efficiently. @@ -296,11 +315,11 @@ -- | Expression or named call to an expression Expression : PreExpression { $1 } | openParen Tuple closeParen { TupleEx $1 $2 } - | Name PreExpression { Call $1 [] [] Nothing [$2] } + | identifierSpace PreExpression { Call (Unqualified $1) [] [] Nothing [$2] } | begin Expression end { Begin $1 $2 } | Expression semicolon Expression { Precede $1 $3 } | Expression semicolon { $1 } - | openParen Expression closeParen { ParenExpr $1 $2 } + | openParen Expression closeParen { $2 } | Expression signature Type { TypeSignature $1 $3 } | openParen Expression vbar Expression closeParen { ProofExpr $1 $2 $4 } @@ -314,12 +333,13 @@ | lbracket TypeIn rbrace { $2 } Call : Name doubleParens { Call $1 [] [] Nothing [] } + | identifierSpace openParen ExpressionPrf closeParen { Call (Unqualified $1) [] [] (fst $3) (snd $3) } | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) } | Name TypeArgs openParen ExpressionPrf closeParen { Call $1 [] $2 (fst $4) (snd $4) } | Name TypeArgs { Call $1 [] $2 Nothing [] } | Name lspecial TypeIn rbracket openParen ExpressionPrf closeParen { Call $1 $3 [] (fst $6) (snd $6) } | Name lspecial TypeIn rbracket { Call $1 $3 [] Nothing [] } - | dollar raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$3] } -- we do this because a $raise can have at most one argument + | dollar raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$3] } -- $raise can have at most one argument StaticArgs : StaticExpression { [$1] } | StaticArgs comma StaticExpression { $3 : $1 } @@ -327,19 +347,24 @@ StaticExpression : Name { StaticVal $1 } | StaticExpression BinOp StaticExpression { StaticBinary $2 $1 $3 } | intLit { StaticInt $1 } + | doubleParens { StaticVoid $1 } | boolLit { StaticBool $1 } | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 } -- TODO separate type for static expressions + | identifierSpace { StaticVal (Unqualified $1) } | Name openParen StaticArgs closeParen { SCall $1 $3 } + | identifierSpace openParen StaticArgs closeParen { SCall (Unqualified $1) $3 } + | StaticExpression semicolon StaticExpression { SPrecede $1 $3 } -- | Parse an expression that can be called without parentheses PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $1) $3 } | Literal { $1 } | Call { $1 } | case PreExpression of Case { Case $3 $1 $2 $4 } - | PreExpression BinOp Expression { Binary $2 $1 $3 } - | openParen PreExpression BinOp PreExpression closeParen { ParenExpr $1 (Binary $3 $2 $4) } + | openParen Expression closeParen { ParenExpr $1 $2 } + | PreExpression BinOp PreExpression { Binary $2 $1 $3 } | UnOp PreExpression { Unary $1 $2 } -- FIXME throw error when we try to negate a string literal/time | PreExpression dot Name { Access $2 $1 $3 } + | PreExpression dot identifierSpace { Access $2 $1 (Unqualified $3) } | if Expression then Expression { If $2 $4 Nothing} | if Expression then Expression else Expression { If $2 $4 (Just $6) } | let ATS in end { Let $1 $2 Nothing } @@ -352,9 +377,11 @@ | atbrace RecordVal rbrace { RecordValue $1 $2 Nothing } | atbrace RecordVal rbrace signature Type { RecordValue $1 $2 (Just $5) } | exclamation PreExpression { Deref $1 $2 } + | PreExpression mutateArrow identifierSpace mutateEq PreExpression { FieldMutate $2 $1 $3 $5 } | PreExpression mutateArrow identifier mutateEq PreExpression { FieldMutate $2 $1 $3 $5 } | PreExpression mutateEq PreExpression { Mutate $1 $3 } | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 } + | identifierSpace { NamedVal (Unqualified $1) } | Name { NamedVal $1 } | lbrace ATS rbrace { Actions $2 } | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 } @@ -366,7 +393,7 @@ | fromVT {% Left $ Expected $1 "Expression" "?!" } | prfTransform {% Left $ Expected $1 "Expression" ">>" } | maybeProof {% Left $ Expected $1 "Expression" "?" } - | let openParen {% Left $ Expected $1 "Declaration" "(" } + | let openParen {% Left $ Expected $1 "Expression" "let (" } -- | Parse a termetric Termetric : openTermetric StaticExpression closeTermetric { ($1, $2) } @@ -395,36 +422,42 @@ -- | Parse a function name FunName : identifier { Unqualified $1 } | identifier dollar identifier { Functorial $1 $3 } + | identifierSpace { Unqualified $1 } -- | Parse a general name Name : identifier { Unqualified $1 } | listVT { Unqualified "list_vt" } | dollar identifier dot identifier { Qualified $1 $4 $2 } + | dollar identifier dot identifierSpace { Qualified $1 $4 $2 } | dollar effmaskWrt { SpecialName $1 "effmask_wrt" } | dollar effmaskAll { 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 - | underscore {% Left $ Expected $1 "_" "Name" } - | dollar {% Left $ Expected $1 "$" "Name" } + | underscore {% Left $ Expected $1 "Name" "_" } + | dollar {% Left $ Expected $1 "Name" "$" } -- | Parse a list of values in a record RecordVal : identifier eq Expression { [($1, $3)] } + | identifierSpace eq Expression { [($1, $3)] } | RecordVal comma identifier eq Expression { ($3, $5) : $1 } + | RecordVal comma identifierSpace eq Expression { ($3, $5) : $1 } -- | Parse a list of types in a record Records : identifier eq Type { [($1, $3)] } + | identifierSpace eq Type { [($1, $3)] } | Records comma identifier eq Type { ($3, $5) : $1 } + | Records comma identifierSpace eq Type { ($3, $5) : $1 } -- | Parse a constructor for a sum type SumLeaf : vbar identifier { ($2, Nothing) } - | vbar identifier of Type { ($2, Just $4) } + | vbar identifierSpace of Type { ($2, Just $4) } -- | Parse all constructors of a sum type Leaves : SumLeaf { [$1] } | Leaves SumLeaf { $2 : $1 } - | identifier of Type { [($1, Just $3)] } + | identifierSpace of Type { [($1, Just $3)] } | identifier { [($1, Nothing)] } - | dollar {% Left $ Expected $1 "$" "|" } + | dollar {% Left $ Expected $1 "|" "$" } Universals : { [] } | doubleBraces { [] } @@ -459,8 +492,10 @@ | eq Expression { Just $2 } -- FIXME only let this happen for external declarations -- | Parse a constructor for a 'dataprop' -DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 } - | Universals Expression { DataPropLeaf $1 $2 } +DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 Nothing } + | Universals Expression { DataPropLeaf $1 $2 Nothing } + | vbar Universals Expression of Expression { DataPropLeaf $2 $3 (Just $5) } + | Universals Expression of Expression { DataPropLeaf $1 $2 (Just $4) } -- | Parse several constructors for a 'dataprop' DataPropLeaves : DataPropLeaf { [$1] } @@ -481,14 +516,16 @@ | FunName Universals OptTermetric doubleParens signature Type OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 } | FunName Universals OptTermetric openParen FullArgs closeParen signature Type OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 } | Universals FunName Universals OptTermetric openParen FullArgs closeParen signature Type OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 } + | Universals FunName Universals OptTermetric signature Type OptExpression { PreF $2 $5 $1 $3 [] $6 $4 $7 } | prval {% Left $ Expected $1 "Function signature" "prval" } | var {% Left $ Expected $1 "Function signature" "var" } | lambda {% Left $ Expected $1 "Function signature" "lam" } | llambda {% Left $ Expected $1 "Function signature" "llam" } + | lsqbracket {% Left $ Expected $1 "Function signature" "[" } -- | Parse affiliated `sortdef`s -AndSort : AndSort and identifier eq Type { AndD $1 (SortDef $2 $3 $5) } -- TODO figure out if this is building up the slow way - | sortdef identifier eq Type { SortDef $1 $2 $4 } +AndSort : AndSort and IdentifierOr eq Type { AndD $1 (SortDef $2 $3 $5) } -- TODO figure out if this is building up the slow way + | sortdef IdentifierOr eq Type { SortDef $1 $2 $4 } -- | Function declaration FunDecl : fun PreFunction { [ Func $1 (Fun $2) ] } @@ -507,47 +544,57 @@ | lambda {% Left $ Expected $1 "Function declaration" "lam" } | llambda {% Left $ Expected $1 "Function declaration" "llam" } +IdentifierOr : identifier { $1 } + | identifierSpace { $1 } + +MaybeType : eq Type { Just $2 } + | { Nothing } + -- | Parse a declaration defining a type -TypeDecl : typedef identifier eq Universals atbrace Records rbrace { RecordType $2 [] $4 $6 } - | typedef identifier openParen FullArgs closeParen eq Universals atbrace Records rbrace { RecordType $2 $4 $7 $9 } - | vtypedef identifier eq Universals atbrace Records rbrace { RecordViewType $2 [] $4 $6 } - | vtypedef identifier openParen FullArgs closeParen eq Universal atbrace Records rbrace { RecordViewType $2 $4 [$7] $9 } - | vtypedef identifier openParen FullArgs closeParen eq Universals atbrace Records rbrace { RecordViewType $2 $4 $7 $9 } - | datatype identifier eq Leaves { SumType $2 [] $4 } - | datatype identifier openParen Args closeParen eq Leaves { SumType $2 $4 $7 } - | datavtype identifier eq Leaves { SumViewType $2 [] $4 } - | datavtype identifier openParen Args closeParen eq Leaves { SumViewType $2 $4 $7 } - | abstype identifier openParen FullArgs closeParen eq Type { AbsType $1 $2 $4 (Just $7) } - | abstype identifier openParen FullArgs closeParen { AbsType $1 $2 $4 Nothing } - | absvtype identifier openParen FullArgs closeParen eq Type { AbsViewType $1 $2 $4 (Just $7) } - | absvtype identifier openParen FullArgs closeParen { AbsViewType $1 $2 $4 Nothing } - | dataprop identifier openParen FullArgs closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 } - | absprop identifier openParen FullArgs closeParen { AbsProp $1 $2 [] } - | typedef identifier eq Type { TypeDef $1 $2 [] $4 } - | typedef identifier openParen FullArgs closeParen eq Type { TypeDef $1 $2 $4 $7 } - | vtypedef identifier eq Type { ViewTypeDef $1 $2 [] $4 } - | vtypedef identifier openParen FullArgs closeParen eq Type { ViewTypeDef $1 $2 $4 $7 } - | stadef identifier eq Name { Stadef $2 $4 [] } - | stadef identifier eq Name openParen TypeIn closeParen { Stadef $2 $4 $6 } - | sortdef identifier eq Type { SortDef $1 $2 $4 } +TypeDecl : typedef IdentifierOr eq Universals atbrace Records rbrace { RecordType $2 [] $4 $6 } + | typedef IdentifierOr openParen FullArgs closeParen eq Universals atbrace Records rbrace { RecordType $2 $4 $7 $9 } + | typedef IdentifierOr eq Type { TypeDef $1 $2 [] $4 } + | typedef IdentifierOr openParen FullArgs closeParen eq Type { TypeDef $1 $2 $4 $7 } + | vtypedef IdentifierOr eq Universals atbrace Records rbrace { RecordViewType $2 [] $4 $6 } + | vtypedef IdentifierOr openParen FullArgs closeParen eq Universal atbrace Records rbrace { RecordViewType $2 $4 [$7] $9 } + | vtypedef IdentifierOr openParen FullArgs closeParen eq Universals atbrace Records rbrace { RecordViewType $2 $4 $7 $9 } + | vtypedef IdentifierOr eq Type { ViewTypeDef $1 $2 [] $4 } + | vtypedef IdentifierOr openParen FullArgs closeParen eq Type { ViewTypeDef $1 $2 $4 $7 } + | datatype IdentifierOr eq Leaves { SumType $2 [] $4 } + | datatype IdentifierOr openParen Args closeParen eq Leaves { SumType $2 $4 $7 } + | datavtype IdentifierOr eq Leaves { SumViewType $2 [] $4 } + | datavtype IdentifierOr openParen Args closeParen eq Leaves { SumViewType $2 $4 $7 } + | abst0p IdentifierOr eq Type { AbsT0p $1 $2 $4 } + | viewdef IdentifierOr openParen FullArgs closeParen eq Type { ViewDef $1 $2 $4 $7 } + | absvt0p IdentifierOr openParen FullArgs closeParen MaybeType { AbsVT0p $1 $2 $4 $6 } + | absview IdentifierOr openParen FullArgs closeParen MaybeType { AbsView $1 $2 $4 $6 } + | abstype IdentifierOr openParen FullArgs closeParen MaybeType { AbsType $1 $2 $4 $6 } + | absvtype IdentifierOr openParen FullArgs closeParen MaybeType { AbsViewType $1 $2 $4 $6 } + | dataprop IdentifierOr openParen FullArgs closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 } + | absprop IdentifierOr openParen FullArgs closeParen { AbsProp $1 $2 [] } + | stadef IdentifierOr eq Name { Stadef $2 $4 [] } + | stadef IdentifierOr eq Name openParen TypeIn closeParen { Stadef $2 $4 $6 } + | stadef boolLit eq Name { Stadef (over _head toLower (show $2)) $4 [] } + | sortdef IdentifierOr eq Type { SortDef $1 $2 $4 } | AndSort { $1 } -- | Parse a declaration Declaration : include string { Include $2 } | define { Define $1 } + | define identifierSpace string { Define ($1 ++ $2 ++ $3) } -- FIXME better approach? | cblock { CBlock $1 } | lineComment { Comment $1 } | staload underscore eq string { Staload (Just "_") $4 } | staload string { Staload Nothing $2 } - | staload identifier eq string { Staload (Just $2) $4 } + | staload IdentifierOr eq string { Staload (Just $2) $4 } | extern Declaration { Extern $1 $2 } - | var Pattern signature Type with PreExpression { Var (Just $4) $2 Nothing (Just $6) } -- FIXME + | var Pattern signature Type with PreExpression { Var (Just $4) $2 Nothing (Just $6) } -- FIXME signature is too general. | var Pattern signature Type eq PreExpression { Var (Just $4) $2 (Just $6) Nothing } | val Pattern signature Type eq PreExpression { Val $1 (Just $4) $2 $6 } | val Pattern eq Expression { Val $1 Nothing $2 $4 } - | var Pattern eq PreExpression { Var Nothing $2 (Just $4) Nothing } + | var Pattern eq Expression { Var Nothing $2 (Just $4) Nothing } | var Pattern signature Type { Var (Just $4) $2 Nothing Nothing } - | var Pattern eq fixAt identifier openParen Args closeParen signature Type plainArrow Expression { Var Nothing $2 (Just $ FixAt (PreF (Unqualified $5) $9 [] [] $7 $10 Nothing (Just $12))) Nothing } + | var Pattern eq fixAt IdentifierOr openParen Args closeParen signature Type plainArrow Expression { Var Nothing $2 (Just $ FixAt (PreF (Unqualified $5) $9 [] [] $7 $10 Nothing (Just $12))) Nothing } | var Pattern eq lambdaAt openParen Args closeParen signature Type plainArrow Expression { Var Nothing $2 (Just $ LambdaAt (PreF (Unnamed $4) $8 [] [] $6 $9 Nothing (Just $11))) Nothing } | prval Pattern eq PreExpression { PrVal $2 $4 } | praxi PreFunction { Func $1 (Praxi $2) } @@ -555,9 +602,12 @@ | implement Implementation { Impl [] $2 } | implement openParen Args closeParen Implementation { Impl $3 $5 } | overload BinOp with Name { OverloadOp $1 $2 $4 } + | overload identifierSpace with Name { OverloadIdent $1 $2 $4 } | assume Name openParen Args closeParen eq Expression { Assume $2 $4 $7 } - | tkindef Name eq string { TKind $1 $2 $4 } + | tkindef IdentifierOr eq string { TKind $1 (Unqualified $2) $4 } | TypeDecl { $1 } + | symintr Name { SymIntr $1 $2 } + | stacst IdentifierOr signature Type OptExpression { Stacst $1 (Unqualified $2) $4 $5 } | lambda {% Left $ Expected $1 "Declaration" "lam" } | llambda {% Left $ Expected $1 "Declaration" "llam" } | minus {% Left $ Expected $1 "Declaration" "-" } 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 @@ -67,7 +67,7 @@ printATS :: ATS -> String printATS (ATS x) = g mempty - where g = (displayS . renderPretty 0.6 120 . pretty) (ATS $ reverse x) + where g = (displayS . renderPretty 0.6 120 . (<> "\n") . pretty) (ATS $ reverse x) printATSCustom :: Float -> Int -> ATS -> String printATSCustom r i (ATS x) = g mempty @@ -145,8 +145,6 @@ a (UnaryF Negate e) = "~" <> e a (NamedValF name) = pretty name a (CallF name [] [] Nothing []) = pretty name <> "()" - a (CallF name [] [] Nothing [x]) - | startsParens x = pretty name <> pretty x a (CallF name [] [] (Just e) xs) = pretty name <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs -- FIXME split eagerly on "|" a (CallF name [] [] Nothing xs) = pretty name <> prettyArgsG "(" ")" xs a (CallF name [] us Nothing []) = pretty name <> prettyArgsU "{" "}" us @@ -188,7 +186,7 @@ a _ = "FIXME" prettyCases [] = mempty prettyCases [(s, l, t)] = "|" <+> pretty s <+> pretty l <+> t - prettyCases ((s, l, t): xs) = prettyCases xs $$ "|" <+> pretty s <+> pretty l <+> t + prettyCases ((s, l, t): xs) = prettyCases xs $$ "|" <+> pretty s <+> pretty l <+> t -- FIXME can leave space with e.g. => \n begin ... noParens :: Doc -> Bool noParens = all (`notElem` ("()" :: String)) . show @@ -208,6 +206,7 @@ a (GuardedF _ e p) = p <+> "when" <+> pretty e a (ProofF _ p p') = parens (patternHelper p <+> "|" <+> patternHelper p') a (TuplePatternF ps) = parens (patternHelper ps) + a (AtPatternF _ p) = "@" <> p instance Pretty Arg where pretty (Arg (First s)) = pretty s @@ -228,10 +227,12 @@ | squish op = se <> pretty op <> se' | otherwise = se <+> pretty op <+> se' a (StaticIntF i) = pretty i + a StaticVoidF{} = "()" a (SifF e e' e'') = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e'' a (StaticBoolF True) = "true" a (StaticBoolF False) = "false" a (SCallF n cs) = pretty n <> parens (mconcat (punctuate "," . reverse . fmap pretty $ cs)) + a (SPrecedeF e e') = e <> ";" <+> e' instance Pretty Type where pretty = cata a where @@ -240,6 +241,7 @@ a BoolF = "bool" a VoidF = "void" a NatF = "nat" + a AddrF = "addr" a CharF = "char" a (NamedF n) = string n a (ExF e t) = pretty e <+> t @@ -264,6 +266,7 @@ a (RefTypeF t) = "&" <> t a (ViewTypeF _ t) = "view@" <> parens t a (FunctionTypeF s t t') = t <+> string s <+> t' + a (ViewLiteralF c) = "view" <> pretty c a NoneTypeF{} = "()" a ImplicitTypeF{} = ".." @@ -277,7 +280,8 @@ pretty (Existential bs ty (Just e)) = lbracket <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket where go (Arg (First s)) = pretty s go (Arg (Both s t)) = pretty s <+> colon <+> pretty t - go _ = "FIXME" -- maybe use a new type? I don't think this should ever happen. + go (Arg (Second t)) = pretty t + go _ = "FIXME" instance Pretty Universal where pretty (Universal [x@PrfArg{}] Nothing Nothing) = lbrace <+> pretty x <+> rbrace -- FIXME universals can now be length-one arguments @@ -347,8 +351,10 @@ prettyDL :: [DataPropLeaf] -> Doc prettyDL [] = mempty -prettyDL [DataPropLeaf us e] = indent 2 ("|" <+> foldMap pretty us <+> pretty e) -prettyDL (DataPropLeaf us e:xs) = prettyDL xs $$ indent 2 ("|" <+> foldMap pretty us <+> pretty e) +prettyDL [DataPropLeaf us e Nothing] = indent 2 ("|" <+> foldMap pretty us <+> pretty e) +prettyDL [DataPropLeaf us e (Just e')] = indent 2 ("|" <+> foldMap pretty us <+> pretty e <+> "of" <+> pretty e') +prettyDL (DataPropLeaf us e Nothing:xs) = prettyDL xs $$ indent 2 ("|" <+> foldMap pretty us <+> pretty e) +prettyDL (DataPropLeaf us e (Just e'):xs) = prettyDL xs $$ indent 2 ("|" <+> foldMap pretty us <+> pretty e <+> "of" <+> pretty e') prettyLeaf :: [(String, Maybe Type)] -> Doc prettyLeaf [] = mempty @@ -407,7 +413,8 @@ pretty _ = "FIXME" instance Pretty DataPropLeaf where - pretty (DataPropLeaf us e) = "|" <+> foldMap pretty (reverse us) <+> pretty e + pretty (DataPropLeaf us e Nothing) = "|" <+> foldMap pretty (reverse us) <+> pretty e + pretty (DataPropLeaf us e (Just e')) = "|" <+> foldMap pretty (reverse us) <+> pretty e <+> "of" <+> pretty e' typeHelper :: [(String, Type)] -> Doc typeHelper rs = group (flatAlt ("=" <$> indent 2 (prettyRecord rs)) ("=" <+> prettyRecord rs)) @@ -425,7 +432,6 @@ pretty (SumType s [] ls) = "datatype" <+> string s <+> "=" <$> prettyLeaf ls pretty (SumType s as ls) = "datatype" <+> string s <> prettyArgs as <+> "=" <$> prettyLeaf ls pretty (Impl [] i) = pretty i - pretty Impl{} = "FIXME" pretty (PrVal p e) = "prval" <+> pretty p <+> "=" <+> pretty e pretty (Val a Nothing p e) = "val" <> pretty a <+> pretty p <+> "=" <+> pretty e pretty (Val a (Just t) p e) = "val" <> pretty a <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e @@ -438,6 +444,7 @@ pretty (CBlock s) = string s pretty (Comment s) = string s pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n + pretty (OverloadIdent _ i n) = "overload" <+> string i <+> "with" <+> pretty n pretty (Func _ (Fn pref)) = "fn" pretty pref pretty (Func _ (Fun pref)) = "fun" pretty pref pretty (Func _ (CastFn pref)) = "castfn" pretty pref @@ -455,4 +462,7 @@ pretty (TypeDef _ s as t) = "typedef" <+> string s <> prettyArgs as <+> "=" <+> pretty t pretty (AbsProp _ n as) = "absprop" <+> string n <+> prettyArgs as pretty (Assume n as e) = "assume" pretty n <> prettyArgs as <+> "=" pretty e + pretty (SymIntr _ n) = "symintr" <+> pretty n + pretty (Stacst _ n t Nothing) = "stacst" pretty n <+> ":" pretty t + pretty (Stacst _ n t (Just e)) = "stacst" pretty n <+> ":" pretty t <+> "=" pretty e pretty _ = "FIXME" 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 @@ -73,7 +73,12 @@ | SumViewType String [Arg] [(String, Maybe Type)] | AbsType AlexPosn String [Arg] (Maybe Type) | AbsViewType AlexPosn String [Arg] (Maybe Type) + | AbsView AlexPosn String [Arg] (Maybe Type) + | AbsVT0p AlexPosn String [Arg] (Maybe Type) + | AbsT0p AlexPosn String Type + | ViewDef AlexPosn String [Arg] Type | OverloadOp AlexPosn BinOp Name + | OverloadIdent AlexPosn String Name | Comment String | DataProp AlexPosn String [Arg] [DataPropLeaf] | Extern AlexPosn Declaration @@ -84,9 +89,11 @@ | AbsProp AlexPosn String [Arg] | Assume Name [Arg] Expression | TKind AlexPosn Name String + | SymIntr AlexPosn Name + | Stacst AlexPosn Name Type (Maybe Expression) deriving (Show, Eq, Generic, NFData) -data DataPropLeaf = DataPropLeaf [Universal] Expression +data DataPropLeaf = DataPropLeaf [Universal] Expression (Maybe Expression) deriving (Show, Eq, Generic, NFData) -- | A type for parsed ATS types @@ -96,6 +103,7 @@ | Char | Int | Nat + | Addr | DependentInt StaticExpression | DependentBool StaticExpression | DepString StaticExpression @@ -120,6 +128,7 @@ | FunctionType String Type Type | NoneType AlexPosn | ImplicitType AlexPosn + | ViewLiteral Addendum deriving (Show, Eq, Generic, NFData) -- | A type for the various lambda arrows (`=>`, `=`, etc.) @@ -145,6 +154,7 @@ | Free Pattern | Proof AlexPosn [Pattern] [Pattern] | TuplePattern [Pattern] + | AtPattern AlexPosn Pattern deriving (Show, Eq, Generic, NFData) data Paired a b = Both a b @@ -190,7 +200,9 @@ data StaticExpression = StaticVal Name | StaticBinary BinOp StaticExpression StaticExpression | StaticInt Int + | SPrecede StaticExpression StaticExpression | StaticBool Bool + | StaticVoid AlexPosn | Sif { scond :: StaticExpression, wwhenTrue :: StaticExpression, selseExpr :: StaticExpression } -- Static if (for proofs) | SCall Name [StaticExpression] deriving (Show, Eq, Generic, NFData) @@ -288,10 +300,12 @@ makeBaseFunctor ''StaticExpression makeBaseFunctor ''Type +-- precedence: rewrite n + 2 * x to n + (2 * x) rewriteATS :: Expression -> Expression rewriteATS = cata a where - a (PrecedeF e e'@PrecedeList{}) = PrecedeList (e : _exprs e') - a (PrecedeF e e') = PrecedeList [e, e'] - a x = embed x - {- a (BinaryF Add e e'@BinList{}) = BinList Add (e : _exprs e') -} - {- a (BinaryF Add e e') = BinList Add [e, e'] -} + a (PrecedeF e e'@PrecedeList{}) = PrecedeList (e : _exprs e') + a (PrecedeF e e') = PrecedeList [e, e'] + a (BinaryF Mult (Binary Add e e') e'') = Binary Add e (Binary Mult e' e'') + a (ParenExprF _ e@Precede{}) = e + a (ParenExprF _ e@PrecedeList{}) = e + a x = embed x diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -1,5 +1,5 @@ --- -resolver: lts-10.1 +resolver: lts-10.2 packages: - '.' extra-deps: diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -26,7 +26,7 @@ testFile f = it f $ do sample <- readFile f expected <- readFile (replaceExtension f ".out") - (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected + (fmap printATS . parseATS . lexATS) sample `shouldBe` Right expected main :: IO () main = hspec $