Changeset 3570 for LTS/stack.ma


Ignore:
Timestamp:
Jun 17, 2015, 5:49:19 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/stack.ma

    r3566 r3570  
    4949inductive stack_seq:Type[0]≝
    5050| pop_Ass: variable → stack_seq
    51 | push : guard_combinators → stack_seq.
     51| push : guard_combinators → stack_seq
     52| popreg : variable → stack_seq.
    5253
    5354definition eq_stack_seq : stack_seq → stack_seq → bool ≝
     
    5556[ pop_Ass v1 ⇒ λy.match y with [pop_Ass v2 ⇒ eqb v1 v2 | _ ⇒ false ]
    5657| push c1 ⇒ λy.match y with [push c2 ⇒ eq_guard_combinator c1 c2 | _ ⇒ false]
     58| popreg v⇒ λy.match y with [popreg v' ⇒ eqb v v' | _ ⇒ false]
    5759].
    5860
     
    6062∀x1,x2.(x1 = x2 → P true) → (x1 ≠ x2 → P false) →
    6163P(eq_stack_seq x1 x2).
    62 #P * [#v1 | #c1] * [1,3: #v2 |*: #c2] #H1 #H2 try(@H2 % #EQ destruct)
     64#P * [#v1 | #c1 | #v1 ] * [1,4,7: #v2 |2,5,8: #c2 |*: #v2] #H1 #H2 try(@H2 % #EQ destruct)
    6365[ normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
    6466| whd in match eq_stack_seq; normalize nodelta @eq_guard_combinator_elim /2/
    6567 * #H @H2 % #EQ destruct @H %
     68| normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
    6669]
    6770qed.
     
    7881 
    7982definition stack_instr_params ≝ mk_instr_params DeqStackSeq (mk_DeqSet io_i io_i_eq io_i_eq_equality)
    80  (mk_DeqSet unit (λ_.λ_.true) ?) (DeqSet_List DeqGuardCombinator) variable (mk_DeqSet unit (λ_.λ_.true) ?).
     83 (mk_DeqSet unit (λ_.λ_.true) ?) (DeqSet_List DeqGuardCombinator) (mk_DeqSet unit (λ_.λ_.true) ?) (mk_DeqSet unit (λ_.λ_.true) ?).
    8184@hide_prf ** % // qed.
    8285
     
    8992λs,n.match \fst s with
    9093[nil ⇒ None ?
    91 |cons x xs ⇒ return 〈〈(n::(\fst x)),\snd x〉 :: xs,\snd s〉
     94|cons x xs ⇒ return 〈(n::x) :: xs,\snd s〉
    9295].
    9396
     
    9598λs.match \fst s with
    9699[nil ⇒ None ?
    97 |cons x xs ⇒ match \fst x with
     100|cons x xs ⇒ match x with
    98101             [ nil ⇒ None ?
    99              | cons y ys ⇒ return 〈y,〈〈ys,\snd x〉::xs,\snd s〉〉
     102             | cons y ys ⇒ return 〈y,〈ys::xs,\snd s〉〉
    100103             ]
    101104             ].
     
    118121[ pop_Ass v ⇒ ! 〈val1,st1〉 ← pop s;frame_assign_var st1 (to_shift +v) val1
    119122| push c ⇒ eval_combinators c s
     123| popreg v ⇒ frame_assign_var s (to_shift +v) (\snd (\snd s))
    120124].
    121125
     
    137141λsgn.λvar,st.
    138142    !〈n,st1〉 ← pop st; 
    139     frame_assign_var 〈(〈list_n … O (pred (to_shift + (f_pars … sgn))),var〉::(\fst st1)),(\snd st1)〉 to_shift n.
     143    frame_assign_var 〈(list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st1),(\snd st1)〉 to_shift n.
    140144
    141145definition stack_return_call:frame_store_t→ (option frame_store_t)≝
    142146λs.match (\fst s) with
    143147[nil⇒ None ?
    144 |cons hd tl⇒ let 〈env,v〉≝ hd in
    145              !〈n,st1〉 ← pop s;
    146              frame_assign_var 〈tl,\snd s〉 v n
     148|cons hd tl⇒ !〈n,st1〉 ← pop s;
     149             return 〈tl,〈(\fst (\snd s)),n〉〉
    147150].
    148151 
    149 definition stack_init_store ≝ λn : ℕ.〈[〈list_n … O (to_shift + n),O〉],〈O,O〉〉.
     152definition stack_init_store ≝ λn : ℕ.〈[list_n … O (to_shift + n)],〈O,O〉〉.
    150153
    151154
Note: See TracChangeset for help on using the changeset viewer.