From eed4c344441c796a9e9e0a7e4375fc597d0d5bfa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Tue, 30 May 2023 14:01:30 +0200 Subject: [PATCH 1/6] =?UTF-8?q?Update=20blockOnMeta=20=E2=86=92=20blockTC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/ci-ubuntu.yml | 2 +- src/Reflection/TCM.agda | 6 ++++-- src/Tactic/Cong.agda | 2 +- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 2b08c7d6e6..45fab62778 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -79,7 +79,7 @@ jobs: elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \ || '${{ github.base_ref }}' == 'experimental' ]]; then # Pick Agda version for experimental - echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> $GITHUB_ENV; + echo "AGDA_COMMIT=481361ab76163e2245e5deb37f396d4ac15bbecc" >> $GITHUB_ENV; echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV fi diff --git a/src/Reflection/TCM.agda b/src/Reflection/TCM.agda index a3df1f1bc3..8402a9543d 100644 --- a/src/Reflection/TCM.agda +++ b/src/Reflection/TCM.agda @@ -28,8 +28,10 @@ open Builtin public ; catchTC; quoteTC; unquoteTC ; getContext; extendContext; inContext; freshName ; declareDef; declarePostulate; defineFun; getType; getDefinition - ; blockOnMeta; commitTC; isMacro; withNormalisation - ; debugPrint; noConstraints; runSpeculative) + ; blockTC; commitTC; isMacro; withNormalisation + ; debugPrint; noConstraints; runSpeculative + ; Blocker ; blockerMeta ; blockAny ; blockAll + ) renaming (returnTC to pure) open Format public diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 5a545a4c77..856b4cdc56 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -98,7 +98,7 @@ private destructEqualityGoal goal@(def (quote _≡_) (lvl ∷ tp ∷ lhs ∷ rhs ∷ [])) = pure $ equals (unArg lvl) (unArg tp) (unArg lhs) (unArg rhs) destructEqualityGoal (meta m args) = - blockOnMeta m + blockTC (blockerMeta m) destructEqualityGoal goal = notEqualityError goal From 32b5937a4721d630a0e524df14682c2a38aa016c Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sun, 20 Aug 2023 13:42:26 +0900 Subject: [PATCH 2/6] Update ci-ubuntu.yml to latest version of Agda --- .github/workflows/ci-ubuntu.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 45fab62778..9d89793bcc 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -79,7 +79,7 @@ jobs: elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \ || '${{ github.base_ref }}' == 'experimental' ]]; then # Pick Agda version for experimental - echo "AGDA_COMMIT=481361ab76163e2245e5deb37f396d4ac15bbecc" >> $GITHUB_ENV; + echo "AGDA_COMMIT=84b6bb2e90f2774ce9792fde2bc6238f27aea389" >> $GITHUB_ENV; echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV fi From a0a74ec39158b1635d0ca744f97ae3b38449cd7b Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Fri, 13 Oct 2023 10:59:47 +0900 Subject: [PATCH 3/6] Undo bump of experimental --- .github/workflows/ci-ubuntu.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 9d89793bcc..2b08c7d6e6 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -79,7 +79,7 @@ jobs: elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \ || '${{ github.base_ref }}' == 'experimental' ]]; then # Pick Agda version for experimental - echo "AGDA_COMMIT=84b6bb2e90f2774ce9792fde2bc6238f27aea389" >> $GITHUB_ENV; + echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> $GITHUB_ENV; echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV fi From 9a598e980e505bcf2255713c7633a3c3908fe6b3 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Fri, 13 Oct 2023 11:40:12 +0900 Subject: [PATCH 4/6] Ensure backwards compatability --- src/Reflection/TCM.agda | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/Reflection/TCM.agda b/src/Reflection/TCM.agda index 8402a9543d..a263460f1a 100644 --- a/src/Reflection/TCM.agda +++ b/src/Reflection/TCM.agda @@ -8,8 +8,9 @@ module Reflection.TCM where +open import Agda.Builtin.Reflection as Builtin using (Meta) + open import Reflection.AST.Term -import Agda.Builtin.Reflection as Builtin import Reflection.TCM.Format as Format ------------------------------------------------------------------------ @@ -28,9 +29,9 @@ open Builtin public ; catchTC; quoteTC; unquoteTC ; getContext; extendContext; inContext; freshName ; declareDef; declarePostulate; defineFun; getType; getDefinition - ; blockTC; commitTC; isMacro; withNormalisation + ; commitTC; isMacro; withNormalisation ; debugPrint; noConstraints; runSpeculative - ; Blocker ; blockerMeta ; blockAny ; blockAll + ; Blocker ; blockTC; blockerMeta ; blockerAny ; blockerAll ) renaming (returnTC to pure) @@ -42,3 +43,6 @@ open Format public newMeta : Type → TC Term newMeta = checkType unknown + +blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A +blockOnMeta m = blockTC (blockerMeta m) From 0e3458ca9e07d355c6fc2043a131abf833bbccf1 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Fri, 13 Oct 2023 11:43:33 +0900 Subject: [PATCH 5/6] Ensure backwardwards compatibility --- CHANGELOG.md | 9 +++++++++ src/Reflection/TCM.agda | 9 +++------ 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6bfd659aa9..d012d754a2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3801,6 +3801,15 @@ This is a full list of proofs that have changed form to use irrelevant instance WellFounded _<_ → Irreflexive _≈_ _<_ ``` +* Added new types and operations to `Reflection.TCM`: + ``` + Blocker : Set + blockerMeta : Meta → Blocker + blockerAny : List Blocker → Blocker + blockerAll : List Blocker → Blocker + blockTC : Blocker → TC A + ``` + * Added new file `Relation.Binary.Reasoning.Base.Apartness` This is how to use it: diff --git a/src/Reflection/TCM.agda b/src/Reflection/TCM.agda index a263460f1a..d762dab2c5 100644 --- a/src/Reflection/TCM.agda +++ b/src/Reflection/TCM.agda @@ -8,7 +8,7 @@ module Reflection.TCM where -open import Agda.Builtin.Reflection as Builtin using (Meta) +import Agda.Builtin.Reflection as Builtin open import Reflection.AST.Term import Reflection.TCM.Format as Format @@ -29,9 +29,9 @@ open Builtin public ; catchTC; quoteTC; unquoteTC ; getContext; extendContext; inContext; freshName ; declareDef; declarePostulate; defineFun; getType; getDefinition - ; commitTC; isMacro; withNormalisation + ; blockOnMeta; commitTC; isMacro; withNormalisation ; debugPrint; noConstraints; runSpeculative - ; Blocker ; blockTC; blockerMeta ; blockerAny ; blockerAll + ; Blocker; blockerMeta; blockerAny; blockerAll; blockTC ) renaming (returnTC to pure) @@ -43,6 +43,3 @@ open Format public newMeta : Type → TC Term newMeta = checkType unknown - -blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A -blockOnMeta m = blockTC (blockerMeta m) From fbf4761beab3e4891c32fd6893e7953772f94152 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Fri, 13 Oct 2023 11:44:19 +0900 Subject: [PATCH 6/6] Undo unnecessary change --- src/Tactic/Cong.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 7e9a84d602..b7accfcc08 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -98,7 +98,7 @@ private destructEqualityGoal goal@(def (quote _≡_) (lvl ∷ tp ∷ lhs ∷ rhs ∷ [])) = pure $ equals (unArg lvl) (unArg tp) (unArg lhs) (unArg rhs) destructEqualityGoal (meta m args) = - blockTC (blockerMeta m) + blockOnMeta m destructEqualityGoal goal = notEqualityError goal