language-ats 1.5.0.0 → 1.6.0.0
raw patch · 15 files changed
+438/−98 lines, 15 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
- Language.ATS: ParenType :: a -> (Type a) -> Type a
- Language.ATS: Wildcard :: a -> Pattern a
+ Language.ATS: BoxRecordValue :: a -> (NonEmpty (String, Expression a)) -> Expression a
+ Language.ATS: Witness :: a -> (StaticExpression a) -> (StaticExpression a) -> StaticExpression a
- Language.ATS: Call :: Name a -> [[Type a]] -> [Type a] -> Maybe [Expression a] -> [Expression a] -> Expression a
+ Language.ATS: Call :: Name a -> [[Type a]] -> [[Type a]] -> Maybe [Expression a] -> [Expression a] -> Expression a
- Language.ATS: RecordValue :: a -> (NonEmpty (String, Expression a)) -> (Maybe (Type a)) -> Expression a
+ Language.ATS: RecordValue :: a -> (NonEmpty (String, Expression a)) -> Expression a
- Language.ATS: SCall :: (Name a) -> [StaticExpression a] -> StaticExpression a
+ Language.ATS: SCall :: (Name a) -> [[Type a]] -> [StaticExpression a] -> StaticExpression a
- Language.ATS: [$sel:callUniversals:Let] :: Expression a -> [Type a]
+ Language.ATS: [$sel:callUniversals:Let] :: Expression a -> [[Type a]]
Files
- CHANGELOG.md +22/−0
- language-ats.cabal +2/−1
- src/Language/ATS/Parser.y +51/−47
- src/Language/ATS/PrettyPrint.hs +28/−20
- src/Language/ATS/Types.hs +18/−17
- test/data/list_append.dats +47/−0
- test/data/list_append.out +39/−0
- test/data/prf_sqrt2.dats +130/−0
- test/data/prf_sqrt2.out +101/−0
- test/data/stdlib/array.out +0/−1
- test/data/stdlib/arrayref.out +0/−3
- test/data/stdlib/basics_dyn.out +0/−5
- test/data/stdlib/gorder.out +0/−1
- test/data/stdlib/option_vt.out +0/−1
- test/data/stdlib/unsafe.out +0/−2
+ CHANGELOG.md view
@@ -0,0 +1,22 @@+# language-ats ++## 1.6.0.0++Breaking Changes:++ * Remove types for `RecordValues` and instead rely on typed expressions.+ * Remove `Wildcard` constructor and instead treat `_` as a name+ * Remove `ParenType` and instead use tuples++Enhancements:++ * Better Error messages+ * Add support for boxed records+ * Add support for proof expressions introducing witnesses (`[ m | [] ]`)++Bug Fixes:++ * Fix bug with formatting for type arguments+ * Fix formatting for `val ... and ...` declarations+ * Fix parse error on expressions like `list_vt_cons(x, _)`+ * Add support for patterns using binary operators.
language-ats.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.18 name: language-ats-version: 1.5.0.0+version: 1.6.0.0 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018 Vanessa McHale@@ -19,6 +19,7 @@ test/data/stdlib/*.sats test/data/stdlib/*.out extra-doc-files: README.md+ CHANGELOG.md source-repository head type: darcs
src/Language/ATS/Parser.y view
@@ -157,6 +157,7 @@ closeParen { Special $$ ")" } openParen { Special $$ "(" } boxTuple { Special $$ "'(" }+ boxRecord { Special $$ "'{" } colon { SignatureTok $$ "" } signature { SignatureTok _ $$ } comma { Special $$ "," }@@ -247,13 +248,18 @@ comma_sep(p) : sep_by(p, comma) { $1 } -between(p1,p,p2) : p1 p p2 { $2 }+parens(p) : openParen p closeParen { $2 } -parens(p) : between(openParen, p, closeParen) { $1 }+sqbrackets(p) : lsqbracket p rsqbracket { $2 } +braces(p) : lbrace p rbrace { $2 }+ alt(p,q) : p { $1 } | q { $1 } +optional(p) : p { Just $1 }+ | { Nothing }+ ATS : Declarations { ATS (reverse $1) } -- | Parse declarations in a list@@ -272,7 +278,7 @@ -- | Parse a type Type : Name parens(TypeInExpr) { Dependent $1 $2 } | Name doubleParens { Dependent $1 [] }- | identifierSpace openParen TypeInExpr closeParen { Dependent (Unqualified $ to_string $1) $3 }+ | identifierSpace parens(TypeInExpr) { Dependent (Unqualified $ to_string $1) $2 } | identifierSpace { Named (Unqualified $ to_string $1) } | specialIdentifier string { Dependent (SpecialName (token_posn $1) (to_string $1)) [Named (Unqualified $ $2)] } | Name { Named $1 }@@ -284,14 +290,12 @@ | Name maybeProof { MaybeVal (Named $1) } | Type fromVT { FromVT $1 } | Type prfTransform Type { AsProof $1 (Just $3) }- | Type prfTransform underscore { AsProof $1 Nothing } | view at Type { ViewType $1 $3 } | viewPlusMinus { ViewLiteral $1 }- | Existential Type { Ex $1 (Just $2) }- | Existential { Ex $1 Nothing }+ | Existential optional(Type) { Ex $1 $2 } | Universal Type { ForA $1 $2 } | Type at StaticExpression { AtExpr $2 $1 $3 }- | at lsqbracket Type rsqbracket lsqbracket StaticExpression rsqbracket { ArrayType $1 $3 $6 }+ | at sqbrackets(Type) sqbrackets(StaticExpression) { ArrayType $1 $2 $3 } | atbrace Records rbrace { AnonymousRecord $1 $2 } | openParen TypeIn vbar TypeIn closeParen { ProofType $1 $2 $4 } | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] }@@ -299,7 +303,6 @@ | 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 } | addr { AddrType $1 } | doubleParens { Tuple $1 mempty } | Type where IdentifierOr SortArgs eq Type { WhereType $2 $1 $3 $4 $6 }@@ -323,7 +326,7 @@ | exclamation IdentifierOr colon {% left $ OneOf $3 [",", ")"] ":" } Arg : TypeArg { $1 }- | StaticExpression { Arg (Second (ConcreteType $1)) } -- TODO: have some sort of stop showing bound variables that we can use to disambiguate types vs. static expressions?+ | StaticExpression { Arg (Second (ConcreteType $1)) } -- TODO: have some sort of state showing bound variables that we can use to disambiguate types vs. static expressions? -- | Parse a literal Literal : uintLit { UintLit $1 }@@ -340,7 +343,6 @@ -- | Parse a pattern match Pattern : Name { PName $1 [] } | identifierSpace { PName (Unqualified $ to_string $1) [] }- | underscore { Wildcard $1 } | identifier doubleParens { PName (Unqualified (to_string $1 ++ "()")) [] } | tilde Pattern { Free $2 } | Name openParen PatternIn closeParen { PName $1 $3 }@@ -374,7 +376,7 @@ IfCase : case_pattern(Expression, Expression) { $1 } ExpressionPrf : ExpressionIn { (Nothing, $1) }- | ExpressionIn vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof?+ | ExpressionIn vbar ExpressionIn { (Just $1, $3) } -- | A list of comma-separated expressions ExpressionIn : comma_sep(Expression) { toList $1 }@@ -404,30 +406,29 @@ -- | 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 { 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?- | list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 }+ | Expression colon Type { TypeSignature $1 $3 }+ | list_vt braces(Type) parens(ExpressionIn) { ListLiteral $1 "vt" $2 $3 } | begin Expression extern {% left $ Expected $3 "end" "extern" } | Expression prfTransform underscore {% left $ Expected $2 "Rest of expression or declaration" ">>" } -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 TypeInExpr rbrace { $3 ++ $1 }+TypeArgs : braces(alt(Type,ExprType)) { [[$1]] }+ | braces(TypeInExpr) { [$1] }+ | TypeArgs braces(alt(Type,ExprType)) { [$2] : $1 }+ | braces(doubleDot) { [[ ImplicitType $1 ]] } -- FIXME only valid on function calls+ | TypeArgs braces(TypeInExpr) { [$2] ++ $1 } Call : Name doubleParens { Call $1 [] [] Nothing [] }- | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) }- | identifierSpace openParen ExpressionPrf closeParen { Call (Unqualified $ to_string $1) [] [] (fst $3) (snd $3) }- | Name TypeArgs openParen ExpressionPrf closeParen { Call $1 [] $2 (fst $4) (snd $4) }+ | Name parens(ExpressionPrf) { Call $1 [] [] (fst $2) (snd $2) }+ | identifierSpace parens(ExpressionPrf) { Call (Unqualified $ to_string $1) [] [] (fst $2) (snd $2) }+ | Name TypeArgs parens(ExpressionPrf) { Call $1 [] $2 (fst $3) (snd $3) } | Name TypeArgs doubleParens { Call $1 [] $2 Nothing [VoidLiteral $3] } | Name TypeArgs { Call $1 [] $2 Nothing [] } | Name Implicits doubleParens { Call $1 $2 [] Nothing [VoidLiteral $3] }- | Name Implicits openParen ExpressionPrf closeParen { Call $1 $2 [] (fst $4) (snd $4) }+ | Name Implicits parens(ExpressionPrf) { Call $1 $2 [] (fst $3) (snd $3) } | 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" }@@ -449,18 +450,20 @@ | doubleParens { StaticVoid $1 } | 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 }- | identifierSpace openParen StaticArgs closeParen { SCall (Unqualified $ to_string $1) $3 }+ | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [] [$2] }+ | Name parens(StaticArgs) { SCall $1 [] $2 }+ | identifierSpace parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] $2 } -- TODO: static tuple? | StaticExpression semicolon StaticExpression { SPrecede $1 $3 } | UnOp StaticExpression { SUnary $1 $2 }- | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] }- | identifier doubleParens { SCall (Unqualified $ to_string $1) [] }- | let StaticDecls comment_after(in) end { SLet $1 $2 Nothing }- | let StaticDecls in StaticExpression end { SLet $1 $2 (Just $4) }- | openParen StaticExpression closeParen { $2 }+ | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] [] }+ | identifier TypeArgs doubleParens { SCall (Unqualified $ to_string $1) $2 [] }+ | identifier doubleParens { SCall (Unqualified $ to_string $1) [] [] }+ | let StaticDecls comment_after(in) end { SLet $1 (reverse $2) Nothing }+ | let StaticDecls in StaticExpression end { SLet $1 (reverse $2) (Just $4) }+ | parens(StaticExpression) { $1 } | openParen lineComment StaticExpression closeParen { $3 } | case StaticExpression of StaticCase { SCase $1 $2 $4 }+ | openExistential StaticExpression vbar StaticExpression rsqbracket { Witness $1 $2 $4 } -- | Parse an expression that can be called without parentheses PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 }@@ -487,20 +490,20 @@ | llambda Pattern LambdaArrow Expression { LinearLambda $1 $3 $2 $4 } | addrAt PreExpression { AddrAt $1 $2 } | viewAt PreExpression { ViewAt $1 $2 }- | atbrace RecordVal rbrace { RecordValue $1 $2 Nothing }- | atbrace RecordVal rbrace colon Type { RecordValue $1 $2 (Just $5) }+ | atbrace RecordVal rbrace { RecordValue $1 $2 }+ | boxRecord RecordVal rbrace { RecordValue $1 $2 } | begin Expression end { Begin $1 $2 } | identifierSpace { NamedVal (Unqualified $ to_string $1) } | Name { NamedVal $1 }- | lbrace ATS rbrace { Actions $2 }- | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }- | for openParen PreExpression closeParen PreExpression { For $1 $3 $5 }- | whileStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $8 $9 Nothing }- | whileStar Universals Termetric openParen Args closeParen colon openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $5 $12 $13 (Just $9) }- | forStar Universals Termetric openParen Args closeParen plainArrow Expression Expression { ForStar $1 $2 (snd $3) $5 $8 $9 }+ | braces(ATS) { Actions $1 }+ | while parens(PreExpression) PreExpression { While $1 $2 $3 }+ | for parens(PreExpression) PreExpression { For $1 $2 $3 }+ | whileStar Universals Termetric parens(Args) plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $4 $6 $7 Nothing }+ | whileStar Universals Termetric parens(Args) colon openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $4 $10 $11 (Just $7) }+ | forStar Universals Termetric parens(Args) plainArrow Expression Expression { ForStar $1 $2 (snd $3) $4 $6 $7 } | lineComment PreExpression { CommentExpr (to_string $1) $2 }- | comma openParen identifier closeParen { MacroVar $1 (to_string $3) }- | PreExpression where lbrace ATS rbrace { WhereExp $1 $4 }+ | comma parens(identifier) { MacroVar $1 (to_string $2) }+ | PreExpression where braces(ATS) { WhereExp $1 $3 } | include {% left $ Expected $1 "Expression" "include" } | staload {% left $ Expected (token_posn $1) "Expression" "staload" } | overload {% left $ Expected $1 "Expression" "overload" }@@ -549,7 +552,7 @@ | lsqbracket QuantifierArgs colon Sort rsqbracket { Existential $2 False (Just $4) Nothing } | openExistential QuantifierArgs colon Sort rsqbracket { Existential $2 True (Just $4) Nothing } | openExistential QuantifierArgs colon Sort vbar StaticExpression rsqbracket { Existential $2 True (Just $4) (Just $6) }- | lsqbracket StaticExpression rsqbracket { Existential mempty False Nothing (Just $2) }+ | sqbrackets(StaticExpression) { Existential mempty False Nothing (Just $1) } Predicates : { [] } | StaticExpression { [$1] }@@ -673,6 +676,7 @@ | let {% left $ Expected $1 "=" "let" } | ifcase {% left $ Expected $1 "=" "ifcase" } | eq fun {% left $ Expected $2 "Expression" "=" }+ | eq fn {% left $ Expected $2 "Expression" "=" } | eq lineComment fun {% left $ Expected $3 "Expression" "=" } | lbrace {% left $ Expected $1 "Expression" "{" } @@ -784,7 +788,7 @@ | Sort { [Anonymous $1] } | SortArg Comment { $1 } -SortArgs : openParen SortArg closeParen { Just $2 }+SortArgs : parens(SortArg) { Just $1 } | doubleParens { Just [] } | { Nothing } @@ -809,7 +813,7 @@ | abstype IdentifierOr SortArgs MaybeType { AbsType $1 $2 $3 $4 } | absvtype IdentifierOr SortArgs MaybeType { AbsViewType $1 $2 $3 $4 } | dataprop IdentifierOr SortArgs eq DataPropLeaves { DataProp $1 $2 $3 $5 }- | absprop IdentifierOr openParen Args closeParen { AbsProp $1 $2 $4 }+ | absprop IdentifierOr parens(Args) { AbsProp $1 $2 $3 } | AndSort { $1 } | AndStadef { $1 } | SumDecl { $1 }@@ -822,7 +826,7 @@ | dataprop IdentifierOr SortArgs vbar {% left $ Expected $4 "=" "|" } EitherInt : intLit { Left $1 }- | openParen Operator closeParen { Right $2 }+ | parens(Operator) { Right $1 } Fixity : infixr EitherInt { RightFix $1 $2 } | infixl EitherInt { LeftFix $1 $2 }@@ -861,7 +865,7 @@ ValDecl : val Pattern colon Type eq PreExpression { [ Val (get_addendum $1) (Just $4) $2 $6 ] } | val Pattern eq Expression { [ Val (get_addendum $1) Nothing $2 $4 ] }- | ValDecl and Pattern eq Expression { Val None Nothing $3 $5 : $1 }+ | ValDecl and Pattern eq Expression { AndDecl Nothing $3 $5 : $1 } | extern ValDecl { over _head (Extern $1) $2 } | val Pattern eq colon {% left $ Expected $4 "Expression" ":" } @@ -899,7 +903,7 @@ | dynload { (False, $1) } MacroArgs : doubleParens { Just [] }- | openParen IdentifiersIn closeParen { Just $2 }+ | parens(IdentifiersIn) { Just $1 } | { Nothing } -- | Parse a declaration
src/Language/ATS/PrettyPrint.hs view
@@ -14,7 +14,7 @@ import Control.Composition hiding ((&)) import Data.Bool (bool)-import Data.Foldable (fold, toList)+import Data.Foldable (toList) import Data.Functor.Foldable (cata) import Data.List (isPrefixOf) import Data.List.NonEmpty (NonEmpty (..))@@ -144,22 +144,22 @@ 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 []) = pretty nam <> prettyTypes 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+ | startsParens x = pretty nam <> prettyTypes us <> pretty x+ a (CallF nam [] us e xs) = pretty nam <> prettyTypes 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 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+ | startsParens x = pretty nam <> prettyImplicits is <> prettyTypes us <> pretty x+ a (CallF nam is us e xs) = pretty nam <> prettyImplicits is <> prettyTypes 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 _) = "()"- a (RecordValueF _ es Nothing) = prettyRecord es- a (RecordValueF _ es (Just x)) = prettyRecord es <+> ":" <+> pretty x+ a (RecordValueF _ es) = prettyRecord es+ a (BoxRecordValueF _ es) = "'" <> prettyRecord es a (PrecedeF e e') = parens (e <+> ";" </> e') a (PrecedeListF es) = lineAlt (prettyArgsList "; " "(" ")" es) ("(" <> mconcat (punctuate " ; " es) <> ")") a (AccessF _ e n)@@ -195,8 +195,6 @@ a (MacroVarF _ s) = ",(" <> text s <> ")" a BinListF{} = undefined -- Shouldn't happen - prettyImplicits = fold . fmap (prettyArgsU "<" ">") . reverse- prettyIfCase [] = mempty prettyIfCase [(s, l, t)] = "|" <+> s <+> pretty l <+> t prettyIfCase ((s, l, t): xs) = prettyIfCase xs $$ "|" <+> s <+> pretty l <+> t@@ -214,7 +212,6 @@ instance Eq a => Pretty (Pattern a) where pretty = cata a where- a (WildcardF _) = "_" a (PSumF s x) = string s <+> x a (PLiteralF e) = pretty e a (PNameF s []) = pretty s@@ -254,6 +251,15 @@ endLet Nothing = "in end" endLet (Just d) = "in" <$> indent 2 d <$> "end" +prettyExtras :: Pretty a => Doc -> Doc -> [[a]] -> Doc+prettyExtras d1 d2 = foldMap (prettyArgsU d1 d2) . reverse++prettyTypes :: Pretty a => [[a]] -> Doc+prettyTypes = prettyExtras "{" "}"++prettyImplicits :: Pretty a => [[a]] -> Doc+prettyImplicits = prettyExtras "<" ">"+ instance Eq a => Pretty (StaticExpression a) where pretty = cata a where a (StaticValF n) = pretty n@@ -264,14 +270,16 @@ a (StaticHexF h) = text h 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 "," . fmap pretty $ cs))+ a (SCallF n [] cs) = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))+ a (SCallF n us cs) = pretty n <> prettyTypes us <> parens (mconcat (punctuate "," . fmap pretty $ cs)) a (SPrecedeF e e') = e <> ";" <+> e' a (SUnaryF op e) = pretty op <> e a (SLetF _ e e') = flatAlt- ("let" <$> indent 2 (pretty e) <$> endLet e')- ("let" <+> pretty e <$> endLet e')+ ("let" <$> indent 2 (concatSame e) <$> endLet e')+ ("let" <+> concatSame e <$> endLet e') a (SCaseF ad e sls) = "case" <> pretty ad <+> e <+> "of" <$> indent 2 (prettyCases sls) a (SStringF s) = text s+ a (WitnessF _ e e') = "#[" <+> e <+> "|" <+> e' <+> "]" instance Eq a => Pretty (Sort a) where pretty = cata a where@@ -313,7 +321,6 @@ a (ViewLiteralF c) = "view" <> pretty c a ImplicitTypeF{} = ".." a (AnonymousRecordF _ rs) = prettyRecord rs- a (ParenTypeF _ t) = parens t a (WhereTypeF _ t i sa t') = t <#> indent 2 ("where" </> pretty i <+> prettySortArgs sa <+> "=" <+> pretty t') a AddrTypeF{} = "addr" @@ -362,11 +369,12 @@ 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-isVal Var{} = True-isVal PrVal{} = True-isVal PrVar{} = True-isVal _ = False+isVal Val{} = True+isVal Var{} = True+isVal PrVal{} = True+isVal PrVar{} = True+isVal AndDecl{} = True+isVal _ = False notDefine :: String -> Bool notDefine = not . ("#define" `isPrefixOf`)
src/Language/ATS/Types.hs view
@@ -153,7 +153,6 @@ | ImplicitType a | ViewLiteral Addendum | AnonymousRecord a (NonEmpty (String, Type a))- | ParenType a (Type a) | WhereType a (Type a) String (SortArgs a) (Type a) | AddrType a -- ^ @addr@ deriving (Show, Eq, Generic, NFData)@@ -178,7 +177,6 @@ | ImplicitTypeF a | ViewLiteralF Addendum | AnonymousRecordF a (NonEmpty (String, x))- | ParenTypeF a x | WhereTypeF a x String (SortArgs a) x | AddrTypeF a deriving (Functor)@@ -206,7 +204,6 @@ project (ImplicitType l) = ImplicitTypeF l project (ViewLiteral a) = ViewLiteralF a project (AnonymousRecord l stys) = AnonymousRecordF l stys- project (ParenType l ty) = ParenTypeF l ty project (WhereType l ty s sas ty') = WhereTypeF l ty s sas ty' project (AddrType l) = AddrTypeF l @@ -226,8 +223,7 @@ deriving (Show, Eq, Generic, NFData) -- | A data type for patterns.-data Pattern a = Wildcard a- | PName (Name a) [Pattern a]+data Pattern a = PName (Name a) [Pattern a] | PSum String (Pattern a) | PLiteral (Expression a) | Guarded a (Expression a) (Pattern a)@@ -242,8 +238,7 @@ | BinPattern a (BinOp a) (Pattern a) (Pattern a) -- ^ For use with e.g. @::@. deriving (Show, Eq, Generic, NFData) -data PatternF a x = WildcardF a- | PNameF (Name a) [x]+data PatternF a x = PNameF (Name a) [x] | PSumF String x | PLiteralF (Expression a) | GuardedF a (Expression a) x@@ -261,7 +256,6 @@ type instance Base (Pattern a) = PatternF a instance Recursive (Pattern a) where- project (Wildcard a) = WildcardF a project (PName x ps) = PNameF x ps project (PSum x p) = PSumF x p project (PLiteral e) = PLiteralF e@@ -368,11 +362,12 @@ | SPrecede (StaticExpression a) (StaticExpression a) | StaticVoid a | Sif { scond :: StaticExpression a, whenTrue :: StaticExpression a, selseExpr :: StaticExpression a } -- Static if (for proofs)- | SCall (Name a) [StaticExpression a]+ | SCall (Name a) [[Type a]] [StaticExpression a] | SUnary (UnOp a) (StaticExpression a) | SLet a [Declaration a] (Maybe (StaticExpression a)) | SCase Addendum (StaticExpression a) [(Pattern a, LambdaType a, StaticExpression a)] | SString String -- ^ @ext#@+ | Witness a (StaticExpression a) (StaticExpression a) -- ^ @#[ m | () ]@ deriving (Show, Eq, Generic, NFData) data StaticExpressionF a x = StaticValF (Name a)@@ -382,11 +377,12 @@ | SPrecedeF x x | StaticVoidF a | SifF x x x- | SCallF (Name a) [x]+ | SCallF (Name a) [[Type a]] [x] | SUnaryF (UnOp a) x | SLetF a [Declaration a] (Maybe x) | SCaseF Addendum x [(Pattern a, LambdaType a, x)] | SStringF String+ | WitnessF a x x deriving (Functor) type instance Base (StaticExpression a) = StaticExpressionF a@@ -399,18 +395,19 @@ project (SPrecede x x') = SPrecedeF x x' project (StaticVoid x) = StaticVoidF x project (Sif e e' e'') = SifF e e' e''- project (SCall n es) = SCallF n es+ project (SCall n ts es) = SCallF n ts es project (SUnary u x) = SUnaryF u x project (SLet x ds e) = SLetF x ds e project (SCase a x ples) = SCaseF a x ples project (SString s) = SStringF s+ project (Witness a e e') = WitnessF a e e' -- | A (possibly effectful) expression. 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}@+ , 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. }@@ -443,7 +440,8 @@ , val :: Expression a , _arms :: [(Pattern a, LambdaType a, Expression a)] -- ^ Each (('Pattern' a), ('Expression' a)) pair corresponds to a branch of the 'case' statement }- | RecordValue a (NonEmpty (String, Expression a)) (Maybe (Type a))+ | RecordValue a (NonEmpty (String, Expression a))+ | BoxRecordValue a (NonEmpty (String, Expression a)) | Precede (Expression a) (Expression a) | ProofExpr a (NonEmpty (Expression a)) (Expression a) | TypeSignature (Expression a) (Type a)@@ -467,7 +465,7 @@ data ExpressionF a x = LetF a (ATS a) (Maybe x) | VoidLiteralF a- | CallF (Name a) [[Type a]] [Type a] (Maybe [x]) [x]+ | CallF (Name a) [[Type a]] [[Type a]] (Maybe [x]) [x] | NamedValF (Name a) | ListLiteralF a String (Type a) [x] | IfF x x (Maybe x)@@ -488,7 +486,8 @@ | UnaryF (UnOp a) x | IfCaseF a [(x, LambdaType a, x)] | CaseF a Addendum x [(Pattern a, LambdaType a, x)]- | RecordValueF a (NonEmpty (String, x)) (Maybe (Type a))+ | RecordValueF a (NonEmpty (String, x))+ | BoxRecordValueF a (NonEmpty (String, x)) | PrecedeF x x | ProofExprF a (NonEmpty x) x | TypeSignatureF x (Type a)@@ -536,7 +535,8 @@ project (Unary op e) = UnaryF op e project (IfCase l arms) = IfCaseF l arms project (Case l k e arms) = CaseF l k e arms- project (RecordValue l recs mty) = RecordValueF l recs mty+ project (RecordValue l recs) = RecordValueF l recs+ project (BoxRecordValue l recs) = BoxRecordValueF l recs project (Precede e e') = PrecedeF e e' project (ProofExpr a e e') = ProofExprF a e e' project (TypeSignature e ty) = TypeSignatureF e ty@@ -581,7 +581,8 @@ embed (UnaryF op e) = Unary op e embed (IfCaseF l arms) = IfCase l arms embed (CaseF l k e arms) = Case l k e arms- embed (RecordValueF l recs mty) = RecordValue l recs mty+ embed (RecordValueF l recs) = RecordValue l recs+ embed (BoxRecordValueF l recs) = RecordValue l recs embed (PrecedeF e e') = Precede e e' embed (ProofExprF a e e') = ProofExpr a e e' embed (TypeSignatureF e ty) = TypeSignature e ty
+ test/data/list_append.dats view
@@ -0,0 +1,47 @@+fun+{a:t@ype}+list_append+ {m,n:nat} (+ xs: list (a, m)+, ys: list (a, n)+) : list (a, m+n) =+(+case+ xs of+| list_cons+ (x, xs) => list_cons (x, list_append (xs, ys))+| list_nil ((*void*)) => ys+) // end of [list_append]++fun+{a:t@ype}+list_append2+ {m,n:nat} (+ xs: list (a, m)+, ys: list (a, n)+) : list (a, m+n) = let+//+fun loop{m:nat}+(+ xs: list (a, m)+, ys: list (a, n)+, res: &ptr? >> list (a, m+n)+) : void =+(+case+ xs of+| list_cons+ (x, xs1) => let+ val () = res := list_cons{a}{0}(x, _)+ val+list_cons (_, res1) = res+ val () = loop (xs1, ys, res1) // of [xs1] and [ys]+ in+ fold@(res)+ end+| list_nil ((*void*)) => res := ys+)+//+var res: ptr+val () = loop (xs, ys, res)+//+in+ res+end // end of [list_append2]
+ test/data/list_append.out view
@@ -0,0 +1,39 @@+fun {a:t@ype} list_append { m, n : nat }( xs : list(a, m)+ , ys : list(a, n)+ ) : list(a, m+n) =+ (case+ xs of+ | list_cons (x, xs) => list_cons((x, list_append(xs, ys)))+ | list_nil () => ys)++// end of [list_append]+fun {a:t@ype} list_append2 { m, n : nat }( xs : list(a, m)+ , ys : list(a, n)+ ) : list(a, m+n) =+ let+ //+ fun loop {m:nat}( xs : list(a, m)+ , ys : list(a, n)+ , res : &ptr? >> list(a, m+n)+ ) : void =+ (case+ xs of+ | list_cons (x, xs1) => let+ val () = res := list_cons{a}{0}(x, _)+ val+ list_cons (_, res1) = res+ val () = loop((xs1, ys, res1))+ + // of [xs1] and [ys]+ in+ fold@(res)+ end+ | list_nil () => res := ys)+ + //+ var res: ptr+ val () = loop((xs, ys, res))+ + //+ in+ res+ end++// end of [list_append2]
+ test/data/prf_sqrt2.dats view
@@ -0,0 +1,130 @@+(*+** Some code used in the book INT2PROGINATS+*)++(* ****** ****** *)++abstype+MOD0(m: int, p: int) // m=p*q+ +(* ****** ****** *)+//+extern+prfun+lemma_MOD0_intr+ {m,p,q:nat | m==p*q}(): MOD0(m, p)+extern+prfun+lemma_MOD0_elim+ {m,p:int}+ (MOD0(m, p)): [q:nat] EQINT(m, p*q)+//+(* ****** ****** *)++abstype PRIME(p:int)++(* ****** ****** *)+//+extern+prfun+lemma_PRIME_param+ {p:int}(pf: PRIME(p)): [p >= 2] void+//+(* ****** ****** *)+//+extern+prfun+mylemma1{n,p:int}+ (MOD0(n*n, p), PRIME(p)): MOD0(n, p)+//+(* ****** ****** *)++extern+prfun+mylemma_main+{m,n,p:int | m*m==p*n*n}(PRIME(p)): [m2:nat | n*n==p*m2*m2] void++(* ****** ****** *)++extern+prfun+square_is_nat{m:int}(): [m*m>=0] void++(* ****** ****** *)++primplmnt+mylemma_main+{m,n,p}(pfprm) = let+ prval pfeq_mm_pnn =+ eqint_make{m*m,p*n*n}()+ prval () = square_is_nat{m}()+ prval () = square_is_nat{n}()+ prval () = lemma_PRIME_param(pfprm)+ prval+ pfmod1 =+ lemma_MOD0_intr{m*m,p,n*n}()+ prval+ pfmod2 = mylemma1{m,p}(pfmod1, pfprm)+ prval+ [m2:int]+ EQINT() =+ lemma_MOD0_elim(pfmod2)+ prval EQINT() = pfeq_mm_pnn+ prval () =+ __assert{p}{p*m2*m2,n*n}() where+ {+ extern prfun __assert{p:pos}{x,y:int | p*x==p*y}(): [x==y] void+ }+in+ 0+end // end of [mylemma_main]++(* ****** ****** *)+//+extern+prfun+sqrt2_irrat+{m,n:nat |+ n >= 1; m*m==2*n*n}((*void*)): [false] void+//+(* ****** ****** *)++primplmnt+sqrt2_irrat+ {m,n}((*void*)) = let+prfun+auxmain +{m,n:nat |+ n >= 1;+ m*m==2*n*n} .<m>.+(+// argless+) : [false] void = let+//+prval pfprm =+__assert() where+{+ extern praxi __assert(): PRIME(2)+}+prval+[m2:int] () = mylemma_main{m,n,2}(pfprm)+//+prval () =+__assert() where { extern praxi __assert(): [m > n] void }+prval () =+__assert() where { extern praxi __assert(): [m2 >= 1] void }+//+in+ auxmain{n,m2}()+end+in+ auxmain{m,n}()+end // end of [sqrt2_irrat]++(* ****** ****** *)++implement main0 () = ()++(* ****** ****** *)++(* end of [sqrt2_irrat.dats] *)
+ test/data/prf_sqrt2.out view
@@ -0,0 +1,101 @@+(*+** Some code used in the book INT2PROGINATS+*)+(* ****** ****** *)+abstype MOD0(m: int, p: int)++// m=p*q+(* ****** ****** *)+//+extern+prfun lemma_MOD0_intr { m, p, q : nat | m == p*q } () : MOD0(m, p)++extern+prfun lemma_MOD0_elim { m, p : int } (MOD0(m,p)) : [q:nat] EQINT(m, p*q)++//+(* ****** ****** *)+abstype PRIME(p: int)++(* ****** ****** *)+//+extern+prfun lemma_PRIME_param {p:int} (pf : PRIME(p)) : [p >= 2] void++//+(* ****** ****** *)+//+extern+prfun mylemma1 { n, p : int } (MOD0(n*n,p), PRIME(p)) : MOD0(n, p)++//+(* ****** ****** *)+extern+prfun mylemma_main { m, n, p : int | m*m == p*n*n } (PRIME(p)) :+ [ m2 : nat | n*n == p*m2*m2 ] void++(* ****** ****** *)+extern+prfun square_is_nat {m:int} () : [m*m >= 0] void++(* ****** ****** *)+primplmnt mylemma_main {m,n,p} (pfprm) =+ let+ prval pfeq_mm_pnn = eqint_make{m*m,p*n*n}()+ prval () = square_is_nat{m}()+ prval () = square_is_nat{n}()+ prval () = lemma_PRIME_param(pfprm)+ prval pfmod1 = lemma_MOD0_intr{m*m,p,n*n}()+ prval pfmod2 = mylemma1{m,p}(pfmod1, pfprm)+ prval [m2:int]EQINT() = lemma_MOD0_elim(pfmod2)+ prval EQINT() = pfeq_mm_pnn+ prval () = __assert{p}{p*m2*m2,n*n}() where+ { extern+ prfun __assert {p:pos}{ x, y : int | p*x == p*y } () : [x == y] void }+ in+ 0+ end++// end of [mylemma_main]+(* ****** ****** *)+//+extern+prfun sqrt2_irrat { m, n : nat | n >= 1; m*m == 2*n*n } () :+ [false] void++//+(* ****** ****** *)+primplmnt sqrt2_irrat {m,n} () =+ let+ prfun auxmain { m, n : nat | n >= 1; m*m == 2*n*n } .<m>. () :+ [false] void =+ let+ //+ prval pfprm = __assert() where+ { extern+ praxi __assert() : PRIME(2) }+ prval [m2:int]() = mylemma_main{m,n,2}(pfprm)+ + //+ prval () = __assert() where+ { extern+ praxi __assert() : [m > n] void }+ prval () = __assert() where+ { extern+ praxi __assert() : [m2 >= 1] void }+ + //+ in+ auxmain{n,m2}()+ end+ in+ auxmain{m,n}()+ end++// end of [sqrt2_irrat]+(* ****** ****** *)+implement main0 () =+ ()++(* ****** ****** *)+(* end of [sqrt2_irrat.dats] *)
test/data/stdlib/array.out view
@@ -321,7 +321,6 @@ // fun {a:vt0p} array_tabulate$fopr (i : size_t) : (a) -// fun {a:vt0p} array_ptr_tabulate {n:int} (asz : size_t(n)) : [l:addr] (array_v(a, l, n), mfree_gc_v(l)| ptr(l))
test/data/stdlib/arrayref.out view
@@ -140,7 +140,6 @@ // fun {a:t0p} arrayref_head {n:pos} (A : arrayref(a, n)) :<!ref> (a) -// A[0] fun {a:t0p} arrayref_tail {n:pos} (A : arrayref(a, n)) :<!ref> arrayref(a, n-1) @@ -150,12 +149,10 @@ fun {a:t0p}{tk:tk} arrayref_get_at_gint {n:int}{ i : nat | i < n } (A0 : arrayref(a, n), i : g1int(tk, i)) :<!ref> (a) -// arrayref_get_at_gint // fun {a:t0p}{tk:tk} arrayref_get_at_guint {n:int}{ i : nat | i < n } (A0 : arrayref(a, n), i : g1uint(tk, i)) :<!ref> (a) -// arrayref_get_at_guint // symintr arrayref_get_at
test/data/stdlib/basics_dyn.out view
@@ -218,10 +218,8 @@ // fun {a:t0p} lazy_force (lazyval : lazy(INV(a))) :<!laz> (a) -// fun {a:vt0p} lazy_vt_force (lazyval : lazy_vt(INV(a))) :<!all> (a) -// (* // // HX-2016-08:@@ -436,7 +434,6 @@ fun {a:vtype} unbox_vt : boxed_vt(INV(a)) -> (a) -// (* ****** ****** *) // stadef array (a: vt@ype, n: int) = @[a][n]@@ -562,7 +559,6 @@ // fun {a:vt0p} opt_unsome_get (x : &opt(INV(a), true) >> a?) : (a) -// praxi opt_none {a:vt0p} (x : !(a?) >> opt(a, false)) :<prf> void praxi opt_unnone {a:vt0p} (x : !opt(INV(a), false) >> a?) :<prf> void@@ -581,7 +577,6 @@ | VOR_l(a0, a1, 0) of (INV(a0)) | VOR_r(a0, a1, 1) of (INV(a1)) -// stadef por = or_prop_prop_int_prop stadef vor = or_view_view_int_view
test/data/stdlib/gorder.out view
@@ -110,7 +110,6 @@ fun {a:t0p} gmin_val_val (x : a, y : a) :<> (a) -// (* ****** ****** *) // fun {a:vt0p} glt_ref_ref (x : &INV(a), y : &a) :<> bool
test/data/stdlib/option_vt.out view
@@ -71,7 +71,6 @@ fun {a:vt0p} option_vt_unsome (opt : option_vt(INV(a), true)) :<!wrt> (a) -// fun {a:vt0p} option_vt_unnone (opt : option_vt(INV(a), false)) :<!wrt> void
test/data/stdlib/unsafe.out view
@@ -199,7 +199,6 @@ fun {a:vt0p} ptr1_get (p : Ptr1) :<> (a) -// fun {a:vt0p} ptr0_set (p : ptr, x : INV(a)) :<!wrt> void fun {a:vt0p} ptr1_set (p : Ptr1, x : INV(a)) :<!wrt> void@@ -222,7 +221,6 @@ fun {a:vt0p} ptr1_getinc {l:addr} (p : &ptr(l) >> ptr(l+sizeof(a))) : (a) -// fun {a:vt0p} ptr0_setinc (p : &ptr >> _, x : a) : void fun {a:vt0p} ptr1_setinc {l:addr} ( p : &ptr(l) >> ptr(l+sizeof(a))