Skip to content

Commit

Permalink
Add OverloadedStrings to Record for simplicity
Browse files Browse the repository at this point in the history
  • Loading branch information
naucke committed Sep 23, 2024
1 parent f636b3d commit 691eb44
Showing 1 changed file with 8 additions and 7 deletions.
15 changes: 8 additions & 7 deletions src/Agda2Hs/Compile/Record.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE OverloadedStrings #-}
module Agda2Hs.Compile.Record where

import Control.Monad ( unless, when )
Expand Down Expand Up @@ -82,7 +83,7 @@ compileMinRecords def sls = do
| all (x ==) xs = return x
| otherwise = genericDocError =<< do
text ("Conflicting default implementations for " ++ pp f ++ ":") $$
vcat [ text "-" <+> multilineText (pp d) | d <- nub (x : xs) ]
vcat [ "-" <+> multilineText (pp d) | d <- nub (x : xs) ]
decls <- Map.traverseWithKey getUnique
$ Map.unionsWith (<>) $ (map . fmap) (:| []) defaults

Expand Down Expand Up @@ -177,23 +178,23 @@ checkUnboxPragma def = do
-- recRecursive can be used again after agda 2.6.4.2 is released
-- see agda/agda#7042
unless (all null recMutual) $ genericDocError
=<< text "Unboxed record" <+> prettyTCM (defName def)
<+> text "cannot be recursive"
=<< "Unboxed record" <+> prettyTCM (defName def)
<+> "cannot be recursive"

TelV tel _ <- telViewUpTo recPars (defType def)
addContext tel $ do
pars <- getContextArgs
let fieldTel = recTel `apply` pars
fields <- nonErasedFields fieldTel
unless (length fields == 1) $ genericDocError
=<< text "Unboxed record" <+> prettyTCM (defName def)
<+> text "should have exactly one non-erased field"
=<< "Unboxed record" <+> prettyTCM (defName def)
<+> "should have exactly one non-erased field"

where
nonErasedFields :: Telescope -> C [String]
nonErasedFields EmptyTel = return []
nonErasedFields (ExtendTel a tel) = compileDom a >>= \case
DODropped -> underAbstraction a tel nonErasedFields
DOType -> genericDocError =<< text "Type field in unboxed record not supported"
DOInstance -> genericDocError =<< text "Instance field in unboxed record not supported"
DOType -> genericDocError =<< "Type field in unboxed record not supported"
DOInstance -> genericDocError =<< "Instance field in unboxed record not supported"
DOTerm -> (absName tel:) <$> underAbstraction a tel nonErasedFields

0 comments on commit 691eb44

Please sign in to comment.