From 0a16353fadf2194a18c0c79dcbd8c167df9b16a5 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Sun, 29 May 2022 21:02:11 +0200 Subject: [PATCH] Updating existing tests, fixing treatment of DT parameters, WIP on emacs leg. WIP [ Makefile ] goal continue-cubical-test; update cubical submodule Fix typo in CHANGELOG (#5905) [ workflows ] fix stack/Win (ICU again) (#5909) Stack was updated to MSYS2 2022-05-03 upstream. This solved the keyring problem, but we need to reset the cache. Provenance of where modules in Internal syntax. Qualify some prelude functions in .ghci Running stack repl failed due to these functions not being in scope [ debug ] bump some verbosity levels Fix #5901: use --batch when installing agda-mode for emacs [ doc ] User-manual: installation: add agda to apt-get install Replaces PR https://github.com/agda/agda/pull/5896 by @RosieBaish, thanks for the contribution. User-manual: small improvements to section on `postulate` (#5916) * [ doc ] User-manual: trick how to postulate sth in an expression * [ doc ] remove silly `let open POSTULATE` trick again [ cubical ] cosmetics: generalize iApplyVars [ cosmetics ] turn absV (local def) into global def [ cosmetics ] rewrite some TelView functions Fixed #5920. Re #5924: add LANGUAGE TypeOperators to pacify GHC 9.4 Re #5901: setup agda-mode: don't --no-site-file with --user @nad reports errors with --no-site-file for agda-mode setup. [ user-manual ] +example repeat for Streams, link copatterns->coinduction Finish @RemcoSchrijver's PR #5918 [ re #5923 ] Don't apply rewrite rule instead of generating dummy terms when variables are not bound after matching whitespacefix wip wip wip --- .ghci | 4 +- .github/workflows/stack.yml | 5 +- Agda.cabal | 2 + CHANGELOG.md | 2 +- Makefile | 6 ++ cubical | 2 +- .../getting-started/installation.rst | 2 +- .../language/coinduction.lagda.rst | 11 ++- doc/user-manual/language/copatterns.lagda.rst | 18 ++-- doc/user-manual/language/postulates.lagda.rst | 22 ++++- .../unicode-symbols-sphinx.tex.txt | 1 + src/agda-mode/Main.hs | 55 +++++++---- src/data/emacs-mode/agda2-mode.el | 13 ++- src/full/Agda/Auto/Auto.hs | 4 +- src/full/Agda/Auto/Convert.hs | 11 ++- src/full/Agda/Interaction/BasicOps.hs | 97 +++++++++++++------ .../Interaction/Highlighting/FromAbstract.hs | 2 +- src/full/Agda/Interaction/MakeCase.hs | 45 +++++---- src/full/Agda/Syntax/Abstract.hs | 10 +- src/full/Agda/Syntax/Abstract/Views.hs | 4 +- src/full/Agda/Syntax/Internal.hs | 27 +++--- src/full/Agda/Syntax/Internal/Names.hs | 2 +- .../Syntax/Translation/AbstractToConcrete.hs | 6 +- .../Syntax/Translation/ConcreteToAbstract.hs | 2 +- src/full/Agda/TypeChecking/Coverage.hs | 27 +++--- .../Agda/TypeChecking/Coverage/Cubical.hs | 85 ++++++++-------- src/full/Agda/TypeChecking/Functions.hs | 8 +- .../Agda/TypeChecking/IApplyConfluence.hs | 2 +- src/full/Agda/TypeChecking/Irrelevance.hs | 10 +- src/full/Agda/TypeChecking/Monad/Signature.hs | 17 ++-- src/full/Agda/TypeChecking/ProjectionLike.hs | 4 +- src/full/Agda/TypeChecking/Reduce.hs | 3 +- .../TypeChecking/Rewriting/NonLinMatch.hs | 18 ++-- .../TypeChecking/Rules/Builtin/Coinduction.hs | 5 +- src/full/Agda/TypeChecking/Rules/Data.hs | 4 +- src/full/Agda/TypeChecking/Rules/Def.hs | 44 ++++----- src/full/Agda/TypeChecking/Rules/Record.hs | 29 +++--- src/full/Agda/TypeChecking/Rules/Term.hs | 3 +- .../Serialise/Instances/Internal.hs | 2 +- src/full/Agda/TypeChecking/Sort.hs | 2 +- src/full/Agda/TypeChecking/Substitute.hs | 12 ++- src/full/Agda/TypeChecking/Telescope.hs | 93 +++++++++--------- src/full/Agda/TypeChecking/Telescope/Path.hs | 50 ++++++---- src/github/workflows/stack.yml | 7 +- test/Fail/Issue5920a.agda | 10 ++ test/Fail/Issue5920a.err | 3 + test/Fail/Issue5920b.agda | 7 ++ test/Fail/Issue5920b.err | 4 + test/Fail/Issue5923.agda | 16 +++ test/Fail/Issue5923.err | 3 + test/Succeed/Issue5923-OP.agda | 38 ++++++++ .../Issue5250/Issue5250.agda-lib-e | 2 + test/interaction/Issue737.out | 4 +- test/interaction/Issue810.out | 10 +- test/interaction/Long.out | 29 +++--- 55 files changed, 559 insertions(+), 345 deletions(-) create mode 100644 test/Fail/Issue5920a.agda create mode 100644 test/Fail/Issue5920a.err create mode 100644 test/Fail/Issue5920b.agda create mode 100644 test/Fail/Issue5920b.err create mode 100644 test/Fail/Issue5923.agda create mode 100644 test/Fail/Issue5923.err create mode 100644 test/Succeed/Issue5923-OP.agda create mode 100644 test/interaction/Issue5250/Issue5250.agda-lib-e diff --git a/.ghci b/.ghci index 33cce203a32..407e15e1f5c 100644 --- a/.ghci +++ b/.ghci @@ -41,8 +41,8 @@ :def agda_load_local_ghci \_ -> do let localGhci = ".ghci.local" exists <- System.Directory.doesFileExist localGhci - return $ if exists - then ":script " ++ localGhci + Prelude.return Prelude.$ if exists + then ":script " Prelude.++ localGhci else "" :} :agda_load_local_ghci diff --git a/.github/workflows/stack.yml b/.github/workflows/stack.yml index 9b485362b9f..16cb540b5e9 100644 --- a/.github/workflows/stack.yml +++ b/.github/workflows/stack.yml @@ -96,7 +96,7 @@ jobs: - with: path: ${{ steps.haskell-setup.outputs.stack-root }} key: | - ${{ runner.os }}-stack-00-${{ env.STACK_VER }}-${{ env.GHC_VER }}-${{ hashFiles(format('stack-{0}.yaml.lock', env.GHC_VER)) }} + ${{ runner.os }}-stack-20220503-${{ env.STACK_VER }}-${{ env.GHC_VER }}-${{ hashFiles(format('stack-{0}.yaml.lock', env.GHC_VER)) }} uses: actions/cache@v2 name: Cache dependencies id: cache @@ -112,7 +112,8 @@ jobs: name: Install the icu library (Ubuntu) - if: ${{ runner.os == 'Windows' }} run: | - stack exec ${ARGS} -- pacman --noconfirm -Sy msys2-keyring + stack exec ${ARGS} -- pacman --noconfirm -Syuu + # stack exec ${ARGS} -- pacman --noconfirm -Sy msys2-keyring stack exec ${ARGS} -- pacman --noconfirm -S ${ICU} stack exec ${ARGS} -- pacman --noconfirm -S mingw-w64-x86_64-pkg-config name: Install the icu library (Windows) diff --git a/Agda.cabal b/Agda.cabal index 6562a7afe84..560cb0f9a98 100644 --- a/Agda.cabal +++ b/Agda.cabal @@ -811,6 +811,7 @@ library , StandaloneDeriving , TupleSections , TypeFamilies + , TypeOperators , TypeSynonymInstances executable agda @@ -998,6 +999,7 @@ test-suite agda-tests , StandaloneDeriving , TupleSections , TypeFamilies + , TypeOperators , TypeSynonymInstances if flag(optimise-heavily) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4879545a8ff..653e5f2c4c9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -30,7 +30,7 @@ Language ([#4786](https://github.com/agda/agda/issues/4786)). For instance, the type of the constructor `c` below is now `{@0 A : - Set} → D A`, and the type of the record field `R.f` is {@0 A : Set} + Set} → D A`, and the type of the record field `R.f` is `{@0 A : Set} → R A → A`: ```agda data D (A : Set) : Set where diff --git a/Makefile b/Makefile index c8549417c81..053c8a8ca4c 100644 --- a/Makefile +++ b/Makefile @@ -526,6 +526,12 @@ cubical-test : time $(MAKE) -C cubical \ AGDA_BIN=$(AGDA_BIN) RTS_OPTIONS=$(AGDA_OPTS)) +.PHONY : continue-cubical-test ## +continue-cubical-test : + @$(call decorate, "Continuing cubical library test", \ + time $(MAKE) -C cubical \ + AGDA_BIN=$(AGDA_BIN) RTS_OPTIONS=$(AGDA_OPTS)) + .PHONY : continue-std-lib-test ## continue-std-lib-test : @(cd std-lib && \ diff --git a/cubical b/cubical index 2b389a09089..ef37f14113f 160000 --- a/cubical +++ b/cubical @@ -1 +1 @@ -Subproject commit 2b389a090895832d91771260f1f1ead3c4e40c3d +Subproject commit ef37f14113fa85cb7f7f9fad00e0069e4070f0da diff --git a/doc/user-manual/getting-started/installation.rst b/doc/user-manual/getting-started/installation.rst index ac5c7c28476..0ce382ce6da 100644 --- a/doc/user-manual/getting-started/installation.rst +++ b/doc/user-manual/getting-started/installation.rst @@ -236,7 +236,7 @@ Prebuilt packages are available for Debian and Ubuntu from Karmic onwards. To in .. code-block:: bash - apt-get install agda-mode + apt-get install agda agda-mode This should install Agda and the Emacs mode. diff --git a/doc/user-manual/language/coinduction.lagda.rst b/doc/user-manual/language/coinduction.lagda.rst index 8db5ce88022..1130ea88dd9 100644 --- a/doc/user-manual/language/coinduction.lagda.rst +++ b/doc/user-manual/language/coinduction.lagda.rst @@ -58,11 +58,15 @@ constructor to the record type ``Stream``. fst : A snd : B +Now we can use :ref:`copatterns ` to create ``Stream``\s, like one that +repeats a given element ``a`` infinitely many times:: -We can also define pointwise equality (a bisimulation and an equivalence) of a pair of ``Stream``\s as a -coinductive record: + repeat : {A : Set} (a : A) -> Stream A + hd (repeat a) = a + tl (repeat a) = repeat a -:: +We can also define pointwise equality (a bisimulation and an equivalence) of a pair of ``Stream``\s as a +coinductive record:: record _≈_ {A} (xs : Stream A) (ys : Stream A) : Set where coinductive @@ -108,7 +112,6 @@ Finally, we can prove that ``merge`` is a left inverse for ``split``: tl-≈ (merge-split-id xs) = merge-split-id (tl xs) - Old Coinduction --------------- diff --git a/doc/user-manual/language/copatterns.lagda.rst b/doc/user-manual/language/copatterns.lagda.rst index 41fe0b0b0bf..8c0f1025950 100644 --- a/doc/user-manual/language/copatterns.lagda.rst +++ b/doc/user-manual/language/copatterns.lagda.rst @@ -21,9 +21,10 @@ Copatterns ********** -Consider the following record: +.. note:: If you are looking for information on how to use copatterns with + coinductive records, please visit the section on :ref:`coinduction `. -:: +Consider the following record:: record Enumeration (A : Set) : Set where constructor enumeration @@ -72,8 +73,8 @@ specify all the fields in a single expression: open Enumeration enum-Nat : Enumeration Nat - enum-Nat = record { - start = 0 + enum-Nat = record + { start = 0 ; forward = suc ; backward = pred } @@ -138,8 +139,8 @@ Without copatterns, we just add the extra argument to the function declaration: open Enumeration enum-Nat : Nat → Enumeration Nat - enum-Nat initial = record { - start = initial + enum-Nat initial = record + { start = initial ; forward = suc ; backward = pred } @@ -191,8 +192,8 @@ value to start with based on the user-provided flag: if false then _ else y = y enum-Nat : Bool → Enumeration Nat - enum-Nat ahead = record { - start = if ahead then 42 else 0 + enum-Nat ahead = record + { start = if ahead then 42 else 0 ; forward = suc ; backward = pred } @@ -266,4 +267,3 @@ With copatterns, we can do the case analysis directly by pattern matching: forward enum-Nat n = suc n backward enum-Nat zero = zero backward enum-Nat (suc n) = n - diff --git a/doc/user-manual/language/postulates.lagda.rst b/doc/user-manual/language/postulates.lagda.rst index 69a08a6215f..706b7d3657e 100644 --- a/doc/user-manual/language/postulates.lagda.rst +++ b/doc/user-manual/language/postulates.lagda.rst @@ -25,7 +25,7 @@ Example: :: A B : Set a : A b : B - _=AB=_ : A -> B -> Set + _=AB=_ : A → B → Set a==b : a =AB= b Introducing postulates is in general not recommended. Once postulates are introduced the consistency of the whole development is at risk, because there is nothing that prevents us from introducing an element in the empty set. @@ -36,16 +36,16 @@ Introducing postulates is in general not recommended. Once postulates are introd postulate bottom : False -A preferable way to work is to define a module parametrised by the elements we need +Postulates are forbidden in :ref:`Safe Agda ` (option :option:`--safe`) to prevent accidential inconsistencies. -:: +A preferable way to work with assumptions is to define a module parametrised by the elements we need:: module Absurd (bt : False) where -- ... module M (A B : Set) (a : A) (b : B) - (_=AB=_ : A -> B -> Set) (a==b : a =AB= b) where + (_=AB=_ : A → B → Set) (a==b : a =AB= b) where -- ... @@ -53,4 +53,16 @@ A preferable way to work is to define a module parametrised by the elements we n Postulated built-ins -------------------- -Some :ref:`built-ins` such as `Float` and `Char` are introduced as a postulate and then given a meaning by the corresponding ``{-# BUILTIN ... #-}`` pragma. +Some :ref:`built-ins ` such as `Float` and `Char` are introduced as a postulate and then given a meaning by the corresponding ``{-# BUILTIN ... #-}`` pragma. + +Local uses of ``postulate`` +--------------------------- + +Postulates are declarations and can appear in positions where arbitrary declarations are allowed, e.g., in ``where`` blocks:: + + module PostulateInWhere where + + my-theorem : (A : Set) → A + my-theorem A = I-prove-this-later + where + postulate I-prove-this-later : _ diff --git a/doc/user-manual/unicode-symbols-sphinx.tex.txt b/doc/user-manual/unicode-symbols-sphinx.tex.txt index 3a70342f453..cad74f82d9b 100644 --- a/doc/user-manual/unicode-symbols-sphinx.tex.txt +++ b/doc/user-manual/unicode-symbols-sphinx.tex.txt @@ -259,6 +259,7 @@ \DeclareUnicodeCharacter{2467}{\ensuremath{\text{\ding{179}}}} % Symbol ⑧ \DeclareUnicodeCharacter{2468}{\ensuremath{\text{\ding{180}}}} % Symbol ⑨ +\DeclareUnicodeCharacter{25A1}{\ensuremath{\Box}} % Symbol □ \DeclareUnicodeCharacter{25C5}{\ensuremath{\triangleleft}} % Symbol ◅ \DeclareUnicodeCharacter{2660}{\ensuremath{\spadesuit}} % Symbol ♠ diff --git a/src/agda-mode/Main.hs b/src/agda-mode/Main.hs index 3c29c4a2fd1..0b48bd9554a 100644 --- a/src/agda-mode/Main.hs +++ b/src/agda-mode/Main.hs @@ -122,7 +122,7 @@ setupDotEmacs files = do -- | Tries to find the user's .emacs file by querying Emacs. findDotEmacs :: IO FilePath -findDotEmacs = askEmacs "(insert (expand-file-name user-init-file))" +findDotEmacs = askEmacs "(expand-file-name user-init-file)" -- | Has the Agda mode already been set up? @@ -167,14 +167,24 @@ askEmacs query = do (removeFile . fst) $ \(file, h) -> do hClose h exit <- rawSystemWithDiagnostics "emacs" - [ "--no-desktop", "-nw", "--no-splash" - -- Andreas, 2014-01-11: ^ try a leaner startup of emacs - -- Andreas, 2018-09-08: -nw instead of --no-window-system as some emacses do not support the long version - , "--eval" - , "(with-temp-file " ++ escape file ++ " " - ++ query ++ ")" - , "--kill" - ] + [ "--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 @@ -249,16 +259,16 @@ compileElispFiles = do where compile dataDir f = do exit <- rawSystemWithDiagnostics "emacs" $ - [ "--no-init-file", "--no-site-file" - , "--directory", dataDir - , "--batch" - , "--eval" - , "(progn \ - \(setq byte-compile-error-on-warn t) \ - \(byte-compile-disable-warning 'cl-functions) \ - \(batch-byte-compile))" - , f - ] + [ "--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 ------------------------------------------------------------------------ @@ -269,3 +279,10 @@ compileElispFiles = do inform = hPutStr stderr informLn = hPutStrLn stderr + +parens :: String -> String +parens s = concat [ "(", s, ")" ] + +-- LISP application +apply :: [String] -> String +apply = parens . unwords diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el index 65fa63ecd00..a9a6931ebe1 100644 --- a/src/data/emacs-mode/agda2-mode.el +++ b/src/data/emacs-mode/agda2-mode.el @@ -874,13 +874,18 @@ The action depends on the prefix argument: (defun agda2-intro-constructor-select (old-g choices) - "con select" ;; TODO : write description here + "Constructor select interface." (interactive) - (let* ((choicesLabels (mapcar (lambda (x) (propertize (car x) 'display (concat (car x) " : " (car (cdr x)) ) )) choices)) + (let* ((choicesLabels + (mapcar (lambda (x) (cons (car x) (propertize (concat " : " (car (cdr x))) 'face 'bold))) + choices)) (z (minibuffer-with-setup-hook 'minibuffer-complete - (completing-read "Constructor: " choicesLabels nil t))) + (let ((completion-extra-properties + '(:annotation-function + (lambda (candidate) (cdr (assoc candidate choicesLabels)))))) + (completing-read "Constructor: " choicesLabels nil t)))) (y (cdr (cdr (assoc z choices ))))) - (if y (agda2-give-action old-g y)))) + (if y (agda2-give-action old-g y) (force-mode-line-update)))) (defun agda2-refine (pmlambda) diff --git a/src/full/Agda/Auto/Auto.hs b/src/full/Agda/Auto/Auto.hs index 918a03f9307..1076cff6d91 100644 --- a/src/full/Agda/Auto/Auto.hs +++ b/src/full/Agda/Auto/Auto.hs @@ -382,12 +382,12 @@ auto ii rng argstr = liftTCM $ locallyTC eMakeCase (const True) $ do case cls' of Left{} -> stopWithMsg "No solution found" Right cls' -> do - cls'' <- forM cls' $ \ (I.Clause _ _ tel ps body t catchall exact recursive reachable ell) -> do + cls'' <- forM cls' $ \ (I.Clause _ _ tel ps body t catchall exact recursive reachable ell wm) -> do withCurrentModule (AN.qnameModule def) $ do -- Normalise the dot patterns ps <- addContext tel $ normalise ps body <- etaContract body - fmap modifyAbstractClause $ inTopContext $ reify $ AN.QNamed def $ I.Clause noRange noRange tel ps body t catchall exact recursive reachable ell + fmap modifyAbstractClause $ inTopContext $ reify $ AN.QNamed def $ I.Clause noRange noRange tel ps body t catchall exact recursive reachable ell wm moduleTel <- lookupSection (AN.qnameModule def) pcs <- withInteractionId ii $ inTopContext $ addContext moduleTel $ mapM prettyA cls'' ticks <- liftIO $ readIORef ticks diff --git a/src/full/Agda/Auto/Convert.hs b/src/full/Agda/Auto/Convert.hs index 1e837fee5a3..b21a571d7d0 100644 --- a/src/full/Agda/Auto/Convert.hs +++ b/src/full/Agda/Auto/Convert.hs @@ -668,18 +668,19 @@ frommyClause (ids, pats, mrhs) = do Nothing -> return $ Nothing Just e -> Just <$> convert e let cperm = Perm nv perm - return $ I.Clause + return I.Clause { I.clauseLHSRange = SP.noRange , I.clauseFullRange = SP.noRange , I.clauseTel = tel , I.namedClausePats = IP.numberPatVars __IMPOSSIBLE__ cperm $ applySubst (renamingR $ compactP cperm) ps - , I.clauseBody = body - , I.clauseType = Nothing -- TODO: compute clause type - , I.clauseCatchall = False + , I.clauseBody = body + , I.clauseType = Nothing -- TODO: compute clause type + , I.clauseCatchall = False , I.clauseExact = Nothing -- TODO , I.clauseRecursive = Nothing -- TODO: Don't know here whether recursive or not !? , I.clauseUnreachable = Nothing -- TODO: Don't know here whether reachable or not !? - , I.clauseEllipsis = Cm.NoEllipsis + , I.clauseEllipsis = Cm.NoEllipsis + , I.clauseWhereModule = Nothing } contains_constructor :: [CSPat O] -> Bool diff --git a/src/full/Agda/Interaction/BasicOps.hs b/src/full/Agda/Interaction/BasicOps.hs index bf2e9774e31..afe73b54829 100644 --- a/src/full/Agda/Interaction/BasicOps.hs +++ b/src/full/Agda/Interaction/BasicOps.hs @@ -7,6 +7,7 @@ module Agda.Interaction.BasicOps where import Prelude hiding (null) import Control.Arrow ( first ) +import Control.Applicative ( (<*) ) import Control.Monad ( (>=>), forM, guard ) import Control.Monad.Except import Control.Monad.Reader @@ -1099,9 +1100,9 @@ introTactic pmLambda ii = do I.Def d _ -> do def <- getConstInfo d case theDef def of - Datatype{} -> addContext tel' $ introData t + Datatype{ dataCons = dc } -> addContext tel' $ introData t dc Record{ recNamedCon = name } - | name -> addContext tel' $ introData t + | name -> addContext tel' $ introData t [] | otherwise -> IntroTactic_Success <$> (addContext tel' $ introRec d) _ -> fallback _ -> fallback @@ -1137,47 +1138,63 @@ introTactic pmLambda ii = do makeName ("_", t) = ("x", t) makeName (x, t) = (x, t) - introData :: I.Type -> TCM IntroTacticResult - introData t = do + introData :: I.Type -> [QName] -> TCM IntroTacticResult + introData t cNms = do + reportSDoc "interaction.intro" 10 $ do "introData" TP.<+> prettyTCM t let tel = telFromList [defaultDom ("_", t)] pat = [defaultArg $ unnamed $ debruijnNamedVar "c" 0] r <- splitLast CoInductive tel pat - case r of - Left err -> return IntroTactic_NotFound - Right cov -> do - mTy <- getMetaType =<< lookupInteractionId ii - l <- mapM (makeIntroductionTerm mTy) $ mapMaybe (conName . scPats) $ splitClauses cov - return $ - case l of - [] -> IntroTactic_NotFound - [x@IntroOportunity{}] -> IntroTactic_Success (stringToIntroduce x) - _ -> IntroTactic_MultiplePossibleConstructors l + cHds <- + case r of + Left err -> (reportSLn "interaction.introData" 20 $ "obtaining constructors from Datatype definition") + >> return cNms + + Right cov -> do + reportSLn "interaction.introData" 20 $ "obtaining constructors via covering" + let cls = splitClauses cov + reportSLn "interaction.introData" 50 $ "splitClausesNr: " ++ show (length cls) + return $ mapMaybe (conName . scPats) $ cls + mTy <- getMetaTypeInContext =<< lookupInteractionId ii + l <- mapM (makeIntroductionTerm mTy) $ cHds + return $ + case l of + [] -> IntroTactic_NotFound + [x@IntroOportunity{}] -> IntroTactic_Success (stringToIntroduce x) + _ -> IntroTactic_MultiplePossibleConstructors l where - conName :: [NamedArg SplitPattern] -> Maybe I.ConHead + conName :: [NamedArg SplitPattern] -> Maybe QName conName [p] = case namedArg p of - I.ConP c _ _ -> Just c + I.ConP c _ _ -> Just (I.conName c) _ -> Nothing conName _ = __IMPOSSIBLE__ showUnambiguousConName v = - runAbsToCon (lookupQName AmbiguousNothing $ I.conName v) + runAbsToCon (lookupQName AmbiguousNothing $ v) + makeIntroductionTerm :: I.Type -> QName -> TCM IntroOportunity makeIntroductionTerm mTy ch = do + tcSt <- getTC cn <- (render . pretty) <$> showUnambiguousConName ch - reportSLn "interaction.introData.makeIntroductionTerm" 20 $ "constructor: " ++ cn - + reportSLn "interaction.introData.makeIntroductionTerm" 30 $ "constructor: " ++ cn (tel , renderedConstructorType) <- do - cDefTy <- defType <$> getConstInfo (I.conName ch) + cDefTy <- defType <$> getConstInfo ch ct <- prettyATop =<< reifyUnblocked =<< normalForm Normalised cDefTy return (telToList $ theTel $ telView' cDefTy , render ct) scope <- getScope + + reportSLn "interaction.introData.makeIntroductionTerm" 50 $ "telescope: " ++ (render $ pretty tel) + + mTyPP <- prettyATop =<< reifyUnblocked =<< normalForm Normalised mTy + reportSLn "interaction.introData.makeIntroductionTerm" 50 $ "against: " ++ (render $ pretty mTyPP) + + -- This applies constructor to all of its arguments, including hidden trailing args. - -- Depending on the flag, it can skip instance arguments. + -- Depending on the `includeInsArgs` flag, it can skip instance arguments. -- Resulting Expr is checked against the type of the hole. let applyMetasAndCheckAgainstHole includeInsArgs = (includeInsArgs ,) <$> do let toNA :: Dom (ArgName, I.Type) -> TCM (Maybe ((NamedArg A.Expr) , InteractionId)) @@ -1195,22 +1212,41 @@ introTactic pmLambda ii = do return $ Just (namedArgFromDom $ fmap (\_ -> metaVar) d , ii) else return Nothing mArgs <- fmap catMaybes $ traverse toNA tel - let conAppMetas = A.app (A.Con $ unambiguous $ (I.conName ch)) (fst <$> mArgs) + let conAppMetas = A.app (A.Con $ unambiguous ch) (fst <$> mArgs) checkExpr conAppMetas mTy -- If type checking without metas for instane arguments fails, -- another attempt is made - this time with metas everywhere. - (wereInstanceArgumentsIncluded , chE@(I.Con _ _ es)) <- - catchError (applyMetasAndCheckAgainstHole False) - (\_ -> applyMetasAndCheckAgainstHole True ) + (wereInstanceArgumentsIncluded , chE) <- + catchError (applyMetasAndCheckAgainstHole False + <* reportSLn "interaction.introData.makeIntroductionTerm" 40 + "Instance resolution sucessfull") + (\e -> applyMetasAndCheckAgainstHole True + <* reportSLn "interaction.introData.makeIntroductionTerm" 40 + "Instance resolution failed, fallback to adding holes for instance arguments") + + reportSLn "interaction.introData.makeIntroductionTerm" 100 $ "chE: " ++ (render $ pretty chE) + + + let (I.Con _ _ es) = chE + + reportSLn "interaction.introData.makeIntroductionTerm" 100 $ "es: " ++ (show es) + + + -- This inspects elims in typechecked term, + -- depending on the path teaken above metas for instance arguments + -- may have been introduced either during type checking or explcitly + -- in `applyMetasAndCheckAgainstHole`. + + -- elims are zipped with telescope starting from the end, so DT parameters + -- will be discarded + let revZip x y = reverse $ zip (reverse x) (reverse y) + - -- This inspects elims in inferred term, depending on the path teaken above - -- metas for instance arguments may have been introduced either - -- during type checking or manually in `applyMetasAndCheckAgainstHole`. (t :: [(MetaInstantiation , (Maybe String , Hiding))]) <- - forM (zip (argsFromElims es) tel) (\(a , d) -> do + forM (revZip (argsFromElims es) tel) (\(a , d) -> do mi <- case (unArg a) of - I.MetaV mId [] -> lookupMetaInstantiation mId + I.MetaV mId _ -> lookupMetaInstantiation mId _ -> __IMPOSSIBLE__ return (mi , (((>>= (filterMaybe (not . isGeneratedName))) . (fmap (rangedThing . woThing)) . getNameOf) d , getHiding d))) @@ -1243,6 +1279,7 @@ introTactic pmLambda ii = do then concat ["(",introStr,")"] else introStr + putTC tcSt return $ IntroOportunity { constructorName = cn , stringToIntroduce = introStrFinal diff --git a/src/full/Agda/Interaction/Highlighting/FromAbstract.hs b/src/full/Agda/Interaction/Highlighting/FromAbstract.hs index 2b69932a1de..1d5a322aaec 100644 --- a/src/full/Agda/Interaction/Highlighting/FromAbstract.hs +++ b/src/full/Agda/Interaction/Highlighting/FromAbstract.hs @@ -333,7 +333,7 @@ instance Hilite A.ProblemEq where hilite (A.ProblemEq p _t _dom) = hilite p instance Hilite A.WhereDeclarations where - hilite (A.WhereDecls m ds) = hilite m <> hilite ds + hilite (A.WhereDecls m _ ds) = hilite m <> hilite ds instance Hilite A.GeneralizeTelescope where hilite (A.GeneralizeTel _gen tel) = hilite tel diff --git a/src/full/Agda/Interaction/MakeCase.hs b/src/full/Agda/Interaction/MakeCase.hs index 3178578fa6f..ef7f0ad12c2 100644 --- a/src/full/Agda/Interaction/MakeCase.hs +++ b/src/full/Agda/Interaction/MakeCase.hs @@ -223,18 +223,19 @@ getClauseZipperForIP f clauseNo = do recheckAbstractClause :: Type -> Maybe Substitution -> A.SpineClause -> TCM (Clause, Context, [AsBinding]) recheckAbstractClause t sub acl = checkClauseLHS t sub acl $ \ lhs -> do - let cl = Clause{ clauseLHSRange = getRange acl - , clauseFullRange = getRange acl - , clauseTel = lhsVarTele lhs - , namedClausePats = lhsPatterns lhs - , clauseBody = Nothing -- We don't need the body for make case - , clauseType = Just (lhsBodyType lhs) - , clauseCatchall = False - , clauseExact = Nothing - , clauseRecursive = Nothing - , clauseUnreachable = Nothing - , clauseEllipsis = lhsEllipsis $ A.spLhsInfo $ A.clauseLHS acl - } + let cl = Clause { clauseLHSRange = getRange acl + , clauseFullRange = getRange acl + , clauseTel = lhsVarTele lhs + , namedClausePats = lhsPatterns lhs + , clauseBody = Nothing -- We don't need the body for make case + , clauseType = Just (lhsBodyType lhs) + , clauseCatchall = False + , clauseExact = Nothing + , clauseRecursive = Nothing + , clauseUnreachable = Nothing + , clauseEllipsis = lhsEllipsis $ A.spLhsInfo $ A.clauseLHS acl + , clauseWhereModule = A.whereModule $ A.clauseWhereDecls acl + } cxt <- getContext let asb = lhsAsBindings lhs return (cl, cxt, asb) @@ -501,15 +502,25 @@ makeAbsurdClause f ell (SClause tel sps _ _ t) = do , "ell =" <+> text (show ell) ] ] - withCurrentModule (qnameModule f) $ do + withCurrentModule (qnameModule f) $ -- Andreas, 2015-05-29 Issue 635 -- Contract implicit record patterns before printing. -- c <- translateRecordPatterns $ Clause noRange tel perm ps NoBody t False -- Jesper, 2015-09-19 Don't contract, since we do on-demand splitting - let c = Clause noRange noRange tel ps Nothing (argFromDom <$> t) False Nothing Nothing Nothing ell - let ps = namedClausePats c - inTopContext $ reify $ QNamed f $ c { namedClausePats = ps } - + inTopContext $ reify $ QNamed f $ Clause + { clauseLHSRange = noRange + , clauseFullRange = noRange + , clauseTel = tel + , namedClausePats = ps + , clauseBody = Nothing + , clauseType = argFromDom <$> t + , clauseCatchall = False + , clauseExact = Nothing + , clauseRecursive = Nothing + , clauseUnreachable = Nothing + , clauseEllipsis = ell + , clauseWhereModule = Nothing + } -- | Make a clause with a question mark as rhs. diff --git a/src/full/Agda/Syntax/Abstract.hs b/src/full/Agda/Syntax/Abstract.hs index 744ef5caf5e..4fa6cb0e3e7 100644 --- a/src/full/Agda/Syntax/Abstract.hs +++ b/src/full/Agda/Syntax/Abstract.hs @@ -368,12 +368,14 @@ data WhereDeclarations = WhereDecls { whereModule :: Maybe ModuleName -- #2897: we need to restrict named where modules in refined contexts, -- so remember whether it was named here - , whereDecls :: Maybe Declaration + , whereAnywhere :: Bool + -- ^ is it an ordinary unnamed @where@? + , whereDecls :: Maybe Declaration -- ^ The declaration is a 'Section'. } deriving (Data, Show, Eq, Generic) instance Null WhereDeclarations where - empty = WhereDecls empty empty + empty = WhereDecls empty False empty noWhereDecls :: WhereDeclarations noWhereDecls = empty @@ -702,7 +704,7 @@ instance HasRange RHS where getRange (RewriteRHS xes _ rhs wh) = getRange (xes, rhs, wh) instance HasRange WhereDeclarations where - getRange (WhereDecls _ ds) = getRange ds + getRange (WhereDecls _ _ ds) = getRange ds instance HasRange LetBinding where getRange (LetBind i _ _ _ _ ) = getRange i @@ -845,7 +847,7 @@ instance KillRange RHS where killRange (RewriteRHS xes spats rhs wh) = killRange4 RewriteRHS xes spats rhs wh instance KillRange WhereDeclarations where - killRange (WhereDecls a b) = killRange2 WhereDecls a b + killRange (WhereDecls a b c) = killRange3 WhereDecls a b c instance KillRange LetBinding where killRange (LetBind i info a b c) = killRange5 LetBind i info a b c diff --git a/src/full/Agda/Syntax/Abstract/Views.hs b/src/full/Agda/Syntax/Abstract/Views.hs index eebec8f8ee6..67190f798b9 100644 --- a/src/full/Agda/Syntax/Abstract/Views.hs +++ b/src/full/Agda/Syntax/Abstract/Views.hs @@ -367,7 +367,7 @@ instance (ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (Rewrite Invert qn pes -> Invert <$> recurseExpr f qn <*> recurseExpr f pes instance ExprLike WhereDeclarations where - recurseExpr f (WhereDecls a b) = WhereDecls a <$> recurseExpr f b + recurseExpr f (WhereDecls a b c) = WhereDecls a b <$> recurseExpr f c instance ExprLike ModuleApplication where recurseExpr :: forall m. RecurseExprFn m ModuleApplication @@ -519,7 +519,7 @@ instance DeclaredNames Clause where declaredNames (Clause _ _ rhs decls _) = declaredNames rhs <> declaredNames decls instance DeclaredNames WhereDeclarations where - declaredNames (WhereDecls _ ds) = declaredNames ds + declaredNames (WhereDecls _ _ ds) = declaredNames ds instance DeclaredNames RHS where declaredNames = \case diff --git a/src/full/Agda/Syntax/Internal.hs b/src/full/Agda/Syntax/Internal.hs index a7e82f1e47a..bb99315eac3 100644 --- a/src/full/Agda/Syntax/Internal.hs +++ b/src/full/Agda/Syntax/Internal.hs @@ -367,21 +367,21 @@ type NAPs = [NamedArg DeBruijnPattern] -- For the purpose of the permutation and the body dot patterns count -- as variables. TODO: Change this! data Clause = Clause - { clauseLHSRange :: Range - , clauseFullRange :: Range - , clauseTel :: Telescope + { clauseLHSRange :: Range + , clauseFullRange :: Range + , clauseTel :: Telescope -- ^ @Δ@: The types of the pattern variables in dependency order. - , namedClausePats :: NAPs + , namedClausePats :: NAPs -- ^ @Δ ⊢ ps@. The de Bruijn indices refer to @Δ@. - , clauseBody :: Maybe Term + , clauseBody :: Maybe Term -- ^ @Just v@ with @Δ ⊢ v@ for a regular clause, or @Nothing@ for an -- absurd one. - , clauseType :: Maybe (Arg Type) + , clauseType :: Maybe (Arg Type) -- ^ @Δ ⊢ t@. The type of the rhs under @clauseTel@. -- Used, e.g., by @TermCheck@. -- Can be 'Irrelevant' if we encountered an irrelevant projection -- pattern on the lhs. - , clauseCatchall :: Bool + , clauseCatchall :: Bool -- ^ Clause has been labelled as CATCHALL. , clauseExact :: Maybe Bool -- ^ Pattern matching of this clause is exact, no catch-all case. @@ -401,8 +401,10 @@ data Clause = Clause -- @Nothing@ means coverage checker has not run yet (clause may be unreachable). -- @Just False@ means clause is not unreachable. -- @Just True@ means clause is unreachable. - , clauseEllipsis :: ExpandedEllipsis + , clauseEllipsis :: ExpandedEllipsis -- ^ Was this clause created by expansion of an ellipsis? + , clauseWhereModule :: Maybe ModuleName + -- ^ Keeps track of the module name associate with the clause's where clause. } deriving (Data, Show, Generic) @@ -1046,11 +1048,12 @@ instance Null (Tele a) where -- | A 'null' clause is one with no patterns and no rhs. -- Should not exist in practice. instance Null Clause where - empty = Clause empty empty empty empty empty empty False Nothing Nothing Nothing empty - null (Clause _ _ tel pats body _ _ _ _ _ _) + empty = Clause empty empty empty empty empty empty False Nothing Nothing Nothing empty empty + null (Clause _ _ tel pats body _ _ _ _ _ _ wm) = null tel && null pats && null body + && null wm --------------------------------------------------------------------------- @@ -1224,8 +1227,8 @@ instance KillRange a => KillRange (Pattern' a) where DefP o q ps -> killRange2 (DefP o) q ps instance KillRange Clause where - killRange (Clause rl rf tel ps body t catchall exact recursive unreachable ell) = - killRange10 Clause rl rf tel ps body t catchall exact recursive unreachable ell + killRange (Clause rl rf tel ps body t catchall exact recursive unreachable ell wm) = + killRange11 Clause rl rf tel ps body t catchall exact recursive unreachable ell wm instance KillRange a => KillRange (Tele a) where killRange = fmap killRange diff --git a/src/full/Agda/Syntax/Internal/Names.hs b/src/full/Agda/Syntax/Internal/Names.hs index 368a17a1ff7..dee89042ec2 100644 --- a/src/full/Agda/Syntax/Internal/Names.hs +++ b/src/full/Agda/Syntax/Internal/Names.hs @@ -160,7 +160,7 @@ instance NamesIn Defn where -> namesAndMetasIn' sg (cl, cc) instance NamesIn Clause where - namesAndMetasIn' sg (Clause _ _ tel ps b t _ _ _ _ _) = + namesAndMetasIn' sg (Clause _ _ tel ps b t _ _ _ _ _ _) = namesAndMetasIn' sg (tel, ps, b, t) instance NamesIn CompiledClauses where diff --git a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs index fded7d4c6c1..c6d47e09819 100644 --- a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs +++ b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs @@ -1035,15 +1035,15 @@ instance ToConcrete A.LetBinding where instance ToConcrete A.WhereDeclarations where type ConOfAbs A.WhereDeclarations = WhereClause - bindToConcrete (A.WhereDecls _ Nothing) ret = ret C.NoWhere - bindToConcrete (A.WhereDecls (Just am) (Just (A.Section _ _ _ ds))) ret = do + bindToConcrete (A.WhereDecls _ _ Nothing) ret = ret C.NoWhere + bindToConcrete (A.WhereDecls (Just am) False (Just (A.Section _ _ _ ds))) ret = do ds' <- declsToConcrete ds cm <- unqualify <$> lookupModule am -- Andreas, 2016-07-08 I put PublicAccess in the following SomeWhere -- Should not really matter for printing... let wh' = (if isNoName cm then AnyWhere noRange else SomeWhere noRange cm PublicAccess) $ ds' local (openModule' am defaultImportDir id) $ ret wh' - bindToConcrete (A.WhereDecls _ (Just d)) ret = + bindToConcrete (A.WhereDecls _ _ (Just d)) ret = ret . AnyWhere noRange =<< toConcrete d mergeSigAndDef :: [C.Declaration] -> [C.Declaration] diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs index 7966e2bf7ba..c2e7ea495e2 100644 --- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs @@ -2524,7 +2524,7 @@ whereToAbstract1 r whname whds inner = do void $ -- We can ignore the returned default A.ImportDirective. openModule TopOpenModule (Just am) (C.QName m) $ defaultImportDir { publicOpen = Just noRange } - return (x, A.WhereDecls (am <$ whname) $ singleton d) + return (x, A.WhereDecls (Just am) (isNothing whname) $ singleton d) data TerminationOrPositivity = Termination | Positivity deriving (Show) diff --git a/src/full/Agda/TypeChecking/Coverage.hs b/src/full/Agda/TypeChecking/Coverage.hs index bc3c69da609..7a3f3296b8e 100644 --- a/src/full/Agda/TypeChecking/Coverage.hs +++ b/src/full/Agda/TypeChecking/Coverage.hs @@ -173,17 +173,18 @@ coverageCheck f t cs = do -- ifNotM (isEmptyTel tel) (return True) $ do -- Jesper, 2018-11-28, Issue #3407: if the clause is absurd, -- add the appropriate absurd clause to the definition. - let cl = Clause { clauseLHSRange = noRange - , clauseFullRange = noRange - , clauseTel = tel - , namedClausePats = applySubst sub ps - , clauseBody = Nothing - , clauseType = Nothing + let cl = Clause { clauseLHSRange = noRange + , clauseFullRange = noRange + , clauseTel = tel + , namedClausePats = applySubst sub ps + , clauseBody = Nothing + , clauseType = Nothing , clauseCatchall = True -- absurd clauses are safe as catch-all , clauseExact = Just False , clauseRecursive = Just False , clauseUnreachable = Just False , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } reportSDoc "tc.cover.missing" 20 $ inTopContext $ do sep [ "adding missing absurd clause" @@ -390,11 +391,12 @@ cover f cs sc@(SClause tel ps _ _ target) = updateRelevance $ do , namedClausePats = (s `applySubst` ps) ++ extra , clauseBody = (`applyE` patternsToElims extra) . (s `applyPatSubst`) <$> clauseBody cl , clauseType = ty - , clauseCatchall = clauseCatchall cl - , clauseExact = clauseExact cl - , clauseRecursive = clauseRecursive cl + , clauseCatchall = clauseCatchall cl + , clauseExact = clauseExact cl + , clauseRecursive = clauseRecursive cl , clauseUnreachable = clauseUnreachable cl - , clauseEllipsis = clauseEllipsis cl + , clauseEllipsis = clauseEllipsis cl + , clauseWhereModule = clauseWhereModule cl } where (vs,qs) = unzip mps @@ -600,11 +602,12 @@ inferMissingClause f (SClause tel ps _ cps (Just t)) = setCurrentRange f $ do , namedClausePats = fromSplitPatterns ps , clauseBody = Just rhs , clauseType = Just (argFromDom t) - , clauseCatchall = False + , clauseCatchall = False , clauseExact = Just True , clauseRecursive = Nothing -- could be recursive , clauseUnreachable = Just False -- missing, thus, not unreachable - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } addClauses f [cl] -- Important: add at the end. return cl diff --git a/src/full/Agda/TypeChecking/Coverage/Cubical.hs b/src/full/Agda/TypeChecking/Coverage/Cubical.hs index 5b0849213cd..0f9e13fd9a1 100644 --- a/src/full/Agda/TypeChecking/Coverage/Cubical.hs +++ b/src/full/Agda/TypeChecking/Coverage/Cubical.hs @@ -359,18 +359,19 @@ createMissingTrXTrXClause q_trX f n x old_sc = do (,,) <$> ps <*> rhsTy <*> rhs let (ps,ty,rhs) = unAbsN $ unAbs $ unAbsN $ unAbs $ unAbsN $ unAbs $ unAbsN $ ps_ty_rhs reportSDoc "tc.cover.trx.trx" 20 $ "trX-trX clause for" <+> prettyTCM f - let c = Clause { clauseTel = cTel - , namedClausePats = ps - , clauseBody = Just rhs - , clauseType = Just $ Arg (getArgInfo ty) (unDom ty) - , clauseLHSRange = noRange - , clauseFullRange = noRange - , clauseCatchall = False - , clauseRecursive = Just True - , clauseUnreachable = Just False - , clauseEllipsis = NoEllipsis - , clauseExact = Nothing - } + let c = Clause { clauseLHSRange = noRange + , clauseFullRange = noRange + , clauseTel = cTel + , namedClausePats = ps + , clauseBody = Just rhs + , clauseType = Just $ Arg (getArgInfo ty) (unDom ty) + , clauseCatchall = False + , clauseExact = Nothing + , clauseRecursive = Just True + , clauseUnreachable = Just False + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing + } debugClause "tc.cover.trx.trx" c return $ c createMissingTrXHCompClause :: QName @@ -627,20 +628,21 @@ createMissingTrXHCompClause q_trX f n x old_sc = do (,,) <$> ps <*> rhsTy <*> pure rhs let (ps,ty,rhs) = unAbsN $ unAbs $ unAbs $ unAbs $ unAbsN $ unAbs $ unAbsN $ ps_ty_rhs reportSDoc "tc.cover.trx.hcomp" 20 $ "trX-hcomp clause for" <+> prettyTCM f - let c = Clause { clauseTel = cTel - , namedClausePats = ps - , clauseBody = Just rhs - , clauseType = Just $ Arg (getArgInfo ty) (unDom ty) - , clauseLHSRange = noRange - , clauseFullRange = noRange - , clauseCatchall = False - , clauseRecursive = Just True - , clauseUnreachable = Just False - , clauseEllipsis = NoEllipsis - , clauseExact = Nothing - } + let c = Clause { clauseLHSRange = noRange + , clauseFullRange = noRange + , clauseTel = cTel + , namedClausePats = ps + , clauseBody = Just rhs + , clauseType = Just $ Arg (getArgInfo ty) (unDom ty) + , clauseCatchall = False + , clauseExact = Nothing + , clauseRecursive = Just True + , clauseUnreachable = Just False + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing + } debugClause "tc.cover.trx.hcomp" c - return $ c + return c createMissingTrXConClause :: QName -- trX -> QName -- f defined -> Arg Nat @@ -861,17 +863,18 @@ createMissingTrXConClause q_trX f n x old_sc c (UE gamma gamma' xTel u v rho tau qs <- mapM (fmap (fromMaybe __IMPOSSIBLE__) . getName') [builtinINeg, builtinIMax, builtinIMin] rhs <- addContext cTel $ locallyReduceDefs (OnlyReduceDefs (Set.fromList $ q_trX : qs)) $ normalise rhs - let cl = Clause { clauseTel = cTel - , namedClausePats = ps - , clauseBody = Just rhs - , clauseType = Just $ Arg (getArgInfo ty) (unDom ty) - , clauseLHSRange = noRange + let cl = Clause { clauseLHSRange = noRange , clauseFullRange = noRange - , clauseCatchall = False - , clauseRecursive = Just True + , clauseTel = cTel + , namedClausePats = ps + , clauseBody = Just rhs + , clauseType = Just $ Arg (getArgInfo ty) (unDom ty) + , clauseCatchall = False + , clauseExact = Nothing + , clauseRecursive = Just True , clauseUnreachable = Just False - , clauseEllipsis = NoEllipsis - , clauseExact = Nothing + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } @@ -1111,11 +1114,12 @@ createMissingConIdClause f _n x old_sc (TheInfo info) = setCurrentRange f $ do , namedClausePats = ps , clauseBody = Just $ rhs , clauseType = Just $ Arg (domInfo ty) (unDom ty) - , clauseCatchall = False + , clauseCatchall = False , clauseUnreachable = Just False -- missing, thus, not unreachable - , clauseRecursive = Just False - , clauseEllipsis = NoEllipsis - , clauseExact = Nothing + , clauseRecursive = Just False + , clauseEllipsis = NoEllipsis + , clauseExact = Nothing + , clauseWhereModule = Nothing } addClauses f [cl] return $ Just ((SplitCon conId,SplittingDone (size working_tel)),cl) @@ -1356,11 +1360,12 @@ createMissingHCompClause f n x old_sc (SClause tel ps _sigma' _cps (Just t)) cs , namedClausePats = fromSplitPatterns ps , clauseBody = Just $ rhs , clauseType = Just $ defaultArg t - , clauseCatchall = False + , clauseCatchall = False , clauseExact = Just True , clauseRecursive = Nothing -- TODO: can it be recursive? , clauseUnreachable = Just False -- missing, thus, not unreachable - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } addClauses f [cl] -- Important: add at the end. let result = CoverResult diff --git a/src/full/Agda/TypeChecking/Functions.hs b/src/full/Agda/TypeChecking/Functions.hs index 7c6147958a1..c1aa9559b7e 100644 --- a/src/full/Agda/TypeChecking/Functions.hs +++ b/src/full/Agda/TypeChecking/Functions.hs @@ -38,9 +38,9 @@ import Agda.Utils.Size etaExpandClause :: MonadTCM tcm => Clause -> tcm Clause etaExpandClause clause = liftTCM $ do case clause of - Clause _ _ ctel ps _ Nothing _ _ _ _ _ -> return clause - Clause _ _ ctel ps Nothing (Just t) _ _ _ _ _ -> return clause - Clause rl rf ctel ps (Just body) (Just t) catchall exact recursive unreachable ell -> do + Clause _ _ ctel ps _ Nothing _ _ _ _ _ _ -> return clause + Clause _ _ ctel ps Nothing (Just t) _ _ _ _ _ _ -> return clause + Clause rl rf ctel ps (Just body) (Just t) catchall exact recursive unreachable ell wm -> do -- Get the telescope to expand the clause with. TelV tel0 t' <- addContext ctel $ telView $ unArg t @@ -62,7 +62,7 @@ etaExpandClause clause = liftTCM $ do , " xs = " <+> text (prettyShow xs) , " new tel = " <+> prettyTCM ctel' ] - return $ Clause rl rf ctel' ps' (Just body') (Just (t $> t')) catchall exact recursive unreachable ell + return $ Clause rl rf ctel' ps' (Just body') (Just (t $> t')) catchall exact recursive unreachable ell wm where -- Get all initial lambdas of the body. peekLambdas :: Term -> [Arg ArgName] diff --git a/src/full/Agda/TypeChecking/IApplyConfluence.hs b/src/full/Agda/TypeChecking/IApplyConfluence.hs index 5131e2412f2..57a8bdbd062 100644 --- a/src/full/Agda/TypeChecking/IApplyConfluence.hs +++ b/src/full/Agda/TypeChecking/IApplyConfluence.hs @@ -49,7 +49,7 @@ checkIApplyConfluence_ f = whenM (isJust . optCubical <$> pragmaOptions) $ do case theDef d of Function{funClauses = cls', funCovering = cls} -> do reportSDoc "tc.cover.iapply" 10 $ text "length cls =" <+> pretty (length cls) - when (null cls && not (null $ concatMap (iApplyVars . namedClausePats) cls')) $ + when (null cls && any (not . null . iApplyVars . namedClausePats) cls') $ __IMPOSSIBLE__ modifySignature $ updateDefinition f $ updateTheDef $ updateCovering (const []) diff --git a/src/full/Agda/TypeChecking/Irrelevance.hs b/src/full/Agda/TypeChecking/Irrelevance.hs index 4ee1f2e450d..8e5b0867ac7 100644 --- a/src/full/Agda/TypeChecking/Irrelevance.hs +++ b/src/full/Agda/TypeChecking/Irrelevance.hs @@ -399,7 +399,15 @@ instance UsableModality Term where text ("has modality " ++ show fmod ++ ", which is a " ++ (if ok then "" else "NOT ") ++ "more usable modality than " ++ show mod) return ok `and2M` usableMod mod vs - Con c _ vs -> usableMod mod vs + Con c o vs -> do + cmod <- modalityOfConst (conName c) + let ok = cmod `moreUsableModality` mod + reportSDoc "tc.irr" 50 $ + "The constructor" <+> prettyTCM (Con c o []) <+> + text ("has the modality " ++ show cmod ++ ", which is " ++ + (if ok then "" else "NOT ") ++ + "more usable than the modality " ++ show mod ++ ".") + return ok `and2M` usableMod mod vs Lit l -> return True Lam info v -> usableModAbs info mod v -- Even if Pi contains Type, here we check it as a constructor for terms in the universe. diff --git a/src/full/Agda/TypeChecking/Monad/Signature.hs b/src/full/Agda/TypeChecking/Monad/Signature.hs index 625dcecb06a..32e0972d1dd 100644 --- a/src/full/Agda/TypeChecking/Monad/Signature.hs +++ b/src/full/Agda/TypeChecking/Monad/Signature.hs @@ -552,19 +552,20 @@ applySection' new ptel old ts ScopeCopyInfo{ renNames = rd, renModules = rm } = reportSDoc "tc.mod.apply" 80 $ ("new def for" <+> pretty x) pretty newDef return newDef - cl = Clause { clauseLHSRange = getRange $ defClauses d - , clauseFullRange = getRange $ defClauses d - , clauseTel = EmptyTel - , namedClausePats = [] - , clauseBody = Just $ dropArgs pars $ case oldDef of + cl = Clause { clauseLHSRange = getRange $ defClauses d + , clauseFullRange = getRange $ defClauses d + , clauseTel = EmptyTel + , namedClausePats = [] + , clauseBody = Just $ dropArgs pars $ case oldDef of Function{funProjection = Just p} -> projDropParsApply p ProjSystem rel ts' _ -> Def x $ map Apply ts' - , clauseType = Just $ defaultArg t - , clauseCatchall = False + , clauseType = Just $ defaultArg t + , clauseCatchall = False , clauseExact = Just True , clauseRecursive = Just False -- definitely not recursive , clauseUnreachable = Just False -- definitely not unreachable - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } where -- The number of remaining parameters. We need to drop the diff --git a/src/full/Agda/TypeChecking/ProjectionLike.hs b/src/full/Agda/TypeChecking/ProjectionLike.hs index 1b4a7518fcc..382091ed3bb 100644 --- a/src/full/Agda/TypeChecking/ProjectionLike.hs +++ b/src/full/Agda/TypeChecking/ProjectionLike.hs @@ -161,9 +161,9 @@ data ProjEliminator = EvenLone | ButLone | NoPostfix -- on (applications of) projection-like functions. elimView :: PureTCM m => ProjEliminator -> Term -> m Term elimView pe v = do - reportSDoc "tc.conv.elim" 30 $ "elimView of " <+> prettyTCM v + reportSDoc "tc.conv.elim" 60 $ "elimView of " <+> prettyTCM v v <- reduceProjectionLike v - reportSDoc "tc.conv.elim" 40 $ + reportSDoc "tc.conv.elim" 65 $ "elimView (projections reduced) of " <+> prettyTCM v case pe of NoPostfix -> return v diff --git a/src/full/Agda/TypeChecking/Reduce.hs b/src/full/Agda/TypeChecking/Reduce.hs index 0cc7c2a53dd..4531242c0fd 100644 --- a/src/full/Agda/TypeChecking/Reduce.hs +++ b/src/full/Agda/TypeChecking/Reduce.hs @@ -1587,7 +1587,7 @@ instance InstantiateFull CompiledClauses where instantiateFull' (Case n bs) = Case n <$> instantiateFull' bs instance InstantiateFull Clause where - instantiateFull' (Clause rl rf tel ps b t catchall exact recursive unreachable ell) = + instantiateFull' (Clause rl rf tel ps b t catchall exact recursive unreachable ell wm) = Clause rl rf <$> instantiateFull' tel <*> instantiateFull' ps <*> instantiateFull' b @@ -1597,6 +1597,7 @@ instance InstantiateFull Clause where <*> return recursive <*> return unreachable <*> return ell + <*> return wm instance InstantiateFull Instantiation where instantiateFull' (Instantiation a b) = diff --git a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs index a857c5cb05c..503c93ebbee 100644 --- a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs +++ b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs @@ -410,9 +410,9 @@ reallyFree xs v = do pickFree NotFree f2 = f2 -makeSubstitution :: Telescope -> Sub -> Substitution +makeSubstitution :: Telescope -> Sub -> Maybe Substitution makeSubstitution gamma sub = - parallelS $ map (fromMaybe __DUMMY_TERM__ . val) [0 .. size gamma-1] + parallelS <$> traverse val [0 .. size gamma-1] where val i = case IntMap.lookup i sub of Just (Irrelevant, v) -> Just $ dontCare v @@ -437,13 +437,15 @@ nonLinMatch gamma t p v = do [ "matching failed during" <+> text msg , "blocking: " <+> text (show b) ]) $ return (Left b) caseEitherM (runNLM $ match Relevant gamma EmptyTel t p v) (no "matching") $ \ s -> do - let sub = makeSubstitution gamma $ s^.nlmSub + let msub = makeSubstitution gamma $ s^.nlmSub eqs = s^.nlmEqs - traceSDoc "rewriting.match" 90 (text $ "sub = " ++ show sub) $ do - ok <- checkPostponedEquations sub eqs - case ok of - Nothing -> return $ Right sub - Just b -> no "checking of postponed equations" b + traceSDoc "rewriting.match" 90 (text $ "msub = " ++ show msub) $ case msub of + Nothing -> no "checking that all variables are bound" notBlocked_ + Just sub -> do + ok <- checkPostponedEquations sub eqs + case ok of + Nothing -> return $ Right sub + Just b -> no "checking of postponed equations" b -- | Typed βη-equality, also handles empty record types. -- Returns `Nothing` if the terms are equal, or `Just b` if the terms are not diff --git a/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs b/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs index 78a2c50a71f..b60f3b3c847 100644 --- a/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs +++ b/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs @@ -135,11 +135,12 @@ bindBuiltinFlat x = ConP sharpCon cpi [ argN $ Named Nothing $ debruijnNamedVar "x" 0 ] ] , clauseBody = Just $ var 0 , clauseType = Just $ defaultArg $ El (varSort 2) $ var 1 - , clauseCatchall = False + , clauseCatchall = False , clauseExact = Just True , clauseRecursive = Just False , clauseUnreachable = Just False - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } cc = Case (defaultArg 0) $ conCase sharp False $ WithArity 1 $ Done [defaultArg "x"] $ var 0 projection = Projection diff --git a/src/full/Agda/TypeChecking/Rules/Data.hs b/src/full/Agda/TypeChecking/Rules/Data.hs index 599dc2f9074..c8c45609294 100644 --- a/src/full/Agda/TypeChecking/Rules/Data.hs +++ b/src/full/Agda/TypeChecking/Rules/Data.hs @@ -608,6 +608,7 @@ defineCompData d con params names fsT t boundary = do -- Or: Just False; is it known to be non-recursive? , clauseUnreachable = Just False , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } cs = [clause] addClauses theName cs @@ -1274,7 +1275,8 @@ defineConClause trD' isHIT mtrX npars nixs xTel' telI sigma dT' cnames = do -- it is indirectly recursive through transp, does it count? , clauseUnreachable = Just False , clauseEllipsis = NoEllipsis - , clauseExact = Nothing + , clauseExact = Nothing + , clauseWhereModule = Nothing } reportSDoc "tc.data.transp.con" 20 $ "gamma:" <+> prettyTCM gamma diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs index 79a7a72da27..8162b7e36b7 100644 --- a/src/full/Agda/TypeChecking/Rules/Def.hs +++ b/src/full/Agda/TypeChecking/Rules/Def.hs @@ -194,11 +194,12 @@ checkAlias t ai delayed i name e mc = , namedClausePats = [] , clauseBody = Just $ bodyMod v , clauseType = Just $ Arg ai t - , clauseCatchall = False - , clauseExact = Just True - , clauseRecursive = Nothing -- we don't know yet + , clauseCatchall = False + , clauseExact = Just True + , clauseRecursive = Nothing -- we don't know yet , clauseUnreachable = Just False - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } ] , funCompiled = Just $ Done [] $ bodyMod v , funSplitTree = Just $ SplittingDone 0 @@ -332,15 +333,16 @@ checkFunDefS t ai delayed extlam with i name withSub cs = do let c = Clause { clauseFullRange = noRange , clauseLHSRange = noRange - , clauseTel = tel + , clauseTel = tel , namedClausePats = teleNamedArgs tel - , clauseBody = Nothing - , clauseType = Just (defaultArg t) - , clauseCatchall = False - , clauseExact = Just True - , clauseRecursive = Just False + , clauseBody = Nothing + , clauseType = Just (defaultArg t) + , clauseCatchall = False + , clauseExact = Just True + , clauseRecursive = Just False , clauseUnreachable = Just False - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } return (cs ++ [c], pure sys) @@ -746,19 +748,6 @@ checkClause t withSub c@(A.Clause lhs@(A.SpineLHS i x aps) strippedPats rhs0 wh ] ] - -- check naturality wrt the interval. - let - -- TODO:: Defined but not used - iApplyVars :: [NamedArg DeBruijnPattern] -> [(Int, (Term,Term))] - iApplyVars ps = flip concatMap (map namedArg ps) $ \case - IApplyP _ t u x -> [(dbPatVarIndex x,(t,u))] - VarP{} -> [] - ProjP{}-> [] - LitP{} -> [] - DotP{} -> [] - DefP _ _ ps -> iApplyVars ps - ConP _ _ ps -> iApplyVars ps - -- compute body modification for irrelevant definitions, see issue 610 rel <- asksTC getRelevance let bodyMod body = case rel of @@ -783,7 +772,8 @@ checkClause t withSub c@(A.Clause lhs@(A.SpineLHS i x aps) strippedPats rhs0 wh , clauseExact = exact , clauseRecursive = Nothing -- we don't know yet , clauseUnreachable = Nothing -- we don't know yet - , clauseEllipsis = lhsEllipsis i + , clauseEllipsis = lhsEllipsis i + , clauseWhereModule = A.whereModule wh } @@ -1223,8 +1213,8 @@ checkWhere :: A.WhereDeclarations -- ^ Where-declarations to check. -> TCM a -- ^ Continuation. -> TCM a -checkWhere wh@(A.WhereDecls whmod ds) ret = do - ensureNoNamedWhereInRefinedContext whmod +checkWhere wh@(A.WhereDecls whmod whNamed ds) ret = do + when (not whNamed) $ ensureNoNamedWhereInRefinedContext whmod loop ds where loop = \case diff --git a/src/full/Agda/TypeChecking/Rules/Record.hs b/src/full/Agda/TypeChecking/Rules/Record.hs index cfa50b71eaf..058d966d1ea 100644 --- a/src/full/Agda/TypeChecking/Rules/Record.hs +++ b/src/full/Agda/TypeChecking/Rules/Record.hs @@ -489,36 +489,38 @@ defineTranspOrHCompR cmd name params fsT fns rect = do (g0,_:g1) = splitAt (size gamma - 1 - ix) $ flattenTel gamma (ns0,_:ns1) = splitAt (size gamma - 1 - ix) $ teleNames gamma - c = Clause { clauseTel = gamma' - , clauseType = Just $ argN t - , namedClausePats = pats - , clauseFullRange = noRange + c = Clause { clauseFullRange = noRange , clauseLHSRange = noRange - , clauseCatchall = False + , clauseTel = gamma' + , namedClausePats = pats , clauseBody = Just $ rhs + , clauseType = Just $ argN t + , clauseCatchall = False , clauseExact = Just True , clauseRecursive = Just False -- definitely non-recursive! , clauseUnreachable = Just False - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } reportSDoc "trans.rec.face" 17 $ text $ show c return c cs <- forM (zip3 fns clause_types bodies) $ \ (fname, clause_ty, body) -> do let pats = teleNamedArgs gamma ++ [defaultNamedArg $ ProjP ProjSystem $ unArg fname] - c = Clause { clauseTel = gamma - , clauseType = Just $ argN (unDom clause_ty) - , namedClausePats = pats - , clauseFullRange = noRange + c = Clause { clauseFullRange = noRange , clauseLHSRange = noRange - , clauseCatchall = False + , clauseTel = gamma + , namedClausePats = pats , clauseBody = Just body + , clauseType = Just $ argN (unDom clause_ty) + , clauseCatchall = False , clauseExact = Just True , clauseRecursive = Nothing -- Andreas 2020-02-06 TODO -- Or: Just False; is it known to be non-recursive? , clauseUnreachable = Just False - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } reportSDoc "trans.rec" 17 $ text $ show c reportSDoc "trans.rec" 16 $ text "type =" <+> text (show (clauseType c)) @@ -695,7 +697,8 @@ checkRecordProjections m r hasNamedCon con tel ftel fs = do , clauseExact = Just True , clauseRecursive = Just False , clauseUnreachable = Just False - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } let projection = Projection diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs b/src/full/Agda/TypeChecking/Rules/Term.hs index 4969d9a802b..65d37f3b773 100644 --- a/src/full/Agda/TypeChecking/Rules/Term.hs +++ b/src/full/Agda/TypeChecking/Rules/Term.hs @@ -759,7 +759,8 @@ checkAbsurdLambda cmp i h e t = localTC (set eQuantity topQuantity) $ do , clauseExact = Just False , clauseRecursive = Just False , clauseUnreachable = Just True -- absurd clauses are unreachable - , clauseEllipsis = NoEllipsis + , clauseEllipsis = NoEllipsis + , clauseWhereModule = Nothing } ] , funCompiled = Just $ Fail [Arg info' "()"] diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs index bbfd0df4387..98e5bab9f9f 100644 --- a/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs +++ b/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs @@ -485,7 +485,7 @@ instance EmbPrj TermHead where valu _ = malformed instance EmbPrj I.Clause where - icod_ (Clause a b c d e f g h i j k) = icodeN' Clause a b c d e f g h i j k + icod_ (Clause a b c d e f g h i j k l) = icodeN' Clause a b c d e f g h i j k l value = valueN Clause diff --git a/src/full/Agda/TypeChecking/Sort.hs b/src/full/Agda/TypeChecking/Sort.hs index 1d1bf5fd954..3ef187f62f8 100644 --- a/src/full/Agda/TypeChecking/Sort.hs +++ b/src/full/Agda/TypeChecking/Sort.hs @@ -165,7 +165,7 @@ sortOf :: forall m. (PureTCM m, MonadBlock m) => Term -> m Sort sortOf t = do - reportSDoc "tc.sort" 40 $ "sortOf" <+> prettyTCM t + reportSDoc "tc.sort" 60 $ "sortOf" <+> prettyTCM t sortOfT =<< elimView EvenLone t where diff --git a/src/full/Agda/TypeChecking/Substitute.hs b/src/full/Agda/TypeChecking/Substitute.hs index 943ac62e3ee..c00b3b2a2d3 100644 --- a/src/full/Agda/TypeChecking/Substitute.hs +++ b/src/full/Agda/TypeChecking/Substitute.hs @@ -360,7 +360,7 @@ instance Apply Clause where -- It is assumed that we only apply a clause to "parameters", i.e. -- arguments introduced by lambda lifting. The problem is that these aren't -- necessarily the first elements of the clause telescope. - apply cls@(Clause rl rf tel ps b t catchall exact recursive unreachable ell) args + apply cls@(Clause rl rf tel ps b t catchall exact recursive unreachable ell wm) args | length args > length ps = __IMPOSSIBLE__ | otherwise = Clause rl rf @@ -373,6 +373,7 @@ instance Apply Clause where recursive unreachable ell + wm where -- We have -- Γ ⊢ args, for some outer context Γ @@ -702,7 +703,7 @@ instance Abstract PrimFun where where n = size tel instance Abstract Clause where - abstract tel (Clause rl rf tel' ps b t catchall exact recursive unreachable ell) = + abstract tel (Clause rl rf tel' ps b t catchall exact recursive unreachable ell wm) = Clause rl rf (abstract tel tel') (namedTelVars m tel ++ ps) b @@ -712,6 +713,7 @@ instance Abstract Clause where recursive unreachable ell + wm where m = size tel + size tel' instance Abstract CompiledClauses where @@ -1201,8 +1203,10 @@ telView'UpTo 0 t = TelV EmptyTel t telView'UpTo n t = case unEl t of Pi a b -> absV a (absName b) $ telView'UpTo (n - 1) (absBody b) _ -> TelV EmptyTel t - where - absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t + +-- | Add given binding to the front of the telescope. +absV :: Dom a -> ArgName -> TelV a -> TelV a +absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t -- ** Creating telescopes from lists of types diff --git a/src/full/Agda/TypeChecking/Telescope.hs b/src/full/Agda/TypeChecking/Telescope.hs index f74d6e72653..04e1f3481cc 100644 --- a/src/full/Agda/TypeChecking/Telescope.hs +++ b/src/full/Agda/TypeChecking/Telescope.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ViewPatterns #-} module Agda.TypeChecking.Telescope where @@ -5,6 +6,7 @@ import Prelude hiding (null) import Control.Monad +import Data.Bifunctor (first) import Data.Foldable (find) import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet @@ -377,25 +379,23 @@ telViewUpTo' n p t = do Pi a b | p a -> absV a (absName b) <$> do underAbstractionAbs a b $ \b -> telViewUpTo' (n - 1) p b _ -> return $ TelV EmptyTel t - where - absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t telViewPath :: PureTCM m => Type -> m TelView telViewPath = telViewUpToPath (-1) -- | @telViewUpToPath n t@ takes off $t$ -- the first @n@ (or arbitrary many if @n < 0@) function domains or Path types. +-- +-- @telViewUpToPath n t = fst <$> telViewUpToPathBoundary'n t@ telViewUpToPath :: PureTCM m => Int -> Type -> m TelView -telViewUpToPath 0 t = return $ TelV EmptyTel t -telViewUpToPath n t = do - vt <- pathViewAsPi $ t - case vt of - Left (a,b) -> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b) - Right (El _ t) | Pi a b <- t - -> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b) - Right t -> return $ TelV EmptyTel t +telViewUpToPath n t = if n == 0 then done t else do + pathViewAsPi t >>= \case + Left (a, b) -> recurse a b + Right (El _ (Pi a b)) -> recurse a b + Right t -> done t where - absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t + done t = return $ TelV EmptyTel t + recurse a b = absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b) -- | [[ (i,(x,y)) ]] = [(i=0) -> x, (i=1) -> y] type Boundary = Boundary' (Term,Term) @@ -405,20 +405,17 @@ type Boundary' a = [(Term,a)] -- by the Path types encountered. The boundary terms live in the -- telescope given by the @TelView@. -- Each point of the boundary has the type of the codomain of the Path type it got taken from, see @fullBoundary@. -telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView,Boundary) -telViewUpToPathBoundary' 0 t = return $ (TelV EmptyTel t,[]) -telViewUpToPathBoundary' n t = do - vt <- pathViewAsPi' $ t - case vt of - Left ((a,b),xy) -> addEndPoints xy . absV a (absName b) <$> telViewUpToPathBoundary' (n - 1) (absBody b) - Right (El _ t) | Pi a b <- t - -> absV a (absName b) <$> telViewUpToPathBoundary' (n - 1) (absBody b) - Right t -> return $ (TelV EmptyTel t,[]) +telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView, Boundary) +telViewUpToPathBoundary' n t = if n == 0 then done t else do + pathViewAsPi' t >>= \case + Left ((a, b), xy) -> addEndPoints xy <$> recurse a b + Right (El _ (Pi a b)) -> recurse a b + Right t -> done t where - absV a x (TelV tel t, cs) = (TelV (ExtendTel a (Abs x tel)) t, cs) - addEndPoints xy (telv@(TelV tel _),cs) = (telv, (var $ size tel - 1, xyInTel):cs) - where - xyInTel = raise (size tel) xy + done t = return (TelV EmptyTel t, []) + recurse a b = first (absV a (absName b)) <$> telViewUpToPathBoundary' (n - 1) (absBody b) + addEndPoints xy (telv@(TelV tel _), cs) = + (telv, (var $ size tel - 1, raise (size tel) xy) : cs) fullBoundary :: Telescope -> Boundary -> Boundary @@ -478,10 +475,12 @@ teleElims tel boundary = recurse (teleArgs tel) Just i | Just (t,u) <- matchVar i -> IApply t u p _ -> Apply a +-- | Reduces 'Type'. pathViewAsPi :: PureTCM m => Type -> m (Either (Dom Type, Abs Type) Type) pathViewAsPi t = either (Left . fst) Right <$> pathViewAsPi' t +-- | Reduces 'Type'. pathViewAsPi' :: PureTCM m => Type -> m (Either ((Dom Type, Abs Type), (Term,Term)) Type) pathViewAsPi' t = do @@ -493,44 +492,42 @@ pathViewAsPi'whnf pathViewAsPi'whnf = do view <- pathView' minterval <- getTerm' builtinInterval - return $ \ t -> case view t of - PathType s l p a x y | Just interval <- minterval -> + return $ \case + (view -> PathType s l p a x y) | Just interval <- minterval -> let name | Lam _ (Abs n _) <- unArg a = n | otherwise = "i" - i = El intervalSort interval in - Left $ ((defaultDom $ i, Abs name $ El (raise 1 s) $ raise 1 (unArg a) `apply` [defaultArg $ var 0]), (unArg x, unArg y)) + Left ( ( defaultDom $ El intervalSort interval + , Abs name $ El (raise 1 s) $ raise 1 (unArg a) `apply` [defaultArg $ var 0] + ) + , (unArg x, unArg y) + ) - _ -> Right t + t -> Right t --- | returns Left (a,b) in case the type is @Pi a b@ or @PathP b _ _@ --- assumes the type is in whnf. +-- | Returns @Left (a,b)@ in case the type is @Pi a b@ or @PathP b _ _@. +-- Assumes the 'Type' is in whnf. piOrPath :: HasBuiltins m => Type -> m (Either (Dom Type, Abs Type) Type) piOrPath t = do - t <- pathViewAsPi'whnf <*> pure t - case t of - Left (p,_) -> return $ Left p - Right (El _ (Pi a b)) -> return $ Left (a,b) - Right t -> return $ Right t + (pathViewAsPi'whnf <*> pure t) <&> \case + Left (p, _) -> Left p + Right (El _ (Pi a b)) -> Left (a,b) + Right _ -> Right t +-- | Assumes 'Type' is in whnf. telView'UpToPath :: Int -> Type -> TCM TelView -telView'UpToPath 0 t = return $ TelV EmptyTel t -telView'UpToPath n t = do - vt <- pathViewAsPi'whnf <*> pure t - case vt of - Left ((a,b),_) -> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b) - Right (El _ t) | Pi a b <- t - -> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b) - Right t -> return $ TelV EmptyTel t +telView'UpToPath n t = if n == 0 then done else do + piOrPath t >>= \case + Left (a, b) -> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b) + Right _ -> done where - absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t + done = return $ TelV EmptyTel t telView'Path :: Type -> TCM TelView telView'Path = telView'UpToPath (-1) -isPath - :: PureTCM m => Type -> m (Maybe (Dom Type, Abs Type)) -isPath t = either Just (const Nothing) <$> pathViewAsPi t +isPath :: PureTCM m => Type -> m (Maybe (Dom Type, Abs Type)) +isPath = either Just (const Nothing) <.> pathViewAsPi telePatterns :: DeBruijn a => Telescope -> Boundary -> [NamedArg (Pattern' a)] telePatterns = telePatterns' teleNamedArgs diff --git a/src/full/Agda/TypeChecking/Telescope/Path.hs b/src/full/Agda/TypeChecking/Telescope/Path.hs index 82f811454ae..4e315aafdf1 100644 --- a/src/full/Agda/TypeChecking/Telescope/Path.hs +++ b/src/full/Agda/TypeChecking/Telescope/Path.hs @@ -17,6 +17,7 @@ import Agda.TypeChecking.Reduce import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope +import Agda.Utils.Functor import Agda.Utils.List import Agda.Utils.Maybe import Agda.Utils.Size @@ -91,27 +92,34 @@ telePiPath_ tel t bndry = do -- Does not reduce the type. arityPiPath :: Type -> TCM Int arityPiPath t = do - t' <- piOrPath t - case t' of - Left (_ , u) -> (+1) <$> arityPiPath (unAbs u) - Right _ -> return 0 - -iApplyVars :: DeBruijn a => [NamedArg (Pattern' a)] -> [Int] -iApplyVars ps = flip concatMap (map namedArg ps) $ \case - IApplyP _ t u x -> - [fromMaybe __IMPOSSIBLE__ (deBruijnView x)] - VarP{} -> [] - ProjP{}-> [] - LitP{} -> [] - DotP{} -> [] - DefP _ _ ps -> iApplyVars ps - ConP _ _ ps -> iApplyVars ps + piOrPath t >>= \case + Left (_, u) -> (+1) <$> arityPiPath (unAbs u) + Right _ -> return 0 +-- | Collect the interval copattern variables as list of de Bruijn indices. +class IApplyVars p where + iApplyVars :: p -> [Int] + +instance DeBruijn a => IApplyVars (Pattern' a) where + iApplyVars = \case + IApplyP _ t u x -> [ fromMaybe __IMPOSSIBLE__ $ deBruijnView x ] + VarP{} -> [] + ProjP{} -> [] + LitP{} -> [] + DotP{} -> [] + DefP _ _ ps -> iApplyVars ps + ConP _ _ ps -> iApplyVars ps + +instance IApplyVars p => IApplyVars (NamedArg p) where + iApplyVars = iApplyVars . namedArg + +instance IApplyVars p => IApplyVars [p] where + iApplyVars = concatMap iApplyVars + +-- | Check whether a type is the built-in interval type. isInterval :: (MonadTCM m, MonadReduce m) => Type -> m Bool isInterval t = liftTCM $ do - mi <- getName' builtinInterval - caseMaybe mi (return False) $ \ i -> do - t <- reduce $ unEl t - case t of - Def q [] -> return $ q == i - _ -> return $ False + caseMaybeM (getName' builtinInterval) (return False) $ \ i -> do + reduce (unEl t) <&> \case + Def q [] -> q == i + _ -> False diff --git a/src/github/workflows/stack.yml b/src/github/workflows/stack.yml index 43496e48cc5..39b5f7c7ea2 100644 --- a/src/github/workflows/stack.yml +++ b/src/github/workflows/stack.yml @@ -163,7 +163,7 @@ jobs: # A unique cache is used for each stack.yaml. # Note that matrix.stack-ver might be simply 'latest', so we use STACK_VER. key: | - ${{ runner.os }}-stack-00-${{ env.STACK_VER }}-${{ env.GHC_VER }}-${{ hashFiles(format('stack-{0}.yaml.lock', env.GHC_VER)) }} + ${{ runner.os }}-stack-20220503-${{ env.STACK_VER }}-${{ env.GHC_VER }}-${{ hashFiles(format('stack-{0}.yaml.lock', env.GHC_VER)) }} - name: Set up pkg-config for the ICU library (macOS) if: ${{ runner.os == 'macOS' }} @@ -184,10 +184,13 @@ jobs: # NB: the ${ARGS} is necessary, otherwise stack installs another GHC... # Andreas, 2022-02-04, issue #5768: # To work around keyring problems, we update msys2-keyring before installing ICU. + # Andreas, 2022-05-15, pr #5909: the keyring problem was solved upstream by + # updating Stack-MSYS to 2022-05-03. - name: Install the icu library (Windows) if: ${{ runner.os == 'Windows' }} run: | - stack exec ${ARGS} -- pacman --noconfirm -Sy msys2-keyring + stack exec ${ARGS} -- pacman --noconfirm -Syuu + # stack exec ${ARGS} -- pacman --noconfirm -Sy msys2-keyring stack exec ${ARGS} -- pacman --noconfirm -S ${ICU} stack exec ${ARGS} -- pacman --noconfirm -S mingw-w64-x86_64-pkg-config diff --git a/test/Fail/Issue5920a.agda b/test/Fail/Issue5920a.agda new file mode 100644 index 00000000000..4c3c1aa24f1 --- /dev/null +++ b/test/Fail/Issue5920a.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --without-K #-} + +data D : Set where + @0 c : D + +data P (x : D) : Set where + +record R : Set where + field + f : P c diff --git a/test/Fail/Issue5920a.err b/test/Fail/Issue5920a.err new file mode 100644 index 00000000000..a26ef531edd --- /dev/null +++ b/test/Fail/Issue5920a.err @@ -0,0 +1,3 @@ +Issue5920a.agda:8,8-9 +(f : P c) → R is not usable at the required modality +when checking the definition of R diff --git a/test/Fail/Issue5920b.agda b/test/Fail/Issue5920b.agda new file mode 100644 index 00000000000..b2fc507b2a3 --- /dev/null +++ b/test/Fail/Issue5920b.agda @@ -0,0 +1,7 @@ +{-# OPTIONS --without-K #-} + +data D : Set where + @0 c : D + +data P : D → Set where + d : P c diff --git a/test/Fail/Issue5920b.err b/test/Fail/Issue5920b.err new file mode 100644 index 00000000000..c327a935149 --- /dev/null +++ b/test/Fail/Issue5920b.err @@ -0,0 +1,4 @@ +Issue5920b.agda:7,3-4 +P c is not usable at the required modality +when checking that the type P c of the constructor d fits in the +sort Set of the datatype. diff --git a/test/Fail/Issue5923.agda b/test/Fail/Issue5923.agda new file mode 100644 index 00000000000..c822bf0bd54 --- /dev/null +++ b/test/Fail/Issue5923.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --rewriting #-} + +open import Agda.Builtin.Equality +open import Agda.Builtin.Equality.Rewrite +open import Agda.Builtin.Unit + +postulate + A : Set + a : A + f : {X : Set} → X → A + g : {X : Set} → A → X + rew-fg : {X : Set} (a : A) → f (g {X} a) ≡ a +{-# REWRITE rew-fg #-} + +test : f tt ≡ a +test = refl diff --git a/test/Fail/Issue5923.err b/test/Fail/Issue5923.err new file mode 100644 index 00000000000..f1711fd1203 --- /dev/null +++ b/test/Fail/Issue5923.err @@ -0,0 +1,3 @@ +Issue5923.agda:16,8-12 +f tt != a of type A +when checking that the expression refl has type f tt ≡ a diff --git a/test/Succeed/Issue5923-OP.agda b/test/Succeed/Issue5923-OP.agda new file mode 100644 index 00000000000..57541db688a --- /dev/null +++ b/test/Succeed/Issue5923-OP.agda @@ -0,0 +1,38 @@ +{-# OPTIONS --type-in-type --rewriting #-} + +module _ where + +postulate + _≡_ : {A : Set} → A → A → Set + +{-# BUILTIN REWRITE _≡_ #-} + +record ⊤ : Set where + constructor [] +open ⊤ + +postulate + ID : (Δ : Set) (δ₀ δ₁ : Δ) → Set + ID⊤ : (δ₀ δ₁ : ⊤) → ID ⊤ δ₀ δ₁ ≡ ⊤ + Id : {Δ : Set} (A : Δ → Set) {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) (a₀ : A δ₀) (a₁ : A δ₁) → Set + ap : {Δ : Set} {A : Δ → Set} (f : (δ : Δ) → A δ) {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) → Id A δ₂ (f δ₀) (f δ₁) + AP : {Θ Δ : Set} (f : Θ → Δ) {t₀ t₁ : Θ} (t₂ : ID Θ t₀ t₁) → ID Δ (f t₀) (f t₁) + Id-AP : {Θ Δ : Set} (f : Θ → Δ) {t₀ t₁ : Θ} (t₂ : ID Θ t₀ t₁) (A : Δ → Set) (a₀ : A (f t₀)) (a₁ : A (f t₁)) → + Id A (AP f t₂) a₀ a₁ ≡ Id (λ w → A (f w)) t₂ a₀ a₁ + Copy : Set → Set + uncopy : {A : Set} → Copy A → A + +{-# REWRITE ID⊤ #-} +{-# REWRITE Id-AP #-} + +postulate + utr→ : {Δ : Set} (A : Δ → Set) {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) (a₁ a₁' : A δ₁) → Id {⊤} (λ _ → A δ₁) [] a₁ a₁' + IdU : {Δ : Set} {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) (A B : Set) → + Id {Δ} (λ _ → Set) δ₂ A B ≡ Copy ((b₀ : B) (b₁ : B) → Id {⊤} (λ _ → B) [] b₀ b₁) + +{-# REWRITE IdU #-} + +postulate + apU : {Δ : Set} (A : Δ → Set) {δ₀ δ₁ : Δ} (δ₂ : ID Δ δ₀ δ₁) → uncopy (ap A δ₂) ≡ utr→ A δ₂ + +{-# REWRITE apU #-} diff --git a/test/interaction/Issue5250/Issue5250.agda-lib-e b/test/interaction/Issue5250/Issue5250.agda-lib-e new file mode 100644 index 00000000000..00198968ccc --- /dev/null +++ b/test/interaction/Issue5250/Issue5250.agda-lib-e @@ -0,0 +1,2 @@ +flags: -Wall +include: . diff --git a/test/interaction/Issue737.out b/test/interaction/Issue737.out index ed4e6b833fe..dd384461984 100644 --- a/test/interaction/Issue737.out +++ b/test/interaction/Issue737.out @@ -16,7 +16,7 @@ (agda2-status-action "") (agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?4 : P s → W S P × X " nil) ((last . 1) . (agda2-goals-action '(4 1))) -(agda2-give-action 4 "(λ x → ?)") +(agda2-give-action 4 "λ x → ?") (agda2-status-action "") (agda2-info-action "*All Goals*" "?1 : (A × A) × (A → A) × (A → A) ?5 : W S P × X " nil) ((last . 1) . (agda2-goals-action '(5 1))) @@ -60,7 +60,7 @@ (agda2-status-action "") (agda2-info-action "*All Goals*" "?13 : A ?14 : A ?16 : A → A ?17 : A " nil) ((last . 1) . (agda2-goals-action '(13 14 17 16))) -(agda2-give-action 16 "(λ x → ?)") +(agda2-give-action 16 "λ x → ?") (agda2-status-action "") (agda2-info-action "*All Goals*" "?13 : A ?14 : A ?17 : A ?18 : A " nil) ((last . 1) . (agda2-goals-action '(13 14 17 18))) diff --git a/test/interaction/Issue810.out b/test/interaction/Issue810.out index 4552e9dabaf..fec115c0648 100644 --- a/test/interaction/Issue810.out +++ b/test/interaction/Issue810.out @@ -8,11 +8,11 @@ (agda2-status-action "") (agda2-info-action "*All Goals*" "?1 : Sg a ?2 : (a : A) → Sg a ?3 : A " nil) ((last . 1) . (agda2-goals-action '(3 1 2))) -(agda2-give-action 1 "sg ?") +(agda2-give-action 1 "sg _") (agda2-status-action "") -(agda2-info-action "*All Goals*" "?2 : (a : A) → Sg a ?3 : A ?4 : A " nil) -((last . 1) . (agda2-goals-action '(3 4 2))) +(agda2-info-action "*All Goals*" "?2 : (a : A) → Sg a ?3 : A " nil) +((last . 1) . (agda2-goals-action '(3 2))) (agda2-give-action 2 "λ a → ?") (agda2-status-action "") -(agda2-info-action "*All Goals*" "?3 : A ?4 : A ?5 : Sg a " nil) -((last . 1) . (agda2-goals-action '(3 4 5))) +(agda2-info-action "*All Goals*" "?3 : A ?4 : Sg a " nil) +((last . 1) . (agda2-goals-action '(3 4))) diff --git a/test/interaction/Long.out b/test/interaction/Long.out index b26f3ce61ef..89d3c3f4b77 100644 --- a/test/interaction/Long.out +++ b/test/interaction/Long.out @@ -35,7 +35,7 @@ (agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?4 : D′ z ?5 : Set ?6 : Maybe ?5 ?7 : Nat " nil) ((last . 1) . (agda2-goals-action '(7 1 2 3 4 5 6))) (agda2-status-action "") -(agda2-info-action "*Intro*" "Don't know which constructor to introduce of z or s" nil) +(agda2-intro-constructor-select 7 '(("z" . ("Nat" . "z")) ("s" . ("Nat → Nat" . "(s ?)")))) ((last . 1) . (agda2-goals-action '(7 1 2 3 4 5 6))) (agda2-give-action 4 "d") (agda2-status-action "") @@ -57,23 +57,24 @@ (agda2-info-action "*Module contents*" "Modules Names d : D z" nil) (agda2-status-action "") (agda2-info-action "*Module contents*" "Modules D Exp Maybe Nat Names D : Nat → Set D′ : Nat → Set Exp : Set Just : {@0 A : Set} → A → Maybe A Maybe : Set → Set Nat : Set Nothing : {@0 A : Set} → Maybe A d : D z eval : Exp → Maybe Nat foo : D ?2 s : Nat → Nat s′ : Nat → Nat throw : Exp val : Nat → Exp z : Nat" nil) +(agda2-give-action 3 "d") (agda2-status-action "") -(agda2-info-action "*Intro*" "No introduction forms found." nil) -((last . 1) . (agda2-goals-action '(7 1 2 3 5 6))) +(agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?5 : Set ?6 : Maybe ?5 ?7 : Nat " nil) +((last . 1) . (agda2-goals-action '(7 1 2 5 6))) (agda2-give-action 6 "Just ?") (agda2-status-action "") -(agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?5 : Set ?7 : Nat ?8 : ?5 " nil) -((last . 1) . (agda2-goals-action '(7 1 2 3 5 8))) +(agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?5 : Set ?7 : Nat ?8 : ?5 " nil) +((last . 1) . (agda2-goals-action '(7 1 2 5 8))) (agda2-status-action "") (agda2-info-action "*Normal Form*" "s′ z" nil) (agda2-status-action "") (agda2-info-action "*Normal Form*" "s z" nil) (agda2-give-action 8 "d") (agda2-status-action "") -(agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?5 : Set ?7 : Nat " nil) -((last . 1) . (agda2-goals-action '(7 1 2 3 5))) -((last . 2) . (agda2-solveAll-action '(5 "D z"))) -((last . 1) . (agda2-goals-action '(7 1 2 3 5))) +(agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?5 : Set ?7 : Nat " nil) +((last . 1) . (agda2-goals-action '(7 1 2 5))) +((last . 2) . (agda2-solveAll-action '(2 "z" 5 "D z"))) +((last . 1) . (agda2-goals-action '(7 1 2 5))) (agda2-info-action "*Error*" "1,1-4 Nat !=< Maybe Nat when checking that the inferred type of an application Nat matches the expected type Maybe Nat" nil) (agda2-highlight-load-and-delete-action) (agda2-status-action "") @@ -81,12 +82,12 @@ (agda2-info-action "*Normal Form*" "?1" nil) (agda2-give-action 1 "Nothing") (agda2-status-action "") -(agda2-info-action "*All Goals*" "?2 : Nat ?3 : D ?2 ?5 : Set ?7 : Nat " nil) -((last . 1) . (agda2-goals-action '(7 2 3 5))) +(agda2-info-action "*All Goals*" "?2 : Nat ?5 : Set ?7 : Nat " nil) +((last . 1) . (agda2-goals-action '(7 2 5))) (agda2-give-action 7 "n") (agda2-status-action "") -(agda2-info-action "*All Goals*" "?2 : Nat ?3 : D ?2 ?5 : Set " nil) -((last . 1) . (agda2-goals-action '(2 3 5))) +(agda2-info-action "*All Goals*" "?2 : Nat ?5 : Set " nil) +((last . 1) . (agda2-goals-action '(2 5))) (agda2-status-action "") (agda2-info-action "*Inferred Type*" "Maybe Nat" nil) (agda2-status-action "") @@ -99,7 +100,7 @@ (agda2-status-action "") (agda2-info-action "*Module contents*" "Modules Names d : D z" nil) (agda2-status-action "") -(agda2-info-action "*Module contents*" "Modules D Exp Maybe Nat Names D : Nat → Set D′ : Nat → Set Exp : Set Just : {@0 A : Set} → A → Maybe A Maybe : Set → Set Nat : Set Nothing : {@0 A : Set} → Maybe A bar : D′ z baz : Maybe (D z) d : D z eval : Exp → Maybe Nat foo : D ?2 s : Nat → Nat s′ : Nat → Nat throw : Exp val : Nat → Exp z : Nat" nil) +(agda2-info-action "*Module contents*" "Modules D Exp Maybe Nat Names D : Nat → Set D′ : Nat → Set Exp : Set Just : {@0 A : Set} → A → Maybe A Maybe : Set → Set Nat : Set Nothing : {@0 A : Set} → Maybe A bar : D′ z baz : Maybe (D z) d : D z eval : Exp → Maybe Nat foo : D z s : Nat → Nat s′ : Nat → Nat throw : Exp val : Nat → Exp z : Nat" nil) (agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear)