Fix projection on sum-of-product types (#340)

Fixes #310.
This commit is contained in:
Martin Huschenbett 2019-04-09 21:25:33 +02:00 committed by Neil Mitchell
parent 6a1659047f
commit 1db23f9568
2 changed files with 10 additions and 4 deletions

View File

@ -566,7 +566,11 @@ convertExpr env0 e = do
go env (VarIs "getFieldPrim") (Type (isStrLitTy -> Just name) : Type record : Type _field : args) = fmap (, args) $ do
record' <- convertType env record
pure $ ETmLam (varV1, record') $ ERecProj (fromTCon record') (mkField $ unpackFS name) $ EVar varV1
go env (VarIs "getField") (Type (isStrLitTy -> Just name) : Type recordType : Type _fieldType : _dict : record : args) = fmap (, args) $ do
-- NOTE(MH): We only inline `getField` for record types. This is required
-- for contract keys. Projections on sum-of-records types have to through
-- the type class for `getField`.
go env (VarIs "getField") (Type (isStrLitTy -> Just name) : Type recordType@(TypeCon recordTyCon _) : Type _fieldType : _dict : record : args)
| Just [_] <- tyConDataCons_maybe recordTyCon = fmap (, args) $ do
recordType <- convertType env recordType
record <- convertExpr env record
pure $ ERecProj (fromTCon recordType) (mkField $ unpackFS name) record

View File

@ -11,6 +11,8 @@ data SumOfProducts
deriving (Eq,Ord)
main = scenario do
alice <- getParty "alice"
submit alice $ assert $ Sum1 3 "test" /= Sum2
submit alice $ assert $ Sum1 3 "test" < Sum2
let sum1 = Sum1 3 "test"
let sum3 = Sum3 3 None True
assert $ sum1 /= Sum2
assert $ sum1 < Sum2
assert $ sum1.field1 == sum3.field1