Agda: Conor'un yığın örneği için işlev çalıştırma

Question

ICFP 2012'de Conor McBride, "Agda-meraklısı" kutucuğuyla bir açılış notu verdi.

Küçük bir yığın makine uygulaması özellikli.

Video youtube geçerli: http://www.youtube.com/watch?v=XGyJ519RY6Y

kod edilir çevrimiçi çok: kodu indirilen eğer Bölüm 5 (yani "Part5Done.agda" nin run işlevi hakkında merak ediyorum http://personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz

). Konuşma, run işlevinin açıklanmasından önce durur. run fonksiyonunun doğru türde imza

data Inst : Rel Sg SC Stk where 
    PUSH : {t : Ty} (v : El t) -> forall {ts vs} -> 
      Inst (ts & vs) ((t , ts) & (E v , vs)) 
    ADD : {x y : Nat}{ts : SC}{vs : Stk ts} -> 
      Inst ((nat , nat , ts) & (E y , E x , vs)) 
       ((nat , ts) & (E (x + y) , vs)) 
    IFPOP : forall {ts vs ts' vst vsf b} -> 
      List Inst (ts & vs) (ts' & vst) -> List Inst (ts & vs) (ts' & vsf) 
      -> Inst ((bool , ts) & (E b , vs)) (ts' & if b then vst else vsf) 

postulate 
    Level : Set 
    zl : Level 
    sl : Level -> Level 

{-# BUILTIN LEVEL Level #-} 
{-# BUILTIN LEVELZERO zl #-} 
{-# BUILTIN LEVELSUC sl #-} 

data _==_ {l : Level}{X : Set l}(x : X) : X -> Set l where 
    refl : x == x 

{-# BUILTIN EQUALITY _==_ #-} 
{-# BUILTIN REFL refl #-} 


fact : forall {T S} -> (b : Bool)(t f : El T)(s : Stk S) -> 
     (E (if b then t else f) , s) == 
     (if b then (E t , s) else (E f , s)) 
fact tt t f s = refl 
fact ff t f s = refl 

compile : {t : Ty} -> (e : Expr t) -> forall {ts vs} -> 
    List Inst (ts & vs) ((t , ts) & (E (eval e) , vs)) 
compile (val y)  = PUSH y , [] 
compile (e1 +' e2) = compile e1 ++ compile e2 ++ ADD , [] 
compile (if' e0 then e1 else e2) {vs = vs} 
    rewrite fact (eval e0) (eval e1) (eval e2) vs 
    = compile e0 ++ IFPOP (compile e1) (compile e2) , [] 

{- 
-- ** old run function from Part4Done.agda 
run : forall {ts ts'} -> List Inst ts ts' -> List Elt ts [] -> List Elt ts' [] 
run []    vs    = vs 
run (PUSH v , is) vs    = run is (E v , vs) 
run (ADD  , is) (E v2 , E v1 , vs) = run is (E 0 , vs) 
run (IFPOP is1 is2 , is) (E tt , vs) = run is (run is2 vs) 
run (IFPOP is1 is2 , is) (E ff , vs) = run is (run is1 vs) 
-} 

run : forall {i j} -> List Inst i j -> Sg Stack (λ s -> s == i) → (Sg SC Stk) 
run {vs & vstack} [] _ 
    = (vs & vstack) 
run _ _ = {!!} -- I have no clue about the other cases... 

--Perhaps the correct type is: 
run' : forall {i j} -> List Inst i j -> Sg Stack (λ s -> s == i) → Sg (Sg SC Stk) (λ s → s == j) 
run' _ _ = {!!} 

nedir? run işlevi nasıl uygulanmalıdır?

Derleme işlevi about 55 minutes into the talk açıklanmıştır.

Kodun tamamı available from Conor's webpage'dur. kalırken Suçlu

Answer 1

, Part4Done.agda den run fonksiyon türü, baca düzeni ts başlar ve baca düzeni ts' ve konfigürasyon ts bir istif içinde tamamlanır "Verilen kod demek anlamına gelir

run : forall {ts ts'} -> List Inst ts ts' -> List Elt ts [] -> List Elt ts' [] 
run []    vs    = vs 
run (PUSH v , is) vs    = run is (E v , vs) 
run (ADD  , is) (E v2 , E v1 , vs) = run is (E 0 , vs) 
run (IFPOP is1 is2 , is) (E tt , vs) = run is (run is2 vs) 
run (IFPOP is1 is2 , is) (E ff , vs) = run is (run is1 vs) 

olduğu ts' yapılandırmasında bir yığın alırsınız. "Yığın yapılandırması", yığında itilen şeylerin türlerinin bir listesidir.

Part5Done.agda'da, kod yalnızca yığının başlangıçta ve nihayetinde tuttuğu türlerle değil, aynı zamanda değerlerle de giderildi. run işlevi bu nedenle kodun tanımına dokunmuştur. Derleyici, üretilen kodun, eval'a karşılık gelen run davranışına sahip olmasını gerektirecek şekilde yazılır. Yani, derlenmiş kodun çalışma zamanı davranışı, referans semantiğine uymak zorundadır. Eğer bu kodu çalıştırmak istiyorsanız, kendi gözlerinizle doğru olduğunu bildiklerinizi görmek için, aynı satırları aynı satırlara yazınız, sadece bu türleri indeksleyen tip ve değer çiftlerinden tek tek seçmemiz gerekir. kodu.

run : forall {ts ts' vs vs'} -> List Inst (ts & vs) (ts' & vs') -> 
     List Elt ts [] -> List Elt ts' [] 
run []    vs    = vs 
run (PUSH v , is) vs    = run is (E v , vs) 
run (ADD  , is) (E v2 , E v1 , vs) = run is (E (v1 + v2) , vs) 
run (IFPOP is1 is2 , is) (E tt , vs) = run is (run is1 vs) 
run (IFPOP is1 is2 , is) (E ff , vs) = run is (run is2 vs) 

Alternatif olarak, tip-endeksli koduna türleri-ve-değerleri-endeksli kodu eşler bariz silme fonksiyonu uygulayabilir, daha sonra eski run işlevini kullanın. Pierre-Évariste Dagand ile süslerindeki numaralı süslemelerle yaptığım çalışmam, bu katman katmanlarını bir programın sistematik olarak bir tür üzerinde başlattığı ve daha sonra ovalayarak ek bir diziyi otomatik hale getiriyor. Bu, hesaplanmış dizini silerseniz ve silinen sürümden yeniden hesaplarsanız, (GASP!) Tam olarak sildiğiniz dizini aldığınız genel bir teoremdir. Bu durumda, eval ile aynı hizada yazılan kodun run ning kodu eval ile aynı cevabı verecektir.