Skip to content

Commit 59d8c2a

Browse files
jespercockxjespercockx
committed
[ fix #324 ] Keep track of instance-only imports
1 parent f2fef22 commit 59d8c2a

File tree

15 files changed

+120
-59
lines changed

15 files changed

+120
-59
lines changed

‎src/Agda2Hs/Compile/ClassInstance.hs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
3636
import Agda2Hs.AgdaUtils
3737
import Agda2Hs.Compile.Function
3838
import Agda2Hs.Compile.Name
39+
import Agda2Hs.Compile.Term
3940
import Agda2Hs.Compile.Type
4041
import Agda2Hs.Compile.Types
4142
import Agda2Hs.Compile.Utils

‎src/Agda2Hs/Compile/Imports.hs‎

Lines changed: 20 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -25,10 +25,12 @@ type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap
2525

2626
compileImports :: String -> Imports -> TCM [Hs.ImportDecl ()]
2727
compileImports top is0 = do
28-
let is = filter (not . (top ==) . Hs.prettyPrint . importModule) is0
28+
let is = filter ((top /=) . Hs.prettyPrint . importModule) is0
2929
checkClashingImports is
3030
let imps = Map.toList $ groupModules is
31-
return $ map (uncurry $ uncurry makeImportDecl) imps
31+
reportSLn "agda2hs.import" 10 $ "All imported modules: " ++ show (map (pp . fst . fst) imps)
32+
let decls = map (uncurry $ uncurry makeImportDecl) imps
33+
return decls
3234
where
3335
mergeChildren :: ImportSpecMap -> ImportSpecMap -> ImportSpecMap
3436
mergeChildren = Map.unionWith Set.union
@@ -38,18 +40,20 @@ compileImports top is0 = do
3840
makeSingle (Just p) q = Map.singleton p $ Set.singleton q
3941

4042
groupModules :: [Import] -> ImportDeclMap
41-
groupModules = foldr
42-
(\(Import mod as p q ns) -> Map.insertWith mergeChildren (mod,as)
43-
(makeSingle (parentNN p) (NamespacedName ns q)))
44-
Map.empty
45-
where
46-
parentNN :: Maybe (Hs.Name ()) -> Maybe NamespacedName
47-
parentNN (Just name@(Hs.Symbol _ _)) = Just $ NamespacedName (Hs.TypeNamespace ()) name
48-
-- ^ for parents, if they are operators, we assume they are type operators
49-
-- but actually, this will get lost anyway because of the structure of ImportSpec
50-
-- the point is that there should not be two tuples with the same name and diffenrent namespaces
51-
parentNN (Just name) = Just $ NamespacedName (Hs.NoNamespace ()) name
52-
parentNN Nothing = Nothing
43+
groupModules = flip foldr Map.empty $ \case
44+
(Import mod as p q ns) ->
45+
Map.insertWith mergeChildren (mod,as)
46+
(makeSingle (parentNN p) (NamespacedName ns q))
47+
(ImportInstances mod) ->
48+
Map.insertWith mergeChildren (mod,Unqualified) Map.empty
49+
where
50+
parentNN :: Maybe (Hs.Name ()) -> Maybe NamespacedName
51+
parentNN (Just name@(Hs.Symbol _ _)) = Just $ NamespacedName (Hs.TypeNamespace ()) name
52+
-- ^ for parents, if they are operators, we assume they are type operators
53+
-- but actually, this will get lost anyway because of the structure of ImportSpec
54+
-- the point is that there should not be two tuples with the same name and diffenrent namespaces
55+
parentNN (Just name) = Just $ NamespacedName (Hs.NoNamespace ()) name
56+
parentNN Nothing = Nothing
5357

5458
-- TODO: avoid having to do this by having a CName instead of a
5559
-- Name in the Import datatype
@@ -81,11 +85,13 @@ compileImports top is0 = do
8185
[] -> checkClashingImports is
8286
where
8387
isClashing (Import _ as' p' q' _) = (as' == as) && (p' /= p) && (q' == q)
88+
isClashing ImportInstances{} = False
8489
mkErrorMsg (Import _ _ p' q' _) =
8590
"Clashing import: " ++ pp q ++ " (both from "
8691
++ prettyShow (pp <$> p) ++ " and "
8792
++ prettyShow (pp <$> p') ++ ")"
8893
-- TODO: no range information as we only have Haskell names at this point
94+
checkClashingImports (ImportInstances mod : is) = checkClashingImports is
8995

9096

9197
-- | Generate a prelude import considering prelude config options (hiding, implicit, etc).

‎src/Agda2Hs/Compile/Name.hs‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -230,3 +230,10 @@ compileModuleName m = do
230230
text "Top-level module name for" <+> prettyTCM m <+>
231231
text "is" <+> text (pp tlm)
232232
return tlm
233+
234+
importInstance :: QName -> C ()
235+
importInstance f = do
236+
mod <- compileModuleName $ qnameModule f
237+
unless (isPrimModule mod) $ do
238+
reportSLn "agda2hs.import" 20 $ "Importing instances from " ++ pp mod
239+
tellImport $ ImportInstances mod

‎src/Agda2Hs/Compile/Term.hs‎

Lines changed: 47 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ module Agda2Hs.Compile.Term where
22

33
import Control.Arrow ( (>>>), (&&&), second )
44
import Control.Monad ( unless, zipWithM )
5+
import Control.Monad.Except
56
import Control.Monad.Reader
67

78
import Data.Foldable ( toList )
@@ -19,11 +20,16 @@ import Agda.Syntax.Common
1920
import Agda.Syntax.Literal
2021
import Agda.Syntax.Internal
2122

23+
import Agda.TypeChecking.CheckInternal ( infer )
24+
import Agda.TypeChecking.Constraints ( noConstraints )
25+
import Agda.TypeChecking.Conversion ( equalTerm )
26+
import Agda.TypeChecking.InstanceArguments ( findInstance )
27+
import Agda.TypeChecking.MetaVars ( newInstanceMeta )
2228
import Agda.TypeChecking.Monad
2329
import Agda.TypeChecking.Pretty
2430
import Agda.TypeChecking.Records ( shouldBeProjectible, isRecordType, recordFieldNames )
2531
import Agda.TypeChecking.Datatypes ( getConType )
26-
import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, instantiate )
32+
import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, instantiate, reduce )
2733
import Agda.TypeChecking.Substitute
2834
import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM, flattenTel )
2935
import Agda.TypeChecking.ProjectionLike ( reduceProjectionLike )
@@ -35,7 +41,7 @@ import Agda.Utils.Monad
3541
import Agda.Utils.Size
3642

3743
import Agda2Hs.AgdaUtils
38-
import Agda2Hs.Compile.Name ( compileQName )
44+
import Agda2Hs.Compile.Name ( compileQName, importInstance )
3945

4046
import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTelSize )
4147
import Agda2Hs.Compile.Types
@@ -615,3 +621,42 @@ compileLiteral (LitChar c) = return $ Hs.charE c
615621
compileLiteral (LitString t) = return $ Hs.Lit () $ Hs.String () s s
616622
where s = Text.unpack t
617623
compileLiteral l = genericDocError =<< text "bad term:" <?> prettyTCM (Lit l)
624+
625+
626+
checkInstance :: Term -> C ()
627+
checkInstance u = do
628+
reportSDoc "agda2hs.checkInstance" 12 $ text "checkInstance" <+> prettyTCM u
629+
reduce u >>= \case
630+
Var x es -> do
631+
unlessM (isInstance <$> domOfBV x) illegalInstance
632+
checkInstanceElims es
633+
Def f es -> do
634+
unlessM (isJust . defInstance <$> getConstInfo f) illegalInstance
635+
importInstance f
636+
checkInstanceElims es
637+
-- We need to compile applications of `fromNat`, `fromNeg`, and
638+
-- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally
639+
-- this constraint would be marked as erased but this would involve
640+
-- changing Agda builtins.
641+
Con c _ _
642+
| prettyShow (conName c) == "Agda.Builtin.Unit.tt" ||
643+
prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" ||
644+
prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return ()
645+
_ -> illegalInstance
646+
647+
where
648+
illegalInstance :: C ()
649+
illegalInstance = do
650+
reportSDoc "agda2hs.checkInstance" 15 $ text "illegal instance: " <+> pretty u
651+
genericDocError =<< text "illegal instance: " <+> prettyTCM u
652+
653+
checkInstanceElims :: Elims -> C ()
654+
checkInstanceElims = mapM_ checkInstanceElim
655+
656+
checkInstanceElim :: Elim -> C ()
657+
checkInstanceElim (Apply v) =
658+
when (isInstance v && usableQuantity v) $
659+
checkInstance $ unArg v
660+
checkInstanceElim IApply{} = illegalInstance
661+
checkInstanceElim (Proj _ f) =
662+
unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance

‎src/Agda2Hs/Compile/Types.hs‎

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -108,15 +108,20 @@ qualifiedAs = join
108108

109109
-- | Encoding of a Haskell module import statement.
110110
data Import = Import
111-
{ importModule :: Hs.ModuleName ()
112-
, importQualified :: Qualifier
113-
, importParent :: Maybe (Hs.Name ())
114-
, importName :: Hs.Name ()
115-
, importNamespace :: Hs.Namespace ()
111+
{ _importModule :: Hs.ModuleName ()
112+
, _importQualified :: Qualifier
113+
, _importParent :: Maybe (Hs.Name ())
114+
, _importName :: Hs.Name ()
115+
, _importNamespace :: Hs.Namespace ()
116116
-- ^^ if this is a type or something like that, we can add a namespace qualifier to the import spec
117117
-- now it's only useful for differentiating type operators; so for others we always put Hs.NoNamespace () here
118118
-- (we don't calculate it if it's not necessary)
119119
}
120+
| ImportInstances (Hs.ModuleName ())
121+
122+
importModule :: Import -> Hs.ModuleName ()
123+
importModule (Import{ _importModule = mod }) = mod
124+
importModule (ImportInstances mod) = mod
120125

121126
type Imports = [Import]
122127

‎src/Agda2Hs/Compile/Utils.hs‎

Lines changed: 0 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -253,43 +253,6 @@ isInlinedFunction q = do
253253
(InlinePragma ==) <$> processPragma r
254254
_ -> return False
255255

256-
checkInstance :: Term -> C ()
257-
checkInstance u = do
258-
reportSDoc "agda2hs.checkInstance" 12 $ text "checkInstance" <+> prettyTCM u
259-
reduce u >>= \case
260-
Var x es -> do
261-
unlessM (isInstance <$> domOfBV x) illegalInstance
262-
checkInstanceElims es
263-
Def f es -> do
264-
unlessM (isJust . defInstance <$> getConstInfo f) illegalInstance
265-
checkInstanceElims es
266-
-- We need to compile applications of `fromNat`, `fromNeg`, and
267-
-- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally
268-
-- this constraint would be marked as erased but this would involve
269-
-- changing Agda builtins.
270-
Con c _ _
271-
| prettyShow (conName c) == "Agda.Builtin.Unit.tt" ||
272-
prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" ||
273-
prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return ()
274-
_ -> illegalInstance
275-
276-
where
277-
illegalInstance :: C ()
278-
illegalInstance = do
279-
reportSDoc "agda2hs.checkInstance" 15 $ text "illegal instance: " <+> pretty u
280-
genericDocError =<< text "illegal instance: " <+> prettyTCM u
281-
282-
checkInstanceElims :: Elims -> C ()
283-
checkInstanceElims = mapM_ checkInstanceElim
284-
285-
checkInstanceElim :: Elim -> C ()
286-
checkInstanceElim (Apply v) =
287-
when (isInstance v && usableQuantity v) $
288-
checkInstance $ unArg v
289-
checkInstanceElim IApply{} = illegalInstance
290-
checkInstanceElim (Proj _ f) =
291-
unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance
292-
293256
withNestedType :: C a -> C a
294257
withNestedType = local $ \e -> e { isNestedInType = True }
295258

‎src/Agda2Hs/Render.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ prettyShowImportDecl (Hs.ImportDecl _ m qual src safe mbPkg mbName mbSpecs) =
104104
++ parenList (map prettyShowSpec ispecs)
105105

106106
parenList :: [String] -> String
107-
parenList [] = ""
107+
parenList [] = "()"
108108
parenList (x:xs) = '(' : (x ++ go xs)
109109
where
110110
go :: [String] -> String

‎test/AllTests.agda‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,7 @@ import CustomTuples
9292
import ProjectionLike
9393
import FunCon
9494
import Issue308
95+
import Issue324
9596

9697
{-# FOREIGN AGDA2HS
9798
import Issue14
@@ -181,4 +182,5 @@ import CustomTuples
181182
import ProjectionLike
182183
import FunCon
183184
import Issue308
185+
import Issue324
184186
#-}

‎test/Issue324.agda‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
2+
open import Haskell.Prelude
3+
open import Issue324instance
4+
5+
test : Bool
6+
test = not == id
7+
8+
{-# COMPILE AGDA2HS test #-}

‎test/Issue324instance.agda‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
2+
open import Haskell.Prelude
3+
4+
instance
5+
eqBoolFun : Eq (Bool → Bool)
6+
eqBoolFun ._==_ x y = x True == y True && x False == y False
7+
8+
{-# COMPILE AGDA2HS eqBoolFun #-}
9+

0 commit comments

Comments
 (0)