Skip to content

Commit

Permalink
[ fix #212 ] Be more flexible with unboxed records
Browse files Browse the repository at this point in the history
  • Loading branch information
flupe authored and omelkonian committed Nov 6, 2023
1 parent 9883f96 commit 330333c
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 4 deletions.
13 changes: 9 additions & 4 deletions src/Agda2Hs/Compile/Record.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE NamedFieldPuns #-}
module Agda2Hs.Compile.Record where

import Control.Monad ( unless )
Expand Down Expand Up @@ -168,7 +169,11 @@ compileRecord target def = setCurrentRange (nameBindingSite $ qnameName $ defNam
return $ Hs.DataDecl () don Nothing hd [conDecl] ds

checkUnboxPragma :: Defn -> C ()
checkUnboxPragma def@Record{ recFields = (f:fs) }
| keepArg f , all (not . keepArg) fs , not (recRecursive def) = return ()
checkUnboxPragma _ = genericError $
"An unboxed type must be a non-recursive record type with exactly one non-erased field."
checkUnboxPragma def
| Record{recFields} <- def
, length (filter keepArg recFields) == 1
, not (recRecursive def)
= return ()

| otherwise
= genericError "An unboxed type must be a non-recursive record type with exactly one non-erased field."
7 changes: 7 additions & 0 deletions test/UnboxPragma.agda
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,13 @@ open ∃ public

{-# COMPILE AGDA2HS ∃ unboxed #-}

record Σ0 (A : Set) (P : @0 A Set) : Set where
field
@0 el : A
pf : P el

{-# COMPILE AGDA2HS Σ0 unboxed #-}

postulate
IsSorted : List Int Set
looksfine : {xs : List Int} IsSorted xs
Expand Down

0 comments on commit 330333c

Please sign in to comment.