agda2hs (empty) → 1.0
raw patch · 22 files changed
+2759/−0 lines, 22 filesdep +Agdadep +basedep +containers
Dependencies added: Agda, base, containers, deepseq, directory, filepath, haskell-src-exts, mtl, syb, text, unordered-containers
Files
- LICENSE +7/−0
- agda2hs.cabal +60/−0
- src/Agda2Hs/AgdaUtils.hs +94/−0
- src/Agda2Hs/Compile.hs +98/−0
- src/Agda2Hs/Compile/ClassInstance.hs +227/−0
- src/Agda2Hs/Compile/Data.hs +78/−0
- src/Agda2Hs/Compile/Function.hs +271/−0
- src/Agda2Hs/Compile/Function.hs-boot +7/−0
- src/Agda2Hs/Compile/Imports.hs +78/−0
- src/Agda2Hs/Compile/Name.hs +158/−0
- src/Agda2Hs/Compile/Postulate.hs +25/−0
- src/Agda2Hs/Compile/Record.hs +174/−0
- src/Agda2Hs/Compile/Term.hs +291/−0
- src/Agda2Hs/Compile/Type.hs +197/−0
- src/Agda2Hs/Compile/TypeDefinition.hs +46/−0
- src/Agda2Hs/Compile/Types.hs +107/−0
- src/Agda2Hs/Compile/Utils.hs +271/−0
- src/Agda2Hs/HsUtils.hs +266/−0
- src/Agda2Hs/Pragma.hs +97/−0
- src/Agda2Hs/Render.hs +107/−0
- src/AgdaInternals.hs +53/−0
- src/Main.hs +47/−0
+ LICENSE view
@@ -0,0 +1,7 @@+Copyright 2023 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, and Henry Blanchette.++Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ agda2hs.cabal view
@@ -0,0 +1,60 @@+cabal-version: 2.2+name: agda2hs+version: 1.0+license: BSD-3-Clause+license-file: LICENSE+author: Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette+maintainer: jesper@sikanda.be+copyright: 2023 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette+category: Language, Compiler+build-type: Simple+synopsis: Compiling Agda code to readable Haskell.+description:+ Produces verified and readable Haskell code by extracting it from a+ (lightly annotated) Agda program.+ The tool is implemented as an Agda backend, which means that `agda2hs` is a+ fully functional Agda compiler.++source-repository head+ type: git+ location: https://github.com/agda/agda2hs.git++executable agda2hs+ hs-source-dirs: src+ main-is: Main.hs+ other-modules: Agda2Hs.AgdaUtils,+ Agda2Hs.Compile,+ Agda2Hs.Compile.ClassInstance,+ Agda2Hs.Compile.Data,+ Agda2Hs.Compile.Function,+ Agda2Hs.Compile.Imports,+ Agda2Hs.Compile.Name,+ Agda2Hs.Compile.Postulate,+ Agda2Hs.Compile.Record,+ Agda2Hs.Compile.Term,+ Agda2Hs.Compile.Type,+ Agda2Hs.Compile.TypeDefinition,+ Agda2Hs.Compile.Types,+ Agda2Hs.Compile.Utils,+ Agda2Hs.HsUtils,+ Agda2Hs.Pragma+ Agda2Hs.Render+ AgdaInternals+ build-depends: base >= 4.10 && < 4.18,+ Agda >= 2.6.3 && < 2.6.4,+ containers >= 0.6 && < 0.7,+ unordered-containers >= 0.2,+ mtl >= 2.2,+ directory >= 1.2.6.2 && < 1.4,+ filepath >= 1.4.1.0 && < 1.5,+ haskell-src-exts >= 1.23 && < 1.25,+ syb >= 0.7,+ text >= 1.2.3.0,+ deepseq >= 1.4.1.1+ default-language: Haskell2010+ default-extensions: LambdaCase,+ RecordWildCards,+ FlexibleContexts,+ MultiWayIf,+ TupleSections,+ ScopedTypeVariables
+ src/Agda2Hs/AgdaUtils.hs view
@@ -0,0 +1,94 @@+module Agda2Hs.AgdaUtils where++import Data.Data+import Data.Monoid ( Any(..) )+import Data.Maybe ( fromMaybe )++import Agda.Compiler.Backend hiding ( Args )++import Agda.Interaction.FindFile ( findFile' )++import Agda.Syntax.Common ( Arg, defaultArg )+import Agda.Syntax.Internal+import Agda.Syntax.Internal.Names+import Agda.Syntax.TopLevelModuleName++import Agda.TypeChecking.Monad ( topLevelModuleName )+import Agda.TypeChecking.Pretty +import Agda.TypeChecking.Substitute++import Agda.Utils.Either ( isRight )+import Agda.Utils.List ( initMaybe )+import Agda.Utils.Monad ( ifM )+import Agda.Utils.Pretty ( prettyShow )+import Agda.Utils.Impossible ( __IMPOSSIBLE__ )++import AgdaInternals++multilineText :: Monad m => String -> m Doc+multilineText s = vcat $ map text $ lines s++(~~) :: QName -> String -> Bool+q ~~ s = prettyShow q == s++-- | Check whether a module is an *immediate* parent of another.+isFatherModuleOf :: ModuleName -> ModuleName -> Bool+isFatherModuleOf m = maybe False (mnameToList m ==) . initMaybe . mnameToList++-- | Apply a clause's telescope arguments to a local where definition.+-- i.e. reverse Agda's λ-lifting+applyUnderTele :: Definition -> Args -> Definition+applyUnderTele d as = raise (length as) d `apply` as++-- | Check whether the given name (1) is the name of an extended+-- lambda and (2) is used anywhere inside the second argument.+extLamUsedIn :: NamesIn a => QName -> a -> Bool+extLamUsedIn n x = isExtendedLambdaName n && getAny (namesIn' (Any . (n ==)) x)++-- | All mentions of local definitions that occur anywhere inside the argument.+getLocalUses :: NamesIn a => [QName] -> a -> [QName]+getLocalUses ls = namesIn' $ \q -> [ q | q `elem` ls ]++-- | Convert the final 'Proj' projection elimination into a+-- 'Def' projection application.+unSpine1 :: Term -> Term+unSpine1 v =+ case hasElims v of+ Just (h, es) -> fromMaybe v $ loop h [] es+ Nothing -> v+ where+ loop :: (Elims -> Term) -> Elims -> Elims -> Maybe Term+ loop h res es =+ case es of+ [] -> Nothing+ Proj o f : es' -> Just $ fromMaybe (Def f (Apply (defaultArg v) : es')) $ loop h (Proj o f : res) es'+ e : es' -> loop h (e : res) es'+ where v = h $ reverse res++mapDef :: (Term -> Term) -> Definition -> Definition+mapDef f d = d{ theDef = mapDefn (theDef d) }+ where+ mapDefn def@Function{} = def{ funClauses = map mapClause (funClauses def) }+ mapDefn defn = defn -- We only need this for Functions++ mapClause c = c{ clauseBody = f <$> clauseBody c }++topLevelModuleNameForModuleName :: ModuleName -> TCM TopLevelModuleName+topLevelModuleNameForModuleName = topLevelModuleName . rawTopLevelModuleNameForModuleName++isTopLevelModule :: ModuleName -> TCM (Maybe TopLevelModuleName)+isTopLevelModule m = do+ tlm <- topLevelModuleNameForModuleName m+ ifM (isRight <$> findFile' tlm) (return $ Just tlm) (return Nothing)++getTopLevelModuleForModuleName :: ModuleName -> TCM (Maybe TopLevelModuleName)+getTopLevelModuleForModuleName = loop . mnameToList+ where+ loop ns+ | null ns = return Nothing+ | otherwise = isTopLevelModule (MName ns) >>= \case+ Nothing -> loop (init ns)+ tlm@(Just _) -> return tlm++getTopLevelModuleForQName :: QName -> TCM (Maybe TopLevelModuleName)+getTopLevelModuleForQName = getTopLevelModuleForModuleName . qnameModule
+ src/Agda2Hs/Compile.hs view
@@ -0,0 +1,98 @@+module Agda2Hs.Compile where++import Control.Monad.Reader ( ReaderT(runReaderT) )+import Control.Monad.Writer ( WriterT(runWriterT) )+import Control.Monad.State ( StateT, evalStateT, get )++import qualified Data.Map as M++import Agda.Compiler.Backend+import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName )+import Agda.TypeChecking.Pretty+import Agda.Utils.Null+import Agda.Utils.Monad ( whenM )++import qualified Language.Haskell.Exts.Extension as Hs++import Agda2Hs.Compile.ClassInstance ( compileInstance )+import Agda2Hs.Compile.Data ( compileData )+import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma )+import Agda2Hs.Compile.Postulate ( compilePostulate )+import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma )+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils ( tellExtension )+import Agda2Hs.Pragma++initCompileEnv :: TopLevelModuleName -> CompileEnv+initCompileEnv tlm = CompileEnv+ { currModule = tlm+ , minRecordName = Nothing+ , locals = []+ , copatternsEnabled = False+ , checkVar = False+ }++initCompileState :: CompileState+initCompileState = CompileState { lcaseUsed = 0 }++runC :: TopLevelModuleName -> C a -> TCM (a, CompileOutput)+runC tlm = runWriterT+ . flip runReaderT (initCompileEnv tlm)+ . flip evalStateT initCompileState++-- Main compile function+------------------------++compile :: Options -> ModuleEnv -> IsMain -> Definition ->+ TCM (CompiledDef, CompileOutput)+compile _ tlm _ def = withCurrentModule (qnameModule $ defName def) $ runC tlm $+ compileAndTag <* postCompile+ where+ tag code = [(nameBindingSite $ qnameName $ defName def, code)]+ single x = [x]++ compileAndTag :: C CompiledDef+ compileAndTag = processPragma (defName def) >>= \ p -> do+ reportSDoc "agda2hs.compile" 5 $+ text "Compiling definition: " <+> prettyTCM (defName def)+ reportSDoc "agda2hs.compile" 45 $+ text "Pragma: " <+> text (show p)+ reportSDoc "agda2hs.compile" 45 $+ text "Compiling definition: " <+> pretty (theDef def)+ case (p , defInstance def , theDef def) of+ (NoPragma, _, _) ->+ return []+ (ExistingClassPragma, _, _) ->+ return [] -- No code generation, but affects how projections are compiled+ (UnboxPragma s, _, defn) ->+ checkUnboxPragma defn >> return [] -- also no code generation+ (TransparentPragma , _, Function{}) ->+ checkTransparentPragma def >> return [] -- also no code generation+ (ClassPragma ms, _, Record{}) ->+ tag . single <$> compileRecord (ToClass ms) def+ (NewTypePragma ds, _, Record{}) ->+ tag . single <$> compileRecord (ToRecordNewType ds) def+ (NewTypePragma ds, _, Datatype{}) ->+ tag <$> compileData ToDataNewType ds def+ (DefaultPragma ds, _, Datatype{}) ->+ tag <$> compileData ToData ds def+ (DerivePragma s, Just _, _) ->+ tag . single <$> compileInstance (ToDerivation s) def+ (DefaultPragma _, Just _, Axiom{}) ->+ tag . single <$> compileInstance (ToDerivation Nothing) def+ (DefaultPragma _, Just _, _) ->+ tag . single <$> compileInstance ToDefinition def+ (DefaultPragma _, _, Axiom{}) ->+ tag <$> compilePostulate def+ (DefaultPragma _, _, Function{}) ->+ tag <$> compileFun True def+ (DefaultPragma ds, _, Record{}) ->+ tag . single <$> compileRecord (ToRecord ds) def+ _ ->+ genericDocError =<< do+ text "Don't know how to compile" <+> prettyTCM (defName def)++ postCompile :: C ()+ postCompile =+ whenM ((> 0) . lcaseUsed <$> get) $+ tellExtension Hs.LambdaCase
+ src/Agda2Hs/Compile/ClassInstance.hs view
@@ -0,0 +1,227 @@+module Agda2Hs.Compile.ClassInstance where++import Control.Monad ( when, filterM, unless )+import Control.Monad.Reader ( local )++import Data.List ( nub )+import Data.Maybe ( isNothing, mapMaybe )+import qualified Data.HashMap.Strict as HMap++import qualified Language.Haskell.Exts.Syntax as Hs+import Language.Haskell.Exts.Extension as Hs++import Agda.Compiler.Backend+import Agda.Compiler.Common ( curDefs, sortDefs )++import Agda.Interaction.BasicOps ( parseName )++import Agda.Syntax.Common hiding ( Ranged )+import Agda.Syntax.Internal+import Agda.Syntax.Position ( noRange )+import Agda.Syntax.Scope.Base+import Agda.Syntax.Scope.Monad ( resolveName )++import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Substitute ( Apply(applyE) )+import Agda.TypeChecking.Records++import Agda.Utils.Lens+import Agda.Utils.Pretty ( prettyShow )+import Agda.Utils.Impossible ( __IMPOSSIBLE__ )++import Agda2Hs.AgdaUtils+import Agda2Hs.Compile.Function+import Agda2Hs.Compile.Name+import Agda2Hs.Compile.Type+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.HsUtils++enableCopatterns :: C a -> C a+enableCopatterns = local $ \e -> e { copatternsEnabled = True }++disableCopatterns :: C a -> C a+disableCopatterns = local $ \e -> e { copatternsEnabled = False }++enableStrategies :: Maybe (Hs.DerivStrategy ()) -> C ()+enableStrategies Nothing = return ()+enableStrategies (Just s) = do+ tellExtension Hs.DerivingStrategies+ enableStrategy s++enableStrategy :: Hs.DerivStrategy () -> C ()+enableStrategy (Hs.DerivStock ()) = return () -- is included in GHC+enableStrategy (Hs.DerivAnyclass ()) = tellExtension Hs.DeriveAnyClass -- since 7.10.1+enableStrategy (Hs.DerivNewtype ()) = tellExtension Hs.GeneralizedNewtypeDeriving -- since 6.8.1.+enableStrategy (Hs.DerivVia () t) = tellExtension Hs.DerivingVia -- since 8.6.1++compileInstance :: InstanceTarget -> Definition -> C (Hs.Decl ())+compileInstance (ToDerivation strategy) def@Defn{..} =+ setCurrentRangeQ defName $ do+ tellExtension Hs.StandaloneDeriving+ enableStrategies strategy+ ir <- compileInstRule [] (unEl defType)+ return $ Hs.DerivDecl () strategy Nothing ir+compileInstance ToDefinition def@Defn{..} =+ enableCopatterns $ setCurrentRangeQ defName $ do+ ir <- compileInstRule [] (unEl defType)+ withFunctionLocals defName $ do+ (ds, rs) <- concatUnzip+ <$> mapM (compileInstanceClause (qnameModule defName)) funClauses+ when (length (nub rs) > 1) $+ genericDocError =<< fsep (pwords "More than one minimal record used.")+ return $ Hs.InstDecl () Nothing ir (Just ds)+ where Function{..} = theDef++compileInstRule :: [Hs.Asst ()] -> Term -> C (Hs.InstRule ())+compileInstRule cs ty = case unSpine1 ty of+ Def f es | Just args <- allApplyElims es -> do+ vs <- mapM (compileType . unArg) $ filter keepArg args+ f <- compileQName f+ return $+ Hs.IRule () Nothing (ctx cs) $ foldl (Hs.IHApp ()) (Hs.IHCon () f) (map pars vs)+ where ctx [] = Nothing+ ctx cs = Just (Hs.CxTuple () cs)+ -- put parens around anything except a var or a constant+ pars :: Hs.Type () -> Hs.Type ()+ pars t@(Hs.TyVar () _) = t+ pars t@(Hs.TyCon () _) = t+ pars t = Hs.TyParen () t+ Pi a b -> compileDom (absName b) a >>= \case+ DomDropped -> underAbstr a b (compileInstRule cs . unEl)+ DomConstraint hsA ->+ underAbstraction a b (compileInstRule (cs ++ [hsA]) . unEl)+ DomType _ t -> __IMPOSSIBLE__+ _ -> __IMPOSSIBLE__++-- Plan:+-- - ✓ Eta-expand if no copatterns (top-level)+-- - ✓ drop default implementations and chase definitions of primitive methods in minimal records + *checks*+-- - ✓ compileInstanceClause on resulting clauses+--+-- *checks*+-- - ✓ Only one minimal record+-- - ✓ all primitives of the minimal are projected from the same dictionary+-- - ✓ default implementation that get dropped are also projected from that same dictionary++etaExpandClause :: Clause -> C [Clause]+etaExpandClause cl@Clause{clauseBody = Nothing} =+ genericError "Instance definition with absurd pattern!"+etaExpandClause cl@Clause{namedClausePats = ps, clauseBody = Just t} = do+ case t of+ Con c _ _ -> do+ let fields = conFields c+ let cls = [ cl{ namedClausePats = ps ++ [unnamed . ProjP ProjSystem <$> f],+ clauseBody = Just $ t `applyE` [Proj ProjSystem $ unArg f] }+ | f <- fields ]+ return cls+ _ -> genericDocError =<< fsep (pwords $+ "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+ -- abuse compileClause:+ -- 1. drop any patterns before record projection to suppress the instance arg+ -- 2. use record proj. as function name+ -- 3. process remaing patterns as usual++ -- 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)+ p : ps -> do+ let c' = c {namedClausePats = ps}+ ProjP _ q = namedArg p++ -- We want the actual field name, not the instance-opened projection.+ (q, _, _) <- origProjection q+ arg <- fieldArgInfo q+ let uf = hsName $ prettyShow $ nameConcrete $ qnameName q++ let+ (.~) :: QName -> QName -> Bool+ x .~ y = nameConcrete (qnameName x) == nameConcrete (qnameName y)++ resolveExtendedLambda :: QName -> C QName+ resolveExtendedLambda n | isExtendedLambdaName n = defName <$> getConstInfo n+ | otherwise = return n++ chaseDef :: QName -> C Definition+ chaseDef n = do+ d <- getConstInfo n+ let Function {..} = theDef d+ case funClauses of+ [ Clause {clauseBody = Just (Def n' [])} ] -> do+ chaseDef n'+ _ -> return d++ if+ | isInstance arg, usableModality arg -> do+ unless (null ps) $ genericDocError =<< text "not allowed: explicitly giving superclass"+ body <- case clauseBody c' of+ Nothing -> genericDocError =<< text "not allowed: absurd clause for superclass"+ Just b -> return b+ addContext (clauseTel c') $ checkInstance body+ return ([], [])+ | not (keepArg arg) -> return ([], [])+ -- Projection of a primitive field: chase down definition and inline as instance clause.+ | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'+ , [(_, f)] <- mapMaybe isProjElim es+ , f .~ q+ -> do d <- chaseDef n+ fc <- compileFun False d+ let hd = hsName $ prettyShow $ nameConcrete $ qnameName $ defName d+ let fc' = dropPatterns 1 $ replaceName hd uf fc+ return (map (Hs.InsDecl ()) fc', [n])++ -- Projection of a default implementation: drop while making sure these are drawn from the+ -- same (minimal) dictionary as the primitive fields.+ | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'+ , n .~ q+ , Just [ Def n' _ ] <- map unArg . filter keepArg <$> allApplyElims es+ -> do n' <- resolveExtendedLambda n'+ return ([], [n'])++ -- No minimal dictionary used, proceed with compiling as a regular clause.+ | otherwise+ -> do ms <- disableCopatterns $ compileClause curModule uf c'+ return ([Hs.InsDecl () (Hs.FunBind () [ms]) | keepArg arg], [])++fieldArgInfo :: QName -> C ArgInfo+fieldArgInfo f = do+ r <- maybe badness return =<< liftTCM (getRecordOfField f)+ Record{ recFields = fs } <- theDef <$> getConstInfo r+ case filter ((== f) . unDom) fs of+ df : _ -> return $ getArgInfo df+ [] -> badness+ where+ badness = genericDocError =<< text "Not a record field:" <+> prettyTCM f++findDefinitions :: (QName -> Definition -> C Bool) -> ModuleName -> C [Definition]+findDefinitions p m = do+ localDefs <- (^. sigDefinitions) <$> (^. stSignature) <$> getTCState+ importedDefs <- (^. sigDefinitions) <$> (^. stImports) <$> getTCState+ let allDefs = HMap.union localDefs importedDefs+ inMod = [ (x, def) | (x, def) <- HMap.toList allDefs, isInModule x m ]+ map snd <$> filterM (uncurry p) inMod++resolveStringName :: String -> C QName+resolveStringName s = do+ cqname <- liftTCM $ parseName noRange s+ rname <- liftTCM $ resolveName cqname+ case rname of+ DefinedName _ aname _ -> return $ anameName aname+ _ -> genericDocError =<< text ("Couldn't find " ++ s)++lookupDefaultImplementations :: QName -> [Hs.Name ()] -> C [Definition]+lookupDefaultImplementations recName fields = do+ let modName = qnameToMName recName+ isField f _ = (`elem` fields) . unQual <$> compileQName f+ findDefinitions isField modName++classMemberNames :: Definition -> C [Hs.Name ()]+classMemberNames def =+ case theDef def of+ Record{recFields = fs} -> fmap unQual <$> traverse compileQName (map unDom fs)+ _ -> genericDocError =<< text "Not a record:" <+> prettyTCM (defName def)
+ src/Agda2Hs/Compile/Data.hs view
@@ -0,0 +1,78 @@+module Agda2Hs.Compile.Data where++import qualified Language.Haskell.Exts.Syntax as Hs++import Agda.Compiler.Backend+import Agda.Syntax.Common+import Agda.Syntax.Internal++import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Reduce+import Agda.TypeChecking.Substitute+import Agda.TypeChecking.Telescope++import Agda.Utils.Pretty ( prettyShow )+import Agda.Utils.Impossible ( __IMPOSSIBLE__ )++import Agda2Hs.Compile.Type ( compileDom, compileTeleBinds )+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.HsUtils++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"++compileData :: DataTarget -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()]+compileData target ds def = setCurrentRange (nameBindingSite $ qnameName $ defName def) $ do+ let d = hsName $ prettyShow $ qnameName $ defName def+ checkValidTypeName d+ case theDef def of+ Datatype{dataPars = n, dataIxs = numIxs, dataCons = cs} -> do+ TelV tel t <- telViewUpTo n (defType def)+ reportSDoc "agda2hs.data" 10 $ text "Datatype telescope:" <+> prettyTCM tel+ allIndicesErased t+ let params = teleArgs tel+ addContext tel $ do+ binds <- compileTeleBinds tel+ cs <- mapM (compileConstructor params) cs+ let hd = foldl (Hs.DHApp ()) (Hs.DHead () d) binds++ case target of+ ToData -> return [Hs.DataDecl () (Hs.DataType ()) Nothing hd cs ds]+ ToDataNewType -> do+ checkNewtype d cs+ return [Hs.DataDecl () (Hs.NewType ()) Nothing hd cs ds]+ _ -> __IMPOSSIBLE__+ where+ allIndicesErased :: Type -> C ()+ allIndicesErased t = reduce (unEl t) >>= \case+ Pi dom t -> compileDom (absName t) dom >>= \case+ DomDropped -> allIndicesErased (unAbs t)+ DomType{} -> genericDocError =<< text "Not supported: indexed datatypes"+ DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types"+ _ -> return ()++compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())+compileConstructor params c = checkingVars $ do+ reportSDoc "agda2hs.data.con" 15 $ text "compileConstructor" <+> prettyTCM c+ reportSDoc "agda2hs.data.con" 20 $ text " params = " <+> prettyTCM params+ ty <- (`piApplyM` params) . defType =<< getConstInfo c+ reportSDoc "agda2hs.data.con" 20 $ text " ty = " <+> prettyTCM ty+ TelV tel _ <- telView ty+ let conName = hsName $ prettyShow $ qnameName c+ checkValidConName conName+ args <- compileConstructorArgs tel+ return $ Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args++compileConstructorArgs :: Telescope -> C [Hs.Type ()]+compileConstructorArgs EmptyTel = return []+compileConstructorArgs (ExtendTel a tel) = compileDom (absName tel) a >>= \case+ DomType s hsA -> do+ ty <- addTyBang s hsA+ (ty :) <$> underAbstraction a tel compileConstructorArgs+ DomConstraint hsA -> genericDocError =<< text "Not supported: constructors with class constraints"+ DomDropped -> underAbstraction a tel compileConstructorArgs
+ src/Agda2Hs/Compile/Function.hs view
@@ -0,0 +1,271 @@+{-# LANGUAGE OverloadedStrings #-}+module Agda2Hs.Compile.Function where++import Control.Monad ( (>=>), filterM, forM_ )+import Control.Monad.Reader ( asks )++import Data.Generics+import Data.List+import Data.Maybe ( fromMaybe, isJust )+import qualified Data.Text as Text++import qualified Language.Haskell.Exts.Syntax as Hs+import qualified Language.Haskell.Exts.Build as Hs++import Agda.Compiler.Backend+import Agda.Compiler.Common++import Agda.Syntax.Common+import Agda.Syntax.Internal+import Agda.Syntax.Literal++import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Substitute+import Agda.TypeChecking.Telescope ( telView )+import Agda.TypeChecking.Sort ( ifIsSort )++import Agda.Utils.Functor ( (<&>) )+import Agda.Utils.Impossible ( __IMPOSSIBLE__ )+import Agda.Utils.Pretty ( prettyShow )+import Agda.Utils.Monad++import Agda2Hs.AgdaUtils+import Agda2Hs.Compile.Name ( compileQName )+import Agda2Hs.Compile.Term ( compileTerm, compileVar )+import Agda2Hs.Compile.Type ( compileTopLevelType )+import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.HsUtils++isSpecialPat :: QName -> Maybe (ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ()))+isSpecialPat qn = case prettyShow qn of+ "Haskell.Prim.Tuple._;_" -> Just tuplePat+ "Agda.Builtin.Int.Int.pos" -> Just posIntPat+ "Agda.Builtin.Int.Int.negsuc" -> Just negSucIntPat+ s | s `elem` badConstructors -> Just $ \ _ _ _ -> genericDocError =<<+ "constructor `" <> prettyTCM qn <> "` not supported in patterns"+ _ -> Nothing+ where+ badConstructors =+ [ "Agda.Builtin.Nat.Nat.zero"+ , "Agda.Builtin.Nat.Nat.suc"+ ]++isUnboxCopattern :: DeBruijnPattern -> C Bool+isUnboxCopattern (ProjP _ q) = isJust <$> isUnboxProjection q+isUnboxCopattern _ = return False++tuplePat :: ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())+tuplePat cons i ps = do+ let p = ConP cons i ps+ err = sep [ "Tuple pattern"+ , nest 2 $ prettyTCM p+ , "does not have a known size." ]+ xs <- makeListP' "Agda.Builtin.Unit.tt" "Haskell.Prim.Tuple._;_" err p+ qs <- mapM compilePat xs+ return $ Hs.PTuple () Hs.Boxed qs++-- Agda2Hs does not support natural number patterns directly (since+-- they don't exist in Haskell), however they occur as part of+-- patterns of type Integer, so we need to compile literal natural+-- number patterns.+compileLitNatPat :: DeBruijnPattern -> C Integer+compileLitNatPat = \case+ ConP ch _ ps+ | prettyShow (conName ch) == "Agda.Builtin.Nat.Nat.zero" -> return 0+ | prettyShow (conName ch) == "Agda.Builtin.Nat.Nat.suc"+ , [p] <- ps -> (1+) <$> compileLitNatPat (namedArg p)+ p -> genericDocError =<< "not a literal natural number pattern:" <?> prettyTCM p++posIntPat :: ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())+posIntPat c i [p] = do+ n <- compileLitNatPat (namedArg p)+ return $ Hs.PLit () (Hs.Signless ()) (Hs.Int () n (show n))+posIntPat _ _ _ = __IMPOSSIBLE__++negSucIntPat :: ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())+negSucIntPat c i [p] = do+ n <- (1+) <$> compileLitNatPat (namedArg p)+ return $ Hs.PLit () (Hs.Negative ()) (Hs.Int () n (show (negate n)))+negSucIntPat _ _ _ = __IMPOSSIBLE__++-- The bool argument says whether we also want the type signature or just the body+compileFun, compileFun' :: Bool -> Definition -> C [Hs.Decl ()]+-- initialize locals when first stepping into a function+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+ let keepClause = maybe False keepArg . clauseType+ withCurrentModule m $ setCurrentRange (nameBindingSite n) $ do+ ifM (endsInSort defType) (ensureNoLocals err >> compileTypeDef x def) $ do+ when withSig $ checkValidFunName x+ compileTopLevelType withSig defType $ \ty -> do+ -- Instantiate the clauses to the current module parameters+ pars <- getContextArgs+ reportSDoc "agda2hs.compile" 10 $ "applying clauses to parameters: " <+> prettyTCM pars+ let clauses = filter keepClause funClauses `apply` pars+ cs <- mapM (compileClause (qnameModule defName) x) clauses+ return $ [Hs.TypeSig () [x] ty | withSig ] ++ [Hs.FunBind () cs]+ where+ Function{..} = theDef+ m = qnameModule defName+ n = qnameName defName+ x = hsName $ prettyShow n+ endsInSort t = do+ TelV tel b <- telView t+ addContext tel $ ifIsSort b (\_ -> return True) (return False)+ err = "Not supported: type definition with `where` clauses"++compileClause :: ModuleName -> Hs.Name () -> Clause -> C (Hs.Match ())+compileClause curModule x c@Clause{..} = withClauseLocals curModule c $ do+ reportSDoc "agda2hs.compile" 7 $ "compiling clause: " <+> prettyTCM c+ addContext (KeepNames clauseTel) $ do+ ps <- compilePats namedClausePats+ ls <- asks locals+ let+ (children, ls') = partition+ ( not . isExtendedLambdaName+ /\ (curModule `isFatherModuleOf`) . qnameModule )+ ls+ withLocals ls' $ do+ body <- compileTerm $ fromMaybe __IMPOSSIBLE__ clauseBody+ whereDecls <- mapM (getConstInfo >=> compileFun' True) children+ let rhs = Hs.UnGuardedRhs () body+ whereBinds | null whereDecls = Nothing+ | otherwise = Just $ Hs.BDecls () (concat whereDecls)+ match = case (x, ps) of+ (Hs.Symbol{}, p : q : ps) -> Hs.InfixMatch () p x (q : ps) rhs whereBinds+ _ -> Hs.Match () x ps rhs whereBinds+ return match++noAsPatterns :: DeBruijnPattern -> C ()+noAsPatterns = \case+ VarP i _ -> checkPatternInfo i+ DotP i _ -> checkPatternInfo i+ ConP _ cpi ps -> do+ checkPatternInfo $ conPInfo cpi+ forM_ ps $ noAsPatterns . namedArg+ LitP i _ -> checkPatternInfo i+ ProjP{} -> return ()+ IApplyP i _ _ _ -> checkPatternInfo i+ DefP i _ ps -> do+ checkPatternInfo i+ forM_ ps $ noAsPatterns . namedArg+ where+ checkPatternInfo i = unless (null $ patAsNames i) $+ genericDocError =<< "not supported by agda2hs: as patterns"++compilePats :: NAPs -> C [Hs.Pat ()]+compilePats ps = mapM (compilePat . namedArg) =<< filterM keepPat ps+ where+ keepPat :: NamedArg DeBruijnPattern -> C Bool+ keepPat p = do+ keep <- return (keepArg p) `and2M` (not <$> isUnboxCopattern (namedArg p))+ when keep $ noAsPatterns $ namedArg p+ -- We do not allow forced (dot) patterns for non-erased arguments (see issue #142).+ when (usableModality p && isForcedPat (namedArg p)) $+ genericDocError =<< "not supported by agda2hs: forced (dot) patterns in non-erased positions"+ return keep++ isForcedPat :: DeBruijnPattern -> Bool+ isForcedPat = \case+ VarP{} -> False+ DotP{} -> True+ ConP c cpi ps -> conPLazy cpi+ LitP{} -> False+ ProjP{} -> False+ IApplyP{} -> False+ DefP{} -> False+++compilePat :: DeBruijnPattern -> C (Hs.Pat ())+compilePat p@(VarP o x)+ | PatOWild <- patOrigin o = return $ Hs.PWildCard ()+ | otherwise = do+ n <- hsName <$> compileVar (dbPatVarIndex x)+ checkValidVarName n+ return $ Hs.PVar () n+compilePat (ConP h i ps)+ | Just semantics <- isSpecialPat (conName h) = setCurrentRange h $ semantics h i ps+compilePat (ConP h _ ps) = isUnboxConstructor (conName h) >>= \case+ Just s -> compileErasedConP ps >>= addPatBang s+ Nothing -> do+ ps <- compilePats ps+ c <- compileQName (conName h)+ return $ pApp c ps+compilePat (LitP _ l) = compileLitPat l+compilePat (ProjP _ q) = do+ reportSDoc "agda2hs.compile" 6 $ "compiling copattern: " <+> text (prettyShow q)+ unlessM (asks copatternsEnabled) $+ genericDocError =<< "not supported in Haskell: copatterns"+ let x = hsName $ prettyShow q+ return $ Hs.PVar () x+compilePat p = genericDocError =<< "bad pattern:" <?> prettyTCM p++compileErasedConP :: NAPs -> C (Hs.Pat ())+compileErasedConP ps = compilePats ps <&> \case+ [p] -> p+ _ -> __IMPOSSIBLE__++compileLitPat :: Literal -> C (Hs.Pat ())+compileLitPat = \case+ LitChar c -> return $ Hs.charP c+ l -> genericDocError =<< "bad literal pattern:" <?> prettyTCM l++-- Local (where) declarations ---------------------------------------------++-- | Before checking a function, grab all of its local declarations.+-- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax+withFunctionLocals :: QName -> C a -> C a+withFunctionLocals q k = do+ ls <- takeWhile (isAnonymousModuleName . qnameModule)+ . dropWhile (<= q)+ . map fst+ . sortDefs <$> liftTCM curDefs+ withLocals ls k++-- | Retain only those local declarations that belong to current clause's module.+zoomLocals :: ModuleName -> LocalDecls -> LocalDecls+zoomLocals mname = filter ((mname `isLeParentModuleOf`) . qnameModule)++-- | Before checking a clause, grab all of its local declarationaas.+-- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax+withClauseLocals :: ModuleName -> Clause -> C a -> C a+withClauseLocals curModule c@Clause{..} k = do+ ls <- asks locals+ let+ uses = filter+ ( (curModule `isFatherModuleOf`) . qnameModule+ \/ (`extLamUsedIn` c) )+ (getLocalUses ls c)+ nonExtLamUses = qnameModule <$> filter (not . isExtendedLambdaName) uses+ whereModuleName+ | null uses = Nothing+ | otherwise = Just $ head (nonExtLamUses ++ [curModule])+ ls' = case whereModuleName of+ Nothing -> []+ Just m -> zoomLocals m ls+ withLocals ls' k++checkTransparentPragma :: Definition -> C ()+checkTransparentPragma def = compileFun False def >>= \case+ [Hs.FunBind _ cls] ->+ mapM_ checkTransparentClause cls+ [Hs.TypeDecl _ hd b] ->+ checkTransparentTypeDef hd b+ _ -> __IMPOSSIBLE__+ where+ checkTransparentClause :: Hs.Match () -> C ()+ checkTransparentClause = \case+ Hs.Match _ _ [p] (Hs.UnGuardedRhs _ e) _ | patToExp p == Just e -> return ()+ _ -> errNotTransparent++ checkTransparentTypeDef :: Hs.DeclHead () -> Hs.Type () -> C ()+ checkTransparentTypeDef (Hs.DHApp _ _ (Hs.UnkindedVar _ x)) (Hs.TyVar _ y) | x == y = return ()+ checkTransparentTypeDef _ _ = errNotTransparent++ errNotTransparent = genericDocError =<<+ "Cannot make function" <+> prettyTCM (defName def) <+> "transparent." <+>+ "A transparent function must have exactly one non-erased argument and return it unchanged."
+ src/Agda2Hs/Compile/Function.hs-boot view
@@ -0,0 +1,7 @@+module Agda2Hs.Compile.Function where++import qualified Language.Haskell.Exts.Syntax as Hs ( Match, Name )+import Agda.Syntax.Internal ( Clause, ModuleName )+import Agda2Hs.Compile.Types ( C )++compileClause :: ModuleName -> Hs.Name () -> Clause -> C (Hs.Match ())
+ src/Agda2Hs/Compile/Imports.hs view
@@ -0,0 +1,78 @@++module Agda2Hs.Compile.Imports ( compileImports ) where++import Data.Char ( isUpper )+import Data.List ( isPrefixOf )+import Data.Map ( Map )+import qualified Data.Map as Map+import Data.Set ( Set )+import qualified Data.Set as Set++import qualified Language.Haskell.Exts as Hs++import Agda.Compiler.Backend+import Agda.TypeChecking.Pretty ( text )+import Agda.Utils.Pretty ( prettyShow )++import Agda2Hs.AgdaUtils+import Agda2Hs.Compile.Name+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.HsUtils++type ImportSpecMap = Map (Hs.Name ()) (Set (Hs.Name ()))+type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap++compileImports :: String -> Imports -> TCM [Hs.ImportDecl ()]+compileImports top is0 = do+ let is = filter (not . (top `isPrefixOf`) . Hs.prettyPrint . importModule) is0+ checkClashingImports is+ let imps = Map.toList $ groupModules is+ return $ map (uncurry $ uncurry makeImportDecl) imps+ where+ mergeChildren :: ImportSpecMap -> ImportSpecMap -> ImportSpecMap+ mergeChildren = Map.unionWith Set.union++ makeSingle :: Maybe (Hs.Name ()) -> Hs.Name () -> ImportSpecMap+ makeSingle Nothing q = Map.singleton q Set.empty+ makeSingle (Just p) q = Map.singleton p $ Set.singleton q++ groupModules :: [Import] -> ImportDeclMap+ groupModules = foldr+ (\(Import mod as p q) -> Map.insertWith mergeChildren (mod,as) (makeSingle p q))+ Map.empty++ -- TODO: avoid having to do this by having a CName instead of a+ -- Name in the Import datatype+ makeCName :: Hs.Name () -> Hs.CName ()+ makeCName n@(Hs.Ident _ s)+ | isUpper (head s) = Hs.ConName () n+ | otherwise = Hs.VarName () n+ makeCName n@(Hs.Symbol _ s)+ | head s == ':' = Hs.ConName () n+ | otherwise = Hs.VarName () n++ makeImportSpec :: Hs.Name () -> Set (Hs.Name ()) -> Hs.ImportSpec ()+ makeImportSpec q qs+ | Set.null qs = Hs.IVar () q+ | otherwise = Hs.IThingWith () q $ map makeCName $ Set.toList qs++ makeImportDecl :: Hs.ModuleName () -> Qualifier -> ImportSpecMap -> Hs.ImportDecl ()+ makeImportDecl mod qual specs = Hs.ImportDecl ()+ mod (isQualified qual) False False Nothing (qualifiedAs qual)+ (Just $ Hs.ImportSpecList () False $ map (uncurry makeImportSpec) $ Map.toList specs)++ checkClashingImports :: Imports -> TCM ()+ checkClashingImports [] = return ()+ checkClashingImports (Import mod as p q : is) =+ case filter isClashing is of+ (i : _) -> genericDocError =<< text (mkErrorMsg i)+ [] -> checkClashingImports is+ where+ isClashing (Import _ as' p' q') = (as' == as) && (p' /= p) && (q' == q)+ mkErrorMsg (Import _ _ p' q') =+ "Clashing import: " ++ pp q ++ " (both from "+ ++ prettyShow (pp <$> p) ++ " and "+ ++ prettyShow (pp <$> p') ++ ")"+ -- TODO: no range information as we only have Haskell names at this point+
+ src/Agda2Hs/Compile/Name.hs view
@@ -0,0 +1,158 @@+module Agda2Hs.Compile.Name where++import Control.Arrow ( (>>>) )+import Control.Applicative ( (<|>) )+import Control.Monad+import Control.Monad.Reader++import Data.List ( intercalate, isPrefixOf )+import Data.Text ( unpack )++import qualified Language.Haskell.Exts as Hs++import Agda.Compiler.Backend hiding ( topLevelModuleName )+import Agda.Compiler.Common ( topLevelModuleName )++import Agda.Syntax.Common+import Agda.Syntax.Position+import qualified Agda.Syntax.Concrete as C+import Agda.Syntax.Scope.Base ( inverseScopeLookupName )+import Agda.Syntax.TopLevelModuleName++import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Records ( isRecordConstructor )++import qualified Agda.Utils.List1 as List1+import Agda.Utils.Maybe ( isJust, whenJust, fromMaybe, caseMaybeM )+import Agda.Utils.Pretty ( prettyShow )+import qualified Agda.Utils.Pretty as P ( Pretty(pretty) )++import Agda2Hs.AgdaUtils+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.HsUtils++isSpecialCon :: QName -> Maybe (Hs.QName ())+isSpecialCon = prettyShow >>> \case+ "Agda.Builtin.List.List" -> special Hs.ListCon+ "Agda.Builtin.List.List._∷_" -> special Hs.Cons+ "Agda.Builtin.List.List.[]" -> special Hs.ListCon+ "Agda.Builtin.Unit.⊤" -> special Hs.UnitCon+ "Agda.Builtin.Unit.tt" -> special Hs.UnitCon+ _ -> Nothing+ where special c = Just (Hs.Special () $ c ())++isSpecialName :: QName -> Maybe (Hs.Name (), Maybe Import)+isSpecialName = prettyShow >>> \case+ "Agda.Builtin.Nat.Nat" -> withImport "Numeric.Natural" "Natural"+ "Agda.Builtin.Int.Int" -> noImport "Integer"+ "Agda.Builtin.Word.Word64" -> noImport "Word"+ "Agda.Builtin.Float.Float" -> noImport "Double"+ "Agda.Builtin.Bool.Bool.false" -> noImport "False"+ "Agda.Builtin.Bool.Bool.true" -> noImport "True"+ "Haskell.Prim._∘_" -> noImport "_._"+ "Haskell.Prim.seq" -> noImport "seq"+ "Haskell.Prim._$!_" -> noImport "_$!_"+ "Haskell.Prim.Monad.Dont._>>=_" -> noImport "_>>=_"+ "Haskell.Prim.Monad.Dont._>>_" -> noImport "_>>_"+ _ -> Nothing+ where+ noImport x = Just (hsName x, Nothing)+ withImport mod x =+ let imp = Import (hsModuleName mod) Unqualified Nothing (hsName x)+ in Just (hsName x, Just imp)++compileName :: Applicative m => Name -> m (Hs.Name ())+compileName n = hsName . show <$> pretty (nameConcrete n)++compileQName :: QName -> C (Hs.QName ())+compileQName f+ | Just c <- isSpecialCon f+ = do+ reportSDoc "agda2hs.name" 25 $ text $+ "compiling name: " ++ prettyShow f +++ " to special constructor: " ++ Hs.prettyPrint c+ return c+ | otherwise = do+ f <- isRecordConstructor f >>= return . \case+ Just (r, Record{recNamedCon = False}) -> r -- use record name for unnamed constructors+ _ -> f+ hf0 <- compileName (qnameName f)+ let (hf, mimpBuiltin) = fromMaybe (hf0, Nothing) (isSpecialName f)+ parent <- parentName f+ par <- traverse (compileName . qnameName) parent+ let mod0 = qnameModule $ fromMaybe f parent+ mod <- compileModuleName mod0+ currMod <- hsTopLevelModuleName <$> asks currModule+ let skipModule = mod == currMod+ || isJust mimpBuiltin+ || prettyShow mod0 `elem` primMonadModules+ qual <- if | skipModule -> return Unqualified+ | otherwise -> getQualifier (fromMaybe f parent) mod+ let (mod', mimp) = mkImport mod qual par hf+ qf = qualify mod' hf qual++ -- add (possibly qualified) import+ whenJust (mimpBuiltin <|> mimp) tellImport++ reportSDoc "agda2hs.name" 25 $ text+ $ "-------------------------------------------------"+ ++ "\ncompiling name: " ++ prettyShow f+ ++ "\nhaskell name: " ++ Hs.prettyPrint hf+ ++ "\nparent name: " ++ prettyShow parent+ ++ "\nmod0: " ++ prettyShow mod0+ ++ "\nmodule name: " ++ Hs.prettyPrint mod+ ++ "\ncurrent module: " ++ Hs.prettyPrint currMod+ ++ "\nqualifier: " ++ prettyShow (fmap (fmap pp) qual)+ ++ "\n(qualified) haskell name: " ++ pp qf+ return qf+ where+ parentName :: QName -> C (Maybe QName)+ parentName q = (theDef <$> getConstInfo q) >>= return . \case+ Constructor {conData = dt} -> Just dt+ Function {funProjection = proj}+ | Right (Projection {projProper = Just{}, projFromType = rt}) <- proj+ -> Just $ unArg rt+ _ -> Nothing++ getQualifier :: QName -> Hs.ModuleName () -> C Qualifier+ getQualifier f mod =+ (inverseScopeLookupName f <$> getScope) >>= return . \case+ (C.Qual as C.QName{} : _)+ | qual <- hsModuleName $ prettyShow as, qual /= mod+ -> QualifiedAs (Just qual)+ (C.Qual{} : _) -> QualifiedAs Nothing+ _ -> Unqualified++ qualify :: Hs.ModuleName () -> Hs.Name () -> Qualifier -> Hs.QName ()+ qualify mod n = \case+ (QualifiedAs as) -> Hs.Qual () (fromMaybe mod as) n+ Unqualified -> Hs.UnQual () n++ primModules = ["Agda.Builtin", "Haskell.Prim", "Haskell.Prelude"]+ primMonadModules = ["Haskell.Prim.Monad.Dont", "Haskell.Prim.Monad.Do"]++ mkImport mod qual par hf+ -- make sure the Prelude is properly qualified+ | any (`isPrefixOf` pp mod) primModules+ = if isQualified qual then+ let mod' = hsModuleName "Prelude"+ in (mod', Just (Import mod' qual Nothing hf))+ else (mod, Nothing)+ | otherwise+ = (mod, Just (Import mod qual par hf))++hsTopLevelModuleName :: TopLevelModuleName -> Hs.ModuleName ()+hsTopLevelModuleName = hsModuleName . intercalate "." . map unpack+ . List1.toList . moduleNameParts++compileModuleName :: ModuleName -> C (Hs.ModuleName ())+compileModuleName m =+ caseMaybeM+ (liftTCM $ fmap hsTopLevelModuleName <$> getTopLevelModuleForModuleName m)+ (genericDocError =<< text "Cannot compile non-existing module: " <+> prettyTCM m)+ $ \tlm -> do+ reportSDoc "agda2hs.name" 25 $+ text "Top-level module name for" <+> prettyTCM m <+>+ text "is" <+> text (pp tlm)+ return tlm
+ src/Agda2Hs/Compile/Postulate.hs view
@@ -0,0 +1,25 @@+module Agda2Hs.Compile.Postulate where++import qualified Language.Haskell.Exts.Syntax as Hs++import Agda.Compiler.Backend++import Agda.Syntax.Internal++import Agda.Utils.Pretty ( prettyShow )++import Agda2Hs.Compile.Type ( compileType )+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.HsUtils++compilePostulate :: Definition -> C [Hs.Decl ()]+compilePostulate def = do+ let n = qnameName (defName def)+ x = hsName $ prettyShow n+ checkValidFunName x+ setCurrentRange (nameBindingSite n) $ do+ ty <- compileType (unEl $ defType def)+ let body = hsError $ "postulate: " ++ pp ty+ return [ Hs.TypeSig () [x] ty+ , Hs.FunBind () [Hs.Match () x [] (Hs.UnGuardedRhs () body) Nothing] ]
+ src/Agda2Hs/Compile/Record.hs view
@@ -0,0 +1,174 @@+module Agda2Hs.Compile.Record where++import Control.Monad ( unless )+import Control.Monad.Reader ( MonadReader(local) )++import Data.List ( (\\), nub )+import Data.List.NonEmpty ( NonEmpty(..) )+import Data.Map ( Map )+import qualified Data.Map as Map++import qualified Language.Haskell.Exts as Hs++import Agda.Compiler.Backend++import Agda.Syntax.Common ( Arg(unArg), defaultArg )+import Agda.Syntax.Internal++import Agda.TypeChecking.Pretty ( ($$), (<+>), text, vcat )+import Agda.TypeChecking.Substitute ( TelV(TelV), Apply(apply) )+import Agda.TypeChecking.Telescope++import Agda.Utils.Pretty ( prettyShow )+import Agda.Utils.Impossible ( __IMPOSSIBLE__ )++import Agda2Hs.AgdaUtils+import Agda2Hs.Compile.ClassInstance+import Agda2Hs.Compile.Function ( compileFun )+import Agda2Hs.Compile.Type ( compileDom, compileTeleBinds )+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.HsUtils++-- | Primitive fields and default implementations+type MinRecord = ([Hs.Name ()], Map (Hs.Name ()) (Hs.Decl ()))++withMinRecord :: QName -> C a -> C a+withMinRecord m = local $ \ e -> e { minRecordName = Just (qnameToMName m) }++compileMinRecord :: [Hs.Name ()] -> QName -> C MinRecord+compileMinRecord fieldNames m = do+ rdef <- getConstInfo m+ definedFields <- classMemberNames rdef+ let Record{recPars = npars, recTel = tel} = theDef rdef+ pars = map Apply $ take npars $ teleArgs tel+ rtype = El __DUMMY_SORT__ $ Def m pars+ defaults <- lookupDefaultImplementations m (fieldNames \\ definedFields)+ -- We can't simply compileFun here for two reasons:+ -- * it has an explicit dictionary argument+ -- * it's using the fields and definitions from the minimal record and not the parent record+ compiled <- withMinRecord m $ addContext (defaultDom rtype) $+ fmap concat $ traverse (compileFun False) defaults+ let declMap = Map.fromList [ (definedName c, def) | def@(Hs.FunBind _ (c : _)) <- compiled ]+ return (definedFields, declMap)++compileMinRecords :: Definition -> [String] -> C [Hs.Decl ()]+compileMinRecords def sls = do++ members <- classMemberNames def++ qnames <- traverse resolveStringName sls+ (prims, defaults) <- unzip <$> traverse (compileMinRecord members) qnames++ -- 0. [OPTIONAL] check all record signatures match (or simply leave to GHC)++ -- 1. build minimal pragma++ let+ -- make the formula for a list of names of methods for for a single minimal instance+ helpAnd :: [Hs.Name ()] -> Hs.BooleanFormula ()+ helpAnd xs = Hs.AndFormula () $ Hs.VarFormula () <$> xs++ -- combine formulae for all minimal instances+ helpOr :: [Hs.BooleanFormula ()] -> Hs.Decl ()+ helpOr bs = Hs.MinimalPragma () (Just $ Hs.OrFormula () bs)++ minPragma = helpOr (map helpAnd prims)++ -- 2. assert that all default implementations are the same (for a certain field)+ let getUnique f (x :| xs)+ | all (x ==) xs = return x+ | otherwise = genericDocError =<< do+ text ("Conflicting default implementations for " ++ pp f ++ ":") $$+ vcat [ text "-" <+> multilineText (pp d) | d <- nub (x : xs) ]+ decls <- Map.traverseWithKey getUnique+ $ Map.unionsWith (<>) $ (map . fmap) (:| []) defaults++ -- TODO: order default implementations differently?+ return ([minPragma | not (null prims)] ++ Map.elems decls)++compileRecord :: RecordTarget -> Definition -> C (Hs.Decl ())+compileRecord target def = setCurrentRange (nameBindingSite $ qnameName $ defName def) $ do+ TelV tel _ <- telViewUpTo recPars (defType def)+ addContext tel $ checkingVars $ do+ checkValidTypeName rName+ binds <- compileTeleBinds tel+ let hd = foldl (Hs.DHApp ()) (Hs.DHead () rName) binds+ let fieldTel = snd $ splitTelescopeAt recPars recTel+ case target of+ ToClass ms -> do+ (classConstraints, classDecls) <- compileRecFields classDecl recFields fieldTel+ let context = case classConstraints of+ [] -> Nothing+ [asst] -> Just (Hs.CxSingle () asst)+ assts -> Just (Hs.CxTuple () assts)+ defaultDecls <- compileMinRecords def ms+ return $ Hs.ClassDecl () context hd [] (Just (classDecls ++ map (Hs.ClsDecl ()) defaultDecls))+ ToRecord ds -> do+ checkValidConName cName+ (constraints, fieldDecls) <- compileRecFields fieldDecl recFields fieldTel+ compileDataRecord constraints fieldDecls (Hs.DataType ()) hd ds+ ToRecordNewType ds -> do+ checkValidConName cName+ (constraints, fieldDecls) <- compileRecFields fieldDecl recFields fieldTel+ checkSingleElement cName fieldDecls "Newtype must have exactly one field in constructor"+ compileDataRecord constraints fieldDecls (Hs.NewType ()) hd ds++ where+ rName = hsName $ prettyShow $ qnameName $ defName def+ cName | recNamedCon = hsName $ prettyShow $ qnameName $ conName recConHead+ | otherwise = rName -- Reuse record name for constructor if no given name++ -- In Haskell, projections live in the same scope as the record type, so check here that the+ -- record module has been opened.+ checkFieldInScope f = isInScopeUnqualified f >>= \case+ True -> return ()+ False -> setCurrentRange (nameBindingSite $ qnameName f) $ genericError $+ "Record projections (`" ++ prettyShow (qnameName f) +++ "` in this case) must be brought into scope when compiling to Haskell record types. " +++ "Add `open " ++ Hs.prettyPrint rName ++ " public` after the record declaration to fix this."++ Record{..} = theDef def++ classDecl :: Hs.Name () -> Hs.Type () -> Hs.ClassDecl ()+ classDecl n = Hs.ClsDecl () . Hs.TypeSig () [n]++ fieldDecl :: Hs.Name () -> Hs.Type () -> Hs.FieldDecl ()+ fieldDecl n = Hs.FieldDecl () [n]++ compileRecFields :: (Hs.Name () -> Hs.Type () -> b)+ -> [Dom QName] -> Telescope -> C ([Hs.Asst ()], [b])+ compileRecFields decl ns tel = case (ns, tel) of+ (_ , EmptyTel ) -> return ([], [])+ (n:ns, ExtendTel dom tel') -> do+ hsDom <- compileDom (absName tel') dom+ (hsAssts, hsFields) <- underAbstraction dom tel' $ compileRecFields decl ns+ case hsDom of+ DomType s hsA -> do+ let fieldName = hsName $ prettyShow $ qnameName $ unDom n+ fieldType <- addTyBang s hsA+ checkValidFunName fieldName+ return (hsAssts, decl fieldName fieldType : hsFields)+ DomConstraint hsA -> case target of+ ToClass{} -> return (hsA : hsAssts , hsFields)+ ToRecord{} -> genericError $+ "Not supported: record/class with constraint fields"+ DomDropped -> return (hsAssts , hsFields)+ (_, _) -> __IMPOSSIBLE__++ compileDataRecord :: [Hs.Asst ()] -> [Hs.FieldDecl ()] -- compiled rec fields+ -> Hs.DataOrNew () -- whether to compile to data or newtype+ -> Hs.DeclHead () -- the head of the type declaration+ -> [Hs.Deriving ()] -- data extracted from the pragma+ -> C (Hs.Decl ())+ compileDataRecord constraints fieldDecls don hd ds = do+ unless (null constraints) __IMPOSSIBLE__ -- no constraints for records+ mapM_ checkFieldInScope (map unDom recFields)+ let conDecl = Hs.QualConDecl () Nothing Nothing $ Hs.RecDecl () cName fieldDecls+ return $ Hs.DataDecl () don Nothing hd [conDecl] ds++checkUnboxPragma :: Defn -> C ()+checkUnboxPragma def@Record{ recFields = (f:fs) }+ | keepArg f , all (not . keepArg) fs , not (recRecursive def) = return ()+checkUnboxPragma _ = genericError $+ "An unboxed type must be a non-recursive record type with exactly one non-erased field."
+ src/Agda2Hs/Compile/Term.hs view
@@ -0,0 +1,291 @@+module Agda2Hs.Compile.Term where++import Control.Arrow ( (>>>), (&&&) )+import Control.Monad ( unless )+import Control.Monad.Reader++import Data.List ( isPrefixOf )+import Data.Maybe ( fromMaybe, isJust )+import qualified Data.Text as Text ( unpack )++import qualified Language.Haskell.Exts as Hs++import Agda.Syntax.Common+import Agda.Syntax.Literal+import Agda.Syntax.Internal++import Agda.TypeChecking.Monad+import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Reduce ( instantiate )+import Agda.TypeChecking.Substitute ( Apply(applyE) )++import Agda.Utils.Lens+import Agda.Utils.Pretty ( prettyShow )+import qualified Agda.Utils.Pretty as P++import Agda.Utils.Impossible ( __IMPOSSIBLE__ )+import Agda.Utils.Monad+import Agda.Utils.Size++import Agda2Hs.AgdaUtils+import Agda2Hs.Compile.Name ( compileQName )+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.HsUtils++import {-# SOURCE #-} Agda2Hs.Compile.Function ( compileClause )++isSpecialTerm :: QName -> Maybe (QName -> Elims -> C (Hs.Exp ()))+isSpecialTerm q = case prettyShow q of+ _ | isExtendedLambdaName q -> Just lambdaCase+ "Haskell.Prim.if_then_else_" -> Just ifThenElse+ "Haskell.Prim.Enum.Enum.enumFrom" -> Just mkEnumFrom+ "Haskell.Prim.Enum.Enum.enumFromTo" -> Just mkEnumFromTo+ "Haskell.Prim.Enum.Enum.enumFromThen" -> Just mkEnumFromThen+ "Haskell.Prim.Enum.Enum.enumFromThenTo" -> Just mkEnumFromThenTo+ "Haskell.Prim.case_of_" -> Just caseOf+ "Haskell.Prim.Monad.Do.Monad._>>=_" -> Just bind+ "Haskell.Prim.Monad.Do.Monad._>>_" -> Just sequ+ "Agda.Builtin.FromNat.Number.fromNat" -> Just fromNat+ "Agda.Builtin.FromNeg.Negative.fromNeg" -> Just fromNeg+ "Agda.Builtin.FromString.IsString.fromString" -> Just fromString+ _ -> Nothing++isSpecialCon :: QName -> Maybe (ConHead -> ConInfo -> Elims -> C (Hs.Exp ()))+isSpecialCon = prettyShow >>> \case+ "Haskell.Prim.Tuple._;_" -> Just tupleTerm+ _ -> Nothing++fromNat :: QName -> Elims -> C (Hs.Exp ())+fromNat _ es = compileElims es <&> \case+ _ : n@Hs.Lit{} : es' -> n `eApp` es'+ es' -> hsVar "fromIntegral" `eApp` drop 1 es'++fromNeg :: QName -> Elims -> C (Hs.Exp ())+fromNeg _ es = compileElims es <&> \case+ _ : n@Hs.Lit{} : es' -> Hs.NegApp () n `eApp` es'+ es' -> (hsVar "negate" `o` hsVar "fromIntegral") `eApp` drop 1 es'+ where+ f `o` g = Hs.InfixApp () f (Hs.QVarOp () $ hsUnqualName "_._") g++fromString :: QName -> Elims -> C (Hs.Exp ())+fromString _ es = compileElims es <&> \case+ _ : s@Hs.Lit{} : es' -> s `eApp` es'+ es' -> hsVar "fromString" `eApp` drop 1 es'++tupleTerm :: ConHead -> ConInfo -> Elims -> C (Hs.Exp ())+tupleTerm cons i es = do+ let v = Con cons i es+ err = sep [ text "Tuple value"+ , nest 2 $ prettyTCM v+ , text "does not have a known size." ]+ xs <- makeList' "Agda.Builtin.Unit.tt" "Haskell.Prim.Tuple._;_" err v+ ts <- mapM compileTerm xs+ return $ Hs.Tuple () Hs.Boxed ts++ifThenElse :: QName -> Elims -> C (Hs.Exp ())+ifThenElse _ es = compileElims es >>= \case+ -- fully applied+ b : t : f : es' -> return $ Hs.If () b t f `eApp` es'+ -- partially applied+ _ -> genericError $ "if_then_else must be fully applied"++mkEnumFrom :: QName -> Elims -> C (Hs.Exp ())+mkEnumFrom q es = compileElims es >>= \case+ _ : a : es' -> return $ Hs.EnumFrom () a `eApp` es'+ es' -> return $ hsVar "enumFrom" `eApp` drop 1 es'++mkEnumFromTo :: QName -> Elims -> C (Hs.Exp ())+mkEnumFromTo q es = compileElims es >>= \case+ _ : a : b : es' -> return $ Hs.EnumFromTo () a b `eApp` es'+ es' -> return $ hsVar "enumFromTo" `eApp` drop 1 es'++mkEnumFromThen :: QName -> Elims -> C (Hs.Exp ())+mkEnumFromThen q es = compileElims es >>= \case+ _ : a : a' : es' -> return $ Hs.EnumFromThen () a a' `eApp` es'+ es' -> return $ hsVar "enumFromThen" `eApp` drop 1 es'++mkEnumFromThenTo :: QName -> Elims -> C (Hs.Exp ())+mkEnumFromThenTo q es = compileElims es >>= \case+ _ : a : a' : b : es' -> return $ Hs.EnumFromThenTo () a a' b `eApp` es'+ es' -> return $ hsVar "enumFromThenTo" `eApp` drop 1 es'++delay :: QName -> Elims -> C (Hs.Exp ())+delay _ = compileErasedApp++force :: QName -> Elims -> C (Hs.Exp ())+force _ = compileErasedApp++bind :: QName -> Elims -> C (Hs.Exp ())+bind q (e:es) = do+ checkInstance $ unArg $ isApplyElim' __IMPOSSIBLE__ e+ compileElims es >>= \case+ [u, Hs.Lambda _ [p] v] -> return (bind' u p v)+ [u, Hs.LCase () [Hs.Alt () p (Hs.UnGuardedRhs () v) Nothing]] ->+ decrementLCase >> return (bind' u p v)+ vs -> return $ hsVar "_>>=_" `eApp` vs+ where+ bind' :: Hs.Exp () -> Hs.Pat () -> Hs.Exp () -> Hs.Exp ()+ bind' u p v =+ let stmt1 = Hs.Generator () p u in+ case v of+ Hs.Do _ stmts -> Hs.Do () (stmt1 : stmts)+ _ -> Hs.Do () [stmt1, Hs.Qualifier () v]+bind q [] = return $ hsVar "_>>=_"++sequ :: QName -> Elims -> C (Hs.Exp ())+sequ q (e:es) = do+ checkInstance $ unArg $ isApplyElim' __IMPOSSIBLE__ e+ compileElims es >>= \case+ (u : v : vs) -> do+ let stmt1 = Hs.Qualifier () u+ case v of+ Hs.Do _ stmts -> return $ Hs.Do () (stmt1 : stmts)+ _ -> return $ Hs.Do () [stmt1, Hs.Qualifier () v]+ vs -> return $ hsVar "_>>_" `eApp` vs+sequ q [] = return $ hsVar "_>>_"++caseOf :: QName -> Elims -> C (Hs.Exp ())+caseOf _ es = compileElims es >>= \case+ -- applied to pattern lambda+ e : Hs.LCase _ alts : es' -> do+ decrementLCase+ return $ eApp (Hs.Case () e alts) es'+ -- applied to regular lambda+ e : Hs.Lambda _ (p : ps) b : es' -> do+ let lam [] = id+ lam qs = Hs.Lambda () qs+ return $ eApp (Hs.Case () e [Hs.Alt () p (Hs.UnGuardedRhs () $ lam ps b) Nothing]) es'+ -- applied to non-lambda / partially applied+ _ -> genericError $ "case_of_ must be fully applied to a lambda"++lambdaCase :: QName -> Elims -> C (Hs.Exp ())+lambdaCase q es = setCurrentRange (nameBindingSite $ qnameName q) $ do+ Function{funClauses = cls, funExtLam = Just ExtLamInfo {extLamModule = mname}}+ <- theDef <$> getConstInfo q+ npars <- size <$> lookupSection mname+ let (pars, rest) = splitAt npars es+ cs = applyE cls pars+ ls <- filter (`extLamUsedIn` cs) <$> asks locals+ cs <- withLocals ls $ mapM (compileClause (qnameModule q) $ hsName "(lambdaCase)") cs+ case cs of+ -- If there is a single clause and all patterns got erased, we+ -- simply return the body.+ [Hs.Match _ _ [] (Hs.UnGuardedRhs _ rhs) _] -> return rhs+ _ -> do+ lcase <- hsLCase =<< mapM clauseToAlt cs -- Pattern lambdas cannot have where blocks+ eApp lcase <$> compileElims rest++clauseToAlt :: Hs.Match () -> C (Hs.Alt ())+clauseToAlt (Hs.Match _ _ [p] rhs wh) = pure $ Hs.Alt () p rhs wh+clauseToAlt (Hs.Match _ _ ps _ _) = genericError $ "Pattern matching lambdas must take a single argument"+clauseToAlt Hs.InfixMatch{} = __IMPOSSIBLE__++compileLiteral :: Literal -> C (Hs.Exp ())+compileLiteral (LitNat n) = return $ Hs.intE n+compileLiteral (LitFloat d) = return $ Hs.Lit () $ Hs.Frac () (toRational d) (show d)+compileLiteral (LitWord64 w) = return $ Hs.Lit () $ Hs.PrimWord () (fromIntegral w) (show w)+compileLiteral (LitChar c) = return $ Hs.charE c+compileLiteral (LitString t) = return $ Hs.Lit () $ Hs.String () s s+ where s = Text.unpack t+compileLiteral l = genericDocError =<< text "bad term:" <?> prettyTCM (Lit l)++compileVar :: Nat -> C String+compileVar x = do+ (d, n) <- (fmap snd &&& fst . unDom) <$> lookupBV x+ let cn = prettyShow $ nameConcrete n+ let b | notVisible d = "hidden"+ | hasQuantity0 d = "erased"+ | otherwise = ""+ whenM (asks checkVar) $ unless (null b) $ genericDocError =<<+ text ("Cannot use " <> b <> " variable " <> cn)+ return cn++compileTerm :: Term -> C (Hs.Exp ())+compileTerm v = do+ reportSDoc "agda2hs.compile" 7 $ text "compiling term:" <+> prettyTCM v+ reportSDoc "agda2hs.compile" 27 $ text "compiling term:" <+> pure (P.pretty v)+ case unSpine1 v of+ Var x es -> do+ s <- compileVar x+ hsVar s `app` es+ -- v currently we assume all record projections are instance+ -- args that need attention+ Def f es+ | Just semantics <- isSpecialTerm f -> semantics f es+ | otherwise -> isClassFunction f >>= \case+ True -> compileClassFunApp f es+ False -> (isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f >>= \case+ True -> compileErasedApp es+ False -> do+ -- Drop module parameters (unless projection-like)+ n <- (theDef <$> getConstInfo f) >>= \case+ Function{ funProjection = Right{} } -> return 0+ _ -> size <$> lookupSection (qnameModule f)+ (`app` drop n es) . Hs.Var () =<< compileQName f+ Con h i es+ | Just semantics <- isSpecialCon (conName h) -> semantics h i es+ Con h i es -> isUnboxConstructor (conName h) >>= \case+ Just _ -> compileErasedApp es+ Nothing -> (`app` es) . Hs.Con () =<< compileQName (conName h)+ Lit l -> compileLiteral l+ Lam v b | usableModality v, getOrigin v == UserWritten -> do+ when (patternInTeleName `isPrefixOf` absName b) $ genericDocError =<< do+ text "Record pattern translation not supported. Use a pattern matching lambda instead."+ unless (visible v) $ genericDocError =<< do+ text "Implicit lambda not supported: " <+> prettyTCM (absName b)+ hsLambda (absName b) <$> underAbstr_ b compileTerm+ Lam v b | usableModality v ->+ -- System-inserted lambda, no need to preserve the name.+ underAbstraction_ b $ \ body -> do+ x <- showTCM (Var 0 [])+ let hsx = hsVar x+ body <- compileTerm body+ return $ case body of+ Hs.InfixApp _ a op b+ | a == hsx -> Hs.RightSection () op b -- System-inserted visible lambdas can only come from sections+ _ -> hsLambda x body -- so we know x is not free in b.+ Lam v b ->+ -- Drop erased lambdas (#65)+ underAbstraction_ b $ \ body -> compileTerm body+ t -> genericDocError =<< text "bad term:" <?> prettyTCM t+ where+ app :: Hs.Exp () -> Elims -> C (Hs.Exp ())+ app hd es = eApp <$> pure hd <*> compileElims es++-- `compileErasedApp` compiles an application of an erased constructor+-- or projection.+compileErasedApp :: Elims -> C (Hs.Exp ())+compileErasedApp es = compileElims es >>= \case+ [] -> return $ hsVar "id"+ (v:vs) -> return $ v `eApp` vs++-- `compileClassFunApp` is used when we have a record projection and we want to+-- drop the first visible arg (the record)+compileClassFunApp :: QName -> Elims -> C (Hs.Exp ())+compileClassFunApp f es = do+ hf <- compileQName f+ case dropWhile notVisible (fromMaybe __IMPOSSIBLE__ $ allApplyElims es) of+ [] -> __IMPOSSIBLE__+ (x:xs) -> do+ curMod <- currentModule+ reportSDoc "agda2hs.compile" 15 $ nest 2 $ vcat+ [ text "symbol module: " <+> prettyTCM (qnameModule f)+ , text "current module: " <+> prettyTCM curMod+ ]+ unless (curMod `isLeChildModuleOf` qnameModule f) $ checkInstance $ unArg x+ args <- compileArgs xs+ return $ Hs.Var () hf `eApp` args++compileElims :: Elims -> C [Hs.Exp ()]+compileElims es = compileArgs $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es++compileArgs :: Args -> C [Hs.Exp ()]+compileArgs args = mapMaybeM compileArg args++compileArg :: Arg Term -> C (Maybe (Hs.Exp ()))+compileArg x = do+ reportSDoc "agda2hs.compile" 8 $ text "compiling argument" <+> prettyTCM x+ if | keepArg x -> Just <$> compileTerm (unArg x)+ | isInstance x, usableModality x -> Nothing <$ checkInstance (unArg $ x)+ | otherwise -> return Nothing
+ src/Agda2Hs/Compile/Type.hs view
@@ -0,0 +1,197 @@+{-# LANGUAGE TypeApplications #-}++module Agda2Hs.Compile.Type where++import Control.Arrow ( (>>>) )+import Control.Monad ( forM, when )+import Control.Monad.Reader ( asks )+import Data.Maybe ( mapMaybe )++import qualified Language.Haskell.Exts.Syntax as Hs+import qualified Language.Haskell.Exts.Extension as Hs+import qualified Language.Haskell.Exts.Pretty as Hs++import Agda.Compiler.Backend hiding ( Args )++import Agda.Syntax.Common+import Agda.Syntax.Internal++import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Reduce ( reduce )+import Agda.TypeChecking.Substitute+import Agda.TypeChecking.Telescope++import Agda.Utils.Impossible ( __IMPOSSIBLE__ )+import Agda.Utils.Pretty ( prettyShow )+import Agda.Utils.List ( downFrom )+import Agda.Utils.Maybe ( ifJustM, fromMaybe )+import Agda.Utils.Monad ( ifM, unlessM )+import Agda.Utils.Size ( Sized(size) )+import Agda.Utils.Functor ( ($>) )++import Agda2Hs.AgdaUtils+import Agda2Hs.Compile.Name ( compileQName )+import Agda2Hs.Compile.Term ( compileVar )+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.AgdaUtils+import Agda2Hs.HsUtils++isSpecialType :: QName -> Maybe (QName -> Elims -> C (Hs.Type ()))+isSpecialType = prettyShow >>> \case+ "Haskell.Prim.Tuple.Tuple" -> Just tupleType+ "Haskell.Prim.Tuple._×_" -> Just tupleType+ "Haskell.Prim.Tuple._×_×_" -> Just tupleType+ _ -> Nothing++tupleType' :: C Doc -> Term -> C [Term]+tupleType' err xs =+ reduce xs >>= \case+ Def q es+ | [] <- vis es, q ~~ "Agda.Builtin.Unit.⊤" -> pure []+ | [_,_] <- vis es, q ~~ "Haskell.Prim.Tuple.Pair" -> pairToTuple es+ _ -> genericDocError =<< err+ where+ vis es = [ unArg a | Apply a <- es, visible a ]++ pairToTuple :: Elims -> C [Term]+ pairToTuple es+ | Just [x, xs] <- allApplyElims es = (unArg x:) <$> tupleType' err (unArg xs)+ | otherwise = genericDocError =<< text "Bad arguments for Pair: " <?> text (show es)++tupleType :: QName -> Elims -> C (Hs.Type ())+tupleType q es = do+ let err = sep [ prettyTCM (Def q es)+ , text "is not a concrete sequence of types."+ ]+ xs <- reduce (Def q es) >>= tupleType' err+ ts <- mapM compileType xs+ return $ Hs.TyTuple () Hs.Boxed ts++constrainType :: Hs.Asst () -> Hs.Type () -> Hs.Type ()+constrainType c = \case+ Hs.TyForall _ as (Just (Hs.CxTuple _ cs)) t -> Hs.TyForall () as (Just (Hs.CxTuple () (c:cs))) t+ Hs.TyForall _ as (Just (Hs.CxSingle _ c')) t -> Hs.TyForall () as (Just (Hs.CxTuple () [c,c'])) t+ Hs.TyForall _ as _ t -> Hs.TyForall () as (Just (Hs.CxSingle () c)) t+ t -> Hs.TyForall () Nothing (Just (Hs.CxSingle () c)) t++qualifyType :: String -> Hs.Type () -> Hs.Type ()+qualifyType s = \case+ Hs.TyForall _ (Just as) cs t -> Hs.TyForall () (Just (a:as)) cs t+ Hs.TyForall _ Nothing cs t -> Hs.TyForall () (Just [a]) cs t+ t -> Hs.TyForall () (Just [a]) Nothing t+ where+ a = Hs.UnkindedVar () $ Hs.Ident () s++-- Compile a top-level type that binds the current module parameters+-- (if any) as explicitly bound type arguments.+-- The continuation is called in an extended context with these type+-- arguments bound.+compileTopLevelType :: Bool -> Type -> (Hs.Type () -> C a) -> C a+compileTopLevelType keepType t cont = do+ ctxArgs <- getContextArgs+ modTel <- lookupSection =<< currentModule+ go (modTel `apply` ctxArgs) cont+ where+ go :: Telescope -> (Hs.Type () -> C a) -> C a+ go EmptyTel cont = do+ ctxArgs <- getContextArgs+ ty <- compileType . unEl =<< t `piApplyM` ctxArgs+ cont ty+ go (ExtendTel a atel) cont+ | isInstance a = do+ c <- Hs.TypeA () <$> compileType (unEl $ unDom a)+ underAbstraction a atel $ \tel ->+ go tel (cont . constrainType c)+ | otherwise = underAbstraction a atel $ \tel -> do+ when keepType $ tellExtension Hs.ScopedTypeVariables+ go tel (cont . qualifyType (absName atel))++compileType' :: Term -> C (Strictness, Hs.Type ())+compileType' t = do+ s <- case t of+ Def f es -> fromMaybe Lazy <$> isUnboxRecord f+ _ -> return Lazy+ (s,) <$> compileType t++compileType :: Term -> C (Hs.Type ())+compileType t = do+ case t of+ Pi a b -> compileDom (absName b) a >>= \case+ DomType _ hsA -> do+ hsB <- underAbstraction a b $ compileType . unEl+ return $ Hs.TyFun () hsA hsB+ DomConstraint hsA -> do+ hsB <- underAbstraction a b (compileType . unEl)+ return $ constrainType hsA hsB+ DomDropped -> underAbstr a b (compileType . unEl)+ Def f es+ | Just semantics <- isSpecialType f -> setCurrentRange f $ semantics f es+ | Just args <- allApplyElims es ->+ ifJustM (isUnboxRecord f) (\_ -> compileUnboxType f args) $+ ifM (isTransparentFunction f) (compileTransparentType args) $ do+ vs <- compileTypeArgs args+ f <- compileQName f+ return $ tApp (Hs.TyCon () f) vs+ Var x es | Just args <- allApplyElims es -> do+ unlessM (usableModality <$> lookupBV x) $ genericDocError =<<+ text "Not supported by agda2hs: erased type variable" <+> prettyTCM (var x)+ vs <- compileTypeArgs args+ x <- hsName <$> compileVar x+ return $ tApp (Hs.TyVar () x) vs+ Sort s -> return (Hs.TyStar ())+ t -> genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t++compileTypeArgs :: Args -> C [Hs.Type ()]+compileTypeArgs args = mapM (compileType . unArg) $ filter keepArg args++compileUnboxType :: QName -> Args -> C (Hs.Type ())+compileUnboxType r pars = do+ def <- theDef <$> getConstInfo r+ case recTel def `apply` pars of+ EmptyTel -> __IMPOSSIBLE__+ (ExtendTel a _) -> compileType $ unEl $ unDom a++compileTransparentType :: Args -> C (Hs.Type ())+compileTransparentType args = compileTypeArgs args >>= \case+ [] -> genericError "Not supported: underapplied type synonyms"+ (v:vs) -> return $ v `tApp` vs++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 <$> compileType' (unEl $ unDom a)+ Hidden ->+ ifM (canErase $ unDom a)+ (return DomDropped)+ (genericDocError =<< do text "Implicit type argument not supported: " <+> prettyTCM x)+ | otherwise = return DomDropped++compileTeleBinds :: Telescope -> C [Hs.TyVarBind ()]+compileTeleBinds tel =+ forM+ (mapMaybe+ (fmap unArgDom . checkArgDom)+ (teleArgNames tel `zip` flattenTel @Type tel))+ (uncurry compileKeptTeleBind)+ where+ checkArgDom (argName, argDom) | keepArg argName = Just (argName, argDom)+ checkArgDom _ | otherwise = Nothing++ unArgDom (argName, argDom) = (hsName . unArg $ argName, unDom argDom)++compileKeptTeleBind :: Hs.Name () -> Type -> C (Hs.TyVarBind ())+compileKeptTeleBind x t = do+ checkValidTyVarName x+ case compileKind t of+ Just k -> pure $ Hs.UnkindedVar () x -- In the future we may want to show kind annotations+ _ -> genericDocError =<<+ text "Kind of bound argument not supported:"+ <+> parens (text (Hs.prettyPrint x) <> text " : " <> prettyTCM t)++compileKind :: Type -> Maybe (Hs.Kind ())+compileKind t = case unEl t of+ Sort (Type _) -> pure (Hs.TyStar ())+ Pi a b -> Hs.TyFun () <$> compileKind (unDom a) <*> compileKind (unAbs b)+ _ -> Nothing
+ src/Agda2Hs/Compile/TypeDefinition.hs view
@@ -0,0 +1,46 @@+module Agda2Hs.Compile.TypeDefinition where++import Control.Monad ( unless )++import Data.Maybe ( fromMaybe )++import qualified Language.Haskell.Exts.Syntax as Hs++import Agda.Compiler.Backend++import Agda.Syntax.Common ( namedArg )+import Agda.Syntax.Internal++import Agda.Utils.Impossible ( __IMPOSSIBLE__ )+import Agda.Utils.Monad++import Agda2Hs.Compile.Term ( compileVar )+import Agda2Hs.Compile.Type ( compileType )+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Utils+import Agda2Hs.HsUtils++compileTypeDef :: Hs.Name () -> Definition -> C [Hs.Decl ()]+compileTypeDef name (Defn {..}) = do+ unlessM (isTransparentFunction defName) $ checkValidTypeName name+ Clause{..} <- singleClause funClauses+ addContext (KeepNames clauseTel) $ do+ as <- compileTypeArgs namedClausePats+ let hd = foldl (Hs.DHApp ()) (Hs.DHead () name) as+ rhs <- compileType $ fromMaybe __IMPOSSIBLE__ clauseBody+ return [Hs.TypeDecl () hd rhs]+ where+ Function{..} = theDef+ singleClause = \case+ [cl] -> return cl+ _ -> genericError "Not supported: type definition with several clauses"++compileTypeArgs :: NAPs -> C [Hs.TyVarBind ()]+compileTypeArgs ps = mapM (compileTypeArg . namedArg) $ filter keepArg ps++compileTypeArg :: DeBruijnPattern -> C (Hs.TyVarBind ())+compileTypeArg p@(VarP o i) = do+ name <- hsName <$> compileVar (dbPatVarIndex i)+ checkValidTyVarName name+ return $ Hs.UnkindedVar () name+compileTypeArg _ = genericError "Not supported: type definition by pattern matching"
+ src/Agda2Hs/Compile/Types.hs view
@@ -0,0 +1,107 @@+{-# LANGUAGE PatternSynonyms #-}+module Agda2Hs.Compile.Types where++import Control.Monad.Reader ( ReaderT )+import Control.Monad.Writer ( WriterT )+import Control.Monad.State ( StateT )+import Control.DeepSeq ( NFData(..) )++import Data.Maybe ( fromMaybe, isJust )+import Data.Set ( Set )+import Data.Map ( Map )++import qualified Language.Haskell.Exts.SrcLoc as Hs+import qualified Language.Haskell.Exts.Syntax as Hs+import qualified Language.Haskell.Exts.Extension as Hs+import qualified Language.Haskell.Exts.Comments as Hs++import Agda.Compiler.Backend ( Definition, QName, ModuleName, TCM )+import Agda.Syntax.Position ( Range )+import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName )++import Agda2Hs.HsUtils ( Strictness )++type ModuleEnv = TopLevelModuleName+type ModuleRes = ()+type CompiledDef = [Ranged [Hs.Decl ()]]+type Ranged a = (Range, a)++type Code = (Hs.Module Hs.SrcSpanInfo, [Hs.Comment])++data Options = Options { optOutDir :: Maybe FilePath,+ optExtensions :: [Hs.Extension] }++-- Required by Agda-2.6.2, but we don't really care.+instance NFData Options where+ rnf _ = ()++data CompileEnv = CompileEnv+ { currModule :: TopLevelModuleName+ -- ^ the current module we are compiling+ , minRecordName :: Maybe ModuleName+ -- ^ keeps track of the current minimal record we are compiling+ , locals :: LocalDecls+ -- ^ keeps track of the current clause's where declarations+ , copatternsEnabled :: Bool+ -- ^ whether copatterns should be allowed when compiling patterns+ , checkVar :: Bool+ -- ^ whether to ensure compiled variables are usable and visible+ }++type Qualifier = Maybe (Maybe (Hs.ModuleName ()))+pattern Unqualified = Nothing+pattern QualifiedAs m = Just m++isQualified = isJust+qualifiedAs = fromMaybe Nothing++data CompilingCategory = ClassInstance | CaseOf | MonadicBind+ deriving Eq++data Import = Import+ { importModule :: Hs.ModuleName ()+ , importQualified :: Qualifier+ , importParent :: Maybe (Hs.Name ())+ , importName :: Hs.Name ()+ }+type Imports = [Import]++data CompileOutput = CompileOutput+ { imports :: Imports+ -- ^ Information we generate during compilation related to import statements.+ , haskellExtensions :: [Hs.KnownExtension]+ -- ^ Necessary language extensions to be automatically inserted.+ }++instance Semigroup CompileOutput where+ CompileOutput imps exts <> CompileOutput imps' exts' =+ CompileOutput (imps ++ imps') (exts ++ exts')++instance Monoid CompileOutput where+ mempty = CompileOutput [] []++-- | State used while compiling a single module.+data CompileState = CompileState+ { lcaseUsed :: Int+ -- ^ Keeps track of how many times we've used an extension.+ -- NB: can be removed by subsequent program transformations, hence the StateT.+ }++type C = StateT CompileState (ReaderT CompileEnv (WriterT CompileOutput TCM))++-- 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)+data CompiledDom+ = DomType Strictness (Hs.Type ())+ | DomConstraint (Hs.Asst ())+ | DomDropped++type LocalDecls = [QName]++data DataTarget = ToData | ToDataNewType++data RecordTarget = ToRecord [Hs.Deriving ()] | ToRecordNewType [Hs.Deriving ()] | ToClass [String]++data InstanceTarget = ToDefinition | ToDerivation (Maybe (Hs.DerivStrategy ()))
+ src/Agda2Hs/Compile/Utils.hs view
@@ -0,0 +1,271 @@+module Agda2Hs.Compile.Utils where++import Control.Arrow ( Arrow((***)) )+import Control.Monad.Except+import Control.Monad.Reader+import Control.Monad.Writer ( tell )+import Control.Monad.State ( put, modify )++import Data.Maybe ( isJust )+import qualified Data.Map as M++import qualified Language.Haskell.Exts as Hs++import Agda.Compiler.Backend hiding ( Args )++import Agda.Syntax.Common+import qualified Agda.Syntax.Concrete.Name as C+import Agda.Syntax.Internal+import Agda.Syntax.Position ( noRange )+import Agda.Syntax.Scope.Base+import Agda.Syntax.Scope.Monad ( bindVariable, freshConcreteName )++import Agda.TypeChecking.CheckInternal ( infer )+import Agda.TypeChecking.Constraints ( noConstraints )+import Agda.TypeChecking.Conversion ( equalTerm )+import Agda.TypeChecking.InstanceArguments ( findInstance )+import Agda.TypeChecking.Level ( isLevelType )+import Agda.TypeChecking.MetaVars ( newInstanceMeta )+import Agda.TypeChecking.Monad.SizedTypes ( isSizeType )+import Agda.TypeChecking.Pretty ( Doc, (<+>), text, PrettyTCM(..) )+import Agda.TypeChecking.Records ( isRecordConstructor, getRecordOfField )+import Agda.TypeChecking.Reduce ( instantiate, reduce )+import Agda.TypeChecking.Substitute ( Subst, TelV(TelV) )+import Agda.TypeChecking.Telescope ( telView )++import Agda.Utils.Lens ( (<&>) )+import Agda.Utils.Pretty ( prettyShow )+import qualified Agda.Utils.Pretty as P+import Agda.Utils.Maybe+import Agda.Utils.Monad+import Agda.Utils.Singleton++import AgdaInternals+import Agda2Hs.AgdaUtils ( (~~) )+import Agda2Hs.Compile.Types+import Agda2Hs.HsUtils+import Agda2Hs.Pragma++concatUnzip :: [([a], [b])] -> ([a], [b])+concatUnzip = (concat *** concat) . unzip++infixr 0 /\, \/+(/\), (\/) :: (a -> Bool) -> (a -> Bool) -> a -> Bool+f /\ g = \x -> f x && g x+f \/ g = \x -> f x || g x++showTCM :: PrettyTCM a => a -> C String+showTCM x = liftTCM $ show <$> prettyTCM x++setCurrentRangeQ :: QName -> C a -> C a+setCurrentRangeQ = setCurrentRange . nameBindingSite . qnameName++isInScopeUnqualified :: QName -> C Bool+isInScopeUnqualified x = lift $ do+ ys <- inverseScopeLookupName' AmbiguousAnything x <$> getScope+ return $ any (not . C.isQualified) ys++freshString :: String -> C String+freshString s = liftTCM $ do+ scope <- getScope+ ctxNames <- map (prettyShow . nameConcrete) <$> getContextNames+ return $ head $ filter (isFresh scope ctxNames) $ s : map (\i -> s ++ show i) [0..]+ where+ dummyName s = C.QName $ C.Name noRange C.NotInScope $ singleton $ C.Id s+ isFresh scope ctxNames s =+ null (scopeLookup (dummyName s) scope :: [AbstractName]) &&+ not (s `elem` ctxNames)++makeList :: C Doc -> Term -> C [Term]+makeList = makeList' "Agda.Builtin.List.List.[]" "Agda.Builtin.List.List._∷_"++makeList' :: String -> String -> C Doc -> Term -> C [Term]+makeList' nil cons err v = do+ v <- reduce v+ case v of+ Con c _ es+ | [] <- vis es, conName c ~~ nil -> return []+ | [x, xs] <- vis es, conName c ~~ cons -> (x :) <$> makeList' nil cons err xs+ _ -> genericDocError =<< err+ where+ vis es = [ unArg a | Apply a <- es, visible a ]++makeListP' :: String -> String -> C Doc -> DeBruijnPattern -> C [DeBruijnPattern]+makeListP' nil cons err p = do+ case p of+ ConP c _ ps+ | [] <- vis ps, conName c ~~ nil -> return []+ | [x, xs] <- vis ps, conName c ~~ cons -> (x :) <$> makeListP' nil cons err xs+ _ -> genericDocError =<< err+ where+ vis ps = [ namedArg p | p <- ps, visible p ]++-- When going under a binder we need to update the scope as well as the context in order to get+-- correct printing of variable names (Issue #14).+bindVar :: Int -> C ()+bindVar i = do+ x <- nameOfBV i+ liftTCM $ bindVariable LambdaBound (nameConcrete x) x++underAbstr :: Subst a => Dom Type -> Abs a -> (a -> C b) -> C b+underAbstr = underAbstraction' KeepNames++underAbstr_ :: Subst a => Abs a -> (a -> C b) -> C b+underAbstr_ = underAbstr __DUMMY_DOM__++-- Determine whether an argument should be kept or dropped.+-- We drop all arguments that have quantity 0 (= run-time erased).+-- We also drop hidden non-erased arguments (which should all be of+-- type Level or Set l).+keepArg :: (LensHiding a, LensModality a) => a -> Bool+keepArg x = usableModality x && visible x++-- Determine whether it is ok to erase arguments of this type,+-- even in the absence of an erasure annotation.+canErase :: Type -> C Bool+canErase a = do+ TelV tel b <- telView a+ addContext tel $ orM+ [ isLevelType b+ , isJust <$> isSizeType b+ , ((isJust . isSort) <$> reduce (unEl b))+ ]++-- Exploits the fact that the name of the record type and the name of the record module are the+-- same, including the unique name ids.+isClassFunction :: QName -> C Bool+isClassFunction = isClassModule . qnameModule++isClassModule :: ModuleName -> C Bool+isClassModule m+ | null $ mnameToList m = return False+ | otherwise = do+ minRec <- asks minRecordName+ getConstInfo' (mnameToQName m) >>= \case+ _ | Just m == minRec -> return True+ Right Defn{defName = r, theDef = Record{}} ->+ -- It would be nicer if we remembered this from when we looked at the record the first time.+ processPragma r <&> \case+ ClassPragma _ -> True+ ExistingClassPragma -> True+ _ -> False+ _ -> return False++-- Drops the last (record) module for typeclass methods+dropClassModule :: ModuleName -> C ModuleName+dropClassModule m@(MName ns) = isClassModule m >>= \case+ True -> dropClassModule $ MName $ init ns+ False -> return m++isUnboxRecord :: QName -> C (Maybe Strictness)+isUnboxRecord q = do+ getConstInfo q >>= \case+ Defn{defName = r, theDef = Record{}} ->+ processPragma r <&> \case+ UnboxPragma s -> Just s+ _ -> Nothing+ _ -> return Nothing++isUnboxConstructor :: QName -> C (Maybe Strictness)+isUnboxConstructor q =+ caseMaybeM (isRecordConstructor q) (return Nothing) $ isUnboxRecord . fst++isUnboxProjection :: QName -> C (Maybe Strictness)+isUnboxProjection q =+ caseMaybeM (liftTCM $ getRecordOfField q) (return Nothing) isUnboxRecord++isTransparentFunction :: QName -> C Bool+isTransparentFunction q = do+ getConstInfo q >>= \case+ Defn{defName = r, theDef = Function{}} ->+ processPragma r <&> \case+ TransparentPragma -> True+ _ -> False+ _ -> return False++checkInstance :: Term -> C ()+checkInstance u | varOrDef u = liftTCM $ noConstraints $ do+ reportSDoc "agda2hs.checkInstance" 5 $ text "checkInstance" <+> prettyTCM u+ t <- infer u+ reportSDoc "agda2hs.checkInstance" 15 $ text " inferred type:" <+> prettyTCM t+ (m, v) <- newInstanceMeta "" t+ reportSDoc "agda2hs.checkInstance" 15 $ text " instance meta:" <+> prettyTCM m+ findInstance m Nothing+ reportSDoc "agda2hs.checkInstance" 15 $ text " inferred instance:" <+> (prettyTCM =<< instantiate v)+ reportSDoc "agda2hs.checkInstance" 65 $ text " inferred instance:" <+> (pure . P.pretty =<< instantiate v)+ reportSDoc "agda2hs.checkInstance" 65 $ text " checking instance:" <+> (pure . P.pretty =<< instantiate u)+ equalTerm t u v `catchError` \_ ->+ genericDocError =<< text "illegal instance: " <+> prettyTCM u+ where+ varOrDef Var{} = True+ varOrDef Def{} = True+ varOrDef _ = False+-- We need to compile applications of `fromNat`, `fromNeg`, and+-- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally+-- this constraint would be marked as erased but this would involve+-- changing Agda builtins.+checkInstance u@(Con c _ _)+ | prettyShow (conName c) == "Agda.Builtin.Unit.tt" ||+ prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" ||+ prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" = return ()+checkInstance u = genericDocError =<< text "illegal instance: " <+> prettyTCM u++modifyLCase :: (Int -> Int) -> CompileState -> CompileState+modifyLCase f (CompileState {lcaseUsed = n}) = CompileState {lcaseUsed = f n}++incrementLCase, decrementLCase :: C ()+incrementLCase = modify $ modifyLCase (+ 1)+decrementLCase = modify $ modifyLCase (\n -> n - 1)++-- Always construct lambda cases with this function.+hsLCase :: [Hs.Alt ()] -> C (Hs.Exp ())+hsLCase = (incrementLCase >>) . return . Hs.LCase ()++ensureNoLocals :: String -> C ()+ensureNoLocals msg = unlessM (null <$> asks locals) $ genericError msg++withLocals :: LocalDecls -> C a -> C a+withLocals ls = local $ \e -> e { locals = ls }++checkValidVarName :: Hs.Name () -> C ()+checkValidVarName x = unless (validVarName x) $ genericDocError =<< do+ text "Invalid name for Haskell variable: " <+> text (Hs.prettyPrint x)++checkValidTyVarName :: Hs.Name () -> C ()+checkValidTyVarName x = unless (validVarName x) $ genericDocError =<< do+ text "Invalid name for Haskell type variable: " <+> text (Hs.prettyPrint x)++checkValidFunName :: Hs.Name () -> C ()+checkValidFunName x = unless (validVarName x) $ genericDocError =<< do+ text "Invalid name for Haskell function: " <+> text (Hs.prettyPrint x)++checkValidTypeName :: Hs.Name () -> C ()+checkValidTypeName x = unless (validConName x) $ genericDocError =<< do+ text "Invalid name for Haskell type: " <+> text (Hs.prettyPrint x)++checkValidConName :: Hs.Name () -> C ()+checkValidConName x = unless (validConName x) $ genericDocError =<< do+ text "Invalid name for Haskell constructor: " <+> text (Hs.prettyPrint x)++tellImport :: Import -> C ()+tellImport imp = tell $ CompileOutput [imp] []++tellExtension :: Hs.KnownExtension -> C ()+tellExtension pr = tell $ CompileOutput [] [pr]++addPatBang :: Strictness -> Hs.Pat () -> C (Hs.Pat ())+addPatBang Strict p = tellExtension Hs.BangPatterns >>+ return (Hs.PBangPat () p)+addPatBang Lazy p = return p++addTyBang :: Strictness -> Hs.Type () -> C (Hs.Type ())+addTyBang Strict ty = tellExtension Hs.BangPatterns >>+ return (Hs.TyBang () (Hs.BangedTy ()) (Hs.NoUnpackPragma ()) ty)+addTyBang Lazy ty = return ty++checkSingleElement :: Hs.Name () -> [b] -> String -> C ()+checkSingleElement name fs s = unless (length fs == 1) $ genericDocError =<< do+ text (s ++ ":") <+> text (Hs.prettyPrint name)++checkingVars :: C a -> C a+checkingVars = local $ \e -> e { checkVar = True }
+ src/Agda2Hs/HsUtils.hs view
@@ -0,0 +1,266 @@++module Agda2Hs.HsUtils where++import Control.Monad ( guard )++import Data.Data ( Data )+import Data.Generics ( listify, everywhere, mkT, extT )+import Data.List ( foldl' )+import Data.Map ( Map )++import qualified Data.Map as Map++import Language.Haskell.Exts hiding ( Strict, Lazy )++import Agda.Syntax.Position++import Agda.Utils.FileName ( mkAbsolute )+import Agda.Utils.List ( initLast )+import Agda.Utils.Maybe.Strict ( toStrict )++-- Names ------------------------------------------------------------------+++validVarId :: String -> Bool+validVarId s = case lexTokenStream s of+ ParseOk [Loc _ VarId{}] -> True+ _ -> False++validConId :: String -> Bool+validConId s = case lexTokenStream s of+ ParseOk [Loc _ ConId{}] -> True+ _ -> False++validVarSym :: String -> Bool+validVarSym s = case lexTokenStream s of+ ParseOk [Loc _ VarSym{}] -> True+ _ -> False++validConSym :: String -> Bool+validConSym s = case lexTokenStream s of+ ParseOk [Loc _ ConSym{}] -> True+ _ -> False++validVarName :: Name () -> Bool+validVarName (Ident _ s) = validVarId s+validVarName (Symbol _ s) = validVarSym s++validConName :: Name () -> Bool+validConName (Ident _ s) = validConId s+validConName (Symbol _ s) = validConSym s++isInfix :: String -> Maybe String+isInfix ('_' : f) = do+ (op, '_') <- initLast f+ guard $ not $ '_' `elem` op+ return op+isInfix _ = Nothing++hsName :: String -> Name ()+hsName x+ | Just op <- isInfix x = Symbol () op+ | otherwise = Ident () (map underscore x)+ where+ -- Agda uses underscores for operators, which means that you can't have both mapM and mapM_+ -- without getting ambiguities. To work around this we translate subscript '-' to underscore.+ underscore '₋' = '_'+ underscore c = c++extToName :: KnownExtension -> Name ()+extToName = Ident () . show++hsModuleName :: String -> ModuleName ()+hsModuleName = ModuleName ()++isOp :: QName () -> Bool+isOp (UnQual _ Symbol{}) = True+isOp (Special _ Cons{}) = True+isOp _ = False++isSpecial :: QName () -> Bool+isSpecial (Special _ _) = True+isSpecial _ = False++unQual :: QName () -> Name ()+unQual (UnQual _ n) = n+unQual (Qual _ _ n) = n+unQual (Special _ _) = error "Unexpected special con"++definedName :: Match l -> Name l+definedName (Match _ f _ _ _) = f+definedName (InfixMatch _ _ f _ _ _) = f++replaceName :: Data a => Name () -> Name () -> a -> a+replaceName pre post = everywhere (mkT go `extT` go')+ where+ go :: QName () -> QName ()+ go n | isSpecial n = n+ | unQual n == pre = UnQual () post+ | otherwise = n++ go' :: Match () -> Match ()+ go' m = case m of+ (Match () n ps rhs bs) -> Match () (f n) ps rhs bs+ (InfixMatch () p n ps rhs bs) -> InfixMatch () p (f n) ps rhs bs+ where f n | n == pre = post+ | otherwise = n++dropPatterns :: Data a => Int -> a -> a+dropPatterns n = everywhere (mkT go)+ where+ go :: Match () -> Match ()+ go (Match () f ps rhs bs) = Match () f (drop n ps) rhs bs+ go m = m+++-- Utilities for building Haskell constructs++pp :: Pretty a => a -> String+pp = prettyPrintWithMode defaultMode{ spacing = False+ , classIndent = 4+ , whereIndent = 2+ }+++-- exactPrint really looks at the line numbers (and we're using the locations from the agda source+-- to report Haskell parse errors at the right location), so shift everything to start at line 1.+moveToTop :: Annotated ast => (ast SrcSpanInfo, [Comment]) -> (ast SrcSpanInfo, [Comment])+moveToTop (x, cs) = (subtractLine l <$> x, [ Comment b (sub l r) str | Comment b r str <- cs ])+ where l = startLine (ann x) - 1+ subtractLine :: Int -> SrcSpanInfo -> SrcSpanInfo+ subtractLine l (SrcSpanInfo s ss) = SrcSpanInfo (sub l s) (map (sub l) ss)++ sub :: Int -> SrcSpan -> SrcSpan+ sub l (SrcSpan f l0 c0 l1 c1) = SrcSpan f (l0 - l) c0 (l1 - l) c1++getList :: Exp () -> Maybe [Exp ()]+getList (Con _ (Special _ ListCon{})) = Just []+getList (List _ es) = Just es+getList _ = Nothing++getListP :: Pat () -> Maybe [Pat ()]+getListP (PApp _ (Special _ ListCon{}) []) = Just []+getListP (PList _ es) = Just es+getListP _ = Nothing++pApp :: QName () -> [Pat ()] -> Pat ()+pApp c@(UnQual () (Symbol () _)) [p, q] = PInfixApp () p c q+pApp (Special _ Cons{}) [p, q] | Just ps <- getListP q = PList () (p : ps)+pApp c@(Special () Cons{}) [p, q] = PInfixApp () p c q+pApp c ps = PApp () c ps++getOp :: Exp () -> Maybe (QOp ())+getOp (Var _ x) | isOp x = Just $ QVarOp () x+getOp (Con _ c) | isOp c = Just $ QConOp () c+getOp _ = Nothing++eApp :: Exp () -> [Exp ()] -> Exp ()+eApp f [a, b] | Just (QConOp () (Special _ Cons{})) <- getOp f,+ Just as <- getList b = List () (a : as)+eApp f (a : b : as) | Just op <- getOp f = foldl (App ()) (InfixApp () a op b) as+eApp f [a] | Just op <- getOp f = LeftSection () a op+eApp f es = foldl (App ()) f es++tApp :: Type () -> [Type ()] -> Type ()+tApp (TyCon () (Special () ListCon{})) [a] = TyList () a+tApp t vs = foldl (TyApp ()) t vs++hsLambda :: String -> Exp () -> Exp ()+hsLambda x e =+ case e of+ Lambda l ps b -> Lambda l (p : ps) b+ _ -> Lambda () [p] e+ where+ p = PVar () $ hsName x++hsUnqualName :: String -> QName ()+hsUnqualName = UnQual () . hsName++hsVar :: String -> Exp ()+hsVar = Var () . hsUnqualName++hsUndefined :: Exp ()+hsUndefined = hsVar "undefined"++hsError :: String -> Exp ()+hsError s = hsVar "error" `eApp` [strE s]++cname :: CName l -> Name l+cname (VarName _ n) = n+cname (ConName _ n) = n++cloc :: CName l -> l+cloc (VarName l _) = l+cloc (ConName l _) = l++srcSpanToRange :: SrcSpan -> Range+srcSpanToRange (SrcSpan file l1 c1 l2 c2) =+ intervalToRange (toStrict $ Just $ mkRangeFile (mkAbsolute file) Nothing) $ Interval (pos l1 c1) (pos l2 c2)+ where pos l c = Pn () 0 (fromIntegral l) (fromIntegral c)++srcLocToRange :: SrcLoc -> Range+srcLocToRange (SrcLoc file l c) = srcSpanToRange (SrcSpan file l c l c)++srcSpanInfoToRange :: SrcSpanInfo -> Range+srcSpanInfoToRange = srcSpanToRange . srcInfoSpan++allUsedTypes :: Data a => a -> [Type ()]+allUsedTypes = listify (const True)++usedTypesOf :: Data a => String -> a -> [Type ()]+usedTypesOf s = listify $ (== s) . pp++uses :: Data a => String -> a -> Bool+uses ty = not . null . usedTypesOf ty++-- Fixities++insertParens :: Data a => a -> a+insertParens = everywhere (mkT $ insertPars $ fixityMap baseFixities)+ where+ fixityMap fxs = Map.fromList [ (q, fx) | fx@(Fixity _ _ q) <- fxs ]++insertPars :: Map (QName ()) Fixity -> Exp () -> Exp ()+insertPars fixs (InfixApp l e1 op e2) = InfixApp l (parL e1) op (parR e2)+ where+ getFix op = Map.lookup (qopName op) fixs+ topFix = getFix op++ qopName (QVarOp _ x) = x+ qopName (QConOp _ x) = x++ needParen same (Just (Fixity atop top _)) (Just (Fixity achild child _))+ | top > child = True+ | top < child = False+ | atop /= achild = True+ | otherwise = same atop+ needParen _ Nothing _ = True -- If we don't know, add parens+ needParen _ _ Nothing = True++ parL = par $ needParen (AssocLeft () /=)+ parR = par $ needParen (AssocRight () /=)++ par need e@(InfixApp _ _ op _)+ | need topFix (getFix op) = Paren () e+ par _ e = e+insertPars _ e = e++-- Patterns+patToExp :: Pat l -> Maybe (Exp l)+patToExp = \case+ PVar l x -> Just $ Var l (UnQual l x)+ PLit l s v -> Just $ Lit l v+ PInfixApp l p f q -> InfixApp l <$> patToExp p <*> pure (QConOp l f) <*> patToExp q+ PApp l x ps -> foldl' (App l) (Con l x) <$> traverse patToExp ps+ PTuple l b ps -> Tuple l b <$> traverse patToExp ps+ PUnboxedSum l i j p -> UnboxedSum l i j <$> patToExp p+ PList l ps -> List l <$> traverse patToExp ps+ PParen l p -> Paren l <$> patToExp p+ PAsPat _ _ p -> patToExp p+ PIrrPat _ p -> patToExp p+ PatTypeSig _ p _ -> patToExp p+ PBangPat _ p -> patToExp p+ _ -> Nothing++data Strictness = Lazy | Strict+ deriving Show
+ src/Agda2Hs/Pragma.hs view
@@ -0,0 +1,97 @@+module Agda2Hs.Pragma where++import Data.List ( isPrefixOf )+import Data.Maybe ( fromMaybe )+import qualified Data.Map as Map++import qualified Language.Haskell.Exts.Syntax as Hs+import qualified Language.Haskell.Exts.Parser as Hs+import qualified Language.Haskell.Exts.Extension as Hs++import Agda.Compiler.Backend+import Agda.Compiler.Common ( curIF )++import Agda.Syntax.Position++import Agda.Utils.FileName ( filePath )+import Agda.Utils.Maybe.Strict ( toLazy )++import Agda2Hs.HsUtils+import Agda2Hs.Compile.Types++pragmaName :: String+pragmaName = "AGDA2HS"++languagePragmas :: Code -> [Hs.Extension]+languagePragmas (Hs.Module _ _ ps _ _, _) =+ [ Hs.parseExtension s | Hs.LanguagePragma _ ss <- ps, Hs.Ident _ s <- ss ]+languagePragmas _ = []++getForeignPragmas :: [Hs.Extension] -> TCM [(Range, Code)]+getForeignPragmas exts = do+ pragmas <- fromMaybe [] . Map.lookup pragmaName . iForeignCode <$> curIF+ getCode exts $ reverse pragmas+ where+ getCode :: [Hs.Extension] -> [ForeignCode] -> TCM [(Range, Code)]+ getCode _ [] = return []+ getCode exts (ForeignCode r code : pragmas) = do+ let Just file = fmap (filePath . rangeFilePath) $ toLazy $ rangeFile r+ pmode = Hs.defaultParseMode { Hs.parseFilename = file,+ Hs.ignoreLinePragmas = False,+ Hs.extensions = exts }+ line = case posLine <$> rStart r of+ Just l -> "{-# LINE " ++ show l ++ show file ++ " #-}\n"+ Nothing -> ""+ case Hs.parseWithComments pmode (line ++ code) of+ Hs.ParseFailed loc msg -> setCurrentRange (srcLocToRange loc) $ genericError msg+ Hs.ParseOk m -> ((r, m) :) <$> getCode (exts ++ languagePragmas m) pragmas++data ParsedPragma+ = NoPragma+ | DefaultPragma [Hs.Deriving ()]+ | ClassPragma [String]+ | ExistingClassPragma+ | UnboxPragma Strictness+ | TransparentPragma+ | NewTypePragma [Hs.Deriving ()]+ | DerivePragma (Maybe (Hs.DerivStrategy ()))+ deriving Show++derivePragma :: String+derivePragma = "derive"++parseStrategy :: String -> Maybe (Hs.DerivStrategy ())+parseStrategy "stock" = Just (Hs.DerivStock ())+parseStrategy "newtype" = Just (Hs.DerivNewtype ())+parseStrategy "anyclass" = Just (Hs.DerivAnyclass ())+parseStrategy _ = Nothing++newtypePragma :: String+newtypePragma = "newtype"++processDeriving :: String -> ([Hs.Deriving ()] -> ParsedPragma) -> C ParsedPragma+processDeriving d pragma =+ -- parse a deriving clause for a datatype by tacking it onto a+ -- dummy datatype and then only keeping the deriving part+ case Hs.parseDecl ("data X = X " ++ d) of+ Hs.ParseFailed loc msg ->+ setCurrentRange (srcLocToRange loc) $ genericError msg+ Hs.ParseOk (Hs.DataDecl _ _ _ _ _ ds) ->+ return $ pragma (map (() <$) ds)+ Hs.ParseOk _ -> return $ pragma []++processPragma :: QName -> C ParsedPragma+processPragma qn = liftTCM (getUniqueCompilerPragma pragmaName qn) >>= \case+ Nothing -> return NoPragma+ Just (CompilerPragma _ s)+ | "class" `isPrefixOf` s -> return $ ClassPragma (words $ drop 5 s)+ | s == "existing-class" -> return ExistingClassPragma+ | s == "unboxed" -> return $ UnboxPragma Lazy+ | s == "unboxed-strict" -> return $ UnboxPragma Strict+ | s == "transparent" -> return TransparentPragma+ | s == newtypePragma -> return $ NewTypePragma []+ | s == derivePragma -> return $ DerivePragma Nothing+ | derivePragma `isPrefixOf` s -> return $ DerivePragma (parseStrategy (drop (length derivePragma + 1) s))+ | "deriving" `isPrefixOf` s -> processDeriving s DefaultPragma+ | (newtypePragma ++ " deriving") `isPrefixOf` s -> processDeriving (drop (length newtypePragma + 1) s) NewTypePragma+ _ -> return $ DefaultPragma []
+ src/Agda2Hs/Render.hs view
@@ -0,0 +1,107 @@+module Agda2Hs.Render where++import Control.Monad ( unless )+import Control.Monad.Except ( MonadIO(liftIO) )++import Data.Function ( on )+import Data.List ( sortBy, nub )+import Data.Maybe ( fromMaybe )+import Data.Set ( Set )+import qualified Data.Set as Set++import System.FilePath ( takeDirectory, (</>) )+import System.Directory ( createDirectoryIfMissing )++import qualified Language.Haskell.Exts.SrcLoc as Hs+import qualified Language.Haskell.Exts.Syntax as Hs+import qualified Language.Haskell.Exts.Build as Hs+import qualified Language.Haskell.Exts.ExactPrint as Hs+import qualified Language.Haskell.Exts.Extension as Hs++import Agda.Compiler.Backend+import Agda.Compiler.Common ( curIF, compileDir )++import Agda.TypeChecking.Pretty+import qualified Agda.Syntax.Concrete.Name as C+import Agda.Syntax.Position+import Agda.Syntax.TopLevelModuleName++import Agda.Utils.Pretty ( prettyShow )+import Agda2Hs.Compile+import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Imports+import Agda2Hs.HsUtils+import Agda2Hs.Pragma ( getForeignPragmas )++-- Rendering --------------------------------------------------------------++type Block = Ranged [String]++sortRanges :: [Ranged a] -> [a]+sortRanges = map snd . sortBy (compare `on` rLine . fst)++rLine :: Range -> Int+rLine r = fromIntegral $ fromMaybe 0 $ posLine <$> rStart r++renderBlocks :: [Block] -> String+renderBlocks = unlines . map unlines . sortRanges . filter (not . null . snd)++defBlock :: [Ranged [Hs.Decl ()]] -> [Block]+defBlock def = [ (r, map (pp . insertParens) ds) | (r, ds) <- def ]++renderLangExts :: [Hs.KnownExtension] -> String+renderLangExts exts+ | null exts = ""+ | otherwise = pp (Hs.LanguagePragma () $ nub $ map extToName exts) ++ "\n"++codePragmas :: [Ranged Code] -> [Block]+codePragmas code = [ (r, map pp ps) | (r, (Hs.Module _ _ ps _ _, _)) <- code ]++codeBlocks :: [Ranged Code] -> [Block]+codeBlocks code = [(r, [uncurry Hs.exactPrint $ moveToTop $ noPragmas mcs]) | (r, mcs) <- code, nonempty mcs]+ where noPragmas (Hs.Module l h _ is ds, cs) = (Hs.Module l h [] is ds, cs)+ noPragmas m = m+ nonempty (Hs.Module _ _ _ is ds, cs) = not $ null is && null ds && null cs+ nonempty _ = True++-- Generating the files -------------------------------------------------------++moduleFileName :: Options -> TopLevelModuleName -> TCM FilePath+moduleFileName opts name = do+ outDir <- compileDir+ return $ fromMaybe outDir (optOutDir opts) </> moduleNameToFileName name "hs"++moduleSetup :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath -> TCM (Recompile ModuleEnv ModuleRes)+moduleSetup _ _ m _ = do+ reportSDoc "agda2hs.compile" 3 $ text "Compiling module: " <+> prettyTCM m+ setScope . iInsideScope =<< curIF+ return $ Recompile m++ensureDirectory :: FilePath -> IO ()+ensureDirectory = createDirectoryIfMissing True . takeDirectory++writeModule :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName+ -> [(CompiledDef, CompileOutput)] -> TCM ModuleRes+writeModule opts _ isMain m outs = do+ code <- getForeignPragmas (optExtensions opts)+ let mod = prettyShow m+ (cdefs, impss, extss) = unzip3 $ flip map outs $+ \(cdef, CompileOutput imps exts) -> (cdef, imps, exts)+ defs = concatMap defBlock cdefs ++ codeBlocks code+ imps = concat impss+ exts = concat extss+ unless (null code && null defs && isMain == NotMain) $ do+ -- Add automatic imports+ let unlines' [] = []+ unlines' ss = unlines ss ++ "\n"+ autoImports <- unlines' . map pp <$> compileImports mod imps+ -- The comments makes it hard to generate and pretty print a full module+ hsFile <- moduleFileName opts m+ let output = concat+ [ renderLangExts exts+ , renderBlocks $ codePragmas code+ , "module " ++ mod ++ " where\n\n"+ , autoImports+ , renderBlocks defs ]+ reportSLn "" 1 $ "Writing " ++ hsFile+ liftIO $ ensureDirectory hsFile >> writeFile hsFile output
+ src/AgdaInternals.hs view
@@ -0,0 +1,53 @@+-- TODO: merge upstream, useful for other backends+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+module AgdaInternals where++import Control.Monad.Writer+import Control.Monad.State++import Data.String++import Agda.Syntax.Internal+import Agda.TypeChecking.Monad+import Agda.TypeChecking.Substitute+import Agda.Utils.Size++instance Subst Clause where+ type SubstArg Clause = DeBruijnPattern+ applySubst rhoP c@Clause{..} = c+ { clauseTel = applyPatSubst rhoP clauseTel+ , namedClausePats = applySubst rhoP' namedClausePats+ , clauseBody = applyPatSubst rhoP' clauseBody+ , clauseType = applyPatSubst rhoP' clauseType+ } where rhoP' = liftS (size clauseTel) rhoP++instance Subst Defn where+ type SubstArg Defn = DeBruijnPattern+ applySubst rhoP = \case+ f@Function{..} ->+ f { funClauses = applySubst rhoP <$> funClauses+ , funCovering = applySubst rhoP <$> funCovering }+ (PrimitiveSort q s) -> PrimitiveSort q (applyPatSubst rhoP s)+ d -> d++instance Subst Definition where+ type SubstArg Definition = DeBruijnPattern+ applySubst rhoP d@Defn{..} =+ d {defType = applyPatSubst rhoP defType, theDef = applySubst rhoP theDef}++instance (Monoid r, MonadFresh i m) => MonadFresh i (WriterT r m)+instance (Monoid r, MonadInteractionPoints m) => MonadInteractionPoints (WriterT r m)+instance (Monoid r, MonadStConcreteNames m) => MonadStConcreteNames (WriterT r m) where+ --runStConcreteNames :: StateT ConcreteNames (WriterT r m) a -> WriterT r m a+ runStConcreteNames m = WriterT $ runStConcreteNames $ StateT $ \s -> do+ ((x,s'),ns) <- runWriterT $ runStateT m s+ return ((x,ns),s')+instance (Monoid r, Monad m, IsString (m a)) => IsString (WriterT r m a) where+ fromString s = WriterT $ fmap (,mempty) $ fromString s+instance (Monoid r, MonadBlock m) => MonadBlock (WriterT r m) where+ catchPatternErr h m = WriterT $ catchPatternErr (runWriterT . h) (runWriterT m)+instance MonadBlock m => MonadBlock (StateT s m) where+ catchPatternErr h m = StateT $ \s -> catchPatternErr (flip runStateT s . h) (runStateT m s)
+ src/Main.hs view
@@ -0,0 +1,47 @@+module Main where++import System.Console.GetOpt++import qualified Language.Haskell.Exts.Syntax as Hs+import qualified Language.Haskell.Exts.Build as Hs+import qualified Language.Haskell.Exts.Parser as Hs+import qualified Language.Haskell.Exts.Extension as Hs++import Agda.Main+import Agda.Compiler.Backend++import Agda2Hs.Compile+import Agda2Hs.Compile.Types+import Agda2Hs.Render++defaultOptions :: Options+defaultOptions = Options{ optOutDir = Nothing, optExtensions = [] }++outdirOpt :: Monad m => FilePath -> Options -> m Options+outdirOpt dir opts = return opts{ optOutDir = Just dir }++extensionOpt :: Monad m => String -> Options -> m Options+extensionOpt ext opts = return opts{ optExtensions = Hs.parseExtension ext : optExtensions opts }++backend :: Backend' Options Options ModuleEnv ModuleRes (CompiledDef, CompileOutput)+backend = Backend'+ { backendName = "agda2hs"+ , backendVersion = Just "1.0"+ , options = defaultOptions+ , commandLineFlags =+ [ Option ['o'] ["out-dir"] (ReqArg outdirOpt "DIR")+ "Write Haskell code to DIR. (default: project root)"+ , Option ['X'] [] (ReqArg extensionOpt "EXTENSION")+ "Enable Haskell language EXTENSION. Affects parsing of Haskell code in FOREIGN blocks."+ ]+ , isEnabled = \ _ -> True+ , preCompile = return+ , postCompile = \ _ _ _ -> return ()+ , preModule = moduleSetup+ , postModule = writeModule+ , compileDef = compile+ , scopeCheckingSuffices = False+ , mayEraseType = \ _ -> return True+ }++main = runAgda [Backend backend]