fix module imports

agda · Feb 2, 2024 · bc2d9ab · bc2d9ab
1 parent 73eea7d
commit bc2d9ab
Show file tree

Hide file tree

Showing 12 changed files with 153 additions and 127 deletions.
diff --git a/agda2hs.agda-lib b/agda2hs.agda-lib
@@ -1,4 +1,4 @@
 name: agda2hs
 depend:
 include: lib
-flags: -W noUnsupportedIndexedMatch --erasure
+flags: -W noUnsupportedIndexedMatch --erasure --no-projection-like
diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs
@@ -68,7 +68,7 @@ compileInstance ToDefinition def@Defn{..} =
     ir <- compileInstRule [] (unEl defType)
     withFunctionLocals defName $ do
       (ds, rs) <- concatUnzip
-              <$> mapM (compileInstanceClause (qnameModule defName)) funClauses
+              <$> mapM (compileInstanceClause (qnameModule defName) defType) funClauses
       when (length (nub rs) > 1) $
         genericDocError =<< fsep (pwords "More than one minimal record used.")
       return $ Hs.InstDecl () Nothing ir (Just ds)
@@ -120,8 +120,8 @@ etaExpandClause cl@Clause{namedClausePats = ps, clauseBody = Just t} = do
       "Type class instances must be defined using copatterns (or top-level" ++
       " records) and cannot be defined using helper functions.")
 
-compileInstanceClause :: ModuleName -> Clause -> C ([Hs.InstDecl ()], [QName])
-compileInstanceClause curModule c = withClauseLocals curModule c $ do
+compileInstanceClause :: ModuleName -> Type -> Clause -> C ([Hs.InstDecl ()], [QName])
+compileInstanceClause curModule ty c = withClauseLocals curModule c $ do
   -- abuse compileClause:
   -- 1. drop any patterns before record projection to suppress the instance arg
   -- 2. use record proj. as function name
@@ -130,7 +130,7 @@ compileInstanceClause curModule c = withClauseLocals curModule c $ do
   -- TODO: check that the things we drop here are not doing any matching
   case dropWhile (isNothing . isProjP) (namedClausePats c) of
     [] ->
-      concatUnzip <$> (mapM (compileInstanceClause curModule) =<< etaExpandClause c)
+      concatUnzip <$> (mapM (compileInstanceClause curModule ty) =<< etaExpandClause c)
     p : ps -> do
       let c' = c {namedClausePats = ps}
           ProjP _ q = namedArg p
@@ -203,7 +203,7 @@ compileInstanceClause curModule c = withClauseLocals curModule c $ do
         | otherwise -> do
           reportSDoc "agda2hs.compile.instance" 20 $ text "Compiling instance clause" <+> prettyTCM c'
           --TODO(flupe)
-          ms <- disableCopatterns $ compileClause curModule uf undefined c'
+          ms <- disableCopatterns $ compileClause curModule uf ty c'
           return ([Hs.InsDecl () (Hs.FunBind () (toList ms))], [])
 
 fieldArgInfo :: QName -> C ArgInfo

diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
@@ -141,8 +141,13 @@ compileFun' withSig def@Defn{..} = do
           reportSDoc "agda2hs.compile.type" 6 $ "Applying module parameters to clauses: " <+> prettyTCM pars
         let clauses = if weAreOnTop then filtered else filtered `apply` pars
 
-        -- TODO(flupe): check whether we need to "apply" module parameters to deftype
         typ <- if weAreOnTop then pure defType else piApplyM defType pars
+
+
+        -- TODO(flupe):
+        -- for projection-like functions, patterns only start at the record argument
+        -- so it is incorrect to use defType as a way to discard patterns, as they are not aligned
+
         cs  <- mapMaybeM (compileClause (qnameModule defName) x typ) clauses
 
         when (null cs) $ genericDocError
@@ -171,6 +176,7 @@ compileClause' curModule x ty c@Clause{..} = do
   reportSDoc "agda2hs.compile" 17 $ "Old context: "      <+> (prettyTCM =<< getContext)
   reportSDoc "agda2hs.compile" 17 $ "Clause telescope: " <+> prettyTCM clauseTel
   reportSDoc "agda2hs.compile" 17 $ "Clause type:      " <+> prettyTCM clauseType
+  reportSDoc "agda2hs.compile" 17 $ "Function type:    " <+> prettyTCM ty
   reportSDoc "agda2hs.compile" 17 $ "Clause patterns:  " <+> text (prettyShow namedClausePats)
 
   addContext (KeepNames clauseTel) $ do

diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
@@ -48,23 +48,17 @@ import {-# SOURCE #-} Agda2Hs.Compile.Function ( compileClause' )
 
 type DefCompileRule = Type -> [Term] -> C (Hs.Exp ())
 
-
-  {-
-isSpecialDef q = case prettyShow q of
-  -- _ | isExtendedLambdaName q                 -> Just $ lambdaCase q
-  "Haskell.Extra.Delay.runDelay"                -> Just compileErasedApp
-  _                                             -> Nothing
-  -}
-
 isSpecialDef :: QName -> Maybe DefCompileRule
 isSpecialDef q = case prettyShow q of
-  _ | isExtendedLambdaName q   -> Just (lambdaCase q)
-  "Haskell.Prim.if_then_else_" -> Just ifThenElse
-  "Haskell.Prim.case_of_"      -> Just caseOf
-  "Haskell.Prim.the"           -> Just expTypeSig
-  _                            -> Nothing
+  _ | isExtendedLambdaName q     -> Just (lambdaCase q)
+  "Haskell.Prim.if_then_else_"   -> Just ifThenElse
+  "Haskell.Prim.case_of_"        -> Just caseOf
+  "Haskell.Prim.the"             -> Just expTypeSig
+  "Haskell.Extra.Delay.runDelay" -> Just compileErasedApp
+  _                              -> Nothing
+
 
--- | Compile a lambda-case to the equivalent @\case@ expression.
+-- | Compile a @\where@ to the equivalent @\case@ expression.
 lambdaCase :: QName -> DefCompileRule
 lambdaCase q ty args = setCurrentRangeQ q $ do
   Function
@@ -90,6 +84,7 @@ lambdaCase q ty args = setCurrentRangeQ q $ do
       eApp lcase <$> compileArgs ty' rest
       -- undefined -- compileApp lcase (undefined, undefined, rest)
 
+
 -- | Compile @if_then_else_@ to a Haskell @if ... then ... else ... @ expression.
 ifThenElse :: DefCompileRule
 ifThenElse ty args = compileArgs ty args >>= \case
@@ -98,6 +93,7 @@ ifThenElse ty args = compileArgs ty args >>= \case
   -- partially applied
   _               -> genericError "if_then_else_ must be fully applied"
 
+
 -- | Compile @case_of_@ to Haskell @\case@ expression.
 caseOf :: DefCompileRule
 caseOf ty args = compileArgs ty args >>= \case
@@ -110,6 +106,7 @@ caseOf ty args = compileArgs ty args >>= \case
     in return $ eApp (Hs.Case () e [Hs.Alt () p (Hs.UnGuardedRhs () $ lam ps b) Nothing]) es'
   _ -> genericError "case_of_ must be fully applied to a lambda term."
 
+
 -- | Compile @the@ to an explicitly-annotated Haskell expression.
 expTypeSig :: DefCompileRule
 expTypeSig ty args@(_:typ:_:_) = do
@@ -119,7 +116,6 @@ expTypeSig ty args@(_:typ:_:_) = do
 expTypeSig _ _ = genericError "`the` must be fully applied"
 
 
-
 -- should really be named compileVar, TODO: rename compileVar
 compileV :: Int -> Type -> [Term] -> C (Hs.Exp ())
 compileV i ty es = do
@@ -167,12 +163,6 @@ compileSpined ty tm =
     aux _ _ _ _ = __IMPOSSIBLE__
 
 
-  {-
-
--- TODO(flupe)
-
--}
-
 -- TODO(flupe):
 -- maybeUnfoldCopy f es compileTerm $ \f es ->
 
@@ -187,14 +177,27 @@ compileDef f ty args = do
   -- ifM (isInlinedFunction f) (compileInlineFunctionApp f es) $ do
     reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function:" <+> prettyTCM f
 
-    -- TODO(flupe): drop parameters again
-    -- Drop module parameters of local `where` functions
-    moduleArgs <- getDefFreeVars f
-    -- reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs
+    currentMod <- currentModule
+    let defMod = qnameModule f
+
+    (ty', args') <-
+
+      -- if the function is called from the same module it's defined in,
+      -- we drop the module parameters
+      -- TODO: in the future we're not always gonna be erasing module parameters
+      if prettyShow currentMod `isPrefixOf` prettyShow defMod then do
+        npars <- size <$> (lookupSection =<< currentModule)
+        let (pars, rest) = splitAt npars args
+        ty' <- piApplyM ty pars
+        pure (ty', rest)
+      else pure (ty, args)
+
+    reportSDoc "agda2hs.compile.term" 15 $ text " module args" <+> prettyTCM ty'
+    reportSDoc "agda2hs.compile.term" 15 $ text "args to def: " <+> prettyTCM args'
 
     hsName <- compileQName f
 
-    compileApp (Hs.Var () hsName) ty (drop moduleArgs args)
+    compileApp (Hs.Var () hsName) ty' args'
 
 
 -- * Compilation of projection(-like) definitions
@@ -357,24 +360,24 @@ compileErasedApp ty args = do
     [v] -> return v
     _   -> __IMPOSSIBLE__
 
+
 compileCon :: ConHead -> ConInfo -> Type -> [Term] -> C (Hs.Exp ())
--- TODO(flupe:)
--- -- the constructor may be a copy introduced by module application,
--- -- therefore we need to find the original constructor
--- info <- getConstInfo (conName h)
--- if not (defCopy info)
---   then compileCon h i es
---   else let Constructor{conSrcCon = c} = theDef info in
---        compileCon c ConOSystem es
 compileCon h i ty args
   | Just semantics <- isSpecialCon (conName h)
   = semantics ty args
 compileCon h i ty args = do
   isUnboxConstructor (conName h) >>= \case
     Just _  -> compileErasedApp ty args
     Nothing -> do
-      con <- Hs.Con () <$> compileQName (conName h)
-      compileApp con ty args
+      info <- getConstInfo (conName h)
+      -- the constructor may be a copy introduced by module application,
+      -- therefore we need to find the original constructor
+      if defCopy info then
+        let Constructor{conSrcCon = ch'} = theDef info in
+        compileCon ch' i ty args
+      else do
+        con <- Hs.Con () <$> compileQName (conName h)
+        compileApp con ty args
 
 
 -- * Term compilation
@@ -406,40 +409,38 @@ usableDom dom = usableModality dom
 compileLam :: Type -> ArgInfo -> Abs Term -> C (Hs.Exp ())
 compileLam ty argi abs = do
   reportSDoc "agda2hs.compile.term" 50 $ text "Reached lambda"
-  reduce (unEl ty) >>= \case
-    Pi dom cod -> do
-      -- unusable domain, we remove the lambda and compile the body only
-      if not (usableDom dom) then
-        addContext dom $ compileTerm (absBody cod) (absBody abs)
+  (dom, cod) <- mustBePi ty
 
-      -- usable domain, user-written lambda is preserved
-      else if getOrigin argi == UserWritten then do
+  -- unusable domain, we remove the lambda and compile the body only
+  if not (usableDom dom) then
+    addContext dom $ compileTerm (absBody cod) (absBody abs)
 
-        when (patternInTeleName `isPrefixOf` absName abs) $ genericDocError =<<
-          text "Record pattern translation not supported. Use a pattern matching lambda instead."
+  -- usable domain, user-written lambda is preserved
+  else if getOrigin argi == UserWritten then do
 
-        reportSDoc "agda2hs.compile" 17 $ text "compiling regular lambda"
+    when (patternInTeleName `isPrefixOf` absName abs) $ genericDocError =<<
+      text "Record pattern translation not supported. Use a pattern matching lambda instead."
 
-        let varName = absName abs
-            ctxElt  = (varName,) <$> dom
+    reportSDoc "agda2hs.compile" 17 $ text "compiling regular lambda"
 
-        hsLambda varName <$> addContext ctxElt (compileTerm (absBody cod) (absBody abs))
+    let varName = absName abs
+        ctxElt  = (varName,) <$> dom
 
-      -- usable domain, generated lambda means we introduce a section
-      else do
+    hsLambda varName <$> addContext ctxElt (compileTerm (absBody cod) (absBody abs))
 
-        let varName = absName abs
-            ctxElt  = (varName,) <$> dom
+  -- usable domain, generated lambda means we introduce a section
+  else do
 
-        x <- compileVar 0
+    let varName = absName abs
+        ctxElt  = (varName,) <$> dom
 
-        addContext ctxElt $ do
-          compileTerm (absBody cod) (absBody abs) <&> \case
-            Hs.InfixApp () a op b
-              | a == hsVar x -> Hs.RightSection () op b
-            body             -> hsLambda x body
+    addContext ctxElt $ do
+      x <- compileVar 0
+      compileTerm (absBody cod) (absBody abs) <&> \case
+        Hs.InfixApp () a op b
+          | a == hsVar x -> Hs.RightSection () op b
+        body             -> hsLambda x body
 
-    _ -> __IMPOSSIBLE__