release

ats-pkg/ats-pkg.cabal

@@ -1,6 +1,6 @@
 cabal-version: 2.0
 name: ats-pkg
-version: 3.2.1.1
+version: 3.2.1.2
 license: BSD3
 license-file: LICENSE
 copyright: Copyright: (c) 2018 Vanessa McHale

language-ats/CHANGELOG.md

@@ -2,17 +2,21 @@
 
 ## 1.6.0.0
 
+Breaking Changes:
+
   * Remove types for `RecordValues` and instead rely on typed expressions.
-  * Better Error messages
-  * Add support for boxed records
-  * Fix formatting for `val ... and ...` declarations
-  * Fix parse error on expressions like `list_vt_cons(x, _)`
-  * Add support for proof expressions introducing witnesses (`[ m | [] ]`)
   * Remove `Wildcard` constructor and instead treat `_` as a name
   * Remove `ParenType` and instead use tuples
 
-## 1.5.0.0
+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/src/Language/ATS/Parser.y

@@ -415,11 +415,11 @@ Expression : identifierSpace PreExpression { Call (Unqualified $ to_string $1) [
            | begin Expression extern {% left $ Expected $3 "end" "extern" }
            | Expression prfTransform underscore {% left $ Expected $2 "Rest of expression or declaration" ">>" }
 
-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 }
+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 parens(ExpressionPrf) { Call $1 [] [] (fst $2) (snd $2) }

language-ats/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,17 +144,17 @@ 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 _)              = "()"
@@ -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
@@ -253,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,7 +271,7 @@ instance Eq a => Pretty (StaticExpression a) where
         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 us cs)          = pretty n <> prettyArgsU "{" "}" us <> 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

language-ats/src/Language/ATS/Types.hs

@@ -362,7 +362,7 @@ 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) [Type 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)]
@@ -377,7 +377,7 @@ data StaticExpressionF a x = StaticValF (Name a)
                            | SPrecedeF x x
                            | StaticVoidF a
                            | SifF x x x
-                           | SCallF (Name a) [Type 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)]
@@ -407,7 +407,7 @@ 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.
                          }
@@ -465,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)

language-ats/test/data/list_append.out

@@ -17,7 +17,7 @@ fun {a:t@ype} list_append2 { m, n : nat }( xs : list(a, m)
                     ) : void =
       (case+ xs of
         | list_cons (x, xs1) => let
-          val () = res := list_cons{a,0}(x, _)
+          val () = res := list_cons{a}{0}(x, _)
           val+ list_cons (_, res1) = res
           val () = loop((xs1, ys, res1))
 

language-ats/test/data/prf_sqrt2.out

@@ -49,7 +49,7 @@ primplmnt mylemma_main {m,n,p} (pfprm) =
     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
+    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