packages feed

copilot-prettyprinter (empty) → 3.12

raw patch · 8 files changed

+419/−0 lines, 8 filesdep +basedep +copilot-coredep +prettysetup-changed

Dependencies added: base, copilot-core, pretty

Files

+ CHANGELOG view
@@ -0,0 +1,3 @@+2022-11-07+        * Version bump (3.12). (#389)+        * Create new library for pretty-printer. (#383)
+ LICENSE view
@@ -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.
+ README.md view
@@ -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).
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot-prettyprinter.cabal view
@@ -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+  <https://copilot-language.github.io>.++author:              Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe,+                     Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez+license:             BSD3+license-file:        LICENSE+maintainer:          Ivan Perez <ivan.perezdominguez@nasa.gov>+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
+ src/Copilot/PrettyPrint.hs view
@@ -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
+ src/Copilot/PrettyPrint/Error.hs view
@@ -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 <ivan.perezdominguez@nasa.gov>"++-- | 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
+ src/Copilot/PrettyPrint/Type.hs view
@@ -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