summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorvmchale <>2018-08-10 03:43:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-08-10 03:43:00 (GMT)
commit2d88079b52abc6edf70dfff5fd0b20751418fa2d (patch)
treed7aab7b58e5851c0f79f946f6504c21abdd217ae
parent25284c1ccd199b70f405c6e9df28755c1b74ea08 (diff)
version 1.6.0.01.6.0.0
-rw-r--r--CHANGELOG.md22
-rw-r--r--language-ats.cabal3
-rw-r--r--src/Language/ATS/Parser.y98
-rw-r--r--src/Language/ATS/PrettyPrint.hs48
-rw-r--r--src/Language/ATS/Types.hs35
-rw-r--r--test/data/list_append.dats47
-rw-r--r--test/data/list_append.out39
-rw-r--r--test/data/prf_sqrt2.dats130
-rw-r--r--test/data/prf_sqrt2.out101
-rw-r--r--test/data/stdlib/array.out1
-rw-r--r--test/data/stdlib/arrayref.out3
-rw-r--r--test/data/stdlib/basics_dyn.out5
-rw-r--r--test/data/stdlib/gorder.out1
-rw-r--r--test/data/stdlib/option_vt.out1
-rw-r--r--test/data/stdlib/unsafe.out2
15 files changed, 438 insertions, 98 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..d387917
--- /dev/null
+++ b/CHANGELOG.md
@@ -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.
diff --git a/language-ats.cabal b/language-ats.cabal
index 965f4a5..1488d75 100644
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -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 @@ data-files:
test/data/stdlib/*.sats
test/data/stdlib/*.out
extra-doc-files: README.md
+ CHANGELOG.md
source-repository head
type: darcs
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
index 5e53321..facf25a 100644
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -157,6 +157,7 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
closeParen { Special $$ ")" }
openParen { Special $$ "(" }
boxTuple { Special $$ "'(" }
+ boxRecord { Special $$ "'{" }
colon { SignatureTok $$ "" }
signature { SignatureTok _ $$ }
comma { Special $$ "," }
@@ -247,13 +248,18 @@ sep_by(p,sep) : p { $1 :| [] }
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 @@ TypeInExpr : comma_sep(alt(Type,ExprType)) { toList $1 }
-- | 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 @@ Type : Name parens(TypeInExpr) { Dependent $1 $2 }
| 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 @@ Type : Name parens(TypeInExpr) { Dependent $1 $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 }
| addr { AddrType $1 }
| doubleParens { Tuple $1 mempty }
| Type where IdentifierOr SortArgs eq Type { WhereType $2 $1 $3 $4 $6 }
@@ -323,7 +326,7 @@ TypeArg : IdentifierOr { Arg (First $1) }
| 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 @@ PatternIn : comma_sep(Pattern) { reverse (toList $1) }
-- | 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 @@ StaticCase : case_pattern(Pattern, StaticExpression) { $1 }
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 @@ LambdaArrow : plainArrow { Plain $1 }
-- | 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 @@ StaticExpression : Name { StaticVal $1 }
| 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 @@ PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqua
| 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 @@ Existential : lsqbracket QuantifierArgs colon Sort vbar StaticExpression rsqbrac
| 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 @@ OptExpression : { Nothing }
| 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 @@ SortArg : IdentifierOr colon Sort { [ SortArg $1 $3 ] }
| Sort { [Anonymous $1] }
| SortArg Comment { $1 }
-SortArgs : openParen SortArg closeParen { Just $2 }
+SortArgs : parens(SortArg) { Just $1 }
| doubleParens { Just [] }
| { Nothing }
@@ -809,7 +813,7 @@ TypeDecl : typedef IdentifierOr SortArgs eq Type MaybeAnnot { TypeDef $1 $2 $3 $
| 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 @@ TypeDecl : typedef IdentifierOr SortArgs eq Type MaybeAnnot { TypeDef $1 $2 $3 $
| 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 @@ StackFunction : parens(Args) Signature Type plainArrow Expression { StackF $2 $1
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 @@ Load : staload { (True, $1) }
| dynload { (False, $1) }
MacroArgs : doubleParens { Just [] }
- | openParen IdentifiersIn closeParen { Just $2 }
+ | parens(IdentifiersIn) { Just $1 }
| { Nothing }
-- | Parse a declaration
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
index 501cffa..93c144d 100644
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -14,7 +14,7 @@ module Language.ATS.PrettyPrint ( printATS
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 @@ instance Eq a => Pretty (Expression a) where
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 @@ instance Eq a => Pretty (Expression a) where
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 @@ patternHelper ps = mconcat (punctuate ", " ps)
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 :: Maybe Doc -> Doc
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 @@ instance Eq a => Pretty (StaticExpression a) where
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 @@ instance Eq a => Pretty (Type a) where
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 @@ instance Eq a => Pretty (Implementation a) where
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`)
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
index 299dc4c..0d0beb8 100644
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -153,7 +153,6 @@ data Type a = Tuple a [Type a]
| 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 @@ data TypeF a x = TupleF a [x]
| 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 @@ instance Recursive (Type a) where
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 @@ data Name a = Unqualified String
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 @@ data Pattern a = Wildcard a
| 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 @@ data PatternF a x = WildcardF a
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 @@ data StaticExpression a = StaticVal (Name a)
| 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 @@ data StaticExpressionF a x = StaticValF (Name a)
| 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 @@ instance Recursive (StaticExpression a) where
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 @@ data Expression a = Let a (ATS a) (Maybe (Expression a))
, 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 Expression a = Let a (ATS a) (Maybe (Expression a))
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 @@ data ExpressionF a x = LetF a (ATS a) (Maybe x)
| 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 @@ instance Recursive (Expression a) where
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 @@ instance Corecursive (Expression a) where
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
diff --git a/test/data/list_append.dats b/test/data/list_append.dats
new file mode 100644
index 0000000..549a09f
--- /dev/null
+++ b/test/data/list_append.dats
@@ -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]
diff --git a/test/data/list_append.out b/test/data/list_append.out
new file mode 100644
index 0000000..c4fba82
--- /dev/null
+++ b/test/data/list_append.out
@@ -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]
diff --git a/test/data/prf_sqrt2.dats b/test/data/prf_sqrt2.dats
new file mode 100644
index 0000000..d64a593
--- /dev/null
+++ b/test/data/prf_sqrt2.dats
@@ -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] *)
diff --git a/test/data/prf_sqrt2.out b/test/data/prf_sqrt2.out
new file mode 100644
index 0000000..3d0482f
--- /dev/null
+++ b/test/data/prf_sqrt2.out
@@ -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] *)
diff --git a/test/data/stdlib/array.out b/test/data/stdlib/array.out
index 2f5f28a..128a1a5 100644
--- a/test/data/stdlib/array.out
+++ b/test/data/stdlib/array.out
@@ -321,7 +321,6 @@ macdef array2list = array_copy_to_list_vt
//
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))
diff --git a/test/data/stdlib/arrayref.out b/test/data/stdlib/arrayref.out
index a9a7a78..3d17ebd 100644
--- a/test/data/stdlib/arrayref.out
+++ b/test/data/stdlib/arrayref.out
@@ -140,7 +140,6 @@ fun {a:t0p} arrayref_make_rlist {n:int} ( asz : int(n)
//
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} arrayref_tail {n:pos} (A : arrayref(a, n)) :<!ref>
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
diff --git a/test/data/stdlib/basics_dyn.out b/test/data/stdlib/basics_dyn.out
index a6b4210..19d26f4 100644
--- a/test/data/stdlib/basics_dyn.out
+++ b/test/data/stdlib/basics_dyn.out
@@ -218,10 +218,8 @@ overload free with cloptr_free of 0
//
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} box_vt : (INV(a)) -> boxed_vt(a)
fun {a:vtype} unbox_vt : boxed_vt(INV(a)) -> (a)
-//
(* ****** ****** *)
//
stadef array (a: vt@ype, n: int) = @[a][n]
@@ -562,7 +559,6 @@ praxi opt_unsome {a:vt0p} (x : !opt(INV(a), true) >> a) :<prf> void
//
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 @@ dataview or_view_view_int_view(a0: view+, a1: view+, int) =
| 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
diff --git a/test/data/stdlib/gorder.out b/test/data/stdlib/gorder.out
index 77a27fe..4cfcc26 100644
--- a/test/data/stdlib/gorder.out
+++ b/test/data/stdlib/gorder.out
@@ -110,7 +110,6 @@ fun {a:t0p} gmax_val_val (x : a, y : a) :<> (a)
fun {a:t0p} gmin_val_val (x : a, y : a) :<> (a)
-//
(* ****** ****** *)
//
fun {a:vt0p} glt_ref_ref (x : &INV(a), y : &a) :<> bool
diff --git a/test/data/stdlib/option_vt.out b/test/data/stdlib/option_vt.out
index 564de62..c8320e7 100644
--- a/test/data/stdlib/option_vt.out
+++ b/test/data/stdlib/option_vt.out
@@ -71,7 +71,6 @@ fun option_vt_is_none {a:vt0p}{b:bool} (opt : !option_vt(INV(a), b)) :<>
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
diff --git a/test/data/stdlib/unsafe.out b/test/data/stdlib/unsafe.out
index 68ca3c4..0d74924 100644
--- a/test/data/stdlib/unsafe.out
+++ b/test/data/stdlib/unsafe.out
@@ -199,7 +199,6 @@ fun {a:vt0p} ptr0_get (p : ptr) :<> (a)
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} ptr0_getinc (p : &ptr >> _) : (a)
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))