10

ICFP 2012 で、Conor McBride はタイル「Agda-curious?」で基調講演を行いました。

小さなスタック マシンの実装が特徴でした。

ビデオは YouTube にあります: http://www.youtube.com/watch?v=XGyJ519RY6Y

コードもオンラインです: http://personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz

runパート 5 (コードをダウンロードした場合は「Part5Done.agda」)の機能について疑問に思っています。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' _ _ = {!!}

run関数の正しい型シグネチャは何ですか? 機能はどのrunように実装する必要がありますか?

コンパイル機能については、トークの約 55 分後に説明されています。

完全なコードは、Conor の Web ページ から入手できます。

4

1 に答える 1

9

起訴されたとして有罪、runからの関数のタイプ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)

これは、「スタック構成から始まり、スタック構成tsで終了するコードと構成でスタックを指定するts'と、構成tsでスタックを取得しますts'。「スタック構成」は、スタックにプッシュされるもののタイプのリストです。

ではPart5Done.agda、スタックが最初と最後に保持する型だけでなく、値によってもコードにインデックスが付けられます。したがって、run関数はコードの定義に織り込まれます。次に、コンパイラは、生成されたコードがrunに対応する動作を持たなければならないことを要求するように型指定されevalます。つまり、コンパイルされたコードの実行時の動作は、参照セマンティクスを尊重するようにバインドされています。そのコードを実行して、自分の目で正しいことがわかっていることを確認したい場合は、同じ行に沿って同じ関数を入力します。コード。

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)

または、型と値のインデックス付きコードを型インデックス付きコードにマップする明らかな消去関数を適用してから、古いrun関数を使用することもできます。Pierre-Évariste Dagand との装飾に関する私の仕事は、プログラムによって生成された余分なインデックスを体系的にタイプの上に重ね、後でそれをこすり落とすというこれらのパターンを自動化します。計算されたインデックスを消去し、消去されたバージョンから再計算すると、(GASP!) 消去したインデックスが正確に得られるというのは一般的な定理です。この場合、run同意するために入力されたコードを ning すると、eval実際には と同じ答えが得られることを意味しますeval。

于 2013-01-12T08:06:08.500 に答える