Merge branch 'develop-prettyprinter'. Close #383.

ivanperez-keera · ivanperez-keera · commit 2f105a7caf8d · 2022-10-22T00:11:55.000Z
**Description** Currently, the architecture of Copilot mixes backends with other libraries, which makes the result not uniform. For example, the pretty-printer is part of `copilot-core`, while the C99 backend and the interpreter are in separate libraries. The implementation does not match our desired architecture according to our design documents, and it makes the code partly harder to maintain. A better solution would be to move the pretty-printer to a separate library, and to deprecate any pretty-printer modules exported from `copilot-core`. **Type** - Maintenance: match proposed design. **Additional context** None. **Requester** - Ivan Perez **Method to check presence of bug** None (not a bug). **Expected result** There should be a `copilot-prettyprinter` library, and all pretty-printer modules in `copilot-core` should be deprecated. The following Dockerfile checks that the new library is installed and the modules in the pretty-printer can be used from their new location, in which case it prints the message `Success`: ```Dockerfile FROM ubuntu:trusty RUN apt-get update RUN apt-get install --yes software-properties-common RUN add-apt-repository ppa:hvr/ghc RUN apt-get update RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4 RUN apt-get install --yes libz-dev ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH RUN cabal update RUN cabal v1-sandbox init RUN cabal v1-install alex happy RUN apt-get install --yes git SHELL ["/bin/bash", "-c"] CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \ && cabal v1-install copilot/copilot**/ --enable-tests --enable-documentation --run-tests \ && cabal v1-exec -- runhaskell -Wall -Werror=deprecations <<< "import Copilot.PrettyPrint(); main :: IO (); main = return ()" \ && echo "Success" ``` Command (substitute variables based on new path after merge): ``` $ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-383 ``` **Solution implemented** Deprecate `Copilot.Core.PrettyPrinter`. Move module to a different name-space and library (e.g., `copilot-prettyprinter`). Modify the tests accordingly. Deprecate `Copilot.Core.PrettyPrint`. Move module to a new library `copilot-prettyprinter` and place it under a new namespace (`Copilot.PrettyPrint`). Copy over the necessary definitions from `Copilot.Core.Type.ShowInternal`, as well as `Copilot.Core.Error`. Adapt cabal file in new library, minimizing dependencies. Adapt README in new library to reflect the purpose of the library. Modify copilot-language, copilot-theorem, and copilot-interpreter so that the definitions used and exported (when appropriate) are taken from copilot-prettyprinter. **Further notes** None.
diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG
@@ -1,3 +1,6 @@
+2022-10-21
+        * Deprecate Copilot.Core.PrettyPrinter. (#383)
+
 2022-09-07
         * Version bump (3.11). (#376)
         * Deprecate Copilot.Core.PrettyDot. (#359)
diff --git a/copilot-core/src/Copilot/Core/PrettyPrint.hs b/copilot-core/src/Copilot/Core/PrettyPrint.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE Safe  #-}
 
 module Copilot.Core.PrettyPrint
+  {-# DEPRECATED "This module is deprecated in Copilot 3.12. Use copilot-prettyprinter instead." #-}
   ( prettyPrint
   , ppExpr
   ) where
diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG
@@ -1,3 +1,6 @@
+2022-10-21
+        * Use pretty-printer from copilot-prettyprinter. (#383)
+
 2022-09-07
         * Version bump (3.11). (#376)
         * Split copilot-interpreter into separate library. (#361)
diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal
@@ -76,6 +76,7 @@ test-suite unit-tests
 
     , copilot-core
     , copilot-interpreter
+    , copilot-prettyprinter
 
   hs-source-dirs:
     tests
diff --git a/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs b/copilot-interpreter/tests/Test/Copilot/Interpret/Eval.hs
@@ -28,11 +28,11 @@ import Text.PrettyPrint.HughesPJ            (render)
 import Copilot.Core.Expr        (Expr (Const, Drop, Op1, Op2, Op3),
                                  UExpr (UExpr))
 import Copilot.Core.Operators   (Op1 (..), Op2 (..), Op3 (..))
-import Copilot.Core.PrettyPrint (ppExpr)
 import Copilot.Core.Spec        (Observer (..), Spec (..), Stream (Stream))
 import Copilot.Core.Type        (Type (..), Typed (typeOf))
 import Copilot.Interpret.Eval   (ExecTrace (interpObservers),
                                  ShowType (Haskell), eval)
+import Copilot.PrettyPrint      (ppExpr)
 
 -- Internal imports: auxiliary functions
 import Test.Extra (apply1, apply2, apply3)
diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG
@@ -1,3 +1,6 @@
+2022-10-21
+        * Use pretty-printer from copilot-prettyprinter. (#383)
+
 2022-09-07
         * Version bump (3.11). (#376)
         * Deprecate prettyPrint. (#362)
diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal
@@ -35,16 +35,17 @@ source-repository head
 library
   default-language: Haskell2010
   hs-source-dirs: src
-  build-depends: base                >= 4.9 && < 5
+  build-depends: base                  >= 4.9 && < 5
 
-               , array               >= 0.5 && < 0.6
-               , containers          >= 0.4 && < 0.7
-               , data-reify          >= 0.6 && < 0.7
-               , mtl                 >= 2.0 && < 3
+               , array                 >= 0.5 && < 0.6
+               , containers            >= 0.4 && < 0.7
+               , data-reify            >= 0.6 && < 0.7
+               , mtl                   >= 2.0 && < 3
 
-               , copilot-core        >= 3.11 && < 3.12
-               , copilot-interpreter >= 3.11 && < 3.12
-               , copilot-theorem     >= 3.11 && < 3.12
+               , copilot-core          >= 3.11 && < 3.12
+               , copilot-interpreter   >= 3.11 && < 3.12
+               , copilot-prettyprinter >= 3.11 && < 3.12
+               , copilot-theorem       >= 3.11 && < 3.12
 
   exposed-modules: Copilot.Language
                  , Copilot.Language.Operators.BitWise
diff --git a/copilot-language/src/Copilot/Language.hs b/copilot-language/src/Copilot/Language.hs
@@ -47,7 +47,6 @@ import Data.Word
 import Copilot.Core (Name, Typed)
 import Copilot.Core.Type
 import Copilot.Core.Type.Array
-import qualified Copilot.Core.PrettyPrint as PP
 import Copilot.Language.Error
 import Copilot.Language.Interpret
 import Copilot.Language.Operators.Boolean
@@ -68,6 +67,7 @@ import Copilot.Language.Reify
 import Copilot.Language.Prelude
 import Copilot.Language.Spec
 import Copilot.Language.Stream (Stream)
+import qualified Copilot.PrettyPrint as PP
 
 -- | Transform a high-level Copilot Language specification into a low-level
 -- Copilot Core specification and pretty-print it to stdout.
diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG
@@ -0,0 +1,2 @@
+2022-10-21
+        * Create new library for pretty-printer. (#383)
diff --git a/copilot-prettyprinter/LICENSE b/copilot-prettyprinter/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/copilot-prettyprinter/README.md b/copilot-prettyprinter/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/copilot-prettyprinter/Setup.hs b/copilot-prettyprinter/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal
@@ -0,0 +1,57 @@
+cabal-version:       >=1.10
+name:                copilot-prettyprinter
+version:             3.11
+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
diff --git a/copilot-prettyprinter/src/Copilot/PrettyPrint.hs b/copilot-prettyprinter/src/Copilot/PrettyPrint.hs
diff --git a/copilot-prettyprinter/src/Copilot/PrettyPrint/Error.hs b/copilot-prettyprinter/src/Copilot/PrettyPrint/Error.hs
diff --git a/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs b/copilot-prettyprinter/src/Copilot/PrettyPrint/Type.hs
diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG
diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal
diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+2022-10-21`
	`2`	`+ * Create new library for pretty-printer. (#383)`