[3560] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
| 15 | include "variable.ma". |
---|
| 16 | |
---|
| 17 | inductive guard_combinators : Type[0] ≝ |
---|
| 18 | | push_var: variable → guard_combinators |
---|
| 19 | | push_const : DeqNat → guard_combinators |
---|
| 20 | | push_plus : guard_combinators |
---|
| 21 | | push_minus : guard_combinators |
---|
| 22 | | push_eq : guard_combinators |
---|
| 23 | | push_not : guard_combinators. |
---|
| 24 | |
---|
| 25 | definition eq_guard_combinator : guard_combinators → guard_combinators → bool ≝ |
---|
| 26 | λx.match x with |
---|
| 27 | [ push_var v1⇒ λy.match y with [push_var v2 ⇒ eqb v1 v2 | _ ⇒ false] |
---|
| 28 | | push_const n1 ⇒ λy.match y with [push_const n2 ⇒ eqb n1 n2 | _ ⇒ false] |
---|
| 29 | | push_plus ⇒ λy.match y with [push_plus ⇒ true | _ ⇒ false ] |
---|
| 30 | | push_minus ⇒ λy.match y with [push_minus ⇒ true | _⇒ false ] |
---|
| 31 | | push_eq ⇒ λy.match y with [push_eq ⇒ true | _ ⇒ false ] |
---|
| 32 | | push_not ⇒ λy.match y with [push_not ⇒ true | _ ⇒ false ] |
---|
| 33 | ]. |
---|
| 34 | |
---|
| 35 | lemma eq_guard_combinator_elim : ∀P : bool → Prop. |
---|
| 36 | ∀c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → |
---|
| 37 | P(eq_guard_combinator c1 c2). |
---|
| 38 | #P * |
---|
| 39 | [#v1 | #n1 ] |
---|
| 40 | * |
---|
| 41 | [1,7,13,19,25,31: #v2 |2,8,14,20,26,32: #n2] |
---|
| 42 | normalize #H1 #H2 try @H1 try @H2 // |
---|
| 43 | try(% #EQ destruct) |
---|
| 44 | [ @(eqb_elim … v1 v2) [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %] |
---|
| 45 | | @(eqb_elim … n1 n2) [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %] |
---|
| 46 | ] |
---|
| 47 | qed. |
---|
| 48 | |
---|
| 49 | inductive stack_seq:Type[0]≝ |
---|
| 50 | | pop_Ass: variable → stack_seq |
---|
[3570] | 51 | | push : guard_combinators → stack_seq |
---|
| 52 | | popreg : variable → stack_seq. |
---|
[3560] | 53 | |
---|
| 54 | definition eq_stack_seq : stack_seq → stack_seq → bool ≝ |
---|
| 55 | λx.match x with |
---|
| 56 | [ pop_Ass v1 ⇒ λy.match y with [pop_Ass v2 ⇒ eqb v1 v2 | _ ⇒ false ] |
---|
| 57 | | push c1 ⇒ λy.match y with [push c2 ⇒ eq_guard_combinator c1 c2 | _ ⇒ false] |
---|
[3570] | 58 | | popreg v⇒ λy.match y with [popreg v' ⇒ eqb v v' | _ ⇒ false] |
---|
[3560] | 59 | ]. |
---|
| 60 | |
---|
| 61 | lemma eq_stack_seq_elim : ∀P : bool → Prop. |
---|
| 62 | ∀x1,x2.(x1 = x2 → P true) → (x1 ≠ x2 → P false) → |
---|
| 63 | P(eq_stack_seq x1 x2). |
---|
[3570] | 64 | #P * [#v1 | #c1 | #v1 ] * [1,4,7: #v2 |2,5,8: #c2 |*: #v2] #H1 #H2 try(@H2 % #EQ destruct) |
---|
[3560] | 65 | [ normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %] |
---|
| 66 | | whd in match eq_stack_seq; normalize nodelta @eq_guard_combinator_elim /2/ |
---|
| 67 | * #H @H2 % #EQ destruct @H % |
---|
[3570] | 68 | | normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %] |
---|
[3560] | 69 | ] |
---|
| 70 | qed. |
---|
| 71 | |
---|
| 72 | definition DeqStackSeq ≝ mk_DeqSet stack_seq eq_stack_seq ?. |
---|
| 73 | @hide_prf #x #y @eq_stack_seq_elim |
---|
| 74 | [ #EQ destruct % // | * #H % [ #EQ destruct | #EQ destruct cases(H (refl …)) ] |
---|
| 75 | qed. |
---|
| 76 | |
---|
| 77 | definition DeqGuardCombinator ≝ mk_DeqSet guard_combinators eq_guard_combinator ?. |
---|
| 78 | @hide_prf #x #y @eq_guard_combinator_elim |
---|
| 79 | [ #EQ destruct % // | * #H % [ #EQ destruct | #EQ destruct cases(H (refl …)) ] |
---|
| 80 | qed. |
---|
| 81 | |
---|
[3575] | 82 | definition stack_instr_params ≝ mk_instr_params DeqStackSeq DeqFalse |
---|
| 83 | DeqUnit (DeqSet_List DeqGuardCombinator) DeqUnit DeqUnit. |
---|
[3560] | 84 | |
---|
[3566] | 85 | definition stack_env_params ≝ mk_env_params ℕ. |
---|
| 86 | |
---|
[3560] | 87 | definition stack_state_params:state_params≝ |
---|
[3566] | 88 | mk_state_params stack_instr_params stack_env_params flat_labels frame_store_t (*DeqEnv*). |
---|
[3560] | 89 | |
---|
[3575] | 90 | definition push : frame_store_t → DeqNat → option frame_store_t ≝ |
---|
[3560] | 91 | λs,n.match \fst s with |
---|
| 92 | [nil ⇒ None ? |
---|
[3570] | 93 | |cons x xs ⇒ return 〈(n::x) :: xs,\snd s〉 |
---|
[3560] | 94 | ]. |
---|
| 95 | |
---|
[3575] | 96 | definition pop : frame_store_t → option (DeqNat × frame_store_t) ≝ |
---|
[3560] | 97 | λs.match \fst s with |
---|
| 98 | [nil ⇒ None ? |
---|
[3570] | 99 | |cons x xs ⇒ match x with |
---|
[3560] | 100 | [ nil ⇒ None ? |
---|
[3570] | 101 | | cons y ys ⇒ return 〈y,〈ys::xs,\snd s〉〉 |
---|
[3560] | 102 | ] |
---|
| 103 | ]. |
---|
| 104 | |
---|
[3575] | 105 | definition eval_combinators : guard_combinators → frame_store_t→ option frame_store_t≝ |
---|
[3560] | 106 | λc,s.match c with |
---|
| 107 | [ push_var x ⇒ ! curr_env ← frame_current_env s; |
---|
| 108 | ! n ← read_frame curr_env (to_shift+x) O; |
---|
| 109 | push s n |
---|
| 110 | | push_const n ⇒ push s n |
---|
[3565] | 111 | | push_plus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val2 + val1) |
---|
| 112 | | push_minus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val2 - val1) |
---|
| 113 | | push_eq ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (if eqb val2 val1 then 1 else O) |
---|
[3560] | 114 | | push_not ⇒ ! 〈val1,st1〉 ← pop s;push st1 (1-val1) |
---|
| 115 | ]. |
---|
| 116 | |
---|
| 117 | |
---|
[3575] | 118 | definition stack_eval_seq: stack_seq→frame_store_t→ option frame_store_t≝ |
---|
[3560] | 119 | λi,s.match i with |
---|
| 120 | [ pop_Ass v ⇒ ! 〈val1,st1〉 ← pop s;frame_assign_var st1 (to_shift +v) val1 |
---|
| 121 | | push c ⇒ eval_combinators c s |
---|
[3570] | 122 | | popreg v ⇒ frame_assign_var s (to_shift +v) (\snd (\snd s)) |
---|
[3560] | 123 | ]. |
---|
| 124 | |
---|
| 125 | definition stack_eval_cond_cond: |
---|
[3575] | 126 | (list guard_combinators) → frame_store_t→ option (bool × frame_store_t)≝ |
---|
[3560] | 127 | λl,st.! fin_St ← m_fold Option … eval_combinators l st; |
---|
| 128 | !〈val,st2〉← pop fin_St; |
---|
| 129 | return 〈eqb val 1,st2〉. |
---|
| 130 | |
---|
| 131 | |
---|
[3575] | 132 | definition stack_signature≝signature stack_state_params stack_state_params. |
---|
| 133 | |
---|
| 134 | definition stack_eval_call:stack_signature→ |
---|
[3560] | 135 | frame_store_t → (option frame_store_t)≝ |
---|
[3575] | 136 | λsgn.λst. |
---|
[3566] | 137 | !〈n,st1〉 ← pop st; |
---|
[3582] | 138 | frame_assign_var 〈(list_n … O (to_shift + (f_pars … sgn)))::(\fst st1),(\snd st1)〉 to_shift n. |
---|
[3560] | 139 | |
---|
| 140 | definition stack_return_call:frame_store_t→ (option frame_store_t)≝ |
---|
| 141 | λs.match (\fst s) with |
---|
| 142 | [nil⇒ None ? |
---|
[3570] | 143 | |cons hd tl⇒ !〈n,st1〉 ← pop s; |
---|
| 144 | return 〈tl,〈(\fst (\snd s)),n〉〉 |
---|
[3560] | 145 | ]. |
---|
| 146 | |
---|
[3570] | 147 | definition stack_init_store ≝ λn : ℕ.〈[list_n … O (to_shift + n)],〈O,O〉〉. |
---|
[3560] | 148 | |
---|
| 149 | |
---|
[3566] | 150 | definition stack_sem_state_params : ℕ → sem_state_params stack_state_params ≝ |
---|
| 151 | λn.mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io |
---|
[3575] | 152 | (λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond (λsgn.λ_.stack_eval_call sgn) (λ_.stack_return_call) (stack_init_store n). |
---|
[3560] | 153 | |
---|
| 154 | (* Abitare tipo Instructions *) |
---|
| 155 | |
---|
| 156 | definition stack_Instructions≝Instructions stack_state_params flat_labels. |
---|
| 157 | |
---|
| 158 | |
---|
[3566] | 159 | definition stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels). |
---|