diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -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 diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs --- a/src/Language/ATS.hs +++ b/src/Language/ATS.hs @@ -31,6 +31,8 @@ , StackFunction (..) , Paired (..) , Fixity (..) + , SortArg (..) + , Sort (..) -- * Lexical types , Token (..) , AlexPosn (..) diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x --- a/src/Language/ATS/Lexer.x +++ b/src/Language/ATS/Lexer.x @@ -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 diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y --- a/src/Language/ATS/Parser.y +++ b/src/Language/ATS/Parser.y @@ -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) } diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -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 diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -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 diff --git a/test/data/cli.out b/test/data/cli.out --- a/test/data/cli.out +++ b/test/data/cli.out @@ -14,7 +14,7 @@ , help = Strptr1 , return = flag_result } -vtypedef parser(a : vt@ype+) = +vtypedef parser(a: vt@ype+) = @{ modify = Strptr1 - (a, Strptr1) } fn run_parser {a:vt@ype+}(p : parser(a), s : Strptr1) : a = diff --git a/test/data/concurrency.out b/test/data/concurrency.out --- a/test/data/concurrency.out +++ b/test/data/concurrency.out @@ -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(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(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 diff --git a/test/data/fact.out b/test/data/fact.out --- a/test/data/fact.out +++ b/test/data/fact.out @@ -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) diff --git a/test/data/factorial.dats b/test/data/factorial.dats --- a/test/data/factorial.dats +++ b/test/data/factorial.dats @@ -1,4 +1,5 @@ fun factorial_recursion {n:nat} .. (n: int(n)) : int = +// case case+ n of | 0 => 1 | n =>> factorial_recursion(n-1) * n diff --git a/test/data/factorial.out b/test/data/factorial.out --- a/test/data/factorial.out +++ b/test/data/factorial.out @@ -1,4 +1,5 @@ fun factorial_recursion {n:nat} .. (n : int(n)) : int = + // case case+ n of | 0 => 1 | n =>> factorial_recursion(n - 1) * n diff --git a/test/data/left-pad.out b/test/data/left-pad.out --- a/test/data/left-pad.out +++ b/test/data/left-pad.out @@ -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)) diff --git a/test/data/mydepies.out b/test/data/mydepies.out --- a/test/data/mydepies.out +++ b/test/data/mydepies.out @@ -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] *) diff --git a/test/data/number-theory.out b/test/data/number-theory.out --- a/test/data/number-theory.out +++ b/test/data/number-theory.out @@ -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) diff --git a/test/data/types.out b/test/data/types.out --- a/test/data/types.out +++ b/test/data/types.out @@ -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 - (cstream, a) }