I'm using Agda 2.6.4.3 (which is the latest on brew) and I encountered the uncaught pattern violation panic. I know the code is probably buggy, but I didn't expect a panic.
Here's a small reproducer:
variable A B : Set
data ⊥ : Set where
¬_ : Set → Set
¬ A = A → ⊥
record _×_ (A : Set) (B : Set) : Set where
constructor _,_
field
π₁ : A
π₂ : B
infixr 20 _×_
data _⊎_ (A : Set) (B : Set) : Set where
inl : A → A ⊎ B
inr : B → A ⊎ B
data Dec : Set → Set₁ where
yes : A → Dec A
no : ¬ A → Dec A
forget : Dec A → Set
forget {A} _ = A
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
data ⊤ : Set where
tt : ⊤
data Symbol : Set where
s : Symbol
-- ...
data String : Set where
[] : String
_∷_ : Symbol → String → String
variable c : Symbol
w : String
_++_ : String → String → String
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
record Σ (A : Set) (B : A → Set) : Set where
constructor _,_
field
π₁ : A
π₂ : B π₁
infixr 20 _,_
Lang : Set₁
Lang = String → Set
variable V : Set
data Gram V : Set₁ where
∅ ε : Gram V
`_ : Symbol → Gram V
_·_ : {A : Set} → Dec A → Gram V → Gram V
_∪_ _▹_ : Gram V → Gram V → Gram V
var : V → Gram V
variable G G₁ G₂ : Gram V
⟦_⟧ : Gram ⊥ → Lang
⟦ ∅ ⟧ _ = ⊥
⟦ ε ⟧ w = w ≡ []
⟦ A · G ⟧ w = forget A × ⟦ G ⟧ w
⟦ G₁ ∪ G₂ ⟧ w = ⟦ G₁ ⟧ w ⊎ ⟦ G₂ ⟧ w
⟦ G₁ ▹ G₂ ⟧ w = Σ String λ u → Σ String λ v → (w ≡ (u ++ v)) × ⟦ G₁ ⟧ u × ⟦ G₂ ⟧ v
⟦ ` x ⟧ w = w ≡ (x ∷ [])
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4