language-ats 0.1.1.20 → 0.2.0.0

raw patch · 15 files changed

+142/−185 lines, 15 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• language-ats.cabal +1/−1
• src/Language/ATS.hs +2/−0
• src/Language/ATS/Lexer.x +4/−22
• src/Language/ATS/Parser.y +50/−45
• src/Language/ATS/PrettyPrint.hs +34/−43
• src/Language/ATS/Types.hs +25/−24
• test/data/cli.out +1/−1
• test/data/concurrency.out +13/−13
• test/data/fact.out +4/−0
• test/data/factorial.dats +1/−0
• test/data/factorial.out +1/−0
• test/data/left-pad.out +3/−3
• test/data/mydepies.out +0/−30
• test/data/number-theory.out +1/−1
• test/data/types.out +2/−2

@@ -1,5 +1,5 @@ name:                language-ats-version:             0.1.1.20+version:             0.2.0.0 synopsis:            Parser and pretty-printer for ATS. description:         Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex. license:             BSD3

@@ -31,6 +31,8 @@                     , StackFunction (..)                     , Paired (..)                     , Fixity (..)+                    , SortArg (..)+                    , Sort (..)                     -- * Lexical types                     , Token (..)                     , AlexPosn (..)

@@ -105,10 +105,10 @@ tokens :-      $white+                  ;-    ^ @block_comment         { tok (\p s -> CommentLex p s) }-    ^ "//".*                 { tok (\p s -> CommentLex p s) }-    "//".*                   ;-    @block_comment           ;+    @block_comment         { tok (\p s -> CommentLex p s) }+    "//".*                 { tok (\p s -> CommentLex p s) }+    -- "//".*                   ;+    -- @block_comment           ;     "#define".*              { tok (\p s -> MacroBlock p s) }           @if_block                { tok (\p s -> MacroBlock p s) }           @c_block                 { tok (\p s -> CBlockLex p s) }@@ -142,15 +142,10 @@     val"-"                   { tok (\p s -> Keyword p (KwVal Minus)) }     val                      { tok (\p s -> Keyword p (KwVal None)) }     var                      { tok (\p s -> Keyword p KwVar) }-    int                      { tok (\p s -> Keyword p KwInt) }     if                       { tok (\p s -> Keyword p KwIf) }     sif                      { tok (\p s -> Keyword p KwSif) }     then                     { tok (\p s -> Keyword p KwThen) }     else                     { tok (\p s -> Keyword p KwElse) }-    string                   { tok (\p s -> Keyword p KwString) }-    bool                     { tok (\p s -> Keyword p KwBool) }-    void                     { tok (\p s -> Keyword p KwVoid) }-    nat                      { tok (\p s -> Keyword p KwNat) }     implement                { tok (\p s -> Keyword p KwImplement) }     implmnt                  { tok (\p s -> Keyword p KwImplement) }     primplmnt                { tok (\p s -> Keyword p KwProofImplement) }@@ -185,7 +180,6 @@     begin                    { tok (\p s -> Keyword p KwBegin) }     overload                 { tok (\p s -> Keyword p KwOverload) }     with                     { tok (\p s -> Keyword p KwWith) }-    char                     { tok (\p s -> Keyword p KwChar) }     extern                   { tok (\p s -> Keyword p KwExtern) }     sortdef                  { tok (\p s -> Keyword p KwSortdef) }     propdef                  { tok (\p s -> Keyword p KwPropdef) }@@ -271,11 +265,6 @@              | KwSif              | KwThen              | KwElse-             | KwString-             | KwBool-             | KwInt-             | KwVoid-             | KwNat              | KwVal Addendum              | KwVar              | KwLambda@@ -293,7 +282,6 @@              | KwOverload              | KwWith              | KwIfCase-             | KwChar              | KwDataview              | KwDataprop              | KwView Addendum@@ -383,11 +371,6 @@     pretty KwSif = "sif"     pretty KwThen = "then"     pretty KwElse = "else"-    pretty KwString = "string"-    pretty KwBool = "bool"-    pretty KwInt = "int"-    pretty KwVoid = "void"-    pretty KwNat = "nat"     pretty (KwVal c) = "val" <> pretty c     pretty KwVar = "var"     pretty KwLambda = "lam"@@ -402,7 +385,6 @@     pretty KwWhile = "while"     pretty KwOverload = "overload"     pretty KwWith = "with"-    pretty KwChar = "char"     pretty KwDataview = "dataview"     pretty KwDataprop = "dataprop"     pretty (KwView c) = "view" <> pretty c

@@ -62,16 +62,10 @@     viewdef { Keyword $$ KwViewdef }     in { Keyword $$ KwIn }     end { Keyword $$ KwEnd }-    stringType { Keyword $$ KwString }-    charType { Keyword $$ KwChar }-    voidType { Keyword $$ KwVoid }     implement { Keyword $$ KwImplement }+    addr { Keyword $$ KwAddr }     primplmnt { Keyword $$ KwProofImplement }     else { Keyword $$ KwElse }-    bool { Keyword $$ KwBool }-    int { Keyword $$ KwInt }-    nat { Keyword $$ KwNat }-    addr { Keyword $$ KwAddr }     when { Keyword $$ KwWhen }     begin { Keyword $$ KwBegin }     case { Keyword _ (KwCase $$) }@@ -214,21 +208,6 @@ Type : Name openParen TypeInExpr closeParen { Dependent $1 $3 }      | Name doubleParens { Dependent $1 [] }      | identifierSpace openParen TypeInExpr closeParen { Dependent (Unqualified $ to_string $1) $3 }-     | bool { Bool }-     | int { Int }-     | nat { Nat }-     | addr { Addr }-     | stringType { String }-     | charType { Char }-     | voidType { Void }-     | t0pPlain { T0p None }-     | t0pCo { T0p Plus }-     | vt0pPlain { Vt0p None }-     | vt0pCo { Vt0p Plus }-     | stringType openParen StaticExpression closeParen { DepString $3 }-     | stringType StaticExpression { DepString $2 }-     | int openParen StaticExpression closeParen { DependentInt $3 }-     | bool openParen StaticExpression closeParen { DependentBool $3 }      | identifierSpace { Named (Unqualified $ to_string $1) }      | Name { Named $1 }      | exclamation Type { Unconsumed $2 }@@ -251,11 +230,11 @@      | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] }      | openParen TypeIn closeParen { Tuple $1 $2 }      | openParen Type closeParen { ParenType $1 $2 }-     | int StaticExpression { DependentInt $2 }      | doubleParens { NoneType $1 }      | minus {% Left $ Expected $1 "Type" "-" }      | dollar {% Left $ Expected $1 "Type" "$" }-     | int identifier openParen {% Left $ Expected (token_posn $2) "Static integer expression" (to_string $2) }+     | identifierSpace identifier openParen {% Left $ Expected (token_posn $2) "Static integer expression" (to_string $2) }+     | Type identifierSpace {% Left $ Expected (token_posn $2) "," (to_string $2) }  FullArgs : Args { $1 } @@ -264,6 +243,8 @@      | FullArgs comma Arg vbar Arg { PrfArg $3 $5 : $1 }      | Args comma Arg { $3 : $1 }      | Arg vbar Arg { [ PrfArg $1 $3 ] }+     | lineComment { [] }+     | Args lineComment { $1 }      | { [] }  TypeArg : identifier { Arg (First $ to_string $1) }@@ -433,6 +414,7 @@               | Name { NamedVal $1 }               | lbrace ATS rbrace { Actions $2 }               | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }+              | lineComment PreExpression { CommentExpr (to_string $1) $2 }               | include {% Left $ Expected $1 "Expression" "include" }               | staload {% Left $ Expected (token_posn $1) "Expression" "staload" }               | overload {% Left $ Expected $1 "Expression" "overload" }@@ -455,17 +437,28 @@           | underscore {% Left $ Expected $1 "_" "Termination metric" }           | dollar {% Left $ Expected $1 "$" "Termination metric" } --- | Parse an existential quantier on a type-Existential : lsqbracket Args vbar StaticExpression rsqbracket { Existential $2 False Nothing (Just $4) }-            | lsqbracket Args rsqbracket { Existential $2 False Nothing Nothing }-            | openExistential Args rsqbracket { Existential $2 True Nothing Nothing }-            | openExistential Args vbar StaticExpression rsqbracket { Existential $2 True Nothing (Just $4) }-            | lsqbracket Args colon Type rsqbracket { Existential $2 False (Just $4) Nothing } -- FIXME arguments should include more than just ':'-            | lsqbracket StaticExpression rsqbracket { Existential [] False Nothing (Just $2) }-            ++Sort : t0pPlain { T0p None }+     | t0pCo { T0p Plus }+     | vt0pPlain { Vt0p None }+     | vt0pCo { Vt0p Plus }+     | addr { Addr }+     | IdentifierOr { NamedSort $1 }++QuantifierArgs : IdentifierOr { [$1] }+               | QuantifierArgs comma IdentifierOr { $3 : $1 }++Existential : lsqbracket QuantifierArgs colon Sort vbar StaticExpression rsqbracket { Existential $2 False (Just $4) (Just $6) }+            | 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) }+ -- | Parse a universal quantifier on a type-Universal : lbrace Args rbrace { Universal $2 Nothing Nothing }-          | lbrace Args vbar StaticExpression rbrace { Universal $2 Nothing (Just $4) }+Universal : lbrace QuantifierArgs rbrace { Universal $2 Nothing Nothing }+          | lbrace QuantifierArgs vbar StaticExpression rbrace { Universal $2 Nothing (Just $4) }+          | lbrace QuantifierArgs colon Sort rbrace { Universal $2 (Just $4) Nothing }+          | lbrace QuantifierArgs colon Sort vbar StaticExpression rbrace { Universal $2 (Just $4) (Just $6) }  Implicits : lspecial TypeIn rbracket { [$2] }           | Implicits lspecial TypeIn rbracket { $3 : $1 }@@ -583,6 +576,8 @@ -- | Parse several constructors for a 'dataprop' DataPropLeaves : DataPropLeaf { [$1] }                | DataPropLeaves DataPropLeaf { $2 : $1 }+               | lineComment { [] }+               | DataPropLeaves lineComment { $1 }                | prval {% Left $ Expected $1 "Constructor" "prval" }                | var {% Left $ Expected $1 "Constructor" "var" }                | val {% Left $ Expected (token_posn $1) "Constructor" "val" }@@ -647,6 +642,7 @@         | fun fn {% Left $ Expected $2 "Function name" "fn" }         | fn fun {% Left $ Expected $2 "Function name" "fun" }         | extern FunDecl identifier openParen {% Left $ Expected (token_posn $3) "Static integer expression" (to_string $3) }+        | extern identifier {% Left $ Expected (token_posn $2) "Declaration" (to_string $2) }  IdentifierOr : identifier { to_string $1 }              | identifierSpace { to_string $1 }@@ -659,25 +655,33 @@         | openParen FullArgs closeParen { $2 }         | doubleParens { [] } +SortArg : IdentifierOr colon Sort { [ SortArg $1 $3 ] }+        | SortArg comma IdentifierOr colon Sort { SortArg $3 $5 : $1 }+        | SortArg comma IdentifierOr { Anonymous (NamedSort $3) : $1 }++SortArgs : openParen SortArg closeParen { Just $2 }+         | doubleParens { Just [] }+         | { Nothing }+ -- | Parse a declaration defining a type-TypeDecl : typedef IdentifierOr FunArgs eq Type { TypeDef $1 $2 $3 $5 }-         | vtypedef IdentifierOr FunArgs eq Type { ViewTypeDef $1 $2 $3 $5 }-         | datatype IdentifierOr FunArgs eq Leaves { SumType $2 $3 $5 }-         | datavtype IdentifierOr FunArgs eq Leaves { SumViewType $2 $3 $5 }+TypeDecl : typedef IdentifierOr SortArgs eq Type { TypeDef $1 $2 $3 $5 }+         | vtypedef IdentifierOr SortArgs eq Type { ViewTypeDef $1 $2 $3 $5 }+         | datatype IdentifierOr SortArgs eq Leaves { SumType $2 $3 $5 }+         | datavtype IdentifierOr SortArgs eq Leaves { SumViewType $2 $3 $5 }          | abst0p IdentifierOr eq Type { AbsT0p $1 $2 $4 }          | viewdef IdentifierOr openParen FullArgs closeParen eq Type { ViewDef $1 $2 $4 $7 }-         | absvt0p IdentifierOr FunArgs eq Type { AbsVT0p $1 $2 $3 (Just $5) }+         | absvt0p IdentifierOr SortArgs eq Type { AbsVT0p $1 $2 $3 (Just $5) }          | absview IdentifierOr openParen FullArgs closeParen MaybeType { AbsView $1 $2 $4 $6 }-         | abstype IdentifierOr FunArgs MaybeType { AbsType $1 $2 $3 $4 }-         | absvtype IdentifierOr FunArgs MaybeType { AbsViewType $1 $2 $3 $4 }+         | abstype IdentifierOr SortArgs MaybeType { AbsType $1 $2 $3 $4 }+         | absvtype IdentifierOr SortArgs MaybeType { AbsViewType $1 $2 $3 $4 }          | dataprop IdentifierOr openParen FullArgs closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 }          | absprop IdentifierOr openParen FullArgs closeParen { AbsProp $1 $2 $4 }          | AndSort { $1 }          | AndStadef { $1 }-         | vtypedef IdentifierOr FunArgs eq vbar {% Left $ Expected $5 "Viewtype" "|" }-         | typedef IdentifierOr FunArgs eq vbar {% Left $ Expected $5 "Type" "|" }-         | datavtype IdentifierOr FunArgs vbar {% Left $ Expected $4 "=" "|" }-         | datatype IdentifierOr FunArgs vbar {% Left $ Expected $4 "=" "|" }+         | vtypedef IdentifierOr SortArgs eq vbar {% Left $ Expected $5 "Viewtype" "|" }+         | typedef IdentifierOr SortArgs eq vbar {% Left $ Expected $5 "Type" "|" }+         | datavtype IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }+         | datatype IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }  Fixity : infixr { RightFix $1 }        | infixl { LeftFix $1 }@@ -700,6 +704,7 @@         | val Pattern eq Expression { [ Val (get_addendum $1) Nothing $2 $4 ] }         | ValDecl and Pattern eq Expression { Val None Nothing $3 $5 : $1 }         | extern ValDecl { over _head (Extern $1) $2 }+        | val Pattern eq colon {% Left $ Expected $4 "Expression" ":" }  StaticDeclaration : prval Pattern eq Expression { PrVal $2 $4 }                   | praxi PreFunction { Func $1 (Praxi $2) }

@@ -193,6 +193,7 @@         a (AddrAtF _ e)                = "addr@" <> e         a (ViewAtF _ e)                = "view@" <> e         a (ListLiteralF _ s t es)      = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es+        a (CommentExprF c e) = text c <$> e         a BinListF{} = undefined -- Shouldn't happen         prettyImplicits = mconcat . fmap (prettyArgsU "<" ">") . reverse         prettyIfCase []              = mempty@@ -224,10 +225,6 @@         a (UniversalPatternF _ n us p) = text n <> prettyArgsU "" "" us <> p         a (ExistentialPatternF e p)    = pretty e <> p -singleArg :: Arg -> Doc-singleArg x@Arg{} = argHelper (<>) x-singleArg x       = pretty x- argHelper :: (Doc -> Doc -> Doc) -> Arg -> Doc argHelper _ (Arg (First s))   = pretty s argHelper _ (Arg (Second t))  = pretty t@@ -235,6 +232,10 @@ argHelper op (PrfArg a a')    = pretty a `op` "|" `op` pretty a' argHelper _ NoArgs            = undefined -- in theory we handle this elsewhere. +instance Pretty SortArg where+    pretty (SortArg n st) = text n <> ":" <+> pretty st+    pretty (Anonymous s)  = pretty s+ instance Pretty Arg where     pretty = argHelper (<+>) @@ -266,31 +267,23 @@             ("let" <$> indent 2 (pretty ((ATS . reverse) e)) <$> endLet e')             ("let" <+> pretty ((ATS . reverse) e) <$> endLet e') +instance Pretty Sort where+    pretty (T0p ad)      = "t@ype" <> pretty ad+    pretty (Vt0p ad)     = "vt@ype" <> pretty ad+    pretty (NamedSort s) = text s+    pretty Addr          = "addr"+ instance Pretty Type where     pretty = cata a where-        a IntF                    = "int"-        a StringF                 = "string"-        a BoolF                   = "bool"-        a VoidF                   = "void"-        a NatF                    = "nat"-        a AddrF                   = "addr"-        a CharF                   = "char"         a (NamedF n)              = pretty n         a (ExF e t)               = pretty e <+> t-        a (DependentIntF e)       = "int(" <> pretty e <> ")"-        a (DependentBoolF e)      = "bool(" <> pretty e <> ")"-        a (DepStringF e)          = "string(" <> pretty e <> ")"         a (DependentF n ts)       = pretty n <> parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))-        a DoubleF                 = "double"-        a FloatF                  = "float"         a (ForAF u t)             = pretty u <+> t         a (UnconsumedF t)         = "!" <> t         a (AsProofF t (Just t'))  = t <+> ">>" <+> t'         a (AsProofF t Nothing)    = t <+> ">> _"         a (FromVTF t)             = t <> "?!"         a (MaybeValF t)           = t <> "?"-        a (T0pF ad)               = "t@ype" <> pretty ad-        a (Vt0pF ad)              = "vt@ype" <> pretty ad         a (AtF _ (Just t) t')     = t <+> "@" <+> t'         a (AtF _ Nothing t)       = "@" <> t         a (ProofTypeF _ t t')     = parens (prettyArgsG "" "" t <+> "|" <+> t')@@ -305,7 +298,7 @@         a (AnonymousRecordF _ rs) = prettyRecord rs         a (ParenTypeF _ t)        = parens t -gan :: Maybe Type -> Doc+gan :: Maybe Sort -> Doc gan (Just t) = " : " <> pretty t <> " " gan Nothing  = "" @@ -314,24 +307,18 @@ withHashtag _    = lbracket  instance Pretty Existential where-    pretty (Existential [] b Nothing (Just e)) = withHashtag b <+> pretty e <+> rbracket-    pretty (Existential [x@Arg{}] b Nothing Nothing) = withHashtag b <> singleArg x <> rbracket-    pretty (Existential bs b ty Nothing)  = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbracket-    pretty (Existential bs b ty (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket-        where go (Arg (First s))  = pretty s-              go (Arg (Both s t)) = pretty s <+> colon <+> pretty t-              go (Arg (Second t)) = pretty t-              go _                = undefined -- Shouldn't happen+    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  instance Pretty Universal where-    pretty (Universal [x@PrfArg{}] Nothing Nothing) = lbrace <+> pretty x <+> rbrace -- FIXME universals can now be length-one arguments-    pretty (Universal [x] Nothing Nothing) = lbrace <> singleArg x <> rbrace -- FIXME universals can now be length-one arguments-    pretty (Universal bs ty Nothing) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <+> gan ty <> rbrace-    pretty (Universal bs ty (Just e)) = lbrace <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbrace-        where go (Arg (First s))  = pretty s-              go (Arg (Both s t)) = pretty s <+> colon <+> pretty t-              go (Arg (Second t)) = pretty t-              go _                = undefined+    pretty (Universal [x] Nothing Nothing) = lbrace <> text x <> rbrace+    pretty (Universal [x] (Just st) Nothing) = lbrace <> text x <> ":" <> pretty st <> rbrace+    pretty (Universal bs Nothing Nothing) = lbrace <> mconcat (punctuate "," (fmap pretty (reverse bs))) <> rbrace+    pretty (Universal bs (Just ty) Nothing) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <+> ":" <+> pretty ty <+> rbrace+    pretty (Universal bs ty (Just e)) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <> "|" <+> pretty e <+> rbrace  instance Pretty ATS where     pretty (ATS xs) = concatSame (fmap rewriteDecl xs)@@ -522,12 +509,16 @@ valSig :: (Pretty a) => Maybe a -> Doc valSig = prettySigG mempty mempty +prettySortArgs :: (Pretty a) => Maybe [a] -> Doc+prettySortArgs Nothing   = mempty+prettySortArgs (Just as) = prettyArgs' ", " "(" ")" as+ instance Pretty Declaration where-    pretty (AbsType _ s as t)              = "abstype" <+> text s <> prettyArgsNil as <> prettyMaybeType t-    pretty (AbsViewType _ s as Nothing)    = "absvtype" <+> text s <> prettyArgsNil as-    pretty (AbsViewType _ s as (Just t))   = "absvtype" <+> text s <> prettyArgsNil as <+> "=" <+> pretty t-    pretty (SumViewType s as ls)           = "datavtype" <+> text s <> prettyArgsNil as <+> "=" <$> prettyLeaf ls-    pretty (SumType s as ls)               = "datatype" <+> text s <> prettyArgsNil as <+> "=" <$> prettyLeaf ls+    pretty (AbsType _ s as t)              = "abstype" <+> text s <> prettySortArgs as <> prettyMaybeType t+    pretty (AbsViewType _ s as Nothing)    = "absvtype" <+> text s <> prettySortArgs as+    pretty (AbsViewType _ s as (Just t))   = "absvtype" <+> text s <> prettySortArgs as <+> "=" <+> pretty t+    pretty (SumViewType s as ls)           = "datavtype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls+    pretty (SumType s as ls)               = "datatype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls     pretty (Impl as i)                     = "implement" <+> prettyArgsNil as <> pretty i -- mconcat (fmap pretty us) <+> pretty i     pretty (ProofImpl as i)                = "primplmnt" <+> prettyArgsNil as <> pretty i     pretty (PrVal p e)                     = "prval" <+> pretty p <+> "=" <+> pretty e@@ -558,8 +549,8 @@     pretty (Func _ (PrFn pref))            = "prfn" </> pretty pref     pretty (Extern _ d)                    = "extern" <$> pretty d     pretty (DataProp _ s as ls)            = "dataprop" <+> text s <> prettyArgs as <+> "=" <$> prettyDL ls-    pretty (ViewTypeDef _ s as t)          = "vtypedef" <+> text s <> prettyArgsNil as <+> "=" <#> pretty t-    pretty (TypeDef _ s as t)              = "typedef" <+> text s <> prettyArgsNil as <+> "=" <+> pretty t+    pretty (ViewTypeDef _ s as t)          = "vtypedef" <+> text s <> prettySortArgs as <+> "=" <#> pretty t+    pretty (TypeDef _ s as t)              = "typedef" <+> text s <> prettySortArgs as <+> "=" <+> pretty t     pretty (AbsProp _ n as)                = "absprop" <+> text n <+> prettyArgs as     pretty (Assume n NoA e)                = "assume" </> pretty n <+> "=" </> pretty e     pretty (Assume n as e)                 = "assume" </> pretty n <> prettyArgs as <+> "=" </> pretty e@@ -576,7 +567,7 @@     pretty (AndD d (Stadef i n []))        = pretty d <+> "and" <+> text i <+> pretty n     pretty (AndD d (Stadef i n as))        = pretty d <+> "and" <+> text i <+> pretty n <> prettyArgs as     pretty (AbsView _ i as t)              = "absview" <+> text i <> prettyArgs as <> prettyMaybeType t-    pretty (AbsVT0p _ i as t)              = "absvt@ype" <+> text i <> prettyArgs as <> prettyMaybeType t+    pretty (AbsVT0p _ i as t)              = "absvt@ype" <+> text i <> prettySortArgs as <> prettyMaybeType t     pretty (AbsT0p _ i t)                  = "abst@ype" <+> text i <+> "=" <+> pretty t     pretty (ViewDef _ s [] t)              = "viewdef" <+> text s <+> "=" <#> pretty t     pretty (ViewDef _ s as t)              = "viewdef" <+> text s <> prettyArgs as <+> "=" <#> pretty t

@@ -41,6 +41,8 @@     , StaticExpressionF (..)     , Fixity (..)     , StackFunction (..)+    , Sort (..)+    , SortArg (..)     , rewriteATS     , rewriteDecl     -- * Lenses@@ -86,14 +88,14 @@                  | Staload Bool (Maybe String) String                  | Stadef String Name [Type]                  | CBlock String-                 | TypeDef AlexPosn String [Arg] Type-                 | ViewTypeDef AlexPosn String [Arg] Type-                 | SumType { typeName :: String, typeArgs :: [Arg], _leaves :: [Leaf] }-                 | SumViewType { typeName :: String, typeArgs :: [Arg], _leaves :: [Leaf] }-                 | AbsType AlexPosn String [Arg] (Maybe Type)-                 | AbsViewType AlexPosn String [Arg] (Maybe Type)+                 | TypeDef AlexPosn String (Maybe [SortArg]) Type+                 | ViewTypeDef AlexPosn String (Maybe [SortArg]) Type+                 | SumType { typeName :: String, typeArgs :: Maybe [SortArg], _leaves :: [Leaf] }+                 | SumViewType { typeName :: String, typeArgs :: Maybe [SortArg], _leaves :: [Leaf] }+                 | AbsType AlexPosn String (Maybe [SortArg]) (Maybe Type)+                 | AbsViewType AlexPosn String (Maybe [SortArg]) (Maybe Type)                  | AbsView AlexPosn String [Arg] (Maybe Type)-                 | AbsVT0p AlexPosn String [Arg] (Maybe Type)+                 | AbsVT0p AlexPosn String (Maybe [SortArg]) (Maybe Type)                  | AbsT0p AlexPosn String Type                  | ViewDef AlexPosn String [Arg] Type                  | OverloadOp AlexPosn BinOp Name@@ -120,19 +122,7 @@                   deriving (Show, Eq, Generic, NFData)  -- | A type for parsed ATS types-data Type = Bool-          | Void-          | String-          | Char-          | Int-          | Nat-          | Addr-          | DependentInt StaticExpression-          | DependentBool StaticExpression-          | DepString StaticExpression-          | Double-          | Float-          | Tuple AlexPosn [Type]+data Type = Tuple AlexPosn [Type]           | Named Name           | Ex Existential Type           | ForA Universal Type@@ -141,8 +131,6 @@           | AsProof Type (Maybe Type) -- a >> b           | FromVT Type -- For a viewtype VT, we can prove there exist a view V and type T such that `VT` is equivalent to `(V | T)` - that T is `VT?!`           | MaybeVal Type -- This is just `a?` or the like-          | T0p Addendum -- t@ype-          | Vt0p Addendum -- vt@ype           | At AlexPosn (Maybe Type) Type           | ProofType AlexPosn [Type] Type -- Aka (prf | val)           | ConcreteType StaticExpression@@ -190,18 +178,30 @@                 | Second b                 deriving (Show, Eq, Generic, NFData) +data SortArg = SortArg String Sort+             | Anonymous Sort+    deriving (Show, Eq, Generic, NFData)+ -- | An argument to a function. data Arg = Arg (Paired String Type)          | PrfArg Arg Arg          | NoArgs     deriving (Show, Eq, Generic, NFData) +-- | A datatype for sorts.+data Sort = NamedSort String+          | T0p Addendum -- ^ t@ype+          | Vt0p Addendum -- ^ vt@ype+          | Addr+          deriving (Show, Eq, Generic, NFData)++-- FIXME a type for sorts? -- | Wrapper for universal quantifiers (refinement types)-data Universal = Universal { bound :: [Arg], typeU :: Maybe Type, prop :: Maybe StaticExpression } -- TODO NonEmpty type?+data Universal = Universal { bound :: [String], typeU :: Maybe Sort, prop :: Maybe StaticExpression } -- TODO NonEmpty type?     deriving (Show, Eq, Generic, NFData)  -- | Wrapper for existential quantifiers/types-data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe StaticExpression }+data Existential = Existential { boundE :: [String], isOpen :: Bool, typeE :: Maybe Sort, propE :: Maybe StaticExpression }     deriving (Show, Eq, Generic, NFData)  -- | @~@ is used to negate numbers in ATS@@ -299,6 +299,7 @@                 | FixAt String StackFunction                 | LambdaAt StackFunction                 | ParenExpr AlexPosn Expression+                | CommentExpr String Expression                 deriving (Show, Eq, Generic, NFData)  -- | An 'implement' declaration

@@ -14,7 +14,7 @@                  , help = Strptr1                  , return = flag_result                  }-vtypedef parser(a : vt@ype+) =+vtypedef parser(a: vt@ype+) =   @{ modify = Strptr1 -<lincloptr1> (a, Strptr1) }  fn run_parser {a:vt@ype+}(p : parser(a), s : Strptr1) : a =

@@ -9,10 +9,10 @@ staload "libats/SATS/deqarray.sats" staload _ = "libats/DATS/deqarray.dats" -absvtype queue_vtype(a : vt@ype+, int) = ptr+absvtype queue_vtype(a: vt@ype+, int) = ptr -vtypedef queue(a : vt0p, id : int) = queue_vtype(a, id)-vtypedef queue(a : vt0p) = [id:int] queue(a, id)+vtypedef queue(a: vt0p, id: int) = queue_vtype(a, id)+vtypedef queue(a: vt0p) = [id:int] queue(a, id)  absprop ISNIL (id : int, b : bool) @@ -45,9 +45,9 @@ assume ISNIL(id : int, b : bool) = unit_p assume ISFULL(id : int, b : bool) = unit_p -absvtype channel_vtype(a : vt@ype+) = ptr+absvtype channel_vtype(a: vt@ype+) = ptr -vtypedef channel(a : vt0p) = channel_vtype(a)+vtypedef channel(a: vt0p) = channel_vtype(a)  extern fun {a:vt0p} channel_insert  (!channel(a), a) : void@@ -98,7 +98,7 @@   let     prval () = __assert(prf) where     { extern-      praxi __assert {id:int} (p : ISNIL(id, false)) : [ false ] void }+      praxi __assert {id:int} (p : ISNIL(id, false)) : [false] void }   in     deqarray_takeout_atbeg<a>(xs)   end@@ -107,7 +107,7 @@   {     prval () = __assert(prf) where     { extern-      praxi __assert {id:int} (p : ISFULL(id, false)) : [ false ] void }+      praxi __assert {id:int} (p : ISFULL(id, false)) : [false] void }     val () = deqarray_insert_atend<a>(xs, x)   } @@ -131,7 +131,7 @@  implement {a} channel_unref (chan) =   let-    val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan+    val @CHANNEL{l0,l1,l2,l3}(ch) = chan     val spin = unsafe_spin_vt2t(ch.spin)     val (prf | ()) = spin_lock(spin)     val () = spin_unlock(prf | spin)@@ -160,7 +160,7 @@  implement channel_refcount {a} (chan) =   let-    val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan+    val @CHANNEL{l0,l1,l2,l3}(ch) = chan     val refcount = ch.refcount   in     (fold@(chan) ; refcount)@@ -211,7 +211,7 @@  implement {a} channel_insert (chan, x) =   let-    val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+    val+ CHANNEL{l0,l1,l2,l3}(ch) = chan     val mutex = unsafe_mutex_vt2t(ch.mutex)     val (prf | ()) = mutex_lock(mutex)     val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))@@ -222,7 +222,7 @@  implement {a} channel_remove (chan) =   x where-  { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+  { val+ CHANNEL{l0,l1,l2,l3}(ch) = chan     val mutex = unsafe_mutex_vt2t(ch.mutex)     val (prf | ()) = mutex_lock(mutex)     val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))@@ -232,7 +232,7 @@  implement {a} channel_remove_helper (chan, xs) =   let-    val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+    val+ CHANNEL{l0,l1,l2,l3}(ch) = chan     val (prf | is_nil) = queue_is_nil(xs)   in     if is_nil then@@ -260,7 +260,7 @@  implement {a} channel_insert_helper (chan, xs, x) =   let-    val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+    val+ CHANNEL{l0,l1,l2,l3}(ch) = chan     val (prf | is_full) = queue_is_full(xs)   in     if is_full then

@@ -24,13 +24,17 @@           loop(pf | n - 1, res)         end     +    // end of [if]     // end of [loop]     var res: int with pf = 1     val () = loop(pf | n, addr@res)+    +    // addr@res: the pointer to res   in     res   end +// end of [fact] implement main0 () =   let     val x = fact(30)

@@ -1,4 +1,5 @@ fun factorial_recursion {n:nat} .<n>. (n: int(n)) : int =+// case case+ n of | 0 => 1 | n =>> factorial_recursion(n-1) * n

@@ -1,4 +1,5 @@ fun factorial_recursion {n:nat} .<n>. (n : int(n)) : int =+  // case   case+ n of     | 0 => 1     | n =>> factorial_recursion(n - 1) * n

@@ -28,7 +28,7 @@     loop(size, c, list_vt_nil())   end -implement left_pad { p, l } (pad, c, s) =+implement left_pad {p,l} (pad, c, s) =   let     val size = strnptr_length(s)   in@@ -58,10 +58,10 @@           (let             prval _ = lemma_not_empty(s) where             { extern-              praxi lemma_not_empty {n:int} (x : string(n)) : [ n > 0 ] void }+              praxi lemma_not_empty {n:int} (x : string(n)) : [n > 0] void }             prval _ = lemma_not_zero(pad) where             { extern-              praxi lemma_not_zero {n:int} (x : int(n)) : [ n > 0 ] void }+              praxi lemma_not_zero {n:int} (x : int(n)) : [n > 0] void }             val (pf | res) = left_pad(i2ssz(pad), c, string1_copy(s))           in             (println!("padding: ", res) ; strnptr_free(res))

@@ -1,31 +1,1 @@-(* ****** ****** *)-//-// HX-2017-02-05:-//-// Generic-// Divide-Conquer in parallel-//-(* ****** ****** *)-//-#include "$PATSHOMELOCS\-/atscntrb-hx-threadkit/mylibies.hats" -//-(* ****** ****** *)-//-#include "$PATSHOMELOCS\-/atscntrb-hx-fworkshop/mylibies.hats"--//-(* ****** ****** *)-//-local-  #define DIVIDECONQUER_CONT 1-in-  #include "$PATSHOMELOCS\-  /atscntrb-bucs320-divideconquer/mylibies.hats"-end--//-(* ****** ****** *)-(* end of [mydepies.hats] *)

@@ -66,7 +66,7 @@   $UN.cast(n)  propdef PRIME (p : int) =-{ x, y : nat | x <= y } MUL(x, y, p) -<> [ x == 1 ] void+{ x, y : nat | x <= y } MUL(x, y, p) -<> [x == 1] void  dataprop FACT(int, int) =   | FACTbas(0, 1)

@@ -16,9 +16,9 @@ vtypedef cstream = stream_vt(char) vtypedef tstream = stream_vt(token) -datavtype either(a : t@ype, b : t@ype+) =+datavtype either(a: t@ype, b: t@ype+) =   | left of a   | right of b -vtypedef parser(a : vt@ype+) =+vtypedef parser(a: vt@ype+) =   @{ modify = cstream -<lincloptr1> (cstream, a) }