 Timestamp:
 Oct 26, 2011, 5:08:59 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/ProofUtils.ma
r1463 r1466 54 54 qed. 55 55 56 definition relabel_lin_instruction: 57 ∀globals: list ident. BitVectorTrie Word 16 → joint_instruction lin_params_ globals → joint_instruction lin_params_ globals ≝ 58 λglobals: list ident. 56 definition relabel_joint_instruction: 57 ∀globals: list ident. 58 ∀params: params_. 59 BitVectorTrie Word 16 → joint_instruction params globals → joint_instruction params globals ≝ 60 λglobals: list ident. 61 λparams. 59 62 λmap. 60 63 λinstr. … … 63 66 let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in 64 67 let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in 65 COND lin_params_globals acc_a located68 COND params globals acc_a located 66 69  _ ⇒ instr 67 70 ]. 68 71 69 definition relabel_lin_statement: 70 ∀globals: list ident. BitVectorTrie Word 16 → pre_lin_statement globals → pre_lin_statement globals ≝ 71 λglobals: list ident. 72 definition relabel_joint_statement: 73 ∀globals: list ident. 74 ∀params: params_. 75 BitVectorTrie Word 16 → joint_statement params globals → joint_statement params globals ≝ 76 λglobals: list ident. 77 λparams: params_. 72 78 λmap: BitVectorTrie Word 16. 73 λstmt: pre_lin_statementglobals.79 λstmt: joint_statement params globals. 74 80 match stmt with 75 81 [ sequential seq l ⇒ 76 let relabelled ≝ relabel_ lin_instruction globals map seq in77 sequential lin_params_ globals relabelled it78  RETURN ⇒ RETURN lin_params_globals82 let relabelled ≝ relabel_joint_instruction globals params map seq in 83 sequential params globals relabelled l 84  RETURN ⇒ RETURN params globals 79 85  GOTO l ⇒ 80 86 let l ≝ match l with [ an_identifier l ⇒ l ] in 81 87 let located ≝ an_identifier LabelTag (lookup … l map l) in 82 GOTO lin_params_globals located88 GOTO params globals located 83 89 ]. 84 90 … … 91 97  cons hd tl ⇒ 92 98 let 〈label, stmt〉 ≝ hd in 93 let relabelled ≝ relabel_ lin_statement globalsmap stmt in99 let relabelled ≝ relabel_joint_statement globals lin_params_ map stmt in 94 100 let label ≝ 95 101 match label with … … 127 133 λprogram. 128 134 transform_program … program (transf_fundef … (pre_erase_lin_internal_function …)). 135 136 include "joint/SemanticUtils.ma". 137 138 definition empty_graph ≝ 139 λa: Type[0]. 140 an_id_map LabelTag a (Stub a 16). 141 142 let rec pre_erase_graph_internal_function' 143 (params1: params1) (sem_params: sem_params) (globals: list ident) 144 (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals)) 145 (labels: list label) (num_nodes: nat) 146 on num_nodes: ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) ≝ 147 match num_nodes return λn. ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) with 148 [ O ⇒ 149 match labels with 150 [ nil ⇒ 〈Stub Word 16, empty_graph …〉 151  _ ⇒ ⊥ 152 ] 153  S num_nodes ⇒ 154 let program_counter ≝ (pc … state) in 155 match code_pointer_of_address program_counter with 156 [ OK code_pointer ⇒ 157 match graph_label_of_pointer code_pointer with 158 [ OK lbl ⇒ 159 match lookup … the_graph lbl with 160 [ Some statement ⇒ 161 let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in 162 let state ≝ set_pc … program_counter state in 163 match statement with 164 [ sequential seq l ⇒ 165 match seq with 166 [ COST_LABEL cost_label ⇒ pre_erase_graph_internal_function' params1 sem_params globals state the_graph (lbl :: labels) num_nodes 167  _ ⇒ 168 let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in 169 let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in 170 〈maps, instructions〉 171 ] 172  _ ⇒ 173 let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in 174 let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in 175 〈maps, instructions〉 176 ] 177  None ⇒ ⊥ (* XXX: shouldn't happen *) 178 ] 179  Error message ⇒ ⊥ (* XXX: shouldn't happen *) 180 ] 181  Error message ⇒ ⊥ (* XXX: shouldn't happen *) 182 ] 183 ]. 184 cases daemon (* XXX *) 185 qed. 186 187 definition pre_erase_graph_internal_function ≝ 188 λparams1: params1. 189 λsem_params: sem_params. 190 λglobals: list ident. 191 λstate: state sem_params. 192 λthe_graph: codeT globals (graph_params params1 globals). 193 λlabels: list label. 194 pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels (graph_num_nodes … the_graph). 195 196 let rec relabel_graph' 197 (params1: params1) (sem_params: sem_params) (globals: list ident) 198 (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals)) 199 (map: BitVectorTrie Word 16) (num_nodes: nat) 200 on num_nodes: codeT globals (graph_params params1 globals) ≝ 201 match num_nodes with 202 [ O ⇒ empty_graph … 203  S num_nodes ⇒ 204 let program_counter ≝ (pc … state) in 205 match code_pointer_of_address program_counter with 206 [ OK code_pointer ⇒ 207 match graph_label_of_pointer code_pointer with 208 [ OK lbl ⇒ 209 match lookup … the_graph lbl with 210 [ Some statement ⇒ 211 let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in 212 let new_statement ≝ relabel_joint_statement globals (graph_params params1 globals) map statement in 213 let new_lbl ≝ an_identifier LabelTag ? in 214 let state' ≝ set_pc … program_counter state in 215 let tail_graph ≝ relabel_graph' params1 sem_params globals state' the_graph map num_nodes in 216 add … tail_graph new_lbl new_statement 217  None ⇒ ⊥ 218 ] 219  Error message ⇒ ⊥ 220 ] 221  Error message ⇒ ⊥ 222 ] 223 ]. 224 [2: @(lookup … lbl' map lbl') 225 *: cases daemon (* XXX *) 226 ] 227 qed. 228 229 definition relabel_graph ≝ 230 λparams1. 231 λsem_params. 232 λglobals. 233 λstate: state sem_params. 234 λthe_graph: codeT globals (graph_params params1 globals). 235 λmap: BitVectorTrie Word 16. 236 relabel_graph' params1 sem_params globals state the_graph map (graph_num_nodes … the_graph). 237 238 definition pre_erase_graph_joint_internal_function ≝ 239 λparams1: params1. 240 λsem_params: sem_params. 241 λglobals: list ident. 242 λstate: state sem_params. 243 λint_fun: joint_internal_function globals (graph_params params1 globals). 244 let luniverse ≝ joint_if_luniverse globals (graph_params params1 globals) int_fun in 245 let runiverse ≝ joint_if_runiverse … int_fun in 246 let result ≝ joint_if_result … int_fun in 247 let params ≝ joint_if_params … int_fun in 248 let locals ≝ joint_if_locals … int_fun in 249 let stacksize ≝ joint_if_stacksize … int_fun in 250 let code ≝ joint_if_code … int_fun in 251 let entry ≝ ? in 252 let exit ≝ ? in 253 let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in 254 let code ≝ relabel_graph params1 sem_params globals state code maps in 255 mk_joint_internal_function … 256 luniverse runiverse result params 257 locals stacksize code entry exit. 258 cases daemon (* XXX *) 259 qed. 260 261 (* XXX: use make_initial_state to build an initial state for a program *)
Note: See TracChangeset
for help on using the changeset viewer.