language-ats 1.2.0.16 → 1.3.0.0

raw patch · 10 files changed

+375/−324 lines, 10 filessetup-changedPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Setup.hs +0/−2
• language-ats.cabal +5/−3
• src/Language/ATS.hs +3/−0
• src/Language/ATS/Lexer.x +9/−3
• src/Language/ATS/Parser.y +69/−59
• src/Language/ATS/PrettyPrint.hs +67/−57
• src/Language/ATS/Rewrite.hs +103/−0
• src/Language/ATS/Types.hs +25/−199
• src/Language/ATS/Types/Lens.hs +93/−0
• test/data/concurrency.out +1/−1

@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain

@@ -1,6 +1,6 @@ cabal-version: 1.18 name: language-ats-version: 1.2.0.16+version: 1.3.0.0 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018 Vanessa McHale@@ -38,12 +38,14 @@         Language.ATS.Parser         Language.ATS.PrettyPrint         Language.ATS.Types+        Language.ATS.Types.Lens+        Language.ATS.Rewrite     default-language: Haskell2010     other-extensions: OverloadedStrings DeriveGeneric DeriveAnyClass                       FlexibleContexts FlexibleInstances PatternSynonyms                       StandaloneDeriving GeneralizedNewtypeDeriving DerivingStrategies                       DuplicateRecordFields DeriveFunctor TypeFamilies-    ghc-options: -Wall+    ghc-options: -Wall -O2     build-depends:         base >=4.9 && <5,         array -any,@@ -86,7 +88,7 @@     main-is: Bench.hs     hs-source-dirs: bench     default-language: Haskell2010-    ghc-options: -Wall+    ghc-options: -Wall -O2     build-depends:         base -any,         language-ats -any,

@@ -41,6 +41,7 @@                     , SortArg (..)                     , Sort (..)                     , SortArgs+                    , Args                     , Fix                     -- * Parser State                     , FixityState@@ -67,7 +68,9 @@ import           Language.ATS.Lexer import           Language.ATS.Parser import           Language.ATS.PrettyPrint+import           Language.ATS.Rewrite import           Language.ATS.Types+import           Language.ATS.Types.Lens import           Lens.Micro import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) 

@@ -67,7 +67,7 @@ @slash_comment = \/\* ([^\/\*] | @not_close_slash | \n)* \*\/ @block_comment = @paren_comment | @slash_comment -@if_block = "#if" (n | "") ("def" | "") ([^\#] | "#then" | "#print" | \n)+ "#endif" .*+@if_block = "#if" (n | "") ("def" | "") ([^\#] | "#then" | "#else" | "#print" | \n)+ "#endif" .*  -- Basically anything that can go inside implicit arguments, i.e. anything -- necessary to construct a type.@@ -79,7 +79,7 @@ @inner_signature = ("!wrt" | "!exn" | "!refwrt" | "!exnwrt" | "!exnrefwrt" | "!exnref" | "0" | "1" | "!all" | "!laz" | "lin" | "fun" | "clo" | "cloptr" | "cloref" | "!ntm" | "!ref" | "prf" | "fe" | @block_comment) @inner_signature_mult = (@inner_signature (("," | "") @inner_signature)*) | "" -@lambda = "=>" | "=>>" | "=/=>" | "=<" @inner_signature_mult ">"+@lambda = "=>" | "=>>" | "=/=>" | "=/=>>" | "=<" @inner_signature_mult ">" @signature = ":<" @inner_signature_mult ">" | ":" @func_type = "->" | "-<" @inner_signature_mult ">" @@ -241,6 +241,7 @@     <0> "println!"               { tok (\p s -> alex $ Identifier p s) }     <0> "fix@"                   { tok (\p _ -> alex $ Keyword p KwFixAt) }     <0> "lam@"                   { tok (\p _ -> alex $ Keyword p KwLambdaAt) }+    <0> "llam@"                  { tok (\p _ -> alex $ Keyword p KwLinearLambdaAt) }     <0> "addr"                   { tok (\p _ -> alex $ Keyword p KwAddr) }     <0> "addr@"                  { tok (\p _ -> alex $ Keyword p KwAddrAt) }     <0> "view@"                  { tok (\p _ -> alex $ Keyword p KwViewAt) }@@ -267,6 +268,9 @@     <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> "<"                      { tok (\p _ -> alex $ Special p "<") }+    <0> ">"                      { tok (\p _ -> alex $ Special p ">") }+    <0> "[]"                     { tok (\p _ -> alex $ Special p "[]") }     <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) }@@ -401,6 +405,7 @@              | KwMod              | KwFixAt              | KwLambdaAt+             | KwLinearLambdaAt              | KwAddrAt              | KwAddr              | KwSta@@ -461,7 +466,7 @@     pretty (KwVtype a) = "vtype" <> pretty a     pretty KwAnd = "and"     pretty KwDatatype = "datatype"-    pretty KwDatavtype = "datavtype" -- FIXME this wrongly squashes dataviewtype+    pretty KwDatavtype = "datavtype"     pretty KwFnx = "fnx"     pretty KwAssume = "assume"     pretty KwAbsimpl = "absimpl"@@ -525,6 +530,7 @@     pretty KwMod = "mod"     pretty KwFixAt = "fix@"     pretty KwLambdaAt = "lam@"+    pretty KwLinearLambdaAt = "llam@"     pretty KwAddrAt = "addr@"     pretty KwAddr = "addr"     pretty KwSta = "sta"

@@ -10,7 +10,17 @@                                , preErr                                ) where +import Control.Composition+import Control.DeepSeq (NFData)+import qualified Data.Map as M+import Control.Monad.Trans.Class+import Control.Monad.Trans.State+import Data.Char (toLower)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Foldable (toList)+import GHC.Generics (Generic) import Language.ATS.Types+import Language.ATS.Types.Lens import Language.ATS.Lexer ( Token (..)                           , AlexPosn (..)                           , Keyword (..)@@ -20,15 +30,7 @@                           , get_addendum                           , get_staload                           )--import Control.Composition-import Control.DeepSeq (NFData) import Lens.Micro (over, _head)-import qualified Data.Map as M-import Control.Monad.Trans.Class-import Control.Monad.Trans.State-import Data.Char (toLower)-import GHC.Generics (Generic) import Prelude import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) @@ -165,8 +167,8 @@     closeTermetric { Operator $$ ">." }     mutateArrow { FuncType $$ "->" }     mutateEq { Operator $$ ":=" }-    lbracket { Operator $$ "<" }-    rbracket { Operator $$ ">" }+    lbracket { Special $$ "<" }+    rbracket { Special $$ ">" }     eq { Operator $$ "=" }     or { Operator $$ "||" }     vbar { Special $$ "|" }@@ -180,8 +182,10 @@     lincloref1Arrow { Arrow $$ "=<lin,cloref1>" }     spear { Arrow $$ "=>>" }     proofArrow { Arrow $$ "=/=>" }+    proofSpear { Arrow $$ "=/=>>" }     lsqbracket { Special $$ "[" }     rsqbracket { Special $$ "]" }+    doubleSqBrackets { Special $$ "[]" }     string { StringTok _ $$ }     charLit { CharTok _ $$ }     underscore { Special $$ "_" }@@ -216,6 +220,7 @@     mod { Keyword $$ KwMod }     fixAt { Keyword $$ KwFixAt }     lamAt { Keyword $$ KwLambdaAt }+    llamAt { Keyword $$ KwLinearLambdaAt }     infixr { FixityTok $$ "infixr" }     infixl { FixityTok $$ "infixl" }     prefix { FixityTok $$ "prefix" }@@ -235,8 +240,8 @@     : some(p) p { $2 : $1 }     | { [] } -sep_by(p,sep) : p { [$1] }-              | sep_by(p,sep) sep p { $3 : $1 }+sep_by(p,sep) : p { $1 :| [] }+              | sep_by(p,sep) sep p { $3 :| (toList $1) }  comma_sep(p)     : sep_by(p, comma) { $1 }@@ -261,7 +266,7 @@  ExprType : StaticExpression { ConcreteType $1 } -TypeInExpr : comma_sep(alt(Type,ExprType)) { $1 }+TypeInExpr : comma_sep(alt(Type,ExprType)) { toList $1 }  -- | Parse a type Type : Name parens(TypeInExpr) { Dependent $1 $2 }@@ -289,8 +294,8 @@      | atbrace Records rbrace { AnonymousRecord $1 $2 }      | 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 closeParen { Tuple $1 (toList $2) }+     | openParen TypeIn closeParen lineComment { Tuple $1 (toList $2) }      | boxTuple TypeIn closeParen { BoxTuple $1 $2 }      | boxTuple TypeIn closeParen lineComment { BoxTuple $1 $2 }      | openParen Type closeParen { ParenType $1 $2 }@@ -328,7 +333,7 @@         | doubleParens { VoidLiteral $1 }  -- | Parse a list of comma-separated patterns-PatternIn : comma_sep(Pattern) { $1 }+PatternIn : comma_sep(Pattern) { reverse (toList $1) }  -- | Parse a pattern match Pattern : Name { PName $1 [] }@@ -369,15 +374,16 @@               | ExpressionIn vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof?  -- | A list of comma-separated expressions-ExpressionIn : comma_sep(Expression) { $1 }+ExpressionIn : comma_sep(Expression) { toList $1 } -Tuple : PreExpression comma PreExpression { [$3, $1] }-      | Tuple comma PreExpression { $3 : $1 }+Tuple : PreExpression comma PreExpression { $3 :| [$1] }+      | Tuple comma PreExpression { $3 :| toList $1 }  -- | Parse an arrow in a case statement CaseArrow : plainArrow { Plain $1 }           | spear { Spear $1 }           | proofArrow { ProofArrow $1 }+          | proofSpear { ProofSpear $1 }           | minus {% left $ Expected $1 "Arrow" "-" }           | eq {% left $ Expected $1 "Arrow" "=" }           | minus {% left $ Expected $1 "Arrow" "-" }@@ -395,22 +401,21 @@ -- | Expression or named call to an expression Expression : identifierSpace PreExpression { Call (Unqualified $ to_string $1) [] [] Nothing [$2] }            | PreExpression { $1 }-           | openParen PreExpression comma PreExpression vbar PreExpression closeParen { TupleEx $1 [$2, $4, $6] } -- FIXME this is wrong+           -- | openParen PreExpression comma PreExpression vbar PreExpression closeParen { ProofExpr $1 [$2, $4] $6 }+           | openParen comma_sep(PreExpression) vbar PreExpression closeParen { ProofExpr $1 $2 $4 }            | Expression semicolon Expression { Precede $1 $3 }            | Expression semicolon { $1 }            | openParen Expression closeParen { $2 }            | 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 }            | begin Expression extern {% left $ Expected $3 "end" "extern" }            | Expression prfTransform underscore {% left $ Expected $2 "Rest of expression or declaration" ">>" } -TypeArgs : lbrace Type rbrace { [$2] }-         | lbrace TypeIn rbrace { $2 }-         | TypeArgs lbrace Type rbrace { $3 : $1 }+TypeArgs : lbrace alt(Type,ExprType) rbrace { [$2] }+         | lbrace TypeInExpr rbrace { $2 }+         | TypeArgs lbrace alt(Type,ExprType) rbrace { $3 : $1 }          | lbrace doubleDot rbrace { [ ImplicitType $2 ] } -- FIXME only valid on function calls-         | TypeArgs lbrace TypeIn rbrace { $3 ++ $1 }-         | TypeArgs lbrace StaticExpression rbrace { (ConcreteType $3) : $1 }+         | TypeArgs lbrace TypeInExpr rbrace { $3 ++ $1 }  Call : Name doubleParens { Call $1 [] [] Nothing [] }      | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) }@@ -422,10 +427,11 @@      | Name Implicits openParen ExpressionPrf closeParen { Call $1 $2 [] (fst $4) (snd $4) }      | Name Implicits { Call $1 $2 [] Nothing [] }      | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] } -- $raise can have at most one argument+     | Name Implicits openParen ExpressionPrf fun {% left $ Expected $5 ")" "fun" }      | Name openParen ExpressionPrf end {% left $ Expected $4 ")" "end"}      | Name openParen ExpressionPrf else {% left $ Expected $4 ")" "else"} -StaticArgs : comma_sep(StaticExpression) { $1 }+StaticArgs : comma_sep(StaticExpression) { reverse (toList $1) }  StaticDecls : StaticDeclaration { [$1] }             | StaticDecls StaticDeclaration { $2 : $1 }@@ -436,7 +442,7 @@                  | StaticExpression BinOp StaticExpression { StaticBinary $2 $1 $3 }                  | intLit { StaticInt $1 }                  | doubleParens { StaticVoid $1 }-                 | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 } -- TODO separate type for static expressions+                 | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 }                  | identifierSpace { StaticVal (Unqualified $ to_string $1) }                  | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [$2] }                  | Name openParen StaticArgs closeParen { SCall $1 $3 }@@ -459,7 +465,7 @@               | ifcase IfCase { IfCase $1 $2 }               | openParen Expression closeParen { ParenExpr $1 $2 }               | PreExpression BinOp PreExpression { Binary $2 $1 $3 }-              | UnOp PreExpression { Unary $1 $2 } -- FIXME throw error when we try to negate a string literal/time+              | UnOp PreExpression { Unary $1 $2 }               | PreExpression dot Name { Access $2 $1 $3 }               | PreExpression dot intLit { Access $2 $1 (Unqualified $ show $3) }               | PreExpression dot identifierSpace { Access $2 $1 (Unqualified $ to_string $3) }@@ -528,7 +534,7 @@      | IdentifierOr { NamedSort $1 }      | IdentifierOr plus { NamedSort ($1 <> "+") } -QuantifierArgs : comma_sep(IdentifierOr) { $1 }+QuantifierArgs : comma_sep(IdentifierOr) { reverse (toList $1) }                | { [] }  -- FIXME handle [l:addr;n:int]@@ -548,19 +554,16 @@           | lbrace QuantifierArgs colon Sort rbrace { Universal $2 (Just $4) [] }           | lbrace QuantifierArgs colon Sort vbar Predicates rbrace { Universal $2 (Just $4) $6 } -Implicits : lspecial TypeIn rbracket { [$2] }-          | Implicits lspecial TypeIn rbracket { $3 : $1 }+Implicits : lspecial TypeIn rbracket { [toList $2] }+          | Implicits lspecial TypeIn rbracket { toList $3 : $1 }           | doubleBrackets { [[Named (Unqualified "")]] }           | Implicits doubleBrackets { [Named (Unqualified "")] : $1 }-          | lbracket TypeIn rbracket { [$2] }-          | Implicits lspecial TypeIn rbracket { $3 : $1 }+          | lbracket TypeIn rbracket { [toList $2] }+          | Implicits lspecial TypeIn rbracket { toList $3 : $1 }            MaybeImplicit : Implicits { $1 }               | { [] } -ImplExpression : StaticExpression { Left $1 }-               | Expression { Right $1 }- comment_after(p) : p { $1 }                  | p Comment { $1 }                  | p lineComment { $1 }@@ -599,12 +602,12 @@ Records : IdentifierOr eq Type { [($1, $3)] }         | Records comma IdentifierOr eq Type { ($3, $5) : $1 } -IdentifiersIn : comma_sep(IdentifierOr) { $1 }+IdentifiersIn : comma_sep(IdentifierOr) { toList $1 }  OfType : { Nothing }        | of Type { Just $2 } -StaticExpressionsIn : comma_sep(StaticExpression) { $1 }+StaticExpressionsIn : comma_sep(StaticExpression) { toList $1 }  -- | Parse a constructor for a sum type SumLeaf : vbar Universals identifier { Leaf $2 (to_string $3) [] Nothing }@@ -616,13 +619,15 @@        | 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 StaticExpressionsIn 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] }        | dollar {% left $ Expected $1 "|" "$" } -Universals : { [] }-           | doubleBraces { [] }-           | Universals Universal { $2 : $1 }+PreUniversals : { [] }+              | doubleBraces { [] }+              | PreUniversals Universal { $2 : $1 } +Universals : PreUniversals { reverse $1 }+ -- | Optionally parse a termetric OptTermetric : { Nothing }              | Termetric { Just (snd $1) }@@ -664,6 +669,9 @@               | eq lineComment fun {% left $ Expected $3 "Expression" "=" }               | lbrace {% left $ Expected $1 "Expression" "{" } +OptStaticExpression : { Nothing }+                    | eq StaticExpression { Just $2 }+ -- | Parse a constructor for a 'dataprop' DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 Nothing }              | Universals Expression { DataPropLeaf $1 $2 Nothing }@@ -693,13 +701,13 @@         | { Nothing }  -- | Parse a type signature and optional function body-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 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 }+PreFunction : FunName openParen Args closeParen OptType OptExpression { (PreF $1 (fmap fst $5) [] [] (Just $3) (fmap snd $5) Nothing $6) }+            | FunName Universals OptTermetric OptType OptExpression { PreF $1 (fmap fst $4) [] $2 Nothing (fmap snd $4) $3 $5 }+            | FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $1 (fmap fst $5) [] $2 (Just []) (fmap snd $5) $3 $6 }+            | FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $1 (fmap fst $7) [] $2 (Just $5) (fmap snd $7) $3 $8 }+            | Universals FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $2 (fmap fst $8) $1 $3 (Just $6) (fmap snd $8) $4 $9 }+            | Universals FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $2 (fmap fst $6) $1 $3 (Just []) (fmap snd $6) $4 $7 }+            | Universals FunName Universals OptTermetric OptType OptExpression { PreF $2 (fmap fst $5) $1 $3 Nothing (fmap snd $5) $4 $6 }             | prval {% left $ Expected $1 "Function signature" "prval" }             | var {% left $ Expected $1 "Function signature" "var" }             | val {% left $ Expected (token_posn $1) "Function signature" "val" }@@ -755,9 +763,9 @@ MaybeType : eq Type { Just $2 }           | { Nothing } -FunArgs : { [NoArgs] }-        | openParen Args closeParen { $2 }-        | doubleParens { [] }+FunArgs : { Nothing }+        | openParen Args closeParen { Just $2 }+        | doubleParens { Just [] }  SortArg : IdentifierOr colon Sort { [ SortArg $1 $3 ] }         | SortArg comma IdentifierOr colon Sort { SortArg $3 $5 : $1 }@@ -772,7 +780,6 @@          | { 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 }@@ -911,7 +918,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 doubleSqBrackets with IdentifierOr { OverloadIdent $1 "[]" (Unqualified $4) 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) }@@ -920,7 +927,7 @@             | overload identifierSpace with identifierSpace of intLit { OverloadIdent $1 (to_string $2) (Unqualified $ to_string $4) (Just $6) }             | overload tilde with identifier { OverloadIdent $1 "~" (Unqualified $ to_string $4) Nothing } -- FIXME figure out a general solution.             | overload tilde with identifierSpace of intLit { OverloadIdent $1 "~" (Unqualified $ to_string $4) (Just $6) }-            | overload lsqbracket rsqbracket with identifierSpace of intLit { OverloadIdent $1 "[]" (Unqualified $ to_string $5) (Just $7) }+            | overload doubleSqBrackets with identifierSpace of intLit { OverloadIdent $1 "[]" (Unqualified $ to_string $4) (Just $6) }             | overload dot identifierSpace with Name { OverloadIdent $1 ('.' : (to_string $3)) $5 Nothing }             | assume identifierSpace SortArgs eq Type { Assume (Unqualified (to_string $2)) $3 $5 }             | assume Name SortArgs eq Type { Assume $2 $3 $5 }@@ -929,8 +936,8 @@             | tkindef IdentifierOr eq string { TKind $1 (Unqualified $2) $4 }             | TypeDecl { $1 }             | 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 }+            | stacst IdentifierOr colon Type OptStaticExpression { Stacst $1 (Unqualified $2) $4 $5 }+            | propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 (Just $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 {% addSt $1 $2 }@@ -958,6 +965,7 @@               | OneOf AlexPosn [String] String               | Unknown Token               | LexError String+              | Exhausted               deriving (Eq, Show, Generic, NFData)  unmatched :: AlexPosn -> String -> Doc@@ -980,11 +988,13 @@ preErr (Unknown (Special l ">")) = unmatched l ">" preErr (Unknown t) = "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak preErr (LexError s) = dullred "lexing:" <+> text s <> linebreak+preErr Exhausted = "unexpectedly out of input"  left :: ATSError -> ParseSt b left = lift . Left  parseError :: [Token] -> ParseSt a-parseError = left . Unknown . head +parseError [] = left Exhausted +parseError x = left . Unknown . head $ x  }

@@ -5,7 +5,6 @@ {-# LANGUAGE FlexibleContexts   #-} {-# LANGUAGE FlexibleInstances  #-} {-# LANGUAGE OverloadedStrings  #-}-{-# LANGUAGE PatternSynonyms    #-} {-# LANGUAGE StandaloneDeriving #-}  module Language.ATS.PrettyPrint ( printATS@@ -15,7 +14,11 @@  import           Control.Composition          hiding ((&)) import           Data.Bool                    (bool)+import           Data.Foldable                (toList) import           Data.Functor.Foldable        (cata)+import           Data.List                    (isPrefixOf)+import           Data.List.NonEmpty           (NonEmpty (..))+import qualified Data.List.NonEmpty           as NE import           Language.ATS.Types import           Lens.Micro import           Prelude                      hiding ((<$>))@@ -23,9 +26,6 @@  infixr 5 $$ -pattern NoA :: [Arg a]-pattern NoA = [NoArgs]- -- | Pretty-print with sensible defaults. printATS :: Eq a => ATS a -> String printATS = (<> "\n") . printATSCustom 0.6 120@@ -53,6 +53,7 @@     pretty Plain{}      = "=>"     pretty Spear{}      = "=>>"     pretty ProofArrow{} = "=/=>"+    pretty ProofSpear{} = "=/=>>"     pretty (Full _ v)   = "=<" <> text v <> ">"  instance Pretty (BinOp a) where@@ -100,7 +101,6 @@ prettyLarge _ []      = mempty prettyLarge op (e:es) = e <$> vsep (fmap (op <+>) es) --- FIXME we really need a monadic pretty printer lol. lengthAlt :: Doc -> Doc -> Doc lengthAlt d1 d2     | length (showFast d2) >= 30 = d1 <$> indent 4 d2@@ -115,6 +115,10 @@     pretty Deref           = "!"     pretty (SpecialOp _ s) = text s +prettyProofExpr :: NonEmpty Doc -> Doc+prettyProofExpr (e:|[]) = e+prettyProofExpr es      = mconcat (punctuate ", " (toList es))+ instance Eq a => Pretty (Expression a) where     pretty = cata a where         a (IfF e e' (Just e''))         = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''@@ -137,20 +141,20 @@             | splits op = e </> pretty op <+> e'             | otherwise = e <+> pretty op <+> e'         a (IndexF _ n e)                = pretty n <> brackets e-        a (NamedValF nam)              = pretty nam-        a (CallF nam [] [] Nothing []) = pretty nam <> "()"-        a (CallF nam [] [] e xs) = pretty nam <> prettyArgsProof e xs-        a (CallF nam [] us Nothing []) = pretty nam <> prettyArgsU "{" "}" us+        a (NamedValF nam)               = pretty nam+        a (CallF nam [] [] Nothing [])  = pretty nam <> "()"+        a (CallF nam [] [] e xs)        = pretty nam <> prettyArgsProof e xs+        a (CallF nam [] us Nothing [])  = pretty nam <> prettyArgsU "{" "}" us         a (CallF nam [] us Nothing [x])             | startsParens x = pretty nam <> prettyArgsU "{" "}" us <> pretty x-        a (CallF nam [] us e xs) = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsProof e xs-        a (CallF nam is [] Nothing []) = pretty nam <> prettyImplicits is+        a (CallF nam [] us e xs)        = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsProof e xs+        a (CallF nam is [] Nothing [])  = pretty nam <> prettyImplicits is         a (CallF nam is [] Nothing [x])             | startsParens x = pretty nam <> prettyImplicits is <> pretty x-        a (CallF nam is [] e xs) = pretty nam <> prettyImplicits is <> prettyArgsProof e xs+        a (CallF nam is [] e xs)        = pretty nam <> prettyImplicits is <> prettyArgsProof e xs         a (CallF nam is us Nothing [x])             | startsParens x = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> pretty x-        a (CallF nam is us e xs) = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> prettyArgsProof e xs+        a (CallF nam is us e xs)        = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> prettyArgsProof e xs         a (CaseF _ add' e cs)           = "case" <> pretty add' <+> e <+> "of" <$> indent 2 (prettyCases cs)         a (IfCaseF _ cs)                = "ifcase" <$> indent 2 (prettyIfCase cs)         a (VoidLiteralF _)              = "()"@@ -160,17 +164,17 @@         a (PrecedeListF es)             = lineAlt (prettyArgsList "; " "(" ")" es) ("(" <> mconcat (punctuate " ; " es) <> ")")         a (AccessF _ e n)             | noParens e = e <> "." <> pretty n-            | otherwise = parens e <> "." <> pretty n+            | otherwise  = parens e <> "." <> pretty n         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 (ProofExprF _ es e')         = "(" <> prettyProofExpr es <+> "|" <+> e' <> ")"         a (TypeSignatureF e t)         = e <+> ":" <+> pretty t         a (WhereExpF e d)              = e <+> "where" <$> braces (" " <> nest 2 (pretty d) <> " ")-        a (TupleExF _ es)              = parens (mconcat $ punctuate ", " (reverse es))-        a (BoxTupleExF _ es)           = "'(" <> mconcat (punctuate ", " (reverse es)) <> ")"+        a (TupleExF _ es)              = parens (mconcat $ punctuate ", " (toList $ NE.reverse es))+        a (BoxTupleExF _ es)           = "'(" <> mconcat (punctuate ", " (toList $ NE.reverse es)) <> ")"         a (WhileF _ e e')              = "while" <> parens e <> e'         a (ForF _ e e')                = "for" <> parens e <> e'         a (WhileStarF _ us t as e e' Nothing)   = "while*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> "=>" <$> indent 4 e <$> indent 4 e'@@ -181,7 +185,7 @@         a UnderscoreLitF{}             = "_"         a (BeginF _ e)             | not (startsParens e) = linebreak <> indent 2 ("begin" <$> indent 2 e <$> "end")-            | otherwise = e+            | otherwise          = e         a (FixAtF _ n (StackF s as t e))  = "fix@" <+> text n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)         a (LambdaAtF _ (StackF s as t e)) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)         a (AddrAtF _ e)                   = "addr@" <> e@@ -190,7 +194,9 @@         a (CommentExprF c e) = text c <$> e         a (MacroVarF _ s) = ",(" <> text s <> ")"         a BinListF{} = undefined -- Shouldn't happen+         prettyImplicits = mconcat . fmap (prettyArgsU "<" ">") . reverse+         prettyIfCase []              = mempty         prettyIfCase [(s, l, t)]     = "|" <+> s <+> pretty l <+> t         prettyIfCase ((s, l, t): xs) = prettyIfCase xs $$ "|" <+> s <+> pretty l <+> t@@ -204,7 +210,7 @@ noParens = all (`notElem` ("()" :: String)) . show  patternHelper :: [Doc] -> Doc-patternHelper ps = mconcat (punctuate ", " (reverse ps))+patternHelper ps = mconcat (punctuate ", " ps)  instance Eq a => Pretty (Pattern a) where     pretty = cata a where@@ -229,7 +235,6 @@ argHelper _ (Arg (Second t))  = pretty t argHelper op (Arg (Both s t)) = pretty s `op` colon `op` pretty t 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@@ -257,7 +262,7 @@         a (StaticIntF i)            = pretty i         a StaticVoidF{}             = "()"         a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''-        a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . reverse . fmap pretty $ cs))+        a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))         a (SPrecedeF e e')          = e <> ";" <+> e'         a (SUnaryF op e)            = pretty op <> e         a (SLetF _ e e') = flatAlt@@ -295,11 +300,11 @@         a (AtExprF _ t t')                 = t <+> "@" <+> pretty t'         a (AtTypeF _ t)                    = "@" <> t         a (ProofTypeF _ t t')              = parens (pre' `op` "|" <+> t')-            where pre' = prettyArgsG mempty mempty t+            where pre' = prettyArgsG mempty mempty (toList 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))) <> ")"+        a (BoxTupleF _ ts)                 = "'(" <> mconcat (punctuate ", " (toList $ fmap pretty (NE.reverse ts))) <> ")"         a (RefTypeF t)                     = "&" <> t         a (FunctionTypeF s t t')           = t <+> string s <+> t'         a (ViewLiteralF c)                 = "view" <> pretty c@@ -321,15 +326,15 @@     pretty (Existential [] b (Just st) (Just e')) = withHashtag b <> pretty st <> pretty e' <> rbracket     pretty (Existential [] b Nothing (Just e')) = withHashtag b <> pretty e' <> rbracket     pretty (Existential [e] b (Just st) Nothing) = withHashtag b <> text e <> ":" <> pretty st <> rbracket-    pretty (Existential bs b st Nothing) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan st <+> rbracket-    pretty (Existential bs b st (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan st <> "|" <+> pretty e <+> rbracket+    pretty (Existential bs b st Nothing) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan st <+> rbracket+    pretty (Existential bs b st (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan st <> "|" <+> pretty e <+> rbracket  instance Eq a => Pretty (Universal a) where     pretty (Universal [x] Nothing []) = lbrace <> text x <> rbrace     pretty (Universal [x] (Just st) []) = lbrace <> text x <> ":" <> pretty st <> rbrace-    pretty (Universal bs Nothing []) = lbrace <> mconcat (punctuate "," (fmap pretty (reverse bs))) <> rbrace-    pretty (Universal bs (Just ty) []) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <+> ":" <+> pretty ty <+> rbrace-    pretty (Universal bs ty es) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <> "|" <+> mconcat (punctuate "; " (fmap pretty es)) <+> rbrace+    pretty (Universal bs Nothing []) = lbrace <> mconcat (punctuate "," (fmap pretty bs)) <> rbrace+    pretty (Universal bs (Just ty) []) = lbrace <+> mconcat (punctuate ", " (fmap pretty bs)) <+> ":" <+> pretty ty <+> rbrace+    pretty (Universal bs ty es) = lbrace <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan ty <> "|" <+> mconcat (punctuate "; " (fmap pretty es)) <+> rbrace  instance Eq a => Pretty (ATS a) where     pretty (ATS xs) = concatSame (reverse xs)@@ -343,12 +348,15 @@ prettyImplExpr (Right e) = pretty e  instance Eq a => Pretty (Implementation a) where-    pretty (Implement _ [] is [] n [] e)  = pretty n <> prettyOr is <+> "() =" <$> indent 2 (prettyImplExpr e)-    pretty (Implement _ [] is [] n NoA e)  = pretty n <> prettyOr is <+> "=" <$> indent 2 (prettyImplExpr e)-    pretty (Implement _ [] is [] n ias e) = pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)-    pretty (Implement _ [] is us n ias e) = pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)-    pretty (Implement _ ps is [] n ias e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)-    pretty (Implement _ ps is us n ias e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ [] is [] n (Just []) e)  = pretty n <> prettyOr is <+> "() =" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ [] is [] n Nothing e)    = pretty n <> prettyOr is <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ [] is [] n (Just ias) e) = pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ [] is us n (Just ias) e) = pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ [] is us n Nothing e) = pretty n <> prettyOr is <+> foldMap pretty us </> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is [] n (Just ias) e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is [] n Nothing e)    = foldMap pretty (reverse ps) </> pretty n <> prettyOr is <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is us n (Just ias) e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is us n Nothing e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> "=" <$> indent 2 (prettyImplExpr e)  isVal :: Declaration a -> Bool isVal Val{}   = True@@ -357,6 +365,9 @@ isVal PrVar{} = True isVal _       = False +notDefine :: String -> Bool+notDefine = not . ("#define" `isPrefixOf`)+ glue :: Declaration a -> Declaration a -> Bool glue x y     | isVal x && isVal y = True@@ -374,6 +385,8 @@ glue Comment{} _                   = True glue (Func _ Fnx{}) (Func _ And{}) = True glue Assume{} Assume{}             = True+glue (Define s) _ | notDefine s    = True+glue _ (Define s) | notDefine s    = True glue _ _                           = False  concatSame :: Eq a => [Declaration a] -> Doc@@ -383,7 +396,6 @@     | glue x x' = pretty x <$> concatSame (x':xs)     | otherwise = pretty x <> line <$> concatSame (x':xs) --- TODO - soft break ($$) :: Doc -> Doc -> Doc x $$ y = align (x <$> y) @@ -396,7 +408,7 @@ prettyRecord :: (Pretty a) => [(String, a)] -> Doc prettyRecord es     | any ((>40) . length . showFast . pretty) es = prettyRecordF True es-    | otherwise = lineAlt (prettyRecordF True es) (prettyRecordS True es)+    | otherwise                                   = lineAlt (prettyRecordF True es) (prettyRecordS True es)  prettyRecordS :: (Pretty a) => Bool -> [(String, a)] -> Doc prettyRecordS _ []             = mempty@@ -414,7 +426,7 @@  prettyUsNil :: Eq a => [Universal a] -> Doc prettyUsNil [] = space-prettyUsNil us = space <> foldMap pretty (reverse us) <> space+prettyUsNil us = space <> foldMap pretty us <> space  prettyOf :: (Pretty a) => Maybe a -> Doc prettyOf Nothing  = mempty@@ -425,9 +437,6 @@ prettyDL [DataPropLeaf us e e']    = indent 2 ("|" <> prettyUsNil us <> pretty e <> prettyOf e') prettyDL (DataPropLeaf us e e':xs) = prettyDL xs $$ indent 2 ("|" <> prettyUsNil us <> pretty e <> prettyOf e') -universalHelper :: Eq a => [Universal a] -> Doc-universalHelper = mconcat . fmap pretty . reverse- prettyDSL :: Eq a => [DataSortLeaf a] -> Doc prettyDSL []                          = mempty prettyDSL [DataSortLeaf us sr sr']    = indent 2 ("|" <> prettyUsNil us <> pretty sr <> prettyOf sr')@@ -443,14 +452,14 @@ prettyLeaf [Leaf [] s as (Just e)]    = indent 2 ("|" <+> text s <> prettyArgs as <+> "of" <+> pretty e) prettyLeaf (Leaf [] s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> text s <> prettyArgs as) prettyLeaf (Leaf [] s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> text s <> prettyArgs as <+> "of" <+> pretty e)-prettyLeaf [Leaf us s [] Nothing]     = indent 2 ("|" <+> universalHelper us <+> text s)-prettyLeaf [Leaf us s [] (Just e)]    = indent 2 ("|" <+> universalHelper us <+> text s <+> "of" <+> pretty e)-prettyLeaf (Leaf us s [] Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s)-prettyLeaf (Leaf us s [] (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <+> "of" <+> pretty e)-prettyLeaf [Leaf us s as Nothing]     = indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as)-prettyLeaf [Leaf us s as (Just e)]    = indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as <+> "of" <+> pretty e)-prettyLeaf (Leaf us s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as)-prettyLeaf (Leaf us s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as <+> "of" <+> pretty e)+prettyLeaf [Leaf us s [] Nothing]     = indent 2 ("|" <+> fancyU us <+> text s)+prettyLeaf [Leaf us s [] (Just e)]    = indent 2 ("|" <+> fancyU us <+> text s <+> "of" <+> pretty e)+prettyLeaf (Leaf us s [] Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> fancyU us <+> text s)+prettyLeaf (Leaf us s [] (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> fancyU us <+> text s <+> "of" <+> pretty e)+prettyLeaf [Leaf us s as Nothing]     = indent 2 ("|" <+> fancyU us <+> text s <> prettyArgs as)+prettyLeaf [Leaf us s as (Just e)]    = indent 2 ("|" <+> fancyU us <+> text s <> prettyArgs as <+> "of" <+> pretty e)+prettyLeaf (Leaf us s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> fancyU us <+> text s <> prettyArgs as)+prettyLeaf (Leaf us s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> fancyU us <+> text s <> prettyArgs as <+> "of" <+> pretty e)  prettyHelper :: Doc -> [Doc] -> [Doc] prettyHelper _ [x]    = [x]@@ -482,17 +491,16 @@ prettyArgs :: (Pretty a) => [a] -> Doc prettyArgs = prettyArgs' ", " "(" ")" -prettyArgsNil :: Eq a => [Arg a] -> Doc-prettyArgsNil NoA = mempty-prettyArgsNil as  = prettyArgs' ", " "(" ")" as+prettyArgsNil :: Eq a => Maybe [Arg a] -> Doc+prettyArgsNil Nothing   = mempty+prettyArgsNil (Just as) = prettyArgs' ", " "(" ")" as  fancyU :: Eq a => [Universal a] -> Doc-fancyU = foldMap pretty . reverse+fancyU = foldMap pretty  (<#>) :: 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 `op` ":" <> text si <#> pretty rt <> d'     where op a b = lineAlt (a <$> indent 2 b) (a <> b)@@ -515,7 +523,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 NoA rt Nothing Nothing) = pretty i </> fancyU us <> prettySigNull si rt+    pretty (PreF i si [] us Nothing 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@@ -559,7 +567,7 @@     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 (Impl as i)                      = "implement" <+> prettyArgsNil as <> 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@@ -587,7 +595,8 @@     -- 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 (Define s) | "#if" `isPrefixOf` s = text ("\n" <> s)+                      | otherwise            = text s     pretty (Func _ (Fn pref))               = "fn" </> pretty pref     pretty (Func _ (Fun pref))              = "fun" </> pretty pref     pretty (Func _ (CastFn pref))           = "castfn" </> pretty pref@@ -605,7 +614,8 @@     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 (PropDef _ s as@Just{} t)        = "propdef" </> text s <+> prettyArgsNil as <+> "=" </> pretty t+    pretty (PropDef _ s Nothing t)          = "propdef" </> text s <+> "=" </> 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)

@@ -0,0 +1,103 @@+module Language.ATS.Rewrite ( rewriteDecl+                            -- * Fixity+                            , defaultFixityState+                            ) where++import           Control.Composition+import           Data.Function           (on)+import           Data.Functor.Foldable+import qualified Data.Map                as M+import           Data.Maybe              (isJust)+import           Language.ATS.Types+import           Language.ATS.Types.Lens+import           Lens.Micro++exprLens :: Eq a => FixityState a -> ASetter s t (Expression a) (Expression a) -> s -> t+exprLens st = flip over (rewriteATS st)++exprLenses :: Eq a => FixityState a -> [ASetter b b (Expression a) (Expression a)] -> b -> b+exprLenses st = thread . fmap (exprLens st)++rewriteDecl :: Eq a => FixityState a -> Declaration a -> Declaration a+rewriteDecl st (Extern l d) = Extern l (rewriteDecl st d)+rewriteDecl st x@Val{} = exprLens st valExpression x+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._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+    where g = over (leaves.mapped.constructorUniversals) h+          h :: Eq a => [Universal a] -> [Universal a]+          h = ana c where+            c (y:y':ys)+                | typeU y == typeU y' && isJust (typeU y) =+                    Cons (Universal (bound y ++ bound y') (typeU y) (StaticBinary LogicalAnd <$> prop y <*> prop y')) ys+            c y = project y+rewriteDecl _ x = x++-- | Fixities for operators in the ATS prelude.+defaultFixityState :: FixityState a+defaultFixityState = M.fromList+    [ ("::", rightFix 40) ]++leftFix :: Int -> Fixity a+leftFix = LeftFix undefined . Left++rightFix :: Int -> Fixity a+rightFix = RightFix undefined . Left++infix_ :: Int -> Fixity a+infix_ = Infix undefined . Left++-- | 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 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)++-- | Among other things, this rewrites expressions so that operator precedence+-- is respected; this ensures @1 + 2 * 3@ will be parsed as the correct+-- expression.+rewriteATS :: Eq a => FixityState a -> Expression a -> Expression a+rewriteATS st = cata a where+    a (LetF loc (ATS ds) e')                         = Let loc (ATS (rewriteDecl st <$> ds)) e'+    a (CallF n ts ts' me [ParenExpr _ e@NamedVal{}]) = Call n ts ts' me [e]+    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)+    a (BinaryF Add e e')                             = BinList Add [e, e']+    a (BinaryF Con{} e (BinList Add es))             = BinList (SpecialInfix undefined "::") (e : es)+    a (BinaryF Con{} e e')                           = BinList (SpecialInfix undefined "::") [e, e']+    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

@@ -43,34 +43,20 @@     , SortF (..)     , SortArg (..)     , SortArgs+    , Args     , DataSortLeaf (..)-    , FixityState     , Fix-    -- * Rewrites-    , rewriteDecl-    -- * Helper functions-    , defaultFixityState-    -- * Lenses-    , preF-    , expression-    , fun-    , leaves-    , constructorUniversals-    , typeCall-    , typeCallArgs-    , comment+    , FixityState     ) where -import           Control.Composition import           Control.DeepSeq       (NFData) import           Data.Function         (on) import           Data.Functor.Foldable hiding (Fix (..))+import           Data.List.NonEmpty    (NonEmpty) import qualified Data.Map              as M-import           Data.Maybe            (isJust) import           Data.Semigroup        (Semigroup) import           GHC.Generics          (Generic) import           Language.ATS.Lexer    (Addendum (..))-import           Lens.Micro  type Fix = Either Int String @@ -89,57 +75,13 @@ data Leaf a = Leaf { _constructorUniversals :: [Universal a], name :: String, constructorArgs :: [StaticExpression a], maybeType :: Maybe (Type a) }     deriving (Show, Eq, Generic, NFData) -constructorUniversals :: Lens' (Leaf a) [Universal a]-constructorUniversals f s = fmap (\x -> s { _constructorUniversals = x}) (f (_constructorUniversals s))- type SortArgs a = Maybe [SortArg a]--fun :: Traversal' (Declaration a) (Function a)-fun f (Func x y) = Func x <$> f y-fun _ x          = pure x--impl :: Traversal' (Declaration a) (Implementation a)-impl f (Impl x y)      = Impl x <$> f y-impl f (ProofImpl x y) = ProofImpl x <$> f y-impl _ x               = pure x--valExpression :: Traversal' (Declaration a) (Expression a)-valExpression f (Val a v p e) = Val a v p <$> f e-valExpression _ x             = pure x--prValExpr :: Traversal' (Declaration a) (Maybe (Expression a))-prValExpr f (PrVal p me t) = (\me' -> PrVal p me' t) <$> f me-prValExpr _ x              = pure x--varExpr1 :: Traversal' (Declaration a) (Maybe (Expression a))-varExpr1 f (Var t p e e') = (\e'' -> Var t p e'' e') <$> f e-varExpr1 _ x              = pure x--varExpr2 :: Traversal' (Declaration a) (Maybe (Expression a))-varExpr2 f (Var t p e e') = (\e'' -> Var t p e e'') <$> f e'-varExpr2 _ x              = pure x--andExpr :: Traversal' (Declaration a) (Expression a)-andExpr f (AndDecl t p e) = AndDecl t p <$> f e-andExpr _ x               = pure x--propLeaves :: Traversal' (Declaration a) [DataPropLeaf a]-propLeaves f (DataProp l n as pl) = DataProp l n as <$> f pl-propLeaves _ x                    = pure x--leaves :: Traversal' (Declaration a) [Leaf a]-leaves f (SumType t as l)     = SumType t as <$> f l-leaves f (SumViewType t as l) = SumViewType t as <$> f l-leaves _ x                    = pure x--comment :: Traversal' (Declaration a) String-comment f (Comment c) = Comment <$> f c-comment _ x           = pure x+type Args a = Maybe [Arg a]  -- | 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 }+                   | Impl { implArgs :: Args a, _impl :: Implementation a } -- TODO do something better for implicit universals+                   | ProofImpl { implArgs :: Args 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 :: Maybe (Expression a), prValType :: Maybe (Type a) }@@ -174,8 +116,8 @@                    | Assume (Name a) (SortArgs a) (Type a)                    | TKind a (Name a) String                    | SymIntr a [Name a]-                   | Stacst a (Name a) (Type a) (Maybe (Expression a))-                   | PropDef a String [Arg a] (Type a)+                   | Stacst a (Name a) (Type a) (Maybe (StaticExpression a))+                   | PropDef a String (Args a) (Type a)                    | FixityDecl (Fixity a) [String]                    | MacDecl a String [String] (Expression a)                    | DataSort a String [DataSortLeaf a]@@ -190,26 +132,20 @@ data DataPropLeaf a = DataPropLeaf { propU :: [Universal a], _propExpr1 :: Expression a, _propExpr2 :: Maybe (Expression a) }                     deriving (Show, Eq, Generic, NFData) -propExpr1 :: Lens' (DataPropLeaf a) (Expression a)-propExpr1 f s = fmap (\x -> s { _propExpr1 = x}) (f (_propExpr1 s))--propExpr2 :: Lens' (DataPropLeaf a) (Maybe (Expression a))-propExpr2 f s = fmap (\x -> s { _propExpr2 = x}) (f (_propExpr2 s))- -- | A type for parsed ATS types data Type a = Tuple a [Type a]-            | BoxTuple a [Type a]+            | BoxTuple a (NonEmpty (Type a))             | Named (Name a)             | Ex (Existential a) (Maybe (Type a))             | ForA (Universal a) (Type a)             | Dependent { _typeCall :: Name a, _typeCallArgs :: [Type a] }             | Unconsumed (Type a) -- @!a@-            | AsProof (Type a) (Maybe (Type a)) -- @a >> b@+            | AsProof (Type a) (Maybe (Type a)) -- @a >> b@ If the second field is 'Nothing' this will print as @a >> _@.             | FromVT (Type a) -- | @a?!@             | MaybeVal (Type a) -- | @a?@             | AtExpr a (Type a) (StaticExpression a)             | AtType a (Type a)-            | ProofType a [Type a] (Type a) -- Aka (prf | val)+            | ProofType a (NonEmpty (Type a)) (Type a) -- Aka (prf | val)             | ConcreteType (StaticExpression a)             | RefType (Type a)             | ViewType a (Type a)@@ -223,7 +159,7 @@             deriving (Show, Eq, Generic, NFData)  data TypeF a x = TupleF a [x]-               | BoxTupleF a [x]+               | BoxTupleF a (NonEmpty x)                | NamedF (Name a)                | ExF (Existential a) (Maybe x)                | ForAF (Universal a) x@@ -234,7 +170,7 @@                | MaybeValF x                | AtExprF a x (StaticExpression a)                | AtTypeF a x-               | ProofTypeF a [x] x+               | ProofTypeF a (NonEmpty x) x                | ConcreteTypeF (StaticExpression a)                | RefTypeF x                | ViewTypeF a x@@ -274,20 +210,12 @@     project (ParenType l ty)           = ParenTypeF l ty     project (WhereType l ty s sas ty') = WhereTypeF l ty s sas ty' -typeCall :: Traversal' (Type a) (Name a)-typeCall f (Dependent x y) = (\x' -> Dependent x' y) <$> f x-typeCall _ x               = pure x--typeCallArgs :: Traversal' (Type a) [Type a]-typeCallArgs f (Dependent x y) = (\y' -> Dependent x y') <$> f y-typeCallArgs _ x               = pure x- -- | A type for @=>@, @=\<cloref1>@, etc. data LambdaType a = Plain a                   | Spear a -- | @=>>@                   | ProofArrow a -- | @=/=>@+                  | ProofSpear a -- | @=/=>>@                   | Full a String-                  -- TODO figure out wtf ProofArrow does                   deriving (Show, Eq, Generic, NFData)  data Name a = Unqualified String@@ -357,7 +285,6 @@ -- | An argument to a function. data Arg a = Arg (Paired String (Type a))            | PrfArg [Arg a] (Arg a)-           | NoArgs            deriving (Show, Eq, Generic, NFData)  -- | A datatype for sorts.@@ -393,7 +320,6 @@     project (TupleSort x s s') = TupleSortF x s s'     project (ArrowSort x s s') = ArrowSortF x s s' --- FIXME a type for sorts? -- | Wrapper for universal quantifiers (refinement types) data Universal a = Universal { bound :: [String], typeU :: Maybe (Sort a), prop :: [StaticExpression a] }     deriving (Show, Eq, Generic, NFData)@@ -492,7 +418,7 @@                   | UnderscoreLit a                   | Lambda a (LambdaType a) (Pattern a) (Expression a)                   | LinearLambda a (LambdaType a) (Pattern a) (Expression a)-                  | Index a (Name a) (Expression a)+                  | Index a (Name a) (Expression a) -- ^ E.g. @array[0]@.                   | Access a (Expression a) (Name a)                   | StringLit String                   | CharLit Char@@ -510,13 +436,13 @@                          }                   | RecordValue a [(String, Expression a)] (Maybe (Type a))                   | Precede (Expression a) (Expression a)-                  | ProofExpr a (Expression a) (Expression a)+                  | ProofExpr a (NonEmpty (Expression a)) (Expression a)                   | TypeSignature (Expression a) (Type a)                   | WhereExp (Expression a) (ATS a)-                  | TupleEx a [Expression a]-                  | BoxTupleEx a [Expression a]+                  | TupleEx a (NonEmpty (Expression a))+                  | BoxTupleEx a (NonEmpty (Expression a))                   | While a (Expression a) (Expression a)-                  | WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) (Maybe [Arg a]) -- ^ A @while@ loop that is guaranteed to terminate.+                  | WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) (Args a) -- ^ A @while@ loop that is guaranteed to terminate.                   | For a (Expression a) (Expression a)                   | ForStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) -- ^ A @for@ loop that is guaranteed to terminate.                   | Actions (ATS a)@@ -555,13 +481,13 @@                      | CaseF a Addendum x [(Pattern a, LambdaType a, x)]                      | RecordValueF a [(String, x)] (Maybe (Type a))                      | PrecedeF x x-                     | ProofExprF a x x+                     | ProofExprF a (NonEmpty x) x                      | TypeSignatureF x (Type a)                      | WhereExpF x (ATS a)-                     | TupleExF a [x]-                     | BoxTupleExF a [x]+                     | TupleExF a (NonEmpty x)+                     | BoxTupleExF a (NonEmpty x)                      | WhileF a x x-                     | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x (Maybe [Arg a])+                     | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x (Args a)                      | ForF a x x                      | ForStarF a [Universal a] (StaticExpression a) [Arg a] x x                      | ActionsF (ATS a)@@ -673,14 +599,11 @@                                   , implicits      :: [[Type a]] -- ^ Implicit arguments                                   , universalsI    :: [Universal a] -- ^ Universal quantifiers                                   , nameI          :: Name a -- ^ ('Name' a) of the template being implemented-                                  , iArgs          :: [Arg a] -- ^ Arguments+                                  , iArgs          :: Args a -- ^ Arguments                                   , _iExpression   :: Either (StaticExpression a) (Expression a) -- ^ Expression (or static expression) holding the function body.                                   }     deriving (Show, Eq, Generic, NFData) -iExpression :: Lens' (Implementation a) (Either (StaticExpression a) (Expression a))-iExpression f s = fmap (\x -> s { _iExpression = x}) (f (_iExpression s))- -- | A function declaration accounting for all keywords ATS uses to -- define them. data Function a = Fun { _preF :: PreFunction a }@@ -693,9 +616,6 @@                 | CastFn { _preF :: PreFunction a }                 deriving (Show, Eq, Generic, NFData) -preF :: Lens' (Function a) (PreFunction a)-preF f s = fmap (\x -> s { _preF = x}) (f (_preF s))- -- | A type for stack-allocated functions. See -- [here](http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c1267.html) -- for more.@@ -710,109 +630,15 @@                           , sig           :: Maybe String -- ^ e.g. <> or \<!wrt>                           , preUniversals :: [Universal a] -- ^ Universal quantifiers making a function generic                           , universals    :: [Universal a] -- ^ (Universal a) quantifiers/refinement type-                          , args          :: [Arg a] -- ^ Actual function arguments+                          , args          :: Args a -- ^ Actual function arguments                           , returnType    :: Maybe (Type a) -- ^ Return type                           , termetric     :: Maybe (StaticExpression a) -- ^ Optional termination metric                           , _expression   :: Maybe (Expression a) -- ^ Expression holding the actual function body (not present in static templates)                           }                           deriving (Show, Eq, Generic, NFData) --- TODO lens/base functor module?-expression :: Lens' (PreFunction a) (Maybe (Expression a))-expression f s = fmap (\x -> s { _expression = x}) (f (_expression s))--exprLens :: Eq a => FixityState a -> ASetter s t (Expression a) (Expression a) -> s -> t-exprLens st = flip over (rewriteATS st)--exprLenses :: Eq a => FixityState a -> [ASetter b b (Expression a) (Expression a)] -> b -> b-exprLenses st = thread . fmap (exprLens st)--rewriteDecl :: Eq a => FixityState a -> Declaration a -> Declaration a-rewriteDecl st (Extern l d) = Extern l (rewriteDecl st d)-rewriteDecl st x@Val{} = exprLens st valExpression x-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._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-    where g = over (leaves.mapped.constructorUniversals) h-          h :: Eq a => [Universal a] -> [Universal a]-          h = ana c where-            c (y:y':ys)-                | typeU y == typeU y' && isJust (typeU y) =-                    Cons (Universal (bound y ++ bound y') (typeU y) (StaticBinary LogicalAnd <$> prop y <*> prop y')) ys-            c y = project y-rewriteDecl _ x = x- -- FIXME left vs. right shouldn't be treated the same instance (Eq a) => Ord (Fixity a) where     compare = on compare ifix -leftFix :: Int -> Fixity a-leftFix = LeftFix undefined . Left--rightFix :: Int -> Fixity a-rightFix = RightFix undefined . Left--infix_ :: Int -> Fixity a-infix_ = Infix undefined . Left- type FixityState a = M.Map String (Fixity a)---- | Fixities for operators in the ATS prelude.-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 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)---- | Among other things, this rewrites expressions so that operator precedence--- is respected; this ensures @1 + 2 * 3@ will be parsed as the correct--- expression.-rewriteATS :: Eq a => FixityState a -> Expression a -> Expression a-rewriteATS st = cata a where-    a (LetF loc (ATS ds) e')                         = Let loc (ATS (rewriteDecl st <$> ds)) e'-    a (CallF n ts ts' me [ParenExpr _ e@NamedVal{}]) = Call n ts ts' me [e]-    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)-    a (BinaryF Add e e')                             = BinList Add [e, e']-    a (BinaryF Con{} e (BinList Add es))             = BinList (SpecialInfix undefined "::") (e : es)-    a (BinaryF Con{} e e')                           = BinList (SpecialInfix undefined "::") [e, e']-    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

@@ -0,0 +1,93 @@+module Language.ATS.Types.Lens ( -- * Lenses+                                 iExpression+                               , constructorUniversals+                               , expression+                               , preF+                               , propExpr1+                               , propExpr2+                               -- * Traversals+                               , typeCall+                               , typeCallArgs+                               , fun+                               , impl+                               , valExpression+                               , prValExpr+                               , varExpr1+                               , varExpr2+                               , andExpr+                               , propLeaves+                               , leaves+                               , comment+                               ) where++import           Language.ATS.Types+import           Lens.Micro++constructorUniversals :: Lens' (Leaf a) [Universal a]+constructorUniversals f s = fmap (\x -> s { _constructorUniversals = x}) (f (_constructorUniversals s))++expression :: Lens' (PreFunction a) (Maybe (Expression a))+expression f s = fmap (\x -> s { _expression = x}) (f (_expression s))++preF :: Lens' (Function a) (PreFunction a)+preF f s = fmap (\x -> s { _preF = x}) (f (_preF s))++iExpression :: Lens' (Implementation a) (Either (StaticExpression a) (Expression a))+iExpression f s = fmap (\x -> s { _iExpression = x}) (f (_iExpression s))++propExpr1 :: Lens' (DataPropLeaf a) (Expression a)+propExpr1 f s = fmap (\x -> s { _propExpr1 = x}) (f (_propExpr1 s))++propExpr2 :: Lens' (DataPropLeaf a) (Maybe (Expression a))+propExpr2 f s = fmap (\x -> s { _propExpr2 = x}) (f (_propExpr2 s))+++typeCall :: Traversal' (Type a) (Name a)+typeCall f (Dependent x y) = (\x' -> Dependent x' y) <$> f x+typeCall _ x               = pure x++typeCallArgs :: Traversal' (Type a) [Type a]+typeCallArgs f (Dependent x y) = (\y' -> Dependent x y') <$> f y+typeCallArgs _ x               = pure x++fun :: Traversal' (Declaration a) (Function a)+fun f (Func x y) = Func x <$> f y+fun _ x          = pure x++impl :: Traversal' (Declaration a) (Implementation a)+impl f (Impl x y)      = Impl x <$> f y+impl f (ProofImpl x y) = ProofImpl x <$> f y+impl _ x               = pure x++valExpression :: Traversal' (Declaration a) (Expression a)+valExpression f (Val a v p e) = Val a v p <$> f e+valExpression _ x             = pure x++prValExpr :: Traversal' (Declaration a) (Maybe (Expression a))+prValExpr f (PrVal p me t) = (\me' -> PrVal p me' t) <$> f me+prValExpr _ x              = pure x++varExpr1 :: Traversal' (Declaration a) (Maybe (Expression a))+varExpr1 f (Var t p e e') = (\e'' -> Var t p e'' e') <$> f e+varExpr1 _ x              = pure x++varExpr2 :: Traversal' (Declaration a) (Maybe (Expression a))+varExpr2 f (Var t p e e') = (\e'' -> Var t p e e'') <$> f e'+varExpr2 _ x              = pure x++andExpr :: Traversal' (Declaration a) (Expression a)+andExpr f (AndDecl t p e) = AndDecl t p <$> f e+andExpr _ x               = pure x++propLeaves :: Traversal' (Declaration a) [DataPropLeaf a]+propLeaves f (DataProp l n as pl) = DataProp l n as <$> f pl+propLeaves _ x                    = pure x++leaves :: Traversal' (Declaration a) [Leaf a]+leaves f (SumType t as l)     = SumType t as <$> f l+leaves f (SumViewType t as l) = SumViewType t as <$> f l+leaves _ x                    = pure x++comment :: Traversal' (Declaration a) String+comment f (Comment c) = Comment <$> f c+comment _ x           = pure x

@@ -113,7 +113,7 @@   deqarray_make_cap(i2sz(cap))  implement {a} queue_free (que) =-  deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que))+  deqarray_free_nil($UN.castvwtp0{deqarray(a,1,0)}(que))  implement {a} channel_ref (chan) =   let