diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,3 @@ +2022-11-07 + * Version bump (3.12). (#389) + * Create new library for pretty-printer. (#383) diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,29 @@ +2009 +BSD3 License terms + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the developers nor the names of its contributors +may be used to endorse or promote products derived from this software +without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,33 @@ +[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) + +# Copilot: a stream DSL +Copilot-prettyprinter implements a pretty-printer of Copilot Core +specifications. + +Copilot is a runtime verification framework written in Haskell. It allows the +user to write programs in a simple but powerful way using a stream-based +approach. + +Programs can be interpreted for testing, or translated C99 code to be +incorporated in a project, or as a standalone application. The C99 backend +ensures us that the output is constant in memory and time, making it suitable +for systems with hard realtime requirements. + + +## Installation +Copilot-prettyprinter can be found on +[Hackage](https://hackage.haskell.org/package/copilot-prettyprinter). It is +typically only installed as part of the complete Copilot distribution. For +installation instructions, please refer to the [Copilot +website](https://copilot-language.github.io). + + +## Further information +For further information, install instructions and documentation, please visit +the Copilot website: +[https://copilot-language.github.io](https://copilot-language.github.io) + + +## License +Copilot is distributed under the BSD-3-Clause license, which can be found +[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-prettyprinter/LICENSE). diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/copilot-prettyprinter.cabal b/copilot-prettyprinter.cabal new file mode 100644 --- /dev/null +++ b/copilot-prettyprinter.cabal @@ -0,0 +1,57 @@ +cabal-version: >=1.10 +name: copilot-prettyprinter +version: 3.12 +synopsis: A prettyprinter of Copilot Specifications. +description: + A prettyprinter of Copilot specifications. + . + Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in + Haskell that compiles into embedded C. Copilot contains an interpreter, + multiple back-end compilers, and other verification tools. + . + A tutorial, examples, and other information are available at + . + +author: Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe, + Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez +license: BSD3 +license-file: LICENSE +maintainer: Ivan Perez +homepage: https://copilot-language.github.io +bug-reports: https://github.com/Copilot-Language/copilot/issues +stability: Experimental +category: Language, Embedded +build-type: Simple +extra-source-files: README.md, CHANGELOG + +x-curation: uncurated + +source-repository head + type: git + location: https://github.com/Copilot-Language/copilot.git + subdir: copilot-prettyprinter + +library + + default-language: Haskell2010 + + hs-source-dirs: src + + ghc-options: + -Wall + -fno-warn-orphans + + build-depends: + base >= 4.9 && < 5, + pretty >= 1.0 && < 1.2, + + copilot-core + + exposed-modules: + + Copilot.PrettyPrint + + other-modules: + + Copilot.PrettyPrint.Error + Copilot.PrettyPrint.Type diff --git a/src/Copilot/PrettyPrint.hs b/src/Copilot/PrettyPrint.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/PrettyPrint.hs @@ -0,0 +1,194 @@ +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. + +-- | A pretty printer for Copilot specifications. + +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Safe #-} + +module Copilot.PrettyPrint + ( prettyPrint + , ppExpr + ) where + +import Copilot.Core +import Copilot.PrettyPrint.Error (impossible) +import Copilot.PrettyPrint.Type (showWithType, ShowType(..), showType) +import Prelude hiding (id, (<>)) +import Text.PrettyPrint.HughesPJ +import Data.List (intersperse) + +-- | Create a unique stream name by prefixing the given ID by a lowercase +-- letter @"s"@. +strmName :: Int -> Doc +strmName id = text "s" <> int id + +-- | Pretty-print a Copilot expression. +-- +-- The type is ignored, and only the expression is pretty-printed. +ppExpr :: Expr a -> Doc +ppExpr e0 = case e0 of + Const t x -> text (showWithType Haskell t x) + Drop _ 0 id -> strmName id + Drop _ i id -> text "drop" <+> text (show i) <+> strmName id + ExternVar _ name _ -> text "Ext_" <> (text name) + Local _ _ name e1 e2 -> text "local" <+> doubleQuotes (text name) <+> equals + <+> ppExpr e1 $$ text "in" <+> ppExpr e2 + Var _ name -> text "var" <+> doubleQuotes (text name) + Op1 op e -> ppOp1 op (ppExpr e) + Op2 op e1 e2 -> ppOp2 op (ppExpr e1) (ppExpr e2) + Op3 op e1 e2 e3 -> ppOp3 op (ppExpr e1) (ppExpr e2) (ppExpr e3) + Label _ s e -> text "label "<> doubleQuotes (text s) <+> (ppExpr e) + +-- | Pretty-print an untyped expression. +-- +-- The type is ignored, and only the expression is pretty-printed. +ppUExpr :: UExpr -> Doc +ppUExpr UExpr { uExprExpr = e0 } = ppExpr e0 + +-- | Pretty-print a unary operation. +ppOp1 :: Op1 a b -> Doc -> Doc +ppOp1 op = case op of + Not -> ppPrefix "not" + Abs _ -> ppPrefix "abs" + Sign _ -> ppPrefix "signum" + Recip _ -> ppPrefix "recip" + Exp _ -> ppPrefix "exp" + Sqrt _ -> ppPrefix "sqrt" + Log _ -> ppPrefix "log" + Sin _ -> ppPrefix "sin" + Tan _ -> ppPrefix "tan" + Cos _ -> ppPrefix "cos" + Asin _ -> ppPrefix "asin" + Atan _ -> ppPrefix "atan" + Acos _ -> ppPrefix "acos" + Sinh _ -> ppPrefix "sinh" + Tanh _ -> ppPrefix "tanh" + Cosh _ -> ppPrefix "cosh" + Asinh _ -> ppPrefix "asinh" + Atanh _ -> ppPrefix "atanh" + Acosh _ -> ppPrefix "acosh" + Ceiling _ -> ppPrefix "ceiling" + Floor _ -> ppPrefix "floor" + BwNot _ -> ppPrefix "~" + Cast _ _ -> ppPrefix "(cast)" + GetField (Struct _) _ f -> \e -> ppInfix "#" e (text $ accessorname f) + GetField _ _ _ -> impossible "ppOp1" "Copilot.PrettyPrint" + +-- | Pretty-print a binary operation. +ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc +ppOp2 op = case op of + And -> ppInfix "&&" + Or -> ppInfix "||" + Add _ -> ppInfix "+" + Sub _ -> ppInfix "-" + Mul _ -> ppInfix "*" + Div _ -> ppInfix "div" + Mod _ -> ppInfix "mod" + Fdiv _ -> ppInfix "/" + Pow _ -> ppInfix "**" + Logb _ -> ppInfix "logBase" + Atan2 _ -> ppInfix "atan2" + Eq _ -> ppInfix "==" + Ne _ -> ppInfix "/=" + Le _ -> ppInfix "<=" + Ge _ -> ppInfix ">=" + Lt _ -> ppInfix "<" + Gt _ -> ppInfix ">" + BwAnd _ -> ppInfix "&" + BwOr _ -> ppInfix "|" + BwXor _ -> ppInfix "^" + BwShiftL _ _ -> ppInfix "<<" + BwShiftR _ _ -> ppInfix ">>" + Index _ -> ppInfix ".!!" + +-- | Pretty-print a ternary operation. +ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc +ppOp3 op = case op of + Mux _ -> \ doc1 doc2 doc3 -> + text "(if" <+> doc1 <+> + text "then" <+> doc2 <+> + text "else" <+> doc3 <> text ")" + +-- | Parenthesize two 'Doc's, separated by an infix 'String'. +ppInfix :: String -> Doc -> Doc -> Doc +ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2 + +-- | Prefix a 'Doc' by a 'String'. +ppPrefix :: String -> Doc -> Doc +ppPrefix cs = (text cs <+>) + +-- | Pretty-print a Copilot stream as a case of a top-level function for +-- streams of that type, by pattern matching on the stream name. +ppStream :: Stream -> Doc +ppStream + Stream + { streamId = id + , streamBuffer = buffer + , streamExpr = e + , streamExprType = t + } + = (parens . text . showType) t + <+> strmName id + <+> text "=" + <+> text ("[" + ++ ( concat $ intersperse "," + $ map (showWithType Haskell t) buffer ) + ++ "]") + <+> text "++" + <+> ppExpr e + +-- | Pretty-print a Copilot trigger as a case of a top-level @trigger@ +-- function, by pattern matching on the trigger name. +ppTrigger :: Trigger -> Doc +ppTrigger + Trigger + { triggerName = name + , triggerGuard = e + , triggerArgs = args } + = text "trigger" <+> text "\"" <> text name <> text "\"" + <+> text "=" + <+> ppExpr e + <+> lbrack + $$ (nest 2 $ vcat (punctuate comma $ + map (\a -> text "arg" <+> ppUExpr a) args)) + $$ nest 2 rbrack + +-- | Pretty-print a Copilot observer as a case of a top-level @observer@ +-- function, by pattern matching on the observer name. +ppObserver :: Observer -> Doc +ppObserver + Observer + { observerName = name + , observerExpr = e } + = text "observer \"" <> text name <> text "\"" + <+> text "=" + <+> ppExpr e + +-- | Pretty-print a Copilot property as a case of a top-level @property@ +-- function, by pattern matching on the property name. +ppProperty :: Property -> Doc +ppProperty + Property + { propertyName = name + , propertyExpr = e } + = text "property \"" <> text name <> text "\"" + <+> text "=" + <+> ppExpr e + +-- | Pretty-print a Copilot specification, in the following order: +-- +-- - Streams definitions +-- - Trigger definitions +-- - Observer definitions +-- - Property definitions +ppSpec :: Spec -> Doc +ppSpec spec = cs $$ ds $$ es $$ fs + where + cs = foldr (($$) . ppStream) empty (specStreams spec) + ds = foldr (($$) . ppTrigger) empty (specTriggers spec) + es = foldr (($$) . ppObserver) empty (specObservers spec) + fs = foldr (($$) . ppProperty) empty (specProperties spec) + +-- | Pretty-print a Copilot specification. +prettyPrint :: Spec -> String +prettyPrint = render . ppSpec diff --git a/src/Copilot/PrettyPrint/Error.hs b/src/Copilot/PrettyPrint/Error.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/PrettyPrint/Error.hs @@ -0,0 +1,24 @@ +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. + +{-# LANGUAGE Safe #-} + +-- | Custom functions to report error messages to users. +module Copilot.PrettyPrint.Error + ( impossible + , badUsage ) where + +-- | Report an error due to a bug in Copilot. +impossible :: String -- ^ Name of the function in which the error was detected. + -> String -- ^ Name of the package in which the function is located. + -> a +impossible function package = + error $ "\"Impossible\" error in function " + ++ function ++ ", in package " ++ package + ++ ". Please file an issue at " + ++ "https://github.com/Copilot-Language/copilot/issues" + ++ "or email the maintainers at " + +-- | Report an error due to an error detected by Copilot (e.g., user error). +badUsage :: String -- ^ Description of the error. + -> a +badUsage msg = error $ "Copilot error: " ++ msg diff --git a/src/Copilot/PrettyPrint/Type.hs b/src/Copilot/PrettyPrint/Type.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/PrettyPrint/Type.hs @@ -0,0 +1,77 @@ +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. + +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Safe #-} + +-- | Show Copilot Core types and typed values. +module Copilot.PrettyPrint.Type + ( showWithType + , ShowType(..) + , showType + ) where + +import Copilot.Core.Type + +-- Are we proving equivalence with a C backend, in which case we want to show +-- Booleans as '0' and '1'. + +-- | Target language for showing a typed value. Used to adapt the +-- representation of booleans. +data ShowType = C | Haskell + +-- | Show a value. The representation depends on the type and the target +-- language. Booleans are represented differently depending on the backend. +showWithType :: ShowType -> Type a -> a -> String +showWithType showT t x = + case showT of + C -> case t of + Bool -> if x then "1" else "0" + _ -> sw + Haskell -> case t of + Bool -> if x then "true" else "false" + _ -> sw + where + sw = case showWit t of + ShowWit -> show x + +-- | Show Copilot Core type. +showType :: Type a -> String +showType t = + case t of + Bool -> "Bool" + Int8 -> "Int8" + Int16 -> "Int16" + Int32 -> "Int32" + Int64 -> "Int64" + Word8 -> "Word8" + Word16 -> "Word16" + Word32 -> "Word32" + Word64 -> "Word64" + Float -> "Float" + Double -> "Double" + Array t -> "Array " ++ showType t + Struct t -> "Struct" + +-- * Auxiliary show instance + +-- | Witness datatype for showing a value, used by 'showWithType'. +data ShowWit a = Show a => ShowWit + +-- | Turn a type into a show witness. +showWit :: Type a -> ShowWit a +showWit t = + case t of + Bool -> ShowWit + Int8 -> ShowWit + Int16 -> ShowWit + Int32 -> ShowWit + Int64 -> ShowWit + Word8 -> ShowWit + Word16 -> ShowWit + Word32 -> ShowWit + Word64 -> ShowWit + Float -> ShowWit + Double -> ShowWit + Array t -> ShowWit + Struct t -> ShowWit