ats-format 0.1.0.16 → 0.1.0.17
raw patch · 10 files changed
+187/−70 lines, 10 filesdep +blaze-htmldep +blaze-markup
Dependencies added: blaze-html, blaze-markup
Files
- Justfile +1/−0
- ats-format.cabal +4/−1
- src/Language/ATS.hs +3/−0
- src/Language/ATS/Doc.hs +16/−0
- src/Language/ATS/Lexer.x +27/−7
- src/Language/ATS/Parser.y +95/−45
- src/Language/ATS/PrettyPrint.hs +19/−9
- src/Language/ATS/Types.hs +20/−6
- stack.yaml +1/−1
- test/Spec.hs +1/−1
Justfile view
@@ -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
ats-format.cabal view
@@ -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
src/Language/ATS.hs view
@@ -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
+ src/Language/ATS/Doc.hs view
@@ -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"
src/Language/ATS/Lexer.x view
@@ -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
src/Language/ATS/Parser.y view
@@ -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" "-" }
src/Language/ATS/PrettyPrint.hs view
@@ -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"
src/Language/ATS/Types.hs view
@@ -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 (`=>`, `=<cloref1>`, 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
stack.yaml view
@@ -1,5 +1,5 @@ ----resolver: lts-10.1+resolver: lts-10.2 packages: - '.' extra-deps:
test/Spec.hs view
@@ -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 $