`copilot-prettyprinter`: Support pretty-printing struct updates

[RyanGlScott]

Copilot 3.20 added support for struct updates via the new UpdateField operation. At the moment, there is no support in the copilot-prettyprinter package for pretty-printing UpdateField operations. For example, this means that the following Copilot specification will fail when executed:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Data.Foldable (for_)
import Data.Functor (void)
import Data.Word (Word32)

import qualified Copilot.PrettyPrint as PP
import Language.Copilot

data S = S
  { unS :: Field "unS" Word32
  }

instance Struct S where
  typeName _ = "s"
  toValues s = [Value typeOf (unS s)]

instance Typed S where
  typeOf = Struct (S (Field 0))

spec :: Spec
spec = do
  let externS :: Stream S
      externS = extern "extern_s" Nothing

      example :: Stream Word32
      example = (externS ## unS =: 42) # unS

  trigger "example" (example == example) [arg externS, arg example]

main :: IO ()
main = do
  spec' <- reify spec
  putStrLn $ PP.prettyPrint spec'

$ runghc UpdateFieldPP.hs 
UpdateFieldPP.hs: src/Copilot/PrettyPrint.hs:(79,12)-(102,31): Non-exhaustive patterns in case

I have a prototype fix available in this branch, which could be used as a starting point for a patch.

[ivanperez-keera]

Description

Copilot currently supports modifying values from streams of structs, but not pretty-printing them using copilot-prettyprinter.

Type

• Bug: exception produced when executing valid specification.

Additional context

• Issue #520 introduced support for modifying structs.

Requester

• Ryan Scott (Galois)

Method to check presence of bug

Running the following specification that pretty-prints a spec with a struct update:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Data.Foldable (for_)
import Data.Functor (void)
import Data.Word (Word32)

import qualified Copilot.PrettyPrint as PP
import Language.Copilot

data S = S
  { unS :: Field "unS" Word32
  }

instance Struct S where
  typeName _ = "s"
  toValues s = [Value typeOf (unS s)]

instance Typed S where
  typeOf = Struct (S (Field 0))

spec :: Spec
spec = do
  let externS :: Stream S
      externS = extern "extern_s" Nothing

      example :: Stream Word32
      example = (externS ## unS =: 42) # unS

  trigger "example" (example == example) [arg externS, arg example]

main :: IO ()
main = do
  spec' <- reify spec
  putStrLn $ PP.prettyPrint spec'

produces an error message:

$ runghc UpdateFieldPP.hs 
UpdateFieldPP.hs: src/Copilot/PrettyPrint.hs:(79,12)-(102,31): Non-exhaustive patterns in case

when it should instead execute correctly and pretty-print the spec.

Expected result

Copilot allows pretty-printing struct updates in copilot-prettyprinter.

Desired result

Copilot allows pretty-printing struct updates in copilot-prettyprinter.

Proposed solution

Introduce a case for pretty-printing struct updates.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 4.

Fix assigned to: @RyanGlScott .

[RyanGlScott]

Implementor: Solution implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:

  • [X] The code proposed compiles and passes all tests. Details: Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/272116442

  • [X] The solution proposed produces the expected result. Details: The following Dockerfile installs copilot and runs a spec that uses copilot-prettyprinter to pretty print an expression with stream with a struct update in it, followed by "Success":

    
    --- Dockerfile
    FROM ubuntu:focal

  ENV DEBIAN_FRONTEND=noninteractive RUN apt-get update

  RUN apt-get install --yes libz-dev RUN apt-get install --yes git

  RUN apt-get install --yes wget RUN mkdir -p $HOME/.ghcup/bin RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup

  RUN chmod a+x $HOME/.ghcup/bin/ghcup ENV PATH=$PATH:/root/.ghcup/bin/ ENV PATH=$PATH:/root/.cabal/bin/ RUN apt-get install --yes curl RUN apt-get install --yes gcc g++ make libgmp3-dev RUN apt-get install --yes pkg-config

  SHELL ["/bin/bash", "-c"]

  RUN ghcup install ghc 9.4 RUN ghcup install cabal 3.2 RUN ghcup set ghc 9.4.8 RUN cabal update

  ADD UpdateFieldPP.hs /tmp/UpdateFieldPP.hs

  CMD git clone $REPO \ && cd $NAME \ && git checkout $COMMIT \ && cabal v1-sandbox init \ && cabal v1-install alex happy \ && cabal v1-install copilot**/ \ && cabal v1-exec -- runhaskell /tmp/UpdateFieldPP.hs \ && echo Success

  --- UpdateFieldPP.hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE NoImplicitPrelude #-} module Main (main) where

  import Data.Foldable (for_) import Data.Functor (void) import Data.Word (Word32)

  import qualified Copilot.PrettyPrint as PP import Language.Copilot

  data S = S { unS :: Field "unS" Word32 }

  instance Struct S where typeName _ = "s" toValues s = [Value typeOf (unS s)]

  instance Typed S where typeOf = Struct (S (Field 0))

  spec :: Spec spec = do let externS :: Stream S externS = extern "extern_s" Nothing

    example :: Stream Word32
    example = (externS ## unS =: 42) # unS

  trigger "example" (example == example) [arg externS, arg example]

  main :: IO () main = do spec' <- reify spec putStrLn $ PP.prettyPrint spec'

  Command (substitute variables based on new path after merge):

  $ docker run -e "REPO=https://github.com/GaloisInc/copilot-1" -e "NAME=copilot-1" -e "COMMIT=cc9ca2276e86676ef41393412224cff96c952a61" -it copilot-verify-526

• [X] Implementation is documented. Details: No new functions are provided; just an update to an existing function.
• [X] Change history is clear.
• [X] Commit messages are clear.
• [X] Changelogs are updated.
• [X] Examples are updated. Details: No updates needed.
• [X] Required version bumps are evaluated. Details: Bump not needed (bug fix).

[ivanperez-keera]

Change Manager: Implementation ready to be merged.