Agda: funzione di esecuzione per l'esempio di pila Conor

Question

All'ICFP 2012, Conor McBride ha fornito una nota chiave con la tessera "Agda-curioso?".

Ha presentato un'implementazione di una piccola impilatrice.

Il video è su YouTube: http://www.youtube.com/watch?v=XGyJ519RY6Y

Il codice è anche online: http://personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz

Mi chiedo sulla funzione run della parte 5 (vale a dire "Part5Done.agda" se è stato scaricato il codice). La conversazione si interrompe prima che venga spiegata la funzione run.

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' _ _ = {!!} 

Qual è il tipo di firma corretta della funzione run? Come dovrebbe essere implementata la funzione run?

La funzione di compilazione è spiegata about 55 minutes into the talk.

Il codice completo è available from Conor's webpage.

Answer 1

e colpevole, il tipo della funzione run da 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) 

ciò equivale a dire "codice Dato che parte dalla configurazione pila ts e termina in configurazione sovrapposta ts' e una pila in configurazione ts, si otterrà una catasta nella configurazione ts'. Una "configurazione di stack" è una lista dei tipi di cose spinte nello stack

In Part5Done.agda, il codice è in dexed non solo dai tipi di ciò che la pila tiene inizialmente e infine ma anche dai valori. La funzione run viene così inserita nella definizione del codice. Il compilatore viene quindi digitato per richiedere che il codice prodotto abbia un comportamento run corrispondente a eval. Cioè, il comportamento in fase di esecuzione del codice compilato è destinato a rispettare la semantica di riferimento. Se vuoi eseguire quel codice, per vedere con i tuoi occhi quello che sai essere vero, digita la stessa funzione lungo le stesse linee, eccetto che dobbiamo selezionare i tipi da soli dalle coppie tipi-e-valori che indicizzano il tipo codice.

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) 

In alternativa, è possibile applicare la funzione di cancellazione ovvio che mappa il codice tipi-e-valori-indicizzato codice tipi-indicizzati, quindi utilizzare la vecchia funzione run. Il mio lavoro con Pierre-Évariste Dagand sugli ornamenti automatizza questi schemi di stratificazione di un indice aggiuntivo indotto da un programma sistematicamente su un tipo e quindi sfregandolo in un secondo momento. È un teorema generico che se cancelli l'indice calcolato lo ricalcoli dalla versione cancellata, ottieni (GASP!) Esattamente l'indice che hai cancellato. In questo caso, ciò significa che run il codice digitato per concordare con eval fornirà effettivamente la stessa risposta di eval.