Copilot-Language/copilot

`copilot-core`: Facilitate use of structs

Closed this issue · 9 comments

ivanperez-keera commented

Description

Currently, using structs in Copilot requires defining instances of several type classes. Defining those instances is unnecessarily cumbersome, and it exposes the user to a substantial amount of Haskell even when they want to stay at the level of the Copilot language.

It would be helpful to facilitate generating instances of Typed and Struct for struct types / record types, by providing functions that implement the default behavior and only requiring users to write their own functions if they wanted to deviate from those defaults.

Type

  • Feature: Improve usability of the language.

Additional context

None.

Requester

  • Ivan Perez.

Method to check presence of bug

Not applicable (not a bug).

Expected result

Introduce functions that implement the default behavior for the methods in the Typed and Struct type classes, so that users can rely on them when implementing their own instances.

Desired result

Introduce functions that implement the default behavior for the methods in the Typed and Struct type classes, so that users can rely on them when implementing their own instances.

Proposed solution

Introduce four definitions in copilot-core:Copilot.Core.Type that provide default implementations for the fields in the Typed and Struct type classes for types that are Generic. Let users use those types so long as they make their structs Generic.

Add an example to the examples directory in copilot that shows how the new implementations can be used.

Further notes

Discussion #540 proposes multiple alternative implementations. Although the preferred solution long-term is 2, the mechanism proposed is not backwards compatible, so it helps to first introduce a mechanism to simplify the implementation without breaking existing code. We can, upon release of this feature, communicate to users that Copilot will move in that direction if appropriate, and encourage users to transition their code so that we can introduce breaking changes 3 versions later per our deprecation policy.

ivanperez-keera commented

Change Manager: Confirmed that the issue exists.

ivanperez-keera commented

Technical Lead: Confirmed that the issue should be addressed.

ivanperez-keera commented

Technical Lead: Issue scheduled for fixing in Copilot 4.2

Fix assigned to: @RyanGlScott .

RyanGlScott commented

Just to be explicit about what I am planning to do for the next release (and to relate it back to the original discussion in #540), my plan is to add the following four functions to Copilot.Core.Type:

  • typeNameDefault :: (Generic a, ...) => a -> String
  • toValuesDefault :: (Generic a, ...) => a -> [Value a]
  • updateFieldDefault :: (Generic a, ...) => a -> Value t -> a
  • typeOfDefault :: (Typed a, Struct a, Generic a, ...) => Type a

Note the following differences from the proposal in #540:

  1. The naming convention is slightly different: I've moved "default" to the end of each function instead of at the beginning.
  2. There is now a default for typeName. This differs from #540, where I envisioned that users would always supply the generated struct name manually. After talking about this with @ivanperez-keera, however, we came to the consensus that most of the time, it would be more convenient just to generate a typeName that converts the name of the Haskell datatype to snake_case (e.g., convert the name FooBar to foo_bar). This is not the only possible way to do it, but we can always add alternative ways to do it later.
  3. In light of having a dedicated typeNameDefault function, I propose not adding a GenericStruct newtype. It was mainly useful to allow users to easily specify the generated type name in conjunction with deriving, but now that we have a reasonable default for typeName, users won't need to perform this extra step in the first place.
  • 👍1
ivanperez-keera commented

Thank you, @RyanGlScott . This looks good.

Please let me know when you start working on this so that I switch it to "Implementation".

RyanGlScott commented

I have a partial implementation of this (based on the work in #516). I'm currently cleaning it up and documenting it, so feel free to switch this to "Implementation".

RyanGlScott commented

Implementor: Solution implemented, review requested.

ivanperez-keera commented

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.
ivanperez-keera commented

Change Manager: Implementation ready to be merged.