Agda 2.6.4.3 → 2.7.0

raw patch · 212 files changed

+9365/−8442 lines, 212 filesdep +pqueuedep −time-compatdep ~basedep ~containersdep ~parallelsetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: pqueue

Dependencies removed: time-compat

Dependency ranges changed: base, containers, parallel, time

API changes (from Hackage documentation)

Files

• Agda.cabal +46/−30
• CHANGELOG.md +436/−11
• LICENSE +12/−9
• README.md +1/−1
• Setup.hs +42/−15
• doc/release-notes/2.6.4.3.md +17/−0
• src/agda-mode/Main.hs +23/−8
• src/data/emacs-mode/agda-input.el +73/−14
• src/data/emacs-mode/agda2-mode-pkg.el +1/−1
• src/data/emacs-mode/agda2-mode.el +19/−16
• src/data/html/Agda.css +1/−0
• src/data/latex/agda.sty +1/−1
• src/data/lib/prim/Agda/Builtin/Reflection.agda +13/−2
• src/full/Agda/Auto/Auto.hs +0/−512
• src/full/Agda/Auto/CaseSplit.hs +0/−668
• src/full/Agda/Auto/Convert.hs +0/−788
• src/full/Agda/Auto/NarrowingSearch.hs +0/−670
• src/full/Agda/Auto/Options.hs +0/−122
• src/full/Agda/Auto/SearchControl.hs +0/−451
• src/full/Agda/Auto/Syntax.hs +0/−463
• src/full/Agda/Auto/Typecheck.hs +0/−846
• src/full/Agda/Benchmarking.hs +12/−1
• src/full/Agda/Compiler/Backend.hs +9/−71
• src/full/Agda/Compiler/Backend.hs-boot +2/−4
• src/full/Agda/Compiler/Backend/Base.hs +77/−0
• src/full/Agda/Compiler/Common.hs +5/−14
• src/full/Agda/Compiler/JS/Compiler.hs +3/−3
• src/full/Agda/Compiler/JS/Pretty.hs +1/−1
• src/full/Agda/Compiler/MAlonzo/Compiler.hs +9/−11
• src/full/Agda/Compiler/ToTreeless.hs +84/−53
• src/full/Agda/Interaction/Base.hs +8/−14
• src/full/Agda/Interaction/BasicOps.hs +26/−21
• src/full/Agda/Interaction/EmacsTop.hs +19/−18
• src/full/Agda/Interaction/FindFile.hs +3/−6
• src/full/Agda/Interaction/Highlighting/Dot/Backend.hs +1/−1
• src/full/Agda/Interaction/Highlighting/Dot/Base.hs +0/−1
• src/full/Agda/Interaction/Highlighting/FromAbstract.hs +16/−12
• src/full/Agda/Interaction/Highlighting/Generate.hs +17/−3
• src/full/Agda/Interaction/Highlighting/HTML/Backend.hs +1/−1
• src/full/Agda/Interaction/Highlighting/HTML/Base.hs +0/−1
• src/full/Agda/Interaction/Highlighting/LaTeX/Backend.hs +1/−1
• src/full/Agda/Interaction/Highlighting/Range.hs +1/−1
• src/full/Agda/Interaction/Imports.hs +93/−84
• src/full/Agda/Interaction/InteractionTop.hs +74/−70
• src/full/Agda/Interaction/JSONTop.hs +9/−1
• src/full/Agda/Interaction/Library.hs +10/−4
• src/full/Agda/Interaction/Library/Base.hs +29/−6
• src/full/Agda/Interaction/MakeCase.hs +3/−4
• src/full/Agda/Interaction/Options/Base.hs +82/−21
• src/full/Agda/Interaction/Options/Warnings.hs +96/−16
• src/full/Agda/Interaction/Output.hs +14/−0
• src/full/Agda/Interaction/Response.hs +19/−213
• src/full/Agda/Interaction/Response.hs-boot +0/−40
• src/full/Agda/Interaction/Response/Base.hs +178/−0
• src/full/Agda/Main.hs +12/−3
• src/full/Agda/Mimer/Mimer.hs +1705/−0
• src/full/Agda/Mimer/Options.hs +89/−0
• src/full/Agda/Syntax/Abstract.hs +50/−51
• src/full/Agda/Syntax/Abstract/Pattern.hs +49/−0
• src/full/Agda/Syntax/Abstract/PatternSynonyms.hs +6/−6
• src/full/Agda/Syntax/Abstract/UsedNames.hs +1/−0
• src/full/Agda/Syntax/Abstract/Views.hs +10/−4
• src/full/Agda/Syntax/Builtin.hs +8/−0
• src/full/Agda/Syntax/Common.hs +160/−30
• src/full/Agda/Syntax/Common/KeywordRange.hs +43/−0
• src/full/Agda/Syntax/Common/Pretty.hs +5/−1
• src/full/Agda/Syntax/Concrete.hs +102/−81
• src/full/Agda/Syntax/Concrete/Attribute.hs +5/−3
• src/full/Agda/Syntax/Concrete/Definitions.hs +107/−82
• src/full/Agda/Syntax/Concrete/Definitions/Errors.hs +54/−49
• src/full/Agda/Syntax/Concrete/Definitions/Monad.hs +1/−1
• src/full/Agda/Syntax/Concrete/Definitions/Types.hs +9/−9
• src/full/Agda/Syntax/Concrete/Fixity.hs +8/−4
• src/full/Agda/Syntax/Concrete/Generic.hs +3/−4
• src/full/Agda/Syntax/Concrete/Operators.hs +0/−1
• src/full/Agda/Syntax/Concrete/Operators/Parser.hs +0/−1
• src/full/Agda/Syntax/Concrete/Pretty.hs +53/−47
• src/full/Agda/Syntax/Info.hs +37/−6
• src/full/Agda/Syntax/Internal.hs +5/−5
• src/full/Agda/Syntax/Internal/Names.hs +5/−2
• src/full/Agda/Syntax/Parser.hs +5/−5
• src/full/Agda/Syntax/Parser/Helpers.hs +658/−0
• src/full/Agda/Syntax/Parser/LexActions.hs +4/−0
• src/full/Agda/Syntax/Parser/Lexer.x +5/−0
• src/full/Agda/Syntax/Parser/Monad.hs +2/−1
• src/full/Agda/Syntax/Parser/Parser.y +68/−691
• src/full/Agda/Syntax/Parser/Tokens.hs +2/−1
• src/full/Agda/Syntax/Scope/Base.hs +49/−12
• src/full/Agda/Syntax/Translation/AbstractToConcrete.hs +80/−51
• src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +227/−95
• src/full/Agda/Syntax/Translation/InternalToAbstract.hs +56/−25
• src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs +1/−1
• src/full/Agda/Termination/Monad.hs +6/−6
• src/full/Agda/Termination/RecCheck.hs +1/−2
• src/full/Agda/Termination/TermCheck.hs +5/−6
• src/full/Agda/TypeChecking/Abstract.hs +7/−4
• src/full/Agda/TypeChecking/CompiledClause/Match.hs +1/−1
• src/full/Agda/TypeChecking/Constraints.hs +17/−5
• src/full/Agda/TypeChecking/Conversion.hs +80/−21
• src/full/Agda/TypeChecking/Coverage.hs +6/−7
• src/full/Agda/TypeChecking/Coverage/Cubical.hs +12/−12
• src/full/Agda/TypeChecking/Datatypes.hs +7/−7
• src/full/Agda/TypeChecking/DeadCode.hs +61/−102
• src/full/Agda/TypeChecking/DiscrimTree.hs +429/−0
• src/full/Agda/TypeChecking/DiscrimTree/Types.hs +139/−0
• src/full/Agda/TypeChecking/Empty.hs +2/−2
• src/full/Agda/TypeChecking/Errors.hs +159/−81
• src/full/Agda/TypeChecking/Errors.hs-boot +3/−0
• src/full/Agda/TypeChecking/Forcing.hs +111/−35
• src/full/Agda/TypeChecking/Generalize.hs +35/−24
• src/full/Agda/TypeChecking/IApplyConfluence.hs +2/−2
• src/full/Agda/TypeChecking/Implicit.hs +16/−19
• src/full/Agda/TypeChecking/Injectivity.hs +2/−2
• src/full/Agda/TypeChecking/InstanceArguments.hs +585/−123
• src/full/Agda/TypeChecking/InstanceArguments.hs-boot +7/−0
• src/full/Agda/TypeChecking/Irrelevance.hs +9/−58
• src/full/Agda/TypeChecking/MetaVars.hs +31/−20
• src/full/Agda/TypeChecking/MetaVars/Mention.hs +1/−0
• src/full/Agda/TypeChecking/Modalities.hs +6/−5
• src/full/Agda/TypeChecking/Monad/Base.hs +416/−138
• src/full/Agda/TypeChecking/Monad/Base.hs-boot +1/−0
• src/full/Agda/TypeChecking/Monad/Base/Types.hs +17/−0
• src/full/Agda/TypeChecking/Monad/Builtin.hs +11/−2
• src/full/Agda/TypeChecking/Monad/Constraints.hs +48/−29
• src/full/Agda/TypeChecking/Monad/Context.hs +4/−3
• src/full/Agda/TypeChecking/Monad/Debug.hs +2/−3
• src/full/Agda/TypeChecking/Monad/MetaVars.hs +20/−10
• src/full/Agda/TypeChecking/Monad/Options.hs +36/−3
• src/full/Agda/TypeChecking/Monad/Pure.hs-boot +1/−1
• src/full/Agda/TypeChecking/Monad/Signature.hs +46/−18
• src/full/Agda/TypeChecking/Monad/Signature.hs-boot +1/−1
• src/full/Agda/TypeChecking/Monad/State.hs +15/−27
• src/full/Agda/TypeChecking/Names.hs +1/−1
• src/full/Agda/TypeChecking/Opacity.hs +2/−3
• src/full/Agda/TypeChecking/Patterns/Abstract.hs +8/−1
• src/full/Agda/TypeChecking/Patterns/Internal.hs +0/−2
• src/full/Agda/TypeChecking/Patterns/Match.hs +57/−36
• src/full/Agda/TypeChecking/Patterns/Match.hs-boot +3/−1
• src/full/Agda/TypeChecking/Positivity.hs +24/−31
• src/full/Agda/TypeChecking/Pretty.hs +51/−9
• src/full/Agda/TypeChecking/Pretty/Constraint.hs +28/−19
• src/full/Agda/TypeChecking/Pretty/Warning.hs +134/−9
• src/full/Agda/TypeChecking/Primitive/Cubical.hs +4/−4
• src/full/Agda/TypeChecking/Primitive/Cubical/Base.hs +3/−5
• src/full/Agda/TypeChecking/Primitive/Cubical/Id.hs +2/−2
• src/full/Agda/TypeChecking/ProjectionLike.hs +4/−2
• src/full/Agda/TypeChecking/Quote.hs +11/−6
• src/full/Agda/TypeChecking/ReconstructParameters.hs +4/−3
• src/full/Agda/TypeChecking/RecordPatterns.hs +0/−36
• src/full/Agda/TypeChecking/Records.hs +115/−96
• src/full/Agda/TypeChecking/Records.hs-boot +6/−5
• src/full/Agda/TypeChecking/Reduce.hs +41/−48
• src/full/Agda/TypeChecking/Reduce/Fast.hs +2/−6
• src/full/Agda/TypeChecking/Rewriting.hs +62/−44
• src/full/Agda/TypeChecking/Rewriting/Confluence.hs +4/−9
• src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs +36/−24
• src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs +1/−1
• src/full/Agda/TypeChecking/Rules/Application.hs +17/−14
• src/full/Agda/TypeChecking/Rules/Builtin.hs +6/−4
• src/full/Agda/TypeChecking/Rules/Data.hs +16/−13
• src/full/Agda/TypeChecking/Rules/Decl.hs +54/−31
• src/full/Agda/TypeChecking/Rules/Def.hs +52/−30
• src/full/Agda/TypeChecking/Rules/LHS.hs +53/−51
• src/full/Agda/TypeChecking/Rules/LHS/Unify.hs +4/−4
• src/full/Agda/TypeChecking/Rules/LHS/Unify/LeftInverse.hs +3/−5
• src/full/Agda/TypeChecking/Rules/Record.hs +21/−13
• src/full/Agda/TypeChecking/Rules/Term.hs +64/−55
• src/full/Agda/TypeChecking/Serialise.hs +1/−1
• src/full/Agda/TypeChecking/Serialise/Instances/Abstract.hs +14/−12
• src/full/Agda/TypeChecking/Serialise/Instances/Common.hs +48/−0
• src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs +144/−13
• src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs +43/−14
• src/full/Agda/TypeChecking/SizedTypes.hs +1/−2
• src/full/Agda/TypeChecking/SizedTypes/Pretty.hs +50/−0
• src/full/Agda/TypeChecking/SizedTypes/Solve.hs +30/−116
• src/full/Agda/TypeChecking/SizedTypes/Syntax.hs +84/−18
• src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs +19/−2
• src/full/Agda/TypeChecking/Substitute.hs +4/−0
• src/full/Agda/TypeChecking/Substitute/Class.hs +22/−22
• src/full/Agda/TypeChecking/Telescope.hs +34/−78
• src/full/Agda/TypeChecking/Unquote.hs +142/−106
• src/full/Agda/TypeChecking/Warnings.hs +11/−14
• src/full/Agda/Utils/BiMap.hs +1/−1
• src/full/Agda/Utils/Function.hs +6/−1
• src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs +17/−7
• src/full/Agda/Utils/IArray.hs +36/−0
• src/full/Agda/Utils/IO.hs +17/−1
• src/full/Agda/Utils/IO/UTF8.hs +5/−0
• src/full/Agda/Utils/Impossible.hs +10/−2
• src/full/Agda/Utils/IndexedList.hs +0/−1
• src/full/Agda/Utils/Lens.hs +3/−0
• src/full/Agda/Utils/List.hs +15/−0
• src/full/Agda/Utils/List1.hs +10/−2
• src/full/Agda/Utils/Monad.hs +19/−4
• src/full/Agda/Utils/Null.hs +7/−1
• src/full/Agda/Utils/ProfileOptions.hs +1/−0
• src/full/Agda/Utils/SmallSet.hs +5/−1
• src/full/Agda/Utils/String.hs +4/−0
• src/full/Agda/Utils/TypeLevel.hs +0/−1
• src/full/Agda/Utils/TypeLits.hs +0/−1
• src/full/Agda/Utils/Unsafe.hs +1/−1
• stack-8.10.7.yaml +1/−0
• stack-8.6.5.yaml +0/−15
• stack-8.8.4.yaml +1/−0
• stack-9.0.2.yaml +1/−0
• stack-9.10.1.yaml +24/−0
• stack-9.2.8.yaml +3/−0
• stack-9.4.8.yaml +3/−0
• stack-9.6.4.yaml +0/−3
• stack-9.6.6.yaml +3/−0
• stack-9.8.1.yaml +0/−3
• stack-9.8.2.yaml +3/−0

@@ -1,6 +1,6 @@ cabal-version:   2.4 name:            Agda-version:         2.6.4.3+version:         2.7.0 build-type:      Custom license:         MIT license-file:    LICENSE@@ -35,8 +35,9 @@     packages.  tested-with:-    GHC == 9.8.1-    GHC == 9.6.4+    GHC == 9.10.1+    GHC == 9.8.2+    GHC == 9.6.6     GHC == 9.4.8     GHC == 9.2.8     GHC == 9.0.2@@ -48,6 +49,7 @@     CHANGELOG.md     README.md     doc/user-manual/agda.svg+    doc/release-notes/2.6.4.3.md     doc/release-notes/2.6.4.2.md     doc/release-notes/2.6.4.1.md     doc/release-notes/2.6.4.md@@ -90,14 +92,14 @@     doc/release-notes/2.2.0.md  extra-source-files:-    stack-9.8.1.yaml-    stack-9.6.4.yaml+    stack-9.10.1.yaml+    stack-9.8.2.yaml+    stack-9.6.6.yaml     stack-9.4.8.yaml     stack-9.2.8.yaml     stack-9.0.2.yaml     stack-8.10.7.yaml     stack-8.8.4.yaml-    stack-8.6.5.yaml  data-dir:     src/data@@ -158,7 +160,7 @@ source-repository this   type:     git   location: https://github.com/agda/agda.git-  tag:      v2.6.4.3+  tag:      v2.7.0  -- Build flags ---------------------------------------------------------------------------@@ -201,10 +203,10 @@  custom-setup   setup-depends:-    , base      >= 4.12.0.0 && < 4.20-    , Cabal     >= 2.4.0.1  && < 3.11+    , base      >= 4.12.0.0 && < 4.21+    , Cabal     >= 2.4.0.1  && < 3.13     , directory >= 1.3.3.0  && < 1.4-    , filepath  >= 1.4.2.1  && < 1.5+    , filepath  >= 1.4.2.1  && < 1.6     , process   >= 1.6.3.0  && < 1.7  -- Common stanzas@@ -243,7 +245,6 @@       -Wwarn=overflowed-literals       -Wwarn=overlapping-patterns --      -Wwarn=redundant-constraints-      -Wwarn=semigroup       -Wwarn=simplifiable-class-constraints       -Wwarn=star-binder       -Wwarn=star-is-type@@ -268,6 +269,11 @@       -Wno-incomplete-patterns       -Wno-overlapping-patterns +  if impl(ghc < 9.10)+    ghc-options:+      -Wwarn=semigroup+        -- The semigroup warning is deprecated in GHC 9.10+   if impl(ghc >= 8.8)     ghc-options:       -Wwarn=missed-extra-shared-lib@@ -301,9 +307,13 @@    if impl(ghc >= 9.4)     ghc-options:-      -Wwarn=forall-identifier       -Wwarn=type-equality-out-of-scope +  if impl(ghc >= 9.4 && < 9.10)+    ghc-options:+      -Wwarn=forall-identifier+        -- The forall-identifier warning is deprecated in GHC 9.10+   default-language: Haskell2010    -- NOTE: If adding or removing default extensions, also change:@@ -326,6 +336,7 @@       FlexibleContexts       FlexibleInstances       FunctionalDependencies+      GADTs       GeneralizedNewtypeDeriving       InstanceSigs       LambdaCase@@ -342,6 +353,7 @@       TypeFamilies       TypeOperators       TypeSynonymInstances+      ViewPatterns    other-extensions:       CPP@@ -402,7 +414,7 @@     , ansi-terminal        >= 0.9       && < 1.2     , array                >= 0.5.2.0   && < 0.6     , async                >= 2.2       && < 2.3-    , base                 >= 4.12.0.0  && < 4.20+    , base                 >= 4.12.0.0  && < 4.21     , binary               >= 0.8.6.0   && < 0.9     , blaze-html           >= 0.8       && < 0.10     , boxes                >= 0.1.3     && < 0.2@@ -417,13 +429,13 @@     , equivalence          >= 0.3.2     && < 0.5     -- exceptions-0.8 instead of 0.10 because of stack     , exceptions           >= 0.8       && < 0.11-    , filepath             >= 1.4.2.1   && < 1.5+    , filepath             >= 1.4.2.1   && < 1.6     , ghc-compact          == 0.1.*     , gitrev               >= 1.3.1     && < 2     -- hashable 1.2.0.10 makes library-test 10x     -- slower. The issue was fixed in hashable 1.2.1.0.     -- https://github.com/tibbe/hashable/issues/57.-    , hashable             >= 1.2.1.0   && < 1.5+    , hashable             >= 1.2.1.0   && < 1.6     , haskeline            >= 0.7.4.3   && < 0.9     -- monad-control-1.0.1.0 is the first to contain liftThrough     , monad-control        >= 1.0.1.0   && < 1.1@@ -431,6 +443,7 @@     , murmur-hash          >= 0.1       && < 0.2     , parallel             >= 3.2.2.0   && < 3.3     , peano                >= 0.1.0.1   && < 0.2+    , pqueue               >= 1.4.1.2   && < 1.6     , pretty               >= 1.1.3.3   && < 1.2     , process              >= 1.6.3.0   && < 1.7     , regex-tdfa           >= 1.3.1.0   && < 1.4@@ -439,9 +452,7 @@     , STMonadTrans         >= 0.4.3     && < 0.5     , strict               >= 0.4.0.1   && < 0.6     , text                 >= 1.2.3.1   && < 2.2-    , time                 >= 1.8.0.2   && < 1.13-    , time-compat          >= 1.9.2     && < 1.10-        -- time-compat adds needed functionality missing in time < 1.9+    , time                 >= 1.9.2     && < 1.15     , transformers         >= 0.5.5.0   && < 0.7     , unordered-containers >= 0.2.9.0   && < 0.3         -- unordered-containers < 0.2.9 need base < 4.11@@ -459,16 +470,9 @@         -- happy-1.19.8 is packaged with Ubuntu 18.04    exposed-modules:-      Agda.Auto.Auto-      Agda.Auto.Options-      Agda.Auto.CaseSplit-      Agda.Auto.Convert-      Agda.Auto.NarrowingSearch-      Agda.Auto.SearchControl-      Agda.Auto.Syntax-      Agda.Auto.Typecheck       Agda.Benchmarking       Agda.Compiler.Backend+      Agda.Compiler.Backend.Base       Agda.Compiler.Builtin       Agda.Compiler.CallCompiler       Agda.Compiler.Common@@ -525,7 +529,9 @@       Agda.Interaction.Highlighting.LaTeX       Agda.Interaction.Imports       Agda.Interaction.InteractionTop+      Agda.Interaction.Output       Agda.Interaction.Response+      Agda.Interaction.Response.Base       Agda.Interaction.MakeCase       Agda.Interaction.Monad       Agda.Interaction.Library@@ -536,6 +542,8 @@       Agda.Interaction.Options.Lenses       Agda.Interaction.Options.Warnings       Agda.Main+      Agda.Mimer.Mimer+      Agda.Mimer.Options       Agda.Syntax.Abstract.Name       Agda.Syntax.Abstract.Pattern       Agda.Syntax.Abstract.PatternSynonyms@@ -545,8 +553,9 @@       Agda.Syntax.Abstract       Agda.Syntax.Builtin       Agda.Syntax.Common-      Agda.Syntax.Common.Pretty       Agda.Syntax.Common.Aspect+      Agda.Syntax.Common.KeywordRange+      Agda.Syntax.Common.Pretty       Agda.Syntax.Common.Pretty.ANSI       Agda.Syntax.Concrete.Attribute       Agda.Syntax.Concrete.Definitions@@ -581,6 +590,7 @@       Agda.Syntax.Notation       Agda.Syntax.Parser.Alex       Agda.Syntax.Parser.Comments+      Agda.Syntax.Parser.Helpers       Agda.Syntax.Parser.Layout       Agda.Syntax.Parser.LexActions       Agda.Syntax.Parser.Lexer@@ -631,6 +641,8 @@       Agda.TypeChecking.DeadCode       Agda.TypeChecking.DisplayForm       Agda.TypeChecking.DropArgs+      Agda.TypeChecking.DiscrimTree+      Agda.TypeChecking.DiscrimTree.Types       Agda.TypeChecking.Empty       Agda.TypeChecking.EtaContract       Agda.TypeChecking.Errors@@ -656,6 +668,7 @@       Agda.TypeChecking.MetaVars.Occurs       Agda.TypeChecking.Modalities       Agda.TypeChecking.Monad.Base+      Agda.TypeChecking.Monad.Base.Types       Agda.TypeChecking.Monad.Base.Warning       Agda.TypeChecking.Monad.Benchmark       Agda.TypeChecking.Monad.Builtin@@ -736,6 +749,7 @@       Agda.TypeChecking.Serialise.Instances.Internal       Agda.TypeChecking.Serialise.Instances.Errors       Agda.TypeChecking.SizedTypes+      Agda.TypeChecking.SizedTypes.Pretty       Agda.TypeChecking.SizedTypes.Solve       Agda.TypeChecking.SizedTypes.Syntax       Agda.TypeChecking.SizedTypes.Utils@@ -775,6 +789,7 @@       Agda.Utils.Hash       Agda.Utils.HashTable       Agda.Utils.Haskell.Syntax+      Agda.Utils.IArray       Agda.Utils.Impossible       Agda.Utils.IndexedList       Agda.Utils.IntSet.Infinite@@ -817,6 +832,7 @@       Agda.Utils.Tuple       Agda.Utils.TypeLevel       Agda.Utils.TypeLits+      Agda.Utils.Unsafe       Agda.Utils.Update       Agda.Utils.VarSet       Agda.Utils.Warshall@@ -830,6 +846,7 @@    other-modules:       Paths_Agda+      -- Need not export submodules if parent module reexports them.       Agda.Interaction.Highlighting.Dot.Backend       Agda.Interaction.Highlighting.Dot.Base       Agda.Interaction.Highlighting.HTML.Backend@@ -840,7 +857,6 @@       Agda.Interaction.Options.HasOptions       Agda.Utils.CallStack.Base       Agda.Utils.CallStack.Pretty-      Agda.Utils.Unsafe  -- Agda binary ---------------------------------------------------------------------------@@ -877,8 +893,8 @@   autogen-modules:  Paths_Agda   other-modules:    Paths_Agda   build-depends:-    , base      >= 4.12.0.0 && < 4.20+    , base      >= 4.12.0.0 && < 4.21     , directory >= 1.3.3.0  && < 1.4-    , filepath  >= 1.4.2.1  && < 1.5+    , filepath  >= 1.4.2.1  && < 1.6     , process   >= 1.6.3.0  && < 1.7   default-language: Haskell2010

@@ -1,17 +1,442 @@-Release notes for Agda version 2.6.4.3-======================================+Release notes for Agda version 2.7.0+==================================== -This release fixes a regression in 2.6.4.3 and one in 2.6.4.-It aims to be API-compatible with 2.6.4.1 and 2.6.4.2.+Highlights+---------- -Agda 2.6.4.3 supports GHC versions 8.6.5 to 9.8.1.+* Mimer, a re-implementation of the "auto" term synthesizer, replaces Agsy. -Closed issues--------------+* New syntax `using x ← e` to bind values on the left-hand-side of a function clause. -For 2.6.4.3, the following issues were-[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.4.3+is%3Aclosed)+* Instance search is more performant thanks to a new indexing structure.+  Additionally, users can now control how instances should be selected+  in the case multiple candidates exist.++* User-facing options `--exact-split`, `--keep-pattern-variables`, and `--postfix-projections`+  are now on by default.++Installation+------------++* Agda versioning scheme switches to the [Haskell Package Versioning Policy](https://pvp.haskell.org/)+  so Agda can be more reliably used as a library.+  Major releases will now bump the second number in the version tuple: 2.7.0, 2.8.0, 2.9.0, ...++* When the creation of the Agda library interface files fails during installation,+  a warning is emitted rather than aborting installation.+  The absence of these interface files is not a problem if the Agda installation+  resides in user space; they will be created on the fly then.+  Yet for system-wide installations in root space or packaging,+  the interface files should be created.+  This can be achieved by a manual invocation of Agda on the library source files+  (i.e., primitive and builtin modules `Agda.*`).+  (See [Issue #7401](https://github.com/agda/agda/issues/7401) and [PR #7404](https://github.com/agda/agda/pull/7404).)++* Agda supports GHC versions 8.6.5 to 9.10.1.++Pragmas and options+-------------------++* [**Breaking**] The option `--overlapping-instances`, which allows+  backtracking during instance search, has been renamed to+  `--backtracking-instance-search`.++* These options are now on by default:++  * `--exact-split`: Warn about clauses that are not definitional equalities.+  * `--keep-pattern-variables`: Do not introduce dot patterns in interactive splitting.+  * `--postfix-projections`: Print projections and projection patterns in postfix.+  * `--save-metas`: Try to not unfold metavariable solutions in interface files.++  To revert to the old behavior, use options `--no-...`.++* Option `--rewriting` is now considered infective.+  This means that if a module has this flag enabled,+  then all modules importing it must also have that flag enabled.++* New warnings:++  * `CoinductiveEtaRecord` if a record is declared both `coinductive` and having `eta-equality`.+    Used to be a hard error; now Agda continues, ignoring `eta-equality`.++  * `ConflictingPragmaOptions` if giving both `--this` and `--that`+    when `--this` implies `--no-that` (and analogous for `--no-this` implies+    `--that`, etc).++  * `ConstructorDoesNotFitInData` when a constructor parameter+    is too big (in the sense of universe level) for the target data type of the constructor.+    Error warning, used to be a hard error.++  * `DuplicateRecordDirectives` if e.g. a `record` is declared both `inductive` and `coinductive`,+    or declared `inductive` twice.++  * `UselessMacro` when a `macro` block does not contain any function definitions.++  * `WarningProblem` when trying to switch an unknown or non-benign warning with the `-W` option.+    Used to be a hard error.++* Rejected rewrite rules no longer cause a hard error but instead cause+  an error warning. The following warnings were added to document the+  various reasons for rejection:+  * `RewriteLHSNotDefinitionOrConstructor`+  * `RewriteVariablesNotBoundByLHS`+  * `RewriteVariablesBoundMoreThanOnce`+  * `RewriteLHSReduces`+  * `RewriteHeadSymbolIsProjection`+  * `RewriteHeadSymbolIsProjectionLikeFunction`+  * `RewriteHeadSymbolIsTypeConstructor`+  * `RewriteHeadSymbolContainsMetas`+  * `RewriteConstructorParametersNotGeneral`+  * `RewriteContainsUnsolvedMetaVariables`+  * `RewriteBlockedOnProblems`+  * `RewriteRequiresDefinitions`+  * `RewriteDoesNotTargetRewriteRelation`+  * `RewriteBeforeFunctionDefinition`+  * `RewriteBeforeMutualFunctionDefinition`++### Lossy unification++* [New option `--require-unique-meta-solutions`](https://agda.readthedocs.io/en/v2.7.0/tools/command-line-options.html#cmdoption-require-unique-meta-solutions)+  (turned on by default).+  Disabling it with `--no-require-unique-meta-solutions` allows the type checker+  to take advantage of `INJECTIVE_FOR_INFERENCE` pragmas (see below).+  The `--lossy-unification` flag implies `--no-require-unique-meta-solutions`.++* [New pragma `INJECTIVE_FOR_INFERENCE`](https://agda.readthedocs.io/en/v2.7.0/pragmas.html#injective-for-inference-pragma)+  which treats functions as injective for inferring implicit arguments if+  `--no-require-unique-meta-solutions` is given. The `--no-require-unique-meta-solutions` flag needs to be given in the+  file where the function is used, and not necessarily in the file where it is defined.+  For example:+  ```agda+  postulate+    reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'++  []≡[] : [] ≡ []+  []≡[] = reverse-≡ (refl {x = reverse []})+  ```+  does not work since Agda won't solve `l` and `l'` for `[]`, even though it knows `reverse l = reverse []`.+  If `reverse` is marked as injective with `{-# INJECTIVE_FOR_INFERENCE reverse #-}` this example will work.++Syntax+------++Additions to the Agda syntax.++* [Left-hand side let](https://agda.readthedocs.io/en/v2.7.0/with-abstraction.html#left-hand-side-let-bindings):+  `using x ← e`+  ([PR #7078](https://github.com/agda/agda/pull/7078))++  This new construct can be use in left-hand sides together with `with` and+  `rewrite` to give names to subexpressions. It is the left-hand side+  counterpart of a `let`-binding and supports the same limited form of pattern+  matching on eta-expandable record values.++  It can be quite useful when you have a function doing a series of nested+  `with`s that share some expressions. Something like++  ```agda+  fun : A → B+  fun x using z ← e with foo z+  ... | p with bar z+  ...   | q = r+  ```++  Here the expression `e` doesn't have to be repeated in the two `with`-expressions.++  As in a `with`, multiple bindings can be separated by a `|`, and variables to+  the left are in scope in bindings to the right.++* Pattern synonyms can now expose existing instance arguments+  ([PR 7173](https://github.com/agda/agda/pull/7173)).+  Example:+  ```agda+  data D : Set where+    c : {{D}} → D++  pattern p {{d}} = c {{d}}+  ```+  This allows us to explicitly bind these argument in a pattern match+  and supply them explicitly when using the pattern synonym in an expression.+  ```agda+  f : D → D+  f (p {{d = x}}) = p {{d = x}}+  ```++  We cannot create new instance arguments this way, though.+  The following is rejected:+  ```agda+  data D : Set where+    c : D → D++  pattern p {{d}} = c d+  ```++Language+--------++Changes to type checker and other components defining the Agda language.++* Agda now uses *discrimination trees* to store and look up instance+  definitions, rather than linearly searching through all instances for+  a given "class" ([PR #7109](https://github.com/agda/agda/pull/7109)).++  This is a purely internal change, and should not result in any change+  to which programs are accepted or rejected. However, it significantly+  improves the performance of instance search, especially for the case+  of a "type class" indexed by a single type argument. The new lookup+  procedure should never be slower than the previous implementation.++Reflection+----------++Changes to the meta-programming facilities.++* [**Breaking**] Erased constructors are now supported in reflection machinery.+  Quantity argument was added to `data-cons`. For erased constructors this+  argument has a value of `quantity-0`, otherwise it's `quantity-ω`.+  `defineData` now requires setting quantity for each constructor.++* Add new primitive to run instance search from reflection code:++  ```agda+    -- Try to solve open instance constraints. When wrapped in `noConstraints`,+    -- fails if there are unsolved instance constraints left over that originate+    -- from the current macro invokation. Outside constraints are still attempted,+    -- but failure to solve them are ignored by `noConstraints`.+    solveInstanceConstraints : TC ⊤+  ```++* A new reflection primitive `workOnTypes : TC A → TC A` was added to+  `Agda.Builtin.Reflection`. This runs the given computation at the type level,+  which enables the use of erased things. In particular, this is needed when+  working with (dependent) function types with erased arguments. For example,+  one can get the type of the tuple constructor `_,_` (which now takes its type+  parameters as erased arguments, see above) and unify it with the current goal+  as follows:+  ```agda+  macro+    testM : Term → TC ⊤+    testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t))++  typeOfComma = testM+  ```++Interaction and emacs mode+--------------------------++* [**Breaking**] [The Auto command](https://agda.readthedocs.io/en/v2.7.0/tools/auto.html)+  _Agsy_ has been replaced by an entirely new implementation _Mimer_+  ([PR #6410](https://github.com/agda/agda/pull/6410)).+  This fixes problems where Auto would fail in the presence of language features+  it did not know about, such as copatterns or anything cubical.++  The reimplementation does not support case splitting (`-c`), disproving+  (`-d`) or refining (`-r`).++* The Agda input method for Emacs has been extended by several character bindings.+  The list of changes can be obtained with a git diff on the sources:+  ```+  git diff v2.6.4.3 v2.7.0 -- src/data/emacs-mode/agda-input.el+  ```++API+---++Highlighting some changes to Agda as a library.++* New module `Agda.Syntax.Common.KeywordRange` providing type `KwRange` isomorphic to `Range`+  to indicate source positions that just span keywords ([PR #7162](https://github.com/agda/agda/pull/7162)).+  The motivation for `KwRange` is to distinguish such ranges from ranges for whole subtrees,+  e.g. in data type `Agda.Syntax.Concrete.Declaration`.++  API:+  ```haskell+  module Agda.Syntax.Common.KeywordRange where++  type KwRange++  -- From Range to KwRange+  kwRange :: HasRange a => a -> KwRange++  -- From KwRange to Range+  instance HasRange KwRange where+    getRange :: KwRange -> Range+  ```++* New hook in ``Agda.Compiler.ToTreeless`` to enable custom pipelines in compiler backends+  ([PR #7273](https://github.com/agda/agda/pull/7273)).+++List of closed issues+---------------------++For 2.7.0, the following issues were+[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.7.0+is%3Aclosed) (see [bug tracker](https://github.com/agda/agda/issues)): -- [Issue #7148](https://github.com/agda/agda/issues/7148): Regression in 2.6.4.2 concerning `with`-- [Issue #7150](https://github.com/agda/agda/issues/7150): Regression in 2.6.4 in `rewrite` with instances+- [Issue #2492](https://github.com/agda/agda/issues/2492): Limit the size of terms agsy is allowed to insert+- [Issue #2853](https://github.com/agda/agda/issues/2853): Auto does not work well with record types+- [Issue #4594](https://github.com/agda/agda/issues/4594): Improve the blocking primitive+- [Issue #4777](https://github.com/agda/agda/issues/4777): Interaction between tactics and instance search+- [Issue #6101](https://github.com/agda/agda/issues/6101): Agsy gives up when no HIT is present+- [Issue #6124](https://github.com/agda/agda/issues/6124): Reflection: cannot reduce type because variable is erased+- [Issue #6181](https://github.com/agda/agda/issues/6181): Agda incorrectly reports type error when an identity function is not properly hidden from the termination checker+- [Issue #6270](https://github.com/agda/agda/issues/6270): Irrelevance in the type of a record module definition+- [Issue #6292](https://github.com/agda/agda/issues/6292): Document interaction between reflection and erasure+- [Issue #6335](https://github.com/agda/agda/issues/6335): Error message for non-canonical value when using Show instances is confusing+- [Issue #6361](https://github.com/agda/agda/issues/6361): Agsy ignores --postfix-projections+- [Issue #6406](https://github.com/agda/agda/issues/6406): Subject reduction problem related to projections with non-erased parameter arguments+- [Issue #6433](https://github.com/agda/agda/issues/6433): Add unicode character BALLOT X as \crossmark to Agda input mode+- [Issue #6509](https://github.com/agda/agda/issues/6509): Agda seems to be very slow at typechecking records with many fields+- [Issue #6584](https://github.com/agda/agda/issues/6584): Case splitting on record renames top-level function+- [Issue #6643](https://github.com/agda/agda/issues/6643): Rewrite rules are allowed in implicit mutual blocks+- [Issue #6663](https://github.com/agda/agda/issues/6663): Function arguments are nonvariant more often than they should be+- [Issue #6667](https://github.com/agda/agda/issues/6667): An internal error occurrs when (mis)using syntax declarations+- [Issue #6744](https://github.com/agda/agda/issues/6744): Alias in constructor index foils the forcing analysis+- [Issue #6768](https://github.com/agda/agda/issues/6768): auto: not implemented HITs error on non-cubical code+- [Issue #6783](https://github.com/agda/agda/issues/6783): `@tactic` does not kick in for lambdas+- [Issue #6806](https://github.com/agda/agda/issues/6806): Remove `GenericWarning`+- [Issue #6841](https://github.com/agda/agda/issues/6841): Uncaught pattern violation when using `with...in...` instead of old-school inspect+- [Issue #6866](https://github.com/agda/agda/issues/6866): User Manual: Make Installation as Easy as Possible+- [Issue #6867](https://github.com/agda/agda/issues/6867): Agda rejects identity function on indexed datatype with erased index+- [Issue #6919](https://github.com/agda/agda/issues/6919): improving formatting of warnings/errors+- [Issue #6943](https://github.com/agda/agda/issues/6943): Making `--exact-split` and `--postfix-projections` default?+- [Issue #6945](https://github.com/agda/agda/issues/6945): Missing warning for non-empty but effectless `private` blocks+- [Issue #6976](https://github.com/agda/agda/issues/6976): Unexpected failure of instance resolution+- [Issue #7017](https://github.com/agda/agda/issues/7017): Document instance projections+- [Issue #7058](https://github.com/agda/agda/issues/7058): Unclear specification and correctness of TypeChecking/DeadCode+- [Issue #7090](https://github.com/agda/agda/issues/7090): REWRITE rule with confluence, inconsistencies with documentation and error messages+- [Issue #7123](https://github.com/agda/agda/issues/7123): Citation.cff+- [Issue #7136](https://github.com/agda/agda/issues/7136): Pattern synonyms with named arguments can be defined but not used+- [Issue #7146](https://github.com/agda/agda/issues/7146): Misprinted domain-free parameters with cohesion attribute+- [Issue #7158](https://github.com/agda/agda/issues/7158): Non-sensical error since 2.5.4 when applying a non-function+- [Issue #7167](https://github.com/agda/agda/issues/7167): Underapplied pattern synonyms expand to lambdas with wrong hiding in expressions+- [Issue #7170](https://github.com/agda/agda/issues/7170): Confusing error "Unused variable in pattern synonym"+- [Issue #7176](https://github.com/agda/agda/issues/7176): Instanceness is lost when expanding absurd pattern in pattern synonym expression+- [Issue #7177](https://github.com/agda/agda/issues/7177): No scope info for underscores inserted by pattern synonym expansion+- [Issue #7181](https://github.com/agda/agda/issues/7181): Forcing translation prevents reduction within function definition+- [Issue #7182](https://github.com/agda/agda/issues/7182): `getDefinition` gives wrong constructor for record from applied parameterised module+- [Issue #7187](https://github.com/agda/agda/issues/7187): Sort metas produce ill-typed reflected terms when quoted+- [Issue #7191](https://github.com/agda/agda/issues/7191): `show` does not respect `abstract`/`opaque` when normalising a term in a hole+- [Issue #7192](https://github.com/agda/agda/issues/7192): GHC 9.10+- [Issue #7193](https://github.com/agda/agda/issues/7193): Agda always has irrelevant projections+- [Issue #7196](https://github.com/agda/agda/issues/7196): Regression when giving instances with visible arguments+- [Issue #7202](https://github.com/agda/agda/issues/7202): `ModuleDoesntExport` has imprecise deadcode highlighting+- [Issue #7208](https://github.com/agda/agda/issues/7208): Importing module with wrong namespace causes internal error instead of user-friendly error.+- [Issue #7218](https://github.com/agda/agda/issues/7218): Internal error in opaque block when case splitting when just given extended lambda+- [Issue #7219](https://github.com/agda/agda/issues/7219): Only warn about unknown warnings, don't fail hard+- [Issue #7227](https://github.com/agda/agda/issues/7227): Save-metas causes OOM during macro execution+- [Issue #7236](https://github.com/agda/agda/issues/7236): Expected a hidden argument, but found a visible argument in with-abstraction when using REWRITE+- [Issue #7262](https://github.com/agda/agda/issues/7262): Error "This clause has target type ... which is not usable" highlights pattern instead of clause+- [Issue #7266](https://github.com/agda/agda/issues/7266): Internal error at Agda/TypeChecking/Substitute.hs:140:33+- [Issue #7286](https://github.com/agda/agda/issues/7286): Hard error on `instance` definition with unsolved type+- [Issue #7301](https://github.com/agda/agda/issues/7301): Agda >=2.6.3 hangs on conflicting record directives+- [Issue #7318](https://github.com/agda/agda/issues/7318): `--postfix-projections` do not make use of mixfix syntax+- [Issue #7326](https://github.com/agda/agda/issues/7326): Internal error on pattern lambda with no clauses+- [Issue #7329](https://github.com/agda/agda/issues/7329): wrong type for unnamed record constructor+- [Issue #7331](https://github.com/agda/agda/issues/7331): Search for project root crashes when (parent) directory lacks permissions+- [Issue #7332](https://github.com/agda/agda/issues/7332): quoteTerm loops on dependent copattern lambda+- [Issue #7337](https://github.com/agda/agda/issues/7337): Caching loses reflection-generated pragmas+- [Issue #7346](https://github.com/agda/agda/issues/7346): Proof of ⊥ using HIT-indexed type+- [Issue #7380](https://github.com/agda/agda/issues/7380): MAlonzo bug: `unreachable code reached`+- [Issue #7382](https://github.com/agda/agda/issues/7382): Agda 2.7.0-rc1 crashes when run twice, probably serialization issue+- [Issue #7401](https://github.com/agda/agda/issues/7401): Cabal 3.12.1.0 install failure for lib:Agda - dist/build/agda/agda does not exist++These (relevant) pull requests were merged for 2.7.0:++- [PR #6410](https://github.com/agda/agda/issues/6410): Mimer: a drop-in replacement for Agsy+- [PR #6569](https://github.com/agda/agda/issues/6569): Do final checks before freezing metas+- [PR #6570](https://github.com/agda/agda/issues/6570): Coerce `unquote` applications+- [PR #6640](https://github.com/agda/agda/issues/6640): Add `INJECTIVE_FOR_INFERENCE` pragma+- [PR #6674](https://github.com/agda/agda/issues/6674): Testcase for fixed #6542+- [PR #6769](https://github.com/agda/agda/issues/6769): Various symbol additions to agda-input+- [PR #6870](https://github.com/agda/agda/issues/6870): [ fix #6867 ] Only consider arguments with @0 for forcing if --erasure is on+- [PR #6978](https://github.com/agda/agda/issues/6978): [ fix #6976 ] Add constraint for resolving the head of an instance+- [PR #7055](https://github.com/agda/agda/issues/7055): Unspine system projections when they have display forms+- [PR #7071](https://github.com/agda/agda/issues/7071): Eta-expand mismatched cubical primitives+- [PR #7078](https://github.com/agda/agda/issues/7078): Left-hand side `let`+- [PR #7109](https://github.com/agda/agda/issues/7109): Discrimination trees for instance search+- [PR #7115](https://github.com/agda/agda/issues/7115): Flake improvements+- [PR #7119](https://github.com/agda/agda/issues/7119): Split GenericWarning into individual warnings+- [PR #7121](https://github.com/agda/agda/issues/7121): Update installation.rst+- [PR #7138](https://github.com/agda/agda/issues/7138): Fix #7136: proper error when pattern definition has unsupported arguments+- [PR #7142](https://github.com/agda/agda/issues/7142): Fix #6783: error for @tactic on lambda+- [PR #7144](https://github.com/agda/agda/issues/7144): Add reference to Cornelis in the documentation+- [PR #7147](https://github.com/agda/agda/issues/7147): Fix #7146: printing of cohesion and lock attributes+- [PR #7149](https://github.com/agda/agda/issues/7149): Fix mutual information not being set properly by the positivity checker+- [PR #7155](https://github.com/agda/agda/issues/7155): Fix #6866: User Manual: Make Installation as Easy as Possible+- [PR #7159](https://github.com/agda/agda/issues/7159): Fix #7158: Application: check for sufficient arity before checking target+- [PR #7160](https://github.com/agda/agda/issues/7160): Fix #6667: case not `__IMPOSSIBLE__` for nullary syntax+- [PR #7161](https://github.com/agda/agda/issues/7161): Fix #6945: warn about useless private even in absense of nice decls+- [PR #7162](https://github.com/agda/agda/issues/7162): Blocks in Concrete syntax: store Range of block keyword+- [PR #7168](https://github.com/agda/agda/issues/7168): Fix #7167: type checking underapplied pattern synonyms+- [PR #7169](https://github.com/agda/agda/issues/7169): Trigger and improve error UnusedVariableInPatternSynonym+- [PR #7173](https://github.com/agda/agda/issues/7173): Part of #2829: Allow instance arguments in pattern synonyms that are such in the pattern already+- [PR #7179](https://github.com/agda/agda/issues/7179): Fix #7177: only setScope when scope is not null+- [PR #7180](https://github.com/agda/agda/issues/7180): Use compareAs for assignE even in compareAtom+- [PR #7183](https://github.com/agda/agda/issues/7183): Instance overlap pragmas+- [PR #7185](https://github.com/agda/agda/issues/7185): Fix #7176: turn absurd pattern in instance position to instance meta+- [PR #7197](https://github.com/agda/agda/issues/7197): Re. #7196: Only prune instances in serialised iface+- [PR #7203](https://github.com/agda/agda/issues/7203): Fix incorrectly quoted sorts+- [PR #7204](https://github.com/agda/agda/issues/7204): Fix #7202: ModuleDoesntExport: only highlight missing names+- [PR #7209](https://github.com/agda/agda/issues/7209): Fix #7208: restore missing check for OverlappingProjects+- [PR #7210](https://github.com/agda/agda/issues/7210): Fix range for deprecated module import warning when applied+- [PR #7211](https://github.com/agda/agda/issues/7211): Fix #7181: Allow matching to continue when stuck on lazy pattern+- [PR #7222](https://github.com/agda/agda/issues/7222): Fix #7219: only warn about problems with warning options+- [PR #7231](https://github.com/agda/agda/issues/7231): Instantiate terms before traversing them in tcExtendContext+- [PR #7237](https://github.com/agda/agda/issues/7237): Fix #7236: use context rather than telescope for lambda-bound variables in rewrite patterns+- [PR #7238](https://github.com/agda/agda/issues/7238): Build with GHC 9.10+- [PR #7241](https://github.com/agda/agda/issues/7241): Drop time-compat dependency and Stack LTS for GHC 8.6+- [PR #7243](https://github.com/agda/agda/issues/7243): re. 7218: Saturate opaque blocks after Give commands+- [PR #7248](https://github.com/agda/agda/issues/7248): Overhaul dead code elimination, make --save-metas the default+- [PR #7249](https://github.com/agda/agda/issues/7249): docs/installation: point new wiki+- [PR #7251](https://github.com/agda/agda/issues/7251): re. 7250: copy instanceinfo+- [PR #7252](https://github.com/agda/agda/issues/7252): Fix #7193: persistently remember what is a projection+- [PR #7260](https://github.com/agda/agda/issues/7260): Reflection primitive to solve instances+- [PR #7273](https://github.com/agda/agda/issues/7273): ToTreeless: allow backends to define custom pipelines+- [PR #7274](https://github.com/agda/agda/issues/7274): #7182: copied records should refer to the copied constructor and fields+- [PR #7276](https://github.com/agda/agda/issues/7276): #7191: respect abstract mode when using show function+- [PR #7283](https://github.com/agda/agda/issues/7283): agdaLatex  documentation+- [PR #7292](https://github.com/agda/agda/issues/7292): New error warning `ConstructorDoesNotFitInData` instead of hard error.+- [PR #7298](https://github.com/agda/agda/issues/7298): Remove fiddly attempt at instance postponement+- [PR #7300](https://github.com/agda/agda/issues/7300): New deadcode warning CoinductiveEtaRecord instead of GenericError+- [PR #7302](https://github.com/agda/agda/issues/7302): Fix #7301 (loop in parser): move verifyRecordDirectives to scope checker+- [PR #7305](https://github.com/agda/agda/issues/7305): Fix #7286: don't fail hard when there are instances with unresolved types+- [PR #7307](https://github.com/agda/agda/issues/7307): fix #7017: document instance projections+- [PR #7310](https://github.com/agda/agda/issues/7310): Add `workOnTypes` reflection primitive+- [PR #7311](https://github.com/agda/agda/issues/7311): [ #6406 ] Add test cases from discussion on this issue+- [PR #7313](https://github.com/agda/agda/issues/7313): Update universe-levels.lagda.rst+- [PR #7314](https://github.com/agda/agda/issues/7314): Add constructors for custom backend warning/errors+- [PR #7315](https://github.com/agda/agda/issues/7315): same shadowing logic for record patterns as for constructor patterns in absToCon+- [PR #7316](https://github.com/agda/agda/issues/7316): add \crossmark to emacs input mode+- [PR #7317](https://github.com/agda/agda/issues/7317): Don't mark eta unit records as irrelevant+- [PR #7319](https://github.com/agda/agda/issues/7319): Make --postfix-projections the default+- [PR #7320](https://github.com/agda/agda/issues/7320): Turn on --exact-split by default+- [PR #7322](https://github.com/agda/agda/issues/7322): Expose constructor erasure in reflection interface+- [PR #7325](https://github.com/agda/agda/issues/7325): add CSS rule for macro names+- [PR #7327](https://github.com/agda/agda/issues/7327): proper error instead of impossible for clauseless pat-lam+- [PR #7330](https://github.com/agda/agda/issues/7330): [#7329] Correct module name in module applications+- [PR #7333](https://github.com/agda/agda/issues/7333): [#7332] don't loop when quoting dependent copattern lambdas+- [PR #7334](https://github.com/agda/agda/issues/7334): Fix #7331: handle permission error in search for project file+- [PR #7336](https://github.com/agda/agda/issues/7336): Remove duplicate imports and pragmas in MAlonzo+- [PR #7338](https://github.com/agda/agda/issues/7338): (#7337) foreign code needs to go in post-scope state+- [PR #7343](https://github.com/agda/agda/issues/7343): Turn illegal rewrite rules into an error warning+- [PR #7347](https://github.com/agda/agda/issues/7347): [ fix #7266 ] Check that constructor names match before projecting in `matchPattern`+- [PR #7349](https://github.com/agda/agda/issues/7349): Fix #7346 by not considering HIT-constructor arguments forced+- [PR #7350](https://github.com/agda/agda/issues/7350): Fix #6744 by reducing during forcing analysis.+- [PR #7352](https://github.com/agda/agda/issues/7352): Fix issue 7262: Range of the lhs modality check+- [PR #7353](https://github.com/agda/agda/issues/7353): Update installation docs (e.g. re #7163: document installation problems with `executable-dynamic`)+- [PR #7355](https://github.com/agda/agda/issues/7355): Make `--keep-pattern-variables` the default+- [PR #7356](https://github.com/agda/agda/issues/7356): Add --save-metas default to CHANGELOG+- [PR #7358](https://github.com/agda/agda/issues/7358): [ doc ] Document `--termination-depth` in user manual+- [PR #7359](https://github.com/agda/agda/issues/7359): Fix #7354 by making types of live metas live in DeadCode+- [PR #7360](https://github.com/agda/agda/issues/7360): Fix for issue #6841 and related changes+- [PR #7362](https://github.com/agda/agda/issues/7362): Fix #6919: separate warnings by empty line+- [PR #7364](https://github.com/agda/agda/issues/7364): Resolve instance overlap for irrelevant metas+- [PR #7367](https://github.com/agda/agda/issues/7367): Minor fixes to instance overlap + constraint postponement+- [PR #7383](https://github.com/agda/agda/issues/7383): Fix #7382: make all module param sections live in DeadCode+- [PR #7386](https://github.com/agda/agda/issues/7386): Testcase for #7382 (completes PR #7383)+- [PR #7404](https://github.com/agda/agda/issues/7404): Fix #7401: do not fail hard in Setup.hs if library interface files cannot be built+- [PR #7410](https://github.com/agda/agda/issues/7410): Fixup #7404 and test agdai-generation in cabal-install workflow+- [PR #7419](https://github.com/agda/agda/issues/7419): #7380: add clauses to generalizedTel projections+- [PR #7423](https://github.com/agda/agda/issues/7423): Fixup #7265: restore passing arguments from goal to Mimer

@@ -6,21 +6,24 @@  Agda 2 is currently actively developed mainly by Andreas Abel, Guillaume Allais, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt,-Nils Anders Danielsson, Amélia Liao, Ulf Norell, and-Andrés Sicard-Ramírez.+Nils Anders Danielsson, Amélia Liao, and Ulf Norell.  Further, Agda 2 has received contributions by, amongst others, Arthur Adjedj, Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, Guillaume Brunerie,-James Chapman, Jonathan Coates,+James Chapman, Lawrence Chonavel, Jonathan Coates, Dominique Devriese, Péter Diviánszky, Robert Estelle,-Olle Fredriksson, Adam Gundry, Daniel Gustafsson, Philipp Hausmann,+Naïm Favier, Kuen-Bang Hou (Favonia), Olle Fredriksson,+Adam Gundry, Daniel Gustafsson,+Philipp Hausmann, Alex Haršáni, Alan Jeffrey, Phil de Joux,-Wolfram Kahl, Wen Kokke, John Leo, Fredrik Lindblad,-Víctor López Juan, Ting-Gan Lua, Francesco Mazzoli, Stefan Monnier,-Guilhem Moulin, Konstantin Nisht, Fredrik Nordvall Forsberg,-Josselin Poiret, Nicolas Pouillard, Jonathan Prieto, Christian Sattler,-Makoto Takeyama, Andrea Vezzosi, Noam Zeilberger, and Tesla Ice Zhang.+Wolfram Kahl, Andre Knispel, Wen Kokke, András Kovács,+John Leo, Fredrik Lindblad, Víctor López Juan, Ting-Gan Lua,+Francesco Mazzoli, Stefan Monnier, Guilhem Moulin,+Konstantin Nisht, Fredrik Nordvall Forsberg, Andreas Nuyts,+Josselin Poiret, Nicolas Pouillard, Jonathan Prieto,+Christian Sattler, Michael Shulman, Andrés Sicard-Ramírez,+Makoto Takeyama, Andrea Vezzosi, Szumi Xie, Noam Zeilberger, and Tesla Ice Zhang. The full list of contributors is available at https://github.com/agda/agda/graphs/contributors or from the git repository via ``git shortlog -sne``.

@@ -7,7 +7,7 @@ [![Documentation Status](https://readthedocs.org/projects/agda/badge/?version=latest)](http://agda.readthedocs.io/en/latest/?badge=latest) [![Agda Zulip](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://agda.zulipchat.com) -![The official Agda logo](doc/user-manual/agda.svg)+![The official Agda logo](https://raw.githubusercontent.com/agda/agda/master/doc/user-manual/agda.svg)  Note that this README is only about Agda, not its standard library. See the [Agda Wiki][agdawiki] for information about the

@@ -1,4 +1,4 @@-{-# LANGUAGE NondecreasingIndentation #-}+{-# LANGUAGE ScopedTypeVariables #-}  import Data.List import Data.Maybe@@ -18,8 +18,8 @@ import System.IO import System.IO.Error (isDoesNotExistError) -import Control.Monad (forM_, unless)-import Control.Exception (bracket, catch, throwIO)+import Control.Monad+import Control.Exception  main :: IO () main = defaultMainWithHooks userhooks@@ -44,9 +44,9 @@   copyHook simpleUserHooks pd lbi hooks flags   unless (skipInterfaces lbi) $ do     -- Generate .agdai files.-    generateInterfaces pd lbi+    success <- generateInterfaces pd lbi     -- Copy again, now including the .agdai files.-    copyHook simpleUserHooks pd' lbi hooks flags+    when success $ copyHook simpleUserHooks pd' lbi hooks flags   where   pd' = pd     { dataFiles = concatMap (expandAgdaExt pd) $ dataFiles pd@@ -89,7 +89,9 @@ skipInterfaces :: LocalBuildInfo -> Bool skipInterfaces lbi = fromPathTemplate (progSuffix lbi) == "-quicker" -generateInterfaces :: PackageDescription -> LocalBuildInfo -> IO ()+-- | Returns 'True' if call to Agda executes without error.+--+generateInterfaces :: PackageDescription -> LocalBuildInfo -> IO Bool generateInterfaces pd lbi = do    -- for debugging, these are examples how you can inspect the flags...@@ -121,6 +123,13 @@    -- Type-check all builtin modules (in a single Agda session to take   -- advantage of caching).+  let agdaDirEnvVar = "Agda_datadir"+  let agdaArgs =+        [ "--interaction"+        , "--interaction-exit-on-error"+        , "-Werror"+        , "-v0"+        ]   let loadBuiltinCmds = concat         [ [ cmd ("Cmd_load " ++ f ++ " []")           , cmd "Cmd_no_metas"@@ -130,21 +139,39 @@         , let f     = show (ddir </> b)               cmd c = "IOTCM " ++ f ++ " None Indirect (" ++ c ++ ")"         ]+  let callLines = concat+        [ [ unwords $ concat+            [ [ concat [ agdaDirEnvVar, "=", ddir ] ]+            , [ agda ]+            , agdaArgs+            , [ "<<EOF" ]+            ]+          ]+        , loadBuiltinCmds+        , [ "EOF" ]+        ]+  let onIOError (e :: IOException) = False <$ do+        putStr $ unlines $ concat+          [ [ "*** Warning!"+            , "*** Could not generate Agda library interface files."+            , "*** Reason:"+            , show e+            , "*** The attempted call to Agda was:"+            ]+          , callLines+          , [ "*** Ignoring error, continuing installation..." ]+          ]   env <- getEnvironment-  _output <- readCreateProcess-      (proc agda-          [ "--interaction"-          , "--interaction-exit-on-error"-          , "-Werror"-          , "-v0"-          ])+  handle onIOError $ do+    True <$ readCreateProcess+      (proc agda agdaArgs)         { delegate_ctlc = True                           -- Make Agda look for data files in a                           -- certain place.-        , env           = Just (("Agda_datadir", ddir) : env)+        , env           = Just ((agdaDirEnvVar, ddir) : env)         }       (unlines loadBuiltinCmds)-  return ()+  agdaExeExtension :: String agdaExeExtension = exeExtension buildPlatform

@@ -0,0 +1,17 @@+Release notes for Agda version 2.6.4.3+======================================++This release fixes a regression in 2.6.4.3 and one in 2.6.4.+It aims to be API-compatible with 2.6.4.1 and 2.6.4.2.++Agda 2.6.4.3 supports GHC versions 8.6.5 to 9.8.1.++Closed issues+-------------++For 2.6.4.3, the following issues were+[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.4.3+is%3Aclosed)+(see [bug tracker](https://github.com/agda/agda/issues)):++- [Issue #7148](https://github.com/agda/agda/issues/7148): Regression in 2.6.4.2 concerning `with`+- [Issue #7150](https://github.com/agda/agda/issues/7150): Regression in 2.6.4 in `rewrite` with instances

@@ -7,7 +7,10 @@ module Main (main) where  import Control.Exception as E+import Control.Applicative import Control.Monad+import Data.Bifunctor (first, second)+import Data.Bool (bool) import Data.Char import Data.List (intercalate, isInfixOf) import Data.Maybe@@ -248,14 +251,18 @@ 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+  (existing, missing) <- partitionM doesFileExist elFiles+  failed <- catMaybes <$> mapM (compile dataDir) existing++  -- If any of the .el files was missing or failed to compile, fail execution.+  unless (null missing) $ do+    informLn "Missing Emacs Lisp files:"+    mapM_ (informLn . ("  " ++)) missing+  unless (null failed) $ do+    informLn "Unable to compile the following Emacs Lisp files:"+    mapM_ (informLn . ("  " ++)) failed+  unless (null missing && null failed) exitFailure+   where   compile dataDir f = do     exit <- rawSystemWithDiagnostics "emacs" $@@ -286,3 +293,11 @@ -- LISP application apply :: [String] -> String apply = parens . unwords++-- Utilities++-- | A ``monadic'' version of @'partition' :: (a -> Bool) -> [a] -> ([a],[a])+partitionM :: Applicative m => (a -> m Bool) -> [a] -> m ([a], [a])+partitionM f =+  foldr (\ x -> liftA2 (bool (second (x:)) (first (x:))) $ f x)+        (pure ([], []))

@@ -277,6 +277,8 @@   ("exn" . ("∄"))   ("0"   . ("∅"))   ("C"   . ("∁"))+  ("uin"    . ("⟒"))+  ("din"    . ("⫙"))    ;; Corners, ceilings and floors. @@ -308,13 +310,15 @@   ("+ "        . ("⊹"))   ("+"         . ("＋"))   ("sqrt"      . ("√"))+  ("surd"      . ("√"))   ("surd3"     . ("∛"))   ("surd4"     . ("∜"))   ("increment" . ("∆"))   ("inf"       . ("∞"))-  ("&"         . ("⅋"))+  ("&"         . ,(agda-input-to-string-list "⅋﹠＆"))   ("z;"        . ,(agda-input-to-string-list "⨟⨾"))   ("z:"        . ("⦂"))+  ("at"        . ,(agda-input-to-string-list "@﹫＠"))    ;; Circled operators. @@ -335,13 +339,19 @@    ;; Boxed operators. -  ("b+" . ("⊞"))-  ("b-" . ("⊟"))-  ("bx" . ("⊠"))-  ("b." . ("⊡"))+  ("b+"  . ("⊞"))+  ("b-"  . ("⊟"))+  ("bx"  . ("⊠"))+  ("b."  . ("⊡")) -  ;; APL boxed operators+  ("b/"  . ("⧄"))+  ("b\\" . ("⧅"))+  ("b*"  . ("⧆"))+  ("bo"  . ("⧇"))+  ("bsq" . ("⧈")) +  ;; APL boxed operators.+   ("box="       . ("⌸"))   ("box?"       . ("⍰"))   ("box'"       . ("⍞"))@@ -376,6 +386,7 @@   ("integral" . ,(agda-input-to-string-list "∫∬∭∮∯∰∱∲∳"))   ("angle"    . ,(agda-input-to-string-list "∟∡∢⊾⊿"))   ("join"     . ,(agda-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗"))+  ("esh"      . ("ʃ"))    ;; Arrows. @@ -690,7 +701,7 @@   ("B8"   . ("𝟖"))   ("B9"   . ("𝟗")) -  ;; Fullwidth letters+  ;; Fullwidth letters.    ("FA"   . ("Ａ"))   ("FB"   . ("Ｂ"))@@ -745,7 +756,7 @@   ("Fy"   . ("ｙ"))   ("Fz"   . ("ｚ")) -  ;; Fullwidth digits+  ;; Fullwidth digits.    ("F0"   . ("０"))   ("F1"   . ("１"))@@ -758,6 +769,42 @@   ("F8"   . ("８"))   ("F9"   . ("９")) +  ;; Fullwidth symbols.++  ("F!"   . ("！"))+  ("F\""  . ("＂"))+  ("F#"   . ("＃"))+  ("F$"   . ("＄"))+  ("F%"   . ("％"))+  ("F&"   . ("＆"))+  ("F'"   . ("＇"))+  ("F("   . ("（"))+  ("F)"   . ("）"))+  ("F*"   . ("＊"))+  ("F+"   . ("＋"))+  ("F,"   . ("，"))+  ("F-"   . ("－"))+  ("F."   . ("．"))+  ("F/"   . ("／"))+  ("F:"   . ("："))+  ("F;"   . ("；"))+  ("F<"   . ("＜"))+  ("F="   . ("＝"))+  ("F>"   . ("＞"))+  ("F?"   . ("？"))+  ("F@"   . ("＠"))+  ("F["   . ("［"))+  ("F\\"  . ("＼"))+  ("F]"   . ("］"))+  ("F_"   . ("＿"))+  ("F{"   . ("｛"))+  ("F|"   . ("｜"))+  ("F}"   . ("｝"))+  ("F~"   . ("～"))+  ("F(("  . ("｟"))+  ("F))"  . ("｠"))+  ("Fneg" . ("￢"))+   ;; Parentheses.    ("(" . ,(agda-input-to-string-list "([{⁅⁽₍〈⎴⟅⟦⟨⟪⦃〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢❪❬❰❲❴⟮⦅⦗⧼⸨❮⦇⦉"))@@ -805,9 +852,11 @@    ;; Musical symbols. -  ("note" . ,(agda-input-to-string-list "♩♪♫♬"))-  ("b"    . ("♭"))-  ("#"    . ("♯"))+  ("note"    . ,(agda-input-to-string-list "♩♪♫♬"))+  ("b"       . ("♭"))+  ("#"       . ("♯"))+  ("bb"      . ("𝄫"))+  ("##"      . ("𝄪"))    ;; Other punctuation and symbols. @@ -837,12 +886,13 @@   ("@"          . ("＠"))   ("__"         . ("＿"))   ("\""         . ("＂"))+  ("crossmark"  . ("✗"))    ;; Some combining characters.   ;;   ;; The following combining characters also have (other)   ;; translations:-  ;; ̀ ́ ̂ ̃ ̄ ̆ ̇ ̈ ̋ ̌ ̣ ̧ ̱+  ;;    ("^--" . ,(agda-input-to-string-list"̅̿"))   ("_--" . ,(agda-input-to-string-list"̲̳"))@@ -888,7 +938,7 @@   ("Gp"  . ("ψ"))  ("GP"  . ("Ψ"))   ("Go"  . ("ω"))  ("GO"  . ("Ω")) -  ;; Mathematical characters+  ;; Mathematical characters.    ("MiA" . ("𝐴"))   ("MiB" . ("𝐵"))@@ -942,6 +992,7 @@   ("Mix" . ("𝑥"))   ("Miy" . ("𝑦"))   ("Miz" . ("𝑧"))+   ("MIA" . ("𝑨"))   ("MIB" . ("𝑩"))   ("MIC" . ("𝑪"))@@ -968,6 +1019,7 @@   ("MIX" . ("𝑿"))   ("MIY" . ("𝒀"))   ("MIZ" . ("𝒁"))+   ("MIa" . ("𝒂"))   ("MIb" . ("𝒃"))   ("MIc" . ("𝒄"))@@ -994,6 +1046,7 @@   ("MIx" . ("𝒙"))   ("MIy" . ("𝒚"))   ("MIz" . ("𝒛"))+   ("McA" . ("𝒜"))   ("McB" . ("ℬ"))   ("McC" . ("𝒞"))@@ -1046,6 +1099,7 @@   ("Mcx" . ("𝓍"))   ("Mcy" . ("𝓎"))   ("Mcz" . ("𝓏"))+   ("MCA" . ("𝓐"))   ("MCB" . ("𝓑"))   ("MCC" . ("𝓒"))@@ -1098,6 +1152,7 @@   ("MCx" . ("𝔁"))   ("MCy" . ("𝔂"))   ("MCz" . ("𝔃"))+   ("MfA" . ("𝔄"))   ("MfB" . ("𝔅"))   ("MfC" . ("ℭ"))@@ -1151,7 +1206,7 @@   ("Mfy" . ("𝔶"))   ("Mfz" . ("𝔷")) -  ;; (Sub / Super) scripts+  ;; (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@@ -1247,13 +1302,17 @@   ;; ("^Y" . ("Y"))   ;; ("^Z" . ("Z")) +  ("^Ga" . ("ᵅ"))   ("^Gb" . ("ᵝ"))   ("^Gg" . ("ᵞ"))   ("^Gd" . ("ᵟ"))   ("^Ge" . ("ᵋ"))   ("^Gth" . ("ᶿ"))+  ("^Gi" . ("ᶥ"))   ("^Gf" . ("ᵠ"))   ("^Gc" . ("ᵡ"))++  ("^GF" . ("ᶲ"))    ;; Some ISO8859-1 characters. 

@@ -1,3 +1,3 @@-(define-package "agda2-mode" "2.6.4.3"+(define-package "agda2-mode" "2.7.0"   "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

@@ -28,7 +28,7 @@  ;;; Code: -(defvar agda2-version "2.6.4.3"+(defvar agda2-version "2.7.0"   "The version of the Agda mode. Note that the same version of the Agda executable must be used.") @@ -232,7 +232,7 @@     (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-mimer-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)")@@ -886,16 +886,6 @@       (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."@@ -1379,13 +1369,26 @@                           'agda2-solveAll)) ) -(defun agda2-auto-maybe-all ()-  "Run auto.+(defun agda2-mimer-maybe-all ()+  "Run proof search. 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-mimer+                          'agda2-mimerAll))+)++(agda2-maybe-normalised-asis+  agda2-mimer+  "Run proof search on a goal."+  "Cmd_autoOne"+  'goal+)++(agda2-maybe-normalised-toplevel-asis-noprompt+  agda2-mimerAll+  "Solves all goals by simple proof search."+  "Cmd_autoAll" )  (agda2-maybe-normalised-toplevel-asis-noprompt

@@ -19,6 +19,7 @@ .Agda .Datatype               { color: #0000CD } .Agda .Field                  { color: #EE1289 } .Agda .Function               { color: #0000CD }+.Agda .Macro                  { color: #0000CD } .Agda .Module                 { color: #A020F0 } .Agda .Postulate              { color: #0000CD } .Agda .Primitive              { color: #0000CD }

@@ -6,7 +6,7 @@ % !!! NOTE: when you make changes to this file, bump the date. !!! % !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! \ProvidesPackage{agda}-  [2021/07/14 version 2.6.4.3 Formatting LaTeX generated by Agda]+  [2021/07/14 version 2.7.0 Formatting LaTeX generated by Agda]  \RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,                 calc, environ, xparse, xkeyval}

@@ -247,7 +247,7 @@   function    : (cs : List Clause) → Definition   data-type   : (pars : Nat) (cs : List Name) → Definition   record-type : (c : Name) (fs : List (Arg Name)) → Definition-  data-cons   : (d : Name) → Definition+  data-cons   : (d : Name) (q : Quantity) → Definition   axiom       : Definition   prim-fun    : Definition @@ -296,7 +296,7 @@   declareDef       : Arg Name → Type → TC ⊤   declarePostulate : Arg Name → Type → TC ⊤   declareData      : Name → Nat → Type → TC ⊤-  defineData       : Name → List (Σ Name (λ _ → Type)) → TC ⊤+  defineData       : Name → List (Σ Name (λ _ → Σ Quantity (λ _ → Type))) → TC ⊤   defineFun        : Name → List Clause → TC ⊤   getType          : Name → TC Type   getDefinition    : Name → TC Definition@@ -334,6 +334,9 @@   -- "blocking" constraints.   noConstraints : ∀ {a} {A : Set a} → TC A → TC A +  -- Run the given computation at the type level, allowing use of erased things.+  workOnTypes : ∀ {a} {A : Set a} → TC A → TC A+   -- Run the given TC action and return the first component. Resets to   -- the old TC state if the second component is 'false', or keep the   -- new TC state if it is 'true'.@@ -343,6 +346,12 @@   -- variable (it does not have to be an instance meta).   getInstances : Meta → TC (List Term) +  -- Try to solve open instance constraints. When wrapped in `noConstraints`,+  -- fails if there are unsolved instance constraints left over that originate+  -- from the current macro invokation. Outside constraints are still attempted,+  -- but failure to solve them are ignored by `noConstraints`.+  solveInstanceConstraints : TC ⊤+ {-# BUILTIN AGDATCM                           TC                         #-} {-# BUILTIN AGDATCMRETURN                     returnTC                   #-} {-# BUILTIN AGDATCMBIND                       bindTC                     #-}@@ -383,8 +392,10 @@ {-# BUILTIN AGDATCMFORMATERRORPARTS           formatErrorParts           #-} {-# BUILTIN AGDATCMDEBUGPRINT                 debugPrint                 #-} {-# BUILTIN AGDATCMNOCONSTRAINTS              noConstraints              #-}+{-# BUILTIN AGDATCMWORKONTYPES                workOnTypes                #-} {-# BUILTIN AGDATCMRUNSPECULATIVE             runSpeculative             #-} {-# BUILTIN AGDATCMGETINSTANCES               getInstances               #-}+{-# BUILTIN AGDATCMSOLVEINSTANCES             solveInstanceConstraints   #-}  -- All the TC primitives are compiled to functions that return -- undefined, rather than just undefined, in an attempt to make sure

@@ -1,512 +0,0 @@--module Agda.Auto.Auto-      (auto-      , AutoResult(..)-      , AutoProgress(..)-      ) where--import Prelude hiding ((!!), null)--import Control.Monad          ( filterM, forM, guard, join, when )-import Control.Monad.Except-import Control.Monad.IO.Class ( MonadIO(..) )-import Control.Monad.State--import qualified Data.List as List-import qualified Data.Map as Map-import Data.IORef-import qualified System.Timeout-import Data.Maybe-import qualified Data.Traversable as Trav-import qualified Data.HashMap.Strict as HMap--import Agda.Utils.Permutation (permute, takeP)-import Agda.TypeChecking.Monad hiding (withCurrentModule)-import Agda.TypeChecking.Telescope-import qualified Agda.Syntax.Abstract as A-import Agda.Syntax.Abstract.Pretty (prettyA)-import qualified Agda.Syntax.Concrete.Name as C-import qualified Text.PrettyPrint.Annotated as PP-import qualified Agda.TypeChecking.Pretty as TCM-import Agda.Syntax.Position-import qualified Agda.Syntax.Internal as I-import Agda.Syntax.Translation.InternalToAbstract-import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcreteScope, abstractToConcrete_, runAbsToCon, toConcrete)-import Agda.Interaction.Base-import Agda.Interaction.BasicOps hiding (refine)-import Agda.TypeChecking.Reduce (normalise)-import Agda.Syntax.Common-import qualified Agda.Syntax.Scope.Base as Scope-import Agda.Syntax.Scope.Monad (withCurrentModule)-import qualified Agda.Syntax.Abstract.Name as AN-import qualified Agda.TypeChecking.Monad.Base as TCM-import Agda.TypeChecking.EtaContract (etaContract)--import Agda.Auto.Options-import Agda.Auto.Convert-import Agda.Auto.NarrowingSearch-import Agda.Auto.Syntax-import Agda.Auto.SearchControl-import Agda.Auto.Typecheck--import Agda.Auto.CaseSplit--import Agda.Utils.Functor-import Agda.Utils.Impossible-import Agda.Utils.Lens-import Agda.Utils.List-import qualified Agda.Utils.List1 as List1-import Agda.Utils.Maybe-import Agda.Utils.Null-import Agda.Syntax.Common.Pretty ( prettyShow )-import Agda.Utils.Size-import Agda.Utils.Tuple---insertAbsurdPattern :: String -> String-insertAbsurdPattern [] = []-insertAbsurdPattern s@(_:_) | take (length abspatvarname) s == abspatvarname = "()" ++ drop (length abspatvarname) s-insertAbsurdPattern (c:s) = c : insertAbsurdPattern s--getHeadAsHint :: A.Expr -> Maybe Hint-getHeadAsHint (A.ScopedExpr _ e) = getHeadAsHint e-getHeadAsHint (A.Def qname)      = Just $ Hint False qname-getHeadAsHint (A.Proj _ qname)   = Just $ Hint False $ AN.headAmbQ qname-getHeadAsHint (A.Con qname)      = Just $ Hint True  $ AN.headAmbQ qname-getHeadAsHint _ = Nothing---- | Result type: Progress & potential Message for the user------   The  of the Auto tactic can be one of the following three:------   1. @Solutions [(ii,s)]@---      A list of solutions @s@ for interaction ids @ii@.---      In particular, @Solutions []@ means Agsy found no solution.------   2. @FunClauses cs@---      A list of clauses for the interaction id @ii@ in which Auto---      was invoked with case-splitting turned on.------   3. @Refinement s@---      A refinement for the interaction id @ii@ in which Auto was invoked.--data AutoProgress =-    Solutions  [(InteractionId, String)]-  | FunClauses [String]-  | Refinement String--data AutoResult = AutoResult-  { autoProgress :: AutoProgress-  , autoMessage  :: Maybe String-  }--stopWithMsg :: String -> TCM AutoResult-stopWithMsg msg = return $ AutoResult (Solutions []) (Just msg)---- | Entry point for Auto tactic (Agsy).------   If the @autoMessage@ part of the result is set to @Just msg@, the---   message @msg@ produced by Agsy should be displayed to the user.--{-# SPECIALIZE auto :: InteractionId -> Range -> String -> TCM AutoResult #-}-auto-  :: MonadTCM tcm-  => InteractionId-  -> Range-  -> String-  -> tcm AutoResult-auto ii rng argstr = liftTCM $ locallyTC eMakeCase (const True) $ do--  -- Parse hints and other configuration.-  let autoOptions = parseArgs argstr-  let hints    = autoOptions ^. aoHints-  let timeout  = autoOptions ^. aoTimeOut-  let pick     = autoOptions ^. aoPick-  let mode     = autoOptions ^. aoMode-  let hintmode = autoOptions ^. aoHintMode-  ahints <- case mode of-    MRefine{} -> return []-    _         -> mapM (parseExprIn ii rng) hints-  let failHints = stopWithMsg "Hints must be a list of constant names"--  eqstuff <- getEqCombinators ii rng--  caseMaybe (mapM getHeadAsHint ahints) failHints $ \ ehints -> do--    -- Get the meta variable for the interaction point we are trying to fill.-    -- Add the @autohints@ for that meta to the hints collection.-    mi <- lookupInteractionId ii-    thisdefinfo <- findClauseDeep ii-    ehints <- (ehints ++) <$> do autohints hintmode mi $ fmap fst3 thisdefinfo--    -- If @thisdefinfo /= Nothing@ get the its type (normalized).-    mrectyp <- maybeToList <$> do-      Trav.forM thisdefinfo $ \ (def, _, _) -> do-        normalise =<< do TCM.defType <$> getConstInfo def--    (myhints', mymrectyp, tccons, eqcons, cmap) <- tomy mi (ehints ++ eqstuff) mrectyp--    let (myhints, c1to6) = splitAt (length myhints' - length eqstuff) myhints'-        meqr = ifNull eqstuff Nothing $ \ _ -> {- else -}-                 let [c1, c2, c3, c4, c5, c6] = c1to6-                 in  Just $ EqReasoningConsts c1 c2 c3 c4 c5 c6---    let tcSearchSC isdep ctx typ trm = caseMaybe meqr a $ \ eqr ->-          mpret $ Sidecondition (calcEqRState eqr trm) a-          where a = tcSearch isdep ctx typ trm--    let (mainm, _, _, _) = tccons Map.! mi-    case mode of-     MNormal listmode disprove -> do-        let numsols = if listmode then 10 else 1-          -- Andreas, 2015-05-17 Issue 1504:-          -- wish to produce several solutions, as-          -- the first one might be ill-typed.-          -- However, currently changing the 1 to something higher makes Agsy loop.-        sols <- liftIO $ newIORef ([] :: [[I.Term]])-        nsol <- liftIO $ newIORef $ pick + numsols-        let hsol = do-             nsol' <- readIORef nsol-             let cond = nsol' <= numsols-             when cond $ do-               trms <- runExceptT-                       $ mapM (\ (m , _, _, _) -> convert (Meta m) :: MOT I.Term)-                       $ Map.elems tccons-               case trms of-                 Left{}     -> writeIORef nsol $! nsol' + 1-                 Right trms -> modifyIORef sols (trms :)-                 -- Right trms -> if listmode then modifyIORef sols (trms :)-                 --                           else writeIORef sols [trms]-        ticks <- liftIO $ newIORef 0--        let exsearch initprop recinfo defdfv =-             liftIO $ System.Timeout.timeout (getTimeOut timeout * 1000)-                    $ loop 0-             where-               loop d = do-                 let rechint x = case recinfo of-                                  Nothing -> x-                                  Just (_, recdef) -> (recdef, HMRecCall) : x-                     env = RIEnv { rieHints             = rechint $ map (,HMNormal) myhints-                                 , rieDefFreeVars       = defdfv-                                 , rieEqReasoningConsts = meqr-                                 }-                 depreached <- topSearch ticks nsol hsol env (initprop) d costIncrease-                 nsol' <- readIORef nsol-                 if nsol' /= 0 && depreached then loop (d + costIncrease) else return depreached--        let getsols :: [I.Term] -> TCM [(MetaId, A.Expr)]-            getsols sol = do-             exprs <- forM (zip (Map.keys tccons) sol) $ \ (mi, e) -> do-               mv   <- lookupLocalMetaAuto mi-               e    <- etaContract e-               expr <- modifyAbstractExpr <$> do withMetaInfo (getMetaInfo mv) $ reify e-               return (mi, expr)--             let loop :: I.MetaId -> StateT [I.MetaId] TCM [(I.MetaId, A.Expr)]-                 loop midx = do-                   let (m, _, _, deps) = tccons Map.! midx-                   asolss <- mapM loop deps-                   dones  <- get-                   asols  <- if midx `elem` dones then return [] else do-                     put (midx : dones)-                     return [(midx, fromMaybe __IMPOSSIBLE__ $ lookup midx exprs)]-                   return $ concat asolss ++ asols-             (asols, _) <- runStateT (loop mi) []-             return asols--        if disprove then-          case eqcons of-           [] -> case Map.elems tccons of-            (m, mytype, mylocalVars, _) : [] -> do-                defdfv <- case thisdefinfo of-                           Just (def, _, _) -> getdfv mi def-                           Nothing -> return 0-                ee <- liftIO $ newIORef $ ConstDef {cdname = "T", cdorigin = __IMPOSSIBLE__, cdtype = NotM $ Sort (Set 0), cdcont = Postulate, cddeffreevars = 0}-                let (restargs, modargs) = splitAt (length mylocalVars - defdfv) mylocalVars-                    mytype' = foldl (\x y -> NotM $ Pi Nothing NotHidden (freeIn 0 y) y (Abs NoId x)) mytype restargs-                    htyp = negtype ee mytype'-                    sctx = (Id "h", closify htyp) : map (\x -> (NoId, closify x)) modargs-                    ntt = closify (NotM $ App Nothing (NotM OKVal) (Const ee) (NotM ALNil))-                res <- exsearch (tcSearchSC False sctx ntt (Meta m)) Nothing defdfv-                rsols <- fmap reverse $ liftIO $ readIORef sols-                if null rsols then do-                  nsol' <- liftIO $ readIORef nsol-                  stopWithMsg $ insuffsols (pick + numsols - nsol')-                 else do-                  aexprss <- mapM getsols rsols-                  cexprss <- forM aexprss $ mapM $ \(mi, e) -> do-                    mv <- lookupLocalMetaAuto mi-                    withMetaInfo (getMetaInfo mv) $ do-                      (mi,) <$> abstractToConcrete_ e-                  let ss = dropWhile (== ' ') . dropWhile (/= ' ') . prettyShow-                      disp [(_, cexpr)] = ss cexpr-                      disp cexprs = concatMap (\ (mi, cexpr) -> ss cexpr ++ " ") cexprs-                  ticks <- liftIO $ readIORef ticks-                  stopWithMsg $ unlines $-                    ("Listing disproof(s) " ++ show pick ++ "-" ++ show (pick + length rsols - 1)) :-                    for (zip cexprss [pick..]) (\ (x, y) -> show y ++ "  " ++ disp x)-            _ -> stopWithMsg "Metavariable dependencies not allowed in disprove mode"-           _ -> stopWithMsg "Metavariable dependencies not allowed in disprove mode"-         else do-          (recinfo, defdfv) <--           case thisdefinfo of-            Just (def, clause, _) -> do-             let [rectyp'] = mymrectyp-             defdfv <- getdfv mi def-             myrecdef <- liftIO $ newIORef $ ConstDef {cdname = "", cdorigin = (Nothing, def), cdtype = rectyp', cdcont = Postulate, cddeffreevars = defdfv}-             (_, pats) <- constructPats cmap mi clause-             defdfv <- getdfv mi def-             return $ if contains_constructor pats then-               (Just (pats, myrecdef), defdfv)-              else-               (Nothing, defdfv)-            Nothing -> return (Nothing, 0)-          let tc (m, mytype, mylocalVars) isdep = tcSearchSC isdep (map (\x -> (NoId, closify x)) mylocalVars) (closify mytype) (Meta m)-              initprop =-                foldl (\x (ineq, e, i) -> mpret $ And Nothing x (comp' ineq (closify e) (closify i)))-                 (foldl (\x (m, mt, mlv, _) ->-                   if hequalMetavar m mainm then-                    case recinfo of-                     Just (recpats, recdef) ->-                      mpret $ Sidecondition (localTerminationSidecond (localTerminationEnv recpats) recdef (Meta m))-                                            (tc (m, mt, mlv) False)-                     Nothing -> mpret $ And Nothing x (tc (m, mt, mlv) False)-                   else-                    mpret $ And Nothing x (tc (m, mt, mlv) True)-                  )-                  (mpret OK)-                  (Map.elems tccons)-                 ) eqcons-          res <- exsearch initprop recinfo defdfv-          riis <- map swap <$> getInteractionIdsAndMetas-          let timeoutString | isNothing res = " after timeout (" ++ show timeout ++ "ms)"-                            | otherwise     = ""-          if listmode then do-            rsols <- fmap reverse $ liftIO $ readIORef sols-            if null rsols then do-              nsol' <- liftIO $ readIORef nsol-              stopWithMsg $ insuffsols (pick + numsols - nsol') ++ timeoutString-             else do-              aexprss <- mapM getsols rsols-              -- cexprss <- mapM (mapM (\(mi, e) -> lookupMeta mi >>= \mv -> withMetaInfo (getMetaInfo mv) $ abstractToConcrete_ e >>= \e' -> return (mi, e'))) aexprss-              cexprss <- forM aexprss $ do-                mapM $ \ (mi, e) -> do-                  mv <- lookupLocalMetaAuto mi-                  withMetaInfo (getMetaInfo mv) $ do-                    e' <- abstractToConcrete_ e-                    return (mi, e')-              let disp [(_, cexpr)] = prettyShow cexpr-                  disp cexprs = concat $ for cexprs $ \ (mi, cexpr) ->-                    maybe (show mi) show (lookup mi riis)-                      ++ " := " ++ prettyShow cexpr ++ " "-              ticks <- liftIO $ readIORef ticks-              stopWithMsg $ "Listing solution(s) " ++ show pick ++ "-" ++ show (pick + length rsols - 1) ++ timeoutString ++-                        "\n" ++ unlines (zipWith (\x y -> show y ++ "  " ++ disp x) cexprss [pick..])-           else {- not listmode -}-            case res of-             Nothing -> do-              nsol' <- liftIO $ readIORef nsol-              stopWithMsg $ insuffsols (pick + numsols - nsol') ++ timeoutString-             Just depthreached -> do-              ticks <- liftIO $ readIORef ticks-              rsols <- liftIO $ readIORef sols-              case rsols of-                [] -> do-                  nsol' <- liftIO $ readIORef nsol-                  stopWithMsg $ insuffsols (pick + numsols - nsol')-                terms -> loop terms where-                  -- Andreas, 2015-05-17  Issue 1504-                  -- If giving a solution failed (e.g. ill-typed)-                  -- we could try the next one.-                  -- However, currently @terms@ is always a singleton list.-                  -- Thus, the following @loop@ is not doing something very-                  -- meaningful.-                  loop :: [[I.Term]] -> TCM AutoResult-                  loop [] = return $ AutoResult (Solutions []) (Just "")-                  loop (term : terms') = do-                    -- On exception, try next solution-                    flip catchError (\ e -> do reportSDoc "auto" 40 $ "Solution failed:" TCM.<?> TCM.prettyTCM e-                                               loop terms') $ do-                      exprs <- getsols term-                      reportSDoc "auto" 20 $ "Trying solution " TCM.<+> TCM.prettyTCM exprs-                      giveress <- forM exprs $ \ (mi, expr0) -> do-                        let expr = killRange expr0-                        case lookup mi riis of-                         Nothing ->-                          -- catchError-                           (giveExpr WithoutForce Nothing mi expr >> return (Nothing, Nothing))-                           -- (const retry)-                           -- (\_ -> return (Nothing, Just ("Failed to give expr for side solution of " ++ show mi)))-                         Just ii' -> do ae <- give WithoutForce ii' Nothing expr-                                        mv <- lookupLocalMetaAuto mi-                                        let scope = getMetaScope mv-                                        ce <- abstractToConcreteScope scope ae-                                        let cmnt = if ii' == ii then agsyinfo ticks else ""-                                        return (Just (ii', prettyShow ce ++ cmnt), Nothing)-                           -- Andreas, 2015-05-17, Issue 1504-                           -- When Agsy produces an ill-typed solution, return nothing.-                           -- TODO: try other solution.-                           -- `catchError` const retry -- (return (Nothing, Nothing))-                      let msg = if natSize exprs == 1 then-                                 Nothing-                                else-                                 Just $ "Also gave solution(s) for hole(s)" ++-                                         concatMap (\(mi', _) ->-                                          if mi' == mi then "" else (" " ++ case lookup mi' riis of {Nothing -> show mi'; Just ii -> show ii})-                                         ) exprs-                      let msgs = catMaybes $ msg : map snd giveress-                          msg' = unlines msgs <$ guard (not $ null msgs)-                      return $ AutoResult (Solutions $ mapMaybe fst giveress) msg'--     MCaseSplit -> do-      case thisdefinfo of-       Just (def, clause, True) ->-        case Map.elems tccons of-         [(m, mytype, mylocalVars, _)] | null eqcons -> do-          (ids, pats) <- constructPats cmap mi clause-          let ctx = zipWith (\(hid, id) t -> HI hid (id, t)) ids mylocalVars-          ticks <- liftIO $ newIORef 0-          let [rectyp'] = mymrectyp-          defdfv <- getdfv mi def-          myrecdef <- liftIO $ newIORef $ ConstDef {cdname = "", cdorigin = (Nothing, def), cdtype = rectyp', cdcont = Postulate, cddeffreevars = defdfv}-          sols <- liftIO $ System.Timeout.timeout (getTimeOut timeout * 1000) (-             let r d = do-                  sols <- liftIO $ caseSplitSearch ticks __IMPOSSIBLE__ myhints meqr __IMPOSSIBLE__ d myrecdef ctx mytype pats-                  case sols of-                   [] -> r (d + costIncrease)-                   (_:_) -> return sols-             in r 0)-          case sols of-           Just (cls : _) -> withInteractionId ii $ do-            cls' <- liftIO $ runExceptT (mapM frommyClause cls)-            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 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 wm-              moduleTel <- lookupSection (AN.qnameModule def)-              pcs <- withInteractionId ii $ inTopContext $ addContext moduleTel $ mapM prettyA cls''-              ticks <- liftIO $ readIORef ticks---              return $ AutoResult (FunClauses $ map (insertAbsurdPattern . PP.renderStyle (PP.style { PP.mode = PP.OneLineMode })) pcs) Nothing--           Just [] -> stopWithMsg "No solution found" -- case not possible at the moment because case split doesnt care about search exhaustiveness-           Nothing -> stopWithMsg $ "No solution found at time out (" ++ show timeout ++ "s)"-         _ -> stopWithMsg "Metavariable dependencies not allowed in case split mode"-       _ -> stopWithMsg "Metavariable is not at top level of clause RHS"--     MRefine listmode -> do-      mv <- lookupLocalMetaAuto mi-      let tt = jMetaType $ mvJudgement mv-          minfo = getMetaInfo mv-      targettyp <- withMetaInfo minfo $ do-       vs <- getContextArgs-       targettype <- tt `piApplyM` permute (takeP (length vs) $ mvPermutation mv) vs-       normalise targettype-      let tctx = length $ envContext $ clEnv minfo--      hits <- if "-a" `elem` hints then do-        st <- liftTCM $ join $ pureTCM $ \st _ -> return st-        let defs    = st ^. stSignature . sigDefinitions-            idefs   = st ^. stImports   . sigDefinitions-            alldefs = HMap.keys defs ++ HMap.keys idefs-        catMaybes <$> mapM (\n ->-          case thisdefinfo of-           Just (def, _, _) | def == n -> return Nothing-           _ -> do-            cn <- withMetaInfo minfo $ runAbsToCon $ toConcrete n-            if C.isInScope cn == C.NotInScope then-              return Nothing-            else getConstInfo' n >>= \case-              Left{} -> return Nothing-              Right c -> do-                ctyp <- normalise $ defType c-                cdfv <- withMetaInfo minfo $ getDefFreeVars n-                return $ case matchType cdfv tctx ctyp targettyp of-                  Nothing -> Nothing-                  Just score -> Just (prettyShow cn, score)-         ) alldefs-       else do-        let scopeinfo = clScope (getMetaInfo mv)-            namespace = Scope.everythingInScope scopeinfo-            names = Scope.nsNames namespace-            qnames = map (\(x, y) -> (x, Scope.anameName $ List1.head y)) $ Map.toList names-            modnames = case thisdefinfo of-                        Just (def, _, _) -> filter (\(_, n) -> n /= def) qnames-                        Nothing -> qnames-        catMaybes <$> mapM (\(cn, n) -> getConstInfo' n >>= \case-          Left{} -> return Nothing-          Right c -> do-            ctyp <- normalise $ defType c-            cdfv <- withMetaInfo minfo $ getDefFreeVars n-            return $ case matchType cdfv tctx ctyp targettyp of-              Nothing -> Nothing-              Just score -> Just (prettyShow cn, score)-         ) modnames--      let sorthits = List.sortBy (\(_, (pa1, pb1)) (_, (pa2, pb2)) -> case compare pa2 pa1 of {EQ -> compare pb1 pb2; o -> o}) hits-      if listmode || pick == (-1) then-        let pick' = max 0 pick-        in if pick' >= length sorthits then-             stopWithMsg $ insuffcands $ length sorthits-            else-             let showhits = take 10 $ drop pick' sorthits-             in stopWithMsg $ "Listing candidate(s) " ++ show pick' ++ "-" ++ show (pick' + length showhits - 1) ++ " (found " ++ show (length sorthits) ++ " in total)\n" ++-                           unlines (zipWith (\i (cn, _) -> show i ++ "  " ++ cn) [pick'..pick' + length showhits - 1] showhits)-       else-        if pick >= length sorthits then-         stopWithMsg $ insuffcands $ length sorthits-        else-         return $ AutoResult (Refinement $ fst $ sorthits !! pick) Nothing-  where-    agsyinfo ticks = ""---- Get the functions and axioms defined in the same module as @def@.-autohints :: AutoHintMode -> I.MetaId -> Maybe AN.QName -> TCM [Hint]-autohints AHMModule mi (Just def) = do-  scope <- clScope . getMetaInfo <$> lookupLocalMetaAuto mi-  let names     = Scope.nsNames $ Scope.everythingInScope scope-      qnames    = map (Scope.anameName . List1.head) $ Map.elems names-      modnames  = filter (\n -> AN.qnameModule n == AN.qnameModule def && n /= def) qnames-  map (Hint False) <$> do-    (`filterM` modnames) $ \ n -> getConstInfo' n >>= \case-      Left{} -> return False-      Right c -> case theDef c of-        Axiom{}    -> return True-        AbstractDefn{} -> return True-        Function{} -> return True-        _          -> return False--autohints _ _ _ = return []------ | Names for the equality reasoning combinators---   Empty if any of these names is not defined.--getEqCombinators :: InteractionId -> Range -> TCM [Hint]-getEqCombinators ii rng = do-  let eqCombinators = ["_≡_", "begin_", "_≡⟨_⟩_", "_∎", "sym", "cong"]-  raw <- mapM (parseExprIn ii rng) eqCombinators `catchError` const (pure [])-  return $ fromMaybe [] $ mapM getHeadAsHint raw---- | Templates for error messages--genericNotEnough :: String -> Int -> String-genericNotEnough str n = unwords $ case n of-  0 -> ["No", str, "found"]-  1 -> ["Only 1", str, "found"]-  _ -> ["Only", show n, str ++ "s", "found"]--insuffsols :: Int -> String-insuffsols  = genericNotEnough "solution"--insuffcands :: Int -> String-insuffcands = genericNotEnough "candidate"

@@ -1,668 +0,0 @@--module Agda.Auto.CaseSplit where--import Prelude hiding ((!!))--import Control.Monad.State as St hiding (lift)-import Control.Monad.Reader as Rd hiding (lift)-import qualified Control.Monad.State as St-import Control.Monad.IO.Class ( MonadIO(..) )--import Data.Function (on)-import Data.IORef-import Data.Tuple (swap)-import Data.List (elemIndex)--- Import of <> needed for 8.2.2, but redundant in 8.8.3-import Data.Monoid ((<>), Sum(..))-import qualified Data.Set    as Set-import qualified Data.IntMap as IntMap--import Agda.Syntax.Common (Hiding(..))-import Agda.Auto.NarrowingSearch-import Agda.Auto.Syntax--import Agda.Auto.SearchControl-import Agda.Auto.Typecheck--import Agda.Utils.Impossible-import Agda.Utils.Monad (or2M)-import Agda.Utils.List ((!!), last1)--abspatvarname :: String-abspatvarname = "\0absurdPattern"--costCaseSplitVeryHigh, costCaseSplitHigh, costCaseSplitLow, costAddVarDepth-  :: Cost-costCaseSplitVeryHigh = 10000-costCaseSplitHigh     = 5000-costCaseSplitLow      = 2000-costAddVarDepth       = 1000--data HI a = HI Hiding a--drophid :: [HI a] -> [a]-drophid = map (\(HI _ x) -> x)--type CSPat o = HI (CSPatI o)-type CSCtx o = [HI (MId, MExp o)]--data CSPatI o = CSPatConApp (ConstRef o) [CSPat o]-              | CSPatProj (ConstRef o)-              | CSPatVar Nat-              | CSPatExp (MExp o)-              | CSWith (MExp o) -- always an App-              | CSAbsurd--              | CSOmittedArg-type Sol o = [(CSCtx o, [CSPat o], Maybe (MExp o))]--caseSplitSearch ::-  forall o . IORef Int -> Int -> [ConstRef o] ->-  Maybe (EqReasoningConsts o) -> Int -> Cost -> ConstRef o ->-  CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]-caseSplitSearch ticks nsolwanted chints meqr depthinterval depth recdef ctx tt pats = do- let branchsearch :: Cost -> CSCtx o -> MExp o ->-                     ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))-     branchsearch depth ctx tt termcheckenv = do--      nsol <- newIORef 1-      m <- initMeta-      sol <- newIORef Nothing-      let trm = Meta m-          hsol = do trm' <- expandMetas trm-                    writeIORef sol (Just trm')-          initcon = mpret-                  $ Sidecondition-                    (localTerminationSidecond termcheckenv recdef trm)-                  $ (case meqr of-                        Nothing  -> id-                        Just eqr -> mpret . Sidecondition (calcEqRState eqr trm)-                     ) $ tcSearch False (map (fmap closify) (drophid ctx))-                         (closify tt) trm-      recdefd <- readIORef recdef-      let env = RIEnv { rieHints = (recdef, HMRecCall) : map (, HMNormal) chints-                      , rieDefFreeVars = cddeffreevars recdefd-                      , rieEqReasoningConsts = meqr-                      }-      depreached <- topSearch ticks nsol hsol env initcon depth (depth + 1)-      readIORef sol-     ctx' = ff 1 ctx-     ff _ [] = []-     ff n (HI hid (id, t) : ctx) = HI hid (id, lift n t) : ff (n + 1) ctx- caseSplitSearch' branchsearch depthinterval depth recdef ctx' tt pats--caseSplitSearch' :: forall o .-  (Cost -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))) ->-  Int -> Cost -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]-caseSplitSearch' branchsearch depthinterval depth recdef ctx tt pats = do-  recdefd <- readIORef recdef-  rc depth (cddeffreevars recdefd) ctx tt pats- where-  rc :: Cost -> Int -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]-  rc depth _ _ _ _ | depth < 0 = return []-  rc depth nscrutavoid ctx tt pats = do--    mblkvar <- getblks tt-    fork-     mblkvar-   where-   fork :: [Nat] -> IO [Sol o]-   fork mblkvar = do-    sols1 <- dobody-    case sols1 of-     (_:_) -> return sols1-     [] -> do-      let r :: [Nat] -> IO [Sol o]-          r [] = return []-          r (v:vs) = do-           sols2 <- splitvar mblkvar v-           case sols2 of-            (_:_) -> return sols2-            [] -> r vs-      r [nv - x | x <- [0..nv]] -- [0..length ctx - 1 - nscrutavoid]-    where nv = length ctx - 1-   dobody :: IO [Sol o]-   dobody = do-    case findperm (map snd (drophid ctx)) of-     Just perm -> do-      let (ctx', tt', pats') = applyperm perm ctx tt pats-      res <- branchsearch depth ctx' tt' (localTerminationEnv pats')-      return $ case res of-       Just trm -> [[(ctx', pats', Just trm)]]-       Nothing -> []-     Nothing -> __IMPOSSIBLE__ -- no permutation found-   splitvar :: [Nat] -> Nat -> IO [Sol o]-   splitvar mblkvar scrut = do-    let scruttype = infertypevar ctx scrut-    case rm __IMPOSSIBLE__ scruttype of-     App _ _ (Const c) _ -> do-      cd <- readIORef c-      case cdcont cd of-       Datatype cons _ -> do-         sols <- dobranches cons-         return $ map (\sol -> case sol of-          [] ->-           case findperm (map snd (drophid ctx)) of-            Just perm ->-             let HI scrhid(_, scrt) = ctx !! scrut-                 ctx1 = take scrut ctx ++ (HI scrhid (Id abspatvarname, scrt)) : drop (scrut + 1) ctx-                 (ctx', _, pats') = applyperm perm ctx1 tt ({-map (replacep scrut 1 CSAbsurd __IMPOSSIBLE__) -}pats)-             in [(ctx', pats', Nothing)]-            Nothing -> __IMPOSSIBLE__ -- no permutation found-          _ -> sol-          ) sols-        where-         dobranches :: [ConstRef o] -> IO [Sol o]-         dobranches [] = return [[]]-         dobranches (con : cons) = do-          cond <- readIORef con-          let ff t = case rm __IMPOSSIBLE__ t of-                        Pi _ h _ it (Abs id ot) ->-                         let (xs, inft) = ff ot-                         in (((h, scrut + length xs), id, lift (scrut + length xs + 1) it) : xs, inft)-                        _ -> ([], lift scrut t)-              (newvars, inftype) = ff (cdtype cond)-              constrapp = NotM $ App Nothing (NotM OKVal) (Const con) (foldl (\xs ((h, v), _, _) -> NotM $ ALCons h (NotM $ App Nothing (NotM OKVal) (Var v) (NotM ALNil)) xs) (NotM ALNil) (reverse newvars))-              pconstrapp = CSPatConApp con (map (\((hid, v), _, _) -> HI hid (CSPatVar v)) newvars)-              thesub = replace scrut (length newvars) constrapp-              Id newvarprefix = fst $ (drophid ctx) !! scrut-              ctx1 = map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (take scrut ctx) ++-                     reverse (zipWith (\((hid, _), id, t) i ->-                       HI hid (Id (case id of {NoId -> newvarprefix{- ++ show i-}; Id id -> id}), t)-                      ) newvars [0..]) ++-                     map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (drop (scrut + 1) ctx)-              tt' = thesub tt-              pats' = map (replacep scrut (length newvars) pconstrapp constrapp) pats-              scruttype' = thesub scruttype  -- scruttype shouldn't really refer to scrutvar so lift is enough, but what if circular ref has been created and this is not detected until case split is done-          case unifyexp inftype scruttype' of-           Nothing -> do-            res <- notequal scrut (length newvars) scruttype' inftype-            if res then -- branch absurd-              dobranches cons-             else -- branch dont know-              return []-           Just unif ->-            do-             let (ctx2, tt2, pats2) = removevar ctx1 tt' pats' unif-                 --cost = if elem scrut mblkvar then costCaseSplit - (costCaseSplit - costCaseSplitFollow) `div` (length mblkvar) else costCaseSplit-                 cost-                   | null mblkvar && scrut < length ctx - nscrutavoid && nothid-                                                                = costCaseSplitLow +-                                                                  costAddVarDepth *-                                                                  Cost (depthofvar scrut pats)-                   | null mblkvar                               = costCaseSplitVeryHigh-                   | scrut `elem` mblkvar                       = costCaseSplitLow-                   | scrut < length ctx - nscrutavoid && nothid = costCaseSplitHigh-                   | otherwise                                  = costCaseSplitVeryHigh--                 nothid = let HI hid _ = ctx !! scrut-                          in hid == NotHidden---             sols <- rc (depth - cost) (length ctx - 1 - scrut) ctx2 tt2 pats2-             case sols of-              [] -> return []-              _ -> do-               sols2 <- dobranches cons-               return $ concatMap (\sol -> map (\sol2 -> sol ++ sol2) sols2) sols-       _ -> return [] -- split failed "scrut type is not datatype"-     _ -> return [] -- split failed "scrut type is not datatype"--infertypevar :: CSCtx o -> Nat -> MExp o-infertypevar ctx v = snd $ (drophid ctx) !! v--class Replace t u where-  type ReplaceWith t u-  replace' :: Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u--replace :: Replace t u => Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u-replace sv nnew e t = replace' 0 e t `runReader` (sv, nnew)--instance Replace t u => Replace (Abs t) (Abs u) where-  type ReplaceWith (Abs t) (Abs u) = ReplaceWith t u-  replace' n re (Abs mid b) = Abs mid <$> replace' (n + 1) re b--instance Replace (Exp o) (MExp o) where-  type ReplaceWith (Exp o) (MExp o) = o-  replace' n re = \case-    App uid ok elr@(Var v) args -> do-      ih         <- NotM <$> replace' n re args-      (sv, nnew) <- ask-      return $-        if v >= n-        then if v - n == sv-             then betareduce (lift n re) ih-             else if v - n > sv-                  then NotM $ App uid ok (Var (v + nnew - 1)) ih-                  else NotM $ App uid ok elr ih-        else NotM $ App uid ok elr ih-    App uid ok elr@Const{} args ->-      NotM . App uid ok elr . NotM <$> replace' n re args-    Lam hid b -> NotM . Lam hid <$> replace' (n + 1) re b-    Pi uid hid possdep it b ->-      fmap NotM $ Pi uid hid possdep <$> replace' n re it <*> replace' n re b-    e@Sort{} -> return $ NotM e-    e@AbsurdLambda{} -> return $ NotM e--instance Replace t u => Replace (MM t (RefInfo o)) u where-  type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u-  replace' n re = replace' n re . rm __IMPOSSIBLE__--instance Replace (ArgList o) (ArgList o) where-  type ReplaceWith (ArgList o) (ArgList o) = o-  replace' n re args = case args of-    ALNil           -> return ALNil-    ALCons hid a as ->-      ALCons hid <$> replace' n re a <*> (NotM <$> replace' n re as)-    ALProj{}        -> __IMPOSSIBLE__-    ALConPar as     -> ALConPar . NotM <$> replace' n re as---betareduce :: MExp o -> MArgList o -> MExp o-betareduce e args = case rm __IMPOSSIBLE__ args of- ALNil -> e- ALCons _ a rargs -> case rm __IMPOSSIBLE__ e of-  App uid ok elr eargs -> NotM $ App uid ok elr (concatargs eargs args)-  Lam _ (Abs _ b) -> betareduce (replace 0 0 a b) rargs-  _ -> __IMPOSSIBLE__ -- not type correct if this happens- ALProj{} -> __IMPOSSIBLE__- ALConPar as -> __IMPOSSIBLE__--concatargs :: MArgList o -> MArgList o -> MArgList o-concatargs xs ys = case rm __IMPOSSIBLE__ xs of-  ALNil -> ys--  ALCons hid x xs -> NotM $ ALCons hid x (concatargs xs ys)--  ALProj{} -> __IMPOSSIBLE__--  ALConPar as -> NotM $ ALConPar (concatargs xs ys)--replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o-replacep sv nnew rp re = r- where-  r :: CSPat o -> CSPat o-  r (HI hid (CSPatConApp c ps)) = HI hid (CSPatConApp c (map r ps))-  r (HI hid (CSPatVar v)) | v == sv   = HI hid rp-                          | v > sv    = HI hid (CSPatVar (v + nnew - 1))-                          | otherwise = HI hid (CSPatVar v)-  r (HI hid (CSPatExp e)) = HI hid (CSPatExp $ replace sv nnew re e)--  r p@(HI _ CSOmittedArg) = p--  r _ = __IMPOSSIBLE__ -- other constructors dont appear in indata Pats------ Unification takes two values of the same type and generates a list--- of assignments making the two terms equal.--type Assignments o = [(Nat, Exp o)]--class Unify t where-  type UnifiesTo t-  unify'    :: t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()-  notequal' :: t -> t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool--unify :: Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))-unify t u = unify' t u `execStateT` []--notequal :: Unify t => Nat -> Nat -> t -> t -> IO Bool-notequal fstnew nbnew t1 t2 = notequal' t1 t2 `runReaderT` (fstnew, nbnew)-                                              `evalStateT` []--instance (Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o)) where-  type UnifiesTo (MM t (RefInfo o)) = o--  unify' = unify' `on` rm __IMPOSSIBLE__--  notequal' = notequal' `on` rm __IMPOSSIBLE__--unifyVar :: Nat -> Exp o -> StateT (Assignments o) Maybe ()-unifyVar v e = do-  unif <- get-  case lookup v unif of-    Nothing -> modify ((v, e) :)-    Just e' -> unify' e e'--instance Unify t => Unify (Abs t) where-  type UnifiesTo (Abs t) = UnifiesTo t-  unify' (Abs _ b1) (Abs _ b2) = unify' b1 b2--  notequal' (Abs _ b1) (Abs _ b2) = notequal' b1 b2--instance Unify (Exp o) where-  type UnifiesTo (Exp o) = o--  unify' e1 e2 = case (e1, e2) of-   (App _ _ elr1 args1, App _ _ elr2 args2) | elr1 == elr2 -> unify' args1 args2-   (Lam hid1 b1, Lam hid2 b2)               | hid1 == hid2 -> unify' b1 b2-   (Pi _ hid1 _ a1 b1, Pi _ hid2 _ a2 b2)   | hid1 == hid2 -> unify' a1 a2-                                                           >> unify' b1 b2-   (Sort _, Sort _) -> return () -- a bit sloppy-   (App _ _ (Var v) (NotM ALNil), _)-     | v `Set.member` (freeVars e2) -> St.lift Nothing -- Occurs check-   (_, App _ _ (Var v) (NotM ALNil))-     | v `Set.member` (freeVars e1) -> St.lift Nothing -- Occurs check-   (App _ _ (Var v) (NotM ALNil), _) -> unifyVar v e2-   (_, App _ _ (Var v) (NotM ALNil)) -> unifyVar v e1-   _ -> St.lift Nothing--  notequal' e1 e2 = do-    (fstnew, nbnew) <- ask-    unifier         <- get-    case (e1, e2) of-      (App _ _ elr1 es1, App _ _ elr2 es2) | elr1 == elr2 -> notequal' es1 es2-      (_, App _ _ (Var v2) (NotM ALNil)) -- why is this not symmetric?!-        | fstnew <= v2 && v2 < fstnew + nbnew ->-        case lookup v2 unifier of-          Nothing  -> modify ((v2, e1):) >> return False-          Just e2' -> notequal' e1 e2'-{--  GA: Skipped these: Not sure why we'd claim they're impossible-      (_, App _ _ (Var v2) (NotM ALProj{})) -> __IMPOSSIBLE__-      (_, App _ _ (Var v2) (NotM ALConPar{})) -> __IMPOSSIBLE__--}-      (App _ _ (Const c1) es1, App _ _ (Const c2) es2) -> do-        cd1 <- liftIO $ readIORef c1-        cd2 <- liftIO $ readIORef c2-        case (cdcont cd1, cdcont cd2) of-          (Constructor{}, Constructor{}) -> if c1 == c2 then notequal' es1 es2-                                            else return True-          _ -> return False-{- GA: Why don't we have a case for distinct heads after all these-       unification cases for vars with no spines & metas that can-       be looked up?-      (App _ _ elr1 _, App _ _ elr2 _) | elr1 <> elr2 -> return True--}-      _ -> return False--instance Unify (ArgList o) where-  type UnifiesTo (ArgList o) = o--  unify' args1 args2 = case (args1, args2) of-   (ALNil, ALNil) -> pure ()-   (ALCons hid1 a1 as1, ALCons hid2 a2 as2) | hid1 == hid2 -> unify' a1 a2-                                                           >> unify' as1 as2-   (ALConPar as1, ALCons _ _ as2) -> unify' as1 as2-   (ALCons _ _ as1, ALConPar as2) -> unify' as1 as2-   (ALConPar as1, ALConPar as2)   -> unify' as1 as2-   _ -> St.lift Nothing--  notequal' args1 args2 = case (args1, args2) of-    (ALCons _ e es, ALCons _ f fs) -> notequal' e f `or2M` notequal' es fs-    (ALConPar es1, ALConPar es2)   -> notequal' es1 es2-    _                              -> return False---- This definition is only here to respect the previous interface.-unifyexp :: MExp o -> MExp o -> Maybe ([(Nat, MExp o)])-unifyexp e1 e2 = fmap (NotM <$>) <$> unify e1 e2--class Lift t where-  lift' :: Nat -> Nat -> t -> t--lift :: Lift t => Nat -> t -> t-lift 0 = id-lift n = lift' n 0--instance Lift t => Lift (Abs t) where-  lift' n j (Abs mid b) = Abs mid (lift' n (j + 1) b)--instance Lift t => Lift (MM t r) where-  lift' n j = NotM . lift' n j . rm __IMPOSSIBLE__--instance Lift (Exp o) where-  lift' n j = \case-    App uid ok elr args -> case elr of-      Var v | v >= j -> App uid ok (Var (v + n)) (lift' n j args)-      _ -> App uid ok elr (lift' n j args)-    Lam hid b -> Lam hid (lift' n j b)-    Pi uid hid possdep it b -> Pi uid hid possdep (lift' n j it) (lift' n j b)-    e@Sort{} -> e-    e@AbsurdLambda{} -> e--instance Lift (ArgList o) where-  lift' n j args = case args of-    ALNil           -> ALNil-    ALCons hid a as -> ALCons hid (lift' n j a) (lift' n j as)-    ALProj{}        -> __IMPOSSIBLE__-    ALConPar as     -> ALConPar (lift' n j as)---removevar :: CSCtx o -> MExp o -> [CSPat o] -> [(Nat, MExp o)] -> (CSCtx o, MExp o, [CSPat o])-removevar ctx tt pats [] = (ctx, tt, pats)-removevar ctx tt pats ((v, e) : unif) =- let-  e2 = replace v 0 __IMPOSSIBLE__ {- occurs check failed -} e-  thesub = replace v 0 e2-  ctx1 = map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (take v ctx) ++-         map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (drop (v + 1) ctx)-  tt' = thesub tt-  pats' = map (replacep v 0 (CSPatExp e2) e2) pats-  unif' = map (\(uv, ue) -> (if uv > v then uv - 1 else uv, thesub ue)) unif- in-  removevar ctx1 tt' pats' unif'--findperm :: [MExp o] -> Maybe [Nat]-findperm ts =- let-  frees = map freevars ts-  m = IntMap.fromList $-      map (\i -> (i, length (filter (elem i) frees)))-          [0..length ts - 1]-  r _ perm 0 = Just $ reverse perm-  r m perm n =-   case lookup 0 (map swap (IntMap.toList m)) of-    Nothing -> Nothing-    Just i -> r (foldl (flip $ IntMap.adjust (subtract 1))-                       (IntMap.insert i (-1) m)-                       (frees !! i))-                 (i : perm) (n - 1)- in r m [] (length ts)---freevars :: FreeVars t => t -> [Nat]-freevars = Set.toList . freeVars--applyperm :: [Nat] -> CSCtx o -> MExp o -> [CSPat o] ->-             (CSCtx o, MExp o, [CSPat o])-applyperm perm ctx tt pats =- let ctx1 = map (\(HI hid (id, t)) -> HI hid (id, rename (ren perm) t)) ctx-     ctx2 = map (\i -> ctx1 !! i) perm-     ctx3 = seqctx ctx2-     tt' = rename (ren perm) tt-     pats' = map (rename (ren perm)) pats- in (ctx3, tt', pats')--ren :: [Nat] -> Nat -> Int-ren n i = let Just j = elemIndex i n in j--instance Renaming t => Renaming (HI t) where-  renameOffset j ren (HI hid t) = HI hid $ renameOffset j ren t--instance Renaming (CSPatI o) where-  renameOffset j ren = \case-    CSPatConApp c pats -> CSPatConApp c $ map (renameOffset j ren) pats-    CSPatVar i         -> CSPatVar $ j + ren i-    CSPatExp e         -> CSPatExp $ renameOffset j ren e-    e@CSOmittedArg     -> e-    _                  -> __IMPOSSIBLE__--seqctx :: CSCtx o -> CSCtx o-seqctx = r (-1)- where-  r _ [] = []-  r n (HI hid (id, t) : ctx) = HI hid (id, lift n t) : r (n - 1) ctx--- ----------------------depthofvar :: Nat -> [CSPat o] -> Nat-depthofvar v pats =- let [depth] = concatMap (f 0) (drophid pats)-     f d (CSPatConApp _ pats) = concatMap (f (d + 1)) (drophid pats)-     f d (CSPatVar v') = [d | v == v']-     f _ _ = []- in depth---- ----------------------- | Speculation: Type class computing the size (?) of a pattern---   and collecting the vars it introduces-class LocalTerminationEnv a where-  sizeAndBoundVars :: a -> (Sum Nat, [Nat])--instance LocalTerminationEnv a => LocalTerminationEnv (HI a) where-  sizeAndBoundVars (HI _ p) = sizeAndBoundVars p--instance LocalTerminationEnv (CSPatI o) where-  sizeAndBoundVars = \case-    CSPatConApp _ ps -> (1, []) <> sizeAndBoundVars ps-    CSPatVar n       -> (0, [n])-    CSPatExp e       -> sizeAndBoundVars e-    _                -> (0, [])--instance LocalTerminationEnv a => LocalTerminationEnv [a] where-  sizeAndBoundVars = foldMap sizeAndBoundVars--instance LocalTerminationEnv (MExp o) where---  sizeAndBoundVars e = case rm __IMPOSSIBLE__ e of--- GA: 2017 06 27: Not actually impossible! (cf. #2620)-  sizeAndBoundVars Meta{} = (0, [])--- Does this default behaviour even make sense? The catchall in the--- following match seems to suggest it does-  sizeAndBoundVars (NotM e) = case e of-    App _ _ (Var v) _      -> (0, [v])-    App _ _ (Const _) args -> (1, []) <> sizeAndBoundVars args-    _                      -> (0, [])--instance (LocalTerminationEnv a, LocalTerminationEnv b) => LocalTerminationEnv (a, b) where-  sizeAndBoundVars (a, b) = sizeAndBoundVars a <> sizeAndBoundVars b--instance LocalTerminationEnv (MArgList o) where-  sizeAndBoundVars as = case rm __IMPOSSIBLE__ as of-    ALNil         -> (0, [])-    ALCons _ a as -> sizeAndBoundVars (a, as)-    ALProj{}      -> __IMPOSSIBLE__-    ALConPar as   -> sizeAndBoundVars as----- | Take a list of patterns and returns (is, size, vars) where (speculation):----  * the is are the pattern indices the vars are contained in---   * size is total number of constructors removed (?) to access vars-localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])-localTerminationEnv pats = (is, getSum s, vs) where--  (is , s , vs) = g 0 pats--  g :: Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])-  g _ [] = ([], 0, [])-  g i (hp@(HI _ p) : ps) = case p of-    CSPatConApp{} -> let (size, vars) = sizeAndBoundVars hp-                     in ([i], size, vars) <> g (i + 1) ps-    _ -> g (i + 1) ps--localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)-localTerminationSidecond (is, size, vars) reccallc b =-  ok b- where-     ok e = mmpcase (False, prioNo, Nothing) e $ \e -> case e of-      App _ _ elr args -> mpret $ Sidecondition-       (oks args)-       (case elr of-          Const c | c == reccallc -> if size == 0 then mpret (Error "localTerminationSidecond: no size to decrement") else okcall 0 size vars args-          _ -> mpret OK-       )-      Lam _ (Abs _ e) -> ok e-      Pi _ _ _ it (Abs _ ot) -> mpret $ Sidecondition-       (ok it)-       (ok ot)-      Sort{} -> mpret OK--      AbsurdLambda{} -> mpret OK---     oks as = mmpcase (False, prioNo, Nothing) as $ \as -> case as of-      ALNil -> mpret OK-      ALCons _ a as -> mpret $ Sidecondition-       (ok a)-       (oks as)--      ALProj eas _ _ as -> mpret $ Sidecondition (oks eas) (oks as)---      ALConPar as -> oks as--     okcall i size vars as = mmpcase (False, prioNo, Nothing) as $ \as -> case as of-      ALNil -> mpret OK-      ALCons _ a as | i `elem` is ->-       mbpcase prioNo Nothing (he size vars a) $ \x -> case x of-        Nothing -> mpret $ Error "localTerminationSidecond: reccall not ok"-        Just (size', vars') -> okcall (i + 1) size' vars' as-      ALCons _ a as -> okcall (i + 1) size vars as--      ALProj{} -> mpret OK---      ALConPar as -> __IMPOSSIBLE__--     he size vars e = mmcase e $ \e -> case e of-      App _ _ (Var v) _ ->-       case remove v vars of-        Nothing -> mbret Nothing-        Just vars' -> mbret $ Just (size, vars')-      App _ _ (Const c) args -> do-       cd <- readIORef c-       case cdcont cd of-        Constructor{} ->-         if size == 1 then-          mbret Nothing-         else-          hes (size - 1) vars args-        _ -> mbret Nothing-      _ -> mbret Nothing-     hes size vars as = mmcase as $ \as -> case as of-      ALNil -> mbret $ Just (size, vars)-      ALCons _ a as ->-       mbcase (he size vars a) $ \x -> case x of-        Nothing -> mbret Nothing-        Just (size', vars') -> hes size' vars' as--      ALProj{} -> __IMPOSSIBLE__---      ALConPar as -> __IMPOSSIBLE__--     remove _ [] = Nothing-     remove x (y : ys) | x == y = Just ys-     remove x (y : ys) = case remove x ys of {Nothing -> Nothing; Just ys' -> Just (y : ys')}---- ------------------------------getblks :: MExp o -> IO [Nat]-getblks tt = do- NotB (hntt, blks) <- hnn_blks (Clos [] tt)- case f blks of-  Just v -> return [v]-  Nothing -> case rawValue hntt of-   HNApp (Const c) args -> do-    cd <- readIORef c-    case cdcont cd of-     Datatype{} -> g [] args-     _ -> return []-   _ -> return []- where-  f blks = case blks of-             (b : bs) -> case rawValue (last1 b bs) of-              HNApp (Var v) _ -> Just v-              _ -> Nothing-             _ -> Nothing-  g vs args = do-   NotB hnargs <- hnarglist args-   case hnargs of-    HNALCons _ a as -> do-     NotB (_, blks) <- hnn_blks a-     let vs' = case f blks of-                Just v | v `notElem` vs -> v : vs-                _ -> vs-     g vs' as-    _ -> return vs--- ---------------------------

@@ -1,788 +0,0 @@--module Agda.Auto.Convert where--import Prelude hiding ((!!))--import Control.Monad          ( when )-import Control.Monad.Except-import Control.Monad.IO.Class ( MonadIO(..) )-import Control.Monad.State--import Data.Bifunctor (first)-import Data.IORef-import Data.Maybe (catMaybes)-import Data.Map (Map)-import qualified Data.Map as Map--import Agda.Syntax.Common (Hiding(..), getHiding, Arg)-import Agda.Syntax.Concrete (exprFieldA)-import qualified Agda.Syntax.Internal as I-import Agda.Syntax.Internal (Dom'(..),domInfo,unDom)-import qualified Agda.Syntax.Internal.Pattern as IP-import qualified Agda.Syntax.Common as Cm-import qualified Agda.Syntax.Abstract.Name as AN-import qualified Agda.Syntax.Abstract as A-import qualified Agda.Syntax.Position as SP--import qualified Agda.TypeChecking.Monad.Base as MB--import Agda.TypeChecking.Monad.Signature (getConstInfo, getDefFreeVars, ignoreAbstractMode)-import Agda.TypeChecking.Level (reallyUnLevelView)-import Agda.TypeChecking.Monad.Base (mvJudgement, mvPermutation, getMetaInfo, envContext, clEnv)-import Agda.TypeChecking.Monad.MetaVars-  (lookupMeta, withMetaInfo, lookupInteractionPoint)-import Agda.TypeChecking.Monad.Context (getContextArgs)-import Agda.TypeChecking.Monad.Constraints (getAllConstraints)-import Agda.TypeChecking.Substitute (applySubst, renamingR)-import Agda.TypeChecking.Telescope (piApplyM)-import qualified Agda.TypeChecking.Substitute as I (absBody)-import Agda.TypeChecking.Reduce (normalise, instantiate)-import Agda.TypeChecking.EtaContract (etaContract)-import Agda.TypeChecking.Monad.Builtin (constructorForm)-import Agda.TypeChecking.Free as Free (freeIn)--import Agda.Interaction.MakeCase (getClauseZipperForIP)--import Agda.Auto.NarrowingSearch-import Agda.Auto.Syntax hiding (getConst)--import Agda.Auto.CaseSplit hiding (lift)--import Agda.Utils.Either-import Agda.Utils.Lens-import Agda.Utils.List-import Agda.Utils.Monad       ( forMaybeMM )-import Agda.Utils.Permutation ( Permutation(Perm), permute, takeP, compactP )-import Agda.Syntax.Common.Pretty      ( prettyShow )--import Agda.Utils.Impossible---data Hint = Hint-  { hintIsConstructor :: Bool-  , hintQName         :: I.QName-  }--type O = (Maybe (Int, [Arg AN.QName]),AN.QName)-  -- Nothing - Def-  -- Just npar - Con with npar parameters which don't appear in Agda--data TMode = TMAll -- can be extended to distinguish between different modes (all, only def)- deriving Eq--type MapS a b = (Map a b, [a])--initMapS :: MapS a b-initMapS = (Map.empty, [])--popMapS :: (S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b)-popMapS r w = do (m, xs) <- gets r-                 case xs of-                  [] -> return Nothing-                  (x:xs) -> do-                   modify (w (m, xs))-                   return $ Just x--data S = S {sConsts :: MapS AN.QName (TMode, ConstRef O),-            sMetas :: MapS I.MetaId (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [I.MetaId]),-            sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O)),-            sCurMeta :: Maybe I.MetaId,-            sMainMeta :: I.MetaId-           }--type TOM = StateT S MB.TCM-type MOT = ExceptT String IO--tomy :: I.MetaId -> [Hint] -> [I.Type] ->-        MB.TCM ([ConstRef O]-               , [MExp O]-               , Map I.MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [I.MetaId])-               , [(Bool, MExp O, MExp O)]-               , Map AN.QName (TMode, ConstRef O))-tomy imi icns typs = do- eqs <- getEqs- let-  r :: [AN.QName] -> TOM [AN.QName]-  r projfcns = do-   nxt <- popMapS sConsts (\x y -> y {sConsts = x})-   case nxt of-    Just cn -> do-     cmap <- gets (fst . sConsts)-     let (mode, c) = cmap Map.! cn-     def <- lift $ getConstInfo cn-     let typ = MB.defType def-         defn = MB.theDef def-     typ <- lift $ normalise typ-     typ' <- convert typ-     let clausesToDef clauses = do-           clauses' <- convert clauses-           let narg = case clauses of-                        [] -> 0-                        I.Clause {I.namedClausePats = xs} : _ -> length xs-           return (Def narg clauses' Nothing Nothing, [])-     (cont, projfcns2) <- case defn of-      MB.Axiom {} -> return (Postulate, [])-      MB.DataOrRecSig{} -> return (Postulate, [])-      MB.GeneralizableVar{} -> __IMPOSSIBLE__-      MB.AbstractDefn{} -> return (Postulate, [])-      MB.Function {MB.funClauses = clauses} -> clausesToDef clauses-      -- MB.Primitive {MB.primClauses = []} -> throwError $ strMsg "Auto: Primitive functions are not supported" -- Andreas, 2013-06-17 breaks interaction/AutoMisc-      MB.Primitive {MB.primClauses = clauses} -> clausesToDef clauses-      MB.PrimitiveSort{} -> __IMPOSSIBLE__-      MB.Datatype {MB.dataCons = cons} -> do-       cons2 <- mapM (\con -> getConst True con TMAll) cons-       return (Datatype cons2 [], [])-      MB.Record {MB.recFields = fields, MB.recTel = tel} -> do -- the value of recPars seems unreliable or don't know what it signifies-       let pars n (I.El _ (I.Pi it typ)) = Cm.Arg (I.domInfo it) (I.var n) :-                                           pars (n - 1) (I.unAbs typ)-           pars _ (I.El _ _) = []-           contyp npar I.EmptyTel = I.El (I.mkType 0 {- arbitrary -}) $-                                      I.Def cn $ map I.Apply $ pars (npar - 1) typ-           contyp npar (I.ExtendTel it (I.Abs v tel)) = I.El (I.mkType 0 {- arbitrary -}) (I.Pi it (I.Abs v (contyp (npar + 1) tel)))-           contyp npar (I.ExtendTel it I.NoAbs{})     = __IMPOSSIBLE__-       contyp' <- convert $ contyp 0 tel-       cc <- lift $ liftIO $ readIORef c-       let Datatype [con] [] = cdcont cc-       lift $ liftIO $ modifyIORef con (\cdef -> cdef {cdtype = contyp'})--       projfcns <- mapM (\ dom -> getConst False (I.unDom dom) TMAll) fields-       -- Equivalently projfcns <- mapM (($ TMAll) . getConst False . I.unDom) fields--       return (Datatype [con] projfcns, []{-map snd fields-})-      MB.Constructor {MB.conData = dt} -> do-       _ <- getConst False dt TMAll -- make sure that datatype is included-       cc <- lift $ liftIO $ readIORef c-       let (Just (nomi,_), _) = cdorigin cc-       return (Constructor (nomi - cddeffreevars cc), [])-     lift $ liftIO $ modifyIORef c (\cdef -> cdef {cdtype = typ', cdcont = cont})-     r $ projfcns2 ++ projfcns-    Nothing -> do-     nxt <- popMapS sMetas (\x y -> y {sMetas = x})-     case nxt of-      Just mi -> do-       mapM_ (\((_, e, i), eqi) -> do-         when (fmExp mi e || fmExp mi i) $ do-          (eqsm, eqsl) <- gets sEqs-          when (Map.notMember eqi eqsm) $ do-           modify $ \s -> s {sEqs = (Map.insert eqi Nothing eqsm, eqi : eqsl)}-        ) (zip eqs [0..])-       mv <- lift $ lookupLocalMetaAuto mi-       msol <- case MB.mvInstantiation mv of-                     MB.InstV{} ->-                      lift $ withMetaInfo (getMetaInfo mv) $ do-                       args <- getContextArgs-                       --sol <- norm (I.MetaV mi args)-                       sol <- instantiate $ I.MetaV mi $ map I.Apply $ permute (takeP (length args) $ mvPermutation mv) args-                       return $ Just sol-                     _ -> return Nothing-       case msol of-        Nothing -> return ()-        Just sol -> do-         m <- getMeta mi-         sol' <- convert sol-         modify $ \s -> s {sEqs = first (Map.insert (Map.size (fst $ sEqs s)) (Just (False, Meta m, sol'))) (sEqs s)}-       let tt = MB.jMetaType $ mvJudgement mv-           minfo = getMetaInfo mv-           localVars = map (snd . I.unDom) . envContext . clEnv $ minfo-       (targettype, localVars) <- lift $ withMetaInfo minfo $ do-        vs <- getContextArgs-        targettype <- tt `piApplyM` permute (takeP (length vs) $ mvPermutation mv) vs-        targettype <- normalise targettype-        localVars <- mapM normalise localVars-        return (targettype, localVars)-       modify (\s -> s {sCurMeta = Just mi})-       typ' <- convert targettype-       ctx' <- mapM convert localVars-       modify (\s -> s {sCurMeta = Nothing})-       modify (\s -> s {sMetas = first (Map.adjust (\(m, _, deps) -> (m, Just (typ', ctx'), deps)) mi) (sMetas s)})-       r projfcns-      Nothing -> do-       nxt <- popMapS sEqs (\x y -> y {sEqs = x})-       case nxt of-        Just eqi -> do-         let (ineq, e, i) = eqs !! eqi-         e' <- convert e-         i' <- convert i-         modify (\s -> s {sEqs = first (Map.adjust (\_ -> Just (ineq, e', i')) eqi) (sEqs s)})-         r projfcns-        Nothing ->-         return projfcns- ((icns', typs'), s) <- runStateT-  (do _ <- getMeta imi-      icns' <- mapM (\ (Hint iscon name) -> getConst iscon name TMAll) icns-      typs' <- mapM convert typs-      projfcns <- r []-      projfcns' <- mapM (\name -> getConst False name TMAll) projfcns-      [] <- r []-      return (projfcns' ++ icns', typs')-  ) (S {sConsts = initMapS, sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = imi})- lift $ liftIO $ mapM_ categorizedecl icns'- return (icns', typs', Map.map flatten (fst (sMetas s)), map fromJust $ Map.elems (fst (sEqs s)), fst (sConsts s))- where- flatten (x, Just (y, z), w) = (x, y, z, w)- flatten (x, Nothing, w) = __IMPOSSIBLE__-- fromJust (Just x) = x- fromJust Nothing = __IMPOSSIBLE__--getConst :: Bool -> AN.QName -> TMode -> TOM (ConstRef O)-getConst iscon name mode = do- def <- lift $ getConstInfo name- case MB.theDef def of-  MB.Record {MB.recConHead = con} -> do-   let conname = I.conName con-       conflds = I.conFields con-   cmap <- gets (fst . sConsts)-   case Map.lookup name cmap of-    Just (mode', c) ->-     if iscon then do-      cd <- lift $ liftIO $ readIORef c-      let Datatype [con] _ = cdcont cd-      return con-     else-      return c-    Nothing -> do-     mainm <- gets sMainMeta-     dfv <- lift $ getdfv mainm name-     let nomi = I.arity (MB.defType def)-     ccon <- lift $ liftIO $ newIORef (ConstDef {cdname = prettyShow name ++ ".CONS", cdorigin = (Just (nomi,conflds), conname), cdtype = __IMPOSSIBLE__, cdcont = Constructor (nomi - dfv), cddeffreevars = dfv}) -- ?? correct value of deffreevars for records?-     c <- lift $ liftIO $ newIORef (ConstDef {cdname = prettyShow name, cdorigin = (Nothing, name), cdtype = __IMPOSSIBLE__, cdcont = Datatype [ccon] [], cddeffreevars = dfv}) -- ?? correct value of deffreevars for records?-     modify (\s -> s {sConsts = (Map.insert name (mode, c) cmap, name : snd (sConsts s))})-     return $ if iscon then ccon else c-  _ -> do-   cmap <- gets (fst . sConsts)-   case Map.lookup name cmap of-    Just (mode', c) ->-     return c-    Nothing -> do-     (miscon, sname) <- if iscon then do-       let MB.Constructor {MB.conPars = npar, MB.conData = dname, MB.conSrcCon = ch} = MB.theDef def-       return (Just (npar,I.conFields ch), prettyShow dname ++ "." ++ prettyShow (I.qnameName name))-      else-       return (Nothing, prettyShow name)-     mainm <- gets sMainMeta-     dfv <- lift $ getdfv mainm name-     c <- lift $ liftIO $ newIORef (ConstDef {cdname = sname, cdorigin = (miscon, name), cdtype = __IMPOSSIBLE__, cdcont = __IMPOSSIBLE__, cddeffreevars = dfv})-     modify (\s -> s {sConsts = (Map.insert name (mode, c) cmap, name : snd (sConsts s))})-     return c--getdfv :: I.MetaId -> A.QName -> MB.TCM Cm.Nat-getdfv mainm name = do- mv <- lookupLocalMetaAuto mainm- withMetaInfo (getMetaInfo mv) $ getDefFreeVars name---- | A variant of 'lookupLocalMeta' that, if applied to a remote--- meta-variable, raises a special error message noting that remote--- meta-variables are not handled by the auto command.--lookupLocalMetaAuto :: I.MetaId -> MB.TCM MB.MetaVariable-lookupLocalMetaAuto m = do-  mv <- lookupMeta m-  case mv of-    Just (Right mv) -> return mv-    Nothing         -> __IMPOSSIBLE__-    Just Left{}     -> MB.typeError $ MB.GenericError $-      "The auto command does not support remote meta-variables," ++-      "consider using --no-save-metas"--getMeta :: I.MetaId -> TOM (Metavar (Exp O) (RefInfo O))-getMeta name = do- mmap <- gets (fst . sMetas)- case Map.lookup name mmap of-  Just (m, _, _) ->-   return m-  Nothing -> do-   m <- lift $ liftIO initMeta-   modify $ \ s -> s { sMetas = (Map.insert name (m, Nothing, []) mmap, name : snd (sMetas s)) }-   return m--getEqs :: MB.TCM [(Bool, I.Term, I.Term)]-getEqs = forMaybeMM getAllConstraints $ \ eqc -> do-  neqc <- normalise eqc-  case MB.clValue $ MB.theConstraint neqc of-    MB.ValueCmp ineq _ i e -> do-      ei <- etaContract i-      ee <- etaContract e-      return $ Just (tomyIneq ineq, ee, ei)-    _ -> return Nothing--literalsNotImplemented :: MB.TCM a-literalsNotImplemented = MB.typeError $ MB.NotImplemented $-  "The Agda synthesizer (Agsy) does not support literals yet"--hitsNotImplemented :: MB.TCM a-hitsNotImplemented = MB.typeError $ MB.NotImplemented $-  "The Agda synthesizer (Agsy) does not support HITs yet"--class Conversion m a b where-  convert :: a -> m b--instance Conversion TOM [I.Clause] [([Pat O], MExp O)] where-  convert = fmap catMaybes . mapM convert--instance Conversion TOM I.Clause (Maybe ([Pat O], MExp O)) where-  convert cl = do-    let -- Jesper, 2016-07-28:-     -- I can't figure out if this should be the old or new-     -- clause body (i.e. relative to the positions of pattern variables or-     -- relative to the clauseTel). Both options pass the test suite, so I-     -- have the impression it doesn't actually matter.-     -- ALTERNATIVE CODE:-     -- perm = fromMaybe __IMPOSSIBLE__ $ IP.clausePerm cl-     -- body = applySubst (renamingR perm) $ I.clauseBody cl-        body = I.clauseBody cl-        pats = I.clausePats cl-    pats' <- mapM convert (IP.unnumberPatVars pats :: [Cm.Arg I.Pattern])-    body' <- traverse convert =<< lift (normalise body)-    return $ (pats',) <$> body'--instance Conversion TOM (Cm.Arg I.Pattern) (Pat O) where-  convert p = case Cm.unArg p of-    I.IApplyP _ _ _ n  -> return $ PatVar (prettyShow n)-    I.VarP _ n  -> return $ PatVar (prettyShow n)-    I.DotP _ _  -> return $ PatVar "_"-      -- because Agda includes these when referring to variables in the body-    I.ConP con _ pats -> do-      let n = I.conName con-      c     <- getConst True n TMAll-      pats' <- mapM (convert . fmap Cm.namedThing) pats-      def   <- lift $ getConstInfo n-      cc    <- lift $ liftIO $ readIORef c-      let Just (npar,_) = fst $ cdorigin cc-      return $ PatConApp c (replicate npar PatExp ++ pats')-    I.ProjP _ q -> PatProj <$> getConst True q TMAll--    -- UNSUPPORTED CASES-    I.LitP{}    -> lift literalsNotImplemented-    I.DefP{}    -> lift hitsNotImplemented--instance Conversion TOM I.Type (MExp O) where-  convert (I.El _ t) = convert t -- sort info is thrown away--instance Conversion TOM I.Term (MExp O) where-  convert v0 =-    case I.unSpine v0 of-      I.Var v es -> do-        let Just as = I.allApplyElims es-        as' <- convert as-        return $ NotM $ App Nothing (NotM OKVal) (Var v) as'-      I.Lam info b -> do-        b' <- convert (I.absBody b)-        return $ NotM $ Lam (getHiding info) (Abs (Id $ I.absName b) b')-      t@I.Lit{} -> do-        t <- lift $ constructorForm t-        case t of-          I.Lit{} -> lift literalsNotImplemented-          _       -> convert t-      I.Level l -> convert =<< lift (reallyUnLevelView l)-      I.Def name es -> do-        let Just as = I.allApplyElims es-        c   <- getConst False name TMAll-        as' <- convert as-        return $ NotM $ App Nothing (NotM OKVal) (Const c) as'-      I.Con con ci es -> do-        let Just as = I.allApplyElims es-        let name = I.conName con-        c   <- getConst True name TMAll-        as' <- convert as-        def <- lift $ getConstInfo name-        cc  <- lift $ liftIO $ readIORef c-        let Just (npar,_) = fst $ cdorigin cc-        return $ NotM $ App Nothing (NotM OKVal) (Const c) (foldl (\x _ -> NotM $ ALConPar x) as' [1..npar])-      I.Pi (I.Dom{domInfo = info, unDom = x}) b -> do-        let y    = I.absBody b-            name = I.absName b-        x' <- convert x-        y' <- convert y-        return $ NotM $ Pi Nothing (getHiding info) (Free.freeIn 0 y) x' (Abs (Id name) y')-      I.Sort (I.Type (I.ClosedLevel l)) -> return $ NotM $ Sort $ Set $ fromIntegral l-      I.Sort _ -> return $ NotM $ Sort UnknownSort-      I.Dummy{}-> return $ NotM $ Sort UnknownSort-      t@I.MetaV{} -> do-        t <- lift $ instantiate t-        case t of-          I.MetaV mid _ -> do-            mcurmeta <- gets sCurMeta-            case mcurmeta of-              Nothing -> return ()-              Just curmeta ->-                modify $ \ s -> s { sMetas = first (Map.adjust (\(m, x, deps) -> (m, x, mid : deps)) curmeta) (sMetas s) }-            m <- getMeta mid-            return $ Meta m-          _ -> convert t-      I.DontCare _ -> return $ NotM dontCare--instance Conversion TOM a b => Conversion TOM (Cm.Arg a) (Hiding, b) where-  convert (Cm.Arg info a) = (getHiding info,) <$> convert a--instance Conversion TOM I.Args (MM (ArgList O) (RefInfo O)) where-  convert as = NotM . foldr (\ (hid,t) -> ALCons hid t . NotM) ALNil-               <$> mapM convert as--tomyIneq :: MB.Comparison -> Bool-tomyIneq MB.CmpEq = False-tomyIneq MB.CmpLeq = True---- -----------------------------------------------fmType :: I.MetaId -> I.Type -> Bool-fmType m (I.El _ t) = fmExp m t--fmExp :: I.MetaId -> I.Term -> Bool-fmExp m (I.Var _ as) = fmExps m $ I.argsFromElims as-fmExp m (I.Lam _ b) = fmExp m (I.unAbs b)-fmExp m (I.Lit _) = False-fmExp m (I.Level (I.Max _ as)) = any (fmLevel m) as-fmExp m (I.Def _ as) = fmExps m $ I.argsFromElims as-fmExp m (I.Con _ ci as) = fmExps m $ I.argsFromElims as-fmExp m (I.Pi x y)  = fmType m (I.unDom x) || fmType m (I.unAbs y)-fmExp m (I.Sort _) = False-fmExp m (I.MetaV mid _) = mid == m-fmExp m (I.DontCare _) = False-fmExp _ I.Dummy{} = False--fmExps :: I.MetaId -> I.Args -> Bool-fmExps m as = any (fmExp m . Cm.unArg) as--fmLevel :: I.MetaId -> I.PlusLevel -> Bool-fmLevel m (I.Plus _ l) = fmExp m l---- -----------------------------------------------icnvh :: Hiding -> Cm.ArgInfo-icnvh h = Cm.setHiding h $-          Cm.setOrigin o $-          Cm.defaultArgInfo-    where-    -- Andreas, 2017-01-18, issue #819.-    -- Visible arguments are made UserWritten,-    -- otherwise they might not be printed in patterns.-    o = case h of-          NotHidden  -> Cm.UserWritten-          Instance{} -> Cm.Inserted-          Hidden     -> Cm.Inserted---- -----------------------------------------------instance Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b where-  convert meta = case meta of-    NotM a -> convert a-    Meta m -> do-      ma <- lift $ readIORef $ mbind m-      case ma of-        Nothing -> throwError "meta not bound"-        Just a  -> convert a--instance Conversion MOT a b => Conversion MOT (Abs a) (I.Abs b) where-  convert (Abs mid t) = I.Abs id <$> convert t where-    id = case mid of-           NoId  -> "x"-           Id id -> id--instance Conversion MOT (Exp O) I.Type where-  convert e = I.El (I.mkType 0) <$> convert e-              -- 0 is arbitrary, sort not read by Agda when reifying--instance Conversion MOT (Exp O) I.Term where-  convert = \case-    App _ _ (Var v) as -> frommyExps 0 as (I.Var v [])-    App _ _ (Const c) as -> do-      cdef <- lift $ readIORef c-      let (iscon, name) = cdorigin cdef-{--   case iscon of-      Just n -> do-        v <- getConTerm name -- We are not in TCM-        frommyExps n as v--}-          (ndrop, h) = case iscon of-                         Just (n,fs) -> (n, \ q -> I.Con (I.ConHead q I.IsData Cm.Inductive fs) Cm.ConOSystem)-                         Nothing -> (0, \ f vs -> I.Def f vs)-      frommyExps ndrop as (h name [])-    Lam hid t -> I.Lam (icnvh hid) <$> convert t-    Pi _ hid _ x y -> do-      x' <- convert x-      let dom = (I.defaultDom x') {domInfo = icnvh hid}-      I.Pi dom <$> convert y-   -- maybe have case for Pi where possdep is False which produces Fun (and has to unweaken y), return $ I.Fun (Cm.Arg (icnvh hid) x') y'-    Sort (Set l) -> return $ I.Sort (I.mkType (fromIntegral l))-    Sort Type -> __IMPOSSIBLE__-    Sort UnknownSort -> return $ I.Sort (I.mkType 0) -- hoping it's thrown away--    AbsurdLambda hid -> return $ I.Lam (icnvh hid)-                               $ I.Abs abslamvarname (I.Var 0 [])--frommyExps :: Nat -> MArgList O -> I.Term -> ExceptT String IO I.Term-frommyExps ndrop (Meta m) trm = do- bind <- lift $ readIORef $ mbind m- case bind of-  Nothing -> throwError "meta not bound"-  Just e -> frommyExps ndrop (NotM e) trm-frommyExps ndrop (NotM as) trm =- case as of-  ALNil -> return trm-  ALCons _ _ xs | ndrop > 0 -> frommyExps (ndrop - 1) xs trm-  ALCons hid x xs -> do-   x' <- convert x-   frommyExps ndrop xs (addend (Cm.Arg (icnvh hid) x') trm)--  -- Andreas, 2013-10-19 TODO: restore postfix projections-  ALProj eas idx hid xs -> do-   idx <- lift $ expandbind idx-   c <- case idx of-            NotM c -> return c-            Meta{} -> throwError "meta not bound"-   cdef <- lift $ readIORef c-   let name = snd $ cdorigin cdef-   trm2 <- frommyExps 0 eas (I.Def name [])-   frommyExps 0 xs (addend (Cm.Arg (icnvh hid) trm) trm2)--  ALConPar xs | ndrop > 0 -> frommyExps (ndrop - 1) xs trm-  ALConPar _ -> __IMPOSSIBLE__- where-  addend x (I.Var h xs) = I.Var h (xs ++ [I.Apply x])-  addend x (I.Con h ci xs) = I.Con h ci (xs ++ [I.Apply x])-  addend x (I.Def h xs) = I.Def h (xs ++ [I.Apply x])-  addend _ _ = __IMPOSSIBLE__---- ----------------------------------abslamvarname :: String-abslamvarname = "\0absurdlambda"--modifyAbstractExpr :: A.Expr -> A.Expr-modifyAbstractExpr = f- where-  f (A.App i e1 (Cm.Arg info (Cm.Named n e2))) =-        A.App i (f e1) (Cm.Arg info (Cm.Named n (f e2)))-  f (A.Lam i (A.DomainFree _ x) _)-     | A.Binder _ (A.BindName{unBind = n}) <- Cm.namedArg x-     , prettyShow (A.nameConcrete n) == abslamvarname =-        A.AbsurdLam i $ Cm.getHiding x-  f (A.Lam i b e) = A.Lam i b (f e)-  f (A.Rec i xs) = A.Rec i (map (mapLeft (over exprFieldA f)) xs)-  f (A.RecUpdate i e xs) = A.RecUpdate i (f e) (map (over exprFieldA f) xs)-  f (A.ScopedExpr i e) = A.ScopedExpr i (f e)-  f e = e--modifyAbstractClause :: A.Clause -> A.Clause-modifyAbstractClause (A.Clause lhs spats (A.RHS e mc) decls catchall) =-  A.Clause lhs spats (A.RHS (modifyAbstractExpr e) mc) decls catchall-modifyAbstractClause cl = cl---- ------------------------------------constructPats :: Map AN.QName (TMode, ConstRef O) -> I.MetaId -> I.Clause -> MB.TCM ([(Hiding, MId)], [CSPat O])-constructPats cmap mainm clause = do- let cnvps ns [] = return (ns, [])-     cnvps ns (p : ps) = do-      (ns', ps') <- cnvps ns ps-      (ns'', p') <- cnvp ns' p-      return (ns'', p' : ps')-     cnvp ns p =-      let hid = getHiding $ Cm.argInfo p-      in case Cm.namedArg p of-       I.VarP _ n -> return ((hid, Id n) : ns, HI hid (CSPatVar $ length ns))-       I.IApplyP _ _ _ n -> return ((hid, Id n) : ns, HI hid (CSPatVar $ length ns))-       I.ConP con _ ps -> do-        let c = I.conName con-        (c2, _) <- runStateT (getConst True c TMAll) (S {sConsts = (cmap, []), sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = mainm})-        (ns', ps') <- cnvps ns ps-        cc <- liftIO $ readIORef c2-        let Just (npar,_) = fst $ cdorigin cc-        return (ns', HI hid (CSPatConApp c2 (replicate npar (HI Hidden CSOmittedArg) ++ ps')))-       I.DotP _ t -> do-        (t2, _) <- runStateT (convert t) (S {sConsts = (cmap, []), sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = mainm})-        return (ns, HI hid (CSPatExp t2))-       I.ProjP po c -> do-        (c2, _) <- runStateT (getConst True c TMAll) (S {sConsts = (cmap, []), sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = mainm})-        cc <- liftIO $ readIORef c2-        return (ns, HI hid (CSPatProj c2))-       I.LitP{} -> literalsNotImplemented-       I.DefP{} -> hitsNotImplemented-- (names, pats) <- cnvps [] (IP.unnumberPatVars $ I.namedClausePats clause)- return (reverse names, pats)---frommyClause :: (CSCtx O, [CSPat O], Maybe (MExp O)) -> ExceptT String IO I.Clause-frommyClause (ids, pats, mrhs) = do- let ctel [] = return I.EmptyTel-     ctel (HI hid (mid, t) : ctx) = do-      let Id id = mid-      tel <- ctel ctx-      t' <- convert t-      let dom = (I.defaultDom t') {domInfo = icnvh hid}-      return $ I.ExtendTel dom (I.Abs id tel)- tel <- ctel $ reverse ids- let getperms 0 [] perm nv = return (perm, nv)-     getperms n [] _ _ = __IMPOSSIBLE__-     getperms 0 (p : ps) perm nv = do-      (perm, nv) <- getperm p perm nv-      getperms 0 ps perm nv-     getperms n (HI _ CSPatExp{} : ps) perm nv = getperms (n - 1) ps perm nv-     getperms n (HI _ CSOmittedArg{} : ps) perm nv = getperms (n - 1) ps perm nv-     getperms n (_ : _) _ _ = __IMPOSSIBLE__-     getperm (HI _ p) perm nv =-      case p of-       --CSPatVar v -> return (length ids + nv - 1 - v : perm, nv)-       CSPatVar v -> return ((length ids - 1 - v, nv) : perm, nv + 1)-       CSPatConApp c ps -> do-        cdef <- lift $ readIORef c-        let (Just (ndrop,_), _) = cdorigin cdef-        getperms ndrop ps perm nv-       CSPatExp e -> return (perm, nv + 1)-       _ -> __IMPOSSIBLE__- (rperm, nv) <- getperms 0 pats [] 0- let --perm = reverse rperm-     perm = map (\i -> let Just x = lookup i rperm in x) [0..length ids - 1]-     --renperm = map (\i -> length ids + nv - 1 - i) rperm-     --renm = rename (\i -> renperm !! i)-     cnvps 0 [] = return []-     cnvps n [] = __IMPOSSIBLE__-     cnvps 0 (p : ps) = do-      p' <- cnvp p-      ps' <- cnvps 0 ps-      return (p' : ps')-     cnvps n (HI _ CSPatExp{} : ps) = cnvps (n - 1) ps-     cnvps n (HI _ CSOmittedArg{} : ps) = cnvps (n - 1) ps-     cnvps n (_ : _) = __IMPOSSIBLE__-     cnvp (HI hid p) = do-      p' <- case p of-       CSPatVar v -> return (I.varP $ let HI _ (Id n, _) = ids !! v in n)-       CSPatConApp c ps -> do-        cdef <- lift $ readIORef c-        let (Just (ndrop,_), name) = cdorigin cdef-        ps' <- cnvps ndrop ps-        let con = I.ConHead name I.IsData Cm.Inductive [] -- TODO: restore DataOrRecord and record fields!-        return (I.ConP con I.noConPatternInfo ps')-       CSPatExp e -> do-        e' <- convert e {- renm e -} -- renaming before adding to clause below-        return (I.dotP e')-       CSAbsurd -> __IMPOSSIBLE__ -- CSAbsurd not used-       _ -> __IMPOSSIBLE__-      return $ Cm.Arg (icnvh hid) $ Cm.unnamed p'   -- TODO: recover names- ps <- cnvps 0 pats- body <- case mrhs of-          Nothing -> return $ Nothing-          Just e -> Just <$> convert e- let cperm =  Perm nv perm- 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.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.clauseWhereModule = Nothing-   }--contains_constructor :: [CSPat O] -> Bool-contains_constructor = any f- where-  f (HI _ p) = case p of-         CSPatConApp{} -> True-         _ -> False---- -----------------------------------freeIn :: Nat -> MExp o -> Bool-freeIn = f- where-  mr x = let NotM x' = x in x'-  f v e = case mr e of-   App _ _ elr args -> case elr of-    Var v' | v' == v -> False-    _ -> fs v args-   Lam _ (Abs _ b) -> f (v + 1) b-   Pi _ _ _ it (Abs _ ot) -> f v it && f (v + 1) ot-   Sort{} -> True--   AbsurdLambda{} -> True---  fs v es = case mr es of-   ALNil -> True-   ALCons _ a as -> f v a && fs v as--   ALProj{} -> __IMPOSSIBLE__---   ALConPar as -> fs v as---negtype :: ConstRef o -> MExp o -> MExp o-negtype ee = f (0 :: Int)- where-  mr x = let NotM x' = x in x'-  f n e = case mr e of-   Pi uid hid possdep it (Abs id ot) -> NotM $ Pi uid hid possdep it (Abs id (f (n + 1) ot))-   _ -> NotM $ Pi Nothing NotHidden False (NotM $ Pi Nothing NotHidden False e (Abs NoId (NotM $ Pi Nothing NotHidden True (NotM $ Sort (Set 0)) (Abs NoId (NotM $ App Nothing (NotM OKVal) (Var 0) (NotM ALNil)))))) (Abs NoId (NotM $ App Nothing (NotM OKVal) (Const ee) (NotM ALNil)))---- -----------------------------------------findClauseDeep :: Cm.InteractionId -> MB.TCM (Maybe (AN.QName, I.Clause, Bool))-findClauseDeep ii = ignoreAbstractMode $ do  -- Andreas, 2016-09-04, issue #2162-  MB.InteractionPoint { MB.ipClause = ipCl} <- lookupInteractionPoint ii-  case ipCl of-    MB.IPNoClause -> return Nothing-    MB.IPClause f clauseNo _ _ _ _ -> do-      (_, (_, c, _)) <- getClauseZipperForIP f clauseNo-      return $ Just (f, c, maybe __IMPOSSIBLE__ toplevel $ I.clauseBody c)-  where-    toplevel e =-     case e of-      I.MetaV{} -> True-      _ -> False---- -----------------------------------------matchType :: Int -> Int -> I.Type -> I.Type -> Maybe (Nat, Nat) -- Nat is deffreevars of const, Nat is ctx length of target type, left arg is const type, right is target type-matchType cdfv tctx ctyp ttyp = trmodps cdfv ctyp- where-  trmodps 0 ctyp = tr 0 0 ctyp-  trmodps n ctyp = case I.unEl ctyp of-   I.Pi _ ot -> trmodps (n - 1) (I.absBody ot)-   _ -> __IMPOSSIBLE__-  tr narg na ctyp =-   case ft 0 0 Just ctyp ttyp of-    Just n -> Just (n, narg)-    Nothing -> case I.unEl ctyp of-     I.Pi _ (I.Abs _ ot) -> tr (narg + 1) (na + 1) ot-     I.Pi _ (I.NoAbs _ ot) -> tr (narg + 1) na ot-     _ -> Nothing-   where-    ft nl n c (I.El _ e1) (I.El _ e2) = f nl n c e1 e2-    f nl n c e1 e2 = case e1 of-     I.Var v1 as1 | v1 < nl -> case e2 of-      I.Var v2 as2 | v1 == v2 -> fes nl (n + 1) c as1 as2-      _ -> Nothing-     I.Var v1 _ | v1 < nl + na -> c n -- unify vars with no args?-     I.Var v1 as1 -> case e2 of-      I.Var v2 as2 | cdfv + na + nl - v1 == tctx + nl - v2 -> fes nl (n + 1) c as1 as2-      _ -> Nothing-     _ -> case (e1, e2) of-      (I.MetaV{}, _) -> c n-      (_, I.MetaV{}) -> c n-      (I.Lam hid1 b1, I.Lam hid2 b2) | hid1 == hid2 -> f (nl + 1) n c (I.absBody b1) (I.absBody b2)-      (I.Lit lit1, I.Lit lit2) | lit1 == lit2 -> c (n + 1)-      (I.Def n1 as1, I.Def n2 as2) | n1 == n2 -> fes nl (n + 1) c as1 as2-      (I.Con n1 _ as1, I.Con n2 _ as2) | n1 == n2 -> fs nl (n + 1) c as1 as2-      (I.Pi (I.Dom{domInfo = info1, unDom = it1})  ot1, I.Pi (I.Dom{domInfo = info2, unDom = it2})  ot2) | Cm.argInfoHiding info1 == Cm.argInfoHiding info2 -> ft nl n (\n -> ft (nl + 1) n c (I.absBody ot1) (I.absBody ot2)) it1 it2-      (I.Sort{}, I.Sort{}) -> c n -- sloppy-      _ -> Nothing-    fs nl n c es1 es2 = case (es1, es2) of-     ([], []) -> c n-     (I.Apply (Cm.Arg info1 e1) : es1, I.Apply (Cm.Arg info2 e2) : es2) | Cm.argInfoHiding info1 == Cm.argInfoHiding info2 -> f nl n (\n -> fs nl n c es1 es2) e1 e2-     _ -> Nothing-    fes nl n c es1 es2 = case (es1, es2) of-     ([], []) -> c n-     (I.Proj _ f : es1, I.Proj _ f' : es2) | f == f' -> fes nl n c es1 es2-     (I.Apply (Cm.Arg info1 e1) : es1, I.Apply (Cm.Arg info2 e2) : es2) | Cm.argInfoHiding info1 == Cm.argInfoHiding info2 -> f nl n (\n -> fes nl n c es1 es2) e1 e2-     _ -> Nothing

@@ -1,670 +0,0 @@-{-# OPTIONS_GHC -Wunused-imports #-}--module Agda.Auto.NarrowingSearch where--import Control.Monad       ( foldM, when )-import Control.Monad.State ( MonadState(..), modify, StateT, evalStateT, runStateT )-import Control.Monad.Trans ( lift )--import Data.IORef hiding (writeIORef, modifyIORef)-import qualified Data.IORef as NoUndo (writeIORef, modifyIORef)--import Agda.Utils.Impossible-import Agda.Utils.Empty--newtype Prio = Prio { getPrio :: Int }- deriving (Eq, Ord, Num)--class Trav a where-  type Block a-  trav :: Monad m => (forall b. TravWith b (Block a) => MM b (Block b) -> m ()) -> a -> m ()---- | Trav instance 'a' with block type 'blk'-type TravWith a blk = (Trav a, Block a ~ blk)--instance TravWith a blk => Trav (MM a blk) where-  type Block (MM a blk) = blk-  trav f me = f me--data Term blk = forall a. TravWith a blk => Term a---- | Result of type-checking.-data Prop blk-  = OK-    -- ^ Success.-  | Error String-    -- ^ Definite failure.-  | forall a . AddExtraRef String (Metavar a blk) (Move' blk a)-    -- ^ Experimental.-  | And (Maybe [Term blk]) (MetaEnv (PB blk)) (MetaEnv (PB blk))-    -- ^ Parallel conjunction of constraints.-  | Sidecondition (MetaEnv (PB blk)) (MetaEnv (PB blk))-    -- ^ Experimental, related to 'mcompoint'.-    -- First arg is sidecondition.-  | Or Prio (MetaEnv (PB blk)) (MetaEnv (PB blk))-    -- ^ Forking proof on something that is not part of the term language.-    --   E.g. whether a term will reduce or not.-  | ConnectHandle (OKHandle blk) (MetaEnv (PB blk))-    -- ^ Obsolete.--data OKVal = OKVal-type OKHandle blk = MM OKVal blk-type OKMeta blk = Metavar OKVal blk---- | Agsy's meta variables.------   @a@ the type of the metavariable (what it can be instantiated with).---   @blk@ the search control information (e.g. the scope of the meta).--data Metavar a blk = Metavar-  { mbind :: IORef (Maybe a)-    -- ^ Maybe an instantiation (refinement).  It is usually shallow,-    --   i.e., just one construct(or) with arguments again being metas.-  , mprincipalpresent :: IORef Bool-    -- ^ Does this meta block a principal constraint-    --   (i.e., a type-checking constraint).-  , mobs :: IORef [(QPB a blk, Maybe (CTree blk))]-    -- ^ List of observers, i.e., constraints blocked by this meta.-  , mcompoint :: IORef [SubConstraints blk]-    -- ^ Used for experiments with independence of subproofs.-  , mextrarefs :: IORef [Move' blk a]-    -- ^ Experimental.-  }--hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool-hequalMetavar m1 m2 = mprincipalpresent m1 == mprincipalpresent m2--instance Eq (Metavar a blk) where- x == y = hequalMetavar x y--newMeta :: IORef [SubConstraints blk] -> IO (Metavar a blk)-newMeta mcompoint = do- bind <- newIORef Nothing- pp <- newIORef False- obs <- newIORef []- erefs <- newIORef []- return $ Metavar bind pp obs mcompoint erefs--initMeta :: IO (Metavar a blk)-initMeta = do- cp <- newIORef []- newMeta cp--data CTree blk = CTree- {ctpriometa :: IORef (PrioMeta blk),-  ctsub :: IORef (Maybe (SubConstraints blk)),-  ctparent :: IORef (Maybe (CTree blk)), -- Nothing - root-  cthandles :: IORef [OKMeta blk]- }--data SubConstraints blk = SubConstraints- {scflip :: IORef Bool,-  sccomcount :: IORef Int,-  scsub1 :: CTree blk,-  scsub2 :: CTree blk- }---newCTree :: Maybe (CTree blk) -> IO (CTree blk)-newCTree parent = do- priometa <- newIORef (NoPrio False)- sub <- newIORef Nothing- rparent <- newIORef parent- handles <- newIORef []- return $ CTree priometa sub rparent handles--newSubConstraints :: CTree blk -> IO (SubConstraints blk)-newSubConstraints node = do- flip <- newIORef True -- False -- initially (and always) True, trying out prefer rightmost subterm when none have priority- comcount <- newIORef 0- sub1 <- newCTree $ Just node- sub2 <- newCTree $ Just node- return $ SubConstraints flip comcount sub1 sub2---data PrioMeta blk = forall a . Refinable a blk => PrioMeta Prio (Metavar a blk)-                  | NoPrio Bool -- True if subconstraint is done (all OK)--instance Eq (PrioMeta blk) where- NoPrio d1 == NoPrio d2 = d1 == d2- PrioMeta p1 m1 == PrioMeta p2 m2 = p1 == p2 && hequalMetavar m1 m2- _ == _ = False---- -------------------------data Restore = forall a . Restore (IORef a) a--type Undo = StateT [Restore] IO--ureadIORef :: IORef a -> Undo a-ureadIORef ptr = lift $ readIORef ptr--uwriteIORef :: IORef a -> a -> Undo ()-uwriteIORef ptr newval = do- oldval <- ureadIORef ptr- modify (Restore ptr oldval :)- lift $ NoUndo.writeIORef ptr newval--umodifyIORef :: IORef a -> (a -> a) -> Undo ()-umodifyIORef ptr f = do- oldval <- ureadIORef ptr- modify (Restore ptr oldval :)- lift $ NoUndo.writeIORef ptr (f oldval)--ureadmodifyIORef :: IORef a -> (a -> a) -> Undo a-ureadmodifyIORef ptr f = do- oldval <- ureadIORef ptr- modify (Restore ptr oldval :)- lift $ NoUndo.writeIORef ptr (f oldval)- return oldval--runUndo :: Undo a -> IO a-runUndo x = do- (res, restores) <- runStateT x []- mapM_ (\(Restore ptr oldval) -> NoUndo.writeIORef ptr oldval) restores- return res---- -------------------------newtype RefCreateEnv blk a = RefCreateEnv-  { runRefCreateEnv :: StateT ((IORef [SubConstraints blk]), Int) IO a }--instance Functor (RefCreateEnv blk) where-  fmap f = RefCreateEnv . fmap f . runRefCreateEnv--instance Applicative (RefCreateEnv blk) where-  pure    = RefCreateEnv . pure-  f <*> t = RefCreateEnv $ runRefCreateEnv f <*> runRefCreateEnv t--instance Monad (RefCreateEnv blk) where-  return = pure-  t >>= f = RefCreateEnv $ runRefCreateEnv t >>= runRefCreateEnv . f---newtype Cost = Cost { getCost :: Int }-  deriving (Num, Eq, Ord)--data Move' blk a = Move-  { moveCost :: Cost-  , moveNext :: RefCreateEnv blk a-  }--class Refinable a blk where- refinements :: blk -> [blk] -> Metavar a blk -> IO [Move' blk a]---newPlaceholder :: RefCreateEnv blk (MM a blk)-newPlaceholder = RefCreateEnv $ do- (mcompoint, c) <- get- m <- lift $ newMeta mcompoint- put (mcompoint, (c + 1))- return $ Meta m--newOKHandle :: RefCreateEnv blk (OKHandle blk)-newOKHandle = RefCreateEnv $ do- (e, c) <- get- cp <- lift $ newIORef []- m  <- lift $ newMeta cp- put (e, (c + 1))- return $ Meta m--dryInstantiate :: RefCreateEnv blk a -> IO a-dryInstantiate bind = evalStateT (runRefCreateEnv bind) (__IMPOSSIBLE__, 0)--type BlkInfo blk = (Bool, Prio, Maybe blk) -- Bool - is principal--data MM a blk = NotM a-              | Meta (Metavar a blk)--rm :: Empty -> MM a b -> a-rm _ (NotM x) = x-rm e Meta{}   = absurd e--type MetaEnv = IO---data MB a blk = NotB a-              | forall b . Refinable b blk => Blocked (Metavar b blk) (MetaEnv (MB a blk))-              | Failed String--data PB blk = NotPB (Prop blk)-            | forall b . Refinable b blk => PBlocked (Metavar b blk) (BlkInfo blk) (MetaEnv (PB blk))-            | forall b1 b2 . (Refinable b1 blk, Refinable b2 blk) => PDoubleBlocked (Metavar b1 blk) (Metavar b2 blk) (MetaEnv (PB blk))--data QPB b blk = QPBlocked (BlkInfo blk) (MetaEnv (PB blk))-               | QPDoubleBlocked (IORef Bool) (MetaEnv (PB blk)) -- flag set True by first observer that continues--mmcase :: Refinable a blk => MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)-mmcase x f = case x of- NotM x -> f x- x@(Meta m) -> do-  bind <- readIORef $ mbind m-  case bind of-   Just x -> f x-   Nothing -> return $ Blocked m (mmcase x f)--mmmcase :: MM a blk -> MetaEnv (MB b blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)-mmmcase x fm f = case x of- NotM x -> f x- Meta m -> do-  bind <- readIORef $ mbind m-  maybe fm f bind--mmpcase :: Refinable a blk => BlkInfo blk -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)-mmpcase blkinfo x f = case x of- NotM x -> f x- x@(Meta m) -> do-  bind <- readIORef $ mbind m-  case bind of-   Just x -> f x-   Nothing -> return $ PBlocked m blkinfo (mmpcase __IMPOSSIBLE__ x f) -- blkinfo not needed because will be notb next time--doubleblock :: (Refinable a blk, Refinable b blk) => MM a blk -> MM b blk -> MetaEnv (PB blk) -> MetaEnv (PB blk)-doubleblock (Meta m1) (Meta m2) cont = return $ PDoubleBlocked m1 m2 cont-doubleblock _ _ _ = __IMPOSSIBLE__--mbcase :: MetaEnv (MB a blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)-mbcase x f = do- x' <- x- case x' of-  NotB x -> f x-  Blocked m x -> return $ Blocked m (mbcase x f)-  Failed msg -> return $ Failed msg--mbpcase :: Prio -> Maybe blk -> MetaEnv (MB a blk) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)-mbpcase prio bi x f = do- x' <- x- case x' of-  NotB x -> f x-  Blocked m x -> return $ PBlocked m (False, prio, bi) (mbpcase prio bi x f)-  Failed msg -> return $ NotPB $ Error msg--mmbpcase :: MetaEnv (MB a blk) -> (forall b . Refinable b blk => MM b blk -> MetaEnv (PB blk)) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)-mmbpcase x fm f = do- x' <- x- case x' of-  NotB x -> f x-  Blocked m _ -> fm (Meta m)-  Failed msg -> return $ NotPB $ Error msg--waitok :: OKHandle blk -> MetaEnv (MB b blk) -> MetaEnv (MB b blk)-waitok okh f =- mmcase okh $ \ OKVal -> f -- principle constraint is never present for okhandle so it will not be refined--mbret :: a -> MetaEnv (MB a blk)-mbret x = return $ NotB x--mbfailed :: String -> MetaEnv (MB a blk)-mbfailed msg = return $ Failed msg--mpret :: Prop blk -> MetaEnv (PB blk)-mpret p = return $ NotPB p--expandbind :: MM a blk -> MetaEnv (MM a blk)-expandbind x = case x of- NotM{} -> return x- Meta m -> do-  bind <- readIORef $ mbind m-  case bind of-   Just x -> return $ NotM x-   Nothing -> return x----- -------------------------type HandleSol = IO ()---type SRes = Either Bool Int--topSearch :: forall blk . IORef Int -> IORef Int -> HandleSol -> blk -> MetaEnv (PB blk) -> Cost -> Cost -> IO Bool-topSearch ticks nsol hsol envinfo p searchdepth depthinterval = do- depthreached <- newIORef False--- mainroot <- newCTree Nothing-- let-  searchSubProb :: [(CTree blk, Maybe (IORef Bool))] -> Cost -> IO SRes-  searchSubProb [] depth = do-   when (depth < depthinterval) $ do---    hsol-    n <- readIORef nsol-    NoUndo.writeIORef nsol $! n - 1---   return $ Left True-  searchSubProb ((root, firstdone) : restprobs) depth =-   let-    search :: Cost -> IO SRes-    search depth = do-     pm <- readIORef $ ctpriometa root-     case pm of-      NoPrio False -> return $ Left False -- nothing to refine but not done, this can happen when eq constraints are passed along with main constraint in agdaplugin-      NoPrio True ->-       searchSubProb restprobs depth -- ?? what should depth be-      PrioMeta _ m -> do-       let carryon = fork m depth-       sub <- readIORef $ ctsub root-       case sub of-        Nothing -> carryon-        Just sc -> do-         let sub1 = scsub1 sc-             sub2 = scsub2 sc-         pm1 <- readIORef $ ctpriometa sub1-         pm2 <- readIORef $ ctpriometa sub2-         let split = carryon -- split disabled-         case pm1 of-          NoPrio True -> split-          _ ->-           case pm2 of-            NoPrio True -> split-            _ -> do-             comc <- readIORef $ sccomcount sc-             case comc of-              0 -> split-              _ -> carryon--    fork :: forall a. Refinable a blk => Metavar a blk -> Cost -> IO SRes-    fork m depth = do-      blkinfos <- extractblkinfos m-      refs <- refinements envinfo blkinfos m-      f refs-     where-      f :: [Move' blk a] -> IO SRes-      f [] = do-       erefs <- readIORef $ mextrarefs m-       case erefs of-        [] -> return (Left False)-        _ -> do-         NoUndo.writeIORef (mextrarefs m) []-         f erefs-      f (Move cost bind : binds) = hsres (refine m bind (depth - cost)) (f binds)-    hsres :: IO SRes -> IO SRes -> IO SRes-    hsres x1 x2 = do-     res <- x1-     case res of-      Right _ -> return res-      Left found -> do-       n <- readIORef nsol-       if n == 0 then-         return res-        else do-         res2 <- x2-         case res2 of-          Right _ -> if found then __IMPOSSIBLE__ else return res2-          Left found2 -> return $ Left (found || found2)--    refine :: Metavar a blk -> RefCreateEnv blk a -> Cost -> IO SRes--    refine _ _ depthleft | depthleft < 0 = do-     NoUndo.writeIORef depthreached True-     return $ Left False---    refine m bind depthleft = runUndo $-     do t <- ureadIORef ticks-        lift $ NoUndo.writeIORef ticks $! t + 1---        (bind, (_, nnewmeta)) <- lift $ runStateT (runRefCreateEnv bind) (mcompoint m, 0)-        uwriteIORef (mbind m) (Just bind)-        mcomptr <- ureadIORef $ mcompoint m-        mapM_ (\comptr ->-          umodifyIORef (sccomcount comptr) (+ (nnewmeta - 1))-          -- umodifyIORef (scflip comptr) not -- don't flip now since trying prefer rightmost subterm if non have prio-         ) mcomptr-        obs <- ureadIORef (mobs m)-        res <- recalcs obs-        if res-          then-            return $ Left False     -- failed-          else-            lift $ search depthleft -- succeeded--    doit = do-     res <- search depth-     return $ case res of-      Right n ->-       case firstdone of-        Nothing ->-         if n == 0 then-          Left False-         else-          Right (n - 1)-        Just _ ->-         Right (n + 1)-      res@(Left True) -> res-      res@(Left False) ->-       case firstdone of-        Nothing -> res-        Just _ -> Right 0-   in-    case firstdone of-     Nothing -> doit-     Just rdone -> do-      done <- readIORef rdone-      if done then-        searchSubProb restprobs depth-       else do-        NoUndo.writeIORef rdone True-        doit-- runUndo $ do-  res <- reccalc p (Just mainroot)-  if res -- failed immediately-    then-        return False-    else-      do-        Left _solFound <- lift $ searchSubProb [(mainroot, Nothing)] searchdepth-        lift $ readIORef depthreached---extractblkinfos :: Metavar a blk -> IO [blk]-extractblkinfos m = do- obs <- readIORef $ mobs m- return $ f obs- where-  f [] = []-  f ((QPBlocked (_,_,mblkinfo) _, _) : cs) =-   case mblkinfo of-    Nothing -> f cs-    Just blkinfo -> blkinfo : f cs-  f ((QPDoubleBlocked{}, _) : cs) = f cs--recalcs :: [(QPB a blk, Maybe (CTree blk))] -> Undo Bool-recalcs cs = foldr (seqc . recalc) (return False) cs--seqc :: Undo Bool -> Undo Bool -> Undo Bool-seqc x y = do- res1 <- x- case res1 of-  res1@True -> return res1-  False -> y--recalc :: (QPB a blk, Maybe (CTree blk)) -> Undo Bool-recalc (con, node) = case con of-  QPBlocked       _    cont -> reccalc cont node-  QPDoubleBlocked flag cont -> do-    fl <- ureadIORef flag-    if fl-      then return False-      else do-        uwriteIORef flag True-        reccalc cont node--reccalc :: MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool-reccalc cont node = do-  res <- calc cont node-  case res of-    Nothing -> return True-    Just pendhandles ->-      foldM-        ( \res1 h ->-            if res1-              then return res1-              else do-                uwriteIORef (mbind h) $ Just OKVal-                obs <- ureadIORef (mobs h)-                recalcs obs-        )-        False-        pendhandles--calc :: forall blk . MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk])-calc cont node = do-  res <- donewp node cont-  case res of-   Just (_, pendhandles) -> do-    pendhandles2 <- case node of-     Just node -> propagatePrio node-     Nothing -> return []-    return $ Just (pendhandles ++ pendhandles2)-   Nothing -> return Nothing- where-  storeprio (Just node) pm pendhandles = do-   pendhandles' <- case pm of-    NoPrio True -> do-     handles <- ureadIORef (cthandles node)-     return $ handles ++ pendhandles-    _ -> return pendhandles-   uwriteIORef (ctpriometa node) pm-   return $ Just (pm, pendhandles')-  storeprio Nothing _ _ =-   return $ Just (NoPrio False, [])-  donewp node p = do-   bp <- lift p-   case bp of-    NotPB p ->-     doprop node p-    PBlocked m blkinfo cont -> do-     oldobs <- ureadmodifyIORef (mobs m) ((QPBlocked blkinfo cont, node) :)-     let (princ, prio, _) = blkinfo-     pp <- ureadIORef (mprincipalpresent m)-     when (princ && not pp) $ do-      uwriteIORef (mprincipalpresent m) True-      mapM_ (\(qpb, node) -> case node of-         Just node ->-          case qpb of-           QPBlocked (_, prio, _) _ -> do---            uwriteIORef (ctpriometa node) (PrioMeta prio m)-            propagatePrio node-           QPDoubleBlocked _flag _ ->-            return []-         Nothing -> return []-       ) oldobs-     if pp || princ then-       storeprio node (PrioMeta prio m) []-      else-       storeprio node (NoPrio False) []-    PDoubleBlocked m1 m2 cont -> do-     flag <- lift $ newIORef False--     let newobs :: forall b. [(QPB b blk, Maybe (CTree blk))]-                          -> [(QPB b blk, Maybe (CTree blk))]-         newobs = ((QPDoubleBlocked flag cont, node) :)-     umodifyIORef (mobs m1) newobs-     umodifyIORef (mobs m2) newobs-     storeprio node (NoPrio False) []-  doprop node p =-   case p of-    OK -> storeprio node (NoPrio True) []-    Error _ -> return Nothing---    AddExtraRef _ m eref -> do-     lift $ NoUndo.modifyIORef (mextrarefs m) (eref :)-     return Nothing-    And coms p1 p2 -> do-     let Just jnode = node-     sc <- lift $ newSubConstraints jnode---     uwriteIORef (ctsub jnode) $ Just sc-     ndep <- case coms of-      Nothing -> return 1 -- no metas pointing to it so will never decrement to 0-      Just _coms  -> return 1 -- dito-     lift $ NoUndo.writeIORef (sccomcount sc) ndep -- OK since sc was just created-     resp1 <- donewp (Just $ scsub1 sc) p1-     case resp1 of-      Just (pm1, phs1) -> do-       resp2 <- donewp (Just $ scsub2 sc) p2-       case resp2 of-        Just (pm2, phs2) ->-         storeprio node (choosePrioMeta False pm1 pm2) (phs1 ++ phs2)-        resp2@Nothing -> return resp2-      resp1@Nothing -> return resp1-    Sidecondition sidep mainp -> do-     resp1 <- donewp Nothing sidep-     case resp1 of-      Just{} -> do-       resp2 <- donewp node mainp-       case resp2 of-        Just (pm2, phs2) ->-         storeprio node pm2 phs2-        resp2@Nothing -> return resp2-      resp1@Nothing -> return resp1-    Or prio p1 p2 -> do-     cm <- lift $ initMeta-     donewp node (choose (Meta cm) prio p1 p2)-    ConnectHandle (Meta handle) p' -> do-     let Just jnode = node-     umodifyIORef (cthandles jnode) (handle :)-     donewp node p'-    ConnectHandle (NotM _) _ -> __IMPOSSIBLE__--choosePrioMeta :: Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk-choosePrioMeta flip pm1@(PrioMeta p1 _) pm2@(PrioMeta p2 _)-  | p1 > p2 = pm1-  | p2 > p1 = pm2-  | flip = pm2-  | otherwise = pm1-choosePrioMeta _ pm@(PrioMeta _ _) (NoPrio _) = pm-choosePrioMeta _ (NoPrio _) pm@(PrioMeta _ _) = pm-choosePrioMeta _ (NoPrio d1) (NoPrio d2) = NoPrio (d1 && d2)--propagatePrio :: CTree blk -> Undo [OKMeta blk]-propagatePrio node = do-  parent <- lift $ readIORef $ ctparent node-  case parent of-    Nothing     -> return []-    Just parent -> do-      Just sc <- ureadIORef (ctsub parent)-      pm1     <- ureadIORef $ ctpriometa $ scsub1 sc-      pm2     <- ureadIORef $ ctpriometa $ scsub2 sc-      flip    <- ureadIORef $ scflip sc-      let pm = choosePrioMeta flip pm1 pm2-      opm <- ureadIORef (ctpriometa parent)-      if (pm /= opm)-        then do-          uwriteIORef (ctpriometa parent) pm-          phs <- case pm of-            NoPrio True -> ureadIORef (cthandles parent)-            _           -> return []-          phs2 <- propagatePrio parent-          return $ phs ++ phs2-        else-          return []--data Choice = LeftDisjunct | RightDisjunct--choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)-choose c prio p1 p2 =- mmpcase (True, prio, Nothing) c $ \c -> case c of-  LeftDisjunct -> p1-  RightDisjunct -> p2--instance Refinable Choice blk where- refinements _ _ _ = return $ Move 0 . return <$> [LeftDisjunct, RightDisjunct]---instance Refinable OKVal blk where- refinements _ _ _ = __IMPOSSIBLE__ -- OKVal should never be refined----- ------------------------------------

@@ -1,122 +0,0 @@-{-# OPTIONS_GHC -Wunused-imports #-}--module Agda.Auto.Options where--import Data.Char-import Control.Monad.State-import Agda.Utils.Lens--data Mode = MNormal Bool Bool -- true if list mode, true if disprove--          | MCaseSplit--          | MRefine Bool -- true if list mode---data AutoHintMode = AHMNone-                  | AHMModule--type Hints = [String]--newtype TimeOut = TimeOut { getTimeOut :: Int } -- in ms--instance Show TimeOut where-  show = show . getTimeOut---- | Options for Auto, default value and lenses--data AutoOptions = AutoOptions-  { autoHints    :: Hints-  , autoTimeOut  :: TimeOut-  , autoPick     :: Int-  , autoMode     :: Mode-  , autoHintMode :: AutoHintMode-  }--initAutoOptions :: AutoOptions-initAutoOptions = AutoOptions-  { autoHints    = []-  , autoTimeOut  = TimeOut 1000-  , autoPick     = 0-  , autoMode     = MNormal False False-  , autoHintMode = AHMNone-  }--aoHints :: Lens' AutoOptions Hints-aoHints f s =-  f (autoHints s) <&>-  \x -> s {autoHints = x}--aoTimeOut :: Lens' AutoOptions TimeOut-aoTimeOut f s =-  f (autoTimeOut s) <&>-  \x -> s {autoTimeOut = x}--aoPick :: Lens' AutoOptions Int-aoPick f s =-  f (autoPick s) <&>-  \x -> s {autoPick = x}--aoMode :: Lens' AutoOptions Mode-aoMode f s =-  f (autoMode s) <&>-  \x -> s {autoMode = x}--aoHintMode :: Lens' AutoOptions AutoHintMode-aoHintMode f s =-  f (autoHintMode s) <&>-  \x -> s {autoHintMode = x}---- | Tokenising the input (makes `parseArgs` cleaner)--data AutoToken =-    M | C | R | D | L-  | T String | S Int | H String--autoTokens :: [String] -> [AutoToken]-autoTokens []              = []-autoTokens ("-t" : t : ws) = T t        : autoTokens ws-autoTokens ("-s" : s : ws) = S (read s) : autoTokens ws-autoTokens ("-l"     : ws) = L          : autoTokens ws-autoTokens ("-d"     : ws) = D          : autoTokens ws-autoTokens ("-m"     : ws) = M          : autoTokens ws-autoTokens ("-c"     : ws) = C          : autoTokens ws-autoTokens ("-r"     : ws) = R          : autoTokens ws-autoTokens (h        : ws) = H h        : autoTokens ws--parseTime :: String -> Int-parseTime [] = 0-parseTime xs = read ds * modifier + parseTime r where-  (ds , modr) = span isDigit xs-  (mod , r)   = break isDigit modr--  modifier = case mod of-    "ms" -> 1-    "cs" -> 10-    "ds" -> 100-    "s"  -> 1000-    _    -> 1000--parseArgs :: String -> AutoOptions-parseArgs s = mapM_ step (autoTokens $ words s)-              `execState` initAutoOptions where--  step :: AutoToken -> State AutoOptions ()-  step M     = aoHintMode .= AHMModule-  step C     = aoMode     .= MCaseSplit-  step R     = aoPick     .= (-1)-            >> aoMode     .= MRefine False-  step (T t) = aoTimeOut  .= TimeOut (parseTime t)-  step (S p) = aoPick     .= p-  step (H h) = aoHints    %= (h :)-  step D     = do-    mode <- use aoMode-    case mode of-      MNormal lm _ -> aoMode .= MNormal lm True-      _            -> return ()-  step L     = do-    mode <- use aoMode-    case mode of-      MNormal _ dp -> aoMode .= MNormal True dp-      MRefine _    -> aoMode .= MRefine True-      _            -> return ()

@@ -1,451 +0,0 @@-{-# LANGUAGE CPP #-}--{-# OPTIONS_GHC -Wunused-imports #-}-{-# OPTIONS_GHC -Wno-orphans #-}-#if __GLASGOW_HASKELL__ > 907-{-# OPTIONS_GHC -Wno-x-partial #-}-#endif----module Agda.Auto.SearchControl where--import Control.Monad-import Data.IORef-import Control.Monad.State-import Data.Maybe (mapMaybe, fromMaybe)--import Agda.Syntax.Common (Hiding(..))-import Agda.Auto.NarrowingSearch-import Agda.Auto.Syntax--import Agda.Utils.Impossible--instance Refinable (ArgList o) (RefInfo o) where- refinements _ infos _ = return $ fmap (Move 0) $-   [ return ALNil, cons NotHidden, cons Hidden ]-   ++ if getIsDep infos then []-      else [ proj NotHidden, proj Hidden ]--   where--    getIsDep :: [RefInfo o] -> Bool-    getIsDep (x : xs) = case x of-      RICheckElim isDep -> isDep-      _                 -> getIsDep xs-    getIsDep _ = __IMPOSSIBLE__--    proj :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)-    proj hid = ALProj <$> newPlaceholder <*> newPlaceholder-                      <*> return hid     <*> newPlaceholder--    cons :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)-    cons hid = ALCons hid <$> newPlaceholder <*> newPlaceholder---data ExpRefInfo o = ExpRefInfo-  { eriMain           :: Maybe (RefInfo o)-  , eriUnifs          :: [RefInfo o]-  , eriInfTypeUnknown :: Bool-  , eriIsEliminand    :: Bool-  , eriUsedVars       :: Maybe ([UId o], [Elr o])-  , eriIotaStep       :: Maybe Bool-  , eriPickSubsVar    :: Bool-  , eriEqRState       :: Maybe EqReasoningState-  }--initExpRefInfo :: ExpRefInfo o-initExpRefInfo = ExpRefInfo-  { eriMain           = Nothing-  , eriUnifs          = []-  , eriInfTypeUnknown = False-  , eriIsEliminand    = False-  , eriUsedVars       = Nothing-  , eriIotaStep       = Nothing-  , eriPickSubsVar    = False-  , eriEqRState       = Nothing-  }--getinfo :: [RefInfo o] -> ExpRefInfo o-getinfo = foldl step initExpRefInfo where--  step :: ExpRefInfo o -> RefInfo o -> ExpRefInfo o-  step eri x@RIMainInfo{}           = eri { eriMain  = Just x }-  step eri x@RIUnifInfo{}           = eri { eriUnifs = x : eriUnifs eri }-  step eri RIInferredTypeUnknown    = eri { eriInfTypeUnknown = True }-  step eri RINotConstructor         = eri { eriIsEliminand = True }-  step eri (RIUsedVars nuids nused) = eri { eriUsedVars = Just (nuids, nused) }-  step eri (RIIotaStep semif)       = eri { eriIotaStep = Just iota' } where-    iota' = semif || (Just True ==) (eriIotaStep eri)-  step eri RIPickSubsvar            = eri { eriPickSubsVar = True }-  step eri (RIEqRState s)           = eri { eriEqRState = Just s }-  step eri _ = __IMPOSSIBLE__----- | @univar sub v@ figures out what the name of @v@ "outside" of---   the substitution @sub@ ought to be, if anything.--univar :: [CAction o] -> Nat -> Maybe Nat-univar cl v = getOutsideName cl v 0 where--  getOutsideName :: [CAction o] -> Nat -> Nat -> Maybe Nat-  -- @v@ is offset by @v'@ binders-  getOutsideName []            v v' = Just (v' + v)-  -- @v@ was introduced by the weakening: disappears-  getOutsideName (Weak n : _)  v v' | v < n = Nothing-  -- @v@ was introduced before the weakening: strengthened-  getOutsideName (Weak n : xs) v v' = getOutsideName xs (v - n) v'-  -- Name of @v@ before the substitution was pushed in-  -- had to be offset by 1-  getOutsideName (Sub _  : xs) v v' = getOutsideName xs v (v' + 1)-  -- If this is the place where @v@ was bound, it used to-  -- be called 0 + offset of all the vars substituted for-  getOutsideName (Skip   : _)  0 v' = Just v'-  -- Going over a binder: de Bruijn name of @v@ decreased-  -- but offset increased-  getOutsideName (Skip   : xs) v v' = getOutsideName xs (v - 1) (v' + 1)---- | List of the variables instantiated by the substitution-subsvars :: [CAction o] -> [Nat]-subsvars = f 0 where--  f :: Nat -> [CAction o] -> [Nat]-  f n []            = []-  f n (Weak _ : xs) = f n xs -- why?-  f n (Sub _  : xs) = n : f (n + 1) xs-  f n (Skip   : xs) = f (n + 1) xs---- | Moves---   A move is composed of a @Cost@ together with an action---   computing the refined problem.--type Move o = Move' (RefInfo o) (Exp o)---- | New constructors---   Taking a step towards a solution consists in picking a---   constructor and filling in the missing parts with---   placeholders to be discharged later on.--newAbs :: MId -> RefCreateEnv blk (Abs (MM a blk))-newAbs mid = Abs mid <$> newPlaceholder--newLam :: Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)-newLam hid mid = Lam hid <$> newAbs mid--newPi :: UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)-newPi uid dep hid = Pi (Just uid) hid dep <$> newPlaceholder <*> newAbs NoId--foldArgs :: [(Hiding, MExp o)] -> MArgList o-foldArgs = foldr (\ (h, a) sp -> NotM $ ALCons h a sp) (NotM ALNil)---- | New spine of arguments potentially using placeholders--newArgs' :: [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)-newArgs' h tms = foldArgs . zip h . (++ tms) <$> replicateM size newPlaceholder-  where size = length h - length tms--newArgs :: [Hiding] -> RefCreateEnv (RefInfo o) (MArgList o)-newArgs h = newArgs' h []---- | New @App@lication node using a new spine of arguments---   respecting the @Hiding@ annotation--newApp' :: UId o -> ConstRef o -> [Hiding] -> [MExp o] ->-           RefCreateEnv (RefInfo o) (Exp o)-newApp' meta cst hds tms =-  App (Just meta) <$> newOKHandle <*> return (Const cst) <*> newArgs' hds tms--newApp :: UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)-newApp meta cst hds = newApp' meta cst hds []---- | Equality reasoning steps---   The begin token is accompanied by two steps because---   it does not make sense to have a derivation any shorter---   than that.--eqStep :: UId o -> EqReasoningConsts o -> Move o-eqStep meta eqrc = Move costEqStep $ newApp meta (eqrcStep eqrc)-  [Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden, NotHidden]--eqEnd :: UId o -> EqReasoningConsts o -> Move o-eqEnd meta eqrc = Move costEqEnd $ newApp meta (eqrcEnd eqrc)-  [Hidden, Hidden, NotHidden]--eqCong :: UId o -> EqReasoningConsts o -> Move o-eqCong meta eqrc = Move costEqCong $ newApp meta (eqrcCong eqrc)-  [Hidden, Hidden, Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden]--eqSym :: UId o -> EqReasoningConsts o -> Move o-eqSym meta eqrc = Move costEqSym $ newApp meta (eqrcSym eqrc)-  [Hidden, Hidden, Hidden, Hidden, NotHidden]--eqBeginStep2 :: UId o -> EqReasoningConsts o -> Move o-eqBeginStep2 meta eqrc = Move costEqStep $ do-  e1 <- newApp meta (eqrcStep eqrc)-          [Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden, NotHidden]-  e2 <- newApp' meta (eqrcStep eqrc)-          [Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden, NotHidden]-          [NotM e1]-  newApp' meta (eqrcBegin eqrc) [Hidden, Hidden, Hidden, Hidden, NotHidden]-    [NotM e2]----- | Pick the first unused UId amongst the ones you have seen (GA: ??)---   Defaults to the head of the seen ones.--pickUid :: forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)-pickUid used seen = maybe (head seen, False) (, True) $ firstUnused seen where-  {- ?? which uid to pick -}--  firstUnused :: [Maybe (UId o)] -> Maybe (Maybe (UId o))-  firstUnused []                 = Nothing-  firstUnused (Nothing     : _)  = Just Nothing-  firstUnused (mu@(Just u) : us) =-    if u `elem` used then firstUnused us else Just mu--instance Refinable (Exp o) (RefInfo o) where- refinements envinfo infos meta =-  let-   hints = rieHints envinfo-   deffreevars = rieDefFreeVars envinfo--   meqr = rieEqReasoningConsts envinfo--   ExpRefInfo { eriMain  = Just (RIMainInfo n tt iotastepdone)-              , eriUnifs = unis-              , eriInfTypeUnknown = inftypeunknown-              , eriIsEliminand = iseliminand -- TODO:: Defined but not used-              , eriUsedVars = Just (uids, usedvars)-              , eriIotaStep = iotastep-              , eriPickSubsVar = picksubsvar -- TODO:: Defined but not used-              , eriEqRState = meqrstate-              } = getinfo infos--   eqrstate = fromMaybe EqRSNone meqrstate--   set l = return $ Sort (Set l)-  in case unis of-   [] ->-    let--     eqr = fromMaybe __IMPOSSIBLE__ meqr-     eq_end         = eqEnd  meta eqr-     eq_step        = eqStep meta eqr-     eq_cong        = eqCong meta eqr-     eq_sym         = eqSym  meta eqr-     eq_begin_step2 = eqBeginStep2 meta eqr--     adjustCost i = if inftypeunknown then costInferredTypeUnkown else i-     varcost v | v < n - deffreevars = adjustCost $-       if v `elem` (mapMaybe getVar usedvars)-       then costAppVarUsed else costAppVar-     varcost v | otherwise           = adjustCost costAppHint-     varapps  = map (\ v -> Move (varcost v) $ app n meta Nothing (Var v)) [0..n - 1]-     hintapps = map (\(c, hm) -> Move (cost c hm) (app n meta Nothing (Const c))) hints-       where-         cost :: ConstRef o -> HintMode -> Cost-         cost c hm = adjustCost $ case (iotastep , hm) of-           (Just _  , _       ) -> costIotaStep-           (Nothing , HMNormal) ->-             if c `elem` (mapMaybe getConst usedvars)-             then costAppHintUsed else costAppHint-           (Nothing , HMRecCall) ->-             if c `elem` (mapMaybe getConst usedvars)-             then costAppRecCallUsed else costAppRecCall-     generics = varapps ++ hintapps-    in case rawValue tt of--     _ | eqrstate == EqRSChain ->-      return [eq_end, eq_step]--     HNPi hid _ _ (Abs id _) -> return $-         Move (adjustCost (if iotastepdone then costLamUnfold else costLam)) (newLam hid id)-       : Move costAbsurdLam (return $ AbsurdLambda hid)-       : generics--     HNSort (Set l) -> return $-          map (Move (adjustCost costSort) . set) [0..l - 1]-       ++ map (Move (adjustCost costPi) . newPi meta True) [NotHidden, Hidden]-       ++ generics---     HNApp (Const c) _ -> do-      cd <- readIORef c-      return $ case cdcont cd of--       Datatype cons _ | eqrstate == EqRSNone ->-         map (\c -> Move (adjustCost $ case iotastep of-                                         Just True -> costUnification-                                         _ -> if length cons <= 1-                                              then costAppConstructorSingle-                                              else costAppConstructor)-                         $ app n meta Nothing (Const c)) cons-         ++ generics-         ++ (guard (maybe False ((c ==) . eqrcId) meqr)-            *> [eq_sym, eq_cong, eq_begin_step2])--       _ | eqrstate == EqRSPrf1 -> generics ++ [eq_sym, eq_cong]-       _ | eqrstate == EqRSPrf2 -> generics ++ [eq_cong]--       _ -> generics-     _ -> return generics-   (RIUnifInfo cl hne : _) ->-    let-     subsvarapps = map (Move costUnification . app n meta Nothing . Var) (subsvars cl)-     mlam = case rawValue tt of-      HNPi hid _ _ (Abs id _) -> [Move costUnification (newLam hid id)]-      _ -> []-     generics = mlam ++ subsvarapps--    in-     return $ case rawValue hne of-      HNApp (Var v) _ ->-       let (uid, isunique) = pickUid uids $ seenUIds hne-           uni = case univar cl v of-                  Just v | v < n -> [Move (costUnificationIf isunique) $ app n meta uid (Var v)]-                  _ -> []-       in uni ++ generics-      HNApp (Const c) _ ->-       let (uid, isunique) = pickUid uids $ seenUIds hne-       in Move (costUnificationIf isunique) (app n meta uid (Const c)) : generics-      HNLam{} -> generics-      HNPi hid possdep _ _ ->-       let (uid, isunique) = pickUid uids $ seenUIds hne-       in Move (costUnificationIf isunique) (newPi (fromMaybe meta uid) possdep hid) : generics-      HNSort (Set l) -> map (Move costUnification . set) [0..l] ++ generics-      HNSort _ -> generics-   _ -> __IMPOSSIBLE__--  where--    app :: Nat -> UId o -> Maybe (UId o) -> Elr o ->-           RefCreateEnv (RefInfo o) (Exp o)-    app n meta muid elr = do-      p <- newPlaceholder-      p <- case elr of-        Var{}   -> return p-        Const c -> do-          cd <- RefCreateEnv $ lift $ readIORef c-          let dfvapp 0 _ = p-              dfvapp i n = NotM $ ALCons NotHidden-                          (NotM $ App Nothing (NotM $ OKVal) (Var n) (NotM ALNil))-                          (dfvapp (i - 1) (n - 1))-         -- NotHidden is ok because agda reification throws these arguments-         -- away and agsy skips typechecking them-          return $ dfvapp (cddeffreevars cd) (n - 1)-      okh <- newOKHandle-      return $ App (Just $ fromMaybe meta muid) okh elr p---extraref :: UId o -> [Maybe (UId o)] -> ConstRef o -> Move o-extraref meta seenuids c = Move costAppExtraRef $ app (head seenuids) (Const c)- where-   app muid elr = App (Just $ fromMaybe meta muid)-              <$> newOKHandle <*> return elr <*> newPlaceholder--instance Refinable (ICExp o) (RefInfo o) where- refinements _ infos _ =-  let (RICopyInfo e : _) = infos-  in return [Move 0 (return e)]---instance Refinable (ConstRef o) (RefInfo o) where- refinements _ [RICheckProjIndex projs] _ = return $ map (Move 0 . return) projs- refinements _ _ _ = __IMPOSSIBLE__----- -----------------------------------costIncrease, costUnificationOccurs, costUnification, costAppVar,-  costAppVarUsed, costAppHint, costAppHintUsed, costAppRecCall,-  costAppRecCallUsed, costAppConstructor, costAppConstructorSingle,-  costAppExtraRef, costLam, costLamUnfold, costPi, costSort, costIotaStep,-  costInferredTypeUnkown, costAbsurdLam-  :: Cost--costUnificationIf :: Bool -> Cost-costUnificationIf b = if b then costUnification else costUnificationOccurs--costIncrease = 1000-costUnificationOccurs = 100 -- 1000001 -- 1 -- 100-costUnification = 0000-costAppVar = 0000 -- 0, 1-costAppVarUsed = 1000 -- 5-costAppHint = 3000 -- 2, 5-costAppHintUsed = 5000-costAppRecCall = 0 -- 1000?-costAppRecCallUsed = 10000 -- 1000?-costAppConstructor = 1000-costAppConstructorSingle = 0000-costAppExtraRef = 1000-costLam = 0000 -- 1, 0-costLamUnfold = 1000 -- 1, 0-costPi = 1000003 -- 100 -- 5-costSort = 1000004 -- 0-costIotaStep = 3000 -- 1000005 -- 2 -- 100-costInferredTypeUnkown = 1000006 -- 100-costAbsurdLam = 0--costEqStep, costEqEnd, costEqSym, costEqCong :: Cost-costEqStep = 2000-costEqEnd = 0-costEqSym = 0-costEqCong = 500--prioNo, prioTypeUnknown, prioTypecheckArgList, prioInferredTypeUnknown,-  prioCompBeta, prioCompBetaStructured, prioCompareArgList, prioCompIota,-  prioCompChoice, prioCompUnif, prioCompCopy, prioNoIota, prioAbsurdLambda,-  prioProjIndex-  :: Prio-prioNo = (-1)-prioTypeUnknown = 0-prioTypecheckArgList = 3000-prioInferredTypeUnknown = 4000-prioCompBeta = 4000-prioCompBetaStructured = 4000-prioCompIota = 4000-prioCompChoice = 5000 -- 700 -- 5000-prioCompUnif = 6000 -- 2-prioCompCopy = 8000-prioCompareArgList = 7000 -- 5 -- 2-prioNoIota = 500 -- 500-prioAbsurdLambda = 1000--prioProjIndex = 3000--prioTypecheck :: Bool -> Prio-prioTypecheck False = 1000-prioTypecheck True = 0---- -----------------------------------instance Trav a => Trav [a] where-  type Block [a] = Block a-  trav _ []     = return ()-  trav f (x:xs) = trav f x >> trav f xs--instance Trav (MId, CExp o) where-  type Block (MId, CExp o) = RefInfo o-  trav f (_, ce) = trav f ce--instance Trav (TrBr a o) where-  type Block (TrBr a o) = RefInfo o-  trav f (TrBr es _) = trav f es--instance Trav (Exp o) where-  type Block (Exp o) = RefInfo o-  trav f = \case-    App _ _ _ args         -> trav f args-    Lam _ (Abs _ b)        -> trav f b-    Pi _ _ _ it (Abs _ ot) -> trav f it >> trav f ot-    Sort _                 -> return ()-    AbsurdLambda{}         -> return ()--instance Trav (ArgList o) where-  type Block (ArgList o) = RefInfo o-  trav _ ALNil               = return ()-  trav f (ALCons _ arg args) = trav f arg >> trav f args-  trav f (ALProj eas _ _ as) = trav f eas >> trav f as-  trav f (ALConPar args)     = trav f args---- ---------------------------------

@@ -1,463 +0,0 @@-{-# OPTIONS_GHC -Wunused-imports #-}--module Agda.Auto.Syntax where--import Data.IORef-import qualified Data.Set as Set--import Agda.Syntax.Common (Hiding)-import Agda.Auto.NarrowingSearch--import Agda.Utils.Impossible---- | Unique identifiers for variable occurrences in unification.-type UId o = Metavar (Exp o) (RefInfo o)--data HintMode = HMNormal-              | HMRecCall--data EqReasoningConsts o = EqReasoningConsts-  { eqrcId    -- "_≡_"-  , eqrcBegin -- "begin_"-  , eqrcStep  -- "_≡⟨_⟩_"-  , eqrcEnd   -- "_∎"-  , eqrcSym   -- "sym"-  , eqrcCong  -- "cong"-  :: ConstRef o-  }--data EqReasoningState = EqRSNone | EqRSChain | EqRSPrf1 | EqRSPrf2 | EqRSPrf3- deriving (Eq, Show)---- | The concrete instance of the 'blk' parameter in 'Metavar'.---   I.e., the information passed to the search control.--data RefInfo o-  = RIEnv-    { rieHints :: [(ConstRef o, HintMode)]-    , rieDefFreeVars :: Nat-      -- ^ Nat - deffreevars-      --   (to make cost of using module parameters correspond to that of hints).-    , rieEqReasoningConsts :: Maybe (EqReasoningConsts o)-    }-  | RIMainInfo-    { riMainCxtLength :: Nat-      -- ^ Size of typing context in which meta was created.-    , riMainType      :: HNExp o-      -- ^ Head normal form of type of meta.-    , riMainIota      :: Bool-       -- ^ True if iota steps performed when normalising target type-       --   (used to put cost when traversing a definition-       --    by construction instantiation).-    }-  | RIUnifInfo [CAction o] (HNExp o)-    -- meta environment, opp hne-  | RICopyInfo (ICExp o)-  | RIIotaStep Bool -- True - semiflex-  | RIInferredTypeUnknown-  | RINotConstructor-  | RIUsedVars [UId o] [Elr o]-  | RIPickSubsvar--  | RIEqRState EqReasoningState---  | RICheckElim Bool -- isdep-  | RICheckProjIndex [ConstRef o] -- noof proj functions---type MyPB o = PB (RefInfo o)-type MyMB a o = MB a (RefInfo o)--type Nat = Int--data MId = Id String-         | NoId---- | Abstraction with maybe a name.------   Different from Agda, where there is also info---   whether function is constant.-data Abs a = Abs MId a---- | Constant signatures.--data ConstDef o = ConstDef-  { cdname        :: String-    -- ^ For debug printing.-  , cdorigin      :: o-    -- ^ Reference to the Agda constant.-  , cdtype        :: MExp o-    -- ^ Type of constant.-  , cdcont        :: DeclCont o-    -- ^ Constant definition.-  , cddeffreevars :: Nat-    -- ^ Free vars of the module where the constant is defined..-  } -- contains no metas---- | Constant definitions.--data DeclCont o-  = Def Nat [Clause o] (Maybe Nat) -- maybe an index to elimand argument-                       (Maybe Nat) -- maybe index to elim arg if semiflex-  | Datatype [ConstRef o] -- constructors-             [ConstRef o] -- projection functions (in case it is a record)--  | Constructor Nat -- number of omitted args-  | Postulate--type Clause o = ([Pat o], MExp o)--data Pat o-  = PatConApp (ConstRef o) [Pat o]-  | PatVar String-  | PatExp-    -- ^ Dot pattern.-  | PatProj (ConstRef o)-    -- ^ Projection pattern.--type ConstRef o = IORef (ConstDef o)---- | Head of application (elimination).-data Elr o-  = Var Nat-  | Const (ConstRef o)-  deriving (Eq)--getVar :: Elr o -> Maybe Nat-getVar (Var n) = Just n-getVar Const{} = Nothing--getConst :: Elr o -> Maybe (ConstRef o)-getConst (Const c) = Just c-getConst Var{}     = Nothing--data Sort-  = Set Nat-  | UnknownSort-  | Type---- | Agsy's internal syntax.-data Exp o-  = App-    { appUId   :: Maybe (UId o)-      -- ^ Unique identifier of the head.-    , appOK    :: OKHandle (RefInfo o)-      -- ^ This application has been type-checked.-    , appHead  :: Elr o-      -- ^ Head.-    , appElims :: MArgList o-      -- ^ Arguments.-    }-  | Lam Hiding (Abs (MExp o))-    -- ^ Lambda with hiding information.-  | Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o))-    -- ^ @True@ if possibly dependent (var not known to not occur).-    --   @False@ if non-dependent.-  | Sort Sort-  | AbsurdLambda Hiding-    -- ^ Absurd lambda with hiding information.--dontCare :: Exp o-dontCare = Sort UnknownSort---- | "Maybe expression":  Expression or reference to meta variable.-type MExp o = MM (Exp o) (RefInfo o)--data ArgList o-  = ALNil-    -- ^ No more eliminations.-  | ALCons Hiding (MExp o) (MArgList o)-    -- ^ Application and tail.--  | ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o)-    -- ^ proj pre args, projfcn idx, tail--  | ALConPar (MArgList o)-    -- ^ Constructor parameter (missing in Agda).-    --   Agsy has monomorphic constructors.-    --   Inserted to cover glitch of polymorphic constructor-    --   applications coming from Agda--type MArgList o = MM (ArgList o) (RefInfo o)--data WithSeenUIds a o = WithSeenUIds-  { seenUIds :: [Maybe (UId o)]-  , rawValue :: a-  }--type HNExp o = WithSeenUIds (HNExp' o) o--data HNExp' o =-    HNApp  (Elr o) (ICArgList o)-  | HNLam  Hiding (Abs (ICExp o))-  | HNPi   Hiding Bool (ICExp o) (Abs (ICExp o))-  | HNSort Sort---- | Head-normal form of 'ICArgList'.  First entry is exposed.------   Q: Why are there no projection eliminations?-data HNArgList o = HNALNil-                 | HNALCons Hiding (ICExp o) (ICArgList o)-                 | HNALConPar (ICArgList o)---- | Lazy concatenation of argument lists under explicit substitutions.-data ICArgList o = CALNil-                 | CALConcat (Clos (MArgList o) o) (ICArgList o)---- | An expression @a@ in an explicit substitution @[CAction a]@.-type ICExp o  = Clos (MExp o) o-data Clos a o = Clos [CAction o] a--type CExp o   = TrBr (ICExp o) o-data TrBr a o = TrBr [MExp o] a---- | Entry of an explicit substitution.------   An explicit substitution is a list of @CAction@s.---   This is isomorphic to the usual presentation where---   @Skip@ and @Weak@ would be constructors of exp. substs.--data CAction o-  = Sub (ICExp o)-    -- ^ Instantation of variable.-  | Skip-    -- ^ For going under a binder, often called "Lift".-  | Weak Nat-    -- ^ Shifting substitution (going to a larger context).--type Ctx o = [(MId, CExp o)]--type EE = IO---- ---------------------------------------------detecteliminand :: [Clause o] -> Maybe Nat-detecteliminand cls =- case map cleli cls of-  [] -> Nothing-  (i:is) -> if all (i ==) is then i else Nothing- where-  cleli (pats, _) = pateli 0 pats-  pateli i (PatConApp _ args : pats) = if all notcon (args ++ pats) then Just i else Nothing-  pateli i (_ : pats) = pateli (i + 1) pats-  pateli i [] = Nothing-  notcon PatConApp{} = False-  notcon _ = True--detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool-detectsemiflex _ _ = return False -- disabled--categorizedecl :: ConstRef o -> IO ()-categorizedecl c = do- cd <- readIORef c- case cdcont cd of-  Def narg cls _ _ -> do-   semif <- detectsemiflex c cls-   let elim = detecteliminand cls-       semifb = case (semif, elim) of-                 (True, Just i) -> Just i -- just copying val of elim arg. this should be changed-                 (_, _) -> Nothing-   writeIORef c (cd {cdcont = Def narg cls elim semifb})-  _ -> return ()---- ---------------------------------------------class MetaliseOKH t where-  metaliseOKH :: t -> IO t--instance MetaliseOKH t => MetaliseOKH (MM t a) where-  metaliseOKH = \case-    Meta m -> return $ Meta m-    NotM e -> NotM <$> metaliseOKH e--instance MetaliseOKH t => MetaliseOKH (Abs t) where-  metaliseOKH (Abs id b) = Abs id <$> metaliseOKH b--instance MetaliseOKH (Exp o) where-  metaliseOKH = \case-    App uid okh elr args ->-      (\ m -> App uid m elr) <$> (Meta <$> initMeta) <*> metaliseOKH args-    Lam hid b -> Lam hid <$> metaliseOKH b-    Pi uid hid dep it ot ->-      Pi uid hid dep <$> metaliseOKH it <*> metaliseOKH ot-    e@Sort{} -> return e-    e@AbsurdLambda{} -> return e--instance MetaliseOKH (ArgList o) where-  metaliseOKH = \case-    ALNil -> return ALNil-    ALCons hid a as -> ALCons hid <$> metaliseOKH a <*> metaliseOKH as-    ALProj eas idx hid as ->-      (\ eas -> ALProj eas idx hid) <$> metaliseOKH eas <*> metaliseOKH as-    ALConPar as -> ALConPar <$> metaliseOKH as--metaliseokh :: MExp o -> IO (MExp o)-metaliseokh = metaliseOKH---- ---------------------------------------------class ExpandMetas t where-  expandMetas :: t -> IO t--instance ExpandMetas t => ExpandMetas (MM t a) where-  expandMetas = \case-    NotM e -> NotM <$> expandMetas e-    Meta m -> do-      mb <- readIORef (mbind m)-      case mb of-        Nothing -> return $ Meta m-        Just e  -> NotM <$> expandMetas e--instance ExpandMetas t => ExpandMetas (Abs t) where-  expandMetas (Abs id b) = Abs id <$> expandMetas b--instance ExpandMetas (Exp o) where-  expandMetas = \case-    App uid okh elr args -> App uid okh elr <$> expandMetas args-    Lam hid b -> Lam hid <$> expandMetas b-    Pi uid hid dep it ot ->-      Pi uid hid dep <$> expandMetas it <*> expandMetas ot-    t@Sort{} -> return t-    t@AbsurdLambda{} -> return t--instance ExpandMetas (ArgList o) where-  expandMetas = \case-    ALNil -> return ALNil-    ALCons hid a as -> ALCons hid <$> expandMetas a <*> expandMetas as-    ALProj eas idx hid as ->-      (\ a b -> ALProj a b hid) <$> expandMetas eas-      <*> expandbind idx <*> expandMetas as-    ALConPar as -> ALConPar <$> expandMetas as---- -----------------------------------addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o-addtrailingargs newargs CALNil = CALConcat newargs CALNil-addtrailingargs newargs (CALConcat x xs) = CALConcat x (addtrailingargs newargs xs)---- -----------------------------------closify :: MExp o -> CExp o-closify e = TrBr [e] (Clos [] e)--sub :: MExp o -> CExp o -> CExp o--- sub e (Clos [] x) = Clos [Sub e] x-sub e (TrBr trs (Clos (Skip : as) x)) = TrBr (e : trs) (Clos (Sub (Clos [] e) : as) x)-{-sub e (Clos (Weak n : as) x) = if n == 1 then-                                Clos as x-                               else-                                Clos (Weak (n - 1) : as) x-}-sub _ _ = __IMPOSSIBLE__--subi :: MExp o -> ICExp o -> ICExp o-subi e (Clos (Skip : as) x) = Clos (Sub (Clos [] e) : as) x-subi _ _ = __IMPOSSIBLE__--weak :: Weakening t => Nat -> t -> t-weak 0 = id-weak n = weak' n--class Weakening t where-  weak' :: Nat -> t -> t--instance Weakening a => Weakening (TrBr a o) where-  weak' n (TrBr trs e) = TrBr trs (weak' n e)--instance Weakening (Clos a o) where-  weak' n (Clos as x) = Clos (Weak n : as) x--instance Weakening (ICArgList o) where-  weak' n = \case-    CALNil         -> CALNil-    CALConcat a as -> CALConcat (weak' n a) (weak' n as)--instance Weakening (Elr o) where-  weak' n = rename (n +)---- | Substituting for a variable.-doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)-doclos = f 0- where-  -- ns is the number of weakenings-  f ns []            i = Left (ns + i)-  f ns (Weak n : xs) i = f (ns + n) xs i-  f ns (Sub s  : _ ) 0 = Right (weak ns s)-  f ns (Skip   : _ ) 0 = Left ns-  f ns (Skip   : xs) i = f (ns + 1) xs (i - 1)-  f ns (Sub _  : xs) i = f ns xs (i - 1)----- | FreeVars class and instances--freeVars :: FreeVars t => t -> Set.Set Nat-freeVars = freeVarsOffset 0--class FreeVars t where-  freeVarsOffset :: Nat -> t -> Set.Set Nat--instance (FreeVars a, FreeVars b) => FreeVars (a, b) where-  freeVarsOffset n (a, b) = Set.union (freeVarsOffset n a) (freeVarsOffset n b)--instance FreeVars t => FreeVars (MM t a) where-  freeVarsOffset n e = freeVarsOffset n (rm __IMPOSSIBLE__ e)--instance FreeVars t => FreeVars (Abs t) where-  freeVarsOffset n (Abs id e) = freeVarsOffset (n + 1) e--instance FreeVars (Elr o) where-  freeVarsOffset n = \case-    Var v   -> Set.singleton (v - n)-    Const{} -> Set.empty--instance FreeVars (Exp o) where-  freeVarsOffset n = \case-   App _ _ elr args -> freeVarsOffset n (elr, args)-   Lam _ b          -> freeVarsOffset n b-   Pi _ _ _ it ot   -> freeVarsOffset n (it, ot)-   Sort{}           -> Set.empty-   AbsurdLambda{}   -> Set.empty--instance FreeVars (ArgList o) where-  freeVarsOffset n es = case es of-    ALNil         -> Set.empty-    ALCons _ e es -> freeVarsOffset n (e, es)-    ALConPar es   -> freeVarsOffset n es-    ALProj{}      -> __IMPOSSIBLE__----- | Renaming Typeclass and instances-rename :: Renaming t => (Nat -> Nat) -> t -> t-rename = renameOffset 0--class Renaming t where-  renameOffset :: Nat -> (Nat -> Nat) -> t -> t--instance (Renaming a, Renaming b) => Renaming (a, b) where-  renameOffset j ren (a, b) = (renameOffset j ren a, renameOffset j ren b)--instance Renaming t => Renaming (MM t a) where-  renameOffset j ren e = NotM $ renameOffset j ren (rm __IMPOSSIBLE__ e)--instance Renaming t => Renaming (Abs t) where-  renameOffset j ren (Abs id e) = Abs id $ renameOffset (j + 1) ren e--instance Renaming (Elr o) where-  renameOffset j ren = \case-    Var v | v >= j -> Var (ren (v - j) + j)-    e              -> e--instance Renaming (Exp o) where-  renameOffset j ren = \case-    App uid ok elr args -> uncurry (App uid ok) $ renameOffset j ren (elr, args)-    Lam hid e -> Lam hid (renameOffset j ren e)-    Pi a b c it ot -> uncurry (Pi a b c) $ renameOffset j ren (it, ot)-    e@Sort{}         -> e-    e@AbsurdLambda{} -> e--instance Renaming (ArgList o) where-  renameOffset j ren = \case-    ALNil           -> ALNil-    ALCons hid a as -> uncurry (ALCons hid) $ renameOffset j ren (a, as)-    ALConPar as     -> ALConPar (renameOffset j ren as)-    ALProj{}        -> __IMPOSSIBLE__