Changeset 1052 for src/RTLabs
- Timestamp:
- Jul 4, 2011, 3:31:18 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLAbstoRTL.ma
r1050 r1052 102 102 〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉. 103 103 104 definition float_free_p ≝ 105 λsig. 106 match sig with 107 [ ASTfloat _ ⇒ False 108 | _ ⇒ True 109 ]. 110 104 111 definition size_of_sig_type ≝ 105 112 λsig. 106 match sig with 113 λprf: float_free_p sig. 114 match sig return λx. float_free_p x → nat with 107 115 [ ASTint isize sign ⇒ 108 let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in 109 Some ? (isize' ÷ (nat_of_bitvector ? int_size)) 110 | ASTfloat _ ⇒ None ? 111 | ASToffset ⇒ Some ? (nat_of_bitvector ? int_size) 112 | ASTptr rgn ⇒ Some ? (nat_of_bitvector ? ptr_size) 113 ]. 116 λast_int_prf. 117 let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in 118 isize' ÷ (nat_of_bitvector ? int_size) 119 | ASTfloat _ ⇒ 120 λast_float_prf. ? 121 | ASToffset ⇒ 122 λast_offset_prf. 123 nat_of_bitvector ? int_size 124 | ASTptr rgn ⇒ 125 λast_ptr_prf. 126 nat_of_bitvector ? ptr_size 127 ]. 128 normalize in ast_float_prf; 129 cases ast_float_prf; 130 qed. 114 131 115 132 inductive register_type: Type[0] ≝ … … 117 134 | register_ptr: register → register → register_type. 118 135 119 definition local_env ≝ map register (list register). 120 definition mem_local_env ≝ map_member register (list register) register_ord. 121 definition add_local_env ≝ map_insert register (list register) register_ord. 122 definition find_local_env ≝ map_lookup register (list register) register_ord. 136 definition local_env ≝ BitVectorTrie (list register). 137 138 definition mem_local_env ≝ 139 λr: register. 140 match r with 141 [ an_identifier w ⇒ member (list register) 16 w 142 ]. 143 144 definition add_local_env ≝ 145 λr: register. 146 match r with 147 [ an_identifier w ⇒ insert (list register) 16 w 148 ]. 149 150 definition find_local_env ≝ 151 λr: register. 152 λbvt. 153 match r with 154 [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ] 155 ]. 123 156 124 157 definition initialize_local_env_internal ≝ … … 131 164 | Some size ⇒ 132 165 let rs ≝ register_freshes runiverse size in 133 add_local_env r rs lenv166 Some ? (add_local_env r rs lenv) 134 167 ]. 135 168 … … 144 177 ] 145 178 in 146 foldl ? ? (initialize_local_env_internal runiverse) [ ] registers. 147 179 foldl ? ? ( 180 λbvt. λr. 181 match bvt with 182 [ None ⇒ None ? 183 | Some bvt' ⇒ initialize_local_env_internal runiverse bvt' r typ 184 ]) ? ?. 148 185 149 186 let initialize_local_env runiverse registers result = 150 187 let registers = 151 registers @ (match result with None -> [] | Some (r, t) ->[(r, t)]) in188 registers @ (match result with None → [ ] | Some (r, t) → [(r, t)]) in 152 189 let f lenv (r, t) = 153 190 let rs = register_freshes runiverse (size_of_sig_type t) in 154 191 add_local_env r rs lenv in 155 192 List.fold_left f Register.Map.empty registers 156 157 193 158 194 definition map_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.