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.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 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 @@ -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 } 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 @@ -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 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 @@ -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