language-ats 1.2.0.9 → 1.2.0.10
raw patch · 7 files changed
+50/−31 lines, 7 filesdep +micro-recursion-schemesdep +microlensdep +microlens-thdep −lensdep −recursion-schemesdep ~base
Dependencies added: micro-recursion-schemes, microlens, microlens-th
Dependencies removed: lens, recursion-schemes
Dependency ranges changed: base
Files
- language-ats.cabal +11/−4
- src/Language/ATS.hs +1/−1
- src/Language/ATS/Lexer.x +5/−0
- src/Language/ATS/Parser.y +3/−1
- src/Language/ATS/PrettyPrint.hs +13/−10
- src/Language/ATS/Types.hs +16/−14
- test/data/fastcount.out +1/−1
language-ats.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.18 name: language-ats-version: 1.2.0.9+version: 1.2.0.10 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018 Vanessa McHale@@ -39,12 +39,19 @@ Language.ATS.PrettyPrint Language.ATS.Types default-language: Haskell2010+ other-extensions: OverloadedStrings DeriveGeneric DeriveAnyClass+ FlexibleContexts FlexibleInstances PatternSynonyms+ StandaloneDeriving LambdaCase GeneralizedNewtypeDeriving+ DeriveTraversable DerivingStrategies DuplicateRecordFields+ DeriveFoldable DeriveDataTypeable DeriveFunctor TypeFamilies+ TemplateHaskell CPP MagicHash ghc-options: -Wall build-depends:- base >=4.10 && <5,+ base >=4.9 && <5, array -any,- recursion-schemes >=5.0.1,- lens -any,+ micro-recursion-schemes >=5.0.1,+ microlens -any,+ microlens-th -any, deepseq -any, ansi-wl-pprint >=0.6.8, composition-prelude -any,
src/Language/ATS.hs view
@@ -60,7 +60,6 @@ , typeCallArgs ) where -import Control.Lens import Control.Monad import Control.Monad.IO.Class import Control.Monad.Trans.State@@ -69,6 +68,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
src/Language/ATS/Lexer.x view
@@ -32,6 +32,7 @@ -- Digits $digit = 0-9 $octal = 0-7+$hex = [0-9 a-f A-F] -- Characters $special = [\+\-\*\&\|\[\]\{\}\(\)\_\=\!\%\^\$\@\;\~\,\.\\\#\<\>\:\?]@@ -267,6 +268,7 @@ -- literals <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> "0x" $hex+ { tok (\p s -> alex $ HexIntTok p (drop 2 s)) } <0> @float { tok (\p s -> alex $ FloatTok p (read s)) } <0> @char_lit { tok (\p s -> alex $ CharTok p (toChar s)) } <0> @string { tok (\p s -> alex $ StringTok p s) }@@ -410,6 +412,7 @@ | SpecialIdentifier AlexPosn String | Keyword AlexPosn Keyword | IntTok AlexPosn Int+ | HexIntTok AlexPosn String | FloatTok AlexPosn Float | CharTok AlexPosn Char | StringTok AlexPosn String@@ -532,6 +535,7 @@ pretty (IdentifierSpace _ s) = text s pretty (Keyword _ kw) = pretty kw pretty (IntTok _ i) = pretty i+ pretty (HexIntTok _ hi) = "0x" <> text hi pretty (FloatTok _ x) = pretty x pretty (CharTok _ c) = squotes (pretty c) pretty (StringTok _ s) = text s@@ -587,6 +591,7 @@ token_posn (CommentContents p _) = p token_posn (CommentBegin p) = p token_posn (CommentEnd p) = p+token_posn (HexIntTok p _) = p token_posn End = undefined toChar :: String -> Char
src/Language/ATS/Parser.y view
@@ -23,7 +23,7 @@ import Control.Composition import Control.DeepSeq (NFData)-import Control.Lens (over, _head)+import Lens.Micro (over, _head) import qualified Data.Map as M import Control.Monad.Trans.Class import Control.Monad.Trans.State@@ -139,6 +139,7 @@ datasort { Keyword $$ KwDatasort } uintLit { UintTok _ $$ } intLit { IntTok _ $$ }+ hexLit { HexIntTok _ $$ } floatLit { FloatTok _ $$ } specialIdentifier { $$@SpecialIdentifier{} } foldAt { Identifier $$ "fold@" }@@ -314,6 +315,7 @@ -- | Parse a literal Literal : uintLit { UintLit $1 } | intLit { IntLit $1 }+ | hexLit { HexLit $1 } | floatLit { FloatLit $1 } | string { StringLit $1 } | charLit { CharLit $1 }
src/Language/ATS/PrettyPrint.hs view
@@ -1,13 +1,12 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} -{-# LANGUAGE DeriveAnyClass #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE StandaloneDeriving #-} module Language.ATS.PrettyPrint ( printATS , printATSCustom@@ -15,9 +14,9 @@ ) where import Control.Composition hiding ((&))-import Control.Lens hiding (op, pre) import Data.Functor.Foldable (cata) import Language.ATS.Types+import Lens.Micro import Prelude hiding ((<$>)) import Text.PrettyPrint.ANSI.Leijen hiding (bool) @@ -125,6 +124,7 @@ ("let" <+> pretty e <$> endLet e') a (UintLitF u) = pretty u <> "u" a (IntLitF i) = pretty i+ a (HexLitF hi) = "0x" <> text hi a (LambdaF _ lt p e) = let pre = "lam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e) a (LinearLambdaF _ lt p e) = let pre = "llam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e) a (FloatLitF f) = pretty f@@ -168,6 +168,7 @@ a (TupleExF _ es) = parens (mconcat $ punctuate ", " (reverse es)) a (BoxTupleExF _ es) = "'(" <> mconcat (punctuate ", " (reverse es)) <> ")" a (WhileF _ e e') = "while" <> parens e <> e'+ a (ActionsF (ATS [d])) = "{" <+> pretty d <+> "}" a (ActionsF as) = "{" <$> indent 2 (pretty as) <$> "}" a UnderscoreLitF{} = "_" a (BeginF _ e)@@ -282,7 +283,9 @@ a (MaybeValF t) = t <> "?" a (AtExprF _ t t') = t <+> "@" <+> pretty t' a (AtTypeF _ t) = "@" <> t- a (ProofTypeF _ t t') = parens (prettyArgsG "" "" t <+> "|" <+> t')+ a (ProofTypeF _ t t') = parens (pre' `op` "|" <+> t')+ where pre' = prettyArgsG mempty mempty t+ op = bool (<+>) (<>) ('\n' `elem` showFast pre') a (ConcreteTypeF e) = pretty e a (TupleF _ ts) = parens (mconcat (punctuate ", " (fmap pretty (reverse ts)))) a (BoxTupleF _ ts) = "'(" <> mconcat (punctuate ", " (fmap pretty (reverse ts))) <> ")"
src/Language/ATS/Types.hs view
@@ -67,7 +67,6 @@ import Control.Composition import Control.DeepSeq (NFData)-import Control.Lens import Control.Monad import Data.Function (on) import Data.Functor.Foldable (ListF (Cons), ana, cata, embed, project)@@ -77,6 +76,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 @@ -87,7 +88,7 @@ | Infix { pos :: a, ifix :: Fix } deriving (Show, Eq, Generic, NFData) --- | Newtype wrapper containing a list of declarations+-- | An ATS file, containing a list of declarations newtype ATS a = ATS { unATS :: [Declaration a] } deriving (Show, Eq, Generic) deriving newtype (NFData, Semigroup, Monoid)@@ -97,7 +98,7 @@ type SortArgs a = Maybe [SortArg a] --- | Declare something in a scope (a function, value, action, etc.)+-- | Declarations for functions, values, actions, etc. data Declaration a = Func { pos :: a, _fun :: Function a } | Impl { implArgs :: [Arg a], _impl :: Implementation a } -- TODO do something better for implicit universals | ProofImpl { implArgs :: [Arg a], _impl :: Implementation a }@@ -177,9 +178,10 @@ -- | A type for @=>@, @=\<cloref1>@, etc. data LambdaType a = Plain a+ | Spear a -- | @=>>@+ | ProofArrow a -- | @=/=>@ | Full a String- | Spear a -- @=>>@- | ProofArrow a -- @=/=>@+ -- TODO figure out wtf ProofArrow does deriving (Show, Eq, Generic, NFData) data Name a = Unqualified String@@ -238,9 +240,9 @@ data Existential a = Existential { boundE :: [String], isOpen :: Bool, typeE :: Maybe (Sort a), propE :: Maybe (StaticExpression a) } deriving (Show, Eq, Generic, NFData) --- | @~@ is used to negate numbers in ATS-data UnOp a = Negate- | Deref+-- | Unary operators+data UnOp a = Negate -- | @~@+ | Deref -- | @!@ | SpecialOp a String deriving (Show, Eq, Generic, NFData) @@ -265,11 +267,9 @@ | SpecialInfix a String deriving (Show, Eq, Generic, NFData) - pattern Con :: a -> BinOp a pattern Con l = SpecialInfix l "::" - data StaticExpression a = StaticVal (Name a) | StaticBinary (BinOp a) (StaticExpression a) (StaticExpression a) | StaticInt Int@@ -297,9 +297,10 @@ , whenTrue :: Expression a -- ^ Expression to be returned when true , elseExpr :: Maybe (Expression a) -- ^ Expression to be returned when false }- | UintLit Word -- ^ @1000u@+ | UintLit Word -- ^ E.g. @1000u@ | FloatLit Float | IntLit Int+ | HexLit String | UnderscoreLit a | Lambda a (LambdaType a) (Pattern a) (Expression a) | LinearLambda a (LambdaType a) (Pattern a) (Expression a)@@ -312,12 +313,12 @@ | Binary (BinOp a) (Expression a) (Expression a) | Unary (UnOp a) (Expression a) | IfCase { posE :: a- , ifArms :: [(Expression a, LambdaType a, Expression a)]+ , ifArms :: [(Expression a, LambdaType a, Expression a)] -- TODO I'm not sure @ifcase@ needs 'LambdaType'? } | Case { posE :: a , kind :: Addendum , val :: Expression a- , _arms :: [(Pattern a, LambdaType a, Expression a)] -- ^ Each @((Pattern a), (Expression a))@ pair corresponds to a branch of the 'case' statement+ , _arms :: [(Pattern a, LambdaType a, Expression a)] -- ^ Each (('Pattern' a), ('Expression' a)) pair corresponds to a branch of the 'case' statement } | RecordValue a [(String, Expression a)] (Maybe (Type a)) | Precede (Expression a) (Expression a)@@ -343,7 +344,7 @@ , preUniversalsI :: [Universal a] , implicits :: [[Type a]] -- ^ Implicit arguments , universalsI :: [Universal a] -- ^ Universal quantifiers- , nameI :: Name a -- ^ (Name a) of the template being implemented+ , nameI :: Name a -- ^ ('Name' a) of the template being implemented , iArgs :: [Arg a] -- ^ Arguments , _iExpression :: Either (StaticExpression a) (Expression a) -- ^ Expression (or static expression) holding the function body. }@@ -425,6 +426,7 @@ type FixityState a = M.Map String (Fixity a) +-- | Fixities for operators in the ATS prelude. defaultFixityState :: FixityState a defaultFixityState = M.fromList [ ("::", rightFix 40) ]
test/data/fastcount.out view
@@ -20,7 +20,7 @@ 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)) =+ | ptr(l2)) = "mac#atslib_rawmemchr" (* ****** ****** *)