Search code examples
context-free-grammaragda

Debugging constraint satisfaction errors in Agda with CFG example

I'm trying to implement this first example from Sipser's theory of computation, and am getting a yellow highlighting which is indecipherable. How does one debug these constraint errors in Agda generally, and in my example specifically? Are there any successful techniques for avoiding them in the first place? SipserExample1 below produces this mess:

_r2_61 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,18-23 ]
_r3_62 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,18-23 ]
_r2_66 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,28-33 ]
_r3_67 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,28-33 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  _r2_66 ++ inj₁ A0 ∷ _r3_67 = inj₁ A0 ∷ []
    : List (CFG.V Sipser1 ⊎ CFG.Σ' Sipser1)
    (blocked on _r2_66)
  _r2_66 ++ (inj₁ B0 ∷ []) ++ _r3_67 = _r2_61 ++ inj₁ A0 ∷ _r3_62
    : List (CFG.V Sipser1 ⊎ CFG.Σ' Sipser1)
    (blocked on any(_r2_61, _r3_62, _r2_66, _r3_67))
  _r2_61 ++ (inj₁ B0 ∷ []) ++ _r3_62
    = inj₂ a0 ∷ map inj₂ (a0 ∷ a# ∷ a1 ∷ a1 ∷ [])
    : List (CFG.V Sipser1 ⊎ CFG.Σ' Sipser1)
    (blocked on _r2_61)

Here is the code that produces the yellow. The CFG is a simple record, and I define the manystep reduction relation on lists of terminals and non-terminals. generation just allows the user to prove a list of terminals is admitted by a given CFG.

module toy where

open import Data.List 
open import Data.Sum using (_⊎_ ; inj₁; inj₂)
open import Data.Product using (_×_; _,_)
open import Data.Unit
open import Data.Empty

binRel : Set → Set → Set₁
binRel A B = A → B → Set

record CFG : Set₁ where
  field
    V : Set -- non-terminal, or variable
    Σ' : Set -- terminals
    R : binRel V (List (V ⊎ Σ'))-- rules
    S : V -- start symbol

module ManyStep where
  open CFG

  rule : CFG → Set
  rule cfg = List (V cfg ⊎ Σ' cfg)

  data ↦* (cfg : CFG) : rule cfg → rule cfg → Set where
    refl : {r : (rule cfg)} → ↦* cfg r r --∀ {σ : Σ' cfg} → {!!}
    trans : {r1 r2 r3 : (rule cfg)} {v : V cfg} {X : (rule cfg)} → R cfg v X
            → ↦* cfg r1 (r2 ++ (inj₁ v) ∷ r3)
            → ↦* cfg r1 (r2 ++ X ++ r3)

  derives : (cfg : CFG) → rule cfg → Set
  derives cfg x = ↦* cfg (inj₁ (S cfg) ∷ []) x

  generates : (cfg : CFG) → List (Σ' cfg) → Set
  generates cfg xs = derives cfg (map inj₂ xs)

open ManyStep public

data V0 : Set where
  A0 : V0
  B0 : V0

data Σ0 : Set where
  a0 : Σ0
  a1 : Σ0
  a# : Σ0

data _⟶_ : V0 → List (V0 ⊎ Σ0) → Set where
  r0 : A0 ⟶ (inj₂ a0 ∷ inj₁ A0 ∷ inj₂ a1 ∷ [])
  r1 : A0 ⟶ (inj₁ B0 ∷ [])
  r2 : B0 ⟶ (inj₂ a# ∷ [])

Sipser1 : CFG
Sipser1 = record { V = V0 ; Σ' = Σ0 ; R = _⟶_ ; S = A0 }

SipserExample1 : generates Sipser1 (a0 ∷ a0 ∷ a# ∷ a1 ∷ a1 ∷ [])
SipserExample1 = trans r1 (trans r1 (refl {Sipser1} {inj₁ A0 ∷ []}))

-----Edit-----

The correct solution is actually, with some insight from @Jesper, is:

SipserExample1 : generates Sipser1 (a0 ∷ a0 ∷ a# ∷ a1 ∷ a1 ∷ [])
SipserExample1 = trans {r2 = inj₂ a0 ∷ inj₂ a0 ∷ []} {r3 = inj₂ a1 ∷ inj₂ a1 ∷ []} r2
                 (trans {r2 = inj₂ a0 ∷ inj₂ a0 ∷ []} {r3 = inj₂ a1 ∷ inj₂ a1 ∷ []} r1
                 (trans {r2 = inj₂ a0 ∷ []} {r3 = inj₂ a1 ∷ []} r0

                 (trans {r2 = []} {r3 = []} r0 refl)))
Solution

  • My strategy for fixing this kind of issues is by ignoring the unsolved constraints at first and instead trying to help Agda filling in the unsolved metavariables, in your case the following part:

    _r2_61 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,18-23 ]
_r3_62 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,18-23 ]
_r2_66 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,28-33 ]
_r3_67 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,28-33 ]

    The nameing of these metavariables together with their position gives you a good clue: they are the second and third implicit arguments of first and second calls to the trans function in the body of SipserExample1. The next step is to make these implicit arguments explicit: write {r2 = ?} {r3 = ?} after the calls to trans, reload the file, and try filling in the holes until either the constraints disappear or you get a proper error message.

    PS: Often people prefer to write these kind of proofs in the equational reasoning style (see e.g. this example in the standard library), which would've forced you to spell out the implicit arguments in this case.