From c2745e8c12370b91f13cabe935a60c3b1820be14 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Tue, 5 Aug 2025 12:52:59 +0300 Subject: [PATCH] Tactic.Derive.DecEq: faster variant --- Meta/Init.agda | 2 - Reflection/Syntax.agda | 51 ++-- Reflection/Utils/Args.agda | 2 +- Reflection/Utils/Core.agda | 5 + Reflection/Utils/Metas.agda | 6 +- Reflection/Utils/Substitute.agda | 6 +- Reflection/Utils/TCI.agda | 6 +- Tactic.agda | 1 + Tactic/Derive/Convertible.agda | 2 +- Tactic/Derive/DecEq.agda | 1 + Tactic/Derive/DecEqFast.agda | 430 +++++++++++++++++++++++++++++++ Tactic/Inline.agda | 2 +- agda-stdlib-meta.agda-lib | 2 +- 13 files changed, 475 insertions(+), 41 deletions(-) create mode 100644 Tactic/Derive/DecEqFast.agda diff --git a/Meta/Init.agda b/Meta/Init.agda index 768cb4ea..d85a3e9f 100644 --- a/Meta/Init.agda +++ b/Meta/Init.agda @@ -5,8 +5,6 @@ module Meta.Init where open import Reflection.Debug public open import Reflection.TCI public open import Reflection.Syntax public -open import Reflection.AST.Term public - using (vΠ[_∶_]_) instance iMonad-TC = Monad-TC diff --git a/Reflection/Syntax.agda b/Reflection/Syntax.agda index 307429da..ae5616a4 100644 --- a/Reflection/Syntax.agda +++ b/Reflection/Syntax.agda @@ -4,40 +4,39 @@ module Reflection.Syntax where open import Meta.Prelude -open import Reflection.AST.Argument public - hiding (map) -open import Reflection.AST.Term public - hiding (_≟_; getName) -open import Reflection.AST.Name public - hiding (_≟_; _≡ᵇ_; _≈_; _≈?_) open import Reflection.AST.Definition public - hiding (_≟_) -open import Reflection.AST.Meta public - hiding (_≟_; _≡ᵇ_; _≈_; _≈?_) + using (Definition; function; data-type; axiom; record′; constructor′; primitive′) +open import Reflection.AST.Pattern public + using (Pattern; con; dot; var; lit; proj; absurd) +open import Reflection.AST.Term public + using ( Term; pi; var; con; def; lam; pat-lam; sort; lit; meta; unknown + ; vLam; hLam; iLam; Π[_∶_]_; vΠ[_∶_]_; hΠ[_∶_]_; iΠ[_∶_]_ + ; Type; Telescope + ; Sort; set; prop; propLit; inf + ; Clause; Clauses; clause; absurd-clause + ) open import Reflection.AST.Abstraction public - using (unAbs) - -open import Agda.Builtin.Reflection public - using (ArgInfo; Modality; Visibility; Literal; Meta) - + using (Abs; abs; unAbs) open import Reflection.AST.Argument public - using (Arg; arg) + using (Arg; Args; arg; vArg; hArg; iArg; unArg; _⟨∷⟩_; map-Args) +open import Reflection.AST.Literal public + using (Literal) +open import Reflection.AST.Meta public + using (Meta) +open import Reflection.AST.Name public + using (Name) open import Reflection.AST.Argument.Visibility public using (Visibility; visible; hidden; instance′) open import Reflection.AST.Argument.Information public using (ArgInfo; arg-info) -open import Reflection.AST.Abstraction public - using (Abs; abs; unAbs) -open import Reflection.AST.Argument public - using (vArg; hArg; iArg; unArg; _⟨∷⟩_; map-Args) +open import Reflection.AST.Argument.Modality public + using (Modality; modality) +open import Reflection.AST.Argument.Relevance public + using (Relevance; relevant; irrelevant) open import Reflection public - using ( Name; Meta; Literal; Pattern; Clause - ; ErrorPart; strErr - ; Term; Type; pi; var; con; def; lam; pat-lam; agda-sort; lit; meta; unknown - ; Definition; data-cons; data-type; record-type - ) + using (ErrorPart; strErr) -open import Reflection using (hidden; instance′; TC) +open import Reflection using (TC) -- ** Smart constructors @@ -103,7 +102,7 @@ pattern _◇ n = Pattern.con n [] pattern _◇⟦_⟧ n x = Pattern.con n (vArg x ∷ []) pattern _◇⟦_∣_⟧ n x y = Pattern.con n (vArg x ∷ vArg y ∷ []) -pattern `Set = agda-sort (set (quote 0ℓ ∙)) +pattern `Set = sort (set (quote 0ℓ ∙)) -- ** useful type aliases PatTelescope = Telescope diff --git a/Reflection/Utils/Args.agda b/Reflection/Utils/Args.agda index 142833a3..4126bc3d 100644 --- a/Reflection/Utils/Args.agda +++ b/Reflection/Utils/Args.agda @@ -2,7 +2,7 @@ module Reflection.Utils.Args where open import Meta.Prelude -open import Meta.Init hiding (toℕ) +open import Meta.Init open import Data.List using (map; zip) open import Data.Fin using (toℕ) diff --git a/Reflection/Utils/Core.agda b/Reflection/Utils/Core.agda index 300d3537..52c072fa 100644 --- a/Reflection/Utils/Core.agda +++ b/Reflection/Utils/Core.agda @@ -49,6 +49,11 @@ argTys = proj₁ ∘ viewTy′ resultTy : Type → Type resultTy = proj₂ ∘ viewTy′ +tyTele : Type → Telescope +tyTele = λ where + (Π[ s ∶ a ] ty) → (s , a) ∷ tyTele ty + _ → [] + -- ** definitions record DataDef : Set where diff --git a/Reflection/Utils/Metas.agda b/Reflection/Utils/Metas.agda index a7a530c7..51581cb9 100644 --- a/Reflection/Utils/Metas.agda +++ b/Reflection/Utils/Metas.agda @@ -20,7 +20,7 @@ mutual (lam _ (abs _ x)) → findMetas x (pat-lam cs as) → findMetasCl cs ++ findMetas* as (pi (arg _ a) (abs _ b)) → findMetas a ++ findMetas b - (agda-sort _) → [] + (sort _) → [] (lit _) → [] m@(meta x as) → m ∷ findMetas* as unknown → [] @@ -33,5 +33,5 @@ mutual findMetasCl : List Clause → List Term findMetasCl = λ where [] → [] - (Clause.clause _ _ t ∷ c) → findMetas t ++ findMetasCl c - (Clause.absurd-clause _ _ ∷ c) → findMetasCl c + (clause _ _ t ∷ c) → findMetas t ++ findMetasCl c + (absurd-clause _ _ ∷ c) → findMetasCl c diff --git a/Reflection/Utils/Substitute.agda b/Reflection/Utils/Substitute.agda index d175f01c..e47c052d 100644 --- a/Reflection/Utils/Substitute.agda +++ b/Reflection/Utils/Substitute.agda @@ -28,7 +28,7 @@ mutual (lam v t) → lam v (substAbs x s t) (pat-lam _ _) → unknown -- ignoring for now (pi a b) → pi (substArg x s a) (substAbs x s b) - (agda-sort st) → agda-sort (substSort x s st) + (sort st) → sort (substSort x s st) (lit l) → lit l (meta m as) → meta m (substArgs x s as) unknown → unknown @@ -75,8 +75,8 @@ module _ (f : ℕ → ℕ) where → pat-lam (mapFreeVarsᶜ∗ bound cs) (mapFreeVars∗ bound as) (pi (arg i t) (abs x t′)) → pi (arg i (mapFreeVars bound t)) (abs x (mapFreeVars (suc bound) t′)) - (agda-sort s) - → agda-sort (mapFreeVarsˢ bound s) + (sort s) + → sort (mapFreeVarsˢ bound s) (meta x as) → meta x (mapFreeVars∗ bound as) t → t diff --git a/Reflection/Utils/TCI.agda b/Reflection/Utils/TCI.agda index 371375f7..413601b4 100644 --- a/Reflection/Utils/TCI.agda +++ b/Reflection/Utils/TCI.agda @@ -78,7 +78,7 @@ ensureNoMetas = λ where (lam v (abs _ t)) → ensureNoMetas t (pat-lam cs args) → noMetaClauses cs >> noMetaArgs args (pi a b) → noMetaArg a >> noMetaAbs b - (agda-sort s) → noMetaSort s + (sort s) → noMetaSort s (lit l) → return _ -- (meta x _) → errorP "meta found!" (meta x _) → blockOnMeta x @@ -233,7 +233,7 @@ getDataDef n = inDebugPath "getDataDef" do getRecordDef : Name → M RecordDef getRecordDef n = do - (record-type c fs) ← getDefinition n + (record′ c fs) ← getDefinition n where _ → error1 "Not a record definition!" args ← proj₁ <$> getType' n return (record { name = c ; fields = fs ; params = args }) @@ -260,7 +260,7 @@ getFuel s = do isSort : Term → M Bool isSort t = do - (agda-sort _) ← normalise t + (sort _) ← normalise t where _ → return false return true diff --git a/Tactic.agda b/Tactic.agda index 8cbdd207..c13e87a7 100644 --- a/Tactic.agda +++ b/Tactic.agda @@ -18,6 +18,7 @@ open import Tactic.J public open import Tactic.ReduceDec public open import Tactic.Derive.DecEq public +open import Tactic.Derive.DecEqFast open import Tactic.Derive.Show public open import Tactic.Derive.HsType public; open import Tactic.Derive.HsType.Tests open import Tactic.Derive.Convertible public diff --git a/Tactic/Derive/Convertible.agda b/Tactic/Derive/Convertible.agda index 22699006..bc159cd7 100644 --- a/Tactic/Derive/Convertible.agda +++ b/Tactic/Derive/Convertible.agda @@ -119,7 +119,7 @@ doPatternLambda hole = patternLambda =<< initTCEnvWithGoal hole -- Deriving a Convertible instance. Usage -- unquoteDecl iName = deriveConvertible iName (quote AgdaTy) (quote HsTy) deriveConvertible : Name → Name → Name → R.TC ⊤ -deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (agda-sort (lit 0)) do +deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (sort (lit 0)) do agdaDef ← getDefinition agdaName hsDef ← getDefinition hsName -- instName ← freshName $ "Convertible" S.++ show hsName diff --git a/Tactic/Derive/DecEq.agda b/Tactic/Derive/DecEq.agda index 08e850c3..28c4ffe7 100644 --- a/Tactic/Derive/DecEq.agda +++ b/Tactic/Derive/DecEq.agda @@ -21,6 +21,7 @@ open import Relation.Nullary open import Reflection.Tactic open import Reflection.QuotedDefinitions open import Reflection.AST.DeBruijn +open import Reflection.AST.Pattern using () renaming (_≟_ to _≟-Pattern_) open import Class.DecEq.Core open import Class.Functor diff --git a/Tactic/Derive/DecEqFast.agda b/Tactic/Derive/DecEqFast.agda new file mode 100644 index 00000000..d9573889 --- /dev/null +++ b/Tactic/Derive/DecEqFast.agda @@ -0,0 +1,430 @@ +-------------------------------------------------------------------------------- +-- ** Generic deriving of DecEq + +-- Alternative to Tactic.Derive.DecEq that supports a different subset of types, +-- and typechecks faster in the presence of many fields/constructors. +-------------------------------------------------------------------------------- +{-# OPTIONS -v DecEqFast:100 #-} +{-# OPTIONS --safe --with-K #-} +module Tactic.Derive.DecEqFast where + +open import Meta.Prelude hiding ([_,_]) + +open import Relation.Nullary +open import Relation.Binary using () renaming (Decidable to Decidable²) +import Data.List as L +open L using ([]; _∷_; map) + +open import Class.Show +open import Class.Semigroup +open import Class.Monoid +open import Class.Functor +open import Class.Bifunctor +open import Class.Monad +open import Class.DecEq.Core +open import Class.DecEq.Instances using (DecEq-Name) +open import Class.DecEq.WithK + +open import Agda.Builtin.Reflection public + using (modality; relevant; irrelevant) +open import Reflection.Syntax +open import Reflection.QuotedDefinitions +open import Reflection.Utils +open import Reflection.Utils.Debug +open Debug ("DecEqFast" , 100) +open import Reflection hiding (_>>=_; _>>_; _≟_) +open import Reflection.Utils.TCM + +-- +allPairs : List A → List (A × A) +allPairs xs = cartesianProduct xs xs + +`λ∅∅ = `λ⦅ [ "()" , vArg? ] ⦆∅ +-- + +-- ** patterns +module _ (toDrop : ℕ) {- module context -} where + mkPattern : Name → TC + ( Args Type -- ^ type arguments of given constructor + × ℕ -- ^ # of introduced variables + × List (ℕ × Arg Type) -- ^ generated variables along with their type + × Pattern -- ^ generated pattern for given constructor + ) + mkPattern c = do + ty ← reduce =<< getType c + let tys = drop toDrop (argTys ty) + n = length tys + vars = enumerate tys + return + $ tys + , n + , vars + , Pattern.con c (map (λ{ (i , arg x _) → arg x (` i) }) vars) + +module _ (toDrop : ℕ) {- module context -} where + derive-DecEq′ : Definition → TC Term + derive-DecEq′ (data-type _ []) = return `λ∅∅ + derive-DecEq′ (data-type ps cs) = do + cls ← concatMap L.fromMaybe <$> mapM f (allPairs cs) + return $ pat-lam cls [] + where + go : ℕ → List (ℕ × Arg Type) → Term + go _ [] = `yes (quote refl ◆) + go n ((x , _) ∷ xs) = + let i = n ∸ suc x in + quote case_of_ + ∙⟦ quote _≟_ ∙⟦ ♯ (i + n) ∣ ♯ i ⟧ + ∣ `λ⟦ ``no (Pattern.var 0 {-"¬p"-}) + ⦅ [ "¬p" , vArg? ] ⦆⇒ + `no (`λ⟦ (quote refl ◇) + ⦅ [] ⦆⇒ (♯ 0 ⟦ quote refl ◆ ⟧) + ⟧) + ∣ ``yes (quote refl ◇) + ⦅ [] ⦆⇒ go n xs + ⟧ + ⟧ + + bumpFreeVars : (ℕ → ℕ) → List (ℕ × Arg Type) → List (ℕ × Arg Type) + bumpFreeVars bump = go′ 0 + where + go′ : ℕ → List (ℕ × Arg Type) → List (ℕ × Arg Type) + go′ _ [] = [] + go′ x ((i , p) ∷ ps) = (bump i , fmap (mapFreeVars bump x) p) ∷ go′ (suc x) ps + + f : Name × Name → TC (Maybe Clause) + f (c , c′) = do + _ , n , pvs , pc ← mkPattern toDrop c + _ , n′ , pvs′ , pc′ ← mkPattern toDrop c′ + let + tel = map (λ (i , argTy) → ("v" ◇ show i) , argTy) (pvs ++ bumpFreeVars (_+ n) pvs′) + PC = mapVariables (λ i → n + n′ ∸ suc i) pc + PC′ = mapVariables (λ i → n′ ∸ suc i) pc′ + ty ← reduce =<< getType c + ty′ ← reduce =<< getType c′ + b ← compatible? (resultTy ty) (resultTy ty′) + return $ + if b then just (⟦ PC ∣ PC′ ⦅ tel ⦆⇒ if c == c′ then go n (filter (isVisible? ∘ proj₂) pvs) + else `no `λ∅∅ ⟧) + else nothing + + derive-DecEq′ (record-type rn fs) = do + return $ `λ⟦ "r" ∣ "r′" ⇒ go fs ⟧ + where + go : List (Arg Name) → Term + go [] = `yes (quote refl ◆) + go (arg (arg-info _ (modality relevant _)) n ∷ args) = + quote case_of_ + ∙⟦ quote _≟_ ∙⟦ n ∙⟦ ♯ 1 ⟧ ∣ n ∙⟦ ♯ 0 ⟧ ⟧ + ∣ `λ⟦ ``no (Pattern.var 0 {-"¬p"-}) + ⦅ [ "¬p" , vArg? ] ⦆⇒ + `no (`λ⟦ (quote refl ◇) + ⦅ [] ⦆⇒ (♯ 0 ⟦ quote refl ◆ ⟧) + ⟧) + ∣ ``yes (quote refl ◇) + ⦅ [] ⦆⇒ go args + ⟧ + ⟧ + go (arg (arg-info _ _) _ ∷ args) = go args + derive-DecEq′ _ = error "[not supported] not a data type or record" + +derive-DecEq : List (Name × Name) → TC ⊤ +derive-DecEq xs = do + (record-type c _) ← getDefinition (quote DecEq) + where _ → error "impossible" + + ys ← forM xs λ (n , f) → do + f′ ← freshName (show {A = Name} f) + T ← getType n + ctx ← getContext + d ← getDefinition n + + let tel = argTys T -- tyTele T + n′ = apply⋯ tel n + is = argTys T + let mctx = take (parameters d ∸ length ctx) is + mtel = map ("_" ,_) mctx + pc = map (λ where (i , _) → hArg (` i) ) (enumerate mctx) + + -- fᵢ′ : ∀ ⋯ → Decidable² {A = Tᵢ ⋯} _≡_ + let ty′ = ∀indices⋯ tel + $ def (quote Decidable²) (hArg? ∷ hArg n′ ∷ vArg (quote _≡_ ∙) ∷ []) + declareDef (vArg f′) ty′ + + -- instance fᵢ : ∀ ⋯ → DecEq (Tᵢ ⋯) + let ty = ∀indices⋯ tel + $ quote DecEq ∙⟦ n′ ⟧ + declareDef (iArg f) ty + -- fᵢ ⋯ = λ where ._≟_ → fᵢ′ + defineFun f [ clause mtel pc (c ◆⟦ f′ ∙ ⟧) ] + + -- fᵢ′ ⋯ = λ where + -- (c₀ x y) (c₀ x′ y′) → case x ≟ x′ of ⋯ + -- ⋯ + t ← inContext (L.reverse mtel) $ do + ctx ← getContext + derive-DecEq′ (length mtel) d + + return (f′ , (pc , mtel) , t) + + return⊤ $ forM ys λ (f′ , (pc , mtel) , t) → + defineFun f′ [ clause mtel pc t ] + +-------------------------- +-- Examples + +private + +-- ** record types + + open import Tactic.Defaults + open import Data.Integer using (ℤ) + open import Data.Fin using (Fin) + + record R⁰ : Set where + unquoteDecl r⁰ = derive-DecEq [ quote R⁰ , r⁰ ] + + record R¹ : Set where + field + x : ℕ + unquoteDecl r¹ = derive-DecEq [ quote R¹ , r¹ ] + + record R² : Set where + field + x : ℕ × ℤ + y : ⊤ ⊎ Bool + unquoteDecl r² = derive-DecEq [ quote R² , r² ] + +-- ** inductive datatypes + + data X⁰ : Set where + unquoteDecl x⁰ = derive-DecEq [ quote X⁰ , x⁰ ] + + data X¹ : Set where + x : X¹ + unquoteDecl x¹ = derive-DecEq [ quote X¹ , x¹ ] + + data X² : Set where + x y : X² + unquoteDecl x² = derive-DecEq [ quote X² , x² ] + + data XX : Set where + c₂ : List X² → XX + c₁ : X¹ → X² → XX + unquoteDecl xx = derive-DecEq [ quote XX , xx ] + + data XXX : Set where + c₂′ : List X² → XXX + _⊗⊗_ : XXX → XXX → XXX + unquoteDecl xxx = derive-DecEq [ quote XXX , xxx ] + +-- ** recursive datatypes + + data ℕ′ : Set where + O : ℕ′ + S : ℕ′ → ℕ′ + unquoteDecl DecEq-ℕ′ = derive-DecEq [ quote ℕ′ , DecEq-ℕ′ ] + +-- ** list recursion + + data Nats : Set where + O : Nats + S : List Nats → Nats + + -- {-# TERMINATING #-} +{- *** T0D0: figure out how to pass termination checker + + go : Decidable² {A = Nat} _≡_ + instance + dn : DecEq Nat + dn ._≟_ = go + go = λ + { O O → yes refl + ; O (S x0) → no (λ { () }) + ; (S x0) O → no (λ { () }) + ; (S x0) (S x0′) + → case _≟_ ⦃ DecEq-List ⦃ dn ⦄ ⦄ x0 x0′ of λ + { (no ¬p) → no λ { refl → ¬p refl } + ; (yes refl) → yes refl ⦄ +-} + -- unquoteDecl DecEq-Nats = derive-DecEq [ quote Nats , DecEq-Nats ] + +-- ** mutually recursive datatypes + + data M₁ : Set + data M₂ : Set + data M₁ where + m₁ : M₁ + m₂→₁ : M₂ → M₁ + data M₂ where + m₂ : M₂ + m₁→₂ : M₁ → M₂ + unquoteDecl DecEq-M₁ DecEq-M₂ = derive-DecEq $ (quote M₁ , DecEq-M₁) ∷ (quote M₂ , DecEq-M₂) ∷ [] + +-- ** make sure all derivations were successful + open import Data.List.Relation.Unary.All using (All; []; _∷_) + _ : All (λ x → Decidable² {A = x} _≡_) (R⁰ ∷ R¹ ∷ R² ∷ X⁰ ∷ X¹ ∷ X² ∷ XX ∷ ℕ′ ∷ M₁ ∷ M₂ ∷ []) + _ = _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ [] + +-- ** indexed types + + data Fin′ : ℕ → Set where + O : ∀ {n} → Fin′ (suc n) + S : ∀ {n} → Fin′ n → Fin′ (suc n) + unquoteDecl DecEq-Fin′ = derive-DecEq [ quote Fin′ , DecEq-Fin′ ] + _ : ∀ {n} → Decidable² {A = Fin′ n} _≡_ + _ = _≟_ + + data λExprℕ (n : ℕ) : Set where + ƛ_ : Fin n → λExprℕ n + unquoteDecl DecEq-λExprℕ = derive-DecEq [ quote λExprℕ , DecEq-λExprℕ ] + + data Boolℕ : Bool → ℕ → Set where + O : Boolℕ true 0 + unquoteDecl DecEq-Boolℕ = derive-DecEq [ quote Boolℕ , DecEq-Boolℕ ] + _ : ∀ {b n} → Decidable² {A = Boolℕ b n} _≡_ + _ = _≟_ + + data Boolℕ² : Bool → ℕ → Set where + O : Boolℕ² false 0 + I : Boolℕ² true 1 + unquoteDecl DecEq-Boolℕ² = derive-DecEq [ quote Boolℕ² , DecEq-Boolℕ² ] + _ : ∀ {b n} → Decidable² {A = Boolℕ² b n} _≡_ + _ = _≟_ + + data Wrapℕ : Set where + Mk : ℕ → Wrapℕ + unquoteDecl DecEq-Wrapℕ = derive-DecEq [ quote Wrapℕ , DecEq-Wrapℕ ] + + variable + n : ℕ + wn : Wrapℕ + + data Exprℕ : Wrapℕ → Set where + var : Fin n → Exprℕ (Mk n) + ‵ : ∀ {x} → ℕ → Exprℕ x + unquoteDecl DecEq-Exprℕ = derive-DecEq [ quote Exprℕ , DecEq-Exprℕ ] + + data Enum : Set where + I II : Enum + unquoteDecl DecEq-Enum = derive-DecEq [ quote Enum , DecEq-Enum ] + + variable en : Enum + + Time = ℕ + + data Exprℕ′ : Wrapℕ → Enum → Set where + var : Fin n → Exprℕ′ (Mk n) I + ‵ : ℕ → Exprℕ′ wn II + _`+_ : Exprℕ′ wn II → Exprℕ′ wn II → Exprℕ′ wn II + _`-_ : Exprℕ′ wn II → Exprℕ′ wn II → Exprℕ′ wn II + _`=_ : Exprℕ′ wn II → Exprℕ′ wn II → Exprℕ′ wn I + _`<_ : Exprℕ′ wn II → Exprℕ′ wn II → Exprℕ′ wn I + + `if_then_else_ : Exprℕ′ wn I → Exprℕ′ wn en → Exprℕ′ wn en → Exprℕ′ wn en + + -- Size + ∣_∣ : Exprℕ′ wn II → Exprℕ′ wn II + + -- Hashing + hash : Exprℕ′ wn II → Exprℕ′ wn II + + -- Signature verification + versig : List ℕ → List (Fin n) → Exprℕ′ (Mk n) I + + -- Temporal constraints + absAfter_⇒_ : Time → Exprℕ′ wn en → Exprℕ′ wn en + relAfter_⇒_ : Time → Exprℕ′ wn en → Exprℕ′ wn en + + unquoteDecl DecEq-Exprℕ′ = derive-DecEq [ quote Exprℕ′ , DecEq-Exprℕ′ ] + +-- ** parametrized datatypes +{- + data Expr (A : Set) : Set where + Con : A → Expr A + _⊕_ : Expr A → Expr A → Expr A + unquoteDecl DecEq-Expr = derive-DecEq [ quote Expr , DecEq-Expr ] + _ : ∀ {A} ⦃ _ : DecEq A ⦄ → Decidable² {A = Expr A} _≡_ + _ = _≟_ + + data Exprℤ : ℤ → Set where + Con : ∀ {n} → ℤ → Exprℤ n + _⊕_ : ∀ {x y z} → Exprℤ x → Exprℤ y → Exprℤ z + unquoteDecl DecEq-Exprℤ = derive-DecEq [ quote Exprℤ , DecEq-Exprℤ ] + _ : ∀ {n} → Decidable² {A = Exprℤ n} _≡_ + _ = _≟_ +-} + +-- ** indexed records + + record Pos (n : ℕ) : Set where + field + pos : Fin n + unquoteDecl DecEq-Pos = derive-DecEq [ quote Pos , DecEq-Pos ] + _ : ∀ {n} → Decidable² {A = Pos n} _≡_ + _ = _≟_ + +-- ** datatypes inside module + + module Test₁ (A : Set) ⦃ _ : DecEq A ⦄ (B : Set) ⦃ _ : DecEq B ⦄ where + + data X : ℕ → Set where + x₀ y₀ z₀ : X 0 + x₁ y₁ z₁ : X 1 + fromA : ∀ {n} → A → X n + fromB : ∀ {n} → B → X n + unquoteDecl DecEq-Test1X = derive-DecEq [ quote X , DecEq-Test1X ] + + _ : ∀ {n} → Decidable² {A = X n} _≡_ + _ = _≟_ + + record R : Set where + field + r₁ : A + r₂ : B + unquoteDecl DecEq-Test1R = derive-DecEq [ quote R , DecEq-Test1R ] + _ : Decidable² {A = R} _≡_ + _ = _≟_ + + record R′ : Set where + field + r₁ : A × B + r₂ : X 0 + unquoteDecl DecEq-Test1R′ = derive-DecEq [ quote R′ , DecEq-Test1R′ ] + _ : Decidable² {A = R′} _≡_ + _ = _≟_ + + module _ (A : Set) ⦃ _ : DecEq A ⦄ {B : Set} ⦃ _ : DecEq B ⦄ where + open Test₁ A B + + _ : ∀ {n} → Decidable² {A = X n} _≡_ + _ = _≟_ + _ : Decidable² {A = R} _≡_ + _ = _≟_ + _ : Decidable² {A = R′} _≡_ + _ = _≟_ + + unquoteDecl DecEq-Test1R = derive-DecEq [ quote Test₁.R , DecEq-Test1R ] + _ : ∀ {A : Set} ⦃ _ : DecEq A ⦄ {B : Set} ⦃ _ : DecEq B ⦄ + → Decidable² {A = Test₁.R A B} _≡_ + _ = _≟_ + + -- unquoteDecl DecEq-Test1R′ = derive-DecEq [ quote Test₁.R′ , DecEq-Test1R′ ] + -- _ : ∀ {A : Set} ⦃ _ : DecEq A ⦄ {B : Set} ⦃ _ : DecEq B ⦄ + -- → Decidable² {A = Test₁.R′ A B} _≡_ + -- _ = _≟_ + + data λExprℕ′ (mn : Wrapℕ) : Set where + ƛ_ : Exprℕ′ mn II → λExprℕ′ mn + unquoteDecl DecEq-λExprℕ′ = derive-DecEq [ quote λExprℕ′ , DecEq-λExprℕ′ ] + + + module Test₂ (A : Set) ⦃ _ : DecEq A ⦄ where + data Label : Set where + auth-divide : A → ℕ → ℕ → ℕ → Label + unquoteDecl DecEq-Label = derive-DecEq [ quote Label , DecEq-Label ] + + data Letter : Set where + α ἄ ὰ ά Ἀ έ ἔ ῆ ἣ η ι ϊ ί ῖ ο ὐ υ ω γ δ θ κ ƛ μ ν Π ρ ς χ : Letter + unquoteDecl DecEq-Letter = derive-DecEq [ (quote Letter , DecEq-Letter) ] + + -- open import Tactic.Derive.TestTypes diff --git a/Tactic/Inline.agda b/Tactic/Inline.agda index 9cc6ae95..99a528ec 100644 --- a/Tactic/Inline.agda +++ b/Tactic/Inline.agda @@ -80,7 +80,7 @@ private (pat-lam cs (vArg a ∷ [])) → `case go lvl a of pat-lam (goCls lvl cs) [] -- ^ use case_of_ for single-argument pattern lambdas (c.f. example 7) (pat-lam cs as) → pat-lam (goCls lvl cs) (go∗ lvl as) - (agda-sort s) → agda-sort (goSort lvl s) + (sort s) → sort (goSort lvl s) (meta x as) → meta x (go∗ lvl as) t → t diff --git a/agda-stdlib-meta.agda-lib b/agda-stdlib-meta.agda-lib index 55418f87..2196b29e 100644 --- a/agda-stdlib-meta.agda-lib +++ b/agda-stdlib-meta.agda-lib @@ -1,5 +1,5 @@ name: standard-library-meta depend: - standard-library-2.2 + standard-library-2.3 standard-library-classes include: .