{-# OPTIONS --without-K --safe #-}
module Lambda.Interpreter.Stack-sizes.Counterexample where
open import Colist
open import Equality.Propositional as E using (_≡_)
open import Prelude
open import Function-universe E.equality-with-J
open import Vec.Data E.equality-with-J
import Lambda.Compiler
import Lambda.Interpreter.Stack-sizes
import Lambda.Virtual-machine
import Lambda.Virtual-machine.Instructions
open import Lambda.Syntax Bool
open Closure Tm
def : Bool → Tm 1
def true = call false (con true)
def false = con true
module I = Lambda.Interpreter.Stack-sizes def
open Lambda.Compiler def
open Lambda.Virtual-machine.Instructions Bool
open module VM = Lambda.Virtual-machine comp-name
go : Tm 0
go = call true (con true)
stack-sizes-not-bisimilar :
¬ [ ∞ ] VM.stack-sizes ⟨ comp₀ go , [] , [] ⟩ ∼ I.stack-sizes go
stack-sizes-not-bisimilar =
[ ∞ ] VM.stack-sizes ⟨ comp₀ go , [] , [] ⟩ ∼ I.stack-sizes go ↝⟨ take-cong 8 ⟩
take 8 (VM.stack-sizes ⟨ comp₀ go , [] , [] ⟩) ≡
take 8 (I.stack-sizes go) ↔⟨⟩
0 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ 2 ∷ 1 ∷ [] ≡
0 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ 2 ∷ 2 ∷ 1 ∷ [] ↝⟨ (λ ()) ⟩□
⊥ □