diff --git a/agda2hs.agda-lib b/agda2hs.agda-lib index c07e0b90..b430f79d 100644 --- 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 index 7f6f06ff..0155e7ee 100644 --- 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 index 87be17b5..a2946e44 100644 --- 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 index ecb706b1..1c310675 100644 --- 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 currentMod <= 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,15 +360,8 @@ 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 @@ -373,8 +369,15 @@ 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__ diff --git a/test/AllTests.agda b/test/AllTests.agda index aa906bab..617adc5c 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -1,7 +1,7 @@ module AllTests where --- import Issue14 +import Issue14 import Issue65 import Issue69 import Issue73 @@ -9,11 +9,11 @@ import Fixities import LanguageConstructs import Numbers import Pragmas --- import Sections +import Sections -- import Test import Tree import Tuples --- import Where +import Where import TypeSynonyms -- import CanonicalInstance import Coinduction @@ -25,10 +25,10 @@ import Default import Vector import Issue90 import Issue93 --- import QualifiedModule +import QualifiedModule import Superclass import UnboxPragma --- import ScopedTypeVariables +import ScopedTypeVariables import LiteralPatterns import Issue92 import HeightMirror @@ -39,18 +39,18 @@ import Issue94 import Issue107 import DoNotation import NewTypePragma --- import Importer --- import QualifiedImports --- import CommonQualifiedImports +import Importer +import QualifiedImports +import CommonQualifiedImports import RequalifiedImports --- import QualifiedPrelude +import QualifiedPrelude import AutoLambdaCaseInCase import AutoLambdaCaseInBind import WitnessedFlows import Kinds import LawfulOrd import Deriving --- import ErasedLocalDefinitions +import ErasedLocalDefinitions import TypeOperators import ErasedTypeArguments import TypeOperatorExport @@ -61,17 +61,16 @@ import Issue200 import Issue169 -- import Issue210 import TypeSignature --- import ModuleParameters --- import ModuleParametersImports +import ModuleParameters +import ModuleParametersImports import Coerce -- import Inlining --- import EraseType +-- import EraseType -- requires inlining import Issue257 import Delay --- import Issue264 {-# FOREIGN AGDA2HS --- import Issue14 +import Issue14 import Issue65 import Issue69 import Issue73 @@ -79,11 +78,11 @@ import Fixities import LanguageConstructs import Numbers import Pragmas --- import Sections +import Sections -- import Test import Tree import Tuples --- import Where +import Where import TypeSynonyms -- import CanonicalInstance import Coinduction @@ -95,10 +94,10 @@ import Default import Vector import Issue90 import Issue93 --- import QualifiedModule +import QualifiedModule import Superclass import UnboxPragma --- import ScopedTypeVariables +import ScopedTypeVariables import LiteralPatterns import Issue92 import HeightMirror @@ -108,18 +107,18 @@ import BangPatterns import Issue94 import DoNotation import NewTypePragma --- import Importer --- import QualifiedImports --- import CommonQualifiedImports +import Importer +import QualifiedImports +import CommonQualifiedImports import RequalifiedImports --- import QualifiedPrelude +import QualifiedPrelude import AutoLambdaCaseInCase import AutoLambdaCaseInBind import WitnessedFlows import Kinds import LawfulOrd import Deriving --- import ErasedLocalDefinitions +import ErasedLocalDefinitions import TypeOperators import ErasedTypeArguments import TypeOperatorExport @@ -130,11 +129,10 @@ import Issue200 import Issue169 -- import Issue210 import TypeSignature --- import ModuleParameters --- import ModuleParametersImports +import ModuleParameters +import ModuleParametersImports import Coerce -- import Inlining -- import EraseType import Delay --- import Issue264 #-} diff --git a/test/Issue264.agda b/test/Issue264.agda deleted file mode 100644 index c2eb496d..00000000 --- a/test/Issue264.agda +++ /dev/null @@ -1,11 +0,0 @@ -module Issue264 {@0 name : Set} where - -postulate - Term : Set → Set - -reduce : Term name → Term name -reduce = go - where postulate - go : Term name → Term name - -{-# COMPILE AGDA2HS reduce #-} diff --git a/test/Makefile b/test/Makefile index 175aaf9b..e4255677 100644 --- a/test/Makefile +++ b/test/Makefile @@ -10,13 +10,13 @@ clean : alltests : @echo == Compiling tests == - ./agda2hs AllTests.agda -o build + ./agda2hs --no-projection-like AllTests.agda -o build @echo == Running ghc == @(cd build; ghc -fno-code AllTests.hs) cubicaltests : @echo == Compiling tests using cubical == - ./agda2hs CubicalTests.agda -o build + ./agda2hs --no-projection-like CubicalTests.agda -o build @echo == Running ghc == @(cd build; ghc -fno-code CubicalTests.hs) @@ -31,7 +31,7 @@ print-fail : build/%.err : Fail/%.agda force-recompile alltests @echo Compiling $< - @(./agda2hs $< -o build -v0 && echo "UNEXPECTED SUCCESS" || true) | sed -e 's:'$(ROOT)'::g' > $@ + @(./agda2hs --no-projection-like $< -o build -v0 && echo "UNEXPECTED SUCCESS" || true) | sed -e 's:'$(ROOT)'::g' > $@ force-recompile : diff --git a/test/ModuleParameters.agda b/test/ModuleParameters.agda index a1a4812b..2869be17 100644 --- a/test/ModuleParameters.agda +++ b/test/ModuleParameters.agda @@ -2,9 +2,7 @@ open import Haskell.Prelude hiding (a) module ModuleParameters (@0 name : Set) - (p : @0 name → Set) - (x : Integer) - where + (p : @0 name → Set) where data Scope : Set where Empty : Scope @@ -18,9 +16,9 @@ unbind (Bind _ _ s) = s module _ {a : Set} where thing : a → a - thing z = y + thing x = y where y : a - y = z + y = x {-# COMPILE AGDA2HS thing #-} stuff : a → Scope → a diff --git a/test/ModuleParametersImports.agda b/test/ModuleParametersImports.agda index 00d4a8e8..14b4a319 100644 --- a/test/ModuleParametersImports.agda +++ b/test/ModuleParametersImports.agda @@ -1,7 +1,7 @@ module ModuleParametersImports where open import Haskell.Prelude -open import ModuleParameters Bool (λ _ → Nat) 3 +open import ModuleParameters Bool (λ _ → Nat) scope : Scope scope = unbind (Bind True 3 (Bind False 2 Empty)) diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index ca6dc4f9..d745612b 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -1,6 +1,6 @@ module AllTests where --- import Issue14 +import Issue14 import Issue65 import Issue69 import Issue73 @@ -8,11 +8,11 @@ import Fixities import LanguageConstructs import Numbers import Pragmas --- import Sections +import Sections -- import Test import Tree import Tuples --- import Where +import Where import TypeSynonyms -- import CanonicalInstance import Coinduction @@ -24,7 +24,7 @@ import Default import Vector import Issue90 import Issue93 --- import QualifiedModule +import QualifiedModule import Superclass import UnboxPragma -- import ScopedTypeVariables @@ -37,11 +37,11 @@ import BangPatterns import Issue94 import DoNotation import NewTypePragma --- import Importer --- import QualifiedImports --- import CommonQualifiedImports +import Importer +import QualifiedImports +import CommonQualifiedImports import RequalifiedImports --- import QualifiedPrelude +import QualifiedPrelude import AutoLambdaCaseInCase import AutoLambdaCaseInBind import WitnessedFlows @@ -59,7 +59,7 @@ import Issue200 import Issue169 -- import Issue210 import TypeSignature --- import ModuleParameters +import ModuleParameters -- import ModuleParametersImports import Coerce -- import Inlining diff --git a/test/golden/ModuleParameters.hs b/test/golden/ModuleParameters.hs new file mode 100644 index 00000000..bb75c348 --- /dev/null +++ b/test/golden/ModuleParameters.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module ModuleParameters where + +data Scope p = Empty + | Bind p (Scope p) + +unbind :: Scope p -> Scope p +unbind Empty = Empty +unbind (Bind _ s) = s + +thing :: forall p a . a -> a +thing x = y + where + y :: a + y = x + +stuff :: forall p a . a -> Scope p -> a +stuff x Empty = x +stuff x (Bind _ _) = x + +more :: forall p a b . b -> a -> Scope p -> Scope p +more _ _ Empty = Empty +more _ _ (Bind _ s) = s + diff --git a/test/golden/ModuleParametersImports.hs b/test/golden/ModuleParametersImports.hs new file mode 100644 index 00000000..83c2c5be --- /dev/null +++ b/test/golden/ModuleParametersImports.hs @@ -0,0 +1,11 @@ +module ModuleParametersImports where + +import qualified ModuleParameters (Scope(Bind, Empty), unbind) +import Numeric.Natural (Natural) + +scope :: ModuleParameters.Scope Natural +scope + = ModuleParameters.unbind + (ModuleParameters.Bind 3 + (ModuleParameters.Bind 2 ModuleParameters.Empty)) +