agda2hs 1.1 → 1.2

raw patch · 27 files changed

+491/−5534 lines, 27 filesdep +aesondep +yamldep −processdep −yaml-lightdep ~basedep ~bytestringdep ~containers

Dependencies added: aeson, yaml

Dependencies removed: process, yaml-light

Dependency ranges changed: base, bytestring, containers, deepseq, mtl, text

Files

• CHANGELOG.md +13/−8
• agda2hs.cabal +19/−45
• src/Agda2Hs/AgdaUtils.hs +25/−6
• src/Agda2Hs/Compile.hs +43/−43
• src/Agda2Hs/Compile/Data.hs +1/−1
• src/Agda2Hs/Compile/Function.hs +39/−17
• src/Agda2Hs/Compile/Imports.hs +24/−11
• src/Agda2Hs/Compile/Name.hs +46/−51
• src/Agda2Hs/Compile/Record.hs +11/−6
• src/Agda2Hs/Compile/Rewrites.hs +0/−107
• src/Agda2Hs/Compile/Term.hs +36/−31
• src/Agda2Hs/Compile/Type.hs +75/−54
• src/Agda2Hs/Compile/Types.hs +27/−23
• src/Agda2Hs/Compile/Utils.hs +5/−1
• src/Agda2Hs/Config.hs +70/−0
• src/Agda2Hs/Render.hs +31/−18
• src/Main.hs +26/−28
• src/agda2hs-mode/Main.hs +0/−298
• src/data/emacs-mode/agda-input.el +0/−1445
• src/data/emacs-mode/agda2-abbrevs.el +0/−106
• src/data/emacs-mode/agda2-highlight.el +0/−596
• src/data/emacs-mode/agda2-mode-pkg.el +0/−3
• src/data/emacs-mode/agda2-mode.el +0/−2063
• src/data/emacs-mode/agda2-queue.el +0/−44
• src/data/emacs-mode/agda2.el +0/−16
• src/data/emacs-mode/annotation.el +0/−301
• src/data/emacs-mode/eri.el +0/−212

@@ -1,17 +1,22 @@-Release notes for agda2hs v1.1+Release notes for agda2hs v1.2 ==============================  Changes ------- -- Updated Agda base version to 2.6.4.-- The `agda2hs` executable can now also be used in interactive mode (e.g. in Emacs or VS Code).-- Added option to specify user-defined rewrites (see https://agda.github.io/agda2hs/features.html#rewrite-rules).-- Type operators with names not starting with a colon are now allowed.-- Added bindings for the `IO` monad.-- Various other additions to the `Haskell.Prelude` library.+- Increased bounds to support GHC 9.6.3+- Changed flag `--rewrite-rules` to `--config`.+- Deprecated `Tuple` (#228). Now there are distinct 2-uples (`_×_`) and 3-uples (`_×_×_`).+  Only 2-uples can be pattern-matched inside of let bindings.+- Experimental support for *erased module parameters* (#229).+- Support for erased hidden type parameters.+- Functions with no clause throw a hard error when getting compiled.+- Unboxed records can preserve any field -- not only the first one.+- Improved documentation. +See https://github.com/agda/agda2hs/issues?q=milestone%3A1.2+is%3Apr for the full list of changes.+ Fixed issues ------------ -See https://github.com/agda/agda2hs/issues?q=milestone%3A1.1+is%3Aissue for the full list of fixed issues.+See https://github.com/agda/agda2hs/issues?q=milestone%3A1.2+is%3Aissue for the full list of fixed issues.

@@ -1,6 +1,6 @@ cabal-version:       2.2 name:                agda2hs-version:             1.1+version:             1.2 license:             BSD-3-Clause license-file:        LICENSE author:              Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette@@ -15,8 +15,6 @@   The tool is implemented as an Agda backend, which means that `agda2hs` is a   fully functional Agda compiler. -data-dir:           src/data-data-files:         emacs-mode/*.el extra-doc-files:    CHANGELOG.md                     README.md @@ -36,60 +34,36 @@                        Agda2Hs.Compile.Name,                        Agda2Hs.Compile.Postulate,                        Agda2Hs.Compile.Record,-                       Agda2Hs.Compile.Rewrites,                        Agda2Hs.Compile.Term,                        Agda2Hs.Compile.Type,                        Agda2Hs.Compile.TypeDefinition,                        Agda2Hs.Compile.Types,                        Agda2Hs.Compile.Utils,+                       Agda2Hs.Config,                        Agda2Hs.HsUtils,-                       Agda2Hs.Pragma-                       Agda2Hs.Render-                       AgdaInternals-  build-depends:       base >= 4.10 && < 4.18,-                       Agda >= 2.6.4 && < 2.6.5,-                       bytestring >= 0.11.5 && < 0.12,-                       containers >= 0.6 && < 0.7,-                       unordered-containers >= 0.2.19 && < 0.3,-                       mtl >= 2.2.2 && < 2.3,-                       directory >= 1.2.6.2 && < 1.4,-                       filepath >= 1.4.1.0 && < 1.5,-                       haskell-src-exts >= 1.23 && < 1.25,-                       syb >= 0.7.2 && < 0.8,-                       text >= 2.0.2 && < 2.1,-                       deepseq >= 1.4.4 && < 1.5,-                       yaml-light >= 0.1.4 && < 2.0-  default-language:    Haskell2010-  default-extensions:  LambdaCase,-                       RecordWildCards,-                       FlexibleContexts,-                       MultiWayIf,-                       TupleSections,-                       ScopedTypeVariables--executable agda2hs-mode-  hs-source-dirs:      src/agda2hs-mode-  main-is:             Main.hs-  other-modules:       Paths_agda2hs+                       Agda2Hs.Pragma,+                       Agda2Hs.Render,+                       AgdaInternals,+                       Paths_agda2hs   autogen-modules:     Paths_agda2hs-  build-depends:       base >= 4.10 && < 4.18,+  build-depends:       base >= 4.10 && < 4.20,                        Agda >= 2.6.4 && < 2.6.5,-                       bytestring >= 0.11.5 && < 0.12,-                       containers >= 0.6 && < 0.7,+                       bytestring >= 0.11.5 && < 0.13,+                       containers >= 0.6 && < 0.8,                        unordered-containers >= 0.2.19 && < 0.3,-                       mtl >= 2.2.2 && < 2.3,+                       mtl >= 2.2.2 && < 2.4,                        directory >= 1.2.6.2 && < 1.4,                        filepath >= 1.4.1.0 && < 1.5,                        haskell-src-exts >= 1.23 && < 1.25,                        syb >= 0.7.2 && < 0.8,-                       text >= 2.0.2 && < 2.1,-                       deepseq >= 1.4.4 && < 1.5,-                       yaml-light >= 0.1.4 && < 2.0,-                       process   >= 1.6.3.0  && < 1.7+                       text >= 2.0.2 && < 2.2,+                       deepseq >= 1.4.4 && < 1.6,+                       yaml >= 0.11 && < 0.12,+                       aeson >= 2.2 && < 2.3,   default-language:    Haskell2010-  default-extensions:  LambdaCase,-                       RecordWildCards,-                       FlexibleContexts,-                       MultiWayIf,-                       TupleSections,+  default-extensions:  LambdaCase+                       RecordWildCards+                       FlexibleContexts+                       MultiWayIf+                       TupleSections                        ScopedTypeVariables

@@ -21,6 +21,7 @@ import Agda.TypeChecking.Monad ( topLevelModuleName ) import Agda.TypeChecking.Pretty import Agda.TypeChecking.Substitute+import Agda.TypeChecking.Reduce ( reduceDefCopy )  import Agda.Utils.Either ( isRight ) import Agda.Utils.List ( initMaybe )@@ -70,11 +71,12 @@         e        : es' -> loop h (e : res) es'       where v = h $ reverse res +-- | Map over the body of all clauses of a function definition. 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+    mapDefn defn = defn      mapClause c = c{ clauseBody = f <$> clauseBody c } @@ -86,18 +88,35 @@   tlm <- topLevelModuleNameForModuleName m   ifM (isRight <$> findFile' tlm) (return $ Just tlm) (return Nothing) -getTopLevelModuleForModuleName :: ModuleName -> TCM (Maybe TopLevelModuleName)+-- | Get the toplevel module parent to a given module.+getTopLevelModuleForModuleName :: ModuleName -> TCM TopLevelModuleName getTopLevelModuleForModuleName = loop . mnameToList   where     loop ns-      | null ns   = return Nothing+      | null ns   = __IMPOSSIBLE__       | otherwise = isTopLevelModule (MName ns) >>= \case-        Nothing      -> loop (init ns)-        tlm@(Just _) -> return tlm+          Nothing  -> loop (init ns)+          Just tlm -> return tlm -getTopLevelModuleForQName :: QName -> TCM (Maybe TopLevelModuleName)+-- | Get the toplevel module parent to a given a name.+getTopLevelModuleForQName :: QName -> TCM TopLevelModuleName getTopLevelModuleForQName = getTopLevelModuleForModuleName . qnameModule  lookupModuleInCurrentModule :: C.Name -> TCM [AbstractModule] lookupModuleInCurrentModule x =   List1.toList' . Map.lookup x . nsModules . thingsInScope [PublicNS, PrivateNS] <$> getCurrentScope++-- | Try to unfold a definition if introduced by module application.+maybeUnfoldCopy+  :: PureTCM m+  => QName -- ^ Name of the definition.+  -> Elims+  -> (Term -> m a)+  -- ^ Callback if the definition is indeed a copy.+  -> (QName -> Elims -> m a)+  -- ^ Callback if the definition isn't a copy.+  -> m a+maybeUnfoldCopy f es onTerm onDef =+  reduceDefCopy f es >>= \case+    NoReduction ()   -> onDef f es+    YesReduction _ t -> onTerm t

@@ -19,13 +19,12 @@ import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma ) import Agda2Hs.Compile.Postulate ( compilePostulate ) import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma )-import Agda2Hs.Compile.Rewrites import Agda2Hs.Compile.Types-import Agda2Hs.Compile.Utils ( tellExtension )+import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension ) import Agda2Hs.Pragma  -- Needs a list of rewrite rules too.-initCompileEnv :: TopLevelModuleName -> Rewrites -> CompileEnv+initCompileEnv :: TopLevelModuleName -> SpecialRules -> CompileEnv initCompileEnv tlm rewrites = CompileEnv   { currModule = tlm   , minRecordName = Nothing@@ -38,7 +37,7 @@ initCompileState :: CompileState initCompileState = CompileState { lcaseUsed = 0 } -runC :: TopLevelModuleName -> Rewrites -> C a -> TCM (a, CompileOutput)+runC :: TopLevelModuleName -> SpecialRules -> C a -> TCM (a, CompileOutput) runC tlm rewrites = runWriterT      . flip runReaderT (initCompileEnv tlm rewrites)      . flip evalStateT initCompileState@@ -55,45 +54,46 @@     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)+    compileAndTag = processPragma (defName def) >>= \ p -> +      setCurrentRangeQ (defName def) $ 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 =

@@ -27,7 +27,7 @@       -> 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+compileData target ds def = do   let d = hsName $ prettyShow $ qnameName $ defName def   checkValidTypeName d   case theDef def of

@@ -19,6 +19,7 @@ import Agda.Syntax.Internal import Agda.Syntax.Literal import Agda.Syntax.Common.Pretty ( prettyShow )+import Agda.Syntax.Scope.Monad ( isDatatypeModule )  import Agda.TypeChecking.Pretty import Agda.TypeChecking.Substitute@@ -27,6 +28,8 @@  import Agda.Utils.Functor ( (<&>) ) import Agda.Utils.Impossible ( __IMPOSSIBLE__ )+import Agda.Utils.List+import Agda.Utils.Maybe import Agda.Utils.Monad  import Agda2Hs.AgdaUtils@@ -37,10 +40,12 @@ import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils import Agda2Hs.HsUtils+import Agda.TypeChecking.Datatypes (isDataOrRecord)  isSpecialPat :: QName -> Maybe (ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())) isSpecialPat qn = case prettyShow qn of-  "Haskell.Prim.Tuple._;_" -> Just tuplePat+  "Haskell.Prim.Tuple._,_"         -> Just tuplePat+  "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 =<<@@ -57,14 +62,7 @@ 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+tuplePat cons i ps = mapM (compilePat . namedArg) ps <&> Hs.PTuple () Hs.Boxed  -- Agda2Hs does not support natural number patterns directly (since -- they don't exist in Haskell), however they occur as part of@@ -96,17 +94,32 @@ 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+  reportSDoc "agda2hs.compile" 6 $ "Compiling function: " <+> prettyTCM defName+  when withSig $ whenJustM (liftTCM $ isDatatypeModule $ qnameModule defName) $ \_ ->+    genericDocError =<< text "not supported by agda2hs: functions inside a record module"   let keepClause = maybe False keepArg . clauseType-  withCurrentModule m $ setCurrentRange (nameBindingSite n) $ do-    ifM (endsInSort defType) (ensureNoLocals err >> compileTypeDef x def) $ do+  withCurrentModule m $ do+    ifM (endsInSort defType)+        -- if the function type ends in Sort, it's a type alias!+        (ensureNoLocals err >> compileTypeDef x def) +        -- otherwise, we have to compile clauses.+        $ do       when withSig $ checkValidFunName x       compileTopLevelType withSig defType $ \ty -> do-        -- Instantiate the clauses to the current module parameters+        let filtered = filter keepClause funClauses+        weAreOnTop <- isJust <$> liftTCM  (currentModule >>= isTopLevelModule)         pars <- getContextArgs-        reportSDoc "agda2hs.compile" 10 $ "applying clauses to parameters: " <+> prettyTCM pars-        let clauses = filter keepClause funClauses `apply` pars+        -- We only instantiate the clauses to the current module parameters+        -- if the current module isn't the toplevel module+        unless weAreOnTop $+          reportSDoc "agda2hs.compile.type" 6 $ "Applying module parameters to clauses: " <+> prettyTCM pars+        let clauses = if weAreOnTop then filtered else filtered `apply` pars         cs <- mapMaybeM (compileClause (qnameModule defName) x) clauses++        when (null cs) $ genericDocError+          =<< text "Functions defined with absurd patterns exclusively are not supported."+          <+> text "Use function `error` from the Haskell.Prelude instead."+         return $ [Hs.TypeSig () [x] ty | withSig ] ++ [Hs.FunBind () cs]   where     Function{..} = theDef@@ -122,16 +135,25 @@ compileClause mod x c = withClauseLocals mod c $ compileClause' mod x c  compileClause' :: ModuleName -> Hs.Name () -> Clause -> C (Maybe (Hs.Match ()))-compileClause' curModule x c@Clause{ clauseBody = Nothing} = return Nothing+compileClause' curModule x c@Clause{clauseBody = Nothing} = pure Nothing compileClause' curModule x c@Clause{..} = do   reportSDoc "agda2hs.compile" 7 $ "compiling clause: " <+> prettyTCM c+  reportSDoc "agda2hs.compile" 17 $ "Old context: " <+> (prettyTCM =<< getContext)+  reportSDoc "agda2hs.compile" 17 $ "Clause telescope: " <+> prettyTCM clauseTel   addContext (KeepNames clauseTel) $ do     ps <- compilePats namedClausePats-    body <- compileTerm $ fromMaybe __IMPOSSIBLE__ clauseBody     let isWhereDecl = not . isExtendedLambdaName           /\ (curModule `isFatherModuleOf`) . qnameModule     children <- filter isWhereDecl <$> asks locals     whereDecls <- mapM (getConstInfo >=> compileFun' True) children+    -- Jesper, 2023-10-30: We should compile the body in the module of the+    -- `where` declarations (if there are any) in order to drop the arguments+    -- that correspond to the pattern variables of this clause from the calls to+    -- the functions defined in the `where` block.+    let inWhereModule = case children of+          [] -> id+          (c:_) -> withCurrentModule $ qnameModule c+    body <- inWhereModule $ compileTerm $ fromMaybe __IMPOSSIBLE__ clauseBody     let rhs = Hs.UnGuardedRhs () body         whereBinds | null whereDecls = Nothing                    | otherwise       = Just $ Hs.BDecls () (concat whereDecls)

@@ -1,5 +1,4 @@--module Agda2Hs.Compile.Imports ( compileImports, makeManualDecl ) where+module Agda2Hs.Compile.Imports ( compileImports, preludeImportDecl ) where  import Data.Char ( isUpper ) import Data.List ( isPrefixOf )@@ -87,12 +86,26 @@           ++ prettyShow (pp <$> p') ++ ")"         -- TODO: no range information as we only have Haskell names at this point --- if the user has provided a "using" or "hiding" list in the config file--- used for Prelude-makeManualDecl :: Hs.ModuleName () -> Qualifier -> Bool -> [String] -> Hs.ImportDecl ()-makeManualDecl mod qual isImplicit namesToHide = Hs.ImportDecl ()-       mod (isQualified qual) False False Nothing (qualifiedAs qual)-      (Just $ Hs.ImportSpecList ()-            isImplicit        -- whether the list should be a list of hidden identifiers ('hiding')-            $ map (Hs.IVar() . (\str -> if validVarId str || validConId str then Hs.Ident() str else Hs.Symbol() str))    -- since we can only read strings from the config file, we have to do this-            namesToHide) -- map (uncurry makeImportSpec) $ Map.toList specs)++-- | Generate a prelude import considering prelude config options (hiding, implicit, etc).+preludeImportDecl :: PreludeOptions -> Hs.ImportDecl ()+preludeImportDecl (PreludeOpts{..}) =+  let toName s | validVarId s || validConId s = Hs.Ident () s+      toName s = Hs.Symbol () s++      -- if the prelude is implicit, we use the provided hiding list.+      -- if it is explicit, we use the import list.+      spec = Hs.ImportSpecList () preludeImplicit $+              map (Hs.IVar () . toName) $+                if preludeImplicit then preludeHiding+                                   else concat preludeImports+  in Hs.ImportDecl+    { importAnn       = ()+    , importModule    = Hs.prelude_mod ()+    , importQualified = False+    , importSrc       = False+    , importSafe      = False+    , importPkg       = Nothing+    , importAs        = Nothing+    , importSpecs     = Just spec+    }

@@ -7,8 +7,10 @@ import Control.Monad.Reader  import Data.Functor ( (<&>) )+import Data.Bifunctor ( bimap ) import Data.List ( intercalate, isPrefixOf ) import Data.Text ( unpack )+import qualified Data.Map.Strict as Map  import qualified Language.Haskell.Exts as Hs @@ -16,7 +18,7 @@ import Agda.Compiler.Common ( topLevelModuleName )  import qualified Agda.Syntax.Abstract as A-import Agda.Syntax.Common+import Agda.Syntax.Common hiding (Rewrite) import Agda.Syntax.Internal import Agda.Syntax.Position import qualified Agda.Syntax.Concrete as C@@ -34,7 +36,6 @@ import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM )  import Agda2Hs.AgdaUtils-import Agda2Hs.Compile.Rewrites import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils import Agda2Hs.HsUtils@@ -44,46 +45,42 @@     "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.⊤"        -> special Hs.UnitCon     "Agda.Builtin.Unit.tt"       -> special Hs.UnitCon     _ -> Nothing   where special c = Just (Hs.Special () $ c ()) --- Gets an extra parameter, with the user-defined rewrite rules in it.--- If finds it in the user-defined or the built-in rewrite rules, then it returns the new name and a possible import in a Just; otherwise returns Nothing.-isSpecialName :: QName -> Rewrites -> Maybe (Hs.Name (), Maybe Import)-isSpecialName f rules = let pretty = prettyShow f in case lookupRules pretty rules of-    result@(Just _)     -> result-    Nothing             -> case pretty of-      "Agda.Builtin.Nat.Nat"          -> withImport "Numeric.Natural" "Natural"-      "Haskell.Control.Monad.guard"   -> withImport "Control.Monad" "guard"-      "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) (Hs.NoNamespace ())-                                                                       -- ^ TODO: add an option to specify this in the config file (whether it is a type or not)-                                                                       -- as far as I know, there are no type operators in Prelude, but maybe a self-defined one could cause trouble-      in Just (hsName x, Just imp)+-- | Convert identifier and import module strings into the Haskell equivalent syntax.+toNameImport :: String -> Maybe String -> (Hs.Name (), Maybe Import)+toNameImport x Nothing = (hsName x, Nothing)+toNameImport x (Just mod) =+  ( hsName x+  , Just $ Import (hsModuleName mod) Unqualified Nothing (hsName x) (Hs.NoNamespace ())+  ) -    lookupRules :: String -> Rewrites -> Maybe (Hs.Name (), Maybe Import)-    lookupRules _ [] = Nothing-    lookupRules pretty (rule:ls)-      | pretty == from rule   = case (importing rule) of     -- check if there is a new import-          Just lib -> withImport lib (to rule)-          Nothing  -> noImport (to rule)-      | otherwise             = lookupRules pretty ls+-- | Default rewrite rules.+defaultSpecialRules :: SpecialRules+defaultSpecialRules = Map.fromList+  [ "Agda.Builtin.Nat.Nat"          `to` "Natural"      `importing` Just "Numeric.Natural"+  , "Haskell.Control.Monad.guard"   `to` "guard"        `importing` Just "Control.Monad"+  , "Haskell.Prelude.coerce"        `to` "unsafeCoerce" `importing` Just "Unsafe.Coerce"+  , "Agda.Builtin.Int.Int"          `to` "Integer"      `importing` Nothing+  , "Agda.Builtin.Word.Word64"      `to` "Word"         `importing` Nothing+  , "Agda.Builtin.Float.Float"      `to` "Double"       `importing` Nothing+  , "Agda.Builtin.Bool.Bool.false"  `to` "False"        `importing` Nothing+  , "Agda.Builtin.Bool.Bool.true"   `to` "True"         `importing` Nothing+  , "Haskell.Prim._∘_"              `to` "_._"          `importing` Nothing+  , "Haskell.Prim.Monad.Dont._>>=_" `to` "_>>=_"        `importing` Nothing+  , "Haskell.Prim.Monad.Dont._>>_"  `to` "_>>_"         `importing` Nothing+  ]+  where infixr 6 `to`, `importing`+        to = (,)+        importing = toNameImport +-- | Check whether the given name should be rewritten to a special Haskell name, possibly with new imports.+isSpecialName :: QName -> C (Maybe (Hs.Name (), Maybe Import))+isSpecialName f = asks (Map.lookup (prettyShow f) . rewrites)+ compileName :: Applicative m => Name -> m (Hs.Name ()) compileName n = hsName . show <$> pretty (nameConcrete n) @@ -100,8 +97,7 @@       Just (r, Record{recNamedCon = False}) -> r -- use record name for unnamed constructors       _                                     -> f     hf0 <- compileName (qnameName f)-    rules <- asks rewrites-    let (hf, mimpBuiltin) = fromMaybe (hf0, Nothing) (isSpecialName f rules)+    (hf, mimpBuiltin) <- fromMaybe (hf0, Nothing) <$> isSpecialName f     parent <- parentName f     par <- traverse (compileName . qnameName) parent     let mod0 = qnameModule $ fromMaybe f parent@@ -150,10 +146,10 @@         (C.Qual as C.QName{} : _) -> liftTCM $ do           let qual = hsModuleName $ prettyShow as           lookupModuleInCurrentModule as >>= \case-            (x:_) | qual /= mod -> isDatatypeModule (amodName x) >>= \case-              Just{} -> return $ QualifiedAs Nothing-              Nothing -> return $ QualifiedAs $ Just qual-            _ -> return Nothing+            (x:_) | qual /= mod -> do+              isDataMod <- isJust <$> isDatatypeModule (amodName x)+              return $ QualifiedAs (if isDataMod then Nothing else Just qual)+            _ -> return $ QualifiedAs Nothing           `catchError` \_ -> return $ QualifiedAs Nothing         _ -> return $ QualifiedAs Nothing @@ -196,13 +192,12 @@ hsTopLevelModuleName = hsModuleName . intercalate "." . map unpack                      . List1.toList . moduleNameParts +-- | Given a module name (assumed to be a toplevel module), +-- compute the associated Haskell module name. 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+compileModuleName m = do+  tlm <- liftTCM $ hsTopLevelModuleName <$> getTopLevelModuleForModuleName m+  reportSDoc "agda2hs.name" 25 $+    text "Top-level module name for" <+> prettyTCM m <+>+    text "is" <+> text (pp tlm)+  return tlm

@@ -1,3 +1,4 @@+{-# LANGUAGE NamedFieldPuns #-} module Agda2Hs.Compile.Record where  import Control.Monad ( unless )@@ -88,7 +89,7 @@   return ([minPragma | not (null prims)] ++ Map.elems decls)  compileRecord :: RecordTarget -> Definition -> C (Hs.Decl ())-compileRecord target def = setCurrentRange (nameBindingSite $ qnameName $ defName def) $ do+compileRecord target def = do   TelV tel _ <- telViewUpTo recPars (defType def)   addContext tel $ checkingVars $ do     checkValidTypeName rName@@ -123,7 +124,7 @@     -- record module has been opened.     checkFieldInScope f = isInScopeUnqualified f >>= \case       True  -> return ()-      False -> setCurrentRange (nameBindingSite $ qnameName f) $ genericError $+      False -> setCurrentRangeQ 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."@@ -168,7 +169,11 @@       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."+checkUnboxPragma def+  | Record{recFields} <- def+  , length (filter keepArg recFields) == 1+  , not (recRecursive def)+  = return ()++  | otherwise+  = genericError "An unboxed type must be a non-recursive record type with exactly one non-erased field."

@@ -1,107 +0,0 @@--- Reads custom rewrite rules of the user from a YAML config file.-module Agda2Hs.Compile.Rewrites (readConfigFile) where--import Data.Yaml.YamlLight-import qualified Data.Map as Map-import qualified Data.Text as Text-import Data.Text.Encoding (decodeUtf8, encodeUtf8)-import qualified Data.ByteString as ByteString-import Data.Char (toLower)-import Data.Maybe (isJust)--import Agda2Hs.Compile.Types---- Conversions from String to ByteString and vice versa.--- We assume UTF-8.-stringToByteString :: String -> ByteString.ByteString-stringToByteString = encodeUtf8 . Text.pack-byteStringToString :: ByteString.ByteString -> String-byteStringToString = Text.unpack . decodeUtf8---- A simple element consisting of the string given. Useful when looking up maps.-stringElement :: String -> YamlLight-stringElement = YStr . stringToByteString---- Read Prelude options from a YamlLight object. Fail if the format is incorrect.-preludeOptionsFromYaml :: YamlLight -> Maybe PreludeOptions-preludeOptionsFromYaml yaml = case lookupYL (stringElement "prelude") yaml of-  Nothing            -> Nothing-  Just (YMap dmap)   -> Just $ preludeOptionsFromMap dmap-  Just otherYaml     -> error $ "Incorrect format for the rewrite rules file: the \"prelude\" element must be a map – " ++ show otherYaml-  where-    preludeOptionsFromMap :: Map.Map YamlLight YamlLight -> PreludeOptions-    preludeOptionsFromMap dmap = (impl, namesToImp)-      where-        impl :: Bool-        impl = case Map.lookup (stringElement "implicit") dmap of-          Nothing        -> isJust $ Map.lookup (YStr $ stringToByteString "hiding") dmap-          Just (YStr bs) -> let str = map toLower $ byteStringToString bs in-                             str == "true" || str == "yes"-          Just otherYaml -> error "Incorrect format for the rewrite rules file: \"implicit\" must be a boolean"--        namesToImp :: NamesToImport-        namesToImp = if impl then hidingNames else importingNames         -- we search for different keys-          where-            hidingNames :: NamesToImport-            hidingNames = case Map.lookup (stringElement "hiding") dmap of-              Nothing        -> Names []    -- then we import the whole Prelude-              Just (YSeq ls) -> Names $ map (parseElement "hiding") $ ls-              Just otherYaml -> error "Incorrect format for the rewrite rules file: \"hiding\" must be a sequence"--            importingNames :: NamesToImport-            importingNames = case Map.lookup (stringElement "using") dmap of-              Nothing        -> Auto       -- then we let agda2hs search for them-              Just (YSeq ls) -> Names $ map (parseElement "using") $ ls-              Just otherYaml -> error "Incorrect format for the rewrite rules file: \"\" must be a sequence"--            parseElement :: String -> YamlLight -> String-            parseElement seqName y = case (unStr y) of-              Nothing -> error "Incorrect format for the rewrite rules file: an element in \"" ++ seqName ++ "\" was not a string"-              Just bs -> byteStringToString bs---- Read rewrite rules from a YamlLight object. Fail if the format is incorrect.-rulesFromYaml :: YamlLight -> Rewrites-rulesFromYaml y = case lookupYL (stringElement "rules") y of-  Nothing           -> case y of   -- maybe the root is the sequence-                         YSeq ls -> map ruleFromElement ls-                         _       -> []-  Just YNil         -> []-  Just (YSeq ls)    -> map ruleFromElement ls-  Just otherYaml    -> error $ "Incorrect format for the rewrite rules file: \"rules\" must be a list of elements – " ++ show otherYaml-  where-    -- parsing a single element-    ruleFromElement :: YamlLight -> Rewrite-    ruleFromElement (YMap dmap) = case (safeRuleFromMap dmap) of-      Right rule -> rule-      Left e     -> error e-    ruleFromElement otherYaml   = error $ "Not a map: " ++ show otherYaml-    -    safeRuleFromMap :: Map.Map YamlLight YamlLight -> Either String Rewrite-    safeRuleFromMap yamlMap = do-      let dmap = Map.mapKeys unpackString $ Map.map unpackString yamlMap-      from <- safeLookup (pure "from") dmap-      to   <- safeLookup (pure "to") dmap-      case Map.lookup (Right "importing") dmap of-        Just (Right lib) -> Right $ Rewrite from to (Just lib)-        Just (Left e)    -> Left e-        Nothing          -> Right $ Rewrite from to Nothing--    -- not too pretty... but Map.Map is not Traversable-    safeLookup :: Either String String -> Map.Map (Either String String) (Either String String) -> Either String String-    safeLookup key dmap = case Map.lookup key dmap of-      Just val -> val-      Nothing  -> Left $ "Key not found: " ++ show key--    unpackString :: YamlLight -> Either String String-    unpackString yaml = case (unStr yaml) of-      Just bytestr -> Right $ byteStringToString $ bytestr-      Nothing      -> Left $ "Not a string element: " ++ show yaml---- The exported function to be used in Main.hs.-readConfigFile :: FilePath -> IO Config-readConfigFile fname = (,) <$>-                       (preludeOptionsFromYaml <$> wholeYaml) <*>-                       (rulesFromYaml <$> wholeYaml)-  where-    wholeYaml :: IO YamlLight-    wholeYaml = parseYamlFile fname

@@ -53,18 +53,12 @@  isSpecialCon :: QName -> Maybe (ConHead -> ConInfo -> Elims -> C (Hs.Exp ())) isSpecialCon = prettyShow >>> \case-  "Haskell.Prim.Tuple._;_" -> Just tupleTerm+  "Haskell.Prim.Tuple._,_"         -> Just tupleTerm+  "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tupleTerm   _ -> Nothing  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+tupleTerm cons i es = compileElims es <&> Hs.Tuple () Hs.Boxed  ifThenElse :: QName -> Elims -> C (Hs.Exp ()) ifThenElse _ es = compileElims es >>= \case@@ -179,7 +173,7 @@   _ -> genericError $ "case_of_ must be fully applied to a lambda"  lambdaCase :: QName -> Elims -> C (Hs.Exp ())-lambdaCase q es = setCurrentRange (nameBindingSite $ qnameName q) $ do+lambdaCase q es = setCurrentRangeQ q $ do   Function{funClauses = cls, funExtLam = Just ExtLamInfo {extLamModule = mname}}     <- theDef <$> getConstInfo q   npars <- size <$> lookupSection mname@@ -208,6 +202,7 @@   where s = Text.unpack t compileLiteral l               = genericDocError =<< text "bad term:" <?> prettyTCM (Lit l) +-- | Compile a variable. If the check is enabled, ensures the variable is usable and visible. compileVar :: Nat -> C String compileVar x = do   (d, n) <- (fmap snd &&& fst . unDom) <$> lookupBV x@@ -229,28 +224,29 @@       hsVar s `app` es     -- v currently we assume all record projections are instance     -- args that need attention-    Def f es+    Def f es -> maybeUnfoldCopy f es compileTerm $ \f es -> if       | Just semantics <- isSpecialTerm f -> do-        reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of special function"-        semantics f es+          reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of special function"+          semantics f es       | otherwise -> isClassFunction f >>= \case-        True  -> compileClassFunApp f es-        False -> (isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f >>= \case-          True  -> compileErasedApp es-          False -> do-            reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"-            -- Drop module parameters of local `where` functions-            xs <- asks locals-            reportSDoc "agda2hs.compile.term" 15 $ text "Locals: " <+> (prettyTCM xs)-            n <- if-              | f `elem` xs -> size <$> lookupSection (qnameModule f)-              | otherwise   -> return 0-            (`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)+          True  -> compileClassFunApp f es+          False -> (isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f >>= \case+            True  -> compileErasedApp es+            False -> do+              reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"+              -- Drop module parameters of local `where` functions+              moduleArgs <- getDefFreeVars f+              reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs+              (`app` drop moduleArgs es) . Hs.Var () =<< compileQName f+    Con h i es -> do+      reportSDoc "agda2hs.compile" 8 $ text "reached constructor:" <+> prettyTCM (conName h)+      -- the constructor may be a copy introduced by module application,+      -- therefore we need to find the original constructor+      info <- getConstInfo (conName h)+      if not (defCopy info)+        then compileCon h i es+        else let Constructor{conSrcCon = c} = theDef info in+             compileCon c ConOSystem es     Lit l -> compileLiteral l     Lam v b | usableModality v, getOrigin v == UserWritten -> do       when (patternInTeleName `isPrefixOf` absName b) $ genericDocError =<< do@@ -274,7 +270,16 @@     t -> genericDocError =<< text "bad term:" <?> prettyTCM t   where     app :: Hs.Exp () -> Elims -> C (Hs.Exp ())-    app hd es = eApp <$> pure hd <*> compileElims es+    app hd es = eApp hd <$> compileElims es++    compileCon :: ConHead -> ConInfo -> Elims -> C (Hs.Exp ())+    compileCon h i es+      | Just semantics <- isSpecialCon (conName h)+      = semantics h i es+    compileCon h i es =+      isUnboxConstructor (conName h) >>= \case+        Just _  -> compileErasedApp es+        Nothing -> (`app` es) . Hs.Con () =<< compileQName (conName h)  -- `compileErasedApp` compiles an application of an erased constructor -- or projection.

@@ -4,8 +4,10 @@  import Control.Arrow ( (>>>) ) import Control.Monad ( forM, when )+import Control.Monad.Trans ( lift ) import Control.Monad.Reader ( asks )-import Data.Maybe ( mapMaybe )+import Data.List ( find )+import Data.Maybe ( mapMaybe, isJust )  import qualified Language.Haskell.Exts.Syntax as Hs import qualified Language.Haskell.Exts.Extension as Hs@@ -29,7 +31,6 @@ 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@@ -39,43 +40,32 @@  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+  let Just as = allApplyElims es+  ts <- mapM (compileType . unArg) as   return $ Hs.TyTuple () Hs.Boxed ts -constrainType :: Hs.Asst () -> Hs.Type () -> Hs.Type ()+-- | Add a class constraint to a Haskell type.+constrainType+  :: Hs.Asst () -- ^ The class assertion.+  -> Hs.Type () -- ^ The type to constrain.+  -> 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 ()+-- | Add explicit quantification over a variable to a Haskell type.+qualifyType+  :: String     -- ^ Name of the variable.+  -> Hs.Type () -- ^ Type to quantify.+  -> 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@@ -83,29 +73,51 @@   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++-- | Compile a top-level type, such that:+--+--   * erased parameters of the current module are dropped.+--   * usable hidden type parameters of the current module are explicitely quantified.+--   * usable instance parameters are added as type constraints.+--   * usable explicit parameters are forbidden (for now).+--+--   The continuation is called in an extended context with these type+--   arguments bound.+compileTopLevelType+    :: Bool+    -- ^ Whether the generated Haskell type will end up in+    --   the final output. If so, this functions asks for+    --   language extension ScopedTypeVariables to be enabled.+    -> Type+    -> (Hs.Type () -> C a) -- ^ Continuation with the compiled type.+    -> C a compileTopLevelType keepType t cont = do     reportSDoc "agda2hs.compile.type" 12 $ text "Compiling top-level type" <+> prettyTCM t+    -- NOTE(flupe): even though we only quantify variable for definitions inside anonymous modules,+    --              they will still get quantified over the toplevel module parameters.+    weAreOnTop <- isJust <$> liftTCM  (currentModule >>= isTopLevelModule)     modTel <- moduleParametersToDrop =<< currentModule-    go modTel cont+    reportSDoc "agda2hs.compile.type" 19 $ text "Module parameters to process: " <+> prettyTCM modTel+    go weAreOnTop modTel cont   where-    go :: Telescope -> (Hs.Type () -> C a) -> C a-    go EmptyTel cont = do+    go :: Bool -> 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+    go onTop (ExtendTel a atel) cont+      | not (usableModality a) =+          underAbstraction a atel $ \tel -> go onTop tel 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))+            go onTop tel (cont . constrainType c)+      | otherwise = do+          compileType (unEl $ unDom a)+          when (keepType && not onTop) $ tellExtension Hs.ScopedTypeVariables+          let qualifier = if onTop then id else qualifyType (absName atel)+          underAbstraction a atel $ \tel ->+            go onTop tel (cont . qualifier)  compileType' :: Term -> C (Strictness, Hs.Type ()) compileType' t = do@@ -114,9 +126,12 @@     _        -> return Lazy   (s,) <$> compileType t +-- | Compile an Agda term into a Haskell type. compileType :: Term -> C (Hs.Type ()) compileType t = do   reportSDoc "agda2hs.compile.type" 12 $ text "Compiling type" <+> prettyTCM t+  reportSDoc "agda2hs.compile.type" 22 $ text "Compiling type" <+> pretty t+   case t of     Pi a b -> compileDom (absName b) a >>= \case       DomType _ hsA -> do@@ -126,24 +141,29 @@         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+    Def f es -> maybeUnfoldCopy f es compileType $ \f es -> do+      def <- getConstInfo f+      if | not (usableModality def) ->+            genericDocError+              =<< text "Cannot use erased definition" <+> prettyTCM f+              <+> text "in Haskell type"+         | 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+         | otherwise -> fail     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 ())     Lam argInfo restAbs-      | not (keepArg argInfo)   -> underAbstraction_ restAbs compileType-    _ -> genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t+      | not (keepArg argInfo) -> underAbstraction_ restAbs compileType+    _ -> fail+  where fail = genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t  compileTypeArgs :: Args -> C [Hs.Type ()] compileTypeArgs args = mapM (compileType . unArg) $ filter keepArg args@@ -151,13 +171,14 @@ 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+  let tel = telToList $ recTel def `apply` pars+  case find keepArg tel of+    Nothing -> __IMPOSSIBLE__+    Just t -> compileType $ unEl $ snd (unDom t)  compileTransparentType :: Args -> C (Hs.Type ()) compileTransparentType args = compileTypeArgs args >>= \case-  [] -> genericError "Not supported: underapplied type synonyms"+  []     -> __IMPOSSIBLE__   (v:vs) -> return $ v `tApp` vs  compileDom :: ArgName -> Dom Type -> C CompiledDom

@@ -28,33 +28,37 @@  type Code = (Hs.Module Hs.SrcSpanInfo, [Hs.Comment]) --- For config files and rewrite rules.--- There is already a RewriteRule identifier in Agda internals, hence the name.--- Elements:-  -- the identifier to rewrite ("from")-  -- the identifier with which we replace it ("to")-  -- the import to use, if any ("importing")-data Rewrite = Rewrite {from :: String, to :: String, importing :: Maybe String}+-- | Custom substitution for a given definition.+data Rewrite = Rewrite+  { rewFrom   :: String+    -- ^ The fully qualified name.+  , rewTo     :: String+    -- ^ The corresponding Haskell name.+  , rewImport :: Maybe String+    -- ^ Haskell module to import.+  }  type Rewrites = [Rewrite] -data NamesToImport = Auto | Names [String]     -- Auto if Prelude is explicit and we want agda2hs to figure out the import list by itself+-- | A lookup table for rewrite rules.+type SpecialRules = Map String (Hs.Name (), Maybe Import) -type PreludeOptions = (Bool, NamesToImport)-                       -- ^ whether Prelude functions should be implicitly imported; if yes, then NamesToImport is a "hiding" list+data PreludeOptions = PreludeOpts+  { preludeImplicit :: Bool+  , preludeImports  :: Maybe [String]+  , preludeHiding   :: [String]+  }+  -- ^ whether Prelude functions should be implicitly imported; if yes, then NamesToImport is a "hiding" list --- The type of an entire parsed config file.-type Config = (Maybe PreludeOptions, Rewrites)-            -- ^ Nothing if there was no "prelude" element in the file -data Options = Options { optIsEnabled         :: Bool,-                      -- ^ false if the backend is disabled because we want vanilla Agda behaviour (important for Emacs)-                         optOutDir            :: Maybe FilePath,-                         optExtensions        :: [Hs.Extension],-                         optRewrites          :: Rewrites,-                      -- ^ the rewrite rules read from user-provided config files-                         optPrelude           :: PreludeOptions }-                      -- ^ options on how to handle Prelude; see Agda2Hs.Compile.Rewrites+data Options = Options+  { optIsEnabled  :: Bool+  , optOutDir     :: Maybe FilePath+  , optConfigFile :: Maybe FilePath+  , optExtensions :: [Hs.Extension]+  , optRewrites   :: SpecialRules+  , optPrelude    :: PreludeOptions+  }  -- Required by Agda-2.6.2, but we don't really care. instance NFData Options where@@ -71,8 +75,8 @@   -- ^ whether copatterns should be allowed when compiling patterns   , checkVar :: Bool   -- ^ whether to ensure compiled variables are usable and visible-  , rewrites :: Rewrites-  -- ^ the user-defined rewrite rules read from a config file+  , rewrites :: SpecialRules+  -- ^ Special compilation rules.   }  type Qualifier = Maybe (Maybe (Hs.ModuleName ()))

@@ -163,8 +163,12 @@    isDatatypeModule mod >>= \case      Just _ -> return EmptyTel      Nothing -> do+       reportSDoc "agda2hs.moduleParameters" 25 $ text "Current context: " <+> (prettyTCM =<< getContext)        ctxArgs <- getContextArgs-       (`apply` ctxArgs) <$> lookupSection mod+       reportSDoc "agda2hs.moduleParameters" 25 $ text "Context arguments: " <+> prettyTCM ctxArgs+       sec <- lookupSection mod+       reportSDoc "agda2hs.moduleParameters" 25 $ text "Module section: " <+> prettyTCM sec+       return $ sec `apply` ctxArgs  isUnboxRecord :: QName -> C (Maybe Strictness) isUnboxRecord q = do

@@ -0,0 +1,70 @@+{-# LANGUAGE OverloadedStrings #-}+-- Read additional configuration options from a file.+module Agda2Hs.Config (checkConfig) where++import Control.Monad.IO.Class ( MonadIO(liftIO) )+import GHC.Generics++import Data.Functor ( (<&>) )+import Data.Foldable ( fold )+import Data.Maybe ( fromMaybe )+import Data.Aeson ( FromJSON(parseJSON), withObject, (.:), (.:?), (.!=) )+import qualified Data.Aeson.Types as Aeson+import qualified Data.Map.Strict as Map+import qualified Data.Yaml as Yaml++import Agda2Hs.Compile.Types+import Agda2Hs.Compile.Name ( toNameImport )+import Agda.TypeChecking.Monad.Base ( TCM, genericDocError )+import Agda.Syntax.Common.Pretty++-- | Config file data.+data Config = Config+  { cfgPrelude  :: Maybe PreludeOptions+  , cfgRewrites :: Maybe Rewrites+  }++instance FromJSON Rewrite where+  parseJSON = withObject "rewrite rule" $ \v ->+    Rewrite <$> v .:  "from"+            <*> v .:  "to"+            <*> v .:? "importing"++instance FromJSON PreludeOptions where+  parseJSON = withObject "prelude options" $ \v ->+    PreludeOpts <$> v .:  "implicit"+                <*> v .:? "using"+                <*> v .:? "hiding" .!= []++instance FromJSON Config where+  parseJSON (Aeson.Object v) =+    Config <$> v .:? "prelude"+           <*> v .:? "rewrites"+  parseJSON Aeson.Null = pure $ Config Nothing Nothing+  parseJSON invalid =+    Aeson.prependFailure "parsing agda2hs config failed, "+      (Aeson.typeMismatch "Object" invalid)++readConfigFile :: FilePath -> TCM Config+readConfigFile src = do+  liftIO (Yaml.decodeFileEither src) >>= \case+    Left err  -> genericDocError $ vcat+      [ text "An error occured while trying to parse config file " <> text src <>":"+      , multiLineText (Yaml.prettyPrintParseException err)+      ]+    Right cfg -> return cfg++applyConfig :: Options -> Config -> Options+applyConfig opts cfg =+  opts { optPrelude  = fromMaybe (optPrelude opts) (cfgPrelude cfg)+       , optRewrites = foldl addRewrite (optRewrites opts) (fold $ cfgRewrites cfg)+       }+  where addRewrite :: SpecialRules -> Rewrite -> SpecialRules+        addRewrite rules (Rewrite from to importing) = Map.insert from (toNameImport to importing) rules++checkConfig :: Options -> TCM Options+checkConfig opts+  | Just src <- optConfigFile opts+  = readConfigFile src <&> applyConfig opts+checkConfig opts = return opts+

@@ -1,11 +1,11 @@ module Agda2Hs.Render where  import Control.Monad ( unless )-import Control.Monad.Except ( MonadIO(liftIO) )+import Control.Monad.IO.Class ( MonadIO(liftIO) )  import Data.Function ( on ) import Data.List ( sortBy, nub )-import Data.Maybe ( fromMaybe )+import Data.Maybe ( fromMaybe, isNothing ) import Data.Set ( Set ) import qualified Data.Set as Set @@ -142,27 +142,40 @@       imps = concat impss       exts = concat extss   unless (null code && null defs && isMain == NotMain) $ do-    -- Add automatic imports+     let unlines' [] = []         unlines' ss = unlines ss ++ "\n"-    let filteredImps = case optPrelude opts of-          (False, Auto) -> imps                                                              -- import Prelude explicitly and search for imported identifiers, just like at other modules-          _             -> filter (not . (== Hs.prelude_mod ()) . importModule) imps         -- handle Prelude separately-    let autoImportList = case optPrelude opts of-          (False, Auto)               -> compileImports mod filteredImps -- then we have left Prelude in filteredImps-          (True,  Names [])           -> compileImports mod filteredImps -- we write nothing about Prelude and import everything-          (isImplicit, Names names)   -> (:) <$>-                                         (pure $ makeManualDecl (Hs.prelude_mod ()) Nothing isImplicit names) <*>-                                         compileImports mod filteredImps-          (True,  Auto)               -> __IMPOSSIBLE__++    let preOpts@PreludeOpts{..} = optPrelude opts++    -- if the prelude is supposed to be implicit,+    -- or the prelude imports have been fixed in the config file,+    -- we remove it from the list of imports+    let filteredImps =+          if not preludeImplicit && isNothing preludeImports+            then imps+            else filter ((/= Hs.prelude_mod ()) . importModule) imps++    -- then we try to add it back+    let autoImportList =+          if (not preludeImplicit && isNothing preludeImports) || null preludeHiding+            then compileImports mod filteredImps+            else (preludeImportDecl preOpts:) <$> compileImports mod filteredImps++    -- Add automatic imports     autoImports <- (unlines' . map prettyShowImportDecl) <$> autoImportList+     -- The comments make 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 ]+          [ renderLangExts exts+          , renderBlocks $ codePragmas code+          , "module " ++ mod ++ " where\n\n"+          , autoImports+          , renderBlocks defs+          ]+     reportSLn "" 1 $ "Writing " ++ hsFile+     liftIO $ ensureDirectory hsFile >> writeFile hsFile output

@@ -1,6 +1,8 @@ module Main where -import Control.Monad.IO.Class ( MonadIO(..) )+import Data.Maybe ( fromMaybe )+import Data.Version ( showVersion )+import Control.Monad.IO.Class ( MonadIO(liftIO) )  import System.Console.GetOpt import System.Environment ( getArgs )@@ -13,18 +15,24 @@ import Agda.Main import Agda.Compiler.Backend +import Agda2Hs.Compile.Name ( defaultSpecialRules ) import Agda2Hs.Compile-import Agda2Hs.Compile.Rewrites+import Agda2Hs.Config ( checkConfig ) import Agda2Hs.Compile.Types import Agda2Hs.Render -import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO)+import Paths_agda2hs ( version )  defaultOptions :: Options-defaultOptions = Options{ optIsEnabled = True,-                          optOutDir = Nothing, optExtensions = [],-                          optPrelude = (False, Auto),   -- default to including Prelude explicitly and letting agda2hs search for identifiers to import automatically-                          optRewrites = [] }+defaultOptions = Options+  { optIsEnabled = True+  , optOutDir = Nothing+  , optConfigFile = Nothing+  , optExtensions = []+  , optPrelude = PreludeOpts False Nothing []+    -- by default the Prelude is imported explicitly+  , optRewrites = defaultSpecialRules+  }  disableOpt :: Monad m => Options -> m Options disableOpt opts = return opts{ optIsEnabled = False }@@ -32,27 +40,18 @@ outdirOpt :: Monad m => FilePath -> Options -> m Options outdirOpt dir opts = return opts{ optOutDir = Just dir } +configOpt :: Monad m => FilePath -> Options -> m Options+configOpt src opts = return opts{optConfigFile = Just src}+ extensionOpt :: Monad m => String -> Options -> m Options extensionOpt ext opts = return opts{ optExtensions = Hs.parseExtension ext : optExtensions opts } --- Here we use unsafePerformIO to read the rewrite rules from the files.-rewriteOpt :: Monad m => FilePath -> Options -> m Options-rewriteOpt file opts = return opts{-                         optRewrites = newRules ++ optRewrites opts,-                         optPrelude = case maybePreludeOptions of {-                                   Nothing       -> optPrelude opts;-                                   Just newPOpts -> newPOpts-                                   -- ^ the new one trumps the older one-                                   -- maybe this should be done so that we are given an error in case of conflicting options-                                   }}-  where-    (maybePreludeOptions, newRules) = UNSAFE.unsafePerformIO (readConfigFile file)-{-# NOINLINE rewriteOpt #-}+-- | Update options by reading the config, if any was specified.  backend :: Backend' Options Options ModuleEnv ModuleRes (CompiledDef, CompileOutput) backend = Backend'   { backendName           = "agda2hs"-  , backendVersion        = Just "1.0"+  , backendVersion        = Just (showVersion version)   , options               = defaultOptions   , commandLineFlags      =       [ Option ['d'] ["disable-backend"] (NoArg disableOpt)@@ -61,11 +60,11 @@         "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."-      , Option [] ["rewrite-rules"] (ReqArg rewriteOpt "FILE")-        "Provide custom rewrite rules in a YAML configuration file. Identifiers contained here will be replaced with the one given, with an appropriate import added if requested. The handling of imports from Prelude should preferably also be included in this file. See rewrite-rules-example.yaml for the format."+      , Option [] ["config"] (ReqArg configOpt "FILE")+        "Provide additional configuration to agda2hs with a YAML file."       ]   , isEnabled             = optIsEnabled-  , preCompile            = return+  , preCompile            = checkConfig   , postCompile           = \ _ _ _ -> return ()   , preModule             = moduleSetup   , postModule            = writeModule@@ -74,8 +73,7 @@   , mayEraseType          = \ _ -> return True   } --- Checking whether we are in interactive mode.--- These will imply --disable-backend.+-- | Parse command-line arguments to check whether we are in interactive mode. isInteractive :: IO Bool isInteractive = do   let interactionFlag = Option ['I'] ["interactive", "interaction", "interaction-json"] (NoArg ()) ""@@ -83,8 +81,8 @@   return $ not $ null i  main = do-  -- Issue #201: drop backend when run in interactive mode+  -- Issue #201: disable backend when run in interactive mode   isInt <- isInteractive   if isInt-    then runAgda [Backend (backend{isEnabled = const False})]+    then runAgda [Backend backend{isEnabled = const False}]     else runAgda [Backend backend]

@@ -1,298 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}---- | A program which either tries to add setup code for Agda's Emacs--- mode to the users .emacs file, or provides information to Emacs--- about where the Emacs mode is installed.--- It uses the Agda compiler bundled with agda2hs.--- Based on Agda's src/agda-mode/Main.hs file.--module Main (main) where--import Control.Exception as E-import Control.Monad-import Data.Char-import Data.List (intercalate, isInfixOf)-import Data.Maybe-import Data.Version-import Numeric-import System.Directory-import System.Environment-import System.Exit-import System.FilePath-import System.IO--- import System.IO.Error (isDoesNotExistError)-import System.Process--import Paths_agda2hs (getDataDir, version)---- | The program.--main :: IO ()-main = do-  prog <- getProgName-  args <- getArgs-  case args of-    [arg] | arg == locateFlag -> printEmacsModeFile-          | arg == setupFlag  -> do-             dotEmacs <- findDotEmacs-             setupDotEmacs (Files { thisProgram = prog-                                  , dotEmacs    = dotEmacs-                                  })-          | arg == compileFlag ->-             compileElispFiles-    _  -> do inform usage-             exitFailure---- Command line options.--setupFlag   = "setup"-locateFlag  = "locate"-compileFlag = "compile"---- | Usage information.--usage :: String-usage = unlines-  [ "This program is part of agda2hs version " ++ ver ++ "."-  , "It performs actions related to the Emacs mode of the Agda compiler"-  , "bundled with agda2hs."-  , ""-  , "The program can be run in three modes, depending on which option"-  , "it is invoked with:"-  , ""-  , setupFlag-  , ""-  , "  The program tries to add setup code for Agda's Emacs mode to the"-  , "  current user's .emacs file. It is assumed that the .emacs file"-  , "  uses the character encoding specified by the locale."-  , ""-  , locateFlag-  , ""-  , "  The path to the Emacs mode's main file is printed on standard"-  , "  output (using the UTF-8 character encoding and no trailing"-  , "  newline)."-  , ""-  , compileFlag-  , ""-  , "  The program tries to compile Agda's Emacs mode's source files."-  , ""-  , "  WARNING: If you reinstall the Agda mode without recompiling the Emacs"-  , "  Lisp files, then Emacs may continue using the old, compiled files."-  ]---- | The current version of Agda.--ver :: String-ver = intercalate "." $ map show $-        versionBranch version----------------------------------------------------------------------------- Locating the Agda mode---- | Prints out the path to the Agda mode's main file (using UTF-8 and--- without any trailing newline).--printEmacsModeFile :: IO ()-printEmacsModeFile = do-  dataDir <- getDataDir-  let path = dataDir </> "emacs-mode" </> "agda2.el"-  hSetEncoding stdout utf8-  putStr path----------------------------------------------------------------------------- Setting up the .emacs file--data Files = Files { dotEmacs :: FilePath-                     -- ^ The .emacs file.-                   , thisProgram :: FilePath-                     -- ^ The name of the current program.-                   }---- | Tries to set up the Agda mode in the given .emacs file.--setupDotEmacs :: Files -> IO ()-setupDotEmacs files = do-  informLn $ "The .emacs file used: " ++ dotEmacs files--  already <- alreadyInstalled files-  if already then-    informLn "It seems as if setup has already been performed."-   else do--    appendFile (dotEmacs files) (setupString files)-    inform $ unlines $-      [ "Setup done. Try to (re)start Emacs and open an Agda file."-      , "The following text was appended to the .emacs file:"-      ] ++ lines (setupString files)---- | Tries to find the user's .emacs file by querying Emacs.--findDotEmacs :: IO FilePath-findDotEmacs = askEmacs "(expand-file-name user-init-file)"---- | Has the Agda mode already been set up?--alreadyInstalled :: Files -> IO Bool-alreadyInstalled files = do-  exists <- doesFileExist (dotEmacs files)-  if not exists then return False else-    withFile (dotEmacs files) ReadMode $ (evaluate . (identifier files `isInfixOf`)) <=< hGetContents-      -- Uses evaluate to ensure that the file is not closed-      -- prematurely.---- | If this string occurs in the .emacs file, then it is assumed that--- setup has already been performed.--identifier :: Files -> String-identifier files =-  takeFileName (thisProgram files) ++ " " ++ locateFlag---- | The string appended to the end of the .emacs file.--setupString :: Files -> String-setupString files = unlines-  [ ""-  , "(setenv \"PATH\" (concat (getenv \"PATH\") \":~/.cabal/bin\"))"-  , "(setq exec-path (append exec-path '(\"~/.cabal/bin\")))"- -- ^ We append ~/.cabal/bin to PATH, since it's the default installation path when using `cabal new-install`.-  , ""-  , "(load-file (let ((coding-system-for-read 'utf-8))"-  , "                (shell-command-to-string \""-                        ++ identifier files ++ "\")))"-  ]----------------------------------------------------------------------------- Querying Emacs---- | Evaluates the given Elisp command using Emacs. The output of the--- command (whatever was written into the current buffer) is returned.------ Note: The input is not checked. The input is assumed to come from a--- trusted source.--askEmacs :: String -> IO String-askEmacs query = do-  tempDir <- getTemporaryDirectory-  bracket (openTempFile tempDir "askEmacs")-          (removeFile . fst) $ \(file, h) -> do-    hClose h-    exit <- rawSystemWithDiagnostics "emacs"-      [ "--batch"-          -- Andreas, 2022-10-15, issue #5901, suggested by Spencer Baugh (catern):-          -- Use Emacs batch mode so that it can run without a terminal.-      , "--user", ""-          -- The flag --user is necessary with --batch so that user-init-file is defined.-          -- The empty user is the default user.-          -- (Option --batch includes --no-init-file, this is reverted by supplying --user.)-      -- Andreas, 2022-05-25, issue #5901 reloaded:-      -- Loading the init file without loading the site fails for some users:-      -- , "--quick"-      --     -- Option --quick includes --no-site-file.-      , "--eval"-      , apply [ "with-temp-file", escape file, apply [ "insert", query ] ]-          -- Short cutting the temp file via just [ "princ", query ]-          -- does not work if the loading of the user-init-file prints extra stuff.-          -- Going via the temp file we can let this stuff go to stdout without-          -- affecting the output we care about.-      ]-    unless (exit == ExitSuccess) $ do-      informLn "Unable to query Emacs."-      exitFailure-    withFile file ReadMode $ \h -> do-      result <- hGetContents h-      evaluate (length result)-      -- Uses evaluate to ensure that the file is not closed-      -- prematurely.-      return result---- | Like 'rawSystem' but handles 'IOException' by printing diagnostics--- (@PATH@) before 'exitFailure'.--rawSystemWithDiagnostics-  :: FilePath  -- ^ Command to run.-  -> [String]  -- ^ Arguments to command.-  -> IO ExitCode-rawSystemWithDiagnostics cmd args =-    rawSystem cmd args-  `E.catch` \ (e :: IOException) -> do-     informLn $ unwords [ "FAILED:", showCommandForUser cmd args ]-     informLn $ unwords [ "Exception:", show e ]-     -- The PATH might be useful in other exceptions, like "permission denied".-     -- when (isDoesNotExistError e) $ do-     path <- fromMaybe "(not found)" <$> findExecutable cmd-     informLn $ unwords [ "Executable", cmd, "at:", path ]-     informLn "PATH:"-     mapM_ (informLn . ("  - " ++)) =<< getSearchPath-     exitFailure---- | Escapes the string so that Emacs can parse it as an Elisp string.--escape :: FilePath -> FilePath-escape s = "\"" ++ concatMap esc s ++ "\""-  where-  esc c | c `elem` ['\\', '"']   = '\\' : [c]-        | isAscii c && isPrint c = [c]-        | otherwise              = "\\x" ++ showHex (fromEnum c) "\\ "----------------------------------------------------------------------------- Compiling Emacs Lisp files---- | The Agda mode's Emacs Lisp files, given in the order in which--- they should be compiled.--emacsLispFiles :: [FilePath]-emacsLispFiles =-  [ "agda2-abbrevs.el"-  , "annotation.el"-  , "agda2-queue.el"-  , "eri.el"-  , "agda2.el"-  , "agda-input.el"-  , "agda2-highlight.el"-  , "agda2-mode.el"-  ]---- | Tries to compile the Agda mode's Emacs Lisp files.--compileElispFiles :: IO ()-compileElispFiles = do-  dataDir <- (</> "emacs-mode") <$> getDataDir-  let elFiles = map (dataDir </>) emacsLispFiles-  elFiles <- filterM doesFileExist elFiles-  results <- mapM (compile dataDir) elFiles-  case catMaybes results of-    [] -> return ()-    fs -> do-      informLn "Unable to compile the following Emacs Lisp files:"-      mapM_ (informLn . ("  " ++)) fs-      exitFailure-  where-  compile dataDir f = do-    exit <- rawSystemWithDiagnostics "emacs" $-      [ "--quick"                -- 'quick' implies 'no-site-file'-      , "--directory", dataDir-      , "--batch"                -- 'batch' implies 'no-init-file' but not 'no-site-file'.-      , "--eval"-      , "(progn \-           \(setq byte-compile-error-on-warn t) \-           \(byte-compile-disable-warning 'cl-functions) \-           \(batch-byte-compile))"-      , f-      ]-    return $ if exit == ExitSuccess then Nothing else Just f----------------------------------------------------------------------------- Helper functions---- These functions inform the user about something by printing on--- stderr.--inform   = hPutStr   stderr-informLn = hPutStrLn stderr--parens :: String -> String-parens s = concat [ "(", s, ")" ]---- LISP application-apply :: [String] -> String-apply = parens . unwords

@@ -1,1445 +0,0 @@-;;; -*- lexical-binding: t; -*--;;; agda-input.el --- The Agda input method--;; SPDX-License-Identifier: MIT License-;;; Commentary:--;; A highly customisable input method which can inherit from other-;; Quail input methods. By default the input method is geared towards-;; the input of mathematical and other symbols in Agda programs.-;;-;; Use M-x customize-group agda-input to customise this input method.-;; Note that the functions defined under "Functions used to tweak-;; translation pairs" below can be used to tweak both the key-;; translations inherited from other input methods as well as the-;; ones added specifically for this one.-;;-;; Use agda-input-show-translations to see all the characters which-;; can be typed using this input method (except for those-;; corresponding to ASCII characters).--;;; Code:--(require 'quail)-(require 'cl-lib)-;; Quail is quite stateful, so be careful when editing this code.  Note-;; that with-temp-buffer is used below whenever buffer-local state is-;; modified.--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Utility functions--(defun agda-input-concat-map (f xs)-  "Concat (map F XS)."-  (apply 'append (mapcar f xs)))--(defun agda-input-to-string-list (s)-  "Convert a string S to a list of one-character strings, after-removing all space and newline characters."-  (agda-input-concat-map-   (lambda (c) (if (member c (string-to-list " \n"))-              nil-            (list (string c))))-   (string-to-list s)))--(defun agda-input-character-range (from to)-  "A string consisting of the characters from FROM to TO."-  (let (seq)-    (dotimes (i (1+ (- to from)))-      (setq seq (cons (+ from i) seq)))-    (concat (nreverse seq))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Functions used to tweak translation pairs--(defun agda-input-compose (f g)-  "λ x -> concatMap F (G x)"-    (lambda (x) (agda-input-concat-map f (funcall g x))))--(defun agda-input-or (f g)-  "λ x -> F x ++ G x"-    (lambda (x) (append (funcall f x) (funcall g x))))--(defun agda-input-nonempty ()-  "Only keep pairs with a non-empty first component."-  (lambda (x) (if (> (length (car x)) 0) (list x))))--(defun agda-input-prepend (prefix)-  "Prepend PREFIX to all key sequences."-    (lambda (x) `((,(concat prefix (car x)) . ,(cdr x)))))--(defun agda-input-prefix (prefix)-  "Only keep pairs whose key sequence starts with PREFIX."-    (lambda (x)-      (if (equal (substring (car x) 0 (length prefix)) prefix)-          (list x))))--(defun agda-input-suffix (suffix)-  "Only keep pairs whose key sequence ends with SUFFIX."-    (lambda (x)-      (if (equal (substring (car x)-                            (- (length (car x)) (length suffix)))-                 suffix)-          (list x))))--(defun agda-input-drop (ss)-  "Drop pairs matching one of the given key sequences.-SS should be a list of strings."-    (lambda (x) (unless (member (car x) ss) (list x))))--(defun agda-input-drop-beginning (n)-  "Drop N characters from the beginning of each key sequence."-    (lambda (x) `((,(substring (car x) n) . ,(cdr x)))))--(defun agda-input-drop-end (n)-  "Drop N characters from the end of each key sequence."-    (lambda (x)-      `((,(substring (car x) 0 (- (length (car x)) n)) .-         ,(cdr x)))))--(defun agda-input-drop-prefix (prefix)-  "Only keep pairs whose key sequence starts with PREFIX.-This prefix is dropped."-  (agda-input-compose-   (agda-input-drop-beginning (length prefix))-   (agda-input-prefix prefix)))--(defun agda-input-drop-suffix (suffix)-  "Only keep pairs whose key sequence ends with SUFFIX.-This suffix is dropped."-    (agda-input-compose-     (agda-input-drop-end (length suffix))-     (agda-input-suffix suffix)))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Customization--;; The :set keyword is set to 'agda-input-incorporate-changed-setting-;; so that the input method gets updated immediately when users-;; customize it. However, the setup functions cannot be run before all-;; variables have been defined. Hence the :initialize keyword is set to-;; 'custom-initialize-default to ensure that the setup is not performed-;; until agda-input-setup is called at the end of this file.--(defgroup agda-input nil-  "The Agda input method.-After tweaking these settings you may want to inspect the resulting-translations using `agda-input-show-translations'."-  :group 'agda2-  :group 'leim)--(defcustom agda-input-tweak-all-  '(agda-input-compose-    (agda-input-prepend "\\")-    (agda-input-nonempty))-  "An expression yielding a function which can be used to tweak-all translations before they are included in the input method.-The resulting function (if non-nil) is applied to every-\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of such-pairs. (Note that the translations can be anything accepted by-`quail-defrule'.)--If you change this setting manually (without using the-customization buffer) you need to call `agda-input-setup' in-order for the change to take effect."-  :group 'agda-input-  :set 'agda-input-incorporate-changed-setting-  :initialize 'custom-initialize-default-  :type 'sexp)--(defcustom agda-input-inherit-  `(("TeX" . (agda-input-compose-              (agda-input-drop '("geq" "leq" "bullet" "qed" "par"))-              (agda-input-or-               (agda-input-drop-prefix "\\")-               (agda-input-or-                (agda-input-compose-                 (agda-input-drop '("^l" "^o" "^r" "^v"))-                 (agda-input-prefix "^"))-                (agda-input-prefix "_")))))-    )-  "A list of Quail input methods whose translations should be-inherited by the Agda input method (with the exception of-translations corresponding to ASCII characters).--The list consists of pairs (qp . tweak), where qp is the name of-a Quail package, and tweak is an expression of the same kind as-`agda-input-tweak-all' which is used to tweak the translation-pairs of the input method.--The inherited translation pairs are added last, after-`agda-input-user-translations' and `agda-input-translations'.--If you change this setting manually (without using the-customization buffer) you need to call `agda-input-setup' in-order for the change to take effect."-  :group 'agda-input-  :set 'agda-input-incorporate-changed-setting-  :initialize 'custom-initialize-default-  :type '(repeat (cons (string :tag "Quail package")-                       (sexp :tag "Tweaking function"))))--(defcustom agda-input-translations-  (let ((max-lisp-eval-depth 2800)) `(--  ;; Equality and similar symbols.--  ("eq"  . ,(agda-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕＝"))-  ("eqn" . ,(agda-input-to-string-list "≠≁ ≉     ≄  ≇≆  ≢                 ≭    "))--                    ("=n"  . ("≠"))-  ("~"    . ,(agda-input-to-string-list "∼～"))-                    ("~n"  . ("≁"))-  ("~~"   . ("≈"))  ("~~n" . ("≉"))-  ("~~~"  . ("≋"))-  (":~"   . ("∻"))-  ("~-"   . ("≃"))  ("~-n" . ("≄"))-  ("-~"   . ("≂"))-  ("~="   . ("≅"))  ("~=n" . ("≇"))-  ("~~-"  . ("≊"))-  ("=="   . ("≡"))  ("==n" . ("≢"))-  ("==="  . ("≣"))-  ("="    . ("＝"))-  (".="   . ("≐"))  (".=." . ("≑"))-  (":="   . ("≔"))  ("=:"  . ("≕"))-  ("=o"   . ("≗"))-  ("(="   . ("≘"))-  ("and=" . ("≙"))  ("or=" . ("≚"))-  ("*="   . ("≛"))-  ("t="   . ("≜"))-  ("def=" . ("≝"))-  ("m="   . ("≞"))-  ("?="   . ("≟"))--  ;; Inequality and similar symbols.--  ("leq"  . ,(agda-input-to-string-list "<≪⋘≤≦≲ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞＜"))-  ("leqn" . ,(agda-input-to-string-list "≮  ≰≨≴⋦≸⊀ ⋨⊄⊈⊊  ⋢⋤ ⋪⋬   ⋠"))-  ("geq"  . ,(agda-input-to-string-list ">≫⋙≥≧≳ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟＞"))-  ("geqn" . ,(agda-input-to-string-list "≯  ≱≩≵⋧≹⊁ ⋩⊅⊉⊋  ⋣⋥ ⋫⋭   ⋡"))--  ("<="   . ("≤"))  (">="   . ("≥"))-  ("<=n"  . ("≰"))  (">=n"  . ("≱"))-  ("len"  . ("≰"))  ("gen"  . ("≱"))-  ("<n"   . ("≮"))  (">n"   . ("≯"))-  ("<~"   . ("≲"))  (">~"   . ("≳"))-  ("<~n"  . ("⋦"))  (">~n"  . ("⋧"))-  ("<~nn" . ("≴"))  (">~nn" . ("≵"))--  ("sub"   . ("⊂"))  ("sup"   . ("⊃"))-  ("subn"  . ("⊄"))  ("supn"  . ("⊅"))-  ("sub="  . ("⊆"))  ("sup="  . ("⊇"))-  ("sub=n" . ("⊈"))  ("sup=n" . ("⊉"))--  ("squb"   . ("⊏"))  ("squp"   . ("⊐"))-  ("squb="  . ("⊑"))  ("squp="  . ("⊒"))-  ("squb=n" . ("⋢"))  ("squp=n" . ("⋣"))--  ;; Set membership etc.--  ("member" . ,(agda-input-to-string-list "∈∉∊∋∌∍⋲⋳⋴⋵⋶⋷⋸⋹⋺⋻⋼⋽⋾⋿"))--  ("inn" . ("∉"))-  ("nin" . ("∌"))--  ;; Intersections, unions etc.--  ("intersection" . ,(agda-input-to-string-list "∩⋂∧⋀⋏⨇⊓⨅⋒∏ ⊼      ⨉"))-  ("union"        . ,(agda-input-to-string-list "∪⋃∨⋁⋎⨈⊔⨆⋓∐⨿⊽⊻⊍⨃⊎⨄⊌∑⅀"))--  ("and" . ("∧"))  ("or"  . ("∨"))-  ("And" . ("⋀"))  ("Or"  . ("⋁"))-  ("i"   . ("∩"))  ("un"  . ("∪"))  ("u+" . ("⊎"))  ("u." . ("⊍"))-  ("I"   . ("⋂"))  ("Un"  . ("⋃"))  ("U+" . ("⨄"))  ("U." . ("⨃"))-  ("glb" . ("⊓"))  ("lub" . ("⊔"))-  ("Glb" . ("⨅"))  ("Lub" . ("⨆"))--  ;; Entailment etc.--  ("entails" . ,(agda-input-to-string-list "⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯"))--  ("|-"   . ("⊢"))  ("|-n"  . ("⊬"))-  ("-|"   . ("⊣"))-  ("|="   . ("⊨"))  ("|=n"  . ("⊭"))-  ("||-"  . ("⊩"))  ("||-n" . ("⊮"))-  ("||="  . ("⊫"))  ("||=n" . ("⊯"))-  ("|||-" . ("⊪"))--  ;; Divisibility, parallelity.--  ("|"  . ("∣"))  ("|n"  . ("∤"))-  ("||" . ("∥"))  ("||n" . ("∦"))--  ;; Some symbols from logic and set theory.--  ("all" . ("∀"))-  ("ex"  . ("∃"))-  ("exn" . ("∄"))-  ("0"   . ("∅"))-  ("C"   . ("∁"))--  ;; Corners, ceilings and floors.--  ("c"  . ,(agda-input-to-string-list "⌜⌝⌞⌟⌈⌉⌊⌋"))-  ("cu" . ,(agda-input-to-string-list "⌜⌝  ⌈⌉  "))-  ("cl" . ,(agda-input-to-string-list "  ⌞⌟  ⌊⌋"))--  ("cul" . ("⌜"))  ("cuL" . ("⌈"))-  ("cur" . ("⌝"))  ("cuR" . ("⌉"))-  ("cll" . ("⌞"))  ("clL" . ("⌊"))-  ("clr" . ("⌟"))  ("clR" . ("⌋"))--  ;; Various operators/symbols.--  ("qed"       . ("∎"))-  ("x"         . ("×"))-  ("o"         . ("∘"))-  ("comp"      . ("∘"))-  ("."         . ,(agda-input-to-string-list "∙．"))-  ("*"         . ("⋆"))-  (".+"        . ("∔"))-  (".-"        . ("∸"))-  (":"         . ,(agda-input-to-string-list "∶⦂ː꞉˸፥፦：﹕︓"))-  (","         . ,(agda-input-to-string-list "ʻ،⸲⸴⹁⹉、︐︑﹐﹑，､"))-  (";"         . ,(agda-input-to-string-list "⨾⨟⁏፤꛶；︔﹔⍮⸵;"))-  ("::"        . ("∷"))-  ("::-"       . ("∺"))-  ("-:"        . ("∹"))-  ("+ "        . ("⊹"))-  ("+"         . ("＋"))-  ("sqrt"      . ("√"))-  ("surd3"     . ("∛"))-  ("surd4"     . ("∜"))-  ("increment" . ("∆"))-  ("inf"       . ("∞"))-  ("&"         . ("⅋"))-  ("z;"        . ,(agda-input-to-string-list "⨟⨾"))-  ("z:"        . ("⦂"))--  ;; Circled operators.--  ("o+"  . ("⊕"))-  ("o--" . ("⊖"))-  ("ox"  . ("⊗"))-  ("o/"  . ("⊘"))-  ("o."  . ("⊙"))-  ("oo"  . ("⊚"))-  ("o*"  . ("⊛"))-  ("o="  . ("⊜"))-  ("o-"  . ("⊝"))--  ("O+"  . ("⨁"))-  ("Ox"  . ("⨂"))-  ("O."  . ("⨀"))-  ("O*"  . ("⍟"))--  ;; Boxed operators.--  ("b+" . ("⊞"))-  ("b-" . ("⊟"))-  ("bx" . ("⊠"))-  ("b." . ("⊡"))--  ;; APL boxed operators--  ("box="       . ("⌸"))-  ("box?"       . ("⍰"))-  ("box'"       . ("⍞"))-  ("box:"       . ("⍠"))-  ("box/"       . ("⍁"))-  ("box\\"      . ("⍂"))-  ("box<"       . ("⍃"))-  ("box>"       . ("⍄"))-  ("boxo"       . ("⌻"))-  ("boxO"       . ("⌼"))--  ("boxcomp"    . ("⌻"))-  ("boxcircle"  . ("⌼"))-  ("boxeq"      . ("⌸"))-  ("boxneq"     . ("⍯"))-  ("boxeqn"     . ("⍯"))--  ("boxl"       . ("⍇"))-  ("boxr"       . ("⍈"))-  ("boxu"       . ("⍐"))-  ("boxd"       . ("⍗"))--  ("boxdi"      . ("⌺"))-  ("boxdiv"     . ("⌹"))-  ("boxwedge"   . ("⍓"))-  ("boxvee"     . ("⍌"))-  ("boxdelta"   . ("⍍"))-  ("boxnabla"   . ("⍔"))--  ;; Various symbols.--  ("integral" . ,(agda-input-to-string-list "∫∬∭∮∯∰∱∲∳"))-  ("angle"    . ,(agda-input-to-string-list "∟∡∢⊾⊿"))-  ("join"     . ,(agda-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗"))--  ;; Arrows.--  ("l"  . ,(agda-input-to-string-list "←⇐⇚⭅⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹     ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲                                     "))-  ("r"  . ,(agda-input-to-string-list "→⇒⇛⭆⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴    ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾⊸"))-  ("u"  . ,(agda-input-to-string-list "↑⇑⤊⟰⇈⇅↥⇧↟↿↾⇡⇞          ↰↱➦ ⇪⇫⇬⇭⇮⇯                                           "))-  ("d"  . ,(agda-input-to-string-list "↓⇓⤋⟱⇊⇵↧⇩↡⇃⇂⇣⇟         ↵↲↳➥ ↯                                                "))-  ("ud" . ,(agda-input-to-string-list "↕⇕   ↨⇳                                                                    "))-  ("lr" . ,(agda-input-to-string-list "↔⇔         ⇼↭⇿⟷⟺↮⇎⇹                                                        "))-  ("ul" . ,(agda-input-to-string-list "↖⇖                        ⇱↸                                               "))-  ("ur" . ,(agda-input-to-string-list "↗⇗                                         ➶➹➚                             "))-  ("dr" . ,(agda-input-to-string-list "↘⇘                        ⇲                ➴➷➘                             "))-  ("dl" . ,(agda-input-to-string-list "↙⇙                                                                         "))--  ("l-"  . ("←"))  ("<-"  . ("←"))  ("l="  . ("⇐"))  ("<="  . ("⇐"))-  ("r-"  . ("→"))  ("->"  . ("→"))  ("r="  . ("⇒"))  ("=>"  . ("⇒"))-  ("u-"  . ("↑"))                   ("u="  . ("⇑"))-  ("d-"  . ("↓"))                   ("d="  . ("⇓"))-  ("ud-" . ("↕"))                   ("ud=" . ("⇕"))-  ("lr-" . ("↔"))  ("<->" . ("↔"))  ("lr=" . ("⇔"))  ("<=>" . ("⇔"))-  ("ul-" . ("↖"))                   ("ul=" . ("⇖"))-  ("ur-" . ("↗"))                   ("ur=" . ("⇗"))-  ("dr-" . ("↘"))                   ("dr=" . ("⇘"))-  ("dl-" . ("↙"))                   ("dl=" . ("⇙"))--  ("l==" . ("⇚"))  ("l-2" . ("⇇"))                   ("l-r-" . ("⇆"))-  ("r==" . ("⇛"))  ("r-2" . ("⇉"))  ("r-3" . ("⇶"))  ("r-l-" . ("⇄"))-  ("u==" . ("⟰"))  ("u-2" . ("⇈"))                   ("u-d-" . ("⇅"))-  ("d==" . ("⟱"))  ("d-2" . ("⇊"))                   ("d-u-" . ("⇵"))--  ("l--"  . ("⟵"))  ("<--"  . ("⟵"))  ("l~"  . ("↜" "⇜"))-  ("r--"  . ("⟶"))  ("-->"  . ("⟶"))  ("r~"  . ("↝" "⇝" "⟿"))-  ("lr--" . ("⟷"))  ("<-->" . ("⟷"))  ("lr~" . ("↭"))--  ("l-n"  . ("↚"))  ("<-n"  . ("↚"))  ("l=n"  . ("⇍"))-  ("r-n"  . ("↛"))  ("->n"  . ("↛"))  ("r=n"  . ("⇏"))  ("=>n"  . ("⇏"))-  ("lr-n" . ("↮"))  ("<->n" . ("↮"))  ("lr=n" . ("⇎"))  ("<=>n" . ("⇎"))--  ("l-|"  . ("↤"))  ("ll-" . ("↞"))-  ("r-|"  . ("↦"))  ("rr-" . ("↠"))-  ("u-|"  . ("↥"))  ("uu-" . ("↟"))-  ("d-|"  . ("↧"))  ("dd-" . ("↡"))-  ("ud-|" . ("↨"))--  ("l->" . ("↢"))-  ("r->" . ("↣"))--  ("r-o" . ("⊸"))  ("-o"  . ("⊸"))--  ("dz" . ("↯"))--  ;; Ellipsis.--  ("..." . ,(agda-input-to-string-list "⋯⋮⋰⋱"))--  ;; Box-drawing characters.--  ("---" . ,(agda-input-to-string-list "─│┌┐└┘├┤┬┼┴╴╵╶╷╭╮╯╰╱╲╳"))-  ("--=" . ,(agda-input-to-string-list "═║╔╗╚╝╠╣╦╬╩     ╒╕╘╛╞╡╤╪╧ ╓╖╙╜╟╢╥╫╨"))-  ("--_" . ,(agda-input-to-string-list "━┃┏┓┗┛┣┫┳╋┻╸╹╺╻-                                        ┍┯┑┕┷┙┝┿┥┎┰┒┖┸┚┠╂┨┞╀┦┟╁┧┢╈┪┡╇┩-                                        ┮┭┶┵┾┽┲┱┺┹╊╉╆╅╄╃ ╿╽╼╾"))-  ("--." . ,(agda-input-to-string-list "╌╎┄┆┈┊-                                        ╍╏┅┇┉┋"))--  ;; Triangles.--  ;; Big/small, black/white.--  ("t" . ,(agda-input-to-string-list "◂◃◄◅▸▹►▻▴▵▾▿◢◿◣◺◤◸◥◹"))-  ("T" . ,(agda-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮"))--  ("tb" . ,(agda-input-to-string-list "◂▸▴▾◄►◢◣◤◥"))-  ("tw" . ,(agda-input-to-string-list "◃▹▵▿◅▻◿◺◸◹"))--  ("Tb" . ,(agda-input-to-string-list "◀▶▲▼"))-  ("Tw" . ,(agda-input-to-string-list "◁▷△▽"))--  ;; Squares.--  ("sq"  . ,(agda-input-to-string-list "■□◼◻◾◽▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳"))-  ("sqb" . ,(agda-input-to-string-list "■◼◾"))-  ("sqw" . ,(agda-input-to-string-list "□◻◽"))-  ("sq." . ("▣"))-  ("sqo" . ("▢"))--  ;; Rectangles.--  ("re"  . ,(agda-input-to-string-list "▬▭▮▯"))-  ("reb" . ,(agda-input-to-string-list "▬▮"))-  ("rew" . ,(agda-input-to-string-list "▭▯"))--  ;; Parallelograms.--  ("pa"  . ,(agda-input-to-string-list "▰▱"))-  ("pab" . ("▰"))-  ("paw" . ("▱"))--  ;; Diamonds.--  ("di"  . ,(agda-input-to-string-list "◆◇◈"))-  ("dib" . ("◆"))-  ("diw" . ("◇"))-  ("di." . ("◈"))--  ;; Circles.--  ("ci"   . ,(agda-input-to-string-list "●○◎◌◯◍◐◑◒◓◔◕◖◗◠◡◴◵◶◷⚆⚇⚈⚉"))-  ("cib"  . ("●"))-  ("ciw"  . ("○"))-  ("ci."  . ("◎"))-  ("ci.." . ("◌"))-  ("ciO"  . ("◯"))--  ;; Stars.--  ("st"   . ,(agda-input-to-string-list "⋆✦✧✶✴✹ ★☆✪✫✯✰✵✷✸"))-  ("st4"  . ,(agda-input-to-string-list "✦✧"))-  ("st6"  . ("✶"))-  ("st8"  . ("✴"))-  ("st12" . ("✹"))--  ;; Blackboard bold letters.--  ("bA"   . ("𝔸"))-  ("bB"   . ("𝔹"))-  ("bC"   . ("ℂ"))-  ("bD"   . ("𝔻"))-  ("bE"   . ("𝔼"))-  ("bF"   . ("𝔽"))-  ("bG"   . ("𝔾"))-  ("bH"   . ("ℍ"))-  ("bI"   . ("𝕀"))-  ("bJ"   . ("𝕁"))-  ("bK"   . ("𝕂"))-  ("bL"   . ("𝕃"))-  ("bM"   . ("𝕄"))-  ("bN"   . ("ℕ"))-  ("bO"   . ("𝕆"))-  ("bP"   . ("ℙ"))-  ("bQ"   . ("ℚ"))-  ("bR"   . ("ℝ"))-  ("bS"   . ("𝕊"))-  ("bT"   . ("𝕋"))-  ("bU"   . ("𝕌"))-  ("bV"   . ("𝕍"))-  ("bW"   . ("𝕎"))-  ("bX"   . ("𝕏"))-  ("bY"   . ("𝕐"))-  ("bZ"   . ("ℤ"))-  ("bGG"  . ("ℾ"))-  ("bGP"  . ("ℿ"))-  ("bGS"  . ("⅀"))-  ("ba"   . ("𝕒"))-  ("bb"   . ("𝕓"))-  ("bc"   . ("𝕔"))-  ("bd"   . ("𝕕"))-  ("be"   . ("𝕖"))-  ("bf"   . ("𝕗"))-  ("bg"   . ("𝕘"))-  ("bh"   . ("𝕙"))-  ("bi"   . ("𝕚"))-  ("bj"   . ("𝕛"))-  ("bk"   . ("𝕜"))-  ("bl"   . ("𝕝"))-  ("bm"   . ("𝕞"))-  ("bn"   . ("𝕟"))-  ("bo"   . ("𝕠"))-  ("bp"   . ("𝕡"))-  ("bq"   . ("𝕢"))-  ("br"   . ("𝕣"))-  ("bs"   . ("𝕤"))-  ("bt"   . ("𝕥"))-  ("bu"   . ("𝕦"))-  ("bv"   . ("𝕧"))-  ("bw"   . ("𝕨"))-  ("bx"   . ("𝕩"))-  ("by"   . ("𝕪"))-  ("bz"   . ("𝕫"))-  ("bGg"  . ("ℽ"))-  ("bGp"  . ("ℼ"))--  ;; Blackboard bold numbers.--  ("b0"   . ("𝟘"))-  ("b1"   . ("𝟙"))-  ("b2"   . ("𝟚"))-  ("b3"   . ("𝟛"))-  ("b4"   . ("𝟜"))-  ("b5"   . ("𝟝"))-  ("b6"   . ("𝟞"))-  ("b7"   . ("𝟟"))-  ("b8"   . ("𝟠"))-  ("b9"   . ("𝟡"))--  ;; Mathematical bold letters.--  ("BA"   . ("𝐀"))-  ("BB"   . ("𝐁"))-  ("BC"   . ("𝐂"))-  ("BD"   . ("𝐃"))-  ("BE"   . ("𝐄"))-  ("BF"   . ("𝐅"))-  ("BG"   . ("𝐆"))-  ("BH"   . ("𝐇"))-  ("BI"   . ("𝐈"))-  ("BJ"   . ("𝐉"))-  ("BK"   . ("𝐊"))-  ("BL"   . ("𝐋"))-  ("BM"   . ("𝐌"))-  ("BN"   . ("𝐍"))-  ("BO"   . ("𝐎"))-  ("BP"   . ("𝐏"))-  ("BQ"   . ("𝐐"))-  ("BR"   . ("𝐑"))-  ("BS"   . ("𝐒"))-  ("BT"   . ("𝐓"))-  ("BU"   . ("𝐔"))-  ("BV"   . ("𝐕"))-  ("BW"   . ("𝐖"))-  ("BX"   . ("𝐗"))-  ("BY"   . ("𝐘"))-  ("BZ"   . ("𝐙"))-  ("Ba"   . ("𝐚"))-  ("Bb"   . ("𝐛"))-  ("Bc"   . ("𝐜"))-  ("Bd"   . ("𝐝"))-  ("Be"   . ("𝐞"))-  ("Bf"   . ("𝐟"))-  ("Bg"   . ("𝐠"))-  ("Bh"   . ("𝐡"))-  ("Bi"   . ("𝐢"))-  ("Bj"   . ("𝐣"))-  ("Bk"   . ("𝐤"))-  ("Bl"   . ("𝐥"))-  ("Bm"   . ("𝐦"))-  ("Bn"   . ("𝐧"))-  ("Bo"   . ("𝐨"))-  ("Bp"   . ("𝐩"))-  ("Bq"   . ("𝐪"))-  ("Br"   . ("𝐫"))-  ("Bs"   . ("𝐬"))-  ("Bt"   . ("𝐭"))-  ("Bu"   . ("𝐮"))-  ("Bv"   . ("𝐯"))-  ("Bw"   . ("𝐰"))-  ("Bx"   . ("𝐱"))-  ("By"   . ("𝐲"))-  ("Bz"   . ("𝐳"))--  ;; Mathematical bold Greek letters.--  ("BGA"  . ("𝚨"))-  ("BGB"  . ("𝚩"))-  ("BGC"  . ("𝚾"))-  ("BGD"  . ("𝚫"))-  ("BGE"  . ("𝚬"))-  ("BGG"  . ("𝚪"))-  ("BGH"  . ("𝚮"))-  ("BGI"  . ("𝚰"))-  ("BGK"  . ("𝚱"))-  ("BGL"  . ("𝚲"))-  ("BGM"  . ("𝚳"))-  ("BGN"  . ("𝚴"))-  ("BGO"  . ("𝛀"))-  ("BOmicron" . ("𝚶"))-  ("BGF"  . ("𝚽"))-  ("BPi"  . ("𝚷"))-  ("BGP"  . ("𝚿"))-  ("BGR"  . ("𝚸"))-  ("BGS"  . ("𝚺"))-  ("BGT"  . ("𝚻"))-  ("BGTH" . ("𝚯"))-  ("BGU"  . ("𝚼"))-  ("BGX"  . ("𝚵"))-  ("BGZ"  . ("𝚭"))-  ("BGa"  . ("𝛂"))-  ("BGb"  . ("𝛃"))-  ("BGc"  . ("𝛘"))-  ("BGd"  . ("𝛅"))-  ("BGe"  . ("𝛆"))-  ("BGg"  . ("𝛄"))-  ("BGh"  . ("𝛈"))-  ("BGi"  . ("𝛊"))-  ("BGk"  . ("𝛋"))-  ("BGl"  . ("𝛌"))-  ("BGm"  . ("𝛍"))-  ("BGn"  . ("𝛎"))-  ("BGo"  . ("𝛚"))-  ("Bomicron" . ("𝛐"))-  ("BGf"  . ("𝛗"))-  ("Bpi"  . ("𝛑"))-  ("BGp"  . ("𝛙"))-  ("BGr"  . ("𝛒"))-  ("BGs"  . ("𝛔"))-  ("BGt"  . ("𝛕"))-  ("BGth" . ("𝛉"))-  ("BGu"  . ("𝛖"))-  ("BGx"  . ("𝛏"))-  ("BGz"  . ("𝛇"))--  ;; Mathematical bold digits.--  ("B0"   . ("𝟎"))-  ("B1"   . ("𝟏"))-  ("B2"   . ("𝟐"))-  ("B3"   . ("𝟑"))-  ("B4"   . ("𝟒"))-  ("B5"   . ("𝟓"))-  ("B6"   . ("𝟔"))-  ("B7"   . ("𝟕"))-  ("B8"   . ("𝟖"))-  ("B9"   . ("𝟗"))--  ;; Fullwidth letters--  ("FA"   . ("Ａ"))-  ("FB"   . ("Ｂ"))-  ("FC"   . ("Ｃ"))-  ("FD"   . ("Ｄ"))-  ("FE"   . ("Ｅ"))-  ("FF"   . ("Ｆ"))-  ("FG"   . ("Ｇ"))-  ("FH"   . ("Ｈ"))-  ("FI"   . ("Ｉ"))-  ("FJ"   . ("Ｊ"))-  ("FK"   . ("Ｋ"))-  ("FL"   . ("Ｌ"))-  ("FM"   . ("Ｍ"))-  ("FN"   . ("Ｎ"))-  ("FO"   . ("Ｏ"))-  ("FP"   . ("Ｐ"))-  ("FQ"   . ("Ｑ"))-  ("FR"   . ("Ｒ"))-  ("FS"   . ("Ｓ"))-  ("FT"   . ("Ｔ"))-  ("FU"   . ("Ｕ"))-  ("FV"   . ("Ｖ"))-  ("FW"   . ("Ｗ"))-  ("FX"   . ("Ｘ"))-  ("FY"   . ("Ｙ"))-  ("FZ"   . ("Ｚ"))-  ("Fa"   . ("ａ"))-  ("Fb"   . ("ｂ"))-  ("Fc"   . ("ｃ"))-  ("Fd"   . ("ｄ"))-  ("Fe"   . ("ｅ"))-  ("Ff"   . ("ｆ"))-  ("Fg"   . ("ｇ"))-  ("Fh"   . ("ｈ"))-  ("Fi"   . ("ｉ"))-  ("Fj"   . ("ｊ"))-  ("Fk"   . ("ｋ"))-  ("Fl"   . ("ｌ"))-  ("Fm"   . ("ｍ"))-  ("Fn"   . ("ｎ"))-  ("Fo"   . ("ｏ"))-  ("Fp"   . ("ｐ"))-  ("Fq"   . ("ｑ"))-  ("Fr"   . ("ｒ"))-  ("Fs"   . ("ｓ"))-  ("Ft"   . ("ｔ"))-  ("Fu"   . ("ｕ"))-  ("Fv"   . ("ｖ"))-  ("Fw"   . ("ｗ"))-  ("Fx"   . ("ｘ"))-  ("Fy"   . ("ｙ"))-  ("Fz"   . ("ｚ"))--  ;; Fullwidth digits--  ("F0"   . ("０"))-  ("F1"   . ("１"))-  ("F2"   . ("２"))-  ("F3"   . ("３"))-  ("F4"   . ("４"))-  ("F5"   . ("５"))-  ("F6"   . ("６"))-  ("F7"   . ("７"))-  ("F8"   . ("８"))-  ("F9"   . ("９"))--  ;; Parentheses.--  ("(" . ,(agda-input-to-string-list "([{⁅⁽₍〈⎴⟅⟦⟨⟪⦃〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢❪❬❰❲❴⟮⦅⦗⧼⸨❮⦇⦉"))-  (")" . ,(agda-input-to-string-list ")]}⁆⁾₎〉⎵⟆⟧⟩⟫⦄〉》」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣❫❭❱❳❵⟯⦆⦘⧽⸩❯⦈⦊"))--  ("[[" . ("⟦"))-  ("]]" . ("⟧"))-  ("<"  . ,(agda-input-to-string-list "⟨<≪⋘≺⊂⋐⊏⊰⊲⋖＜"))-  (">"  . ,(agda-input-to-string-list "⟩>≫⋙≻⊃⋑⊐⊱⊳⋗＞"))-  ("<<" . ("⟪"))-  (">>" . ("⟫"))-  ("{{" . ("⦃"))-  ("}}" . ("⦄"))--  ("(b" . ("⟅"))-  (")b" . ("⟆"))--  ("lbag" . ("⟅"))-  ("rbag" . ("⟆"))--  ("<|" . ("⦉"))  ;; Angle bar brackets-  ("|>" . ("⦊"))--  ("(|" . ("⦇"))  ;; Idiom brackets-  ("|)" . ("⦈"))--  ("((" . ,(agda-input-to-string-list "⦅｟"))  ;; Banana brackets-  ("))" . ,(agda-input-to-string-list "⦆｠"))--  ;; Primes.--  ("'" . ,(agda-input-to-string-list "′″‴⁗＇"))-  ("`" . ,(agda-input-to-string-list "‵‶‷｀"))--  ;; Fractions.--  ("frac" . ,(agda-input-to-string-list "¼½¾⅓⅔⅕⅖⅗⅘⅙⅚⅛⅜⅝⅞⅟"))--  ;; Bullets.--  ("bu"  . ,(agda-input-to-string-list "•◦‣⁌⁍"))-  ("bub" . ("•"))-  ("buw" . ("◦"))-  ("but" . ("‣"))--  ;; Musical symbols.--  ("note" . ,(agda-input-to-string-list "♩♪♫♬"))-  ("b"    . ("♭"))-  ("#"    . ("♯"))--  ;; Other punctuation and symbols.--  ("\\"         . ("\\"))-  ("en"         . ("–"))-  ("em"         . ("—"))-  ("!"          . ("！"))-  ("!!"         . ("‼"))-  ("?"          . ("？"))-  ("??"         . ("⁇"))-  ("?!"         . ("‽" "⁈"))-  ("!?"         . ("⁉"))-  ("die"        . ,(agda-input-to-string-list "⚀⚁⚂⚃⚄⚅"))-  ("asterisk"   . ,(agda-input-to-string-list "⁎⁑⁂✢✣✤✥✱✲✳✺✻✼✽❃❉❊❋＊"))-  ("8<"         . ("✂" "✄"))-  ("tie"        . ("⁀"))-  ("undertie"   . ("‿"))-  ("apl"        . ,(agda-input-to-string-list "⌶⌷⌸⌹⌺⌻⌼⌽⌾⌿⍀⍁⍂⍃⍄⍅⍆⍇⍈-                                               ⍉⍊⍋⍌⍍⍎⍏⍐⍑⍒⍓⍔⍕⍖⍗⍘⍙⍚⍛-                                               ⍜⍝⍞⍟⍠⍡⍢⍣⍤⍥⍦⍧⍨⍩⍪⍫⍬⍭⍮-                                               ⍯⍰⍱⍲⍳⍴⍵⍶⍷⍸⍹⍺⎕"))-  ("#"          . ("＃"))-  ("%"          . ("％"))-  ("&"          . ("＆"))-  ("*"          . ("＊"))-  ("/"          . ,(agda-input-to-string-list "／＼"))-  ("@"          . ("＠"))-  ("__"         . ("＿"))-  ("\""         . ("＂"))--  ;; Some combining characters.-  ;;-  ;; The following combining characters also have (other)-  ;; translations:-  ;; ̀ ́ ̂ ̃ ̄ ̆ ̇ ̈ ̋ ̌ ̣ ̧ ̱--  ("^--" . ,(agda-input-to-string-list"̅̿"))-  ("_--" . ,(agda-input-to-string-list"̲̳"))-  ("^~"  . ,(agda-input-to-string-list"̃͌"))-  ("_~"  .  (                         "̰"))-  ("^."  . ,(agda-input-to-string-list"̇̈⃛⃜"))-  ("_."  . ,(agda-input-to-string-list"̣̤"))-  ("^l"  . ,(agda-input-to-string-list"⃖⃐⃔"))-  ("^l-" .  (                         "⃖"))-  ("^r"  . ,(agda-input-to-string-list"⃗⃑⃕"))-  ("^r-" .  (                         "⃗"))-  ("^lr" .  (                         "⃡"))-  ("_lr" .  (                         "͍"))-  ("^^"  . ,(agda-input-to-string-list"̂̑͆"))-  ("_^"  . ,(agda-input-to-string-list"̭̯̪"))-  ("^v"  . ,(agda-input-to-string-list"̌̆"))-  ("_v"  . ,(agda-input-to-string-list"̬̮̺"))--  ;; Shorter forms of many greek letters plus ƛ.--  ("Ga"  . ("α"))  ("GA"  . ("Α"))-  ("Gb"  . ("β"))  ("GB"  . ("Β"))-  ("Gg"  . ("γ"))  ("GG"  . ("Γ"))-  ("Gd"  . ("δ"))  ("GD"  . ("Δ"))-  ("Ge"  . ("ε"))  ("GE"  . ("Ε"))-  ("Gz"  . ("ζ"))  ("GZ"  . ("Ζ"))-  ("Gh"  . ("η"))  ("GH"  . ("Η"))-  ("Gth" . ("θ"))  ("GTH" . ("Θ"))-  ("Gi"  . ("ι"))  ("GI"  . ("Ι"))-  ("Gk"  . ("κ"))  ("GK"  . ("Κ"))-  ("Gl"  . ("λ"))  ("GL"  . ("Λ"))  ("Gl-" . ("ƛ"))-  ("Gm"  . ("μ"))  ("GM"  . ("Μ"))-  ("Gn"  . ("ν"))  ("GN"  . ("Ν"))-  ("Gx"  . ("ξ"))  ("GX"  . ("Ξ"))-  ;; \omicron \Omicron-  ;; \pi \Pi-  ("Gr"  . ("ρ"))  ("GR"  . ("Ρ"))-  ("Gs"  . ("σ"))  ("GS"  . ("Σ"))-  ("Gt"  . ("τ"))  ("GT"  . ("Τ"))-  ("Gu"  . ("υ"))  ("GU"  . ("Υ"))-  ("Gf"  . ("φ"))  ("GF"  . ("Φ"))-  ("Gc"  . ("χ"))  ("GC"  . ("Χ"))-  ("Gp"  . ("ψ"))  ("GP"  . ("Ψ"))-  ("Go"  . ("ω"))  ("GO"  . ("Ω"))--  ;; Mathematical characters--  ("MiA" . ("𝐴"))-  ("MiB" . ("𝐵"))-  ("MiC" . ("𝐶"))-  ("MiD" . ("𝐷"))-  ("MiE" . ("𝐸"))-  ("MiF" . ("𝐹"))-  ("MiG" . ("𝐺"))-  ("MiH" . ("𝐻"))-  ("MiI" . ("𝐼"))-  ("MiJ" . ("𝐽"))-  ("MiK" . ("𝐾"))-  ("MiL" . ("𝐿"))-  ("MiM" . ("𝑀"))-  ("MiN" . ("𝑁"))-  ("MiO" . ("𝑂"))-  ("MiP" . ("𝑃"))-  ("MiQ" . ("𝑄"))-  ("MiR" . ("𝑅"))-  ("MiS" . ("𝑆"))-  ("MiT" . ("𝑇"))-  ("MiU" . ("𝑈"))-  ("MiV" . ("𝑉"))-  ("MiW" . ("𝑊"))-  ("MiX" . ("𝑋"))-  ("MiY" . ("𝑌"))-  ("MiZ" . ("𝑍"))-  ("Mia" . ("𝑎"))-  ("Mib" . ("𝑏"))-  ("Mic" . ("𝑐"))-  ("Mid" . ("𝑑"))-  ("Mie" . ("𝑒"))-  ("Mif" . ("𝑓"))-  ("Mig" . ("𝑔"))-  ("Mih" . ("ℎ"))-  ("Mii" . ("𝑖"))-  ("Mij" . ("𝑗"))-  ("Mik" . ("𝑘"))-  ("Mil" . ("𝑙"))-  ("Mim" . ("𝑚"))-  ("Min" . ("𝑛"))-  ("Mio" . ("𝑜"))-  ("Mip" . ("𝑝"))-  ("Miq" . ("𝑞"))-  ("Mir" . ("𝑟"))-  ("Mis" . ("𝑠"))-  ("Mit" . ("𝑡"))-  ("Miu" . ("𝑢"))-  ("Miv" . ("𝑣"))-  ("Miw" . ("𝑤"))-  ("Mix" . ("𝑥"))-  ("Miy" . ("𝑦"))-  ("Miz" . ("𝑧"))-  ("MIA" . ("𝑨"))-  ("MIB" . ("𝑩"))-  ("MIC" . ("𝑪"))-  ("MID" . ("𝑫"))-  ("MIE" . ("𝑬"))-  ("MIF" . ("𝑭"))-  ("MIG" . ("𝑮"))-  ("MIH" . ("𝑯"))-  ("MII" . ("𝑰"))-  ("MIJ" . ("𝑱"))-  ("MIK" . ("𝑲"))-  ("MIL" . ("𝑳"))-  ("MIM" . ("𝑴"))-  ("MIN" . ("𝑵"))-  ("MIO" . ("𝑶"))-  ("MIP" . ("𝑷"))-  ("MIQ" . ("𝑸"))-  ("MIR" . ("𝑹"))-  ("MIS" . ("𝑺"))-  ("MIT" . ("𝑻"))-  ("MIU" . ("𝑼"))-  ("MIV" . ("𝑽"))-  ("MIW" . ("𝑾"))-  ("MIX" . ("𝑿"))-  ("MIY" . ("𝒀"))-  ("MIZ" . ("𝒁"))-  ("MIa" . ("𝒂"))-  ("MIb" . ("𝒃"))-  ("MIc" . ("𝒄"))-  ("MId" . ("𝒅"))-  ("MIe" . ("𝒆"))-  ("MIf" . ("𝒇"))-  ("MIg" . ("𝒈"))-  ("MIh" . ("𝒉"))-  ("MIi" . ("𝒊"))-  ("MIj" . ("𝒋"))-  ("MIk" . ("𝒌"))-  ("MIl" . ("𝒍"))-  ("MIm" . ("𝒎"))-  ("MIn" . ("𝒏"))-  ("MIo" . ("𝒐"))-  ("MIp" . ("𝒑"))-  ("MIq" . ("𝒒"))-  ("MIr" . ("𝒓"))-  ("MIs" . ("𝒔"))-  ("MIt" . ("𝒕"))-  ("MIu" . ("𝒖"))-  ("MIv" . ("𝒗"))-  ("MIw" . ("𝒘"))-  ("MIx" . ("𝒙"))-  ("MIy" . ("𝒚"))-  ("MIz" . ("𝒛"))-  ("McA" . ("𝒜"))-  ("McB" . ("ℬ"))-  ("McC" . ("𝒞"))-  ("McD" . ("𝒟"))-  ("McE" . ("ℰ"))-  ("McF" . ("ℱ"))-  ("McG" . ("𝒢"))-  ("McH" . ("ℋ"))-  ("McI" . ("ℐ"))-  ("McJ" . ("𝒥"))-  ("McK" . ("𝒦"))-  ("McL" . ("ℒ"))-  ("McM" . ("ℳ"))-  ("McN" . ("𝒩"))-  ("McO" . ("𝒪"))-  ("McP" . ("𝒫"))-  ("McQ" . ("𝒬"))-  ("McR" . ("ℛ"))-  ("McS" . ("𝒮"))-  ("McT" . ("𝒯"))-  ("McU" . ("𝒰"))-  ("McV" . ("𝒱"))-  ("McW" . ("𝒲"))-  ("McX" . ("𝒳"))-  ("McY" . ("𝒴"))-  ("McZ" . ("𝒵"))-  ("Mca" . ("𝒶"))-  ("Mcb" . ("𝒷"))-  ("Mcc" . ("𝒸"))-  ("Mcd" . ("𝒹"))-  ("Mce" . ("ℯ"))-  ("Mcf" . ("𝒻"))-  ("Mcg" . ("ℊ"))-  ("Mch" . ("𝒽"))-  ("Mci" . ("𝒾"))-  ("Mcj" . ("𝒿"))-  ("Mck" . ("𝓀"))-  ("Mcl" . ("𝓁"))-  ("Mcm" . ("𝓂"))-  ("Mcn" . ("𝓃"))-  ("Mco" . ("ℴ"))-  ("Mcp" . ("𝓅"))-  ("Mcq" . ("𝓆"))-  ("Mcr" . ("𝓇"))-  ("Mcs" . ("𝓈"))-  ("Mct" . ("𝓉"))-  ("Mcu" . ("𝓊"))-  ("Mcv" . ("𝓋"))-  ("Mcw" . ("𝓌"))-  ("Mcx" . ("𝓍"))-  ("Mcy" . ("𝓎"))-  ("Mcz" . ("𝓏"))-  ("MCA" . ("𝓐"))-  ("MCB" . ("𝓑"))-  ("MCC" . ("𝓒"))-  ("MCD" . ("𝓓"))-  ("MCE" . ("𝓔"))-  ("MCF" . ("𝓕"))-  ("MCG" . ("𝓖"))-  ("MCH" . ("𝓗"))-  ("MCI" . ("𝓘"))-  ("MCJ" . ("𝓙"))-  ("MCK" . ("𝓚"))-  ("MCL" . ("𝓛"))-  ("MCM" . ("𝓜"))-  ("MCN" . ("𝓝"))-  ("MCO" . ("𝓞"))-  ("MCP" . ("𝓟"))-  ("MCQ" . ("𝓠"))-  ("MCR" . ("𝓡"))-  ("MCS" . ("𝓢"))-  ("MCT" . ("𝓣"))-  ("MCU" . ("𝓤"))-  ("MCV" . ("𝓥"))-  ("MCW" . ("𝓦"))-  ("MCX" . ("𝓧"))-  ("MCY" . ("𝓨"))-  ("MCZ" . ("𝓩"))-  ("MCa" . ("𝓪"))-  ("MCb" . ("𝓫"))-  ("MCc" . ("𝓬"))-  ("MCd" . ("𝓭"))-  ("MCe" . ("𝓮"))-  ("MCf" . ("𝓯"))-  ("MCg" . ("𝓰"))-  ("MCh" . ("𝓱"))-  ("MCi" . ("𝓲"))-  ("MCj" . ("𝓳"))-  ("MCk" . ("𝓴"))-  ("MCl" . ("𝓵"))-  ("MCm" . ("𝓶"))-  ("MCn" . ("𝓷"))-  ("MCo" . ("𝓸"))-  ("MCp" . ("𝓹"))-  ("MCq" . ("𝓺"))-  ("MCr" . ("𝓻"))-  ("MCs" . ("𝓼"))-  ("MCt" . ("𝓽"))-  ("MCu" . ("𝓾"))-  ("MCv" . ("𝓿"))-  ("MCw" . ("𝔀"))-  ("MCx" . ("𝔁"))-  ("MCy" . ("𝔂"))-  ("MCz" . ("𝔃"))-  ("MfA" . ("𝔄"))-  ("MfB" . ("𝔅"))-  ("MfC" . ("ℭ"))-  ("MfD" . ("𝔇"))-  ("MfE" . ("𝔈"))-  ("MfF" . ("𝔉"))-  ("MfG" . ("𝔊"))-  ("MfH" . ("ℌ"))-  ("MfI" . ("ℑ"))-  ("MfJ" . ("𝔍"))-  ("MfK" . ("𝔎"))-  ("MfL" . ("𝔏"))-  ("MfM" . ("𝔐"))-  ("MfN" . ("𝔑"))-  ("MfO" . ("𝔒"))-  ("MfP" . ("𝔓"))-  ("MfQ" . ("𝔔"))-  ("MfR" . ("ℜ"))-  ("MfS" . ("𝔖"))-  ("MfT" . ("𝔗"))-  ("MfU" . ("𝔘"))-  ("MfV" . ("𝔙"))-  ("MfW" . ("𝔚"))-  ("MfX" . ("𝔛"))-  ("MfY" . ("𝔜"))-  ("MfZ" . ("ℨ"))-  ("Mfa" . ("𝔞"))-  ("Mfb" . ("𝔟"))-  ("Mfc" . ("𝔠"))-  ("Mfd" . ("𝔡"))-  ("Mfe" . ("𝔢"))-  ("Mff" . ("𝔣"))-  ("Mfg" . ("𝔤"))-  ("Mfh" . ("𝔥"))-  ("Mfi" . ("𝔦"))-  ("Mfj" . ("𝔧"))-  ("Mfk" . ("𝔨"))-  ("Mfl" . ("𝔩"))-  ("Mfm" . ("𝔪"))-  ("Mfn" . ("𝔫"))-  ("Mfo" . ("𝔬"))-  ("Mfp" . ("𝔭"))-  ("Mfq" . ("𝔮"))-  ("Mfr" . ("𝔯"))-  ("Mfs" . ("𝔰"))-  ("Mft" . ("𝔱"))-  ("Mfu" . ("𝔲"))-  ("Mfv" . ("𝔳"))-  ("Mfw" . ("𝔴"))-  ("Mfx" . ("𝔵"))-  ("Mfy" . ("𝔶"))-  ("Mfz" . ("𝔷"))--  ;; (Sub / Super) scripts-  ;;-  ;; Unicode 12.1 omits several latin characters from sub/superscript.-  ;; https://www.quora.com/Why-is-there-no-character-for-superscript-q-in-Unicode-  ;;-  ;; Perhaps they will be added in future versions, however there are no-  ;; proposals for it currently in the pipeline:-  ;; https://www.unicode.org/alloc/Pipeline.html--  ("_a" . ("ₐ"))-  ;; ("_b" . ("b"))-  ;; ("_c" . ("c"))-  ;; ("_d" . ("d"))-  ("_e" . ("ₑ"))-  ;; ("_f" . ("f"))-  ;; ("_g" . ("g"))-  ("_h" . ("ₕ"))-  ("_i" . ("ᵢ"))-  ("_j" . ("ⱼ"))-  ("_k" . ("ₖ"))-  ("_l" . ("ₗ"))-  ("_m" . ("ₘ"))-  ("_n" . ("ₙ"))-  ("_o" . ("ₒ"))-  ("_p" . ("ₚ"))-  ;; ("_q" . ("q"))-  ("_r" . ("ᵣ"))-  ("_s" . ("ₛ"))-  ("_t" . ("ₜ"))-  ("_u" . ("ᵤ"))-  ("_v" . ("ᵥ"))-  ;; ("_w" . ("w"))-  ("_x" . ("ₓ"))-  ;; ("_y" . ("y"))-  ;; ("_z" . ("z"))--  ("_Gb" . ("ᵦ"))-  ("_Gg" . ("ᵧ"))-  ("_Gr" . ("ᵨ"))-  ("_Gf" . ("ᵩ"))-  ("_Gc" . ("ᵪ"))--  ("^a" . ("ᵃ"))-  ("^b" . ("ᵇ"))-  ("^c" . ("ᶜ"))-  ("^d" . ("ᵈ"))-  ("^e" . ("ᵉ"))-  ("^f" . ("ᶠ"))-  ("^g" . ("ᵍ"))-  ("^h" . ("ʰ"))-  ("^i" . ("ⁱ"))-  ("^j" . ("ʲ"))-  ("^k" . ("ᵏ"))-  ("^l" . ("ˡ"))-  ("^m" . ("ᵐ"))-  ("^n" . ("ⁿ"))-  ("^o" . ("ᵒ"))-  ("^p" . ("ᵖ"))-  ;; ("^q" . ("q"))-  ("^r" . ("ʳ"))-  ("^s" . ("ˢ"))-  ("^t" . ("ᵗ"))-  ("^u" . ("ᵘ"))-  ("^v" . ("ᵛ"))-  ("^w" . ("ʷ"))-  ("^x" . ("ˣ"))-  ("^y" . ("ʸ"))-  ("^z" . ("ᶻ"))--  ("^A" . ("ᴬ"))-  ("^B" . ("ᴮ"))-  ;; ("^C" . ("C"))-  ("^D" . ("ᴰ"))-  ("^E" . ("ᴱ"))-  ;; ("^F" . ("F"))-  ("^G" . ("ᴳ"))-  ("^H" . ("ᴴ"))-  ("^I" . ("ᴵ"))-  ("^J" . ("ᴶ"))-  ("^K" . ("ᴷ"))-  ("^L" . ("ᴸ"))-  ("^M" . ("ᴹ"))-  ("^N" . ("ᴺ"))-  ("^O" . ("ᴼ"))-  ("^P" . ("ᴾ"))-  ;; ("^Q" . ("Q"))-  ("^R" . ("ᴿ"))-  ;; ("^S" . ("S"))-  ("^T" . ("ᵀ"))-  ("^U" . ("ᵁ"))-  ("^V" . ("ⱽ"))-  ("^W" . ("ᵂ"))-  ;; ("^X" . ("X"))-  ;; ("^Y" . ("Y"))-  ;; ("^Z" . ("Z"))--  ("^Gb" . ("ᵝ"))-  ("^Gg" . ("ᵞ"))-  ("^Gd" . ("ᵟ"))-  ("^Ge" . ("ᵋ"))-  ("^Gth" . ("ᶿ"))-  ("^Gf" . ("ᵠ"))-  ("^Gc" . ("ᵡ"))--  ;; Some ISO8859-1 characters.--  (" "         . (" "))-  ("!"         . ("¡"))-  ("cent"      . ("¢"))-  ("brokenbar" . ("¦"))-  ("degree"    . ("°"))-  ("?"         . ("¿"))-  ("^a_"       . ("ª"))-  ("^o_"       . ("º"))--  ;; Circled, parenthesised etc. numbers and letters.--  ( "(0)" . ,(agda-input-to-string-list " ⓪🄀⓿🄋🄌"))-  ( "(1)" . ,(agda-input-to-string-list "⑴①⒈❶➀➊"))-  ( "(2)" . ,(agda-input-to-string-list "⑵②⒉❷➁➋"))-  ( "(3)" . ,(agda-input-to-string-list "⑶③⒊❸➂➌"))-  ( "(4)" . ,(agda-input-to-string-list "⑷④⒋❹➃➍"))-  ( "(5)" . ,(agda-input-to-string-list "⑸⑤⒌❺➄➎"))-  ( "(6)" . ,(agda-input-to-string-list "⑹⑥⒍❻➅➏"))-  ( "(7)" . ,(agda-input-to-string-list "⑺⑦⒎❼➆➐"))-  ( "(8)" . ,(agda-input-to-string-list "⑻⑧⒏❽➇➑"))-  ( "(9)" . ,(agda-input-to-string-list "⑼⑨⒐❾➈➒"))-  ("(10)" . ,(agda-input-to-string-list "⑽⑩⒑❿➉➓"))-  ("(11)" . ,(agda-input-to-string-list "⑾⑪⒒⓫"))-  ("(12)" . ,(agda-input-to-string-list "⑿⑫⒓⓬"))-  ("(13)" . ,(agda-input-to-string-list "⒀⑬⒔⓭"))-  ("(14)" . ,(agda-input-to-string-list "⒁⑭⒕⓮"))-  ("(15)" . ,(agda-input-to-string-list "⒂⑮⒖⓯"))-  ("(16)" . ,(agda-input-to-string-list "⒃⑯⒗⓰"))-  ("(17)" . ,(agda-input-to-string-list "⒄⑰⒘⓱"))-  ("(18)" . ,(agda-input-to-string-list "⒅⑱⒙⓲"))-  ("(19)" . ,(agda-input-to-string-list "⒆⑲⒚⓳"))-  ("(20)" . ,(agda-input-to-string-list "⒇⑳⒛⓴"))--  ("(a)"  . ,(agda-input-to-string-list "⒜Ⓐⓐ🅐🄰🅰"))-  ("(b)"  . ,(agda-input-to-string-list "⒝Ⓑⓑ🅑🄱🅱"))-  ("(c)"  . ,(agda-input-to-string-list "⒞Ⓒⓒ🅒🄲🅲"))-  ("(d)"  . ,(agda-input-to-string-list "⒟Ⓓⓓ🅓🄳🅳"))-  ("(e)"  . ,(agda-input-to-string-list "⒠Ⓔⓔ🅔🄴🅴"))-  ("(f)"  . ,(agda-input-to-string-list "⒡Ⓕⓕ🅕🄵🅵"))-  ("(g)"  . ,(agda-input-to-string-list "⒢Ⓖⓖ🅖🄶🅶"))-  ("(h)"  . ,(agda-input-to-string-list "⒣Ⓗⓗ🅗🄷🅷"))-  ("(i)"  . ,(agda-input-to-string-list "⒤Ⓘⓘ🅘🄸🅸"))-  ("(j)"  . ,(agda-input-to-string-list "⒥Ⓙⓙ🅙🄹🅹"))-  ("(k)"  . ,(agda-input-to-string-list "⒦Ⓚⓚ🅚🄺🅺"))-  ("(l)"  . ,(agda-input-to-string-list "⒧Ⓛⓛ🅛🄻🅻"))-  ("(m)"  . ,(agda-input-to-string-list "⒨Ⓜⓜ🅜🄼🅼"))-  ("(n)"  . ,(agda-input-to-string-list "⒩Ⓝⓝ🅝🄽🅽"))-  ("(o)"  . ,(agda-input-to-string-list "⒪Ⓞⓞ🅞🄾🅾"))-  ("(p)"  . ,(agda-input-to-string-list "⒫Ⓟⓟ🅟🄿🅿"))-  ("(q)"  . ,(agda-input-to-string-list "⒬Ⓠⓠ🅠🅀🆀"))-  ("(r)"  . ,(agda-input-to-string-list "⒭Ⓡⓡ🅡🅁🆁"))-  ("(s)"  . ,(agda-input-to-string-list "⒮Ⓢⓢ🅢🅂🆂"))-  ("(t)"  . ,(agda-input-to-string-list "⒯Ⓣⓣ🅣🅃🆃"))-  ("(u)"  . ,(agda-input-to-string-list "⒰Ⓤⓤ🅤🅄🆄"))-  ("(v)"  . ,(agda-input-to-string-list "⒱Ⓥⓥ🅥🅅🆅"))-  ("(w)"  . ,(agda-input-to-string-list "⒲Ⓦⓦ🅦🅆🆆"))-  ("(x)"  . ,(agda-input-to-string-list "⒳Ⓧⓧ🅧🅇🆇"))-  ("(y)"  . ,(agda-input-to-string-list "⒴Ⓨⓨ🅨🅈🆈"))-  ("(z)"  . ,(agda-input-to-string-list "⒵Ⓩⓩ🅩🅉🆉"))--  ))-  "A list of translations specific to the Agda input method.-Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS).-All the translation strings are possible translations-of the given key sequence; if there is more than one you can choose-between them using the arrow keys.--Note that if you customize this setting you will not-automatically benefit (or suffer) from modifications to its-default value when the library is updated.  If you just want to-add some bindings it is probably a better idea to customize-`agda-input-user-translations'.--These translation pairs are included after those in-`agda-input-user-translations', but before the ones inherited-from other input methods (see `agda-input-inherit').--If you change this setting manually (without using the-customization buffer) you need to call `agda-input-setup' in-order for the change to take effect."-  :group 'agda-input-  :set 'agda-input-incorporate-changed-setting-  :initialize 'custom-initialize-default-  :type '(repeat (cons (string :tag "Key sequence")-                       (repeat :tag "Translations" string))))--(defcustom agda-input-user-translations nil-  "Like `agda-input-translations', but more suitable for user-customizations since by default it is empty.--These translation pairs are included first, before those in-`agda-input-translations' and the ones inherited from other input-methods."-  :group 'agda-input-  :set 'agda-input-incorporate-changed-setting-  :initialize 'custom-initialize-default-  :type '(repeat (cons (string :tag "Key sequence")-                       (repeat :tag "Translations" string))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Inspecting and modifying translation maps--(defun agda-input-get-translations (qp)-  "Return a list containing all translations from the Quail-package QP (except for those corresponding to ASCII).-Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)."-  (with-temp-buffer-    (activate-input-method qp) ; To make sure that the package is loaded.-    (unless (quail-package qp)-      (error "%s is not a Quail package." qp))-    (let ((decode-map (list 'decode-map)))-      (quail-build-decode-map (list (quail-map)) "" decode-map 0)-      (cdr decode-map))))--(defun agda-input-show-translations (qp)-  "Display all translations used by the Quail package QP (a string).-\(Except for those corresponding to ASCII)."-  (interactive (list (read-input-method-name-                      "Quail input method (default %s): " "Agda")))-  (let ((buf (concat "*" qp " input method translations*")))-    (with-output-to-temp-buffer buf-      (with-current-buffer buf-        (quail-insert-decode-map-         (cons 'decode-map (agda-input-get-translations qp)))))))--(defun agda-input-add-translations (trans)-  "Add the given translations TRANS to the Agda input method.-TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The-translations are appended to the current translations."-  (with-temp-buffer-    (dolist (tr (agda-input-concat-map (eval agda-input-tweak-all) trans))-      (quail-defrule (car tr) (cdr tr) "Agda" t))))--(defun agda-input-inherit-package (qp &optional fun)-  "Let the Agda input method inherit the translations from the-Quail package QP (except for those corresponding to ASCII).--The optional function FUN can be used to modify the translations.-It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return-a list of such pairs."-  (let ((trans (agda-input-get-translations qp)))-    (agda-input-add-translations-     (if fun (agda-input-concat-map fun trans)-       trans))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Setting up the input method--(defun agda-input-setup ()-  "Set up the Agda input method based on the customisable-variables and underlying input methods."--  ;; Create (or reset) the input method.-  (with-temp-buffer-    (quail-define-package "Agda" "UTF-8" "∏" t ; guidance-     "Agda input method.-The purpose of this input method is to edit Agda programs, but-since it is highly customisable it can be made useful for other-tasks as well."-     nil nil nil nil nil nil t ; maximum-shortest-     ))--  (agda-input-add-translations-   (mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr))))-           (append agda-input-user-translations-                   agda-input-translations)))-  (dolist (def agda-input-inherit)-    (agda-input-inherit-package (car def)-                                (eval (cdr def)))))--(defun agda-input-incorporate-changed-setting (sym val)-  "Update the Agda input method based on the customisable-variables and underlying input methods.-Suitable for use in the :set field of `defcustom'."-  (set-default sym val)-  (agda-input-setup))--;; Set up the input method.--(agda-input-setup)--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Administrative details--(provide 'agda-input)-;;; agda-input.el ends here

@@ -1,106 +0,0 @@-;; agda2-abbrevs.el --- Default Agda abbrevs-;; SPDX-License-Identifier: MIT License--;;; Commentary:--;;; Code:--;; Skeletons--(require 'skeleton)--(define-skeleton agda2-abbrevs-module-  "Inserts a module header template."-  nil-  "module " _ " where\n")--(define-skeleton agda2-abbrevs-data-  "Inserts a data template."-  nil-  "data " _ " : Set where\n")--(define-skeleton agda2-abbrevs-record-  "Inserts a record type template."-  nil-  "record " _ " : Set where\n"-  "  field\n")--(define-skeleton agda2-abbrevs-record-value-  "Inserts a record value template."-  nil-  "record {" _ "}")--(define-skeleton agda2-abbrevs-using-  "Inserts a using template."-  nil-  "using (" _ ")")--(define-skeleton agda2-abbrevs-hiding-  "Inserts a hiding template."-  nil-  "hiding (" _ ")")--(define-skeleton agda2-abbrevs-renaming-  "Inserts a renaming template."-  nil-  "renaming (" _ " to " _ ")")--(define-skeleton agda2-abbrevs-forall-  "Inserts a forall template."-  nil-  "∀ {" _ "} ")--(define-skeleton agda2-abbrevs-code-block-  "Inserts a code block."-  nil-  "\\begin{code}\n  " _ "\n\\end{code}\n")--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Abbrevs--(defvar agda2-abbrevs-defaults '(-  ("m"   "" agda2-abbrevs-module)-  ("d"   "" agda2-abbrevs-data)-  ("c"   "" agda2-abbrevs-code-block)-  ("re"  "" agda2-abbrevs-record)-  ("rec" "" agda2-abbrevs-record-value)-  ("u"   "" agda2-abbrevs-using)-  ("h"   "" agda2-abbrevs-hiding)-  ("r"   "" agda2-abbrevs-renaming)-  ("w"   "where\n")-  ("po"  "postulate")-  ("a"   "abstract\n")-  ("pr"  "private\n")-  ("pu"  "public")-  ("mu"  "mutual\n")-  ("f"   "" agda2-abbrevs-forall)-  ("oi"  "open import "))-  "Abbreviations defined by default in the Agda mode.")--(defcustom agda2-mode-abbrevs-use-defaults nil-  "If non-nil include the default Agda mode abbrevs in `agda2-mode-abbrev-table'.-The abbrevs are designed to be expanded explicitly, so users of `abbrev-mode'-probably do not want to include them.--Restart Emacs in order for this change to take effect."-  :group 'agda2-  :type '(choice (const :tag "Yes" t)-                 (const :tag "No" nil)))--(defvar agda2-mode-abbrev-table nil-  "Agda mode abbrev table.")--(define-abbrev-table-  'agda2-mode-abbrev-table-  (if agda2-mode-abbrevs-use-defaults-      (mapcar (lambda (abbrev)-                (append abbrev-                        (make-list (- 4 (length abbrev)) nil)-                        '((:system t))))-              agda2-abbrevs-defaults)))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Administrative details--(provide 'agda2-abbrevs)-;;; agda2-abbrevs.el ends here

@@ -1,596 +0,0 @@-;;; agda2-highlight.el --- Syntax highlighting for Agda (version ≥ 2)-;; SPDX-License-Identifier: MIT License--;;; Commentary:--;; Code to apply syntactic highlighting to Agda source code. This uses-;; Agda's own annotations to figure out what is what, so the parsing-;; is always done correctly, but highlighting is not done on the fly.--;;; Code:--(require 'annotation)-(require 'font-lock)--(defgroup agda2-highlight nil-  "Syntax highlighting for Agda."-  :group 'agda2)--(defcustom agda2-highlight-level 'non-interactive-  "How much syntax highlighting should be produced?-Interactive highlighting includes highlighting of the expression-that is currently being type-checked."-  :type '(choice-          (const :tag "None"            none)-          (const :tag "Non-interactive" non-interactive)-          (const :tag "Interactive"     interactive))-  :group 'agda2-highlight)--(defun agda2-highlight-level nil-  "Formats the highlighting level in a Haskelly way."-  (cond ((equal agda2-highlight-level 'none)            "None")-        ((equal agda2-highlight-level 'non-interactive) "NonInteractive")-        ((equal agda2-highlight-level 'interactive)     "Interactive")-        (t                                              "None")))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Functions for setting faces--(defun agda2-highlight-set-face-attribute (face attrs)-  "Reset (globally) all attributes of the face FACE according to ATTRS.-If the face does not exist, then it is created first."-  (make-face face)-  (set-face-attribute face nil-                      :family         'unspecified-                      :width          'unspecified-                      :height         'unspecified-                      :weight         'unspecified-                      :slant          'unspecified-                      :foreground     'unspecified-                      :background     'unspecified-                      :inverse-video  'unspecified-                      :stipple        'unspecified-                      :underline      'unspecified-                      :overline       'unspecified-                      :strike-through 'unspecified-                      :inherit        'unspecified-                      :box            'unspecified-                      :font           'unspecified)-  (eval `(set-face-attribute face nil ,@attrs)))--(defun agda2-highlight-set-faces (variable group)-  "Set all Agda faces according to the value of GROUP.-Also sets the default value of VARIABLE to GROUP."-  (set-default variable group)-  (mapc (lambda (face-and-attrs)-          (agda2-highlight-set-face-attribute-           (car face-and-attrs) (cdr face-and-attrs)))-        (cond-         ((equal group 'conor)-          '((agda2-highlight-keyword-face-             :bold t)-            (agda2-highlight-string-face-             :foreground "firebrick3")-            (agda2-highlight-number-face-             :foreground "firebrick3")-            (agda2-highlight-symbol-face-             :foreground "grey25")-            (agda2-highlight-primitive-type-face-             :foreground "medium blue")-            (agda2-highlight-bound-variable-face-             :foreground "purple")-            (agda2-highlight-generalizable-variable-face-             :foreground "purple")-            (agda2-highlight-inductive-constructor-face-             :foreground "firebrick3")-            (agda2-highlight-coinductive-constructor-face-             :foreground "firebrick3")-            (agda2-highlight-datatype-face-             :foreground "medium blue")-            (agda2-highlight-field-face-             :foreground "deeppink")-            (agda2-highlight-function-face-             :foreground "darkgreen")-            (agda2-highlight-module-face-             :foreground "medium blue")-            (agda2-highlight-postulate-face-             :foreground "darkgreen")-            (agda2-highlight-primitive-face-             :foreground "darkgreen")-            (agda2-highlight-macro-face-             :foreground "aquamarine4")-            (agda2-highlight-record-face-             :foreground "medium blue")-            (agda2-highlight-dotted-face)-            (agda2-highlight-error-face-             :foreground "red"-             :underline t)-            (agda2-highlight-error-warning-face-             :background "light coral"-             :underline t)-            (agda2-highlight-unsolved-meta-face-             :foreground "black"-             :background "yellow")-            (agda2-highlight-unsolved-constraint-face-             :foreground "black"-             :background "yellow")-            (agda2-highlight-termination-problem-face-             :foreground "black"-             :background "light salmon")-            (agda2-highlight-positivity-problem-face-             :foreground "black"-             :background "peru")-            (agda2-highlight-incomplete-pattern-face-             :foreground "black"-             :background "purple")-            (agda2-highlight-typechecks-face-             :foreground "black"-             :background "light blue")))-         ((equal group 'default-faces)-          (list (cons 'agda2-highlight-keyword-face-                      (list :inherit font-lock-keyword-face))-                (cons 'agda2-highlight-string-face-                      (list :inherit font-lock-string-face))-                (cons 'agda2-highlight-number-face-                      (list :inherit font-lock-constant-face))-                (cons 'agda2-highlight-symbol-face-                      (list :inherit font-lock-keyword-face))-                (cons 'agda2-highlight-primitive-type-face-                      (list :inherit font-lock-keyword-face))-                (cons 'agda2-highlight-bound-variable-face-                      (list :inherit font-lock-variable-name-face))-                (cons 'agda2-highlight-generalizable-variable-face-                      (list :inherit font-lock-variable-name-face))-                (cons 'agda2-highlight-inductive-constructor-face-                      (list :inherit font-lock-type-face))-                (cons 'agda2-highlight-coinductive-constructor-face-                      (list :inherit font-lock-type-face))-                (cons 'agda2-highlight-datatype-face-                      (list :inherit font-lock-type-face))-                (cons 'agda2-highlight-field-face-                      (list :inherit font-lock-variable-name-face))-                (cons 'agda2-highlight-function-face-                      (list :inherit font-lock-function-name-face))-                (cons 'agda2-highlight-module-face-                      (list :inherit font-lock-type-face))-                (cons 'agda2-highlight-postulate-face-                      (list :inherit font-lock-type-face))-                (cons 'agda2-highlight-primitive-face-                      (list :inherit font-lock-constant-face))-                (cons 'agda2-highlight-macro-face-                      (list :inherit font-lock-function-name-face))-                (cons 'agda2-highlight-record-face-                      (list :inherit font-lock-variable-name-face))-                (cons 'agda2-highlight-dotted-face-                      (list :inherit font-lock-variable-name-face))-                (cons 'agda2-highlight-operator-face-                      (list :inherit font-lock-function-name-face))-                (cons 'agda2-highlight-error-face-                      (list :inherit font-lock-warning-face))-                (cons 'agda2-highlight-typechecks-face-                      (list :inherit font-lock-type-face))-                (cons 'agda2-highlight-typechecking-face-                      (list :inherit font-lock-preprocessor-face)))))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Faces--(defcustom agda2-highlight-face-groups nil-  "Colour scheme used in Agda buffers.-Changes to this variable may not take full effect until you have-restarted Emacs. Note also that if you are using the-default-faces option and change your colour theme, then the-changes may not take effect in Agda buffers until you have-restarted Emacs."-  :type '(choice-          (const :tag "Use the settings in the \"Agda2 Highlight Faces\" subgroup." nil)-          (const :tag "Use an approximation of Conor McBride's colour scheme."-                 conor)-          (const :tag "Use simplified highlighting and default font-lock faces."-                 default-faces))-  :group 'agda2-highlight-  :set 'agda2-highlight-set-faces)--(defgroup agda2-highlight-faces nil-  "Faces used to highlight Agda code.-If `agda2-highlight-face-groups' is nil."-  :group 'agda2-highlight)--(defface agda2-highlight-keyword-face-  '((((background light))-     (:foreground "DarkOrange3"))-    (((background dark))-     (:foreground "#FF9932")))-  "The face used for keywords."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-string-face-  '((((background light))-     (:foreground "firebrick"))-    (((background dark))-     (:foreground "#DD4D4D")))-  "The face used for strings."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-number-face-  '((((background light))-     (:foreground "purple"))-    (((background dark))-     (:foreground "#9010E0")))-  "The face used for numbers."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-symbol-face-  '((((background light))-     (:foreground "gray25"))-    (((background dark))-     (:foreground "gray75")))-  "The face used for symbols like forall, =, ->, etc."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-primitive-type-face-  '((((background light))-     (:foreground "medium blue"))-    (((background dark))-     (:foreground "#8080FF")))-  "The face used for primitive types (like Set and Prop)."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-bound-variable-face-  '((t nil))-  "The face used for bound variables."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-generalizable-variable-face-  '((t nil))-  "The face used for generalizable variables."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-inductive-constructor-face-  '((((background light))-     :foreground "green4")-    (((background dark))-     :foreground "#29CC29"))-  "The face used for inductive constructors."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-coinductive-constructor-face-  '((((background light))-     :foreground "gold4")-    (((background dark))-     :foreground "#FFEA75"))-  "The face used for coinductive constructors."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-datatype-face-  '((((background light))-     (:foreground "medium blue"))-    (((background dark))-     (:foreground "#8080FF")))-  "The face used for datatypes."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-field-face-  '((((background light))-     (:foreground "DeepPink2"))-    (((background dark))-     (:foreground "#F570B7")))-  "The face used for record fields."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-function-face-  '((((background light))-     (:foreground "medium blue"))-    (((background dark))-     (:foreground "#8080FF")))-  "The face used for functions."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-module-face-  '((((background light))-     (:foreground "purple"))-    (((background dark))-     (:foreground "#CD80FF")))-  "The face used for module names."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-postulate-face-  '((((background light))-     (:foreground "medium blue"))-    (((background dark))-     (:foreground "#8080FF")))-  "The face used for postulates."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-pragma-face-  '((t nil))-  "The face used for (some text in) pragmas."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-primitive-face-  '((((background light))-     (:foreground "medium blue"))-    (((background dark))-     (:foreground "#8080FF")))-  "The face used for primitive functions."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-macro-face-  '((((background light))-     (:foreground "aquamarine4"))-    (((background dark))-     (:foreground "#73BAA2")))-  "The face used for macros."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-record-face-  '((((background light))-     (:foreground "medium blue"))-    (((background dark))-     (:foreground "#8080FF")))-  "The face used for record types."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-dotted-face-  '((t nil))-  "The face used for dotted patterns."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-operator-face-  '((t nil))-  "The face used for operators."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-error-face-  '((((background light))-     (:foreground "red" :underline t))-    (((background dark))-     (:foreground "#FF0000" :underline t)))-  "The face used for errors."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-error-warning-face-  '((((background light))-     (:background "light coral" :underline t))-    (((background dark))-     (:background "#802400" :underline t)))-  "The face used for fatal warnings."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-unsolved-meta-face-  '((((background light))-     (:background "yellow"))-    (((background dark))-     (:background "#806B00")))-  "The face used for unsolved meta variables."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-unsolved-constraint-face-  '((((background light))-     (:background "yellow"))-    (((background dark))-     (:background "#806B00")))-  "The face used for unsolved constraints which are not connected to metas."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-termination-problem-face-  '((((background light))-     (:background "light salmon"))-    (((background dark))-     (:background "#802400")))-  "The face used for termination problems."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-positivity-problem-face-  '((((background light))-     (:background "peru"))-    (((background dark))-     (:background "#803F00")))-  "The face used for positivity problems."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-deadcode-face-  '((((background light))-     (:background "dark gray"))-    (((background dark))-     (:background "#808080")))-  "The face used for dead code (unreachable clauses, etc.)."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-shadowing-in-telescope-face-  '((((background light))-     (:background "dark gray"))-    (((background dark))-     (:background "#808080")))-  "The face used for shadowed repeated variable names in telescopes."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-coverage-problem-face-  '((((background light))-     (:background "wheat"))-    (((background dark))-     (:background "#805300")))-  "The face used for coverage problems."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-catchall-clause-face-  '((((background light))-     (:background "white smoke"))-    (((background dark))-     (:background "#404040")))-  "The face used for catchall clauses."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-confluence-problem-face-  '((((background light))-     (:background "pink"))-    (((background dark))-     (:background "#800080")))-  "The face used for confluence problems."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-missing-definition-face-  '((((background light))-     (:background "orange"))-    (((background dark))-     (:background "#804040")))-  "The face used for type declarations with missing definitions."-  :group 'agda2-highlight-faces)--(defface agda2-highlight-typechecks-face-  '((((background light))-     (:background "light blue" :foreground "black"))-    (((background dark))-     (:background "#006080" :foreground "white")))-  "The face used for code which is being type-checked."-  :group 'agda2-highlight-faces)--(defvar agda2-highlight-faces-  '((keyword                . agda2-highlight-keyword-face)-    (comment                . font-lock-comment-face)-    (background             . default)-    (markup                 . font-lock-comment-delimiter-face)-    (string                 . agda2-highlight-string-face)-    (number                 . agda2-highlight-number-face)-    (symbol                 . agda2-highlight-symbol-face)-    (primitivetype          . agda2-highlight-primitive-type-face)-    (bound                  . agda2-highlight-bound-variable-face)-    (generalizable          . agda2-highlight-generalizable-variable-face)-    (inductiveconstructor   . agda2-highlight-inductive-constructor-face)-    (coinductiveconstructor . agda2-highlight-coinductive-constructor-face)-    (datatype               . agda2-highlight-datatype-face)-    (field                  . agda2-highlight-field-face)-    (function               . agda2-highlight-function-face)-    (module                 . agda2-highlight-module-face)-    (postulate              . agda2-highlight-postulate-face)-    (pragma                 . agda2-highlight-pragma-face)-    (primitive              . agda2-highlight-primitive-face)-    (macro                  . agda2-highlight-macro-face)-    (record                 . agda2-highlight-record-face)-    (dotted                 . agda2-highlight-dotted-face)-    (operator               . agda2-highlight-operator-face)-    (error                  . agda2-highlight-error-face)-    (errorwarning           . agda2-highlight-error-warning-face)-    (unsolvedmeta           . agda2-highlight-unsolved-meta-face)-    (unsolvedconstraint     . agda2-highlight-unsolved-constraint-face)-    (terminationproblem     . agda2-highlight-termination-problem-face)-    (deadcode               . agda2-highlight-deadcode-face)-    (shadowingintelescope   . agda2-highlight-shadowing-in-telescope-face)-    (coverageproblem        . agda2-highlight-coverage-problem-face)-    (positivityproblem      . agda2-highlight-positivity-problem-face)-    (incompletepattern      . agda2-highlight-incomplete-pattern-face)-    (catchallclause         . agda2-highlight-catchall-clause-face)-    (confluenceproblem      . agda2-highlight-confluence-problem-face)-    (missingdefinition      . agda2-highlight-missing-definition-face)-    (typechecks             . agda2-highlight-typechecks-face))-  "Alist mapping code aspects to the face used when displaying them.--The aspects currently recognised are the following:--`background'             Non-Agda code contents in literate mode.-`bound'                  Bound variables.-`catchallclause'         Clause not holding definitionally.-`coinductiveconstructor' Coinductive constructors.-`comment'                Comments.-`coverageproblem'        Coverage problems.-`datatype'               Data types.-`deadcode'               Deadcode (like unreachable clauses or RHS).-`dotted'                 Dotted patterns.-`error'                  Errors.-`errorwarning'           Fatal warnings.-`field'                  Record fields.-`function'               Functions.-`generalizable'          Generalizable variables.-`incompletepattern'      Incomplete patterns.-`inductiveconstructor'   Inductive constructors.-`keyword'                Keywords.-`macro'                  Macros.-`markup'                 Delimiters to separate the Agda code blocks-                           from other contents.-`module'                 Module names.-`number'                 Numbers.-`operator'               Operators.-`positivityproblem'      Positivity problems.-`postulate'              Postulates.-`pragma'                 Text occurring in pragmas that does not have-                           a more specific (syntactic) aspect.-`primitive'              Primitive functions.-`primitivetype'          Primitive types (like Set and Prop).-`record'                 Record types.-`shadowingintelescope'   Shadowed repeated variable names in telescopes.-`string'                 Strings.-`symbol'                 Symbols like forall, =, ->, etc.-`terminationproblem'     Termination problems.-`typechecks'             Code which is being type-checked.-`unsolvedconstraint'     Unsolved constraints, not connected to meta-                           variables.-`unsolvedmeta'           Unsolved meta variables.")--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Variables--(defvar agda2-highlight-in-progress nil-  "If nil, then highlighting annotations are not applied.")-(make-variable-buffer-local 'agda2-highlight-in-progress)--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Functions--(defun agda2-highlight-setup nil-  "Set up the `annotation' library for use with `agda2-mode'."-  (agda2-highlight-set-faces 'agda2-highlight-face-groups agda2-highlight-face-groups)-  (setq annotation-bindings agda2-highlight-faces))--(defun agda2-highlight-apply (remove &rest cmds)-  "Adds the syntax highlighting information in the annotation list CMDS.--If REMOVE is nil, then old syntax highlighting information is not-removed. Otherwise all token-based syntax highlighting is removed."-  (let (;; Ignore read-only status, otherwise this function may fail.-        (inhibit-read-only t))-    (apply 'annotation-load-           "Click mouse-2 to jump to definition"-           remove-           cmds)))--(defun agda2-highlight-add-annotations (remove &rest cmds)-  "Like `agda2-highlight-apply'.-But only if `agda2-highlight-in-progress' is non-nil."-  (if agda2-highlight-in-progress-      (apply 'agda2-highlight-apply remove cmds)))--(defun agda2-highlight-load (file)-  "Load syntax highlighting information from FILE.--Old syntax highlighting information is not removed."-  (let* ((coding-system-for-read 'utf-8)-         (cmds (with-temp-buffer-                 (insert-file-contents file)-                 (goto-char (point-min))-                 (read (current-buffer)))))-      (apply 'agda2-highlight-apply cmds)))--(defun agda2-highlight-load-and-delete-action (file)-  "Like `agda2-highlight-load', but deletes FILE when done.-And highlighting is only updated if `agda2-highlight-in-progress'-is non-nil."-  (unwind-protect-      (if agda2-highlight-in-progress-          (agda2-highlight-load file))-    (delete-file file)))--(defun agda2-highlight-clear (&optional token-based)-  "Remove all syntax highlighting.--If TOKEN-BASED is non-nil, then only token-based highlighting is-removed."-  (interactive)-  (let ((inhibit-read-only t))-       ; Ignore read-only status, otherwise this function may fail.-    (annotation-remove-annotations token-based)))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Administrative details--(provide 'agda2-highlight)-;;; agda2-highlight.el ends here

@@ -1,3 +0,0 @@-(define-package "agda2-mode" "2.6.4"-  "interactive development for Agda, a dependently typed functional programming language"-  '((emacs "24.3"))) ;; dep defs for `annotation.el` and `eri.el` are not required if they are packaged together

@@ -1,2063 +0,0 @@-;;; agda2-mode.el --- Major mode for agda2hs-;; SPDX-License-Identifier: MIT License--;;; Commentary:--;; A major mode for editing Agda (the dependently typed programming-;; language / interactive theorem prover).-;;-;; Modified to work with agda2hs, a new backend compiling-;; lightly annotated Agda code to readable Haskell.-;;-;; Major features include:-;;-;; - syntax highlighting.-;;-;; - on the fly Agda interpretation.-;;-;; - goal-driven development-;;-;; - interactive case-splitting-;;-;; - proof search-;;-;; - input support (for utf8 characters)-;;-;; see https://agda.readthedocs.io/ for more information--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;; Dependency---;;; Code:--(defvar agda2-version "2.6.4"-  "The version of the Agda mode.-Note that the same version of the Agda executable must be used.")--(require 'cl-lib)-(require 'compile)-(require 'pp)-(require 'time-date)-(require 'eri)-(require 'annotation)-(require 'fontset)-(require 'agda-input)-(require 'agda2)-(require 'agda2-highlight)-(require 'agda2-abbrevs)-(require 'agda2-queue)-(eval-and-compile-  ;; Load filladapt, if it is installed.-  (condition-case nil-      (require 'filladapt)-    (error nil))-  (unless (fboundp 'overlays-in) (load "overlay")) ; for Xemacs-  (unless (fboundp 'propertize)                    ; for Xemacs 21.4-    ;; FIXME: XEmacs-21.4 (patch 22) does have `propertize' and so does Emacs-22-    ;; (and agda2-mode doesn't work in Emacs-21, AFAICT).-    (defun propertize (string &rest properties)-      "Return a copy of STRING with text properties added.-First argument is the string to copy.-Remaining arguments form a sequence of PROPERTY VALUE pairs for text-properties to add to the result."-      (let ((str (copy-sequence string)))-        (add-text-properties 0 (length str) properties str)-        str)))-  (unless (fboundp 'prog-mode)          ;For Emacs<24.-    (defalias 'prog-mode 'fundamental-mode)))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;; Utilities--(defmacro agda2-let (varbind funcbind &rest body)-  "Expands to (let* VARBIND (cl-labels FUNCBIND BODY...)).-Or possibly (let* VARBIND (labels FUNCBIND BODY...))."-  (declare (debug ((&rest [&or symbolp (symbolp form)])-                   (&rest (cl-defun))-                   body))-           (indent 2))-  ;; Use cl-labels if available to avoid obsolescence warnings.-  `(let* ,varbind (,(if (fboundp 'cl-labels) 'cl-labels 'labels) ,funcbind ,@body)))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;; User options--(defgroup agda2 nil-  "Major mode for interactively developing Agda programs."-  :group 'languages)--(defcustom agda2-program-name "agda2hs"-  "The name of the Agda executable."-  :type 'string-  :group 'agda2)--(defcustom agda2-program-args-  '("--disable-backend")       ; so that it doesn't complain about mixing backend with frontend-  "Command-line arguments given to the Agda executable (one per string).--Note: Do not give several arguments in the same string.--The flag \"--interaction\" is always included as the first-argument, and does not need to be listed here."-  :type '(repeat string)-  :group 'agda2)--(defvar agda2-backends '("AGDA2HS" "GHC" "GHCNoMain" "JS" "LaTeX" "QuickLaTeX")-  "Compilation backends.")--(defcustom agda2-backend-  ""-  "The backend used to compile Agda programs (leave blank to ask every time)."-  :type 'string-  :group 'agda2)--(defcustom agda2-information-window-max-height-  0.35-  "The maximum height of the information window.-A multiple of the frame height."-  :type 'number-  :group 'agda2)--(defcustom agda2-fontset-name-  (unless (or (eq window-system 'mac)-              ;; Emacs-23 uses a revamped font engine which should-              ;; make agda2-fontset-name unnecessary in most cases.-              ;; And if it turns out to be necessary, we should-              ;; probably use face-remapping-alist rather than-              ;; set-frame-font so the special font only applies to-              ;; Agda buffers, and so it applies in all frames where-              ;; Agda buffers are displayed.-              (boundp 'face-remapping-alist))-    "fontset-agda2")-  "Default font to use in the selected frame when activating the Agda mode.-This is only used if it's non-nil and Emacs is not running in a-terminal.--Note that this setting (if non-nil) affects non-Agda buffers as-well, and that you have to restart Emacs if you want settings to-this variable to take effect."-  :type '(choice (string :tag "Fontset name")-                 (const :tag "Do not change the font" nil))-  :group 'agda2)--(defcustom agda2-fontset-spec-of-fontset-agda2-    "-*-fixed-Medium-r-Normal-*-18-*-*-*-c-*-fontset-agda2,-    ascii:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO8859-1,-    latin-iso8859-2:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-2,-    latin-iso8859-3:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-3,-    latin-iso8859-4:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-4,-    cyrillic-iso8859-5:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-5,-    greek-iso8859-7:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-7,-    latin-iso8859-9:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-9,-    mule-unicode-0100-24ff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1,-    mule-unicode-2500-33ff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1,-    mule-unicode-e000-ffff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1,-    japanese-jisx0208:-Misc-Fixed-Medium-R-Normal-ja-18-*-*-*-C-*-JISX0208.1990-0,-    japanese-jisx0212:-Misc-Fixed-Medium-R-Normal-ja-18-*-*-*-C-*-JISX0212.1990-0,-    thai-tis620:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-TIS620.2529-1,-    lao:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-MuleLao-1,-    tibetan:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-160-MuleTibetan-0,-    tibetan-1-column:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-80-MuleTibetan-1,-    korean-ksc5601:-Daewoo-Mincho-Medium-R-Normal--16-120-100-100-C-160-KSC5601.1987-0,-    chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0,-    chinese-cns11643-1:-HKU-Fixed-Medium-R-Normal--16-160-72-72-C-160-CNS11643.1992.1-0,-    chinese-big5-1:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0,-    chinese-big5-2:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0"-  "Specification of the \"fontset-agda2\" fontset.-This fontset is only created if `agda2-fontset-name' is-\"fontset-agda2\" and Emacs is not run in a terminal.--Note that the text \"fontset-agda2\" has to be part of the-string (in a certain way; see the default setting) in order for the-agda2 fontset to be created properly.--Note also that the default setting may not work unless suitable-fonts are installed on your system. Refer to the README file-accompanying the Agda distribution for more details.--Note finally that you have to restart Emacs if you want settings-to this variable to take effect."-  :group 'agda2-  :type 'string)--(if (and (equal agda2-fontset-name "fontset-agda2") window-system)-    (create-fontset-from-fontset-spec agda2-fontset-spec-of-fontset-agda2 t t))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;; Global and buffer-local vars, initialization--(defvar agda2-mode-syntax-table-  (let ((tbl (make-syntax-table)))-    ;; Set the syntax of every char to "w" except for those whose default-    ;; syntax in `standard-syntax-table' is `paren' or `whitespace'.-    (map-char-table (lambda (keys val)-                      ;; `keys' here can be a normal char, a generic char-                      ;; (Emacs<23), or a char range (Emacs>=23).-                      (unless (memq (car val)-                                    (eval-when-compile-                                      (mapcar 'car-                                              (list (string-to-syntax "(")-                                                    (string-to-syntax ")")-                                                    (string-to-syntax " ")))))-                        (modify-syntax-entry keys "w" tbl)))-                    (standard-syntax-table))-    ;; Then override the remaining special cases.-    (dolist (cs '((?- . "w 12") (?\n . ">")-                  (?. . ".") (?\; . ".") (?! . ".")))-      (modify-syntax-entry (car cs) (cdr cs) tbl))-    tbl)-  "Syntax table used by the Agda mode:---   | Comment character, word constituent.-\n  | Comment ender.-.;! | Punctuation.--Remaining characters inherit their syntax classes from the-standard syntax table if that table treats them as matching-parentheses or whitespace.  Otherwise they are treated as word-constituents.")--(defconst agda2-command-table-  `(-    (agda2-load                              "\C-c\C-l"           (global)       "Load")-    (agda2-load                              "\C-c\C-x\C-l")-    (agda2-compile                           "\C-c\C-x\C-c"       (global)       "Compile")-    (agda2-quit                              "\C-c\C-x\C-q"       (global)       "Quit")-    (agda2-restart                           "\C-c\C-x\C-r"       (global)       "Kill and restart Agda")-    (agda2-abort                             "\C-c\C-x\C-a"       (global)       "Abort a command")-    (agda2-remove-annotations                "\C-c\C-x\C-d"       (global)       "Remove goals and highlighting (\"deactivate\")")-    (agda2-display-implicit-arguments        "\C-c\C-x\C-h"       (global)       "Toggle display of hidden arguments")-    (agda2-display-irrelevant-arguments      "\C-c\C-x\C-i"       (global)       "Toggle display of irrelevant arguments")-    (agda2-show-constraints                  ,(kbd "C-c C-=")     (global)       "Show constraints")-    (agda2-solve-maybe-all                   ,(kbd "C-c C-s")     (local global) "Solve constraints")-    (agda2-show-goals                        ,(kbd "C-c C-?")     (global)       "Show goals")-    (agda2-next-goal                         "\C-c\C-f"           (global)       "Next goal") ; Forward.-    (agda2-previous-goal                     "\C-c\C-b"           (global)       "Previous goal") ; Back.-    (agda2-give                              ,(kbd "C-c C-SPC")   (local)        "Give")-    (agda2-elaborate-give                    ,(kbd "C-c C-m")     (local)        "Elaborate and Give")-    (agda2-refine                            "\C-c\C-r"           (local)        "Refine")-    (agda2-auto-maybe-all                    "\C-c\C-a"           (local global) "Auto")-    (agda2-make-case                         "\C-c\C-c"           (local)        "Case")-    (agda2-goal-type                         "\C-c\C-t"           (local)        "Goal type")-    (agda2-show-context                      "\C-c\C-e"           (local)        "Context (environment)")-    (agda2-helper-function-type              "\C-c\C-h"           (local)        "Helper function type")-    (agda2-infer-type-maybe-toplevel         "\C-c\C-d"           (local global) "Infer (deduce) type")-    (agda2-why-in-scope-maybe-toplevel       "\C-c\C-w"           (local global) "Explain why a particular name is in scope")-    (agda2-goal-and-context                  ,(kbd "C-c C-,")     (local)        "Goal type and context")-    (agda2-goal-and-context-and-inferred     ,(kbd "C-c C-.")     (local)        "Goal type, context and inferred type")-    (agda2-goal-and-context-and-checked      ,(kbd "C-c C-;")     (local)        "Goal type, context and checked type")-    (agda2-search-about-toplevel             ,(kbd "C-c C-z")     (local global) "Search About")-    (agda2-module-contents-maybe-toplevel    ,(kbd "C-c C-o")     (local global) "Module contents")-    (agda2-compute-normalised-maybe-toplevel "\C-c\C-n"           (local global) "Evaluate term to normal form")-    (describe-char                           nil                  (global)       "Information about the character at point")-    (agda2-comment-dwim-rest-of-buffer       ,(kbd "C-c C-x M-;") (global)       "Comment/uncomment the rest of the buffer")-    (agda2-display-program-version           nil                  (global)       "Version")-    (agda2-set-program-version               "\C-c\C-x\C-s"       (global)       "Switch to another version of Agda")-    (eri-indent                  ,(kbd "TAB"))-    (eri-indent-reverse          [S-iso-lefttab])-    (eri-indent-reverse          [S-lefttab])-    (eri-indent-reverse          [S-tab])-    (agda2-goto-definition-mouse [mouse-2])-    (agda2-goto-definition-keyboard "\M-.")-    (agda2-go-back                  ,(if (version< emacs-version "25.1") "\M-*" "\M-,"))-    )-  "Table of commands, used to build keymaps and menus.-Each element has the form (CMD &optional KEYS WHERE DESC) where-CMD is a command; KEYS is its key binding (if any); WHERE is a-list which should contain \\='local if the command should exist in-the goal menu and \\='global if the command should exist in the main-menu; and DESC is the description of the command used in the-menus.")--(defvar agda2-mode-map-  (let ((map (make-sparse-keymap "Agda2Hs mode")))-    (define-key map [menu-bar Agda]-      (cons "Agda2Hs" (make-sparse-keymap "Agda2Hs")))-    (define-key map [down-mouse-3]  'agda2-popup-menu-3)-    (dolist (d (reverse agda2-command-table))-      (cl-destructuring-bind (f &optional keys kinds desc) d-        (if keys (define-key map keys f))-        (if (member 'global kinds)-            (define-key map-              (vector 'menu-bar 'Agda (intern desc)) (cons desc f)))))-    map)-  "Keymap for `agda2-mode'.")--(defvar agda2-goal-map-  (let ((map (make-sparse-keymap "Agda goal")))-    (dolist (d (reverse agda2-command-table))-      (cl-destructuring-bind (f &optional keys kinds desc) d-        (if (member 'local kinds)-            (define-key map-              (vector (intern desc)) (cons desc f)))))-    map)-  "Keymap for agda2 goal menu.")--(defvar agda2-info-buffer nil-  "Agda information buffer.")--(defvar agda2-process-buffer nil-  "Agda subprocess buffer.-Set in `agda2-restart'.")--(defvar agda2-process nil-  "Agda subprocess.-Set in `agda2-restart'.")--(defvar agda2-in-progress nil-  "Is the Agda process currently busy?-Valid values: `nil' (not busy), `busy' (busy),-`not-so-busy' (busy with something that should typically-terminate fairly quickly).")--;; Some buffer locals-(defvar agda2-buffer-external-status ""-  "External status of an `agda2-mode' buffer (dictated by the Haskell side).")-(make-variable-buffer-local 'agda2-buffer-external-status)--(defvar agda2-output-prompt "Agda2> "-  "The Agda2 buffer's prompt.")--(defconst agda2-help-address-  ""-  "Address accepting submissions of bug reports and questions.")--;; Annotation for a goal-;; {! .... !}-;; ----------  overlay:    agda2-gn num, face highlight, after-string num,-;;                         modification-hooks (agda2-protect-goal-markers)-;; -           text-props: category agda2-delim1-;;  -          text-props: category agda2-delim2-;;         -   text-props: category agda2-delim3-;;          -  text-props: category agda2-delim4-;;-;; Char categories for {! ... !}-(defvar agda2-open-brace  "{")-(defvar agda2-close-brace " }")-(setplist 'agda2-delim1 `(display ,agda2-open-brace))-(setplist 'agda2-delim2 `(display ,agda2-open-brace rear-nonsticky t-                                  agda2-delim2 t))-(setplist 'agda2-delim3 `(display ,agda2-close-brace agda2-delim3 t))-(setplist 'agda2-delim4 `(display ,agda2-close-brace rear-nonsticky t))--;; Note that strings used with the display property are compared by-;; reference. If the agda2-*-brace definitions were inlined, then-;; goals would be displayed as "{{ }}n" instead of "{ }n".--;; The following variables are used by the filter process,-;; `agda2-output-filter'. Their values are only modified by the filter-;; process, `agda2-go', `agda2-restart', `agda2-abort-highlighting',-;; and `agda2-abort-done'.--(defvar agda2-output-chunk-incomplete (agda2-queue-empty)-  "Buffer for incomplete lines.-\(See `agda2-output-filter'.)")-(make-variable-buffer-local 'agda2-output-chunk-incomplete)--(defvar agda2-last-responses nil-  "Response commands which should be run after other commands.-The command which arrived last is stored first in the list.")-(make-variable-buffer-local 'agda2-last-responses)--(defvar agda2-file-buffer nil-  "The Agda buffer.-Note that this variable is not buffer-local.")--(defvar agda2-in-agda2-file-buffer nil-  "Was `agda2-file-buffer' active when `agda2-output-filter' started?-Note that this variable is not buffer-local.")--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;; agda2-mode--;;;###autoload-(add-to-list 'auto-mode-alist '("\\.l?agda\\'" . agda2-mode))-;;;###autoload-(modify-coding-system-alist 'file "\\.l?agda\\'" 'utf-8)-;;;###autoload-(define-derived-mode agda2-mode prog-mode "Agda2Hs"-  "Major mode for Agda files.--The following paragraph does not apply to Emacs 23 or newer.--  Note that when this mode is activated the default font of the-  current frame is changed to the fontset `agda2-fontset-name'.-  The reason is that Agda programs often use mathematical symbols-  and other Unicode characters, so we try to provide a suitable-  default font setting, which can display many of the characters-  encountered. If you prefer to use your own settings, set-  `agda2-fontset-name' to nil.--Special commands:-\\{agda2-mode-map}"-- (if (boundp 'agda2-include-dirs)-     (display-warning 'agda2 "Note that the variable agda2-include-dirs is-no longer used. You may want to update your configuration. You-have at least two choices:-* Use the library management system.-* Set the include path using agda2-program-args.--One way to avoid seeing this warning is to make sure that-agda2-include-dirs is not bound." :warning))-- (setq local-abbrev-table agda2-mode-abbrev-table-       indent-tabs-mode   nil-       mode-line-process-         '((:eval (unless (eq 0 (length agda2-buffer-external-status))-                    (concat ":" agda2-buffer-external-status)))))- (let ((l '(max-specpdl-size    2600-            max-lisp-eval-depth 2800)))-   (while l (set (make-local-variable (pop l)) (pop l))))- (if (and window-system agda2-fontset-name)-     (condition-case nil-         (set-frame-font agda2-fontset-name)-       (error (error "Unable to change the font; change agda2-fontset-name or tweak agda2-fontset-spec-of-fontset-agda2"))))- ;; Deactivate highlighting if the buffer is edited before- ;; typechecking is complete.- (add-hook 'first-change-hook 'agda2-abort-highlighting nil 'local)- ;; If Agda is not running syntax highlighting does not work properly.- (unless (eq 'run (agda2-process-status))-   (agda2-restart))- ;; Make sure that Font Lock mode is not used.- (font-lock-mode 0)- (agda2-highlight-setup)- (condition-case err-     (agda2-highlight-reload)-   (error (message "Highlighting not loaded: %s"-                   (error-message-string err))))- (agda2-comments-and-paragraphs-setup)- (force-mode-line-update)- ;; Protect global value of default-input-method from set-input-method.- (make-local-variable 'default-input-method)- ;; Don't take script into account when determining word boundaries- (set (make-local-variable 'word-combining-categories) (cons '(nil . nil) word-combining-categories))- (set-input-method "Agda")- ;; Highlighting etc. is removed when we switch from the Agda mode.- ;; Use case: When a file M.lagda with a local variables list- ;; including "mode: latex" is loaded chances are that the Agda mode- ;; is activated before the LaTeX mode, and the LaTeX mode does not- ;; seem to remove the text properties set by the Agda mode.- (add-hook 'change-major-mode-hook 'agda2-quit nil 'local))--(defun agda2-restart ()-  "Tries to start or restart the Agda process."-  (interactive)--  ;; Kill any running instance of the Agda process.-  (condition-case nil-      (agda2-term)-    (error nil))--  ;; Check that the right version of Agda is used.-  (let* ((coding-system-for-read 'utf-8)-         (output (with-output-to-string-                   (call-process agda2-program-name-                                 nil standard-output nil "--version")))-         (version (and (string-match "^Agda version \\([0-9.]+\\)" output)-                       (match-string 1 output))))-    (unless (equal version agda2-version)-      (error "The Agda mode's version (%s) does not match that of %s (%s)."-             agda2-version-             agda2-program-name (or version "unknown"))))--  (let ((all-program-args (cons "--interaction" agda2-program-args)))--    ;; Check that the arguments are not malformed.-    (let* ((coding-system-for-read 'utf-8)-           (status)-           (output-            (with-output-to-string-              (setq status-                    (apply 'call-process agda2-program-name-                           nil standard-output nil all-program-args)))))-      (unless (equal status 0)-        (error "Failed to start the Agda process:\n%s" output)))--    ;; Start the Agda process.-    (let ((agda2-bufname "*agda2*"))--      (let ((process-connection-type nil)) ; Pipes are faster than PTYs.-        (setq agda2-process-              (apply 'start-process "Agda2" agda2-bufname-                     agda2-program-name all-program-args)))--      (set-process-coding-system agda2-process 'utf-8 'utf-8)-      (set-process-query-on-exit-flag agda2-process nil)-      (set-process-filter agda2-process 'agda2-output-filter)-      (setq agda2-in-progress nil-            agda2-file-buffer (current-buffer))--      (with-current-buffer agda2-bufname-        (setq agda2-process-buffer (current-buffer)-              mode-name            "Agda executable"-              agda2-last-responses nil)-        (set-buffer-file-coding-system 'utf-8))--      (agda2-remove-annotations))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;; Communicating with Agda--(defun agda2-raise-error ()-  "Raises an error.-The error message directs the user to the *agda2* buffer."-  (error "Problem encountered. The *agda2* buffer can perhaps explain why."))--(defun agda2-running-p nil-  "Does the *agda2* buffer exist, and is the Agda2 process running?"-  (and (buffer-live-p agda2-process-buffer)-       (eq (agda2-process-status) 'run)))--(defun agda2-send-command (restart &rest args)-  "Send a command to the Agda process.-Sends the list of strings ARGS to the process. If RESTART is-non-nil and the process is not running, or the *agda2*-buffer does not exist, then an attempt is made to restart the-process."-  (when (and restart (not (agda2-running-p)))-    ;; Try restarting automatically, but only once, in case there is-    ;; some major problem.-    (agda2-restart)-    (unless (agda2-running-p)-      (agda2-raise-error)))-  (let ((command (apply 'concat (agda2-intersperse " " args))))-    (with-current-buffer agda2-process-buffer-      (goto-char (point-max))-      (insert command)-      (insert "\n")-      (process-send-string agda2-process (concat command "\n")))))--(defun agda2-go (save highlight how-busy do-abort &rest args)-  "Executes commands in the Agda2 interpreter.-Sends the list of strings ARGS to the Agda2 interpreter, waits-for output and executes the responses, if any.--If SAVE is \\='save, then the buffer is saved first.--If HIGHLIGHT is non-nil, then the buffer's syntax highlighting-may be updated. This is also the case if the Agda process is-busy (or `not-so-busy') and `agda2-highlight-in-process' is-non-nil.--The value HOW-BUSY should be `busy' if it should not be possible-to invoke other commands while this command is running (with the-exception of commands for which DO-ABORT is nil). Otherwise it-should be `not-so-busy' (which should only be used for commands-that typically terminate fairly quickly).--If the Agda process is busy (or `not-so-busy'), and the current-buffer does not match `agda2-file-buffer', then the command is-not executed and an error is raised. The same applies if DO-ABORT-is non-nil and the Agda process is `busy'."--  ; Check that how-busy is well-formed.-  (cl-assert (or (equal how-busy 'busy)-              (equal how-busy 'not-so-busy)))--  (when (and agda2-in-progress-             (not (equal agda2-file-buffer-                         (current-buffer))))-    (error "Agda is busy with something in the buffer %s"-           agda2-file-buffer))--  (when (and do-abort-             (equal agda2-in-progress 'busy))-    (error "Agda is busy with something-\(you have the option to abort or restart Agda)"))--  (setq agda2-file-buffer (current-buffer))--  (setq agda2-highlight-in-progress-        (or highlight-            (and agda2-in-progress-                 agda2-highlight-in-progress)))--  (unless agda2-in-progress-    (setq agda2-output-chunk-incomplete (agda2-queue-empty)))--  (setq agda2-in-progress-        (if (or (equal how-busy 'busy)-                (equal agda2-in-progress 'busy))-            'busy-          'not-so-busy))--  (when (equal save 'save) (save-buffer))--  (apply 'agda2-send-command-         'restart-         "IOTCM"-         (agda2-string-quote (buffer-file-name))-         (if highlight (agda2-highlight-level) "None")-         "Indirect"-         "("-         (append args '(")"))))--(defun agda2-abort ()-  "Tries to abort the current computation, if any.-May be more efficient than restarting Agda."-  (interactive)-  (agda2-send-command nil-                      "IOTCM"-                      (agda2-string-quote (buffer-file-name))-                      "None"-                      "Indirect"-                      "Cmd_abort"))--(defun agda2-abort-done ()-  "Resets certain variables.-Intended to be used by the backend if an abort command was-successful."-  (agda2-info-action "*Aborted*" "Aborted." t)-  (setq agda2-highlight-in-progress nil-        agda2-last-responses        nil))--(defun agda2-output-filter (proc chunk)-  "Evaluate the Agda process's commands.-This filter function assumes that every line contains either some-kind of error message (which cannot be parsed as a list), or-exactly one command. Incomplete lines are stored in a-buffer (`agda2-output-chunk-incomplete').--Every command is run by this function, unless it has the form-\"(('last . priority) . cmd)\", in which case it is run by-`agda2-run-last-commands' at the end, after the Agda2 prompt-has reappeared, after all non-last commands, and after all-interactive highlighting is complete. The last commands can have-different integer priorities; those with the lowest priority are-executed first.--Non-last commands should not call the Agda process.--All commands are echoed to the *agda2* buffer, with the exception-of commands of the form \"(agda2-highlight-... ...)\".--The non-last commands are run in the order in which they appear.--When the prompt has been reached highlighting annotations are-reloaded from `agda2-highlighting-file', unless-`agda2-highlighting-in-progress' is nil."--  ;; Beware: the buffer may have been killed in the mean time.  E.g. when-  ;; viewing an attachment containing Agda code in Gnus, Gnus will-  ;; create a temp buffer, set it in agda2-mode, call font-lock-ensure on it-  ;; (which won't know that it needs to wait for some process to reply), then-  ;; extract the fontified text and kill the temp buffer; so when Agda-  ;; finally answers, the temp buffer is long gone.-  (when (buffer-live-p agda2-file-buffer)-  (setq agda2-in-agda2-file-buffer-        (and agda2-file-buffer-             (equal (current-buffer) agda2-file-buffer)))-  (let (;; The input lines in the current chunk.-        (lines (split-string chunk "\n"))--        ;; Non-last commands found in the current chunk (reversed).-        (non-last-commands ())--        ;; Last incomplete line, if any.-        (output-chunk-incomplete ""))-    (with-current-buffer agda2-file-buffer-      (when (consp lines)-        (agda2-queue-enqueue agda2-output-chunk-incomplete (pop lines))-        (when (consp lines)-          ;; The previous uncomplete chunk is now complete.-          (push (agda2-queue-to-string agda2-output-chunk-incomplete)-                lines)--          ;; Stash away the last incomplete line, if any. (Note that-          ;; (split-string "...\n" "\n") evaluates to (... "").)-          (setq output-chunk-incomplete (car (last lines))-                agda2-output-chunk-incomplete-                (agda2-queue-from-string output-chunk-incomplete))--          ;; Handle every complete line.-          (dolist (line (butlast lines))-            (let* (;; The command. Lines which cannot be parsed as a single-                   ;; list, without any junk, are ignored.-                   (cmd (condition-case nil-                            (let ((result (read-from-string line)))-                              (if (and (listp (car result))-                                       (= (cdr result) (length line)))-                                  (car result)))-                          (error nil)))-                   (is-highlighting-command-                    (and cmd-                         (symbolp (car cmd))-                         (let ((case-fold-search nil))-                           (string-match "^agda2-highlight-"-                                         (symbol-name (car cmd)))))))--              ;; Do not echo highlighting commands.-              (unless is-highlighting-command-                (with-current-buffer agda2-process-buffer-                  (save-excursion-                    (goto-char (point-max))-                    (insert line)-                    (insert "\n"))))-              (when cmd-                (if (equal 'last (car-safe (car cmd)))-                    (push (cons (cdr (car cmd)) (cdr cmd))-                          agda2-last-responses)-                  (push cmd non-last-commands)))))--          ;; Run non-last commands.-          (mapc 'agda2-exec-response (nreverse non-last-commands)))--        ;; Check if the prompt has been reached. This function assumes-        ;; that the prompt does not include any newline characters.-        (when (agda2-queue-is-prefix-of agda2-output-prompt-                                        agda2-output-chunk-incomplete)-          (with-current-buffer agda2-process-buffer-            (insert output-chunk-incomplete))-          (setq agda2-output-chunk-incomplete (agda2-queue-empty)-                agda2-in-progress nil-                agda2-last-responses (nreverse agda2-last-responses))--          (agda2-run-last-commands)))))))--(defun agda2-run-last-commands nil-  "Execute the last commands in the right order.-\(After the prompt has reappeared.) See `agda2-output-filter'."--  ;; with-current-buffer is used repeatedly below, because some last-  ;; commands may switch the focus to another buffer.--  (while (with-current-buffer agda2-file-buffer-           (and (not agda2-in-progress) (consp agda2-last-responses)))-    (with-current-buffer agda2-file-buffer-      ;; The list is sorted repeatedly because this function may be-      ;; called recursively (via `agda2-exec-response').-      (setq agda2-last-responses (sort agda2-last-responses-                                       (lambda (x y) (<= (car x) (car y)))))-      (let ((r (pop agda2-last-responses)))-        (agda2-exec-response (cdr r)))))--  ;; Unset agda2-highlight-in-progress when all the asynchronous-  ;; commands have terminated.-  (unless agda2-in-progress-      (setq agda2-highlight-in-progress nil)))--(defun agda2-abort-highlighting nil-  "Abort any interactive highlighting.-This function should be used in `first-change-hook'."-  (when agda2-highlight-in-progress-    (setq agda2-highlight-in-progress nil)-    (message "\"%s\" has been modified. Interrupting highlighting."-             (buffer-name (current-buffer)))))--(defun agda2-goal-cmd (cmd save &optional want ask &rest args)-  "Reads input from goal or minibuffer and sends command to Agda.--An error is raised if point is not in a goal.--The command sent to Agda is--  CMD <goal number> <goal range> <user input> ARGS.--The user input is computed as follows:--* If WANT is nil, then the user input is the empty string.--* If WANT is a string, and either ASK is non-nil or the goal only-  contains whitespace, then the input is taken from the-  minibuffer. In this case WANT is used as the prompt string.--* Otherwise (including if WANT is \\='goal) the goal contents are-  used.--If the user input is not taken from the goal, then an empty goal-range is given.--If SAVE is \\='save, then the buffer is saved just before the-command is sent to Agda (if it is sent)."-  (cl-multiple-value-bind (o g) (agda2-goal-at (point))-    (unless g (error "For this command, please place the cursor in a goal"))-    (let ((txt (buffer-substring-no-properties (+ (overlay-start o) 2)-                                               (- (overlay-end   o) 2)))-          (input-from-goal nil))-      (cond ((null want) (setq txt ""))-            ((and (stringp want)-                  (or ask (string-match "\\`\\s *\\'" txt)))-             (setq txt (read-string (concat want ": ") nil nil txt t)))-            (t (setq input-from-goal t)))-      (apply 'agda2-go save input-from-goal 'busy t cmd-             (format "%d" g)-             (if input-from-goal (agda2-goal-Range o) (agda2-mkRange nil))-             (agda2-string-quote txt) args))))--;; Note that the following function is a security risk, since it-;; evaluates code without first inspecting it. The code (supposedly)-;; comes from the Agda backend, but there could be bugs in the backend-;; which can be exploited by an attacker which manages to trick-;; someone into type-checking compromised Agda code.--(defun agda2-exec-response (response)-  "Interprets response."-  (let ((inhibit-read-only t))-    (eval response)))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;; User commands and response processing--(defun agda2-load ()-  "Load current buffer."-  (interactive)-  (agda2-go 'save t 'busy t "Cmd_load"-            (agda2-string-quote (buffer-file-name))-            (agda2-list-quote agda2-program-args)-            ))--(defun agda2-compile ()-  "Compile the current module.--The variable `agda2-backend' determines which backend is used."-  (interactive)-  (let ((backend (cond ((equal agda2-backend "MAlonzo")       "GHC")-                       ((equal agda2-backend "MAlonzoNoMain") "GHCNoMain")-                       ((equal agda2-backend "")-                        (completing-read "Backend: " agda2-backends-                                         nil nil nil nil nil-                                         'inherit-input-method))-                       (t agda2-backend))))-    (when (equal backend "") (error "No backend chosen"))-    (agda2-go 'save t 'busy t "Cmd_compile"-              backend-              (agda2-string-quote (buffer-file-name))-              (agda2-list-quote agda2-program-args)-              )))--(defmacro agda2-maybe-forced (name comment cmd save want)-  "This macro constructs a function NAME which runs CMD.-COMMENT is used to build the function's comment. The function-NAME takes a prefix argument which tells whether it should-apply force or not when running CMD (through-`agda2-goal-cmd';-SAVE is used as `agda2-goal-cmd's SAVE argument and-WANT is used as `agda2-goal-cmd's WANT argument)."-  (let ((eval (make-symbol "eval")))-  `(defun ,name (&optional prefix)-     ,(concat comment ".--The action depends on the prefix argument:--* If the prefix argument is `nil' (i.e., if no prefix argument is-  given), then no force is applied.--* If any other prefix argument is used (for instance, if C-u is-  typed once or twice right before the command is invoked), then-  force is applied.")-     (interactive "P")-     (let ((,eval (cond ((equal prefix nil) "WithoutForce")-                        ("WithForce"))))-       (agda2-goal-cmd (concat ,cmd " " ,eval)-                       ,save ,want)))))--(agda2-maybe-forced-  agda2-give-  "Give to the goal at point the expression in it"-  "Cmd_give"-  'save-  "expression to give")--;; (defun agda2-give()-;;   "Give to the goal at point the expression in it" (interactive)-;;   (agda2-goal-cmd "Cmd_give" 'save "expression to give"))--(defun agda2-give-action (old-g paren)-  "Update the goal OLD-G with the expression in it."-  (let-     ;; Don't run modification hooks: we don't want this to-      ;; trigger agda2-abort-highlighting.-      ((inhibit-modification-hooks t))-  (agda2-update old-g paren)))--(defun agda2-refine (pmlambda)-  "Refine the goal at point.-If the goal contains an expression e, and some \"suffix\" of the-type of e unifies with the goal type, then the goal is replaced-by e applied to a suitable number of new goals.--PMLAMBDA is only used if the goal has a functional type.-When the prefix argument is given a pattern maching lambda will-be inserted, otherwise a standard lambda will be used.--If the goal is empty, the goal type is a data type, and there is-exactly one constructor which unifies with this type, then the-goal is replaced by the constructor applied to a suitable number-of new goals."-  (interactive "P")-  (if pmlambda-      (agda2-goal-cmd "Cmd_refine_or_intro True" 'save 'goal)-    (agda2-goal-cmd "Cmd_refine_or_intro False" 'save 'goal)))--(defun agda2-autoOne ()- "Simple proof search" (interactive)- (agda2-goal-cmd "Cmd_autoOne" 'save 'goal))--(defun agda2-autoAll ()-  "Solves all goals by simple proof search."-  (interactive)-  (agda2-go nil nil 'busy t "Cmd_autoAll")-)--(defun agda2-make-case ()-  "Refine the pattern variables given in the goal.-Assumes that <clause> = {!<variables>!} is on one line."-  (interactive)-  (agda2-goal-cmd "Cmd_make_case" 'save "pattern variables to case (empty for split on result)"))--(defun agda2-make-case-action (newcls)-  "Replace the line at point with new clauses NEWCLS and reload."-  (agda2-forget-all-goals);; we reload later anyway.-  (let* ((p0 (point))-         (p1 (goto-char (+ (current-indentation) (line-beginning-position))))-         (indent (current-column))-         cl)-    (delete-region p1 (line-end-position))-    (while (setq cl (pop newcls))-      (insert cl)-      (if newcls (insert "\n" (make-string indent ?  ))))-    (goto-char p0))-  (agda2-load))--(defun agda2-make-case-action-extendlam (newcls)-  "Replace definition of extended lambda with new clauses NEWCLS and reload."-  (agda2-forget-all-goals);; we reload later anyway.-  (let* ((p0 (point))-         (pmax (re-search-forward "!}"))-         (bracketCount 0)-         (p1 (goto-char (+ (current-indentation) (line-beginning-position))))-         (indent (current-column))-         cl)-    (goto-char p0)-    (re-search-backward "{!")-    (while (and (not (equal (preceding-char) ?\;)) (>= bracketCount 0) (> (point) p1))-      (backward-char)-      (if (equal (preceding-char) ?}) (cl-incf bracketCount))-      (if (equal (preceding-char) ?{) (cl-decf bracketCount)))-    (let* ((is-lambda-where (= (point) p1))-           (p (point)))-      (delete-region (point) pmax)-      (if (not is-lambda-where) (insert " "))-      (while (setq cl (pop newcls))-        (insert cl)-        (if newcls (if is-lambda-where (insert "\n" (make-string indent ? )) (insert " ; "))))-      (goto-char p)))-  (agda2-load))--(defun agda2-status-action (status)-  "Display the string STATUS in the current buffer's mode line.-\(precondition: the current buffer has to use the Agda mode as the-major mode)."-  (setq agda2-buffer-external-status status)-  (force-mode-line-update))--(defmacro agda2-information-buffer (buffer kind title)-  "Used to define functions like `agda2-info-buffer'."-  `(defun ,buffer nil-     ,(concat "Creates the Agda " kind-              " buffer, if it does not already exist.-The buffer is returned.")-  (unless (buffer-live-p ,buffer)-    (setq ,buffer-          (generate-new-buffer ,title))--    (with-current-buffer ,buffer-      (compilation-mode "AgdaInfo")-      ;; Support for jumping to positions mentioned in the text.-      (set (make-local-variable 'compilation-error-regexp-alist)-           '(("\\([\\\\/][^[:space:]]*\\):\\([0-9]+\\),\\([0-9]+\\)-\\(\\([0-9]+\\),\\)?\\([0-9]+\\)"-              1 (2 . 5) (3 . 6))))-      ;; Do not skip errors that start in the same position as the-      ;; current one.-      (set (make-local-variable 'compilation-skip-to-next-location) nil)-      ;; No support for recompilation. The key binding is removed, and-      ;; attempts to run `recompile' will (hopefully) result in an-      ;; error.-      (let ((map (copy-keymap (current-local-map))))-        (define-key map (kbd "g") 'undefined)-        (use-local-map map))-      (set (make-local-variable 'compile-command)-           'agda2-does-not-support-compilation-via-the-compilation-mode)--      (set-syntax-table agda2-mode-syntax-table)-      (set (make-local-variable 'word-combining-categories) (cons '(nil . nil) word-combining-categories))-      (set-input-method "Agda")))--  ,buffer))--(agda2-information-buffer agda2-info-buffer "info" "*Agda information*")--(defun agda2-info-action (name text &optional append)-  "Insert TEXT into the Agda info buffer and display it.-NAME is displayed in the buffer's mode line.--If APPEND is non-nil, then TEXT is appended at the end of the-buffer, and point placed after this text.--If APPEND is nil, then any previous text is removed before TEXT-is inserted, and point is placed before this text."-  (interactive)-  (let ((buf (agda2-info-buffer)))-    (with-current-buffer buf-      ;; In some cases the jump-to-position-mentioned-in-text-      ;; functionality (see compilation-error-regexp-alist above)-      ;; didn't work: Emacs jumped to the wrong position. However, it-      ;; seems to work if compilation-forget-errors is used. This-      ;; problem may be related to Emacs bug #9679-      ;; (http://debbugs.gnu.org/cgi/bugreport.cgi?bug=9679). The idea-      ;; to use compilation-forget-errors comes from a comment due to-      ;; Oleksandr Manzyuk-      ;; (https://github.com/haskell/haskell-mode/issues/67).-      (compilation-forget-errors)-      (unless append (erase-buffer))-      (save-excursion-        (goto-char (point-max))-        (insert text))-      (put-text-property 0 (length name) 'face '(:weight bold) name)-      (setq mode-line-buffer-identification name)-      (force-mode-line-update))-    ;; If the current window displays the information buffer, then the-    ;; window configuration is left untouched.-    (unless (equal (window-buffer) buf)-      (let ((agda-window-              (and agda2-file-buffer-                   (car-safe-                     ;; All windows, including minibuffers, on any-                     ;; frame on the current terminal, displaying the-                     ;; present Agda file buffer.-                     (get-buffer-window-list agda2-file-buffer t 0)))))-        (save-selected-window-          ;; Select a window displaying the Agda file buffer (if such-          ;; a window exists). With certain configurations of-          ;; display-buffer this should increase the likelihood that-          ;; the info buffer will be displayed on the same frame.-          (when agda-window-            (select-window agda-window 'no-record))-          (let* (;; If there is only one window, then the info window-                 ;; should be created above or below the code window,-                 ;; not to the left or right.-                 (split-width-threshold nil)-                 (window-                   (display-buffer-                     buf-                     ;; Under Emacs 23 the effect of the following-                     ;; argument is only that the current window-                     ;; should not be used.-                     '(nil-                       .-                       (;; Do not use the same window.-                        (inhibit-same-window . t)-                        ;; Do not raise or select another frame.-                        (inhibit-switch-frame . t))))))-            (if window-                (fit-window-to-buffer window-                  (truncate-                    (* (frame-height)-                       agda2-information-window-max-height))))))))-    ;; Move point in every window displaying the information buffer.-    ;; Exception: If we are appending, don't move point in selected-    ;; windows.-    (dolist (window (get-buffer-window-list buf 'no-minibuffer t))-      (unless (and append-                   (equal window (selected-window)))-        (with-selected-window window-          (if append-              (goto-char (point-max))-            (goto-char (point-min))))))))--(defun agda2-info-action-and-copy (name text &optional append)-  "Same as agda2-info-action but also puts TEXT in the kill ring."-  (kill-new text)-  (agda2-info-action name text append))--(defun agda2-show-constraints()-  "Show constraints." (interactive)-  (agda2-go nil t 'busy t "Cmd_constraints"))--(defun agda2-remove-annotations ()-  "Removes buffer annotations (overlays and text properties)."-  (interactive)-  (dolist (o (overlays-in (point-min) (point-max)))-    (delete-overlay o))-  (let ((inhibit-read-only t))-    (annotation-preserve-mod-p-and-undo-     (set-text-properties (point-min) (point-max) '()))-    (force-mode-line-update)))--(defun agda2-next-goal ()     "Go to the next goal, if any."     (interactive)-  (agda2-mv-goal 'next-single-property-change     'agda2-delim2 1 (point-min)))-(defun agda2-previous-goal () "Go to the previous goal, if any." (interactive)-  (agda2-mv-goal 'previous-single-property-change 'agda2-delim3 0 (point-max)))-(defun agda2-mv-goal (change delim adjust wrapped)-  (agda2-let ()-      ((go (p) (while (and (setq p (funcall change p 'category))-                           (not (eq (get-text-property p 'category) delim))))-           (if p (goto-char (+ adjust p)))))-    (or (go (point)) (go wrapped) (message "No goals in the buffer"))))--(defun agda2-quit ()-  "Quit and clean up after agda2."-  (interactive)-  (remove-hook 'first-change-hook 'agda2-abort-highlighting 'local)-  (remove-hook 'after-save-hook 'agda2-highlight-tokens 'local)-  (agda2-remove-annotations)-  (agda2-term))--(defun agda2-term (&optional nicely)-  "Interrupt the Agda process and kill its buffer.-If this function is invoked with a prefix argument, then Agda is-asked nicely to terminate itself after any previously invoked-commands have completed."-  (interactive "P")-  (if nicely-      (progn-        ;; Set up things so that if the Agda process terminates, then-        ;; its buffer is killed.-        (when (and agda2-process-                   (process-status agda2-process))-          (set-process-sentinel agda2-process 'agda2-kill-process-buffer))-        ;; Kill the process buffer if the Agda process has already-        ;; been killed.-        (agda2-kill-process-buffer)-        ;; Try to kill the Agda process.-        (agda2-send-command nil-                            "IOTCM"-                            (agda2-string-quote (buffer-file-name))-                            "None"-                            "Indirect"-                            "Cmd_exit"))-    ;; Try to kill the Agda process and the process buffer.-    (when (and agda2-process-               (process-status agda2-process))-      (interrupt-process agda2-process))-    (when (buffer-live-p agda2-process-buffer)-      (kill-buffer agda2-process-buffer))))--(defun agda2-kill-process-buffer (&optional process event)-  "Kills the Agda process buffer, if any.-But only if the Agda process does not exist or has terminated.--This function can be used as a process sentinel."-  (when (and (or (null agda2-process)-                 (member (process-status agda2-process)-                         '(exit signal failed nil)))-             (buffer-live-p agda2-process-buffer))-    (kill-buffer agda2-process-buffer)))--(cl-defmacro agda2--with-gensyms ((&rest names) &body body)-  "Bind NAMES to fresh symbols in BODY"-  (declare (indent 1))-  `(let ,(cl-loop for x in names collecting `(,x (make-symbol (symbol-name',x))))-     ,@body))--;; This macro is meant to be used to generate other macros which define-;; functions which can be used either directly from a goal or at a global-;; level and are modifiable using one of three levels of normalisation.--(defmacro agda2-proto-maybe-normalised (name comment cmd norm0 norm1 norm2 norm3 spec)-  "This macro constructs a function NAME which runs CMD.-COMMENT is used to build the function's comment.-The function NAME takes a prefix argument which tells whether it-should normalise types according to either NORM0, NORM1, NORM2, or NORM3-when running CMD through `agda2-goal-cmd`.-SPEC can be either (fromgoal want) or (global prompt).-"--  ;; Names bound in a macro should be ``uninterned'' to avoid name capture-  ;; We use the macro `agda2--with-gensyms' to bind these.-  (agda2--with-gensyms (eval prefix args)-    `(defun ,name (,prefix &rest ,args)-       ,(format "%s.--The form of the result depends on the prefix argument:--* If the prefix argument is `nil' (i.e., if no prefix argument is-  given), then the result is %s.--* If the prefix argument is `(4)' (for instance if C-u is typed-  exactly once right before the command is invoked), then the-  result is %s.--* If the prefix argument is `(16)' (for instance if C-u is typed-  exactly twice right before the command is invoked), then the-  result is %s.--* If any other prefix argument is used (for instance if C-u is-  typed thrice right before the command is invoked), then the-  result is %s." comment (nth 1 norm0) (nth 1 norm1) (nth 1 norm2) (nth 1 norm3))--       ;; All the commands generated by the macro are interactive.-       ;; Those called from a goal, grab the value present there (if any)-       ;; Whereas those called globally always use a prompt-       (interactive ,(pcase spec-                       (`(fromgoal ,want)-                        "P")-                       (`(global ,prompt)-                        (if prompt-                            (concat "P\nM" prompt ": ")-                          "P"))))-       ;; Depending on the prefix's value we pick one of the three-       ;; normalisation levels-       (let ((,eval (cond ((null ,prefix)-                           ,(car norm0))-                          ((equal ,prefix '(4))-                           ,(car norm1))-                          ((equal ,prefix '(16))-                           ,(car norm2))-                          (t ,(car norm3)))))-       ;; Finally, if the command is called from a goal, we use `agda2-goal-cmd'-       ;; Otherwise we resort to `agda2-go'-         ,(pcase spec-            (`(fromgoal ,want)-             `(agda2-goal-cmd (concat ,cmd " " ,eval) nil ,want))-            (`(global ,prompt)-             `(agda2-go nil t 'busy t-                        (concat ,cmd " "-                                ,eval " "-                                (if ,prompt-                                    (agda2-string-quote (car ,args))-                                    "")))))))))--(defmacro agda2-maybe-normalised (name comment cmd want)-  `(agda2-proto-maybe-normalised-    ,name ,comment ,cmd-    ("Simplified"   "simplified")-    ("Instantiated" "neither explicitly normalised nor simplified")-    ("Normalised"   "normalised")-    ("HeadNormal"   "head normalised")-    (fromgoal ,want)))--(defmacro agda2-maybe-normalised-asis (name comment cmd want)-  `(agda2-proto-maybe-normalised-    ,name ,comment ,cmd-    ("AsIs"       "returned as is")-    ("Simplified" "simplified")-    ("Normalised" "normalised")-    ("HeadNormal" "head normalised")-    (fromgoal ,want)))--(defmacro agda2-maybe-normalised-toplevel (name comment cmd prompt)-  `(agda2-proto-maybe-normalised-    ,name ,comment ,cmd-    ("Simplified"   "simplified")-    ("Instantiated" "neither explicitly normalised nor simplified")-    ("Normalised"   "normalised")-    ("HeadNormal"   "head normalised")-    (global ,prompt)))--(defmacro agda2-maybe-normalised-toplevel-asis-noprompt (name comment cmd)-  `(agda2-proto-maybe-normalised-    ,name ,comment ,cmd-    ("AsIs"       "returned as is")-    ("Simplified" "simplified")-    ("Normalised" "normalised")-    ("HeadNormal" "head normalised")-    (global nil)))--(agda2-maybe-normalised- agda2-goal-type- "Show the type of the goal at point"- "Cmd_goal_type"- nil)--(agda2-maybe-normalised- agda2-infer-type- "Infer the type of the goal at point"- "Cmd_infer"- "expression to type")--(agda2-maybe-normalised-toplevel-   agda2-infer-type-toplevel-   "Infers the type of the given expression. The scope used for-the expression is that of the last point inside the current-top-level module"-   "Cmd_infer_toplevel"-   "Expression")--(defun agda2-infer-type-maybe-toplevel ()-  "Infers the type of the given expression.-Either uses the scope of the current goal or, if point is not in a goal, the-top-level scope."-  (interactive)-  (call-interactively (if (agda2-goal-at (point))-                          'agda2-infer-type-                        'agda2-infer-type-toplevel)))--(defun agda2-why-in-scope ()-  "Explain why something is in scope in a goal."-  (interactive)-  (agda2-goal-cmd "Cmd_why_in_scope" nil "Name"))--(defun agda2-why-in-scope-toplevel (name)-  "Explain why something is in scope at the top level."-  (interactive "MName: ")-  (agda2-go nil t 'busy t-            "Cmd_why_in_scope_toplevel"-            (agda2-string-quote name)))--(defun agda2-why-in-scope-maybe-toplevel ()-  "Explains why a given name is in scope."-  (interactive)-  (call-interactively (if (agda2-goal-at (point))-                          'agda2-why-in-scope-                          'agda2-why-in-scope-toplevel)))--(agda2-maybe-normalised- agda2-elaborate-give- "Elaborate check the given expression against the hole's type and fill in the- hole with the elaborated term"- "Cmd_elaborate_give"- "expression to elaborate and give")--(agda2-maybe-normalised- agda2-goal-and-context- "Shows the type of the goal at point and the currect context"- "Cmd_goal_type_context"- nil)--(agda2-maybe-normalised- agda2-goal-and-context-and-inferred- "Shows the context, the goal and the given expression's inferred type"- "Cmd_goal_type_context_infer"- "expression to type")--(agda2-maybe-normalised- agda2-goal-and-context-and-checked- "Shows the context, the goal and check the given expression's against- the hole's type"- "Cmd_goal_type_context_check"- "expression to type")--(agda2-maybe-normalised- agda2-show-context- "Show the context of the goal at point"- "Cmd_context"- nil)--(agda2-maybe-normalised-asis- agda2-helper-function-type-  "Compute the type of a hypothetical helper function."-  "Cmd_helper_function"-  "Expression")--(agda2-maybe-normalised-  agda2-module-contents-  "Shows all the top-level names in the given module.-Along with their types."-  "Cmd_show_module_contents"-  "Module name (empty for current module)")--(agda2-maybe-normalised-toplevel-  agda2-module-contents-toplevel-  "Shows all the top-level names in the given module.-Along with their types."-  "Cmd_show_module_contents_toplevel"-  "Module name (empty for top-level module)"-)--(agda2-maybe-normalised-toplevel-  agda2-search-about-toplevel-  "Search About an identifier"-  "Cmd_search_about_toplevel"-  "Name"-)--(defun agda2-module-contents-maybe-toplevel ()-  "Shows all the top-level names in the given module.-Along with their types.--Uses either the scope of the current goal or, if point is not in-a goal, the top-level scope."-  (interactive)-  (call-interactively (if (agda2-goal-at (point))-                          'agda2-module-contents-                        'agda2-module-contents-toplevel)))--(defun agda2-solve-maybe-all ()-  "Solves goals that are already instantiated internally.-Either only one if point is a goal, or all of them."-  (interactive)-  (call-interactively (if (agda2-goal-at (point))-                          'agda2-solveOne-                          'agda2-solveAll))-)--(defun agda2-auto-maybe-all ()-  "Run auto.-Either only one if point is a goal, or all of them."-  (interactive)-  (call-interactively (if (agda2-goal-at (point))-                          'agda2-autoOne-                          'agda2-autoAll))-)--(agda2-maybe-normalised-toplevel-asis-noprompt- agda2-show-goals- "Show all goals."- "Cmd_metas"- )--(agda2-maybe-normalised-toplevel-asis-noprompt- agda2-solveAll- "Solves all goals that are already instantiated internally."- "Cmd_solveAll"- )--(agda2-maybe-normalised-  agda2-solveOne-  "Solves the goal at point if it is already instantiated internally"-  "Cmd_solveOne"-  nil-)--(defun agda2-solveAll-action (iss)-  (while iss-    (let* ((g (pop iss)) (txt (pop iss))-           (cmd (cons 'agda2-solve-action (cons g (cons txt nil)))))-      (if (null agda2-last-responses)-          (push (cons 1 cmd) agda2-last-responses)-        (nconc agda2-last-responses (cons (cons 3 cmd) nil))))))--(defun agda2-solve-action (g txt)-  (save-excursion-    (agda2-replace-goal g txt)-    (agda2-goto-goal g)-    (agda2-give)))--(defun agda2-compute-normalised (&optional arg)-  "Compute the normal form of the expression in the goal at point.--With the prefix argument `(4)' \"abstract\" is ignored during the-computation.--With a prefix argument `(16)' the normal form of-\"show <expression>\" is computed, and then the resulting string-is printed.--With any other prefix the head normal form is computed."-  (interactive "P")-  (let ((cmd (concat "Cmd_compute"-                      (cond ((equal arg nil) " DefaultCompute")-                            ((equal arg '(4)) " IgnoreAbstract")-                            ((equal arg '(16)) " UseShowInstance")-                            (" HeadCompute")))))-    (agda2-goal-cmd cmd nil "expression to normalise")))--(defun agda2-compute-normalised-toplevel (expr &optional arg)-  "Compute the normal form of the given expression.-The scope used for the expression is that of the last point-inside the current top-level module.--With a prefix argument distinct from `(4)' the normal form of-\"show <expression>\" is computed, and then the resulting string-is printed.--With the prefix argument `(4)' \"abstract\" is ignored during the-computation."-  (interactive "MExpression: \nP")-  (let ((cmd (concat "Cmd_compute_toplevel"-                     (cond ((equal arg nil) " DefaultCompute")-                            ((equal arg '(4)) " IgnoreAbstract")-                            ((equal arg '(16)) " UseShowInstance")-                            (" HeadCompute")) " ")))-    (agda2-go nil t 'busy t-              (concat cmd (agda2-string-quote expr)))))--(defun agda2-compute-normalised-maybe-toplevel ()-  "Compute the normal form of the given expression.-The scope used for the expression is that of the last point-inside the current top-level module.--With a prefix argument distinct from `(4)' the normal form of-\"show <expression>\" is computed, and then the resulting string-is printed.--With the prefix argument `(4)' \"abstract\" is ignored during the-computation."-  (interactive)-  (if (agda2-goal-at (point))-      (call-interactively 'agda2-compute-normalised)-    (call-interactively 'agda2-compute-normalised-toplevel)))--(defun agda2-display-program-version ()-  "Display version of Agda"-  (interactive)-  (agda2-go nil nil 'busy t "Cmd_show_version"))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;;--(defun agda2-highlight-reload nil-  "Loads precomputed syntax highlighting info for the current buffer.-Only if the buffer is unmodified, and only if there is anything to load."- (unless (buffer-modified-p)-   (agda2-go nil t 'not-so-busy t-             "Cmd_load_highlighting_info"-             (agda2-string-quote (buffer-file-name)))))--(defun agda2-literate-p ()-  "Is the current buffer a literate Agda buffer?"-  (not (equal (file-name-extension (buffer-file-name)) "agda")))--(defmacro agda2--case (exp &rest branches) ;FIXME: Use `pcase' instead!-  (declare (debug t) (indent 1))-  (let ((s (make-symbol "v")))-    `(let ((,s ,exp))-       (cond-         ,@(mapcar (lambda (branch)-                     `((equal ,s ,(car branch)) ,@(cdr branch)))-                   branches)))))--(defun agda2-goals-action (goals)-  "Annotates the goals in the current buffer with text properties.-GOALS is a list of the buffer's goal numbers, in the order in-which they appear in the buffer. Note that this function should-be run /after/ syntax highlighting information has been loaded,-because the two highlighting mechanisms interact in unfortunate-ways."-  (agda2-forget-all-goals)-  (agda2-let-      ((literate (agda2-literate-p))-       stk-       top-       ;; Don't run modification hooks: we don't want this function to-       ;; trigger agda2-abort-highlighting.-       (inhibit-modification-hooks t))-      ((delims() (re-search-forward "[?]\\|[{][-!]\\|[-!][}]\\|--\\|^%.*\\\\begin{code}\\|\\\\begin{code}\\|\\\\end{code}\\|```\\|\\#\\+begin_src agda2\\|\\#\\+end_src agda2" nil t))-       ;; is-proper checks whether string s (e.g. "?" or "--") is proper-       ;; i.e., is not part of an identifier.-       ;; comment-starter is true if s starts a comment (e.g. "--")-       (is-proper (s comment-starter)-          (save-excursion-            (save-match-data-              (backward-char (length s))-              (unless (bolp) (backward-char 1))  ;; bolp = pointer at beginning of line-              ;; Andreas, 2014-05-17 Issue 1132-              ;; A questionmark can also follow immediately after a .-              ;; for instance to be a place holder for a dot pattern.-              (looking-at (concat "\\([.{}();]\\|^\\|\\s \\)"  ;; \\s = whitespace-                                  (regexp-quote s)-                                  (unless comment-starter-                                    "\\([{}();]\\|$\\|\\s \\)"))))))-       (make(p)  (agda2-make-goal p (point) (pop goals)))-       (inside-comment() (and stk (null     (car stk))))-       (inside-goal()    (and stk (integerp (car stk))))-       (outside-code()   (and stk (eq (car stk) 'outside)))-       (inside-code()    (not (outside-code)))-       ;; inside a multi-line comment ignore everything but the multi-line comment markers-       (safe-delims()-          (if (inside-comment)-               (re-search-forward "{-\\|-}" nil t)-            (delims))))-    (save-excursion-      ;; In literate mode we should start out in the "outside of code"-      ;; state.-      (if literate (push 'outside stk))-      (goto-char (point-min))-      (while (and goals (safe-delims))-        (agda2--case (match-string 0)-          ("\\begin{code}"     (when (outside-code)               (pop stk)))-          ("\\end{code}"       (when (not stk)                    (push 'outside stk)))-          ("#+begin_src agda2" (when (outside-code)               (pop stk)))-          ("#+end_src agda2"   (when (not stk)                    (push 'outside stk)))-          ("```"               (if   (outside-code)               (pop stk)-                               (when (not stk)                    (push 'outside stk))))-          ("--"                (when (and (not stk)-                                          (is-proper "--" t))     (end-of-line)))-          ("{-"                (when (and (inside-code)-                                          (not (inside-goal)))    (push nil           stk)))-          ("-}"                (when (inside-comment)             (pop stk)))-          ("{!"                (when (and (inside-code)-                                          (not (inside-comment))) (push (- (point) 2) stk)))-          ("!}"                (when (inside-goal)-                                 (setq top (pop stk))-                                 (unless stk (make top))))-          ("?"                 (progn-                                 (when (and (not stk) (is-proper "?" nil))-                                   (delete-char -1)-                                   (insert "{!!}")-                                   (make (- (point) 4))))))))))--(defun agda2-make-goal (p q n)-  "Make a goal with number N at <P>{!...!}<Q>.  Assume the region is clean."-  (annotation-preserve-mod-p-and-undo-   (let ((atp (lambda (x ps) (add-text-properties x (1+ x) ps))))-     (funcall atp p       '(category agda2-delim1))-     (funcall atp (1+ p)  '(category agda2-delim2))-     (funcall atp (- q 2) '(category agda2-delim3))-     (funcall atp (1- q)  '(category agda2-delim4)))-   (let ((o (make-overlay p q nil t nil)))-     (overlay-put o 'modification-hooks '(agda2-protect-goal-markers))-     (overlay-put o 'agda2-gn           n)-     (overlay-put o 'face               'highlight)-     (overlay-put o 'after-string       (propertize (format "%s" n) 'face 'highlight)))))--(defun agda2-protect-goal-markers (ol action beg end &optional length)-  "Ensures that the goal markers cannot be tampered with.-Except if `inhibit-read-only' is non-nil or /all/ of the goal is-modified."-  (if action-      ;; This is the after-change hook.-      nil-    ;; This is the before-change hook.-    (cond-     ((and (<= beg (overlay-start ol)) (>= end (overlay-end ol)))-      ;; The user is trying to remove the whole goal:-      ;; manually evaporate the overlay and add an undo-log entry so-      ;; it gets re-added if needed.-      (when (listp buffer-undo-list)-        (push (list 'apply 0 (overlay-start ol) (overlay-end ol)-                    'move-overlay ol (overlay-start ol) (overlay-end ol))-              buffer-undo-list))-      (delete-overlay ol))-     ((or (< beg (+ (overlay-start ol) 2))-          (> end (- (overlay-end ol) 2)))-      (unless inhibit-read-only-        (signal 'text-read-only nil))))))--(defun agda2-update (old-g new-txt)-  "Update the goal OLD-G.-If NEW-TXT is a string, then the goal is replaced by the string,-and otherwise the text inside the goal is retained (parenthesised-if NEW-TXT is `'paren').--Removes the goal braces, but does not remove the goal overlay or-text properties."-  (cl-multiple-value-bind (p q) (agda2-range-of-goal old-g)-    (save-excursion-      (cond ((stringp new-txt)-             (agda2-replace-goal old-g new-txt))-            ((equal new-txt 'paren)-             (goto-char (- q 2)) (insert ")")-             (goto-char (+ p 2)) (insert "(")))-      (cl-multiple-value-bind (p q) (agda2-range-of-goal old-g)-        (delete-region (- q 2) q)-        (delete-region p (+ p 2)))-        ;; Update highlighting-        (if (and (not (equal new-txt 'paren)) (not (equal new-txt 'no-paren)))-            (apply 'agda2-go 'save t 'busy nil "Cmd_highlight"-              (format "%d" old-g)-              (agda2-mkRange `(,p ,(- q 2)))-              (agda2-string-quote new-txt) nil))-    )))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;; Misc--(defun agda2-process-status ()-  "Status of `agda2-process-buffer', or \"no process\"."-  (condition-case nil-      (process-status agda2-process)-    (error "no process")))--(defun agda2-intersperse (sep xs)-  (let(ys)(while xs (push (pop xs) ys)(push sep ys))(pop ys)(nreverse ys)))--(defun agda2-goal-Range (o)-  "The Haskell Range of goal overlay O."-  (agda2-mkRange `(,(+ (overlay-start o) 2)-                   ,(- (overlay-end   o) 2))))--(defun agda2-mkRange (points)-  "A string representing a range corresponding to POINTS.-POINTS must be a list of integers, and its length must be 0 or 2."-  (if points-      (format "(intervalsToRange (Just (mkAbsolute %s)) %s)"-              (agda2-string-quote (file-truename (buffer-file-name)))-              (format "[Interval %s %s]"-                      (agda2-mkPos (car points))-                      (agda2-mkPos (cadr points))))-    "noRange"))--(defun agda2-mkPos (&optional p)-  "The Haskell PositionWithoutFile corresponding to P or `point'."-  (save-excursion-    (save-restriction-      (widen)-      (if p (goto-char p))-      (format "(Pn () %d %d %d)"-              (point)-              (count-lines (point-min) (point))-              (1+ (current-column))))))--(defun agda2-char-quote (c)-  "Convert character C to the notation used in Haskell strings.-The non-ASCII characters are actually rendered as-\"\\xNNNN\\&\", i.e. followed by a \"null character\", to avoid-problems if they are followed by digits.  ASCII characters (code-points < 128) are converted to singleton strings."-  (if (< c 128)-      (list c)-    ;; FIXME: Why return a list rather than a string?  --Stef-    (append (format "\\x%x\\&" (encode-char c 'ucs)) nil)))--(defun agda2-string-quote (s)-  "Format S as a Haskell string literal.-Removes any text properties, escapes newlines, double quotes,-etc., adds surrounding double quotes, and converts non-ASCII-characters to the \\xNNNN notation used in Haskell strings."-  (let ((pp-escape-newlines t)-        (s2 (copy-sequence s)))-    (set-text-properties 0 (length s2) nil s2)-    (mapconcat 'agda2-char-quote (pp-to-string s2) "")))--(defun agda2-list-quote (strings)-  "Convert a list of STRINGS into a string representing it in Haskell syntax."-  (concat "[" (mapconcat 'agda2-string-quote strings ", ") "]"))--(defun agda2-goal-at(pos)-  "Return (goal overlay, goal number) at POS, or nil."-  (let ((os (and pos (overlays-at pos))) o g)-    (while (and os (not(setq g (overlay-get (setq o (pop os)) 'agda2-gn)))))-    (if g (list o g))))--(defun agda2-goal-overlay (g)-  "Returns the overlay of goal number G, if any."-  (car-   (remove nil-           (mapcar (lambda (o) (if (equal (overlay-get o 'agda2-gn) g) o))-                   (overlays-in (point-min) (point-max))))))--(defun agda2-range-of-goal (g)-  "The range of goal G."-  (let ((o (agda2-goal-overlay g)))-    (if o (list (overlay-start o) (overlay-end o)))))--(defun agda2-goto-goal (g)-  (let ((p (+ 2 (car (agda2-range-of-goal g)))))-    (if p (goto-char p))))--(defun agda2-replace-goal (g newtxt)-  "Replace the content of goal G with NEWTXT." (interactive)-  (save-excursion-    (cl-multiple-value-bind (p q) (agda2-range-of-goal g)-      (setq p (+ p 2) q (- q 2))-      (let ((indent (and (goto-char p) (current-column))))-        (delete-region p q) (insert newtxt)-        (while (re-search-backward "^" p t)-          (insert-char ?  indent) (backward-char (1+ indent)))))))--(defun agda2-forget-all-goals ()-  "Remove all goal annotations.-\(Including some text properties which might be used by other-\(minor) modes.)"-  (annotation-preserve-mod-p-and-undo-   (remove-text-properties (point-min) (point-max)-                           '(category nil agda2-delim2 nil agda2-delim3 nil-                             display nil rear-nonsticky nil)))-  (let ((p (point-min)))-    (while (< (setq p (next-single-char-property-change p 'agda2-gn))-              (point-max))-      (delete-overlay (car (agda2-goal-at p))))))--(defun agda2-decl-beginning ()-  "Find the beginning point of the declaration containing the point.-To do: dealing with semicolon separated decls."-  (interactive)-  (save-excursion-    (let* ((pEnd (point))-           (pDef (progn (goto-char (point-min))-                        (re-search-forward "\\s *" pEnd t)))-           (cDef (current-column)))-      (while (re-search-forward-              "where\\(\\s +\\)\\S \\|^\\(\\s *\\)\\S " pEnd t)-        (if (match-end 1)-            (setq pDef (goto-char (match-end 1))-                  cDef (current-column))-          (goto-char (match-end 2))-          (if (>= cDef (current-column))-              (setq pDef (point)-                    cDef (current-column))))-        (forward-char))-      (goto-char pDef)-      (if (equal (current-word) "mutual")-          (or (match-end 2) (match-end 1))-        pDef))))--(defun agda2-beginning-of-decl ()-  (interactive)-  (goto-char (agda2-decl-beginning)))--(defvar agda2-debug-buffer-name "*Agda debug*"-  "The name of the buffer used for Agda debug messages.")--(defun agda2-verbose (msg)-  "Appends the string MSG to the `agda2-debug-buffer-name' buffer.-Note that this buffer's contents is not erased automatically when-a file is loaded."-  (with-current-buffer (get-buffer-create agda2-debug-buffer-name)-    (save-excursion-      (goto-char (point-max))-      (insert msg))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Comments and paragraphs--(defun agda2-comments-and-paragraphs-setup nil-  "Set up comment and paragraph handling for the Agda mode."--  ;; Empty lines (all white space according to Emacs) delimit-  ;; paragraphs.-  (set (make-local-variable 'paragraph-start) "\\s-*$")-  (set (make-local-variable 'paragraph-separate) paragraph-start)--  ;; Support for adding/removing comments.-  (set (make-local-variable 'comment-start) "-- ")--  ;; Use the syntax table to locate comments (and possibly other-  ;; things). Syntax table setup for comments is done elsewhere.-  (set (make-local-variable 'comment-use-syntax) t)--  ;; Update token-based highlighting after the buffer has been saved.-  (add-hook 'after-save-hook 'agda2-highlight-tokens nil 'local)--  ;; Support for proper filling of text in comments (requires that-  ;; Filladapt is activated).-  (when (featurep 'filladapt)-    (add-to-list (make-local-variable-                  'filladapt-token-table)-                 '("--" agda2-comment))-    (add-to-list (make-local-variable 'filladapt-token-match-table)-                 '(agda2-comment agda2-comment) t)-    (add-to-list (make-local-variable 'filladapt-token-conversion-table)-                 '(agda2-comment . exact))))--(defun agda2-comment-dwim-rest-of-buffer ()-  "Comment or uncomment the rest of the buffer.-From the beginning of the current line to the end of the buffer."-  (interactive)-  (save-excursion-    (forward-line 0)-    (push-mark (point) 'no-message 'activate-mark)-    (unwind-protect-        (progn-          (goto-char (point-max))-          (comment-dwim nil))-      (pop-mark))))--(defun agda2-highlight-tokens nil-  "Compute token-based highlighting information.--Unless `agda2-highlight-level' is `none' or the Agda process is-busy (or `not-so-busy') with something. This command might save-the buffer."-  (unless (or agda2-in-progress-              (equal agda2-highlight-level 'none))-    (agda2-go 'save t 'not-so-busy t-              "Cmd_tokenHighlighting"-              (agda2-string-quote (buffer-file-name))-              "Keep")))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Go to definition site--(defun agda2-goto-definition-keyboard (&optional other-window)-  "Go to the definition site of the name under point (if any).-If this function is invoked with a prefix argument then another window is used-to display the given position."-  (interactive "P")-  (annotation-goto-indirect (point) other-window))--(defun agda2-goto-definition-mouse (ev)-  "Go to the definition site of the name clicked on, if any.-Otherwise, yank (see `mouse-yank-primary')."-  (interactive "e")-  (unless (annotation-goto-indirect ev)-    ;; FIXME: Shouldn't we use something like-    ;; (call-interactively (key-binding ev))?  --Stef-    (mouse-yank-primary ev)))--(defun agda2-go-back nil-  "Go back to the previous position in which-`agda2-goto-definition-keyboard' or `agda2-goto-definition-mouse' was-invoked."-  (interactive)-  (annotation-go-back))--(defun agda2-maybe-goto (filepos)-  "Might move point to the given error.-FILEPOS should have the form (FILE . POSITION).--If `agda2-highlight-in-progress' is nil, then nothing happens.-Otherwise, if the current buffer is the one that is connected to-the Agda process, then point is moved to POSITION in-FILE (assuming that the FILE is readable). Otherwise point is-moved to the given position in the buffer visiting the file, if-any, and in every window displaying the buffer, but the window-configuration and the selected window are not changed."-  (when (and agda2-highlight-in-progress-             (consp filepos)-             (stringp (car filepos))-             (integerp (cdr filepos)))-    (if agda2-in-agda2-file-buffer-        (annotation-goto-and-push (current-buffer) (point) filepos)-      (save-excursion-        (let ((buffer (find-buffer-visiting (car filepos))))-          (when buffer-            (let ((windows (get-buffer-window-list buffer-                                                   'no-minibuffer t)))-              (if windows-                  (dolist (window windows)-                    (with-selected-window window-                      (goto-char (cdr filepos))))-                (with-current-buffer buffer-                  (goto-char (cdr filepos)))))))))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Implicit arguments--(defun agda2-display-implicit-arguments (&optional arg)-  "Toggle display of implicit arguments.-With prefix argument, turn on display of implicit arguments if-the argument is a positive number, otherwise turn it off."-  (interactive "P")-  (cond-   ((eq arg nil)-      (agda2-go nil t 'not-so-busy t "ToggleImplicitArgs"))-   ((and (numberp arg) (> arg 0))-      (agda2-go nil t 'not-so-busy t "ShowImplicitArgs" "True"))-   (t (agda2-go nil t 'not-so-busy t "ShowImplicitArgs" "False"))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Irrelevant arguments--(defun agda2-display-irrelevant-arguments (&optional arg)-  "Toggle display of irrelevant arguments.-With prefix argument, turn on display of irrelevant arguments if-the argument is a positive number, otherwise turn it off."-  (interactive "P")-  (cond-   ((eq arg nil)-      (agda2-go nil t 'not-so-busy t "ToggleIrrelevantArgs"))-   ((and (numberp arg) (> arg 0))-      (agda2-go nil t 'not-so-busy t "ShowIrrelevantArgs" "True"))-   (t (agda2-go nil t 'not-so-busy t "ShowIrrelevantArgs" "False"))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;;;;--(defun agda2-popup-menu-3 (ev)-  "If in a goal, popup the goal menu and call chosen command."-  (interactive "e")-  (let (choice)-    (save-excursion-      (and (agda2-goal-at (goto-char (posn-point (event-end ev))))-           (setq choice (x-popup-menu ev agda2-goal-map))-           (call-interactively-            (lookup-key agda2-goal-map (apply 'vector choice)))))))--;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Switching to a different version of Agda--(defun agda2-get-agda-program-versions ()-  "Get \"version strings\" of executables starting with-\\='agda2hs-mode\\=' in current path."-  (delete-dups-   (mapcar (lambda (path)-             ;; strip 'agda2hs-mode' prefix-             (replace-regexp-in-string "^agda2hs-mode-?" ""-                                       (file-name-nondirectory path)))-           (cl-remove-if-not 'file-executable-p-             ;; concatenate result-             (cl-reduce 'append-                     ;; for each directory in exec-path, get list of-                     ;; files whose name starts with 'agda-mode'-                     (mapcar (lambda (path)-                               (when (file-accessible-directory-p path)-                                 (directory-files path 't "^agda2hs-mode")))-                             exec-path))))))--;; Note that other versions of Agda may use different protocols, so-;; this function unloads the Emacs mode.--(defun agda2-set-program-version (version)-  "Tries to switch to Agda version VERSION.--This command assumes that the agda and agda-mode executables for-Agda version VERSION are called agda-VERSION and-agda-mode-VERSION, and that they are located on the PATH. (If-VERSION is empty, then agda and agda-mode are used instead.)--An attempt is made to preserve the default value of-`agda2-mode-hook'."-  (interactive-   (list (completing-read "Version: " (agda2-get-agda-program-versions))))--  (let*-      ((agda-buffers-        (cl-mapcan (lambda (buf)-                  (with-current-buffer buf-                    (when (equal major-mode 'agda2-mode)-                      (list buf))))-                (buffer-list)))--       (default-hook (default-value 'agda2-mode-hook))--       (version-suffix (if (or (equal version "")-                               (equal version nil))-                           ""-                         (concat "-" version)))--       ;; Run agda-mode<version-suffix> and make sure that it returns-       ;; successfully.-       (coding-system-for-read 'utf-8)-       (agda-mode-prog (concat "agda2hs-mode" version-suffix))-       (agda-mode-path-        (condition-case nil-            (with-temp-buffer-              (unless-                  (equal 0 (call-process agda-mode-prog-                                         nil (current-buffer) nil-                                         "locate"))-                (error "%s" (concat "Error when running "-                                    agda-mode-prog)))-              (buffer-string))-          (file-error-           (error "%s" (concat "Could not find " agda-mode-prog))))))--    ;; Make sure that agda-mode<version-suffix> returns a valid file.-    (unless (file-readable-p agda-mode-path)-      (error "%s" (concat "Could not read " agda-mode-path)))--    ;; Turn off the Agda mode.-    (agda2-quit)--    ;; Kill some buffers related to Agda.-    (when (buffer-live-p agda2-info-buffer)-      (kill-buffer agda2-info-buffer))-    (when (and agda2-debug-buffer-name-               (get-buffer agda2-debug-buffer-name))-      (kill-buffer agda2-debug-buffer-name))--    ;; Remove the Agda mode directory from the load path.-    (setq load-path (delete agda2-directory load-path))--    ;; Unload the Agda mode and its dependencies.-    (unload-feature 'agda2-mode      'force)-    (unload-feature 'agda2           'force)-    (unload-feature 'eri             'force)-    (unload-feature 'annotation      'force)-    (unload-feature 'agda-input      'force)-    (unload-feature 'agda2-highlight 'force)-    (unload-feature 'agda2-abbrevs   'force)-    (unload-feature 'agda2-queue     'force)--    ;; Load the new version of Agda.-    (load-file agda-mode-path)-    (require 'agda2-mode)-    (setq agda2-program-name (concat "agda2hs" version-suffix))--    ;; Restore the Agda mode's default hook (if any).-    (when default-hook-      (set-default 'agda2-mode-hook default-hook))--    ;; Restart the Agda mode in all former Agda mode buffers.-    (mapc (lambda (buf)-            (with-current-buffer buf-              (agda2-mode)))-          agda-buffers)))--(provide 'agda2-mode)-;;; agda2-mode.el ends here

@@ -1,44 +0,0 @@-;;; agda2-queue.el --- Simple FIFO character queues.-;; SPDX-License-Identifier: MIT License--(defun agda2-queue-empty ()-  "Creates a new empty FIFO character queue.-Queues are represented as pairs. The car contains the queue. If-the queue is empty, then the cdr contains the symbol nil, and-otherwise it points to the queue's last cons-cell."-  (cons nil nil))--(defun agda2-queue-is-prefix-of (prefix queue)-  "Returns a non-nil result iff the string PREFIX is a prefix of QUEUE.-Linear in the length of PREFIX."-  (let ((queue  (car queue))-        (prefix (append prefix nil)))-    (while (and (consp queue) (consp prefix)-                (equal (car queue) (car prefix)))-      (pop queue)-      (pop prefix))-    (null prefix)))--(defun agda2-queue-enqueue (queue string)-  "Adds the characters in STRING to the end of QUEUE.-This function updates QUEUE destructively, and is linear in the-length of STRING."-  (let ((chars (append string nil)))-    (when (consp chars)-      (if (null (cdr queue))-          (setcar queue chars)-        (setcdr (cdr queue) chars))-      (setcdr queue (last chars))))-  queue)--(defun agda2-queue-from-string (string)-  "Creates a new FIFO containing the characters in STRING.-Linear in the length of STRING."-  (agda2-queue-enqueue (agda2-queue-empty) string))--(defun agda2-queue-to-string (queue)-  "Constructs a string containing all the characters in QUEUE.-Linear in the length of QUEUE."-  (concat "" (car queue)))--(provide 'agda2-queue)

@@ -1,16 +0,0 @@-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;-;; Agda mode code which should run before the first Agda file is-;; loaded-;; SPDX-License-Identifier: MIT License--(defvar agda2-directory (file-name-directory load-file-name)-  "Path to the directory that contains agda2.el(c).")--(add-to-list 'load-path (or agda2-directory (car load-path)))--(autoload 'agda2-mode "agda2-mode"-  "Major mode for editing Agda files (version ≥ 2)." t)-(add-to-list 'auto-mode-alist '("\\.l?agda\\'" . agda2-mode))-(modify-coding-system-alist 'file "\\.l?agda\\'" 'utf-8)--(provide 'agda2)

@@ -1,301 +0,0 @@-;;; annotation.el --- Functions for annotating text with faces and help bubbles--;; Version: 1.0--;; SPDX-License-Identifier: MIT License-;; URL: https://github.com/agda/agda-;; Version: 1.0--;;; Commentary:--;; Note that this library enumerates buffer positions starting from 1,-;; just like Emacs.--(require 'cl-lib)--(defvar annotation-bindings nil-  "An association list mapping symbols to faces.")-(make-variable-buffer-local 'annotation-bindings)--(defvar annotation-goto-stack nil-  "Positions from which `annotation-goto' was invoked.")--(defun annotation-goto-indirect (link &optional other-window)-  "Follow the `annotation-goto' hyperlink pointed to by LINK, if any.--LINK should be a buffer position, or an event object (in which-case the ending position is used).--If the hyperlink exists and the jump is performed successfully,-then `t' is returned, and otherwise `nil' (unless an error is-raised).--If OTHER-WINDOW is non-nil, then another window is used to-display the target position."-  (let (source-pos-        source-window-        source-buffer-        source-file-name-        target)-    (cond ((eventp link)-           (let ((pn (event-end link)))-             (when (not (posn-area pn))-               (setq source-pos (posn-point pn))-               (setq source-window (posn-window pn))-               (setq source-buffer (window-buffer source-window)))))-          ((integerp link)-           (setq source-pos link)-           (setq source-window (selected-window))-           (setq source-buffer (current-buffer)))-          (t (error "Not an integer or event object: %S" link)))-    (when (and source-pos source-buffer)-      (with-current-buffer source-buffer-        (setq target (get-text-property source-pos 'annotation-goto)))-      (when target-        (unless (equal source-window (selected-window))-          (select-window source-window))-        (annotation-goto-and-push source-buffer source-pos target-                                  other-window)))))--(defun annotation-go-back nil-  "Go back to the previous position.-The previous position in which `annotation-goto-and-push' was-successfully invoked."-  (when annotation-goto-stack-    (let ((pos (pop annotation-goto-stack)))-      (annotation-goto pos))))--(defun annotation-goto-and-push (source-buffer source-pos filepos &optional other-window)-  "Like `annotation-goto', but pushes a position when successful.-The position consists of the file visited by SOURCE-BUFFER, and-the position given by SOURCE-POS."-  (let (source-file-name)-    (with-current-buffer source-buffer-      (setq source-file-name buffer-file-name))-    (when (annotation-goto filepos other-window)-      (unless (and (equal source-buffer (current-buffer))-                   (eq source-pos (point)))-        (push `(,source-file-name . ,source-pos)-              annotation-goto-stack))-      t)))--(defun annotation-goto (filepos &optional other-window)-  "Go to file position FILEPOS if the file is readable.-FILEPOS should have the form (FILE . POS).  Return t if successful.--If OTHER-WINDOW is non-nil, use another window to display the-given position."-  (when (consp filepos)-    (let ((file (car filepos)))-      (if (file-readable-p file)-          (progn-            (if other-window-                (find-file-other-window file)-              (find-file file))-            (goto-char (cdr filepos))-            t)-        (error "File does not exist or is unreadable: %s." file)))))--(defun annotation-merge-faces (start end faces)-  "Helper procedure used by `annotation-annotate'.-For each position in the range the FACES are merged-with the current value of the annotation-faces text property, and-both the face and the annotation-faces text properties are set to-the resulting list of faces.--Precondition: START and END must be numbers, and START must be-less than END."-  (cl-assert (condition-case nil (< start end) (error nil)))-  (let ((pos start)-        mid)-    (while (< pos end)-      (setq mid (next-single-property-change pos 'annotation-faces-                                             nil end))-      (let* ((old-faces (get-text-property pos 'annotation-faces))-             (all-faces (cl-union old-faces faces)))-        (mapc (lambda (prop) (put-text-property pos mid prop all-faces))-              '(annotation-faces face))-        (setq pos mid)))))--(defun annotation-annotate-    (start end anns &optional token-based info goto)-  "Annotate text between START and END in the current buffer.--Nothing happens if either START or END are out of bounds for the-current (possibly narrowed) buffer, or END <= START.--If ANNS is nil, then those text properties between START and END-that have been set by this function are deleted. Otherwise the-following happens.--All the symbols in ANNS are looked up in `annotation-bindings',-and the resulting list of faces is used to set the face text-property. For each position in the range the faces are merged-with the current value of the annotation-faces text property, and-both the face and the annotation-faces text properties are set to-the resulting list of faces.--If TOKEN-BASED is non-nil, then the annotation-token-based-property is set to t. This means that all text properties set by-`annotation-annotate' in this range are interpreted as being-token-based, including those set by previous calls to this-procedure.--If the string INFO is non-nil, the mouse-face-property is set to highlight, and INFO is used as the help-echo-string. If GOTO has the form (FILENAME . POSITION), then the-mouse-face property is set to highlight, and the given-filename/position will be used by `annotation-goto-indirect' when-it is invoked with a position in the given range.--Note that if a given attribute is defined by several faces, then-the first face's setting takes precedence.--All characters whose text properties get set also have the-annotation-annotated property set to t, and-annotation-annotations is set to a list with all the properties-that have been set; this ensures that the text properties can-later be removed (if the annotation-* properties are not tampered-with)."-  (when (and (<= (point-min) start)-             (< start end)-             (<= end (point-max)))-    (if (null anns)-        (annotation-remove-annotations nil start end)-      (let ((faces (delq nil-                         (mapcar (lambda (ann)-                                   (cdr (assoc ann annotation-bindings)))-                                 anns)))-            (props nil))-        (when faces-          (annotation-merge-faces start end faces)-          (add-to-list 'props 'face)-          (add-to-list 'props 'annotation-faces))-        (when token-based-          (add-text-properties start end-                               `(annotation-token-based t))-          (add-to-list 'props 'annotation-token-based))-        (when (consp goto)-          (add-text-properties start end-                               `(annotation-goto ,goto-                                 mouse-face highlight))-          (add-to-list 'props 'annotation-goto)-          (add-to-list 'props 'mouse-face))-        (when info-          (add-text-properties start end-                               `(mouse-face highlight help-echo ,info))-          (add-to-list 'props 'mouse-face)-          (add-to-list 'props 'help-echo))-        (when props-          (add-to-list 'props 'annotation-annotated)-          (let ((pos start)-                mid)-            (while (< pos end)-              (setq mid (next-single-property-change pos-                           'annotation-annotations nil end))-              (let* ((old-props (get-text-property pos 'annotation-annotations))-                     (all-props (cl-union old-props props)))-                (add-text-properties pos mid-                   `(annotation-annotated t annotation-annotations ,all-props))-                (setq pos mid)))))))))--(defmacro annotation-preserve-mod-p-and-undo (&rest code)-  "Run CODE preserving both the undo data and the modification bit.-Modification hooks are also disabled."-  (declare (debug (&rest form)))-  (let ((modp (make-symbol "modp")))-  `(let ((,modp (buffer-modified-p))-         ;; Don't check if the file is being modified by some other process.-         (buffer-file-name nil)-         ;; Don't record those changes on the undo-log.-         (buffer-undo-list t)-         ;; Don't run modification hooks.-         (inhibit-modification-hooks t))-     (unwind-protect-         (progn ,@code)-       (restore-buffer-modified-p ,modp)))))--(defun annotation-remove-annotations (&optional token-based start end)-  "Remove text properties set by `annotation-annotate'.--In the current buffer. If START and END are given, then-properties are only removed between these positions. If-TOKEN-BASED is non-nil, then only token-based properties are-removed.--This function preserves the file modification stamp of the-current buffer, does not modify the undo list, and temporarily-disables all modification hooks.--Note: This function may fail if there is read-only text in the-buffer."--  ;; remove-text-properties fails for read-only text.--  (annotation-preserve-mod-p-and-undo-   (let ((tag (if token-based-                  'annotation-token-based-                'annotation-annotated))-         (pos (or start (point-min)))-         (end (or end (point-max)))-         pos2)-     (while pos-       (let ((props (get-text-property pos 'annotation-annotations)))-         (setq pos2 (next-single-property-change pos tag nil end))-         (when (and props-                    (or (not token-based)-                        (member 'annotation-token-based props)))-           (remove-text-properties pos (or pos2 (point-max))-              (cl-mapcan (lambda (prop) (list prop nil))-                      (cons 'annotation-annotations props)))))-       (setq pos (unless (or (not pos2) (>= pos2 end)) pos2))))))--(defun annotation-load (goto-help remove &rest cmds)-  "Apply highlighting annotations in CMDS in the current buffer.--The argument CMDS should be a list of lists (start end anns-&optional info goto). Text between start and end will be-annotated with the annotations in the list anns (using-`annotation-annotate'). If info and/or goto are present they will-be used as the corresponding arguments to `annotation-annotate'.--If INFO is nil in a call to `annotation-annotate', and the GOTO-argument is a cons-cell, then the INFO argument is set to-GOTO-HELP. The intention is that the default help text should-inform the user about the \"goto\" facility.--If REMOVE is nil, then old syntax highlighting information is not-removed. Otherwise all token-based syntax highlighting is-removed. In order to reduce the risk of flicker this highlighting-is removed step by step, in conjunction with the addition of new-highlighting. (This process assumes that CMDS is ordered by the-positions of the annotations. If it isn't, then the highlighting-is still applied correctly, but perhaps with more flicker.)--This function preserves the file modification stamp of the-current buffer, does not modify the undo list, and temporarily-disables all modification hooks.--Note: This function may fail if there is read-only text in the-buffer."-  (annotation-preserve-mod-p-and-undo-    (when (listp cmds)-      (let ((pos (point-min)))-        (dolist (cmd cmds)-          (cl-destructuring-bind-              (start end anns &optional token-based info goto) cmd-            (let ((info (if (and (not info) (consp goto))-                            goto-help-                          info)))-              (when remove-                (annotation-remove-annotations-                 'token-based pos end)-                (setq pos end))-              (annotation-annotate-               start end anns token-based info goto))))-        (when remove-          (annotation-remove-annotations-           'token-based pos (point-max)))))))--(provide 'annotation)-;;; annotation.el ends here

@@ -1,212 +0,0 @@-;;; eri.el --- Enhanced relative indentation (eri)--;; SPDX-License-Identifier: MIT License-;; URL: https://github.com/agda/agda-;; Version: 1.0--;;; Commentary:--;; Cycle between indentation points with enhanced relative indentation.--;;; Code:--(require 'cl-lib)--(defun eri-current-line-length nil-  "Calculate length of current line."-  (- (line-end-position) (line-beginning-position)))--(defun eri-current-line-empty nil-  "Return non-nil if the current line is empty (not counting white space)."-  (equal (current-indentation)-         (eri-current-line-length)))--(defun eri-maximum (xs)-  "Calculate maximum element in XS.-Returns nil if the list is empty."-  (if xs (apply 'max xs)))--(defun eri-take (n xs)-  "Return the first N elements of XS."-  (butlast xs (- (length xs) n)))--(defun eri-split (x xs)-  "Return a pair of lists (XS1 . XS2).-If XS is sorted, then XS = (append XS1 XS2), and all elements in-XS1 are <= X, whereas all elements in XS2 are > X."-  (let* ((pos (or (cl-position-if (lambda (y) (> y x)) xs) (length xs)))-         (xs1 (eri-take pos xs))-         (xs2 (nthcdr pos xs)))-    (cons xs1 xs2)))--(defun eri-calculate-indentation-points-on-line (max)-  "Calculate indentation points on current line.-Only points left of column number MAX are included. If MAX is-nil, then all points are included. Points are returned in-ascending order.--Example (positions marked with ^ are returned):--  f x y = g 3 (Just y) 5 4-  ^ ^ ^ ^ ^ ^ ^     ^  |-                       |-                       MAX"-  (let ((result))-    (save-excursion-      (save-restriction-        (beginning-of-line)-        ; To make \\` work in the regexp below:-        (narrow-to-region (line-beginning-position) (line-end-position))-        (while-            (progn-              (let ((pos (and (search-forward-regexp-                               "\\(?:\\s-\\|\\`\\)\\(\\S-\\)" nil t)-                              (match-beginning 1))))-                (when (not (null pos))-                  (let ((pos1 (- pos (line-beginning-position))))-                    (when (or (null max) (< pos1 max))-                      (add-to-list 'result pos1))))-                (and pos-                     (< (point) (line-end-position))-                     (or (null max) (< (current-column) max))))))-        (nreverse result) ; Destructive operation.-        ))))--(defun eri-new-indentation-points ()-  "Calculate new indentation points.-Returns a singleton list containing the column number two steps-in from the indentation of the first non-empty line (white space-excluded) above the current line. If there is no such line,-then the empty list is returned."-  (let ((start (line-beginning-position)))-    (save-excursion-      ; Find a non-empty line above the current one, if any.-      (while-          (progn-            (forward-line -1)-            (not (or (bobp)-                     (not (eri-current-line-empty))))))-      (if (or (equal (point) start)-              (eri-current-line-empty))-          nil-        (list (+ 2 (current-indentation)))))))--(defun eri-calculate-indentation-points (reverse)-  "Calculate points used to indent the current line.-The points are given in reverse order if REVERSE is non-nil. See-`eri-indent' for a description of how the indentation points are-calculated; note that the current indentation is not included in-the returned list."-  ;; First find a bunch of indentations used above the current line.-  (let ((points)-        (max)-        (start (line-beginning-position)))-    (save-excursion-      (while-          (progn-            (forward-line -1)-            ; Skip the line we started from and lines with nothing but-            ; white space.-            (unless (or (equal (point) start)-                        (eri-current-line-empty))-              (setq points-                    (append-                     (eri-calculate-indentation-points-on-line max)-                     points))-              (setq max (car points)))-            ;; Stop after hitting the beginning of the buffer or a-            ;; non-empty, non-indented line.-            (not (or (bobp)-                     (and (equal (current-indentation) 0)-                          (> (eri-current-line-length) 0)))))))-    ;; Add new indentation points, but remove the current indentation.-    ;; Sort the indentations. Rearrange the points so that the next-    ;; point is the one after the current one. Reverse if necessary.-    ;;-    ;; Note: sort and nreverse are destructive.-    (let* ((ps0 (remove (current-indentation)-                        (append (eri-new-indentation-points) points)))-           (ps1 (eri-split (current-indentation) (sort ps0 '<)))-           (ps2 (append (cdr ps1) (car ps1))))-      (if reverse-          (nreverse ps2)-        ps2))))--(defun eri-indent (&optional reverse)-  "Cycle between some possible indentation points.-With prefix argument REVERSE, cycle in reverse order.--Assume that a file contains the following lines of code, with-point on the line with three dots:--frob = loooooooooooooooooooooooooong identifier-foo = f a b-  where-    f (Foo x) y = let bar = x-                      baz = 3 + 5--...--^ ^ ^ ^    ^  ^ ^ ^   ^ * ^ ^ ^ ^--Then the ^'s and the * mark the indentation points that this-function cycles through. The indentation points are selected as-follows:--  * All lines before the current one, up to and including the-    first non-indented line (or the beginning of the buffer) are-    considered.--      foo = f a b-        where-          f (Foo x) y = let bar = x-                            baz = 3 + 5--  * On these lines, erase all characters that stand to the right-    of some non-white space character on a lower line.--      foo-        whe-          f (Foo x) y = let b-                            baz = 3 + 5--  * Also erase all characters not immediately preceded by white-    space.--      f-        w-          f (    x  y = l   b-                            b   = 3 + 5--  * The columns of all remaining characters are indentation-    points.--      f w f (    x  y = l   b   = 3 + 5-      ^ ^ ^ ^    ^  ^ ^ ^   ^   ^ ^ ^ ^--  * A new indentation point is also added, two steps in from the-    indentation of the first non-empty line (white space-    excluded) above the current line (if there is such a line).--      f w f (    x  y = l   b   = 3 + 5-      ^ ^ ^ ^    ^  ^ ^ ^   ^ * ^ ^ ^ ^"-  (interactive "P")-  (let* ((points (eri-calculate-indentation-points reverse))-         (remaining-points (cdr (member (current-indentation) points)))-         (indentation (if remaining-points-                          (car remaining-points)-                        (car points))))-    (when indentation-      (save-excursion (indent-line-to indentation))-      (if (< (current-column) indentation)-          (indent-line-to indentation)))))--(defun eri-indent-reverse nil-  "Cycle between some possible indentation points (in reverse order).-See `eri-indent' for a description of how the indentation points-are calculated."-  (interactive)-  (eri-indent t))--(provide 'eri)-;;; eri.el ends here