source: LTS/mono_stack.ma @ 3580

Last change on this file since 3580 was 3575, checked in by piccolo, 4 years ago
File size: 5.5 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 "stack.ma".
16
17definition mono_stack_store_t ≝ DeqProd (DeqSet_List DeqNat) (DeqProd DeqNat DeqNat).
18
19definition mono_stack_state_params:state_params≝
20mk_state_params stack_instr_params stack_env_params flat_labels mono_stack_store_t (*DeqEnv*).
21
22definition mono_push : mono_stack_store_t → DeqNat → mono_stack_store_t ≝
23λs,n.〈n::(\fst s),(\snd s)〉.
24
25definition mono_pop : (mono_stack_store_t) → option (DeqNat × (mono_stack_store_t)) ≝
26λs.match \fst s with
27[nil ⇒ None ?
28|cons x xs ⇒ return 〈x,〈xs,(\snd s)〉〉
29].
30
31definition mono_eval_combinators : guard_combinators → (mono_stack_store_t)→ option (mono_stack_store_t)≝
32λc,s.match c with
33[ push_var x ⇒ 
34                ! n ← read_frame (\fst s) (to_shift+x) (\fst (\snd s));
35                return mono_push s n
36| push_const n ⇒ return mono_push s n
37| push_plus ⇒ ! 〈val1,st1〉 ← mono_pop s; ! 〈val2,st2〉 ← mono_pop st1; return mono_push st2 (val2 + val1)
38| push_minus ⇒ ! 〈val1,st1〉 ← mono_pop s; ! 〈val2,st2〉 ← mono_pop st1; return mono_push st2 (val2 - val1)
39| push_eq ⇒ ! 〈val1,st1〉 ← mono_pop s; ! 〈val2,st2〉 ← mono_pop st1; return mono_push st2 (if eqb val2 val1 then 1 else O)
40| push_not ⇒ ! 〈val1,st1〉 ← mono_pop s;return mono_push st1 (1-val1)
41].
42
43definition mono_stack_eval_seq: stack_seq→
44mono_stack_store_t→ option mono_stack_store_t≝
45λi,s.match i with
46[ pop_Ass v ⇒ ! 〈val1,st1〉 ← mono_pop s; ! new_env ← (assign_frame (\fst s) (to_shift +v) (\fst (\snd s)) val1); return 〈new_env,(\snd s)〉
47| push c ⇒ mono_eval_combinators c s
48| popreg v ⇒ ! x ← assign_frame (\fst s) (to_shift +v) (\fst (\snd s)) (\snd (\snd s)); return 〈x,(\snd s)〉
49].
50
51definition mono_stack_eval_cond_cond:
52(list guard_combinators) → mono_stack_store_t→ option (bool × mono_stack_store_t)≝
53λl,st.! fin_St ← m_fold Option … mono_eval_combinators l st;
54      !〈val,st2〉← mono_pop fin_St;
55      return 〈eqb val 1,st2〉.
56
57definition mono_stack_signature≝signature mono_stack_state_params mono_stack_state_params.
58
59definition mono_stack_eval_call:mono_stack_signature →
60mono_stack_store_t → (option mono_stack_store_t)≝
61λsgn.λst.
62    !〈exp_val,st1〉 ← mono_pop st;
63    let new_fp ≝ (|(\fst st1)|) in
64    let st2 ≝ mono_push st1 (\fst (\snd st)) in
65    let st3 ≝ mono_push st2 O in
66    let st4 ≝ mono_push st3 exp_val in
67    let new_frame ≝ list_n … O (pred (to_shift + (f_pars … sgn))) in
68    return 〈new_frame @ (\fst st4),〈new_fp,(\snd(\snd st))〉〉.
69
70let rec reduce_list (A : Type[0]) (l : list A) (n : ℕ) on l : option (list A) ≝
71match n with
72[ O ⇒ return nil ?
73| S m ⇒ match l with
74  [ nil ⇒ None ?
75  | cons x xs ⇒ ! tl ← reduce_list … xs m; return cons ? x tl
76  ]
77].
78
79lemma reduce_list_def : ∀A : Type[0].∀l,l' : list A.∀n : ℕ.
80reduce_list … l n = return l' →
81|l'| = n ∧ ∃l''.l = l'@l''.
82#A #l elim l
83[ #l' * normalize [|#m] #EQ destruct % /2/ ]
84#x #xs #IH #l' * [ whd in ⊢ (??%% → ?); #EQ destruct % /2/]
85#m change with (m_bind ?????) in ⊢ (??%? → ?); #H
86cases(bind_inversion ????? H) -H #l'' * #EQl'' whd in ⊢ (??%% → ?);
87#EQ destruct % [ whd in match (length ??); @eq_f @(proj1 … (IH … EQl''))]
88cases(proj2 … (IH … EQl'')) #l''' #EQl''' %{l'''} >EQl''' %
89qed.
90
91definition mono_pop_frame : mono_stack_store_t → ℕ → option mono_stack_store_t ≝
92λst,n.! new_env ← reduce_list … (\fst st) n; return 〈new_env,(\snd st)〉.
93
94
95definition mono_stack_return_call:mono_stack_store_t → (option mono_stack_store_t)≝
96λs.!〈n,st1〉 ← mono_pop s;
97   ! new_fp ← read_frame (\fst st1) (\fst (\snd s)) O; (* 0 leggi il frame pointer precedente *)
98   ! st2 ← mono_pop_frame st1 (\fst (\snd s)) ;(* 1: accorciare la lista fino a diventare lunga come \snd st1 ovvero il frame pointer corrente *)
99   return 〈(\fst st2),〈new_fp,n〉〉. (* 3: ritornare lo stato con il nuovo fp *)
100
101definition mono_stack_init_store ≝ λn : ℕ.〈list_n … O  (to_shift + n),〈O,O〉〉.
102
103definition mono_stack_sem_state_params : ℕ → sem_state_params mono_stack_state_params ≝
104λn.mk_sem_state_params mono_stack_state_params mono_stack_eval_seq ?
105(λ_.mono_stack_eval_cond_cond (nil ?)) mono_stack_eval_cond_cond (λx.λ_.mono_stack_eval_call x) (λ_.mono_stack_return_call)
106(mono_stack_init_store n). * qed.
107
108  (* Abitare tipo Instructions *)
109 
110definition mono_stack_Instructions≝Instructions mono_stack_state_params flat_labels.
111
112
113definition mono_stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).
Note: See TracBrowser for help on using the repository browser.