diff --git a/Reflection/QuotedDefinitions.agda b/Reflection/QuotedDefinitions.agda new file mode 100644 index 00000000..38e90064 --- /dev/null +++ b/Reflection/QuotedDefinitions.agda @@ -0,0 +1,31 @@ +{-# OPTIONS --safe --without-K #-} + +module Reflection.QuotedDefinitions where + +open import Meta.Prelude + +open import Reflection.Syntax + +infix 4 _`≡_ _``≡_ +_`≡_ : Term → Term → Term +t `≡ t' = quote _≡_ ∙⟦ t ∣ t' ⟧ + +pattern _``≡_ t t' = def (quote _≡_) (_ ∷ _ ∷ vArg t ∷ vArg t' ∷ []) + +`refl : Term +`refl = quote refl ◆ + +pattern ``refl = quote refl ◇ + +`case_of_ : Term → Term → Term +`case t of t' = quote case_of_ ∙⟦ t ∣ t' ⟧ + +-- Syntax for quoting `yes` and `no` +open import Relation.Nullary + +`yes `no : Term → Term +`yes x = quote _because_ ◆⟦ quote true ◆ ∣ quote ofʸ ◆⟦ x ⟧ ⟧ +`no x = quote _because_ ◆⟦ quote false ◆ ∣ quote ofⁿ ◆⟦ x ⟧ ⟧ + +pattern ``yes x = quote _because_ ◇⟦ quote true ◇ ∣ quote ofʸ ◇⟦ x ⟧ ⟧ +pattern ``no x = quote _because_ ◇⟦ quote false ◇ ∣ quote ofⁿ ◇⟦ x ⟧ ⟧ diff --git a/Tactic/Derive/DecEq.agda b/Tactic/Derive/DecEq.agda index 7ad115f3..08e850c3 100644 --- a/Tactic/Derive/DecEq.agda +++ b/Tactic/Derive/DecEq.agda @@ -17,17 +17,13 @@ import Data.List as L import Data.List.NonEmpty as NE open import Relation.Nullary -open import Relation.Nullary.Decidable open import Reflection.Tactic -open import Reflection.AST.Term using (_≟-Pattern_) -open import Reflection.Utils -open import Reflection.Utils.TCI open import Reflection.QuotedDefinitions +open import Reflection.AST.DeBruijn open import Class.DecEq.Core open import Class.Functor -open import Class.Monad open import Class.MonadTC.Instances open import Class.Traversable @@ -37,17 +33,29 @@ open import Tactic.Derive (quote DecEq) (quote _≟_) open ClauseExprM +-- simply typed annotated case_of_, giving better performance than without a type annotation +-- the type annotation prevents elaboration time from doubling on every argument to a constructor +`case_returning_of_ : Term → Term → Term → Term +`case t returning t' of t'' = def (quote case_of_) (hArg? ∷ hArg? ∷ hArg? ∷ hArg t' ∷ vArg t ∷ vArg t'' ∷ []) + private instance _ = ContextMonad-MonadTC - -- We take the Dec P argument first to improve type checking performance. - -- It's easy to infer the type of P from this argument and we need to know - -- P to be able to check the pattern lambda generated for the P → Q direction - -- of the isomorphism. Having the isomorphism first would cause the type checker - -- to go back and forth between the pattern lambda and the Dec P argument, - -- inferring just enough of the type of make progress on the lambda. - map' : ∀ {p q} {P : Set p} {Q : Set q} → Dec P → P ⇔ Q → Dec Q - map' d record { to = to ; from = from } = map′ to from d + -- Here's an example of what code this generates, here for a record R with 3 fields: + -- DecEq : DecEq R + -- DecEq ._≟_ ⟪ x₁ , x₂ , x₃ ⟫ ⟪ y₁ , y₂ , y₃ ⟫ = + -- case (x₁ ≟ y₁) of λ where + -- (false because ¬p) → no (case ¬p of λ where (ofⁿ ¬p) refl → ¬p refl) + -- (true because p₁) → case (x₂ ≟ y₂) of λ where + -- (false because ¬p) → no (case ¬p of λ where (ofⁿ ¬p) refl → ¬p refl) + -- (true because p₂) → case (x₃ ≟ y₃) of λ where + -- (false because ¬p) → no (case ¬p of λ where (ofⁿ ¬p) refl → ¬p refl) + -- (true because p₃) → yes (case p₁ , p₂ , p₃ of λ where (ofʸ refl , ofʸ refl , ofʸ refl) → refl) + + -- patterns almost like `yes` and `no`, except that they don't match the `Reflects` proof + -- delaying maching on the `Reflects` proof as late as possible results in a major speed increase + pattern ``yes' x = quote _because_ ◇⟦ quote true ◇ ∣ x ⟧ + pattern ``no' x = quote _because_ ◇⟦ quote false ◇ ∣ x ⟧ module _ (transName : Name → Maybe Name) where @@ -57,36 +65,54 @@ private ... | nothing = quote _≟_ ∙⟦ t ∣ t' ⟧ eqFromTerm _ t t' = quote _≟_ ∙⟦ t ∣ t' ⟧ - toDecEqName : SinglePattern → List (Term → Term → Term) - toDecEqName (l , _) = L.map (λ where (_ , arg _ t) → eqFromTerm t) l - - -- on the diagonal we have one pattern, outside we don't care + -- `nothing`: outside of the diagonal, not equal + -- `just`: on the diagonal, with that pattern, could be equal -- assume that the types in the pattern are properly normalized - mapDiag : Maybe SinglePattern → TC Term - mapDiag nothing = return $ `no `λ⦅ [ ("" , vArg?) ] ⦆∅ - mapDiag (just p@(l , _)) = let k = length l in do - typeList ← traverse ⦃ Functor-List ⦄ inferType (applyDownFrom ♯ (length l)) - return $ quote map' ∙⟦ genPf k (L.map eqFromTerm typeList) ∣ genEquiv k ⟧ + genBranch : Maybe SinglePattern → TC Term + genBranch nothing = return $ `no `λ⦅ [ ("" , vArg?) ] ⦆∅ + genBranch (just ([] , _)) = return $ `yes `refl + genBranch (just p@(l@(x ∷ xs) , arg _ pat)) = do + (con n args) ← return pat + where _ → error1 "BUG: genBranch" + typeList ← traverse inferType (applyUpTo ♯ (length l)) + let info = L.zip typeList (downFrom (length l)) + let ty = quote Dec ∙⟦ con n (applyDownFrom (vArg ∘ ♯ ∘ (_+ length l)) (length l)) + `≡ con n (applyDownFrom (vArg ∘ ♯) (length l)) ⟧ + return $ foldl (λ t (eq , k) → genCase (weaken k ty) (eqFromTerm eq) t) genTrueCase info where - genPf : ℕ → List (Term → Term → Term) → Term - genPf k [] = `yes (quote tt ◆) - genPf k (n ∷ l) = quote _×-dec_ ∙⟦ genPf k l ∣ n (♯ (length l)) (♯ (length l + k)) ⟧ - - -- c x1 .. xn ≡ c y1 .. yn ⇔ x1 ≡ y1 .. xn ≡ yn - genEquiv : ℕ → Term - genEquiv n = quote mk⇔ ∙⟦ `λ⟦ reflPattern n ⇒ `refl ⟧ ∣ `λ⟦ ``refl ⇒ reflTerm n ⟧ ⟧ - where - reflPattern : ℕ → Pattern - reflPattern 0 = quote tt ◇ - reflPattern (suc n) = quote _,_ ◇⟦ reflPattern n ∣ ``refl ⟧ - - reflTerm : ℕ → Term - reflTerm 0 = quote tt ◆ - reflTerm (suc n) = quote _,_ ◆⟦ reflTerm n ∣ `refl ⟧ + k = ℕ.suc (length xs) + + vars : NE.List⁺ ℕ + vars = 0 NE.∷ applyUpTo ℕ.suc (length xs) + + -- case (xᵢ ≟ yᵢ) of λ { (false because ...) → no ... ; (true because p) → t } + -- since we always add one variable to the scope of t the uncompared terms + -- are always at index 2k+1 and k + genCase : Term → (Term → Term → Term) → Term → Term + genCase goalTy _`≟_ t = `case ♯ (2 * k ∸ 1) `≟ ♯ (k ∸ 1) + returning goalTy + of clauseExprToPatLam (MatchExpr + ( (singlePatternFromPattern (vArg (``yes' (` 0))) , inj₂ (just t)) + ∷ (singlePatternFromPattern (vArg (``no' (` 0))) , inj₂ (just (`no $ + -- case ¬p of λ where (ofⁿ ¬p) refl → ¬p refl + `case ♯ 0 of clauseExprToPatLam (multiClauseExpr + [( singlePatternFromPattern (vArg (quote ofⁿ ◇⟦ ` 0 ⟧)) + NE.∷ singlePatternFromPattern (vArg ``refl) ∷ [] + , inj₂ (just ♯ 0 ⟦ `refl ⟧)) ])))) + ∷ [])) + + -- yes (case p₁ , ... , pₖ of λ where (ofʸ refl , ... , ofʸ refl) → refl) + genTrueCase : Term + genTrueCase = `yes $ + `case NE.foldl₁ (quote _,′_ ∙⟦_∣_⟧) (NE.map ♯ vars) + of clauseExprToPatLam (MatchExpr + [ (singlePatternFromPattern + (vArg (NE.foldl₁ (quote _,_ ◇⟦_∣_⟧) (NE.map (λ _ → quote ofʸ ◇⟦ ``refl ⟧) vars))) + , inj₂ (just `refl)) ]) toMapDiag : SinglePattern → SinglePattern → NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term) toMapDiag p@(_ , arg _ p₁) p'@(_ , arg _ p₂) = - (p NE.∷ [ p' ] , finishMatch (if ⌊ p₁ ≟-Pattern p₂ ⌋ then mapDiag (just p) else mapDiag nothing)) + (p NE.∷ [ p' ] , finishMatch (if ⌊ p₁ ≟-Pattern p₂ ⌋ then genBranch (just p) else genBranch nothing)) module _ ⦃ _ : TCOptions ⦄ where derive-DecEq : List (Name × Name) → UnquoteDecl @@ -118,6 +144,7 @@ private unquoteDecl DecEq-R1 = derive-DecEq [ (quote R1 , DecEq-R1) ] unquoteDecl DecEq-R2 = derive-DecEq [ (quote R2 , DecEq-R2) ] + unquoteDecl DecEq-R20 = derive-DecEq [ (quote R20 , DecEq-R20) ] unquoteDecl DecEq-M₁ DecEq-M₂ = derive-DecEq $ (quote M₁ , DecEq-M₁) ∷ (quote M₂ , DecEq-M₂) ∷ [] diff --git a/Tactic/Derive/TestTypes.agda b/Tactic/Derive/TestTypes.agda index 5d161352..254eda7c 100644 --- a/Tactic/Derive/TestTypes.agda +++ b/Tactic/Derive/TestTypes.agda @@ -42,6 +42,9 @@ record R2 {a} (A : Set a) : Set a where f5R2 : A f6R2 : A +record R20 : Set where + field r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14 r15 r16 r17 r18 r19 : Bool + data M₁ : Set data M₂ : Set data M₁ where