Merge remote-tracking branch 'galois/develop-generic-struct-typed-methods'. Close #564.

**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.

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

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
```

**Solution implemented**

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`.

Update the examples in 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.

Author: ivanperez-keera

copilot-core/CHANGELOG

@@ -1,6 +1,7 @@
-2024-12-29
+2025-01-06
         * Deprecate fields of Copilot.Core.Expr.UExpr. (#565)
         * Increase test coverage. (#555)
+        * Define generic implementations of Struct and Typed methods. (#564)
 
 2024-11-07
         * Version bump (4.1). (#561)

copilot-core/src/Copilot/Core/Type.hs

@@ -4,8 +4,9 @@
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE KindSignatures            #-}
-{-# LANGUAGE Safe                      #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE Trustworthy               #-}
+{-# LANGUAGE TypeApplications          #-}
 {-# LANGUAGE TypeOperators             #-}
 {-# LANGUAGE UndecidableInstances      #-}
 -- |
@@ -20,6 +21,7 @@
 module Copilot.Core.Type
     ( Type (..)
     , Typed (..)
+    , typeOfDefault
     , UType (..)
     , SimpleType (..)
 
@@ -28,25 +30,32 @@ module Copilot.Core.Type
 
     , Value (..)
     , toValues
+    , toValuesDefault
     , Field (..)
     , typeName
+    , typeNameDefault
 
     , Struct
     , fieldName
     , accessorName
     , updateField
+    , updateFieldDefault
     )
   where
 
 -- External imports
+import Data.Char          (isLower, isUpper, toLower)
+import Data.Coerce        (coerce)
 import Data.Int           (Int16, Int32, Int64, Int8)
 import Data.List          (intercalate)
 import Data.Proxy         (Proxy (..))
 import Data.Type.Equality as DE
 import Data.Typeable      (Typeable, eqT, typeRep)
 import Data.Word          (Word16, Word32, Word64, Word8)
+import GHC.Generics       (Datatype (..), D1, Generic (..), K1 (..), M1 (..),
+                           U1 (..), (:*:) (..))
 import GHC.TypeLits       (KnownNat, KnownSymbol, Symbol, natVal, sameNat,
-                           symbolVal)
+                           sameSymbol, symbolVal)
 
 -- Internal imports
 import Copilot.Core.Type.Array (Array)
@@ -61,24 +70,35 @@ class Struct a where
   toValues :: a -> [Value a]
 
   -- | Update the value of a struct field. This is only used by the Copilot
-  -- interpreter, so if you do not plan to use the interpreter, it is safe to
-  -- omit an implementation of this method.
+  -- interpreter.
   --
-  -- In order to implement 'updateField', you should do the following for each
-  -- 'Field' in a struct:
+  -- If you do not plan to use the interpreter, you can omit an implementation
+  -- of this method. If you do so, it is recommended that you derive a 'Generic'
+  -- instance for the struct data type. This is because in a future release, the
+  -- default implementation of 'updateField' (which will be picked if there is
+  -- not a manually written implementation) will be changed to require a
+  -- 'Generic' instance.
   --
-  -- 1. Check that the name of the 'Field' matches the name of the supplied
-  --    'Value' (using 'GHC.TypeLits.sameSymbol').
+  -- In order to implement 'updateField', pick one of the following approaches:
   --
-  -- 2. Check that the type of the 'Field' matches the 'Type' of the supplied
-  --    'Value' (using 'DE.testEquality').
+  -- * Derive a 'Generic' instance for the struct data type and then define
+  --   @'updateField' = 'updateFieldDefault'@ in the 'Struct' instance.
   --
-  -- 3. If both (1) and (2) succeed, update the corresponding struct field using
-  --    a record update.
+  -- * Manually implement 'updateField' by doing the following for each 'Field'
+  --   in a struct:
   --
-  -- For a complete end-to-end example that demonstrates how to implement
-  -- 'updateField' and use it in the Copilot interpreter, see the
-  -- @examples/StructsUpdateField.hs@ example in the @copilot@ library.
+  --   1. Check that the name of the 'Field' matches the name of the supplied
+  --      'Value' (using 'GHC.TypeLits.sameSymbol').
+  --
+  --   2. Check that the type of the 'Field' matches the 'Type' of the supplied
+  --      'Value' (using 'DE.testEquality').
+  --
+  --   3. If both (1) and (2) succeed, update the corresponding struct field
+  --      using a record update.
+  --
+  --   For a complete end-to-end example that demonstrates how to manually
+  --   implement 'updateField' and use it in the Copilot interpreter, see the
+  --   @examples/StructsUpdateField.hs@ example in the @copilot@ library.
   updateField :: a -> Value t -> a
   updateField = error $ unlines
     [ "Field updates not supported for this type."
@@ -272,3 +292,163 @@ data UType = forall a . Typeable a => UType { uTypeType :: Type a }
 
 instance Eq UType where
   UType ty1 == UType ty2 = typeRep ty1 == typeRep ty2
+
+-- * GHC.Generics-based defaults
+
+-- | A default implementation of 'typeName' that leverages 'Generic'. In order
+-- to use this, make sure you derive a 'Generic' instance for your data type and
+-- then define @'typeName' = 'typeNameDefault'@ in its 'Struct' instance.
+--
+-- This generates a struct name that consists of the name of the original
+-- Haskell data type, but converted to snake_case.
+typeNameDefault :: (Generic a, GDatatype (Rep a)) => a -> String
+typeNameDefault = convert . gTypeName . from
+  where
+    convert :: String -> String
+    convert = convert' True True
+
+    convert' :: Bool   -- ^ Is this the first letter
+             -> Bool   -- ^ Was the previous letter capital
+             -> String -- ^ Remainder of the string
+             -> String
+    convert' _ _ []    = []
+    convert' _ v [x]
+      | v && isUpper x = toLower x : []
+      | isUpper x      = '_' : toLower x : []
+      | otherwise      = x : []
+    convert' b v (x1:x2:xs)
+      | not b && isUpper x1 && (isLower x2 || not v)
+      = '_' : toLower x1 : convert' False (isUpper x1) (x2:xs)
+      | otherwise
+      = toLower x1 : convert' False (isUpper x1) (x2:xs)
+
+-- | A default implementation of 'toValues' that leverages 'Generic'. In order
+-- to use this, make sure you derive a 'Generic' instance for your data type and
+-- then define @'toValues' = 'toValuesDefault'@ in its 'Struct' instance.
+toValuesDefault :: (Generic a, GStruct (Rep a)) => a -> [Value a]
+toValuesDefault x = coerce $ gToValues $ from x
+
+-- | A default implementation of 'updateField' that leverages 'Generic'. In
+-- order to use this, make sure you derive a 'Generic' instance for your data
+-- type and then define @'updateField' = 'updateFieldDefault'@ in its 'Struct'
+-- instance.
+updateFieldDefault :: (Generic a, GStruct (Rep a)) => a -> Value t -> a
+updateFieldDefault a v@(Value _ field)
+    | updated   = to a'
+    | otherwise = error $ "Unexpected field: " ++ show field
+  where
+    (a', updated) = gUpdateField (from a) v
+
+-- | A default implementation of 'typeOf' that leverages 'Generic'. In order to
+-- use this, make sure you derive a 'Generic' instance for your data type and
+-- then define @'typeOf' = 'typeOfDefault'@ in its 'Typed' instance.
+typeOfDefault ::
+  forall a. (Typed a, Struct a, Generic a, GTypedStruct (Rep a)) => Type a
+typeOfDefault = Struct $ to $ gStructPlaceholder @(Rep a) @()
+
+-- ** Generic-based classes (not exported)
+
+-- | Capture the name of a Haskell data type from its 'Generic' metadata.
+class GDatatype f where
+  -- | Returns the name of a Haskell data type. (Note that this differs from
+  -- 'typeName', which is expected to return the name of the struct in the
+  -- /target/ language).
+  gTypeName :: f p -> String
+
+-- | The only 'GDatatype' instance we need is for 'D1', which describes
+-- 'Datatype' metadata (@d@). We ignore all other metadata (@_f@).
+instance Datatype d => GDatatype (D1 d _f) where
+  gTypeName = datatypeName
+
+-- | Perform struct-related operations on 'Generic' representation types.
+class GStruct f where
+  -- | Transforms all the struct representation's fields into a list of values.
+  gToValues :: f p -> [Value (f p)]
+
+  -- | Update the value of a struct representation's field. This returns two
+  -- things:
+  --
+  -- 1. @f p@: The struct representation, but with the field updated.
+  --
+  -- 2. 'Bool': This is 'True' if the field was successfully updated and 'False'
+  --    otherwise. If this returns 'False', it is the responsibility of the
+  --    caller to raise an error.
+  gUpdateField :: f p -> Value t -> (f p, Bool)
+
+-- | 'U1' represents a data constructor with no fields. As such, 'gToValues'
+-- returns an empty list of 'Value's, and 'gUpdateField' does not update
+-- anything.
+instance GStruct U1 where
+  gToValues U1 = []
+  gUpdateField u _ = (u, False)
+
+-- | 'M1' is only used to store metadata, which the 'GStruct' class does not
+-- make use of. As such, this instance discards the metadata and recurses.
+instance GStruct f => GStruct (M1 _i _c f) where
+  gToValues (M1 x) = coerce (gToValues x)
+  gUpdateField (M1 x) v = (M1 x', updated)
+    where
+      (x', updated) = gUpdateField x v
+
+-- | @(':*:')@ represents a data constructor with multiple fields.
+instance (GStruct f, GStruct g) => GStruct (f :*: g) where
+  -- Recursively compute two lists of Values and append them.
+  gToValues (f :*: g) = coerce (gToValues f) ++ coerce (gToValues g)
+  -- Recursively attempt to update the field in both branches and combine the
+  -- updated branches. We will have successfully updated the field if either
+  -- branch was successfully updated.
+  gUpdateField (f :*: g) v = (f' :*: g', updatedF || updatedG)
+    where
+      (f', updatedF) = gUpdateField f v
+      (g', updatedG) = gUpdateField g v
+
+-- | 'K1' represents a single field in a data constructor. This is the base
+-- case.
+instance (KnownSymbol name, Typed ty, c ~ Field name ty) =>
+    GStruct (K1 _i c) where
+  -- Now that we have the field, return it in a singleton list.
+  gToValues (K1 field) = [Value typeOf field]
+  -- In order to update the field, we check that the field names and types
+  -- match. If they do, return the updated field and declare the update as
+  -- successful. Otherwise, return the old field and declare the update as
+  -- unsuccessful.
+  gUpdateField (K1 oldField) (Value newTy (newField :: Field newName newTy)) =
+    case (sameSymbol pName pNewName, testEquality ty newTy) of
+      (Just Refl, Just Refl) -> (K1 newField, True)
+      _                      -> (K1 oldField, False)
+    where
+      pName    = Proxy @name
+      pNewName = Proxy @newName
+      ty       = typeOf @ty
+
+-- | Compute a 'Generic' placeholder value to use for a struct type.
+class GTypedStruct f where
+  -- | A placeholder value to supply to use in a generic implementation of
+  -- 'typeOf' for a struct type.
+  gStructPlaceholder :: f p
+
+-- | 'U1' represents a data constructor with no fields. As such,
+-- 'gStructPlaceholder' simply returns the data constructor with no other
+-- information.
+instance GTypedStruct U1 where
+  gStructPlaceholder = U1
+
+-- | 'M1' is only used to store metadata, which the 'GTypedStruct' class does
+-- not make use of. As such, this instance recursively computes a placeholder
+-- value without inspecting the metadata.
+instance GTypedStruct f => GTypedStruct (M1 _i _c f) where
+  gStructPlaceholder = M1 gStructPlaceholder
+
+-- | @(':*:')@ represents a data constructor with multiple fields. As such,
+-- 'gStructPlaceholder' recursively computes placeholders for each field and
+-- combines them into the overall data constructor.
+instance (GTypedStruct f, GTypedStruct g) => GTypedStruct (f :*: g) where
+  gStructPlaceholder = gStructPlaceholder :*: gStructPlaceholder
+
+-- | 'K1' represents a single field in a data constructor. This is the base
+-- case. This instance computes a placeholder value that works for any field of
+-- any type.
+instance (c ~ Field name ty) => GTypedStruct (K1 _i c) where
+  -- We use 'undefined' as the actual value for the 'Field' because Copilot
+  -- never inspects the value.
+  gStructPlaceholder = K1 $ Field undefined

copilot/CHANGELOG

@@ -1,5 +1,6 @@
-2025-01-02
+2025-01-06
         * Bump upper version constraint on filepath. (#570)
+        * Update struct examples to use generic method implementations. (#564)
 
 2024-11-07
         * Version bump (4.1). (#561)

copilot/examples/Structs.hs

@@ -1,28 +1,29 @@
 -- | An example showing how specifications involving structs (in particular,
 -- nested structs) are compiled to C using copilot-c99.
 
-{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DataKinds     #-}
+{-# LANGUAGE DeriveGeneric #-}
 
 module Main where
 
 import qualified Prelude as P
 import Control.Monad (void, forM_)
+import GHC.Generics (Generic)
 
 import Language.Copilot
 import Copilot.Compile.C99
 
 -- | Definition for `Volts`.
 data Volts = Volts
-  { numVolts :: Field "numVolts" Word16
-  , flag     :: Field "flag"     Bool
-  }
+    { numVolts :: Field "numVolts" Word16
+    , flag     :: Field "flag"     Bool
+    }
+  deriving Generic
 
 -- | `Struct` instance for `Volts`.
 instance Struct Volts where
-  typeName _ = "volts"
-  toValues volts = [ Value Word16 (numVolts volts)
-                   , Value Bool   (flag volts)
-                   ]
+  typeName = typeNameDefault
+  toValues = toValuesDefault
   -- Note that we do not implement `updateField` here. `updateField` is only
   -- needed to make updates to structs work in the Copilot interpreter, and we
   -- do not use the interpreter in this example. (See
@@ -31,29 +32,25 @@ instance Struct Volts where
 
 -- | `Volts` instance for `Typed`.
 instance Typed Volts where
-  typeOf = Struct (Volts (Field 0) (Field False))
+  typeOf = typeOfDefault
 
 data Battery = Battery
-  { temp  :: Field "temp"  Word16
-  , volts :: Field "volts" (Array 10 Volts)
-  , other :: Field "other" (Array 10 (Array 5 Word32))
-  }
+    { temp  :: Field "temp"  Word16
+    , volts :: Field "volts" (Array 10 Volts)
+    , other :: Field "other" (Array 10 (Array 5 Word32))
+    }
+  deriving Generic
 
 -- | `Battery` instance for `Struct`.
 instance Struct Battery where
-  typeName _ = "battery"
-  toValues battery = [ Value typeOf (temp battery)
-                     , Value typeOf (volts battery)
-                     , Value typeOf (other battery)
-                     ]
+  typeName = typeNameDefault
+  toValues = toValuesDefault
   -- Note that we do not implement `updateField` here for the same reasons as in
   -- the `Struct Volts` instance above.
 
--- | `Battery` instance for `Typed`. Note that `undefined` is used as an
--- argument to `Field`. This argument is never used, so `undefined` will never
--- throw an error.
+-- | `Battery` instance for `Typed`.
 instance Typed Battery where
-  typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined))
+  typeOf = typeOfDefault
 
 spec :: Spec
 spec = do