source: LTS/stack.ma @ 3570

Last change on this file since 3570 was 3570, checked in by piccolo, 4 years ago
File size: 7.0 KB
Line 
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
15include "variable.ma".
16
17inductive 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
25definition 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
35lemma eq_guard_combinator_elim : ∀P : bool → Prop.
36∀c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) →
37P(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]
42normalize #H1 #H2 try @H1 try @H2 //
43try(% #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]
47qed.
48
49inductive stack_seq:Type[0]≝
50| pop_Ass: variable → stack_seq
51| push : guard_combinators → stack_seq
52| popreg : variable → stack_seq.
53
54definition 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]
58| popreg v⇒ λy.match y with [popreg v' ⇒ eqb v v' | _ ⇒ false]
59].
60
61lemma eq_stack_seq_elim : ∀P : bool → Prop.
62∀x1,x2.(x1 = x2 → P true) → (x1 ≠ x2 → P false) →
63P(eq_stack_seq x1 x2).
64#P * [#v1 | #c1 | #v1 ] * [1,4,7: #v2 |2,5,8: #c2 |*: #v2] #H1 #H2 try(@H2 % #EQ destruct)
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 %
68| normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
69]
70qed.
71
72definition 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 …)) ]
75qed.
76
77definition 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 …)) ]
80qed.
81 
82definition stack_instr_params ≝ mk_instr_params DeqStackSeq (mk_DeqSet io_i io_i_eq io_i_eq_equality)
83 (mk_DeqSet unit (λ_.λ_.true) ?) (DeqSet_List DeqGuardCombinator) (mk_DeqSet unit (λ_.λ_.true) ?) (mk_DeqSet unit (λ_.λ_.true) ?).
84@hide_prf ** % // qed.
85
86definition stack_env_params ≝ mk_env_params ℕ.
87
88definition stack_state_params:state_params≝
89mk_state_params stack_instr_params stack_env_params flat_labels frame_store_t (*DeqEnv*).
90
91definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params) ≝
92λs,n.match \fst s with
93[nil ⇒ None ?
94|cons x xs ⇒ return 〈(n::x) :: xs,\snd s〉
95].
96
97definition pop : (store_type stack_state_params) → option (DeqNat × (store_type stack_state_params)) ≝
98λs.match \fst s with
99[nil ⇒ None ?
100|cons x xs ⇒ match x with
101             [ nil ⇒ None ?
102             | cons y ys ⇒ return 〈y,〈ys::xs,\snd s〉〉
103             ]
104             ].
105
106definition eval_combinators : guard_combinators → (store_type stack_state_params)→ option (store_type stack_state_params)≝
107λc,s.match c with
108[ push_var x ⇒ ! curr_env ← frame_current_env s;
109               ! n ← read_frame curr_env (to_shift+x) O;
110                 push s n
111| push_const n ⇒ push s n
112| push_plus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val2 + val1)
113| push_minus ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (val2 - val1)
114| push_eq ⇒ ! 〈val1,st1〉 ← pop s; ! 〈val2,st2〉 ← pop st1; push st2 (if eqb val2 val1 then 1 else O)
115| push_not ⇒ ! 〈val1,st1〉 ← pop s;push st1 (1-val1)
116].
117
118
119definition stack_eval_seq: (seq_instr stack_state_params)→(store_type stack_state_params)→ option (store_type stack_state_params)≝
120λi,s.match i with
121[ pop_Ass v ⇒ ! 〈val1,st1〉 ← pop s;frame_assign_var st1 (to_shift +v) val1
122| push c ⇒ eval_combinators c s
123| popreg v ⇒ frame_assign_var s (to_shift +v) (\snd (\snd s))
124].
125
126definition stack_eval_cond_cond:
127(list guard_combinators) → (store_type stack_state_params)→ option (bool × (store_type stack_state_params))≝
128λl,st.! fin_St ← m_fold Option … eval_combinators l st;
129      !〈val,st2〉← pop fin_St;
130      return 〈eqb val 1,st2〉.
131
132
133let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
134match n with
135[ O ⇒ nil ?
136| S m ⇒ a :: list_n … a m
137].
138
139definition stack_eval_call:(signature stack_state_params stack_state_params)→ act_params_type stack_state_params →
140frame_store_t → (option frame_store_t)≝
141λsgn.λvar,st.
142    !〈n,st1〉 ← pop st; 
143    frame_assign_var 〈(list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st1),(\snd st1)〉 to_shift n.
144
145definition stack_return_call:frame_store_t→ (option frame_store_t)≝
146λs.match (\fst s) with
147[nil⇒ None ?
148|cons hd tl⇒ !〈n,st1〉 ← pop s;
149             return 〈tl,〈(\fst (\snd s)),n〉〉
150].
151 
152definition stack_init_store ≝ λn : ℕ.〈[list_n … O (to_shift + n)],〈O,O〉〉.
153
154
155definition stack_sem_state_params : ℕ → sem_state_params stack_state_params ≝
156λn.mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
157(λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) (stack_init_store n).
158
159  (* Abitare tipo Instructions *)
160 
161definition stack_Instructions≝Instructions stack_state_params flat_labels.
162
163definition stack_signature≝signature stack_state_params stack_state_params.
164
165
166definition stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).
Note: See TracBrowser for help on using the repository browser.