language-ats 1.0.1.1 → 1.0.2.0
raw patch · 12 files changed
+360/−190 lines, 12 files
Files
- README.md +2/−0
- language-ats.cabal +1/−1
- src/Language/ATS.hs +2/−1
- src/Language/ATS/Lexer.x +17/−16
- src/Language/ATS/Parser.y +85/−36
- src/Language/ATS/PrettyPrint.hs +83/−73
- src/Language/ATS/Types.hs +48/−32
- test/data/concurrency.out +4/−5
- test/data/fact.out +2/−3
- test/data/fastcount.out +12/−23
- test/data/fib-thm.dats +50/−0
- test/data/fib-thm.out +54/−0
README.md view
@@ -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.
language-ats.cabal view
@@ -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
src/Language/ATS.hs view
@@ -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)
src/Language/ATS/Lexer.x view
@@ -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 @@ <three> @comment_in+ / [^\)] { tok (\p s -> alex $ CommentContents p s) } <three> @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
src/Language/ATS/Parser.y view
@@ -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
src/Language/ATS/PrettyPrint.hs view
@@ -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
src/Language/ATS/Types.hs view
@@ -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 @=>@, @=\<cloref1>@, 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<a>+ , 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
test/data/concurrency.out view
@@ -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)
test/data/fact.out view
@@ -14,9 +14,8 @@ // TODO rewrite this for collatz? fnx fact {n:nat}(n : int(n)) : int = let- fun loop {n:nat}{l:addr} .<n>. ( pf : !int @ l | n : int(n)- , res : ptr(l)- ) : void =+ fun loop {n:nat}{l:addr} .<n>. (pf : !int @ l+ | n : int(n), res : ptr(l)) : void = if n > 0 then let val () = !res := n * !res
test/data/fastcount.out view
@@ -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
+ test/data/fib-thm.dats view
@@ -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
+ test/data/fib-thm.out view
@@ -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