Changeset 3570 for LTS/stack.ma
 Timestamp:
 Jun 17, 2015, 5:49:19 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/stack.ma
r3566 r3570 49 49 inductive stack_seq:Type[0]≝ 50 50  pop_Ass: variable → stack_seq 51  push : guard_combinators → stack_seq. 51  push : guard_combinators → stack_seq 52  popreg : variable → stack_seq. 52 53 53 54 definition eq_stack_seq : stack_seq → stack_seq → bool ≝ … … 55 56 [ pop_Ass v1 ⇒ λy.match y with [pop_Ass v2 ⇒ eqb v1 v2  _ ⇒ false ] 56 57  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] 57 59 ]. 58 60 … … 60 62 ∀x1,x2.(x1 = x2 → P true) → (x1 ≠ x2 → P false) → 61 63 P(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) 63 65 [ normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 %  * #H @H2 % #EQ destruct @H %] 64 66  whd in match eq_stack_seq; normalize nodelta @eq_guard_combinator_elim /2/ 65 67 * #H @H2 % #EQ destruct @H % 68  normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 %  * #H @H2 % #EQ destruct @H %] 66 69 ] 67 70 qed. … … 78 81 79 82 definition 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) ?). 81 84 @hide_prf ** % // qed. 82 85 … … 89 92 λs,n.match \fst s with 90 93 [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〉 92 95 ]. 93 96 … … 95 98 λs.match \fst s with 96 99 [nil ⇒ None ? 97 cons x xs ⇒ match \fstx with100 cons x xs ⇒ match x with 98 101 [ nil ⇒ None ? 99  cons y ys ⇒ return 〈y,〈 〈ys,\snd x〉::xs,\snd s〉〉102  cons y ys ⇒ return 〈y,〈ys::xs,\snd s〉〉 100 103 ] 101 104 ]. … … 118 121 [ pop_Ass v ⇒ ! 〈val1,st1〉 ← pop s;frame_assign_var st1 (to_shift +v) val1 119 122  push c ⇒ eval_combinators c s 123  popreg v ⇒ frame_assign_var s (to_shift +v) (\snd (\snd s)) 120 124 ]. 121 125 … … 137 141 λsgn.λvar,st. 138 142 !〈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. 140 144 141 145 definition stack_return_call:frame_store_t→ (option frame_store_t)≝ 142 146 λs.match (\fst s) with 143 147 [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〉〉 147 150 ]. 148 151 149 definition stack_init_store ≝ λn : ℕ.〈[ 〈list_n … O (to_shift + n),O〉],〈O,O〉〉.152 definition stack_init_store ≝ λn : ℕ.〈[list_n … O (to_shift + n)],〈O,O〉〉. 150 153 151 154
Note: See TracChangeset
for help on using the changeset viewer.