source: LTS/variable.ma @ 3566

Last change on this file since 3566 was 3566, checked in by piccolo, 4 years ago
File size: 5.8 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 "imp.ma".
16
17definition to_shift : ℕ ≝ 2.
18
19definition activation_frame ≝ DeqSet_List DeqNat.
20
21let rec update (A : Type[0]) (l : list A) (n : ℕ) (a : A) (def : A) on n : list A ≝
22match l with
23[ nil ⇒ match n with [ O ⇒ [a] | S m ⇒ def :: update … (nil ?) m a def ]
24| cons x xs ⇒ match n with [O ⇒ a :: xs | S m ⇒ x :: update … xs m a def]
25].
26
27definition assign_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.λn:DeqNat.update … env (|env| - v - fp -1) n O.
28
29definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (|env| -v -fp -1) env.
30
31let rec frame_sem_expr (env:activation_frame) (e: expr) on e : (option nat) ≝
32 match e with
33  [ Var v ⇒ read_frame env (to_shift+v) O
34  | Const n ⇒ Some ? n
35  | Plus e1 e2 ⇒ !n1 ← frame_sem_expr env e1;
36                 !n2 ← frame_sem_expr env e2;
37                 return (n1+n2)
38  | Minus e1 e2 ⇒ !n1 ← frame_sem_expr env e1;
39                  !n2 ← frame_sem_expr env e2;
40                  return (n1-n2)
41  ].
42
43let rec frame_sem_condition (env:activation_frame) (c:condition) on c : option bool ≝
44  match c with
45   [ Eq e1 e2 ⇒ !n ← frame_sem_expr env e1;
46                !m ← frame_sem_expr env e2;
47                return (eqb n m)
48   | Not c ⇒ !b ← frame_sem_condition env c;
49             return (notb b)
50   ].
51
52
53
54definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*)
55
56definition frame_env_params ≝ mk_env_params unit.
57
58inductive frame_seq_i : Type[0] ≝
59| Seq_i : seq_i → frame_seq_i
60| PopReg : variable → frame_seq_i.
61
62definition eq_frame_seq_i : frame_seq_i → frame_seq_i → bool ≝
63λx,y.
64match x with
65[ Seq_i s ⇒ match y with [Seq_i s' ⇒ seq_i_eq s s' | _ ⇒ false ]
66| PopReg v ⇒ match y with [PopReg v' ⇒ eqb v v' | _ ⇒ false]
67].
68
69definition DeqFrameSeqI ≝ mk_DeqSet frame_seq_i eq_frame_seq_i ?.
70@hide_prf cases daemon qed.
71
72definition frame_instr_params : instr_params ≝
73mk_instr_params ? ? ? ? ? ?.
74[ @DeqFrameSeqI
75|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
76|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
77|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
78|@(DeqProd variable DeqExpr)
79|@DeqExpr].qed.
80
81definition frame_state_params:state_params≝
82mk_state_params frame_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
83
84definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return hd.
85
86definition frame_assign_var ≝ λenv:frame_store_t.λv:variable.λn:DeqNat.
87match \fst env with
88[ nil ⇒ None ?
89| cons hd tl ⇒ return 〈(assign_frame hd v (\fst (\snd env)) n :: tl),\snd env〉
90].
91
92definition frame_eval_seq:(seq_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝
93λi,s.match i with
94[ Seq_i instr ⇒
95   match instr with
96   [sNop ⇒ Some ? s
97   |sAss v e ⇒ !env ← frame_current_env … s;
98               ! n ← frame_sem_expr env e;
99               frame_assign_var s v n
100   ]
101| PopReg v ⇒ frame_assign_var s v (\snd (\snd s))
102].
103
104
105definition frame_eval_io:(io_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝?.
106// qed.
107
108definition frame_eval_cond_cond:(cond_instr frame_state_params)→ (store_type frame_state_params)→ option (bool × (store_type frame_state_params))≝λc,s.
109!env ← frame_current_env s;
110!b ← frame_sem_condition env c;
111return 〈b,s〉.
112
113
114definition frame_eval_loop_cond:(loop_instr frame_state_params)→ (store_type frame_state_params)→ option (bool × (store_type frame_state_params))≝
115frame_eval_cond_cond.
116
117definition frame_eval_call:(signature frame_state_params frame_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
118λsgn,e,st.
119    let 〈var,act_exp〉 ≝ e in
120    !env ← frame_current_env … st;
121    !n ← frame_sem_expr env act_exp;
122    frame_assign_var 〈((nil ?)::(\fst st)),(\snd st)〉 to_shift n.
123
124definition frame_return_call:(return_type frame_state_params)→ frame_store_t→ (option frame_store_t)≝
125λr,s.match (\fst s) with
126[nil⇒ None ?
127|cons hd tl⇒ !n ← frame_sem_expr hd r;
128             return 〈tl,〈(\fst (\snd s)),n〉〉
129].
130 
131definition frame_init_store: (store_type frame_state_params)≝ 〈[(nil ?)],〈O,O〉〉.
132
133
134definition frame_sem_state_params : sem_state_params frame_state_params ≝ mk_sem_state_params frame_state_params frame_eval_seq frame_eval_io
135frame_eval_cond_cond frame_eval_loop_cond frame_eval_call frame_return_call frame_init_store.
136
137  (* Abitare tipo Instructions *)
138 
139definition frame_Instructions≝Instructions frame_state_params flat_labels.
140
141definition frame_signature≝signature frame_state_params frame_state_params.
142
143
144definition frame_envitem≝ (env_item frame_env_params frame_instr_params flat_labels).
Note: See TracBrowser for help on using the repository browser.