source: LTS/variable.ma @ 3562

Last change on this file since 3562 was 3562, checked in by piccolo, 5 years ago
File size: 5.1 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 (DeqProd activation_frame variable)) (DeqProd DeqNat DeqNat). (*frame_pointer e stack_pointer*)
55
56definition frame_env_params ≝ mk_env_params unit.
57
58definition frame_state_params:state_params≝
59mk_state_params imp_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
60
61definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return \fst hd.
62
63definition frame_assign_var ≝ λenv:frame_store_t.λv:variable.λn:DeqNat.
64match \fst env with
65[ nil ⇒ None ?
66| cons hd tl ⇒ let 〈e,var〉 ≝ hd in return 〈(〈assign_frame e v (\fst (\snd env)) n,var〉 :: tl),\snd env〉
67].
68
69definition frame_eval_seq:(seq_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝
70λi,s.match i with
71[sNop ⇒ Some ? s
72|sAss v e ⇒ !env ← frame_current_env … s;
73            ! n ← frame_sem_expr env e;
74            frame_assign_var s v n
75].
76
77
78definition frame_eval_io:(io_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝?.
79// qed.
80
81definition frame_eval_cond_cond:(cond_instr frame_state_params)→ (store_type frame_state_params)→ option (bool × (store_type frame_state_params))≝λc,s.
82!env ← frame_current_env s;
83!b ← frame_sem_condition env c;
84return 〈b,s〉.
85
86
87definition frame_eval_loop_cond:(loop_instr frame_state_params)→ (store_type frame_state_params)→ option (bool × (store_type frame_state_params))≝
88frame_eval_cond_cond.
89
90definition frame_eval_call:(signature frame_state_params imp_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
91λsgn,e,st.
92    let 〈var,act_exp〉 ≝ e in
93    !env ← frame_current_env … st;
94    !n ← frame_sem_expr env act_exp;
95    frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n.
96
97definition frame_return_call:(return_type frame_state_params)→ frame_store_t→ (option frame_store_t)≝
98λr,s.match (\fst s) with
99[nil⇒ None ?
100|cons hd tl⇒ let 〈env,v〉≝ hd in
101             !n ← frame_sem_expr env r;
102             frame_assign_var 〈tl,\snd s〉 v n
103].
104 
105
106definition frame_init_store: (store_type frame_state_params)≝ 〈[〈(nil ?),O〉],〈O,O〉〉.
107
108
109definition frame_sem_state_params : sem_state_params frame_state_params ≝ mk_sem_state_params frame_state_params frame_eval_seq frame_eval_io
110frame_eval_cond_cond frame_eval_loop_cond frame_eval_call frame_return_call frame_init_store.
111
112  (* Abitare tipo Instructions *)
113 
114definition frame_Instructions≝Instructions frame_state_params flat_labels.
115
116definition frame_signature≝signature frame_state_params frame_state_params.
117
118
119definition frame_envitem≝ (env_item frame_env_params imp_instr_params flat_labels).
Note: See TracBrowser for help on using the repository browser.