various fixes

Author: flupe

src/Agda2Hs/Compile/Data.hs

@@ -24,8 +24,7 @@ checkNewtype :: Hs.Name () -> [Hs.QualConDecl ()] -> C ()
 checkNewtype name cs = do
   checkSingleElement name cs "Newtype must have exactly one constructor in definition"
   case head cs of
-    Hs.QualConDecl () _ _ (Hs.ConDecl () cName types)
-      -> checkSingleElement cName types "Newtype must have exactly one field in constructor"
+    Hs.QualConDecl () _ _ (Hs.ConDecl () cName types) -> checkNewtypeCon cName types
 
 compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()]
 compileData newtyp ds def = do

src/Agda2Hs/Compile/Function.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE OverloadedStrings, ViewPatterns, NamedFieldPuns, BlockArguments #-}
+{-# LANGUAGE OverloadedStrings #-}
 module Agda2Hs.Compile.Function where
 
 import Control.Monad ( (>=>), filterM, forM_ )
@@ -116,6 +116,7 @@ compileFun withSig def@Defn{..} =
     $ withFunctionLocals defName
     $ compileFun' withSig def
 
+-- inherit existing (instantiated) locals
 compileFun' withSig def@Defn{..} = do
   reportSDoc "agda2hs.compile" 6 $ "Compiling function: " <+> prettyTCM defName
 

src/Agda2Hs/Compile/Record.hs

@@ -110,7 +110,7 @@ compileRecord target def = do
       ToRecord newtyp ds -> do
         checkValidConName cName
         (constraints, fieldDecls) <- compileRecFields fieldDecl recFields fieldTel
-        when newtyp $ checkSingleElement cName fieldDecls "Newtype must have exactly one field in constructor"
+        when newtyp $ checkNewtypeCon cName fieldDecls
         let target = if newtyp then Hs.NewType () else Hs.DataType ()
         compileDataRecord constraints fieldDecls target hd ds
 

src/Agda2Hs/Compile/Type.hs

@@ -43,7 +43,7 @@ import Agda2Hs.HsUtils
 
 -- | Type definitions from the prelude that get special translation rules.
 isSpecialType :: QName -> Maybe (Elims -> C (Hs.Type ()))
-isSpecialType x = case prettyShow x of
+isSpecialType = prettyShow >>> \case
   "Haskell.Prim.Tuple._×_"    -> Just tupleType
   "Haskell.Prim.Tuple._×_×_"  -> Just tupleType
   "Haskell.Extra.Erase.Erase" -> Just unitType
@@ -119,8 +119,8 @@ compileTopLevelType keepType t cont = do
 
 
 -- | Compile an Agda term into a Haskell type, along with its strictness.
-compileTypeStrictness :: Term -> C (Strictness, Hs.Type ())
-compileTypeStrictness t = do
+compileTypeWithStrictness :: Term -> C (Strictness, Hs.Type ())
+compileTypeWithStrictness t = do
   s <- case t of
     Def f es -> fromMaybe Lazy <$> isUnboxRecord f
     _        -> return Lazy
@@ -214,7 +214,7 @@ compileDom :: ArgName -> Dom Type -> C CompiledDom
 compileDom x a
   | usableModality a = case getHiding a of
       Instance{} -> DomConstraint . Hs.TypeA () <$> compileType (unEl $ unDom a)
-      NotHidden  -> uncurry DomType <$> compileTypeStrictness (unEl $ unDom a)
+      NotHidden  -> uncurry DomType <$> compileTypeWithStrictness (unEl $ unDom a)
       Hidden     ->
         ifM (canErase $ unDom a)
             (return DomDropped)

src/Agda2Hs/Compile/Types.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE PatternSynonyms, FlexibleInstances, MultiParamTypeClasses, InstanceSigs, TypeFamilies  #-}
+{-# LANGUAGE PatternSynonyms, FlexibleInstances, MultiParamTypeClasses, TypeFamilies #-}
 module Agda2Hs.Compile.Types where
 
 import Control.Applicative ( liftA2 )
@@ -177,14 +177,14 @@ instance Semigroup a => Semigroup (C a) where (<>) = liftA2 (<>)
 
 
 
--- | Currently we can compile an Agda "Dom Type" in three ways:
--- To a type in Haskell (with perhaps a strictness annotation)
--- To a typeclass constraint in Haskell
--- To nothing (e.g. for proofs)
+-- | Agda @Dom Type@ can get compiled in three ways.
 data CompiledDom
   = DomType Strictness (Hs.Type ())
+    -- ^ To a Haskell type (with perhaps a strictness annotation)
   | DomConstraint (Hs.Asst ())
+    -- ^ To a typeclass constraint
   | DomDropped
+    -- ^ To nothing (e.g. erased proofs)
 
 -- | Whether a datatype/record should be compiled as a @newtype@ haskell definition.
 type AsNewType = Bool

src/Agda2Hs/Compile/Utils.hs

@@ -134,7 +134,7 @@ keepArg x = usableModality x && visible x
 
 
 keepClause :: Clause -> Bool
-keepClause = maybe False keepArg . clauseType
+keepClause = any keepArg . clauseType
 
 -- Determine whether it is ok to erase arguments of this type,
 -- even in the absence of an erasure annotation.
@@ -302,6 +302,10 @@ checkSingleElement :: Hs.Name () -> [b] -> String -> C ()
 checkSingleElement name fs s = unless (length fs == 1) $ genericDocError =<< do
   text (s ++ ":") <+> text (Hs.prettyPrint name)
 
+checkNewtypeCon :: Hs.Name () -> [b] -> C ()
+checkNewtypeCon name tys =
+  checkSingleElement name tys "Newtype must have exactly one field in constructor"
+
 checkingVars :: C a -> C a
 checkingVars = local $ \e -> e { checkVar = True }
 

src/Agda2Hs/HsUtils.hs

@@ -297,7 +297,7 @@ constrainType c = \case
 
 -- | Add explicit quantification over a variable to a Haskell type.
 qualifyType
-  :: String     -- ^ Name of the variable.
+  :: String  -- ^ Name of the variable.
   -> Type () -- ^ Type to quantify.
   -> Type ()
 qualifyType s = \case