diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -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, diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs --- a/src/Language/ATS.hs +++ b/src/Language/ATS.hs @@ -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 diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x --- a/src/Language/ATS/Lexer.x +++ b/src/Language/ATS/Lexer.x @@ -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 diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y --- a/src/Language/ATS/Parser.y +++ b/src/Language/ATS/Parser.y @@ -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 } diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -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))) <> ")" diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -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 @=>@, @=\@, 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) ] diff --git a/test/data/fastcount.out b/test/data/fastcount.out --- a/test/data/fastcount.out +++ b/test/data/fastcount.out @@ -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" (* ****** ****** *)