Changeset 761
- Timestamp:
- Apr 19, 2011, 12:22:32 PM (9 years ago)
- Location:
- src
- Files:
-
- 2 added
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/BitVectorTrie.ma
r726 r761 1 1 include "basics/types.ma". 2 2 3 include "utilities/option.ma". 3 4 include "ASM/BitVector.ma". 4 5 … … 75 76 ] 76 77 qed. 78 79 let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝ 80 (match b with 81 [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with 82 [ Leaf _ ⇒ λ_. Some ? (Leaf A a) 83 | Stub _ ⇒ λ_. None ? 84 | Node _ _ _ ⇒ λprf. ⊥ 85 ] (refl ? O) 86 | VCons o hd tl ⇒ λt. 87 match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with 88 [ Leaf l ⇒ λprf.⊥ 89 | Node p l r ⇒ λprf. 90 match hd with 91 [ true ⇒ option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉)) 92 | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉)) 93 ] 94 | Stub p ⇒ λprf. None ? 95 ] (refl ? (S o)) 96 ]). 97 [ 1,2: destruct 98 |*: 99 @ injective_S @sym_eq @prf 100 ] 101 qed. -
src/Cminor/semantics.ma
r760 r761 134 134 ]. 135 135 136 definition init_locals : env → list ident → env ≝ 137 foldr ?? (λid,en. add ?? en id Vundef). 138 136 139 definition eval_step : genv → state → IO io_out io_in (trace × state) ≝ 137 140 λge,st. … … 149 152 | St_assign id e ⇒ 150 153 ! 〈tr,v〉 ← eval_expr ge e en sp m; 151 ret ? 〈tr, State f St_skip (add ?? en id v) m sp k〉 154 ! en' ← update ?? en id v; 155 ret ? 〈tr, State f St_skip en' m sp k〉 152 156 | St_store chunk edst e ⇒ 153 157 ! 〈tr,vdst〉 ← eval_expr ge edst en sp m; … … 204 208 let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in 205 209 ! en ← bind_params args (f_params f); 206 ret ? 〈E0, State f (f_body f) enm' sp k〉210 ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉 207 211 | External fn ⇒ 208 212 ! evargs ← check_eventval_list args (sig_args (ef_sig fn)); … … 217 221 [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ] 218 222 | Some v ⇒ match dst with [ None ⇒ Error ? 219 | Some id ⇒ OK ? (add ?? en id v)]223 | Some id ⇒ update ?? en id v ] 220 224 ]; 221 225 ret ? 〈E0, State f St_skip en' m sp k'〉 -
src/RTLabs/RTLabs-sem.ma
r751 r761 48 48 definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m. 49 49 50 definition init_locals : list register → register_env val ≝ 51 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??). 52 50 53 definition reg_store ≝ 51 54 λreg,v,locals. 52 OK ? (add RegisterTag val locals reg v) 53 . 55 update RegisterTag val locals reg v. 54 56 55 57 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝ … … 57 59 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ] 58 60 | cons r rst ⇒ match vs with [ nil ⇒ Error ? | cons v vst ⇒ 59 do locals' ← reg_store r v locals;61 let locals' ≝ add RegisterTag val locals r v in 60 62 params_store rst vst locals' 61 63 ] ]. … … 182 184 match fd with 183 185 [ Internal fn ⇒ 184 ! locals ← params_store (f_params fn) params ( empty_map RegisterTag ?);186 ! locals ← params_store (f_params fn) params (init_locals (f_locals fn)); 185 187 let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in 186 188 ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉 -
src/common/Identifiers.ma
r757 r761 70 70 (match m with [ an_id_map m' ⇒ m' ]). 71 71 72 (* Always adds the identifier to the map. *) 72 73 definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝ 73 74 λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a 74 75 (match m with [ an_id_map m' ⇒ m' ])). 75 76 77 (* Only updates an existing entry; fails with an error otherwise. *) 78 definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝ 79 λtag,A,m,l,a. 80 match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a 81 (match m with [ an_id_map m' ⇒ m' ]) with 82 [ None ⇒ Error ? (* missing identifier *) 83 | Some m' ⇒ OK ? (an_id_map tag A m') 84 ]. 76 85 -
src/utilities/Coqlib.ma
r747 r761 599 599 (* * Mapping a function over an option type. *) 600 600 601 definition option_map ≝ λA,B.λf:A→B.λv:option A. 602 match v with [ Some v' ⇒ Some ? (f v') | None ⇒ None ? ]. 601 include "utilities/option.ma". 603 602 604 603 (*
Note: See TracChangeset
for help on using the changeset viewer.