language-ats 0.1.1.13 → 0.1.1.14
raw patch · 4 files changed
+97/−96 lines, 4 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Language.ATS: ProofImpl :: Implementation -> Declaration
+ Language.ATS: ProofImpl :: [Arg] -> Implementation -> Declaration
Files
- language-ats.cabal +1/−1
- src/Language/ATS/Parser.y +28/−30
- src/Language/ATS/PrettyPrint.hs +66/−63
- src/Language/ATS/Types.hs +2/−2
language-ats.cabal view
@@ -1,5 +1,5 @@ name: language-ats-version: 0.1.1.13+version: 0.1.1.14 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
src/Language/ATS/Parser.y view
@@ -468,13 +468,10 @@ MaybeImplicit : Implicits { $1 } | { [] } +-- TODO also allow static expressions! -- | Parse the details of an implementation-Implementation : FunName MaybeImplicit doubleParens eq Expression { Implement $3 [] $2 [] $1 [] $5 } -- FIXME actually account for these somewhere- | FunName MaybeImplicit openParen FullArgs closeParen eq Expression { Implement $3 [] $2 [] $1 $4 $7 }- | FunName MaybeImplicit Universals openParen FullArgs closeParen eq Expression { Implement $4 [] $2 $3 $1 $5 $8 }- | Universals FunName MaybeImplicit openParen FullArgs closeParen eq Expression { Implement $4 $1 $3 [] $2 $5 $8 }- | Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq Expression { Implement $5 $1 $3 $4 $2 $6 $9 }- | Universals FunName MaybeImplicit doubleParens eq Expression { Implement $4 $1 $3 [] $2 [] $6 }+Implementation : Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq Expression { Implement $5 $1 $3 $4 $2 $6 $9 }+ | Universals FunName MaybeImplicit Universals doubleParens eq Expression { Implement $5 $1 $3 $4 $2 [] $7 } -- | Parse a function name FunName : IdentifierOr { Unqualified $1 }@@ -608,6 +605,12 @@ AndSort : AndSort and IdentifierOr eq Type { AndD $1 (SortDef $2 $3 $5) } -- TODO figure out if this is building up the slow way | sortdef IdentifierOr eq Type { SortDef $1 $2 $4 } +-- FIXME stadef r() = file_mode_r()+AndStadef : stadef boolLit eq Name { Stadef (over _head toLower (show $2)) $4 [] }+ | stadef boolLit eq identifierSpace { Stadef (over _head toLower (show $2)) (Unqualified $ to_string $4) [] }+ | AndStadef and stadef boolLit eq identifierSpace { AndD $1 (Stadef (over _head toLower (show $4)) (Unqualified $ to_string $6) []) }+ | AndStadef and stadef boolLit eq identifier { AndD $1 (Stadef (over _head toLower (show $4)) (Unqualified $ to_string $6) []) }+ -- | Function declaration FunDecl : fun PreFunction { [ Func $1 (Fun $2) ] } | prfun PreFunction { [ Func $1 (PrFun $2) ] }@@ -636,34 +639,29 @@ MaybeType : eq Type { Just $2 } | { Nothing } +FunArgs : { [NoArgs] }+ | openParen FullArgs closeParen { $2 }+ | doubleParens { [] }+ -- | Parse a declaration defining a type-TypeDecl : typedef IdentifierOr eq Type { TypeDef $1 $2 [] $4 }- | typedef IdentifierOr openParen FullArgs closeParen eq Type { TypeDef $1 $2 $4 $7 }- | vtypedef IdentifierOr eq Type { ViewTypeDef $1 $2 [] $4 }- | vtypedef IdentifierOr openParen FullArgs closeParen eq Type { ViewTypeDef $1 $2 $4 $7 }- | datatype IdentifierOr eq Leaves { SumType $2 [] $4 }- | datatype IdentifierOr openParen Args closeParen eq Leaves { SumType $2 $4 $7 }- | datavtype IdentifierOr eq Leaves { SumViewType $2 [] $4 }- | datavtype IdentifierOr doubleParens eq Leaves { SumViewType $2 [] $5 }- | datavtype IdentifierOr openParen Args closeParen eq Leaves { SumViewType $2 $4 $7 }+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 } | abst0p IdentifierOr eq Type { AbsT0p $1 $2 $4 } | viewdef IdentifierOr openParen FullArgs closeParen eq Type { ViewDef $1 $2 $4 $7 }- | absvt0p IdentifierOr openParen FullArgs closeParen MaybeType { AbsVT0p $1 $2 $4 $6 }- | absvt0p IdentifierOr eq Type { AbsVT0p $1 $2 [] (Just $4) }+ | absvt0p IdentifierOr FunArgs eq Type { AbsVT0p $1 $2 $3 (Just $5) } | absview IdentifierOr openParen FullArgs closeParen MaybeType { AbsView $1 $2 $4 $6 }- | abstype IdentifierOr MaybeType { AbsType $1 $2 [] $3 }- | abstype IdentifierOr openParen FullArgs closeParen MaybeType { AbsType $1 $2 $4 $6 }- | absvtype IdentifierOr MaybeType { AbsViewType $1 $2 [] $3 }- | absvtype IdentifierOr openParen FullArgs closeParen MaybeType { AbsViewType $1 $2 $4 $6 }+ | abstype IdentifierOr FunArgs MaybeType { AbsType $1 $2 $3 $4 }+ | absvtype IdentifierOr FunArgs 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 }- | stadef IdentifierOr eq Name { Stadef $2 $4 [] }- | stadef IdentifierOr eq Name openParen TypeIn closeParen { Stadef $2 $4 $6 }- | stadef boolLit eq Name { Stadef (over _head toLower (show $2)) $4 [] } -- TODO identifierSpace- | sortdef IdentifierOr eq Type { SortDef $1 $2 $4 } | AndSort { $1 }- | vtypedef IdentifierOr eq vbar {% Left $ Expected $3 "Type" "|" }- | datavtype IdentifierOr openParen Args closeParen vbar {% Left $ Expected $6 "=" "|" }+ | 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 "=" "|" } Fixity : infixr { RightFix $1 } | infixl { LeftFix $1 }@@ -709,11 +707,11 @@ | var Pattern eq lamAt StackFunction { Var Nothing $2 (Just $ LambdaAt $5) Nothing } | prval Pattern eq Expression { PrVal $2 $4 } | praxi PreFunction { Func $1 (Praxi $2) }- | primplmnt Implementation { ProofImpl $2 }- | implement Implementation { Impl [] $2 }- | implement openParen Args closeParen Implementation { Impl $3 $5 }+ | primplmnt FunArgs Implementation { ProofImpl $2 $3 }+ | implement FunArgs Implementation { Impl $2 $3 } | overload BinOp with Name { OverloadOp $1 $2 $4 } | overload identifierSpace with Name { OverloadIdent $1 (to_string $2) $4 Nothing }+ | overload identifierSpace with identifierSpace of intLit { OverloadIdent $1 (to_string $2) (Unqualified $ to_string $4) (Just $6) } | overload tilde with identifierSpace of intLit { OverloadIdent $1 "~" (Unqualified $ to_string $4) (Just $6) } -- FIXME figure out a general solution. | assume identifierSpace eq Type { Assume (Unqualified (to_string $2)) [NoArgs] $4 } | assume Name eq Type { Assume $2 [NoArgs] $4 }
src/Language/ATS/PrettyPrint.hs view
@@ -461,6 +461,10 @@ prettyArgs :: (Pretty a) => [a] -> Doc prettyArgs = prettyArgs' ", " "(" ")" +prettyArgsNil :: [Arg] -> Doc+prettyArgsNil NoA = mempty+prettyArgsNil as = prettyArgs' ", " "(" ")" as+ fancyU :: [Universal] -> Doc fancyU = foldMap pretty . reverse @@ -508,70 +512,69 @@ valSig :: (Pretty a) => Maybe a -> Doc valSig = prettySigG mempty mempty +-- prettyUniversalsNil :: [Universal] -> Doc+-- prettyUniversalsNil [] = mempty+-- prettyUniversalsNil us = prettyArgsU mempty softline (fmap pretty us)+ instance Pretty Declaration where- pretty (AbsType _ s as Nothing) = "abstype" <+> text s <> prettyArgs as- pretty (AbsType _ s as (Just t)) = "abstype" <+> text s <> prettyArgs as <+> "=" <+> pretty t- pretty (AbsViewType _ s as Nothing) = "absvtype" <+> text s <> prettyArgs as- pretty (AbsViewType _ s as (Just t)) = "absvtype" <+> text s <> prettyArgs as <+> "=" <+> pretty t- pretty (SumViewType s [] ls) = "datavtype" <+> text s <+> "=" <$> prettyLeaf ls- pretty (SumViewType s as ls) = "datavtype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls- pretty (SumType s [] ls) = "datatype" <+> text s <+> "=" <$> prettyLeaf ls- pretty (SumType s as ls) = "datatype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls- pretty (Impl [] i) = "implement" <+> pretty i- pretty (Impl us i) = "implement" <+> mconcat (fmap pretty us) <+> pretty i- pretty (ProofImpl i) = "primplmnt" <+> pretty i- pretty (PrVal p e) = "prval" <+> pretty p <+> "=" <+> pretty e- pretty (AndDecl t p e) = "and" <+> pretty p <> valSig t <+> "=" <+> pretty e- pretty (Val a t p e) = "val" <> pretty a <+> pretty p <> valSig t <+> "=" <+> pretty e- pretty (Var (Just t) p Nothing (Just e)) = "var" <+> pretty p <> ":" <+> pretty t <+> "with" <+> pretty e- pretty (Var Nothing p e Nothing) = "var" <+> pretty p <+> "=" <+> pretty e- pretty (Var (Just t) p e Nothing) = "var" <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e- pretty (Var _ _ _ Just{}) = undefined- pretty (Include s) = "#include" <+> pretty s- pretty (Staload b Nothing s) = bool "" "#" b <> "staload" <+> pretty s- pretty (Staload b (Just q) s) = bool "" "#" b <> "staload" <+> pretty q <+> "=" <+> pretty s- pretty (CBlock s) = string s- pretty (Comment s) = string s- pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n- pretty (OverloadIdent _ i n Nothing) = "overload" <+> text i <+> "with" <+> pretty n- pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n'+ 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 (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+ pretty (AndDecl t p e) = "and" <+> pretty p <> valSig t <+> "=" <+> pretty e+ pretty (Val a t p e) = "val" <> pretty a <+> pretty p <> valSig t <+> "=" <+> pretty e+ pretty (Var t p Nothing (Just e)) = "var" <+> pretty p <> valSig t <+> "with" <+> pretty e+ pretty (Var t p e Nothing) = "var" <+> pretty p <> valSig t <+> "=" <+> pretty e+ pretty (Var _ _ _ Just{}) = undefined+ pretty (Include s) = "#include" <+> pretty s+ pretty (Staload b Nothing s) = bool "" "#" b <> "staload" <+> pretty s+ pretty (Staload b (Just q) s) = bool "" "#" b <> "staload" <+> pretty q <+> "=" <+> pretty s+ pretty (CBlock s) = string s+ pretty (Comment s) = string s+ pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n+ pretty (OverloadIdent _ i n Nothing) = "overload" <+> text i <+> "with" <+> pretty n+ pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n' -- We use 'text' here, which means indentation might get fucked up for -- C preprocessor macros, but you absolutely deserve it if you indent your -- macros.- pretty (Define s) = text s- pretty (Func _ (Fn pref)) = "fn" </> pretty pref- pretty (Func _ (Fun pref)) = "fun" </> pretty pref- pretty (Func _ (CastFn pref)) = "castfn" </> pretty pref- pretty (Func _ (Fnx pref)) = "fnx" </> pretty pref- pretty (Func _ (And pref)) = "and" </> pretty pref- pretty (Func _ (Praxi pref)) = "praxi" </> pretty pref- pretty (Func _ (PrFun pref)) = "prfun" </> pretty pref- 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 [] t) = "vtypedef" <+> text s <+> "=" <#> pretty t- pretty (ViewTypeDef _ s as t) = "vtypedef" <+> text s <> prettyArgs as <+> "=" <#> pretty t- pretty (TypeDef _ s [] t) = "typedef" <+> text s <+> "=" <+> pretty t- pretty (TypeDef _ s as t) = "typedef" <+> text s <> prettyArgs 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- pretty (SymIntr _ n) = "symintr" <+> pretty n- pretty (Stacst _ n t Nothing) = "stacst" </> pretty n <+> ":" </> pretty t- pretty (Stacst _ n t (Just e)) = "stacst" </> pretty n <+> ":" </> pretty t <+> "=" </> pretty e- pretty (PropDef _ s as t) = "propdef" </> text s <+> prettyArgs as <+> "=" </> pretty t- pretty (Local _ d d') = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end"- pretty (FixityDecl f (Left s) ss) = pretty f <+> "(" <> text s <> ")" <+> hsep (fmap text ss)- pretty (FixityDecl f (Right i) ss) = pretty f <+> pretty i <+> hsep (fmap text ss)- pretty (StaVal us i t) = "val" </> mconcat (fmap pretty us) <+> text i <+> ":" <+> pretty t- pretty (Stadef i n []) = "stadef" <+> text i <+> pretty n- pretty (Stadef i n as) = "stadef" <+> 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 (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- pretty (TKind _ n s) = pretty n <+> "=" <+> text s- pretty (SortDef _ s t) = "sortdef" <+> text s <+> "=" <+> pretty t- pretty (AndD d (SortDef _ i t)) = pretty d <+> "and" <+> text i <+> "=" <+> pretty t- pretty AndD{} = undefined -- probably not valid syntax if we get to this point+ pretty (Define s) = text s+ pretty (Func _ (Fn pref)) = "fn" </> pretty pref+ pretty (Func _ (Fun pref)) = "fun" </> pretty pref+ pretty (Func _ (CastFn pref)) = "castfn" </> pretty pref+ pretty (Func _ (Fnx pref)) = "fnx" </> pretty pref+ pretty (Func _ (And pref)) = "and" </> pretty pref+ pretty (Func _ (Praxi pref)) = "praxi" </> pretty pref+ pretty (Func _ (PrFun pref)) = "prfun" </> pretty pref+ 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 (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+ pretty (SymIntr _ n) = "symintr" <+> pretty n+ pretty (Stacst _ n t Nothing) = "stacst" </> pretty n <+> ":" </> pretty t+ pretty (Stacst _ n t (Just e)) = "stacst" </> pretty n <+> ":" </> pretty t <+> "=" </> pretty e+ pretty (PropDef _ s as t) = "propdef" </> text s <+> prettyArgs as <+> "=" </> pretty t+ pretty (Local _ d d') = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end"+ pretty (FixityDecl f (Left s) ss) = pretty f <+> "(" <> text s <> ")" <+> hsep (fmap text ss)+ pretty (FixityDecl f (Right i) ss) = pretty f <+> pretty i <+> hsep (fmap text ss)+ pretty (StaVal us i t) = "val" </> mconcat (fmap pretty us) <+> text i <+> ":" <+> pretty t+ pretty (Stadef i n []) = "stadef" <+> text i <+> pretty n+ pretty (Stadef i n as) = "stadef" <+> text i <+> pretty n <> prettyArgs as+ 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 (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+ pretty (TKind _ n s) = pretty n <+> "=" <+> text s+ pretty (SortDef _ s t) = "sortdef" <+> text s <+> "=" <+> pretty t+ pretty (AndD d (SortDef _ i t)) = pretty d <+> "and" <+> text i <+> "=" <+> pretty t+ pretty AndD{} = undefined -- probably not valid syntax if we get to this point
src/Language/ATS/Types.hs view
@@ -75,8 +75,8 @@ -- | Declare something in a scope (a function, value, action, etc.) data Declaration = Func AlexPosn Function- | Impl [Arg] Implementation- | ProofImpl Implementation -- primplmnt -- TODO add args+ | Impl [Arg] Implementation -- TODO do something better for implicit universals+ | ProofImpl [Arg] Implementation | Val Addendum (Maybe Type) Pattern Expression | StaVal [Universal] String Type | PrVal Pattern Expression