Define generic implementations of Struct and Typed methods. Refs #564.

[RyanGlScott]

This adds functionality for implementing the class methods of Struct and Typed using GHC.Generics in copilot-core. As such, one can now easily define instances of these classes by deriving a Generic instance for the struct data type, i.e.,

data MyStructType = ...
  deriving Generic

instance Struct MyStructType where
  typeName = typeNameDefault
  toValues = toValuesDefault
  updateField = updateFieldDefault

instance Typed MyStructType where
  typeOf = typeOfDefault

This work is based off of an initial implementation by Marten Wijnja (@Qqwy).

Note that I do not yet change any of the default implementations of any Struct or Typed methods. This is because several Struct instances in the wild currently do not define implementations of updateField, and moreover, they also do not define Generic instances for the corresponding data types. As such, changing the default implementation of updateField to use a Generic-based default would cause these instances in the wild to no longer compile. We will explore changing the default implementations after a suitable transition period.

I have also modified the struct-related copilot examples to implement their Struct and Typed instances using these new functions. Note that I have intentionally not used updateFieldDefault in the StructsUpdateField.hs example, as that example is intended to demonstrate how one would implement updateField by hand.

Fixes #564. Supersedes #516.

[ivanperez-keera]

Change Manager: You mention #561 in your commit messages but you mean #516. It's ok not to mention #516 at all since you are bringing the changes you want from it and #516 won't be merged.

[RyanGlScott]

You mention #561 in your commit messages but you mean #516.

Oops, my apologies!

It's ok not to mention #516 at all since you are bringing the changes you want from it and #516 won't be merged.

Sounds good. I've removed mention of #516 from the commit messages.

[ivanperez-keera]

Change Manager: Can you please make the following changes:

• Import generics explicit.

• Give a few more details in the haddock comments for the instances.

• There is one instance that uses a normal comment instead of a haddock comment. Maybe move the comment on the implementation to accompany the actual implementation and add a haddock comment that is more generic/higher level.

• Change the order of exports in Type.hs so that each function accompanies the one it implements.

• Add more context for the changes in the commit messages (excluding the CHANGELOG commits).

• Change the alignment of Volts and deriving Generic in the example to have deriving Generic in a new line, indented 2 spaces, and the definition above indented 4 spaces.

• In StructUpdateField.hs, since the pragmas were misaligned, do not align them.

• Rebase on top of master.

• Consider using this alternative version of convert that also handles acronyms. Feel free to simplify it or improve it further.

convert3 :: String -> String
convert3 = convert3' True True

convert3' :: Bool   -- ^ Is this the first letter
          -> Bool   -- ^ Was the previous letter capital
          -> String -- ^ Remainder of the string
          -> String
convert3' _ _ []     = []
convert3' _ v (x:[])
  | v && isUpper x = toLower x : []
  | isUpper x      = '_' : toLower x : []
  | otherwise      = x : []
convert3' b v (x1:x2:xs)
  | not b && isUpper x1 && (isLower x2 || not v)
  = '_' : toLower x1 : convert3' False (isUpper x1) (x2:xs)
  | otherwise
  = toLower x1 : convert3' False (isUpper x1) (x2:xs)

[RyanGlScott]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:
  • The code proposed compiles and passes all tests. Details:
    Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/273752793
  • The solution proposed produces the expected result. Details:
    The following Dockerfile checks that the new methods can be used in place of the hand-coded implementations of the Struct and Typed class methods, by comparing the results produced against known expectations, and it also that the examples updated to illustrate the new features compile successfully, after which it prints the message "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
    RUN apt-get install --yes z3
    
    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 Structs.hs /tmp/Structs.hs
    ADD main.c /tmp/main.c
    ADD expected /tmp/expected
    
    CMD git clone $REPO \
        && cd $NAME \
        && git checkout $COMMIT \
        && cabal v1-sandbox init \
        && cabal v1-install alex happy --constraint='happy < 2' \
        && cabal v1-install copilot**/ \
        && cabal v1-exec -- runhaskell /tmp/Structs.hs \
        && mv /tmp/main.c . \
        && gcc main.c structs.c -o main \
        && ./main > actual \
        && diff actual /tmp/expected \
        && cabal v1-exec -- runhaskell copilot/examples/Structs.hs \
        && cabal v1-exec -- runhaskell copilot/examples/StructsUpdateField.hs \
        && cabal v1-exec -- runhaskell copilot/examples/what4/Structs.hs \
        && echo Success
    
    --- Structs.hs
    {-# LANGUAGE DataKinds         #-}
    {-# LANGUAGE GADTs             #-}
    {-# LANGUAGE DeriveGeneric     #-}
    {-# LANGUAGE NoImplicitPrelude #-}
    module Main (main) where
    
    import Copilot.Compile.C99
    import Data.Type.Equality  as DE
    import Language.Copilot
    import GHC.Generics
    
    -- * Struct type definitions
    
    data SoA = SoA
        { arr :: Field "arr" SoB
        }
      deriving Generic
    
    instance Struct SoA where
      typeName = typeNameDefault
      toValues = toValuesDefault
    
    instance Typed SoA where
      typeOf = typeOfDefault
    
    data SoB = SoB
        { arr2 :: Field "arr2" (Array 3 Float)
        }
      deriving Generic
    
    instance Struct SoB where
      typeName = typeNameDefault
      toValues = toValuesDefault
    
    instance Typed SoB where
      typeOf = typeOfDefault
    
    data SoC = SoC
        { arr3 :: Field "arr3" Int32
        }
      deriving Generic
    
    -- | Struct with a custom value for updates
    instance Struct SoC where
      typeName = typeNameDefault
      toValues = toValuesDefault
      updateField = updateFieldDefault
    
    instance Typed SoC where
      typeOf = typeOfDefault
    
    -- Sample values
    
    -- We purposefully leave some type signatures out to check that GHC can infer
    -- them.
    
    -- SoAs
    a1 = SoA $ Field $ SoB $ Field $ array [0, 1, 2]
    b1 = SoB $ Field $ array [10, 20, 30]
    b2 = SoB $ Field $ array [40, 50, 60]
    c1 = SoC $ Field 5
    
    soa :: Stream SoA
    soa = constant a1
    
    soa1  = soa ## arr =: recursiveArray
    soa2  = soa ## arr =: constant b1
    soarr = soa ## arr =: soa # arr
    soc1   = constant c1 ## arr3 =: counter
    soc2   = constant c1 ## arr3 =$ (+5)
    
    recursiveArray :: Stream SoB
    recursiveArray = [b1, b2] ++ recursiveArray
    
    counter :: Stream Int32
    counter = [55] ++ (counter + 1)
    
    spec :: Spec
    spec = do
      trigger "arrays" (soa1 # arr # arr2 ! 1 /= 60) [arg soa, arg soa1, arg soa2]
      trigger "arrays2" true [arg soc1]
      trigger "arrays3" true [arg soc2]
    
    main :: IO ()
    main = do
      spec' <- reify spec
      compile "structs" spec'
    
    --- main.c
    #include <stdio.h>
    #include <stdlib.h>
    #include <stdint.h>
    #include "structs.h"
    #include "structs_types.h"
    
    void arrays( struct so_a * arrays_arg0
               , struct so_a * arrays_arg1
               , struct so_a * arrays_arg2
               ) {
      printf("0: %f %f %f\n"
            , arrays_arg0->arr.arr2[0]
            , arrays_arg0->arr.arr2[1]
            , arrays_arg0->arr.arr2[2]);
    
      printf("1: %f %f %f\n"
            , arrays_arg1->arr.arr2[0]
            , arrays_arg1->arr.arr2[1]
            , arrays_arg1->arr.arr2[2]);
    
      printf("2: %f %f %f\n"
            , arrays_arg2->arr.arr2[0]
            , arrays_arg2->arr.arr2[1]
            , arrays_arg2->arr.arr2[2]);
    }
    
    void arrays2(struct so_c * arrays2_arg0) {
      printf("soc1: %d\n", arrays2_arg0->arr3);
    }
    
    void arrays3(struct so_c * arrays2_arg0) {
      printf("soc2: %d\n", arrays2_arg0->arr3);
    }
    
    int main() {
      step();
      step();
      step();
      step();
    }
    
    --- expected
    0: 0.000000 1.000000 2.000000
    1: 10.000000 20.000000 30.000000
    2: 10.000000 20.000000 30.000000
    soc1: 55
    soc2: 10
    0: 0.000000 1.000000 2.000000
    1: 40.000000 50.000000 60.000000
    2: 10.000000 20.000000 30.000000
    soc1: 56
    soc2: 10
    0: 0.000000 1.000000 2.000000
    1: 10.000000 20.000000 30.000000
    2: 10.000000 20.000000 30.000000
    soc1: 57
    soc2: 10
    0: 0.000000 1.000000 2.000000
    1: 40.000000 50.000000 60.000000
    2: 10.000000 20.000000 30.000000
    soc1: 58
    soc2: 10
    

    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=cbab0cca637753b68d0d775095ab97f5a87937e0" -it copilot-verify-564
    

• Implementation is documented. Details:
  The new classes, instances and examples all include documentation.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  New examples are included, and existing examples are updated to use the new, simpler methods.
• Required version bumps are evaluated. Details:
  No bump required; the new features are backwards compatible.