language-ats 1.0.2.1 → 1.1.0.0

raw patch · 10 files changed

+165/−123 lines, 10 filesdep +microlensdep +microlens-thdep −lensPVP ok

version bump matches the API change (PVP)

Dependencies added: microlens, microlens-th

Dependencies removed: lens

API changes (from Hackage documentation)

Files

• language-ats.cabal +92/−76
• src/Language/ATS.hs +2/−2
• src/Language/ATS/Lexer.x +10/−2
• src/Language/ATS/Parser.y +30/−15
• src/Language/ATS/PrettyPrint.hs +12/−7
• src/Language/ATS/Types.hs +9/−8
• test/data/concurrency.out +2/−3
• test/data/fastcount.out +4/−4
• test/data/numerics.out +2/−3
• test/data/polyglot.out +2/−3

@@ -1,83 +1,99 @@-name:                language-ats-version:             1.0.2.1-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-license-file:        LICENSE-author:              Vanessa McHale-maintainer:          vamchale@gmail.com-copyright:           Copyright: (c) 2018 Vanessa McHale-category:            Language, Lexer, Parser, Pretty Printer, ATS-build-type:          Simple-extra-doc-files:     README.md-data-files:          test/data/*.dats-                   , test/data/*.sats-                   , test/data/*.out-cabal-version:       1.18+cabal-version: 1.18+name: language-ats+version: 1.1.0.0+license: BSD3+license-file: LICENSE+copyright: Copyright: (c) 2018 Vanessa McHale+maintainer: vamchale@gmail.com+author: Vanessa McHale+synopsis: Parser and pretty-printer for ATS.+description:+    Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex.+category: Language, Lexer, Parser, Pretty Printer, ATS+build-type: Simple+data-files:+    test/data/*.dats+    test/data/*.sats+    test/data/*.out+extra-doc-files: README.md -Flag development {-  Description: Enable `-Werror`-  manual: True-  default: False-}+source-repository head+    type: darcs+    location: https://hub.darcs.net/vmchale/ats +flag development+    description:+        Enable `-Werror`+    default: False+    manual: True+ library-  hs-source-dirs:      src-  exposed-modules:     Language.ATS-  other-modules:       Language.ATS.Lexer-                     , Language.ATS.Parser-                     , Language.ATS.Types-                     , Language.ATS.PrettyPrint-  build-depends:       base >= 4.10 && < 5-                     , array-                     , lens-                     , deepseq-                     , ansi-wl-pprint >= 0.6.8-                     , recursion-schemes >= 5.0.1-                     , composition-prelude-                     , ansi-terminal-                     , containers-                     , mtl-                     , transformers-  default-language:    Haskell2010-  build-tools:         happy-                     , alex-  if flag(development)-    ghc-options:       -Werror-  if impl(ghc >= 8.0)-    ghc-options:       -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat-  ghc-options:         -Wall+    exposed-modules:+        Language.ATS+    build-tools: happy -any, alex -any+    hs-source-dirs: src+    other-modules:+        Language.ATS.Lexer+        Language.ATS.Parser+        Language.ATS.PrettyPrint+        Language.ATS.Types+    default-language: Haskell2010+    ghc-options: -Wall+    build-depends:+        base >=4.10 && <5,+        array -any,+        microlens -any,+        microlens-th -any,+        deepseq -any,+        ansi-wl-pprint >=0.6.8,+        recursion-schemes >=5.0.1,+        composition-prelude -any,+        ansi-terminal -any,+        containers -any,+        mtl -any,+        transformers -any+    +    if flag(development)+        ghc-options: -Werror+    +    if impl(ghc >=8.0)+        ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates+                     -Wcompat  test-suite language-ats-test-  type:                exitcode-stdio-1.0-  hs-source-dirs:      test-  main-is:             Spec.hs-  build-depends:       base-                     , language-ats-                     , hspec-                     , hspec-dirstream-                     , system-filepath-  if flag(development)-    ghc-options:       -Werror-  if impl(ghc >= 8.0)-    ghc-options:       -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat-  ghc-options:         -threaded -rtsopts -with-rtsopts=-N -Wall-  default-language:    Haskell2010+    type: exitcode-stdio-1.0+    main-is: Spec.hs+    hs-source-dirs: test+    default-language: Haskell2010+    ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall+    build-depends:+        base -any,+        language-ats -any,+        hspec -any,+        hspec-dirstream -any,+        system-filepath -any+    +    if flag(development)+        ghc-options: -Werror+    +    if impl(ghc >=8.0)+        ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates+                     -Wcompat  benchmark language-ats-bench-  type:                exitcode-stdio-1.0-  hs-source-dirs:      bench-  main-is:             Bench.hs-  build-depends:       base-                     , language-ats-                     , criterion-  if flag(development)-    ghc-options:       -Werror-  if impl(ghc >= 8.0)-    ghc-options:       -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat-  ghc-options:         -Wall-  default-language:    Haskell2010--source-repository head-  type:     darcs-  location: https://hub.darcs.net/vmchale/ats+    type: exitcode-stdio-1.0+    main-is: Bench.hs+    hs-source-dirs: bench+    default-language: Haskell2010+    ghc-options: -Wall+    build-depends:+        base -any,+        language-ats -any,+        criterion -any+    +    if flag(development)+        ghc-options: -Werror+    +    if impl(ghc >=8.0)+        ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates+                     -Wcompat

@@ -57,7 +57,6 @@                     , typeCallArgs                     ) where -import           Control.Lens import           Control.Monad import           Control.Monad.IO.Class import           Control.Monad.Trans.State@@ -66,6 +65,7 @@ import           Language.ATS.Parser import           Language.ATS.PrettyPrint import           Language.ATS.Types+import           Lens.Micro import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))  rewriteATS' :: Eq a => (ATS a, FixityState a) -> ATS a@@ -89,7 +89,7 @@ -- | Extract a list of files that some code depends on. getDependencies :: ATS a -> [FilePath] getDependencies (ATS ds) = g =<< ds-    where g (Staload _ _ s)  = [s]+    where g (Load _ _ _ s)   = [s]           g (Include s)      = [s]           g (Local _ as as') = foldMap getDependencies [as, as']           g _                = mempty

@@ -82,11 +82,15 @@ @func_type = "->" | "-<" @inner_signature_mult ">"  @at_brace = \@ ($white | @block_comment)* \{+@at_tuple = \@ ($white | @block_comment)* \( +@box_tuple = \' ($white | @block_comment)* \(+@box_record = \' ($white | @block_comment)* \{+ $in_operator = $special # [\)\(\}\{\_\[\]\,] $in_l = $in_operator # [\<] $in_r = $in_operator # [\>]-@operator = "+" | "-" | "*" | "/" | "<" | ">" | "=" | "~" | "?" | "%" | "#[" | $in_r{2,} | $in_l{2,} | $in_r{2,} $in_l++@operator = "+" | "-" | "*" | "/" | "<" | ">" | "=" | "~" | "!" | "?" | "%" | "#[" | $in_r{2,} | $in_l{2,} | $in_r{2,} $in_l+  @double_parens = "(" (@block_comment | $white+ | \n | "//".*)+ ")" | "()" @double_braces = "{" @block_comment "}" | "{}"@@ -234,7 +238,10 @@     <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> @at_brace                { tok (\p s -> alex $ Special p "@{") }+    <0> @at_tuple                { tok (\p s -> alex $ Special p "@(") }+    <0> @box_tuple               { tok (\p s -> alex $ Special p "'(") }+    <0> @box_record              { tok (\p s -> alex $ Special p "'{") }     <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) }@@ -531,6 +538,7 @@ toChar "'\\n'" = '\n' toChar "'\\t'" = '\t' toChar "'\\\\'" = '\\'+toChar "'\\0'" = '\0' toChar x = x !! 1  alexEOF :: Alex Token

@@ -26,7 +26,7 @@ import Control.Composition import Data.Char (toLower) import Control.DeepSeq (NFData)-import Control.Lens (over, _head)+import Lens.Micro (over, _head) import GHC.Generics (Generic) import Prelude import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))@@ -105,6 +105,7 @@     exception { Keyword $$ KwException }     include { Keyword $$ KwInclude }     staload { $$@(Keyword _ (KwStaload _)) }+    dynload { $$@(Keyword _ (KwDynload _)) }     overload { Keyword $$ KwOverload }     with { Keyword $$ KwWith }     dataprop { Keyword $$ KwDataprop }@@ -177,10 +178,11 @@     plus { Operator $$ "+" }     div { Operator $$ "/" }     mult { Operator $$ "*" }-    exclamation { Special $$ "!" }+    exclamation { Operator $$ "!" }     dot { Special $$ "." }     at { Special $$ "@" }     tilde { Operator $$ "~" }+    backslash { Special $$ "\\" }     dollar { Special $$ "$" }     semicolon { Special $$ ";" }     andOp { Operator $$ "&&" }@@ -198,7 +200,7 @@     define { MacroBlock _ $$ }     lineComment { $$@CommentLex{} }     lspecial { SpecialBracket $$ }-    atbrace { Operator $$ "@{" }+    atbrace { Special $$ "@{" }     macdef { Keyword $$ KwMacdef }     mod { Keyword $$ KwMod }     fixAt { Keyword $$ KwFixAt }@@ -265,7 +267,6 @@      | openParen Type closeParen { ParenType $1 $2 }      | doubleParens { NoneType $1 }      | 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) }@@ -282,6 +283,7 @@ TypeArg : IdentifierOr { Arg (First $1) }         | IdentifierOr colon Type { Arg (Both $1 $3) }         | Type { Arg (Second $1) }+        | exclamation IdentifierOr colon {% left $ OneOf $3 [",", ")"] ":" }  Arg : TypeArg { $1 }     | StaticExpression { Arg (Second (ConcreteType $1)) }@@ -343,9 +345,10 @@           | minus {% left $ Expected $1 "Arrow" "-" }           | eq {% left $ Expected $1 "Arrow" "=" }           | minus {% left $ Expected $1 "Arrow" "-" }+          | CaseArrow vbar {% left $ Expected $2 "Expression" "|" }  LambdaArrow : plainArrow { Plain $1 }-            | cloref1Arrow { Full $1 "cloref1" } -- TODO do this more efficiently.+            | cloref1Arrow { Full $1 "cloref1" } -- FIXME this is a bad heuristic             | cloptr1Arrow { Full $1 "cloptr1" }             | lincloptr1Arrow { Full $1 "lincloptr1" }             | minus {% left $ Expected $1 "Arrow" "-" }@@ -465,7 +468,6 @@           | underscore {% left $ Expected $1 "_" "Termination metric" }           | dollar {% left $ Expected $1 "$" "Termination metric" } - Sort : t0pPlain { T0p None }      | t0pCo { T0p Plus }      | vt0pPlain { Vt0p None }@@ -601,6 +603,7 @@       | at { At }       | mutateArrow { SpearOp }       | customOperator { SpecialInfix (token_posn $1) (to_string $1) }+      | backslash identifierSpace { SpecialInfix $1 ('\\' : to_string $2) }  -- | Optionally parse a function body OptExpression : { Nothing }@@ -663,6 +666,7 @@           | 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) }+          | stadef Operator Comment SortArgs eq StaticExpression { Stadef $2 $4 (Left $6) }           | 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)) }@@ -690,7 +694,7 @@         | fun fn {% left $ Expected $2 "Function name" "fn" }         | fn fun {% left $ Expected $2 "Function name" "fun" }         | extern FunDecl identifier openParen {% left $ Expected (token_posn $3) "Static integer expression" (to_string $3) }-        | extern identifier {% left $ Expected (token_posn $2) "Declaration" (to_string $2) }+        | extern identifier {% left $ OneOf (token_posn $2) ["fun", "fn", "prfun", "prfun", "praxi", "castfn", "fnx", "val"] (to_string $2) }  IdentifierOr : identifier { to_string $1 }              | identifierSpace { to_string $1 }@@ -778,6 +782,7 @@          | doubleEq { "==" }          | doubleBrackets { "<>" }          | neq { "!=" }+         | backslash identifierSpace { '\\' : to_string $2 }  Operators : Operator { [$1] }           | Operators Operator { $2 : $1 }@@ -818,6 +823,9 @@       | Names identifierSpace { Unqualified (to_string $2) : $1 }       | Names customOperator { Unqualified (to_string $2) : $1 } +Load : staload { (True, $1) }+     | dynload { (False, $1) }+ -- | Parse a declaration Declaration : include string { Include $2 }             | define { Define $1 }@@ -831,12 +839,12 @@             | 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 }-            | staload dollar IdentifierOr { Staload (get_staload $1) Nothing ('$' : $3) }-            | staload dollar IdentifierOr eq string { Staload (get_staload $1) (Just ('$' : $3)) $5 }-            | staload IdentifierOr eq dollar IdentifierOr { Staload (get_staload $1) (Just $2) ('$' : $5) }+            | Load underscore eq string { Load (fst $1) (get_staload $ snd $1) (Just "_") $4 }+            | Load string { Load (fst $1) (get_staload $ snd $1) Nothing $2 }+            | Load IdentifierOr eq string { Load (fst $1) (get_staload $ snd $1) (Just $2) $4 }+            | Load dollar IdentifierOr { Load (fst $1) (get_staload $ snd $1) Nothing ('$' : $3) }+            | Load dollar IdentifierOr eq string { Load (fst $1) (get_staload $ snd $1) (Just ('$' : $3)) $5 }+            | Load IdentifierOr eq dollar IdentifierOr { Load (fst $1) (get_staload $ snd $1) (Just $2) ('$' : $5) }             | var Pattern colon Type with PreExpression { Var (Just $4) $2 Nothing (Just $6) } -- FIXME signature is too general.             | var Pattern colon Type eq PreExpression { Var (Just $4) $2 (Just $6) Nothing }             | var Pattern eq Expression { Var Nothing $2 (Just $4) Nothing }@@ -869,7 +877,6 @@             | val Universals IdentifierOr colon Type { StaVal $2 $3 $5 }             | lambda {% left $ Expected $1 "Declaration" "lam" }             | llambda {% left $ Expected $1 "Declaration" "llam" }-            | minus {% left $ Expected $1 "Declaration" "-" }             | dollar {% left $ Expected $1 "Declaration" "$" }             | fromVT {% left $ Expected $1 "Declaration" "?!" }             | prfTransform {% left $ Expected $1 "Declaration" ">>" }@@ -888,6 +895,7 @@     where inserts = flip M.insert x <$> keys  data ATSError = Expected AlexPosn String String+              | OneOf AlexPosn [String] String               | Unknown Token               | LexError String               deriving (Eq, Show, Generic, NFData)@@ -898,8 +906,15 @@ unmatched :: AlexPosn -> String -> Doc unmatched l chr = red "Error:" <+> "unmatched" <+> squotes (text chr) <+> "at" <+> pretty l <> linebreak  +bear :: Bool -> [Doc] -> Doc+bear _ [] = mempty+bear False [x, y] = x <+> "or" <+> y+bear True [x, y] = x <> ", or" <+> y+bear _ (x:xs) = x <> "," <+> bear True xs+ instance Pretty ATSError where-    pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (text s2) <> ", expected:" <+> squotes (text s1)) <> linebreak+    pretty (OneOf p ss s) = red "Error:" <+> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (text s) <> ", expected one of" <+> bear False (fmap (squotes . text) ss)) <> linebreak+    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 ")")) = unmatched l ")"      pretty (Unknown (Special l "}")) = unmatched l "}"     pretty (Unknown (Special l ">")) = unmatched l ">"

@@ -16,10 +16,10 @@  import           Control.Composition                   hiding ((&)) import           Control.DeepSeq                       (NFData)-import           Control.Lens                          hiding (op, pre) import           Data.Functor.Foldable                 (cata) import           GHC.Generics                          (Generic) import           Language.ATS.Types+import           Lens.Micro import           Prelude                               hiding ((<$>)) import           System.Console.ANSI.Types import           Text.PrettyPrint.ANSI.Leijen          hiding (bool)@@ -178,6 +178,7 @@         a (CharLitF '\\')              = "'\\\\'"         a (CharLitF '\n')              = "'\\n'"         a (CharLitF '\t')              = "'\\t'"+        a (CharLitF '\0')              = "'\\0'"         a (CharLitF c)                 = "'" <> char c <> "'"         a (ProofExprF _ e e')          = "(" <> e <+> "|" <+> e' <> ")"         a (TypeSignatureF e t)         = e <+> ":" <+> pretty t@@ -279,7 +280,9 @@     pretty = cata a where         a (NamedF n)                       = pretty n         a (ViewTypeF _ t)                  = "view@" <> parens t-        a (ExF e (Just t))                 = pretty e <+> t+        a (ExF e (Just t))+            | head (show t) == '['         = pretty e <> t -- FIXME this is a hack+            | otherwise                    = pretty e <+> t         a (ExF e Nothing)                  = pretty e         a (DependentF n@SpecialName{} [t]) = pretty n <+> pretty t         a (DependentF n ts)                = pretty n <> parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))@@ -354,7 +357,7 @@ glue x y     | isVal x && isVal y = True glue Stadef{} Stadef{}             = True-glue Staload{} Staload{}           = True+glue Load{} Load{}                 = True glue Define{} Define{}             = True glue Include{} Include{}           = True glue ViewTypeDef{} ViewTypeDef{}   = True@@ -486,8 +489,10 @@ (<#>) :: Doc -> Doc -> Doc (<#>) a b = lineAlt (a <$> indent 2 b) (a <+> b) + prettySigG :: (Pretty a) => Doc -> Doc -> Maybe String -> Maybe a -> Doc-prettySigG d d' (Just si) (Just rt) = d <> ":" <> text si <#> pretty rt <> d'+prettySigG d d' (Just si) (Just rt) = d `op` ":" <> text si <#> pretty rt <> d'+    where op a b = lineAlt (a <$> indent 2 b) (a <> b) prettySigG _ _ _ _                  = mempty  prettySigNull :: (Pretty a) => Maybe String -> Maybe a -> Doc@@ -552,7 +557,7 @@     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 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@@ -560,8 +565,8 @@     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 (Load sta b Nothing s)           = bool "" "#" b <> bool "dyn" "sta" sta <> "load" <+> pretty s+    pretty (Load sta b (Just q) s)          = bool "" "#" b <> bool "dyn" "sta" sta <> "load" <+> 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'

@@ -65,7 +65,6 @@  import           Control.Composition import           Control.DeepSeq          (NFData)-import           Control.Lens import           Data.Function            (on) import           Data.Functor.Foldable    (ListF (Cons), ana, cata, embed, project) import           Data.Functor.Foldable.TH (makeBaseFunctor)@@ -74,6 +73,8 @@ import           Data.Semigroup           (Semigroup) import           GHC.Generics             (Generic) import           Language.ATS.Lexer       (Addendum (..))+import           Lens.Micro+import           Lens.Micro.TH  type Fix = Either Int String @@ -104,7 +105,7 @@                    | 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+                   | Load { static :: Bool, withOctothorpe :: Bool, qualName :: Maybe String, fileName :: String }                    | Stadef String (SortArgs a) (Either (StaticExpression a) (Type a))                    | CBlock String                    | TypeDef a String (SortArgs a) (Type a)@@ -215,11 +216,11 @@  -- | A datatype for sorts. data Sort a = NamedSort { _sortName :: String }-            | T0p Addendum -- ^ t@ype-            | Vt0p Addendum -- ^ vt@ype+            | T0p Addendum -- ^ @t\@ype@+            | Vt0p Addendum -- ^ @vt\@ype@             | Addr-            | VType a Addendum -- ^ viewtype or vtype-            | View a Addendum -- ^ view+            | VType a Addendum -- ^ @viewtype@ or @vtype@+            | View a Addendum -- ^ @view@             deriving (Show, Eq, Generic, NFData)  -- FIXME a type for sorts?@@ -273,8 +274,8 @@ data Expression a = Let a (ATS a) (Maybe (Expression a))                   | VoidLiteral a -- ^ The '()' literal representing inaction.                   | Call { callName       :: Name a-                         , callImplicits  :: [[Type a]] -- ^ E.g. some_function<a>-                         , callUniversals :: [Type a] -- ^ E.g. some_function{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.                          }

@@ -55,9 +55,8 @@ 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) :

@@ -17,10 +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"  (* ****** ****** *)

@@ -41,9 +41,8 @@     | k =>        begin         let-          fun loop {n:nat}{m:nat} .<max(0,m-n)>. ( i : int(n)-                                                 , bound : int(m)-                                                 ) :<> bool =+          fun loop {n:nat}{m:nat} .<max(0,m-n)>. (i : int(n), bound : int(m)) +            :<> bool =             if i < bound then               if k % i = 0 then                 false

@@ -113,9 +113,8 @@     ""  // helper function for make_table-fun maybe_table { k : int | k >= 0 && k < 20 }( s : string(k)-                                              , f : file-                                              ) : string =+fun maybe_table { k : int | k >= 0 && k < 20 }(s : string(k), f : file) +  : string =   let     var code = f.lines - f.comments - f.blanks   in