language-ats 0.3.0.1 → 0.3.0.2

raw patch · 10 files changed

+182/−59 lines, 10 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• bench/Bench.hs +3/−3
• language-ats.cabal +1/−1
• src/Language/ATS.hs +13/−4
• src/Language/ATS/Lexer.x +28/−15
• src/Language/ATS/Parser.y +39/−11
• src/Language/ATS/PrettyPrint.hs +8/−5
• src/Language/ATS/Types.hs +12/−9
• test/data/concurrency.out +11/−11
• test/data/either.out +37/−0
• test/data/either.sats +30/−0

@@ -7,14 +7,14 @@ main =     defaultMain [ env envFiles $ \ ~(l, m) ->                   bgroup "format"-                      [ bench "lexATS (large)" $ nf lex l+                      [ bench "lexATS (large)" $ nf lexATS l                       , bench "parseATS . lexATS (large)" $ nf parse l                       , bench "printATS . parseATS . lexATS (large)" $ nf (fmap printATS . parse) l-                      , bench "lexATS (medium)" $ nf lex m+                      , bench "lexATS (medium)" $ nf lexATS m                       , bench "parseATS . lexATS (medium)" $ nf parse m                       , bench "printATS . parseATS . lexATS (medium)" $ nf (fmap printATS . parse) m                       ]                 ]     where large = readFile "test/data/polyglot.dats"-          medium = readFile "test/data/stdlib/checkast.sats"+          medium = readFile "test/data/concurrency.dats"           envFiles = (,) <$> large <*> medium

@@ -1,5 +1,5 @@ name:                language-ats-version:             0.3.0.1+version:             0.3.0.2 synopsis:            Parser and pretty-printer for ATS. description:         Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex. license:             BSD3

@@ -1,10 +1,11 @@ -- | Main module for the library module Language.ATS ( -- * Functions for working with syntax-                      lex+                      lexATS                     , parse                     , printATS                     , printATSCustom                     , printATSFast+                    , printErr                     -- * Library functions                     , getDependencies                     -- * Syntax Tree@@ -46,20 +47,28 @@                     , typeCallArgs                     ) where -import           Data.Maybe               (catMaybes)+import           Control.Lens+import           Control.Monad+import           Control.Monad.IO.Class+import           Data.Maybe                   (catMaybes)+import           GHC.IO.Handle.FD             (stderr) import           Language.ATS.Lexer import           Language.ATS.Parser import           Language.ATS.PrettyPrint import           Language.ATS.Types+import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))  rewriteATS' :: ATS -> ATS rewriteATS' (ATS ds) = ATS (rewriteDecl <$> ds) +printErr :: MonadIO m => ATSError String -> m ()+printErr = liftIO . hPutDoc stderr . pretty+ -- | Parse a string containing ATS source. parse :: String -> Either (ATSError String) ATS-parse = fmap rewriteATS' . parseATS . lexATS+parse = fmap rewriteATS' . (parseATS <=< (over _Left LexError . lexATS)) --- TODO use Language.C.Parser here?+-- TODO use prepocessing?? here? getDependencies :: ATS -> [FilePath] getDependencies (ATS ds) = catMaybes (g <$> ds)     where g (Staload _ _ s) = Just s

@@ -100,25 +100,25 @@  @builtin = \$ (("effmask_" (wrt | all | ref)) | "extfcall" | "ldelay" | "delay" | "list_vt" | "tempenver" | "extype" | "mylocation" | "showtype") -@block_comment_start = \(\* | \*\/+@block_comment_start = \(\* | \/\* @block_comment_end = \*\) | \*\/ -@comment_in = [\*\)\(\/$white]+@comment_in = [\*$white]+@comment_general = @comment_in | [\)\(\/]  tokens :-      <0> $white+                  ;-    -- <0> @block_comment_start     { begin one }-    -- <one> @block_comment_end     { begin 0 }-    -- <one> @block_comment_start   { begin two }-    -- <one> [^\*\)\/]+             ;-    -- <one> @comment_in+ / [^\)]   ;-    -- <one> @comment_in            ;-    -- <two> @block_comment_end     { begin one }-    -- <two> [^\*\)\/]+             ;-    -- <two> @comment_in+ / [^\)]   ;-    -- <two> @comment_in            ;-    @block_comment               { tok (\p s -> alex $ CommentLex p s) }+    <0> @block_comment_start     { tok (\p s -> alex $ CommentBegin p) `andBegin` one }+    <one> @block_comment_end     { tok (\p s -> alex $ CommentEnd p) `andBegin` 0 }+    <one> @block_comment_start   { tok (\p s -> alex $ CommentContents p s) `andBegin` two }+    <one> [^\*\(\)\/]+           { tok (\p s -> alex $ CommentContents p s) }+    <one> @comment_in+ / [^\)]   { tok (\p s -> alex $ CommentContents p s) }+    <one> @comment_general       { tok (\p s -> alex $ CommentContents p s) }+    <two> @block_comment_end     { tok (\p s -> alex $ CommentContents p s) `andBegin` one }+    <two> [^\*\(\)\/]+           { tok (\p s -> alex $ CommentContents p s) }+    <two> @comment_in+ / [^\)]   { tok (\p s -> alex $ CommentContents p s) }+    <two> @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) }      @@ -213,6 +213,7 @@     <0> sta                      { tok (\p s -> alex $ Keyword p KwSta) }     <0> symintr                  { tok (\p s -> alex $ Keyword p KwSymintr) }     <0> absview                  { tok (\p s -> alex $ Keyword p KwAbsview) }+    <0> exception                { tok (\p s -> alex $ Keyword p KwException) }     <0> "$list"                  { tok (\p s -> alex $ Keyword p (KwListLit "")) }     <0> "$list_vt"               { tok (\p s -> alex $ Keyword p (KwListLit "_vt")) }     <0> "fold@"                  { tok (\p s -> alex $ IdentifierSpace p s) }@@ -337,6 +338,7 @@              | KwListLit String              | KwMacdef              | KwDatasort+             | KwException              deriving (Eq, Show, Generic, NFData)  data Token = Identifier AlexPosn String@@ -353,6 +355,9 @@            | Arrow AlexPosn String            | FuncType AlexPosn String            | CommentLex AlexPosn String+           | CommentBegin AlexPosn+           | CommentEnd AlexPosn+           | CommentContents AlexPosn String            | MacroBlock AlexPosn String            | TimeTok AlexPosn String            | SignatureTok AlexPosn String@@ -391,6 +396,7 @@     pretty (KwCase c) = "case" <> pretty c     pretty KwIfCase = "ifcase"     pretty KwIf = "if"+    pretty KwException = "exception"     pretty KwSif = "sif"     pretty KwThen = "then"     pretty KwElse = "else"@@ -458,6 +464,9 @@     pretty CBlockLex{} = "%{"     pretty (Arrow _ s) = text s     pretty (CommentLex _ s) = text $ take 2 s+    pretty CommentBegin{} = "(*"+    pretty CommentEnd{} = "*)"+    pretty (CommentContents _ s) = text s     pretty (FuncType _ s) = text s     pretty (TimeTok _ s) = text s     pretty (SignatureTok _ s) = ":" <> text s@@ -475,6 +484,7 @@ to_string (IdentifierSpace _ s) = s to_string (SpecialIdentifier _ s) = s to_string (Operator _ s) = s+to_string (CommentContents _ s) = s to_string _ = undefined  token_posn (SpecialIdentifier p _) = p@@ -499,6 +509,9 @@ token_posn (DoubleBracketTok p) = p token_posn (SpecialBracket p) = p token_posn (FixityTok p _) = p+token_posn (CommentContents p _) = p+token_posn (CommentBegin p) = p+token_posn (CommentEnd p) = p token_posn End = undefined  toChar :: String -> Char@@ -511,8 +524,8 @@ alexEOF = pure End  -- | This function turns a string into a stream of tokens for the parser.-lexATS :: String -> [Token]-lexATS str = either error id . runAlex str $ loop+lexATS :: String -> Either String [Token]+lexATS str = runAlex str $ loop  loop :: Alex [Token] loop = do

@@ -6,7 +6,7 @@      -- | This module contains the parser.     module Language.ATS.Parser ( parseATS-                               , ATSError+                               , ATSError (..)                                ) where  import Language.ATS.Types@@ -71,9 +71,11 @@     case { Keyword _ (KwCase $$) }     ifcase { Keyword $$ KwIfCase }     datatype { Keyword $$ KwDatatype }+    dataview { Keyword $$ KwDataview }     datavtype { Keyword $$ KwDatavtype }     while { Keyword $$ KwWhile }     of { Keyword $$ KwOf }+    exception { Keyword $$ KwException }     include { Keyword $$ KwInclude }     staload { $$@(Keyword _ (KwStaload _)) }     overload { Keyword $$ KwOverload }@@ -177,6 +179,9 @@     prefix { FixityTok $$ "prefix" }     postfix { FixityTok $$ "postfix" }     customOperator { $$@Operator{} }+    beginComment { CommentBegin $$ }+    endComment { CommentEnd $$ }+    commentContents { CommentContents _ $$ }  %% @@ -215,7 +220,8 @@      | Type prfTransform underscore { AsProof $1 Nothing }      | view at Type { ViewType $1 $3 }      | viewPlusMinus { ViewLiteral $1 }-     | Existential Type { Ex $1 $2 }+     | Existential Type { Ex $1 (Just $2) }+     | Existential { Ex $1 Nothing }      | Universal Type { ForA $1 $2 }      | Type at StaticExpression { AtExpr $2 $1 $3 }      | at Type { AtType $1 $2 }@@ -239,6 +245,7 @@      | Arg vbar Arg { [ PrfArg $1 $3 ] }      | lineComment { [] }      | Args lineComment { $1 }+     | Args Comment { $1 }      | { [] }  TypeArg : identifier { Arg (First $ to_string $1) }@@ -394,7 +401,6 @@               | viewAt PreExpression { ViewAt $1 $2 }               | atbrace RecordVal rbrace { RecordValue $1 $2 Nothing }               | atbrace RecordVal rbrace colon Type { RecordValue $1 $2 (Just $5) }-              | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 }               | begin Expression end { Begin $1 $2 }               | identifierSpace { NamedVal (Unqualified $ to_string $1) }               | Name { NamedVal $1 }@@ -402,6 +408,7 @@               | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }               | lineComment PreExpression { CommentExpr (to_string $1) $2 }               | comma openParen identifier closeParen { MacroVar $1 (to_string $3) }+              | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 }               | include {% Left $ Expected $1 "Expression" "include" }               | staload {% Left $ Expected (token_posn $1) "Expression" "staload" }               | overload {% Left $ Expected $1 "Expression" "overload" }@@ -417,6 +424,7 @@               | let ATS in Expression vtypedef {% Left $ Expected $5 "end" "vtypedef" }               | let ATS in Expression implement {% Left $ Expected $5 "end" "implement" }               | 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" }  -- | Parse a termetric@@ -434,10 +442,11 @@      | viewContra { View $1 Minus }      | vtype { VType (token_posn $1) (get_addendum $1) }      | IdentifierOr { NamedSort $1 }+     | IdentifierOr plus { NamedSort ($1 <> "+") }  QuantifierArgs : IdentifierOr { [$1] }-               | { [] }                | QuantifierArgs comma IdentifierOr { $3 : $1 }+               | { [] }  Existential : lsqbracket QuantifierArgs colon Sort vbar StaticExpression rsqbracket { Existential $2 False (Just $4) (Just $6) }             | lsqbracket QuantifierArgs colon Sort rsqbracket { Existential $2 False (Just $4) Nothing }@@ -507,17 +516,20 @@ OfType : { Nothing }        | of Type { Just $2 } +StaticExpressionsIn : StaticExpression { [$1] }+                    | StaticExpressionsIn comma StaticExpression { $3 : $1 }+ -- | Parse a constructor for a sum type SumLeaf : vbar Universals identifier { Leaf $2 (to_string $3) [] Nothing }         | vbar Universals identifierSpace of Type { Leaf $2 (to_string $3) [] (Just $5) }-        | vbar Universals IdentifierOr openParen IdentifiersIn closeParen OfType { Leaf $2 $3 $5 $7 }+        | vbar Universals IdentifierOr openParen StaticExpressionsIn closeParen OfType { Leaf $2 $3 $5 $7 } -- FIXME could also be e.g. '0' (static expression)  -- | Parse all constructors of a sum type Leaves : SumLeaf { [$1] }        | Leaves SumLeaf { $2 : $1 }        | Universals identifierSpace of Type { [Leaf $1 (to_string $2) [] (Just $4)] }        | Universals identifier { [Leaf $1 (to_string $2) [] Nothing] }-       | Universals identifier openParen IdentifiersIn closeParen OfType { [Leaf $1 (to_string $2) $4 $6] } -- FIXME should take any static expression.+       | Universals identifier openParen StaticExpressionsIn closeParen OfType { [Leaf $1 (to_string $2) $4 $6] } -- FIXME should take any static expression.        | dollar {% Left $ Expected $1 "|" "$" }  Universals : { [] }@@ -611,10 +623,9 @@         | sortdef IdentifierOr eq Sort { SortDef $1 $2 (Left $4) }         | sortdef IdentifierOr eq Universal { SortDef $1 $2 (Right $4) } -AndStadef : stadef IdentifierOr eq Name { Stadef $2 $4 [] }-          | stadef IdentifierOr eq identifierSpace { Stadef $2 (Unqualified $ to_string $4) [] }-          | AndStadef and IdentifierOr eq identifierSpace { AndD $1 (Stadef $3 (Unqualified $ to_string $5) []) }-          | AndStadef and IdentifierOr eq identifier { AndD $1 (Stadef $3 (Unqualified $ to_string $5) []) }+-- Feb. 15th 2pm+AndStadef : stadef IdentifierOr SortArgs eq Type { Stadef $2 $3 $5 }+          | AndStadef and IdentifierOr SortArgs eq Type { AndD $1 (Stadef $3 $4 $6) }  StafunDecl : prfun PreFunction { Func $1 (PrFun $2) }            | prfn PreFunction { Func $1 (PrFn $2) }@@ -657,6 +668,7 @@         | SortArg comma Sort { Anonymous $3 : $1 }         | IdentifierOr { [ Anonymous (NamedSort $1) ] }         | Sort { [Anonymous $1] }+        | SortArg Comment { $1 }  SortArgs : openParen SortArg closeParen { Just $2 }          | doubleParens { Just [] }@@ -667,7 +679,10 @@          | 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) }@@ -683,6 +698,8 @@          | typedef IdentifierOr SortArgs eq vbar {% Left $ Expected $5 "Type" "|" }          | datavtype IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }          | datatype IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }+         | 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 }@@ -719,6 +736,11 @@ DataSortLeaves : DataSortLeaf { [$1] }                | DataSortLeaves DataSortLeaf { $2 : $1 } +CommentContents : commentContents { Comment $1 }+                | CommentContents commentContents { over comment (<> $2) $1 }++Comment : beginComment CommentContents endComment { over comment ((<> "*)") . ("(*" <>)) $2 }+ -- | Parse a declaration Declaration : include string { Include $2 }             | define { Define $1 }@@ -730,6 +752,7 @@             | macdef IdentifierOr doubleParens eq Expression { MacDecl $1 $2 [] $5 }             | macdef IdentifierOr openParen IdentifiersIn closeParen eq Expression { MacDecl $1 $2 $4 $7 }             | lineComment { Comment (to_string $1) }+            | Comment { $1 }             | staload underscore eq string { Staload (get_staload $1) (Just "_") $4 }             | staload string { Staload (get_staload $1) Nothing $2 }             | staload IdentifierOr eq string { Staload (get_staload $1) (Just $2) $4 }@@ -760,6 +783,8 @@             | symintr Name { 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) }+            | exception identifierSpace of openParen Type closeParen { Exception (to_string $2) (Tuple $4 [$5]) }             | Fixity Operators { FixityDecl $1 $2 }             | val Universals IdentifierOr colon Type { StaVal $2 $3 $5 }             | lambda {% Left $ Expected $1 "Declaration" "lam" }@@ -770,11 +795,13 @@             | prfTransform {% Left $ Expected $1 "Declaration" ">>" }             | maybeProof {% Left $ Expected $1 "Declaration" "?" }             | identifier {% Left $ Expected (token_posn $1) "Declaration" (to_string $1) }+            | identifierSpace {% Left $ Expected (token_posn $1) "Declaration" (to_string $1) }  {  data ATSError a = Expected AlexPosn a a-                | Unknown Token -- FIXME error type for expression when a static expression was expected (?)+                | Unknown Token+                | LexError String                 deriving (Eq, Show, Generic, NFData)  instance Pretty AlexPosn where@@ -784,6 +811,7 @@     pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (text s2) <> ", expected:" <+> squotes (text s1)) <> linebreak     pretty (Unknown (Special l ")")) = red "Error:" <+> "unmatched ')' at" <+> pretty l <> linebreak      pretty (Unknown t) = red "Error:" <+> "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak+    pretty (LexError s) = red "Lexical error:" <+> text s  parseError :: [Token] -> Either (ATSError String) a parseError = Left . Unknown . head 

@@ -284,7 +284,8 @@     pretty = cata a where         a (NamedF n)              = pretty n         a (ViewTypeF _ t)         = "view@" <> parens t-        a (ExF e t)               = pretty e <+> t+        a (ExF e (Just t))        = pretty e <+> t+        a (ExF e Nothing)         = pretty e         a (DependentF n ts)       = pretty n <> parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))         a (ForAF u t)             = pretty u <+> t         a (UnconsumedF t)         = "!" <> t@@ -356,6 +357,7 @@ glue x y     | isVal x && isVal y = True glue Staload{} Staload{}           = True+glue Define{} Define{} = True glue Include{} Include{}           = True glue ViewTypeDef{} ViewTypeDef{}   = True glue TypeDef{} TypeDef{}           = True@@ -502,6 +504,7 @@     pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgsNil as <+> ":" <> text si <#> pretty rt     pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt     pretty (PreF i si [] us as rt Nothing Nothing) = pretty i </> fancyU us </> prettyArgsNil as <+> ":" <> text si <#> pretty rt+    pretty (PreF i si pus [] as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> prettyArgsNil as <+> ":" <> text si <#> pretty rt     pretty (PreF i si pus us as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> fancyU us </> prettyArgsNil as <+> ":" <> text si <#> pretty rt  instance Pretty DataPropLeaf where@@ -527,10 +530,12 @@ prettySortArgs (Just as) = prettyArgs' ", " "(" ")" as  instance Pretty Declaration 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@@ -576,10 +581,8 @@     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 n [])                 = "stadef" <+> text i <+> pretty n-    pretty (Stadef i n as)                 = "stadef" <+> text i <+> pretty n <> prettyArgs as-    pretty (AndD d (Stadef i n []))        = pretty d <+> "and" <+> text i <+> pretty n-    pretty (AndD d (Stadef i n as))        = pretty d <+> "and" <+> text i <+> pretty n <> prettyArgs as+    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 as t)               = "abst@ype" <+> text i <> prettySortArgs as <> "=" <+> pretty t

@@ -53,6 +53,7 @@     , constructorUniversals     , typeCall     , typeCallArgs+    , comment     ) where  import           Control.Composition@@ -79,7 +80,7 @@     deriving (Show, Eq, Generic)     deriving newtype (NFData, Semigroup, Monoid) -data Leaf = Leaf { _constructorUniversals :: [Universal], name :: String, constructorArgs :: [String], maybeType :: Maybe Type }+data Leaf = Leaf { _constructorUniversals :: [Universal], name :: String, constructorArgs :: [StaticExpression], maybeType :: Maybe Type }     deriving (Show, Eq, Generic, NFData)  type SortArgs = Maybe [SortArg]@@ -95,7 +96,7 @@                  | AndDecl (Maybe Type) Pattern Expression                  | Include String                  | Staload Bool (Maybe String) String-                 | Stadef String Name [Type]+                 | Stadef String SortArgs Type -- [Type] -- FIXME stadef array(a:vt@ype, n:int) = @[a][n]                  | CBlock String                  | TypeDef AlexPosn String SortArgs Type                  | ViewTypeDef AlexPosn String SortArgs Type@@ -109,8 +110,9 @@                  | ViewDef AlexPosn String SortArgs Type                  | OverloadOp AlexPosn BinOp Name (Maybe Int)                  | OverloadIdent AlexPosn String Name (Maybe Int)-                 | Comment String+                 | Comment { _comment :: String }                  | DataProp AlexPosn String SortArgs [DataPropLeaf]+                 | DataView AlexPosn String SortArgs [Leaf]                  | Extern AlexPosn Declaration                  | Define String                  | SortDef AlexPosn String (Either Sort Universal)@@ -125,6 +127,7 @@                  | FixityDecl Fixity [String]                  | MacDecl AlexPosn String [String] Expression                  | DataSort AlexPosn String [DataSortLeaf]+                 | Exception String Type                  deriving (Show, Eq, Generic, NFData)  data DataSortLeaf = DataSortLeaf [Universal] Sort (Maybe Sort)@@ -136,13 +139,13 @@ -- | A type for parsed ATS types data Type = Tuple AlexPosn [Type]           | Named Name-          | Ex Existential Type+          | Ex Existential (Maybe Type)           | ForA Universal Type           | Dependent { _typeCall :: Name, _typeCallArgs :: [Type] }-          | Unconsumed Type -- !a-          | AsProof Type (Maybe Type) -- a >> b-          | FromVT Type -- For a viewtype VT, we can prove there exist a view V and type T such that `VT` is equivalent to `(V | T)` - that T is `VT?!`-          | MaybeVal Type -- This is just `a?` or the like+          | Unconsumed Type -- @!a@+          | AsProof Type (Maybe Type) -- @a >> b@+          | FromVT Type -- | @a?!@+          | MaybeVal Type -- | @a?@           | AtExpr AlexPosn Type StaticExpression           | AtType AlexPosn Type           | ProofType AlexPosn [Type] Type -- Aka (prf | val)@@ -202,7 +205,7 @@     deriving (Show, Eq, Generic, NFData)  -- | A datatype for sorts.-data Sort = NamedSort String+data Sort = NamedSort { _sortName :: String }           | T0p Addendum -- ^ t@ype           | Vt0p Addendum -- ^ vt@ype           | Addr

@@ -36,10 +36,10 @@ (ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) : #[id2:int] a  extern-fun {a:vt0p} queue_make  (cap : intGt(0)) : queue(a)+fun {a:vt0p} queue_make (cap : intGt(0)) : queue(a)  extern-fun {a:t@ype} queue_free  (que : queue(a)) : void+fun {a:t@ype} queue_free (que : queue(a)) : void  assume queue_vtype(a : vt0p, id : int) = deqarray(a) assume ISNIL(id : int, b : bool) = unit_p@@ -50,18 +50,18 @@ vtypedef channel(a: vt0p) = channel_vtype(a)  extern-fun {a:vt0p} channel_insert  (!channel(a), a) : void+fun {a:vt0p} channel_insert (!channel(a), a) : void  extern-fun {a:vt0p} channel_remove  (chan : !channel(a)) : a+fun {a:vt0p} channel_remove (chan : !channel(a)) : a  extern-fun {a:vt0p} channel_remove_helper  ( chan : !channel(a)-                                    , !queue(a) >> _-                                    ) : a+fun {a:vt0p} channel_remove_helper ( chan : !channel(a)+                                   , !queue(a) >> _+                                   ) : a  extern-fun {a:vt0p} channel_insert_helper  (!channel(a), !queue(a) >> _, a) :+fun {a:vt0p} channel_insert_helper (!channel(a), !queue(a) >> _, a) :   void  datavtype channel_ =@@ -75,13 +75,13 @@                                          }  extern-fun {a:vt0p} channel_make  (cap : intGt(0)) : channel(a)+fun {a:vt0p} channel_make (cap : intGt(0)) : channel(a)  extern-fun {a:vt0p} channel_ref  (ch : !channel(a)) : channel(a)+fun {a:vt0p} channel_ref (ch : !channel(a)) : channel(a)  extern-fun {a:vt0p} channel_unref  (ch : channel(a)) : Option_vt(queue(a))+fun {a:vt0p} channel_unref (ch : channel(a)) : Option_vt(queue(a))  extern fun channel_refcount {a:vt0p} (ch : !channel(a)) : intGt(0)

@@ -0,0 +1,37 @@+#include "share/atspre_staload_libats_ML.hats"+#include "libats/ML/SATS/SHARE/monad.hats"++datatype either(a: t@ype, b: t@ype+) =+  | left of a+  | right of b++fun {a:t@ype}{b:t@ype+} eq_either_either ( x : either(a, INV(b))+                                         , y : either(a, b)+                                         ) : bool++fun {a:t@ype}{b:t@ype+} neq_either_either ( x : either(a, INV(b))+                                          , y : either(a, b)+                                          ) : bool++overload = with eq_either_either++overload != with neq_either_either++fun lefts {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :+  [ m : int | m <= n ] list(a, m)++fun rights {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :+  [ m : int | m <= n ] list(b, m)++fun either_ {a:t@ype}{b:t@ype+}{c:t@ype} ( f : a -> c+                                         , g : b -> c+                                         , x : either(a, b)+                                         ) : c++fun is_left {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool++fun is_right {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool++fun from_right {a:t@ype}{b:t@ype+} (x : b, y : either(a, b)) : b++fun from_left {a:t@ype}{b:t@ype+} (x : a, y : either(a, b)) : a

@@ -0,0 +1,30 @@+#include "share/atspre_staload_libats_ML.hats"+#include "libats/ML/SATS/SHARE/monad.hats"++datatype either(a: t@ype, b: t@ype+) =+  | left of a+  | right of b++fun {a:t@ype}{b:t@ype+} eq_either_either  (x : either(a, INV(b)), y : either(a, b)) : bool++fun {a:t@ype}{b:t@ype+} neq_either_either  (x : either(a, INV(b)), y : either(a, b)) : bool++overload = with eq_either_either++overload != with neq_either_either++fun lefts {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :+  [ m : int | m <= n ] list(a, m)++fun rights {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :+  [ m : int | m <= n ] list(b, m)++fun either_ {a:t@ype}{b:t@ype+}{c:t@ype} (f : a -> c, g : b -> c, x : either(a, b)) : c++fun is_left {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool++fun is_right {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool++fun from_right {a:t@ype}{b:t@ype+} (x : b, y : either(a, b)) : b++fun from_left {a:t@ype}{b:t@ype+} (x : a, y : either(a, b)) : a