diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -7,3 +7,5 @@ The parser is slightly buggy but it can handle almost all of the language; see the `test/data` directory for examples of what it can handle. + +The pretty-printer works quite well; you can safely use it for code generation. 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: 1.0.1.1 +version: 1.0.2.0 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.hs b/src/Language/ATS.hs --- a/src/Language/ATS.hs +++ b/src/Language/ATS.hs @@ -9,6 +9,7 @@ , printATSCustom , printATSFast , printErr + , defaultFixityState -- * Library functions , getDependencies -- * Syntax Tree @@ -75,7 +76,7 @@ -- | Parse a string containing ATS source. parse :: String -> Either ATSError (ATS AlexPosn) -parse = parseWithCtx mempty +parse = parseWithCtx defaultFixityState -- | Parse with some fixity declarations already in scope. parseWithCtx :: FixityState AlexPosn -> String -> Either ATSError (ATS AlexPosn) 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 @@ -3,7 +3,6 @@ {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-incomplete-uni-patterns -fno-warn-unused-imports -fno-warn-orphans #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} - {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE OverloadedStrings #-} @@ -21,7 +20,6 @@ ) where import Data.Bool (bool) -import Data.Data (Typeable, Data) import Control.DeepSeq (NFData) import GHC.Generics (Generic) import Text.PrettyPrint.ANSI.Leijen hiding (line, bool, column, (<$>)) @@ -67,7 +65,7 @@ @slash_comment = \/\* ([^\/\*] | @not_close_slash | \n)* \*\/ @block_comment = @paren_comment | @slash_comment -@if_block = "#if" ([^\#] | "#then" | "#print" | \n)+ "#endif" .* +@if_block = "#if" (n | "") ("def" | "") ([^\#] | "#then" | "#print" | \n)+ "#endif" .* -- Basically anything that can go inside implicit arguments, i.e. anything -- necessary to construct a type. @@ -98,7 +96,7 @@ @fixity_decl = "infixr" | "infixl" | "prefix" | "postfix" -@builtin = \$ (("effmask_" (wrt | all | ref)) | "extfcall" | "ldelay" | "delay" | "list_vt" | "tempenver" | "extval" | "extype" | "mylocation" | "showtype") +@builtin = \$ (("effmask_" (wrt | all | ref)) | "extfcall" | "extype" (_struct | "") | "arrpsz" | "ldelay" | "delay" | "list" (_vt | "") | "tempenver" | "extval" | "mylocation" | "solver_assert" | "showtype") @block_comment_start = \(\* | \/\* @block_comment_end = \*\) | \*\/ @@ -126,9 +124,9 @@ @comment_in+ / [^\)] { tok (\p s -> alex $ CommentContents p s) } @comment_general { tok (\p s -> alex $ CommentContents p s) } <0> "//".* { tok (\p s -> alex $ CommentLex p s) } - <0> "#define".* { tok (\p s -> alex $ MacroBlock p s) } - <0> @if_block { tok (\p s -> alex $ MacroBlock p s) } <0> @c_block { tok (\p s -> alex $ CBlockLex p s) } + <0> "#define".* { tok (\p s -> alex $ MacroBlock p s) } + <0> @if_block { tok (\p s -> alex $ MacroBlock p s) } <0> fun { tok (\p _ -> alex $ Keyword p KwFun) } <0> fn { tok (\p _ -> alex $ Keyword p KwFn) } <0> fnx { tok (\p _ -> alex $ Keyword p KwFnx) } @@ -151,6 +149,8 @@ <0> lam { tok (\p _ -> alex $ Keyword p KwLambda) } <0> staload { tok (\p _ -> alex $ Keyword p (KwStaload False)) } <0> "#"staload { tok (\p _ -> alex $ Keyword p (KwStaload True)) } + <0> dynload { tok (\p _ -> alex $ Keyword p (KwDynload False)) } + <0> "#"dynload { tok (\p _ -> alex $ Keyword p (KwDynload True)) } <0> let { tok (\p _ -> alex $ Keyword p KwLet) } <0> in { tok (\p _ -> alex $ Keyword p KwIn) } <0> end { tok (\p _ -> alex $ Keyword p KwEnd) } @@ -211,7 +211,6 @@ <0> mod { tok (\p _ -> alex $ Keyword p KwMod) } <0> datasort { tok (\p _ -> alex $ Keyword p KwDatasort) } <0> "println!" { tok (\p s -> alex $ Identifier p s) } - <0> "prerrln!" { tok (\p s -> alex $ Identifier p s) } <0> "fix@" { tok (\p _ -> alex $ Keyword p KwFixAt) } <0> "lam@" { tok (\p _ -> alex $ Keyword p KwLambdaAt) } <0> "addr" { tok (\p _ -> alex $ Keyword p KwAddr) } @@ -221,27 +220,27 @@ <0> symintr { tok (\p _ -> alex $ Keyword p KwSymintr) } <0> absview { tok (\p _ -> alex $ Keyword p KwAbsview) } <0> exception { tok (\p _ -> alex $ Keyword p KwException) } - <0> "$list" { tok (\p _ -> alex $ Keyword p (KwListLit "")) } <0> "$list_vt" { tok (\p _ -> alex $ Keyword p (KwListLit "_vt")) } + <0> "$list" { tok (\p _ -> alex $ Keyword p (KwListLit mempty)) } <0> "fold@" { tok (\p s -> alex $ IdentifierSpace p s) } <0> "free@" { tok (\p s -> alex $ Identifier p s) } <0> @fixity_decl { tok (\p s -> alex $ FixityTok p s) } <0> @double_parens { tok (\p s -> alex $ DoubleParenTok p) } <0> @double_braces { tok (\p s -> alex $ DoubleBracesTok p) } <0> @double_brackets { tok (\p s -> alex $ DoubleBracketTok p) } - <0> @char_lit { tok (\p s -> alex $ CharTok p (toChar s)) } <0> @lambda { tok (\p s -> alex $ Arrow p s) } <0> @func_type { tok (\p s -> alex $ FuncType p s) } <0> @unsigned_lit { tok (\p s -> alex $ UintTok p (read $ init s)) } <0> @integer { tok (\p s -> alex $ IntTok p (read s)) } -- FIXME shouldn't fail silenty on overflow <0> @float { tok (\p s -> alex $ FloatTok p (read s)) } + <0> @char_lit { tok (\p s -> alex $ CharTok p (toChar s)) } <0> @at_brace { tok (\p s -> alex $ Operator p "@{") } -- FIXME this is kinda sloppy <0> $br / @ref_call { tok (\p s -> alex $ SpecialBracket p) } <0> @signature { tok (\p s -> alex $ SignatureTok p (tail s)) } <0> @operator { tok (\p s -> alex $ Operator p s) } <0> @builtin { tok (\p s -> alex $ SpecialIdentifier p (tail s)) } <0> $special { tok (\p s -> alex $ Special p s) } - <0> @identifier / " " { tok (\p s -> alex $ IdentifierSpace p s) } + <0> @identifier / " " { tok (\p s -> alex $ IdentifierSpace p s) } -- FIXME get rid of this for performance reasons <0> @identifier { tok (\p s -> alex $ Identifier p s) } <0> @string { tok (\p s -> alex $ StringTok p s) } @@ -252,8 +251,6 @@ deriving instance Generic AlexPosn deriving instance NFData AlexPosn -deriving instance Data AlexPosn -deriving instance Typeable AlexPosn tok f (p,_,_,s) len = f p (take len s) @@ -261,7 +258,7 @@ data Addendum = None | Plus | Minus - deriving (Eq, Show, Generic, NFData, Data, Typeable) + deriving (Eq, Show, Generic, NFData) -- TODO ideally we'd handle this as an internal error later in the parser. get_staload (Keyword _ (KwStaload b)) = b @@ -281,6 +278,7 @@ | KwVtypedef | KwVtype Addendum | KwStaload Bool + | KwDynload Bool | KwLet | KwIn | KwLocal @@ -382,6 +380,8 @@ pretty Minus = "-" pretty None = "" +maybeSharp b = ((bool "" "#" b) <>) + instance Pretty Keyword where pretty KwFun = "fun" pretty (KwVtype a) = "vtype" <> pretty a @@ -392,7 +392,8 @@ pretty KwAssume = "assume" pretty KwTypedef = "typedef" pretty KwVtypedef = "vtypedef" - pretty (KwStaload b) = bool "" "#" b <> "staload" + pretty (KwStaload b) = maybeSharp b "staload" + pretty (KwDynload b) = maybeSharp b "dynload" pretty KwLet = "let" pretty KwWhere = "where" pretty KwLocal = "local" @@ -457,7 +458,7 @@ pretty KwInfix = "infix" pretty KwInfixr = "infixr" pretty KwInfixl = "infixl" - pretty (KwListLit s) = "list" <> string s + pretty (KwListLit s) = "$list" <> text s pretty KwMacdef = "macdef" instance Pretty Word where @@ -471,7 +472,7 @@ pretty (IntTok _ i) = pretty i pretty (FloatTok _ x) = pretty x pretty (CharTok _ c) = squotes (pretty c) - pretty (StringTok _ s) = dquotes (text s) + pretty (StringTok _ s) = text s pretty (Special _ s) = text s pretty CBlockLex{} = "%{" pretty (Arrow _ s) = text s 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 @@ -46,6 +46,7 @@ %left percent %left andOp %left or +%left identifierSpace %right at %right in %right mutateArrow @@ -57,6 +58,8 @@ %nonassoc leq %nonassoc geq %nonassoc mutateEq +%nonassoc maybeProof +%nonassoc prfTransform %token fun { Keyword $$ KwFun } @@ -118,6 +121,7 @@ local { Keyword $$ KwLocal } view { Keyword $$ (KwView None) } viewContra { Keyword $$ (KwView Minus) } + viewCo { Keyword $$ (KwView Plus) } vtype { $$@(Keyword _ KwVtype{}) } viewPlusMinus { Keyword _ (KwView $$) } raise { Keyword $$ KwRaise } @@ -128,8 +132,8 @@ symintr { Keyword $$ KwSymintr } stacst { Keyword $$ KwStacst } propdef { Keyword $$ KwPropdef } - list { Keyword $$ (KwListLit "") } list_vt { Keyword $$ (KwListLit "_vt") } + list { Keyword $$ (KwListLit "") } datasort { Keyword $$ KwDatasort } uintLit { UintTok _ $$ } intLit { IntTok _ $$ } @@ -224,7 +228,7 @@ | TypeIn comma Type { $3 : $1 } -- | Several comma-separated types or static expressions -TypeInExpr : TypeIn { $1 } +TypeInExpr : Type { [$1] } | StaticExpression { [ConcreteType $1] } | TypeInExpr comma Type { $3 : $1 } | TypeInExpr comma StaticExpression { ConcreteType $3 : $1 } @@ -240,7 +244,8 @@ | Type mutateArrow Type { FunctionType "->" $1 $3 } | Type funcArrow Type { FunctionType $2 $1 $3 } | refType Type { RefType $2 } - | Type maybeProof { MaybeVal $1 } + | Type maybeProof { MaybeVal $1 } + | Name maybeProof { MaybeVal (Named $1) } | Type fromVT { FromVT $1 } | Type prfTransform Type { AsProof $1 (Just $3) } | Type prfTransform underscore { AsProof $1 Nothing } @@ -252,31 +257,29 @@ | Type at StaticExpression { AtExpr $2 $1 $3 } | at Type { AtType $1 $2 } | atbrace Records rbrace { AnonymousRecord $1 $2 } - | openParen TypeIn vbar Type closeParen { ProofType $1 $2 $4 } -- FIXME can have multiple first parts + | openParen TypeIn vbar Type closeParen { ProofType $1 $2 $4 } | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] } | openParen TypeIn closeParen { Tuple $1 $2 } + | openParen TypeIn closeParen lineComment { Tuple $1 $2 } | openParen TypeIn rbrace {% left $ Expected $3 ")" "}" } | openParen Type closeParen { ParenType $1 $2 } | doubleParens { NoneType $1 } - | Type where PreFunction { WhereType $2 $1 $3 } + | Type where IdentifierOr SortArgs eq Type { WhereType $2 $1 $3 $4 $6 } | minus {% left $ Expected $1 "Type" "-" } | dollar {% left $ Expected $1 "Type" "$" } | identifierSpace identifier openParen {% left $ Expected (token_posn $2) "Static integer expression" (to_string $2) } | Type identifierSpace {% left $ Expected (token_posn $2) "," (to_string $2) } -FullArgs : Args { $1 } - -- | 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 ] } + | Args vbar Arg { [ PrfArg $1 $3 ] } | lineComment { [] } | Args lineComment { $1 } | Args Comment { $1 } | { [] } -TypeArg : identifier { Arg (First $ to_string $1) } +TypeArg : IdentifierOr { Arg (First $1) } | IdentifierOr colon Type { Arg (Both $1 $3) } | Type { Arg (Second $1) } @@ -359,7 +362,6 @@ | Expression colon Type { TypeSignature $1 $3 } -- TODO is a more general expression sensible? | openParen Expression vbar Expression closeParen { ProofExpr $1 $2 $4 } | list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 } - | list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 } -- TODO is this legal?? | begin Expression extern {% left $ Expected $3 "end" "extern" } | Expression prfTransform underscore {% left $ Expected $2 "Rest of expression or declaration" ">>" } @@ -404,6 +406,7 @@ | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] } | let StaticDecls in end { SLet $1 $2 Nothing } | let StaticDecls in StaticExpression end { SLet $1 $2 (Just $4) } + | openParen StaticExpression closeParen { $2 } -- | Parse an expression that can be called without parentheses PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 } @@ -455,6 +458,7 @@ | let ATS in Expression semicolon {% left $ Expected $5 "end" ";" } | let ATS if {% left $ Expected $3 "in" "if" } | if Expression then Expression else else {% left $ Expected $6 "Expression" "else" } + | begin Expression implement {% left $ Expected $3 "end" "implement" } -- | Parse a termetric Termetric : openTermetric StaticExpression closeTermetric { ($1, $2) } @@ -469,6 +473,7 @@ | addr { Addr } | view { View $1 None } | viewContra { View $1 Minus } + | viewCo { View $1 Plus } | vtype { VType (token_posn $1) (get_addendum $1) } | IdentifierOr { NamedSort $1 } | IdentifierOr plus { NamedSort ($1 <> "+") } @@ -534,6 +539,7 @@ -- | Parse a list of values in a record RecordVal : IdentifierOr eq Expression { [($1, $3)] } | RecordVal comma IdentifierOr eq Expression { ($3, $5) : $1 } + | IdentifierOr eq comma {% left $ Expected $3 "Expression" "," } -- | Parse a list of types in a record Records : IdentifierOr eq Type { [($1, $3)] } @@ -598,8 +604,8 @@ -- | Optionally parse a function body OptExpression : { Nothing } - | eq Expression { Just $2 } -- FIXME only let this happen for external declarations (?) - | let {% left $ Expected $1 "=" "let" } -- TODO is this actually a good idea? + | eq Expression { Just $2 } + | let {% left $ Expected $1 "=" "let" } | ifcase {% left $ Expected $1 "=" "ifcase" } | eq fun {% left $ Expected $2 "Expression" "=" } | eq lineComment fun {% left $ Expected $3 "Expression" "=" } @@ -634,11 +640,11 @@ | { Nothing } -- | Parse a type signature and optional function body -PreFunction : FunName openParen FullArgs closeParen OptType OptExpression { (PreF $1 (fmap fst $5) [] [] $3 (fmap snd $5) Nothing $6) } +PreFunction : FunName openParen Args closeParen OptType OptExpression { (PreF $1 (fmap fst $5) [] [] $3 (fmap snd $5) Nothing $6) } | FunName Universals OptTermetric OptType OptExpression { PreF $1 (fmap fst $4) [] $2 [NoArgs] (fmap snd $4) $3 $5 } | FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $1 (fmap fst $5) [] $2 [] (fmap snd $5) $3 $6 } - | FunName Universals OptTermetric openParen FullArgs closeParen OptType OptExpression { PreF $1 (fmap fst $7) [] $2 $5 (fmap snd $7) $3 $8 } - | Universals FunName Universals OptTermetric openParen FullArgs closeParen OptType OptExpression { PreF $2 (fmap fst $8) $1 $3 $6 (fmap snd $8) $4 $9 } + | FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $1 (fmap fst $7) [] $2 $5 (fmap snd $7) $3 $8 } + | Universals FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $2 (fmap fst $8) $1 $3 $6 (fmap snd $8) $4 $9 } | Universals FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $2 (fmap fst $6) $1 $3 [] (fmap snd $6) $4 $7 } | Universals FunName Universals OptTermetric OptType OptExpression { PreF $2 (fmap fst $5) $1 $3 [] (fmap snd $5) $4 $6 } | prval {% left $ Expected $1 "Function signature" "prval" } @@ -649,12 +655,18 @@ | lsqbracket {% left $ Expected $1 "Function signature" "[" } -- | Parse affiliated `sortdef`s -AndSort : AndSort and IdentifierOr eq Sort { AndD $1 (SortDef $2 $3 (Left $5)) } -- TODO figure out if this is building up the slow way +AndSort : AndSort and IdentifierOr eq Sort { AndD $1 (SortDef $2 $3 (Left $5)) } | sortdef IdentifierOr eq Sort { SortDef $1 $2 (Left $4) } | sortdef IdentifierOr eq Universal { SortDef $1 $2 (Right $4) } -AndStadef : stadef IdentifierOr SortArgs eq Type { Stadef $2 $3 $5 } - | AndStadef and IdentifierOr SortArgs eq Type { AndD $1 (Stadef $3 $4 $6) } +AndStadef : stadef IdentifierOr SortArgs eq Type { Stadef $2 $3 (Right $5) } + | stadef IdentifierOr SortArgs eq StaticExpression { Stadef $2 $3 (Left $5) } + | stadef Operator SortArgs eq Type { Stadef $2 $3 (Right $5) } + | stadef Operator SortArgs eq StaticExpression { Stadef $2 $3 (Left $5) } + | AndStadef and IdentifierOr SortArgs eq Type { AndD $1 (Stadef $3 $4 (Right $6)) } + | AndStadef and IdentifierOr SortArgs eq StaticExpression { AndD $1 (Stadef $3 $4 (Left $6)) } + | AndStadef and Operator SortArgs eq Type { AndD $1 (Stadef $3 $4 (Right $6)) } + | AndStadef and Operator SortArgs eq StaticExpression { AndD $1 (Stadef $3 $4 (Left $6)) } StafunDecl : prfun PreFunction { Func $1 (PrFun $2) } | prfn PreFunction { Func $1 (PrFn $2) } @@ -688,7 +700,7 @@ | { Nothing } FunArgs : { [NoArgs] } - | openParen FullArgs closeParen { $2 } + | openParen Args closeParen { $2 } | doubleParens { [] } SortArg : IdentifierOr colon Sort { [ SortArg $1 $3 ] } @@ -703,15 +715,21 @@ | doubleParens { Just [] } | { Nothing } +SumDecl : datatype IdentifierOr SortArgs eq Leaves { SumType $2 $3 $5 } + | datatype IdentifierOr SortArgs eq lineComment Leaves { SumType $2 $3 $6 } + | datatype lineComment IdentifierOr SortArgs eq Leaves { SumType $3 $4 $6 } + | datatype lineComment IdentifierOr SortArgs eq lineComment Leaves { SumType $3 $4 $7 } + | datavtype IdentifierOr SortArgs eq Leaves { SumViewType $2 $3 $5 } + | datavtype IdentifierOr SortArgs eq lineComment Leaves { SumViewType $2 $3 $6 } + | datavtype lineComment IdentifierOr SortArgs eq Leaves { SumViewType $3 $4 $6 } + | datavtype lineComment IdentifierOr SortArgs eq lineComment Leaves { SumViewType $3 $4 $7 } + | dataview IdentifierOr SortArgs eq Leaves { DataView $1 $2 $3 $5 } + | dataview IdentifierOr SortArgs eq lineComment Leaves { DataView $1 $2 $3 $6 } + -- | Parse a declaration defining a type TypeDecl : typedef IdentifierOr SortArgs eq Type { TypeDef $1 $2 $3 $5 } | vtypedef IdentifierOr SortArgs eq Type { ViewTypeDef $1 $2 $3 $5 } | extern vtypedef string SortArgs eq Type { Extern $1 $ ViewTypeDef $2 $3 $4 $6 } - | datatype IdentifierOr SortArgs eq Leaves { SumType $2 $3 $5 } - | datatype lineComment IdentifierOr SortArgs eq Leaves { SumType $3 $4 $6 } - | datavtype IdentifierOr SortArgs eq Leaves { SumViewType $2 $3 $5 } - | datavtype lineComment IdentifierOr SortArgs eq Leaves { SumViewType $3 $4 $6 } - | dataview IdentifierOr SortArgs eq Leaves { DataView $1 $2 $3 $5 } | abst0p IdentifierOr SortArgs MaybeType { AbsT0p $1 $2 $3 $4 } | viewdef IdentifierOr SortArgs eq Type { ViewDef $1 $2 $3 $5 } | absvt0p IdentifierOr SortArgs eq Type { AbsVT0p $1 $2 $3 (Just $5) } @@ -719,9 +737,10 @@ | abstype IdentifierOr SortArgs MaybeType { AbsType $1 $2 $3 $4 } | absvtype IdentifierOr SortArgs MaybeType { AbsViewType $1 $2 $3 $4 } | dataprop IdentifierOr SortArgs eq DataPropLeaves { DataProp $1 $2 $3 $5 } - | absprop IdentifierOr openParen FullArgs closeParen { AbsProp $1 $2 $4 } + | absprop IdentifierOr openParen Args closeParen { AbsProp $1 $2 $4 } | AndSort { $1 } | AndStadef { $1 } + | SumDecl { $1 } | extern typedef {% left $ Expected $2 "external declaration" "typedef" } | vtypedef IdentifierOr SortArgs eq vbar {% left $ Expected $5 "Viewtype" "|" } | typedef IdentifierOr SortArgs eq vbar {% left $ Expected $5 "Type" "|" } @@ -730,16 +749,35 @@ | dataview IdentifierOr SortArgs vbar {% left $ Expected $4 "=" "|" } | dataprop IdentifierOr SortArgs vbar {% left $ Expected $4 "=" "|" } -Fixity : infixr intLit { RightFix $1 $2 } - | infixl intLit { LeftFix $1 $2 } - | prefix intLit { Pre $1 $2 } - | postfix intLit { Post $1 $2 } +EitherInt : intLit { Left $1 } + | openParen Operator closeParen { Right $2 } --- FIXME adopt a principled approach --- perhaps match operators? +Fixity : infixr EitherInt { RightFix $1 $2 } + | infixl EitherInt { LeftFix $1 $2 } + | prefix EitherInt { Pre $1 $2 } + | postfix EitherInt { Post $1 $2 } + Operator : identifierSpace { to_string $1 } | customOperator { to_string $1 } | mutateArrow { "->" } + | exclamation { "!" } + | tilde { "~" } + | mult { "*" } + | div { "/" } + | plus { "+" } + | minus { "-" } + | or { "||" } + | andOp { "&&" } + | lbracket { "<" } + | rbracket { ">" } + | leq { "<=" } + | geq { ">=" } + | percent { "%" } + | mod { "mod" } + | mutateEq { ":=" } + | doubleEq { "==" } + | doubleBrackets { "<>" } + | neq { "!=" } Operators : Operator { [$1] } | Operators Operator { $2 : $1 } @@ -753,7 +791,9 @@ | extern ValDecl { over _head (Extern $1) $2 } | val Pattern eq colon {% left $ Expected $4 "Expression" ":" } -StaticDeclaration : prval Pattern eq Expression { PrVal $2 $4 } +StaticDeclaration : prval Pattern eq Expression { PrVal $2 (Just $4) Nothing } + | prval Pattern colon Type { PrVal $2 Nothing (Just $4) } + | prval Pattern colon Type eq Expression { PrVal $2 (Just $6) (Just $4) } | praxi PreFunction { Func $1 (Praxi $2) } | primplmnt FunArgs StaticImplementation { ProofImpl $2 $3 } | StafunDecl { $1 } @@ -761,6 +801,7 @@ DataSortLeaf : vbar Universals Sort { DataSortLeaf $2 $3 Nothing } | vbar Universals Sort of Sort { DataSortLeaf $2 $3 (Just $5) } + | DataSortLeaf Comment { $1 } DataSortLeaves : DataSortLeaf { [$1] } | DataSortLeaves DataSortLeaf { $2 : $1 } @@ -770,6 +811,13 @@ Comment : beginComment CommentContents endComment { over comment ((<> "*)") . ("(*" <>)) $2 } +Names : Name { [$1] } + | identifierSpace { [Unqualified $ to_string $1] } + | customOperator { [Unqualified $ to_string $1] } + | Names Name { $2 : $1 } + | Names identifierSpace { Unqualified (to_string $2) : $1 } + | Names customOperator { Unqualified (to_string $2) : $1 } + -- | Parse a declaration Declaration : include string { Include $2 } | define { Define $1 } @@ -797,6 +845,7 @@ | var Pattern eq lamAt StackFunction { Var Nothing $2 (Just $ LambdaAt $4 $5) Nothing } | implement FunArgs Implementation { Impl $2 $3 } | StaticDeclaration { $1 } + | overload lsqbracket rsqbracket with IdentifierOr { OverloadIdent $1 "[]" (Unqualified $5) Nothing } | overload BinOp with Name { OverloadOp $1 $2 $4 Nothing } | overload BinOp with customOperator { OverloadOp $1 $2 (Unqualified $ to_string $4) Nothing } | overload BinOp with identifierSpace of intLit { OverloadOp $1 $2 (Unqualified $ to_string $4) (Just $6) } @@ -811,8 +860,7 @@ | assume Name openParen Args closeParen eq Type { Assume $2 $4 $7 } | tkindef IdentifierOr eq string { TKind $1 (Unqualified $2) $4 } | TypeDecl { $1 } - | symintr Name { SymIntr $1 $2 } - | symintr customOperator { SymIntr $1 (Unqualified $ to_string $2) } + | symintr Names { SymIntr $1 $2 } | stacst IdentifierOr colon Type OptExpression { Stacst $1 (Unqualified $2) $4 $5 } | propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 $4 $7 } | exception identifierSpace of doubleParens { Exception (to_string $2) (Tuple $4 mempty) } @@ -829,12 +877,13 @@ | identifier {% left $ Expected (token_posn $1) "Declaration" (to_string $1) } | identifierSpace {% left $ Expected (token_posn $1) "Declaration" (to_string $1) } | where {% left $ Expected $1 "Declaration" "where" } + | vbar {% left $ Expected $1 "Declaration" "|" } { type ParseSt a = StateT (FixityState AlexPosn) (Either ATSError) a -addSt :: Fixity AlexPosn -> [String] -> ParseSt (Declaration AlexPosn) +addSt :: (Fixity AlexPosn) -> [String] -> ParseSt (Declaration AlexPosn) addSt x keys = modify (thread inserts) >> pure (FixityDecl x keys) where inserts = flip M.insert x <$> keys 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 @@ -231,8 +231,8 @@ argHelper _ (Arg (First s)) = pretty s argHelper _ (Arg (Second t)) = pretty t argHelper op (Arg (Both s t)) = pretty s `op` colon `op` pretty t -argHelper op (PrfArg a a') = pretty a `op` "|" `op` pretty a' -argHelper _ NoArgs = undefined -- in theory we handle this elsewhere. +argHelper op (PrfArg a a') = prettyArgs' ", " mempty mempty a "|" `op` pretty a' +argHelper _ NoArgs = undefined instance Eq a => Pretty (SortArg a) where pretty (SortArg n st) = text n <> ":" <+> pretty st @@ -301,7 +301,7 @@ a ImplicitTypeF{} = ".." a (AnonymousRecordF _ rs) = prettyRecord rs a (ParenTypeF _ t) = parens t - a (WhereTypeF _ t pref) = t <#> indent 2 ("where" pretty pref) + a (WhereTypeF _ t i sa t') = t <#> indent 2 ("where" pretty i <+> prettySortArgs sa <+> "=" <+> pretty t') gan :: Eq a => Maybe (Sort a) -> Doc gan (Just t) = " : " <> pretty t <> " " @@ -353,8 +353,9 @@ glue :: Declaration a -> Declaration a -> Bool glue x y | isVal x && isVal y = True +glue Stadef{} Stadef{} = True glue Staload{} Staload{} = True -glue Define{} Define{} = True +glue Define{} Define{} = True glue Include{} Include{} = True glue ViewTypeDef{} ViewTypeDef{} = True glue AbsViewType{} AbsViewType{} = True @@ -506,7 +507,7 @@ pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus pretty i <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e) pretty (PreF i si pus us as rt t (Just e)) = fancyU pus pretty i fancyU us <> prettyTermetric t <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e) pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgsNil as <> prettySigNull si rt - pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i fancyU us <> prettySigNull si rt + pretty (PreF i si [] us NoA rt Nothing Nothing) = pretty i fancyU us <> prettySigNull si rt pretty (PreF i si [] us as rt Nothing Nothing) = pretty i fancyU us prettyArgsNil as <> prettySigNull si rt pretty (PreF i si pus [] as rt t Nothing) = fancyU pus pretty i <> prettyTermetric t prettyArgsNil as <> prettySigNull si rt pretty (PreF i si pus us as rt t Nothing) = fancyU pus pretty i <> prettyTermetric t fancyU us prettyArgsNil as <> prettySigNull si rt @@ -515,12 +516,16 @@ 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' +prettyFix :: (Pretty a) => Either a String -> Doc +prettyFix (Left i) = pretty i +prettyFix (Right s) = parens (text s) + instance Eq a => Pretty (Fixity a) where - pretty (Infix _ i) = "infix" <+> pretty i - pretty (RightFix _ i) = "infixr" <+> pretty i - pretty (LeftFix _ i) = "infixl" <+> pretty i - pretty (Pre _ i) = "prefix" <+> pretty i - pretty (Post _ i) = "postfix" <+> pretty i + pretty (Infix _ i) = "infix" <+> prettyFix i + pretty (RightFix _ i) = "infixr" <+> prettyFix i + pretty (LeftFix _ i) = "infixl" <+> prettyFix i + pretty (Pre _ i) = "prefix" <+> prettyFix i + pretty (Post _ i) = "postfix" <+> prettyFix i prettyMaybeType :: (Pretty a) => Maybe a -> Doc prettyMaybeType (Just a) = " =" <+> pretty a @@ -534,69 +539,74 @@ prettySortArgs (Just as) = prettyArgs' ", " "(" ")" as instance Eq a => Pretty (Declaration a) where - pretty (Exception s t) = "exception" <+> text s <+> "of" <+> pretty t - pretty (AbsType _ s as t) = "abstype" <+> text s <> prettySortArgs as <> prettyMaybeType t - pretty (AbsViewType _ s as Nothing) = "absvtype" <+> text s <> prettySortArgs as - pretty (AbsViewType _ s as (Just t)) = "absvtype" <+> text s <> prettySortArgs as <+> "=" <+> pretty t - pretty (SumViewType s as ls) = "datavtype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls - pretty (DataView _ s as ls) = "dataview" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls - pretty (SumType s as ls) = "datatype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls - pretty (DataSort _ s ls) = "datasort" <+> text s <+> "=" <$> prettyDSL ls - pretty (Impl as i) = "implement" <+> prettyArgsNil as <> pretty i -- mconcat (fmap pretty us) <+> pretty i - pretty (ProofImpl as i) = "primplmnt" <+> prettyArgsNil as <> pretty i - pretty (PrVal p e) = "prval" <+> pretty p <+> "=" <+> pretty e - pretty (AndDecl t p e) = "and" <+> pretty p <> valSig t <+> "=" <+> pretty e - pretty (Val a t p e) = "val" <> pretty a <+> pretty p <> valSig t <+> "=" <+> pretty e - pretty (Var t p Nothing (Just e)) = "var" <+> pretty p <> valSig t <+> "with" <+> pretty e - pretty (Var t p (Just e) Nothing) = "var" <+> pretty p <> valSig t <+> "=" <+> pretty e - pretty (Var t p Nothing Nothing) = "var" <+> pretty p <> valSig t - pretty (Var _ _ _ Just{}) = undefined - pretty (Include s) = "#include" <+> pretty s - pretty (Staload b Nothing s) = bool "" "#" b <> "staload" <+> pretty s - pretty (Staload b (Just q) s) = bool "" "#" b <> "staload" <+> pretty q <+> "=" <+> pretty s - pretty (CBlock s) = string s - pretty (Comment s) = string s - pretty (OverloadOp _ o n (Just n')) = "overload" <+> pretty o <+> "with" <+> pretty n <+> "of" <+> pretty n' - pretty (OverloadOp _ o n Nothing) = "overload" <+> pretty o <+> "with" <+> pretty n - pretty (OverloadIdent _ i n Nothing) = "overload" <+> text i <+> "with" <+> pretty n - pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n' + pretty (Exception s t) = "exception" <+> text s <+> "of" <+> pretty t + pretty (AbsType _ s as t) = "abstype" <+> text s <> prettySortArgs as <> prettyMaybeType t + pretty (AbsViewType _ s as Nothing) = "absvtype" <+> text s <> prettySortArgs as + pretty (AbsViewType _ s as (Just t)) = "absvtype" <+> text s <> prettySortArgs as <+> "=" <+> pretty t + pretty (SumViewType s as ls) = "datavtype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls + pretty (DataView _ s as ls) = "dataview" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls + pretty (SumType s as ls) = "datatype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls + pretty (DataSort _ s ls) = "datasort" <+> text s <+> "=" <$> prettyDSL ls + pretty (Impl as i) = "implement" <+> prettyArgsNil as <> pretty i -- mconcat (fmap pretty us) <+> pretty i + pretty (ProofImpl as i) = "primplmnt" <+> prettyArgsNil as <> pretty i + pretty (PrVal p (Just e) Nothing) = "prval" <+> pretty p <+> "=" <+> pretty e + pretty (PrVal p Nothing (Just t)) = "prval" <+> pretty p <+> ":" <+> pretty t + pretty (PrVal p (Just e) (Just t)) = "prval" <+> pretty p <+> ":" <+> pretty t <+> "=" <+> pretty e + pretty PrVal{} = undefined + pretty (AndDecl t p e) = "and" <+> pretty p <> valSig t <+> "=" <+> pretty e + pretty (Val a t p e) = "val" <> pretty a <+> pretty p <> valSig t <+> "=" <+> pretty e + pretty (Var t p Nothing (Just e)) = "var" <+> pretty p <> valSig t <+> "with" <+> pretty e + pretty (Var t p (Just e) Nothing) = "var" <+> pretty p <> valSig t <+> "=" <+> pretty e + pretty (Var t p Nothing Nothing) = "var" <+> pretty p <> valSig t + pretty (Var _ _ _ Just{}) = undefined + pretty (Include s) = "#include" <+> pretty s + pretty (Staload b Nothing s) = bool "" "#" b <> "staload" <+> pretty s + pretty (Staload b (Just q) s) = bool "" "#" b <> "staload" <+> pretty q <+> "=" <+> pretty s + pretty (CBlock s) = string s + pretty (Comment s) = string s + pretty (OverloadOp _ o n (Just n')) = "overload" <+> pretty o <+> "with" <+> pretty n <+> "of" <+> pretty n' + pretty (OverloadOp _ o n Nothing) = "overload" <+> pretty o <+> "with" <+> pretty n + pretty (OverloadIdent _ i n Nothing) = "overload" <+> text i <+> "with" <+> pretty n + pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n' -- We use 'text' here, which means indentation might get fucked up for -- C preprocessor macros, but you absolutely deserve it if you indent your -- macros. - pretty (Define s) = text s - pretty (Func _ (Fn pref)) = "fn" pretty pref - pretty (Func _ (Fun pref)) = "fun" pretty pref - pretty (Func _ (CastFn pref)) = "castfn" pretty pref - pretty (Func _ (Fnx pref)) = "fnx" pretty pref - pretty (Func _ (And pref)) = "and" pretty pref - pretty (Func _ (Praxi pref)) = "praxi" pretty pref - pretty (Func _ (PrFun pref)) = "prfun" pretty pref - pretty (Func _ (PrFn pref)) = "prfn" pretty pref - pretty (Extern _ d) = "extern" <$> pretty d - pretty (DataProp _ s as ls) = "dataprop" <+> text s <> prettySortArgs as <+> "=" <$> prettyDL ls - pretty (ViewTypeDef _ s as t) = "vtypedef" <+> text s <> prettySortArgs as <+> "=" <#> pretty t - pretty (TypeDef _ s as t) = "typedef" <+> text s <> prettySortArgs as <+> "=" <+> pretty t - pretty (AbsProp _ n as) = "absprop" <+> text n <+> prettyArgs as - pretty (Assume n NoA e) = "assume" pretty n <+> "=" pretty e - 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 (PropDef _ s as t) = "propdef" text s <+> prettyArgsNil as <+> "=" pretty t - pretty (Local _ (ATS ds) (ATS [])) = "local" <$> indent 2 (pretty (ATS $ reverse ds)) <$> "in end" - pretty (Local _ d d') = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end" - pretty (FixityDecl f ss) = pretty f <+> hsep (fmap text ss) - pretty (StaVal us i t) = "val" mconcat (fmap pretty us) <+> text i <+> ":" <+> pretty t - pretty (Stadef i as t) = "stadef" <+> text i <+> prettySortArgs as <> pretty t - pretty (AndD d (Stadef i as t)) = pretty d <+> "and" <+> text i <+> prettySortArgs as <> pretty t - pretty (AbsView _ i as t) = "absview" <+> text i <> prettySortArgs as <> prettyMaybeType t - pretty (AbsVT0p _ i as t) = "absvt@ype" <+> text i <> prettySortArgs as <> prettyMaybeType t - pretty (AbsT0p _ i Nothing t) = "abst@ype" <+> text i <+> "=" <+> pretty t - pretty (AbsT0p _ i as t) = "abst@ype" <+> text i <> prettySortArgs as <> "=" <+> pretty t - pretty (ViewDef _ s as t) = "viewdef" <+> text s <> prettySortArgs as <+> "=" <#> pretty t - pretty (TKind _ n s) = pretty n <+> "=" <+> text s - 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 (MacDecl _ n is e) = "macdef" <+> text n <> "(" <> mconcat (punctuate ", " (fmap text is)) <> ") =" <+> pretty e - pretty (ExtVar _ s e) = "extvar" <+> text s <+> "=" <+> pretty e - pretty AndD{} = undefined -- probably not valid syntax if we get to this point + pretty (Define s) = text s + pretty (Func _ (Fn pref)) = "fn" pretty pref + pretty (Func _ (Fun pref)) = "fun" pretty pref + pretty (Func _ (CastFn pref)) = "castfn" pretty pref + pretty (Func _ (Fnx pref)) = "fnx" pretty pref + pretty (Func _ (And pref)) = "and" pretty pref + pretty (Func _ (Praxi pref)) = "praxi" pretty pref + pretty (Func _ (PrFun pref)) = "prfun" pretty pref + pretty (Func _ (PrFn pref)) = "prfn" pretty pref + pretty (Extern _ d) = "extern" <$> pretty d + pretty (DataProp _ s as ls) = "dataprop" <+> text s <> prettySortArgs as <+> "=" <$> prettyDL ls + pretty (ViewTypeDef _ s as t) = "vtypedef" <+> text s <> prettySortArgs as <+> "=" <#> pretty t + pretty (TypeDef _ s as t) = "typedef" <+> text s <> prettySortArgs as <+> "=" <+> pretty t + pretty (AbsProp _ n as) = "absprop" <+> text n <+> prettyArgs as + pretty (Assume n NoA e) = "assume" pretty n <+> "=" pretty e + pretty (Assume n as e) = "assume" pretty n <> prettyArgs as <+> "=" pretty e + pretty (SymIntr _ ns) = "symintr" <+> hsep (fmap pretty ns) + pretty (Stacst _ n t Nothing) = "stacst" pretty n <+> ":" pretty t + pretty (Stacst _ n t (Just e)) = "stacst" pretty n <+> ":" pretty t <+> "=" pretty e + pretty (PropDef _ s as t) = "propdef" text s <+> prettyArgsNil as <+> "=" pretty t + pretty (Local _ (ATS ds) (ATS [])) = "local" <$> indent 2 (pretty (ATS $ reverse ds)) <$> "in end" + pretty (Local _ d d') = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end" + pretty (FixityDecl f ss) = pretty f <+> hsep (fmap text ss) + pretty (StaVal us i t) = "val" mconcat (fmap pretty us) <+> text i <+> ":" <+> pretty t + pretty (Stadef i as (Right t)) = "stadef" <+> text i <+> prettySortArgs as <+> "=" <+> pretty t + pretty (Stadef i as (Left se)) = "stadef" <+> text i <+> prettySortArgs as <+> "=" <+> pretty se + pretty (AndD d (Stadef i as (Right t))) = pretty d <+> "and" <+> text i <+> prettySortArgs as <+> "=" <+> pretty t + pretty (AndD d (Stadef i as (Left se))) = pretty d <+> "and" <+> text i <+> prettySortArgs as <+> "=" <+> pretty se + pretty (AbsView _ i as t) = "absview" <+> text i <> prettySortArgs as <> prettyMaybeType t + pretty (AbsVT0p _ i as t) = "absvt@ype" <+> text i <> prettySortArgs as <> prettyMaybeType t + pretty (AbsT0p _ i Nothing t) = "abst@ype" <+> text i <+> "=" <+> pretty t + pretty (AbsT0p _ i as t) = "abst@ype" <+> text i <> prettySortArgs as <> "=" <+> pretty t + pretty (ViewDef _ s as t) = "viewdef" <+> text s <> prettySortArgs as <+> "=" <#> pretty t + pretty (TKind _ n s) = pretty n <+> "=" <+> text s + 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 (MacDecl _ n is e) = "macdef" <+> text n <> "(" <> mconcat (punctuate ", " (fmap text is)) <> ") =" <+> pretty e + pretty (ExtVar _ s e) = "extvar" <+> text s <+> "=" <+> pretty e + 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 @@ -50,6 +50,8 @@ -- * Rewrites , rewriteATS , rewriteDecl + -- * Helper functions + , defaultFixityState -- * Lenses , preF , expression @@ -73,11 +75,13 @@ import GHC.Generics (Generic) import Language.ATS.Lexer (Addendum (..)) -data Fixity a = RightFix { pos :: a, ifix :: Int } - | LeftFix { pos :: a, ifix :: Int } - | Pre { pos :: a, ifix :: Int } - | Post { pos :: a, ifix :: Int } - | Infix { pos :: a, ifix :: Int } +type Fix = Either Int String + +data Fixity a = RightFix { pos :: a, ifix :: Fix } + | LeftFix { pos :: a, ifix :: Fix } + | Pre { pos :: a, ifix :: Fix } + | Post { pos :: a, ifix :: Fix } + | Infix { pos :: a, ifix :: Fix } deriving (Show, Eq, Generic, NFData) -- | Newtype wrapper containing a list of declarations @@ -96,12 +100,12 @@ | ProofImpl { implArgs :: [Arg a], _impl :: Implementation a } | Val { add :: Addendum, valT :: Maybe (Type a), valPat :: Pattern a, _valExpression :: Expression a } | StaVal [Universal a] String (Type a) - | PrVal { prvalPat :: Pattern a, _prValExpr :: Expression a } + | PrVal { prvalPat :: Pattern a, _prValExpr :: Maybe (Expression a), prValType :: Maybe (Type a) } | Var { varT :: Maybe (Type a), varPat :: Pattern a, _varExpr1 :: Maybe (Expression a), _varExpr2 :: Maybe (Expression a) } | AndDecl { andT :: Maybe (Type a), andPat :: Pattern a, _andExpr :: Expression a } | Include String | Staload Bool (Maybe String) String - | Stadef String (SortArgs a) (Type a) -- [Type] -- FIXME stadef array(a:vt@ype, n:int) = @[a][n] + | Stadef String (SortArgs a) (Either (StaticExpression a) (Type a)) | CBlock String | TypeDef a String (SortArgs a) (Type a) | ViewTypeDef a String (SortArgs a) (Type a) @@ -126,7 +130,7 @@ | AbsProp a String [Arg a] | Assume (Name a) [Arg a] (Type a) | TKind a (Name a) String - | SymIntr a (Name a) + | SymIntr a [Name a] | Stacst a (Name a) (Type a) (Maybe (Expression a)) | PropDef a String [Arg a] (Type a) | FixityDecl (Fixity a) [String] @@ -164,7 +168,7 @@ | ViewLiteral Addendum | AnonymousRecord a [(String, Type a)] | ParenType a (Type a) - | WhereType a (Type a) (PreFunction a) + | WhereType a (Type a) String (SortArgs a) (Type a) deriving (Show, Eq, Generic, NFData) -- | A type for @=>@, @=\@, etc. @@ -205,7 +209,7 @@ -- | An argument to a function. data Arg a = Arg (Paired String (Type a)) - | PrfArg (Arg a) (Arg a) + | PrfArg [Arg a] (Arg a) | NoArgs deriving (Show, Eq, Generic, NFData) @@ -268,7 +272,12 @@ -- | A (possibly effectful) expression. data Expression a = Let a (ATS a) (Maybe (Expression a)) | VoidLiteral a -- ^ The '()' literal representing inaction. - | Call (Name a) [[Type a]] [Type a] (Maybe [Expression a]) [Expression a] + | Call { callName :: Name a + , callImplicits :: [[Type a]] -- ^ E.g. some_function + , callUniversals :: [Type a] -- ^ E.g. some_function{a} + , callProofs :: Maybe [Expression a] -- ^ E.g. @pf@ in @call(pf | str)@. + , callArgs :: [Expression a] -- ^ The actual call arguments. + } | NamedVal (Name a) | ListLiteral a String (Type a) [Expression a] | If { cond :: Expression a -- ^ Expression evaluating to a boolean value @@ -383,7 +392,7 @@ rewriteDecl st x@Var{} = exprLenses st [varExpr1._Just, varExpr2._Just] x rewriteDecl st x@Func{} = exprLens st (fun.preF.expression._Just) x rewriteDecl st x@Impl{} = exprLens st (impl.iExpression._Right) x -rewriteDecl st x@PrVal{} = exprLens st prValExpr x +rewriteDecl st x@PrVal{} = exprLens st (prValExpr._Just) x rewriteDecl st x@AndDecl{} = exprLens st andExpr x rewriteDecl st x@DataProp{} = exprLenses st (fmap ((propLeaves.each).) [propExpr1, propExpr2._Just]) x rewriteDecl _ x@SumViewType{} = g x @@ -401,40 +410,45 @@ compare = on compare ifix leftFix :: Int -> Fixity a -leftFix = LeftFix undefined +leftFix = LeftFix undefined . Left rightFix :: Int -> Fixity a -rightFix = RightFix undefined +rightFix = RightFix undefined . Left infix_ :: Int -> Fixity a -infix_ = Infix undefined +infix_ = Infix undefined . Left type FixityState a = M.Map String (Fixity a) +defaultFixityState :: FixityState a +defaultFixityState = M.fromList + [ ("::", rightFix 40) ] + -- | Default fixities from @fixity.ats@ getFixity :: FixityState a -> BinOp a -> Fixity a -getFixity _ Add = leftFix 50 -getFixity _ Sub = leftFix 50 -getFixity _ Mutate = infix_ 0 -getFixity _ Mult = leftFix 60 -getFixity _ Div = leftFix 60 -getFixity _ SpearOp = rightFix 10 -getFixity _ LogicalAnd = leftFix 21 -getFixity _ LogicalOr = leftFix 20 -getFixity _ At = rightFix 40 -getFixity _ GreaterThan = infix_ 40 -getFixity _ GreaterThanEq = infix_ 40 -getFixity _ LessThanEq = infix_ 40 -getFixity _ Equal = infix_ 30 -getFixity _ NotEq = infix_ 30 -getFixity _ StaticEq = infix_ 30 -getFixity _ Mod = leftFix 60 -getFixity _ LessThan = infix_ 40 +getFixity _ Add = leftFix 50 +getFixity _ Sub = leftFix 50 +getFixity _ Mutate = infix_ 0 +getFixity _ Mult = leftFix 60 +getFixity _ Div = leftFix 60 +getFixity _ SpearOp = rightFix 10 +getFixity _ LogicalAnd = leftFix 21 +getFixity _ LogicalOr = leftFix 20 +getFixity _ At = rightFix 40 +getFixity _ GreaterThan = infix_ 40 +getFixity _ GreaterThanEq = infix_ 40 +getFixity _ LessThanEq = infix_ 40 +getFixity _ Equal = infix_ 30 +getFixity _ NotEq = infix_ 30 +getFixity _ StaticEq = infix_ 30 +getFixity _ Mod = leftFix 60 +getFixity _ LessThan = infix_ 40 getFixity st (SpecialInfix _ op') = case M.lookup op' st of (Just f) -> f Nothing -> infix_ 100 +-- FIXME this should account for right vs. left associativity. compareFixity :: Eq a => FixityState a -> BinOp a -> BinOp a -> Bool compareFixity st = (== GT) .* on compare (getFixity st) @@ -448,6 +462,7 @@ a (CallF n ts ts' me [ParenExpr _ e@Call{}]) = Call n ts ts' me [e] a (PrecedeF e e'@PrecedeList{}) = PrecedeList (e : _exprs e') a (PrecedeF e e') = PrecedeList [e, e'] + a (CallF n _ _ _ [Unary (SpecialOp loc s) e]) = Binary (SpecialInfix loc s) (NamedVal n) e a (BinaryF op' (Binary op'' e e') e'') | compareFixity st op' op'' = Binary op'' e (Binary op' e' e'') a (BinaryF Add e (BinList Add es)) = BinList Add (e : es) @@ -455,4 +470,5 @@ a (ParenExprF _ e@Precede{}) = e a (ParenExprF _ e@PrecedeList{}) = e a (WhereExpF e (ATS ds)) = WhereExp e (ATS (rewriteDecl st <$> ds)) + a (ActionsF (ATS ds)) = Actions (ATS (rewriteDecl st <$> ds)) a x = embed x diff --git a/test/data/concurrency.out b/test/data/concurrency.out --- a/test/data/concurrency.out +++ b/test/data/concurrency.out @@ -27,13 +27,12 @@ [b:bool] (ISFULL(id, b) | bool(b)) extern -fun {a:vt0p} queue_insert {id:int} -(ISFULL(id,false) | xs : !queue(a, id) >> queue(a, id2), x : a) : - #[id2:int] void +fun {a:vt0p} queue_insert {id:int} (ISFULL(id,false) + | xs : !queue(a, id) >> queue(a, id2), x : a) : #[id2:int] void extern -fun {a:vt0p} queue_remove {id:int} -(ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) : #[id2:int] a +fun {a:vt0p} queue_remove {id:int} (ISNIL(id,false) +| xs : !queue(a, id) >> queue(a, id2)) : #[id2:int] a extern fun {a:vt0p} queue_make (cap : intGt(0)) : queue(a) diff --git a/test/data/fact.out b/test/data/fact.out --- a/test/data/fact.out +++ b/test/data/fact.out @@ -14,9 +14,8 @@ // TODO rewrite this for collatz? fnx fact {n:nat}(n : int(n)) : int = let - fun loop {n:nat}{l:addr} .. ( pf : !int @ l | n : int(n) - , res : ptr(l) - ) : void = + fun loop {n:nat}{l:addr} .. (pf : !int @ l + | n : int(n), res : ptr(l)) : void = if n > 0 then let val () = !res := n * !res diff --git a/test/data/fastcount.out b/test/data/fastcount.out --- a/test/data/fastcount.out +++ b/test/data/fastcount.out @@ -17,11 +17,10 @@ %} extern -fun rawmemchr {l:addr}{m:int}( pf : bytes_v(l, m) | p : ptr(l) - , c : int - ) : [ l2 : addr | l+m > l2 ] ( bytes_v(l, l2-l) - , bytes_v(l2, l+m-l2) - | ptr(l2)) = +fun rawmemchr {l:addr}{m:int}(pf : bytes_v(l, m) + | p : ptr(l), c : int) : [ l2 : addr | l+m > l2 ] ( bytes_v(l, l2-l) + , bytes_v(l2, l+m-l2) + | ptr(l2)) = "mac#atslib_rawmemchr" (* ****** ****** *) @@ -29,10 +28,8 @@ (* ****** ****** *) extern -fun freadc {l:addr} ( pf : !bytes_v(l, BUFSZ) | inp : FILEref - , p : ptr(l) - , c : char - ) : size_t +fun freadc {l:addr} (pf : !bytes_v(l, BUFSZ) + | inp : FILEref, p : ptr(l), c : char) : size_t implement freadc (pf | inp, p, c) = let @@ -44,11 +41,8 @@ (* ****** ****** *) extern -fun wclbuf {l:addr}{n:int} ( pf : !bytes_v(l, n) | p : ptr(l) - , pz : ptr - , c : int - , res : int - ) : int +fun wclbuf {l:addr}{n:int} (pf : !bytes_v(l, n) + | p : ptr(l), pz : ptr, c : int, res : int) : int implement wclbuf (pf | p, pz, c, res) = let @@ -73,18 +67,13 @@ (* ****** ****** *) extern -fun wclfil {l:addr} ( pf : !bytes_v(l, BUFSZ) | inp : FILEref - , p : ptr(l) - , c : int - ) : int +fun wclfil {l:addr} (pf : !bytes_v(l, BUFSZ) + | inp : FILEref, p : ptr(l), c : int) : int implement wclfil {l} (pf | inp, p, c) = let - fun loop( pf : !bytes_v(l, BUFSZ) | inp : FILEref - , p : ptr(l) - , c : int - , res : int - ) : int = + fun loop(pf : !bytes_v(l, BUFSZ) + | inp : FILEref, p : ptr(l), c : int, res : int) : int = let val n = freadc(pf | inp, p, $UN.cast{char}(c)) in diff --git a/test/data/fib-thm.dats b/test/data/fib-thm.dats new file mode 100644 --- /dev/null +++ b/test/data/fib-thm.dats @@ -0,0 +1,50 @@ +// example from the book: http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop/main.html +#include "share/atspre_staload.hats" + +staload "prelude/SATS/integer.sats" + +infixr (->) ->> + +stadef ->> (b1: bool, b2: bool) = ~b1 || b2 + +dataprop fib_p(int, int) = + | fib_p_bas0(0, 0) of () + | fib_p_bas1(1, 1) of () + | {n:nat}{ r0, r1 : int } fib_p_ind2(n + 2, r0 + r1) of (fib_p(n, r0), fib_p(n + 1, r1)) + +stacst fib_b : (int, int) -> bool + +extern +praxi fib_b_bas0() : [fib_b(0,0)] unit_p + +extern +praxi fib_b_bas1() : [fib_b(1,1)] unit_p + +extern +praxi fib_b_ind2 {n:nat}{ r0, r1 : int } : [fib_b(n,r0) && fib_b(n+1,r1) ->> fib_b(n+2,r0+r1)] unit_p + +fun f_fib_p {n:nat}(n : int(n)) : [r:int] (fib_p(n, r) | int(r)) = + let + fun loop { i : nat | i < n }{ r0, r1 : int }(pf0 : fib_p(i, r0), pf1 : fib_p(i+1, r1) + | i : int(i), r0 : int(r0), r1 : int(r1)) : + [r:int] (fib_p(n, r) | int(r)) = + if i + 1 < n then + loop(pf1, fib_p_ind2(pf0, pf1) | i + 1, r1, r0 + r1) + else + (pf1 | r1) + + prval pf0 = fib_p_bas0() + prval pf1 = fib_p_bas1() + in + if n >= 1 then + loop(pf0, pf1 | 0, 0, 1) + else + (pf0 | 0) + end + +implement main0 () = + let + val (_ | i) = f_fib_p(40) + in + println!(i) + end diff --git a/test/data/fib-thm.out b/test/data/fib-thm.out new file mode 100644 --- /dev/null +++ b/test/data/fib-thm.out @@ -0,0 +1,54 @@ +// example from the book: http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop/main.html +#include "share/atspre_staload.hats" + +staload "prelude/SATS/integer.sats" + +infixr (->) ->> + +stadef ->> (b1: bool, b2: bool) = ~b1 || b2 + +dataprop fib_p(int, int) = + | fib_p_bas0(0, 0) of () + | fib_p_bas1(1, 1) of () + | {n:nat}{ r0, r1 : int } fib_p_ind2(n + 2, r0 + r1) of (fib_p( n + , r0 + ), fib_p(n + 1, r1)) + +stacst fib_b : (int, int) -> bool + +extern +praxi fib_b_bas0() : [fib_b(0,0)] unit_p + +extern +praxi fib_b_bas1() : [fib_b(1,1)] unit_p + +extern +praxi fib_b_ind2 {n:nat}{ r0, r1 : int } : + [fib_b(n,r0) && fib_b(n+1,r1) ->> fib_b(n+2,r0+r1)] unit_p + +fun f_fib_p {n:nat}(n : int(n)) : [r:int] (fib_p(n, r) | int(r)) = + let + fun loop { i : nat | i < n }{ r0, r1 : int }( pf0 : fib_p(i, r0) + , pf1 : fib_p(i+1, r1) + | i : int(i), r0 : int(r0), r1 : int(r1)) : + [r:int] (fib_p(n, r) | int(r)) = + if i + 1 < n then + loop(pf1, fib_p_ind2(pf0, pf1) | i + 1, r1, r0 + r1) + else + (pf1 | r1) + + prval pf0 = fib_p_bas0() + prval pf1 = fib_p_bas1() + in + if n >= 1 then + loop(pf0, pf1 | 0, 0, 1) + else + (pf0 | 0) + end + +implement main0 () = + let + val (_ | i) = f_fib_p(40) + in + println!(i) + end