open import config module machine.eval {Inst Value} (CAM→ : MakeConfig Inst Value → MakeConfig Inst Value → Set) where open import Data.List open import config public Config = MakeConfig Inst Value data CAM→* : Config → Config → Set where refl : ∀ {M} → CAM→* M M trans : ∀ {L N M} → CAM→* M N → CAM→ L M → CAM→* L N data Finished : Config → Set where empty : ∀ {e} → Finished ⟨ [] ∣ e ∣ [] ⟩ data Result (C : Config) : Set where done : Finished C → Result C stuck : Result C Steps = List Config createSteps : ∀ {A B} → CAM→* A B → Steps createSteps {B = B} refl = [ B ] createSteps {A} (trans x _) = A ∷ (createSteps x)