 Timestamp:
 Oct 25, 2011, 5:33:53 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/ProofUtils.ma
r1458 r1463 1 include "joint/Joint.ma". 2 include "LIN/LIN.ma". 3 4 let rec pre_erase_lin_internal_function' 5 (globals: list ident) (the_program: list (lin_statement globals)) 6 (labels: list label) 7 on the_program: ((BitVectorTrie Word 16) × (list (lin_statement globals))) ≝ 8 match the_program with 9 [ nil ⇒ 10 match labels with 11 [ nil ⇒ 〈Stub Word 16, [ ]〉 (* XXX: labels should be empty *) 12  _ ⇒ ⊥ 13 ] 14  cons hd tl ⇒ 15 let 〈lbl, instr〉 ≝ hd in 16 match lbl with 17 [ None ⇒ 18 let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in 19 match instr with 20 [ sequential seq l ⇒ 21 match seq with 22 [ COST_LABEL cost ⇒ 〈maps, instructions〉 23  _ ⇒ 〈maps, 〈None …, instr〉 :: instructions〉 24 ] 25  _ ⇒ 〈maps, 〈None …, instr〉 :: instructions〉 26 ] 27  Some lbl ⇒ 28 let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in 29 match instr with 30 [ sequential seq l ⇒ 31 match seq with 32 [ COST_LABEL cost ⇒ pre_erase_lin_internal_function' globals tl (lbl :: labels) 33  _ ⇒ 34 let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in 35 let maps ≝ foldr ? ? (λl. λmap. 36 match l with 37 [ an_identifier l ⇒ insert … l lbl' map 38 ]) maps (lbl :: labels) 39 in 40 〈maps, instructions〉 41 ] 42  _ ⇒ 43 let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in 44 let maps ≝ foldr ? ? (λl. λmap. 45 match l with 46 [ an_identifier l ⇒ insert … l lbl' map 47 ]) maps (lbl :: labels) 48 in 49 〈maps, instructions〉 50 ] 51 ] 52 ]. 53 @daemon 54 qed. 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. 59 λmap. 60 λinstr. 61 match instr with 62 [ COND acc_a lbl ⇒ 63 let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in 64 let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in 65 COND lin_params_ globals acc_a located 66  _ ⇒ instr 67 ]. 68 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 λmap: BitVectorTrie Word 16. 73 λstmt: pre_lin_statement globals. 74 match stmt with 75 [ sequential seq l ⇒ 76 let relabelled ≝ relabel_lin_instruction globals map seq in 77 sequential lin_params_ globals relabelled it 78  RETURN ⇒ RETURN lin_params_ globals 79  GOTO l ⇒ 80 let l ≝ match l with [ an_identifier l ⇒ l ] in 81 let located ≝ an_identifier LabelTag (lookup … l map l) in 82 GOTO lin_params_ globals located 83 ]. 84 85 let rec relabel 86 (globals: list ident) (map: BitVectorTrie Word 16) 87 (program: list (lin_statement globals)) 88 on program: list (lin_statement globals) ≝ 89 match program with 90 [ nil ⇒ [ ] 91  cons hd tl ⇒ 92 let 〈label, stmt〉 ≝ hd in 93 let relabelled ≝ relabel_lin_statement globals map stmt in 94 let label ≝ 95 match label with 96 [ None ⇒ None … 97  Some label ⇒ 98 let label ≝ match label with [ an_identifier l ⇒ l ] in 99 Some … (an_identifier LabelTag (lookup … label map label)) 100 ] 101 in 102 〈label, relabelled〉 :: relabel globals map tl 103 ]. 104 105 definition pre_erase_lin_internal_function: 106 ∀globals: list ident. joint_internal_function globals (lin_params globals) → joint_internal_function globals (lin_params globals) ≝ 107 λglobals. 108 λfunction. 109 let luniverse ≝ joint_if_luniverse … function in 110 let runiverse ≝ joint_if_runiverse … function in 111 let result ≝ joint_if_result … function in 112 let params ≝ joint_if_params … function in 113 let locals ≝ joint_if_locals … function in 114 let stacksize ≝ joint_if_stacksize … function in 115 let code ≝ joint_if_code … function in 116 let entry ≝ ? in 117 let exit ≝ ? in 118 let 〈maps, code〉 ≝ pre_erase_lin_internal_function' globals code [ ] in 119 let code ≝ relabel globals maps code in 120 mk_joint_internal_function … 121 luniverse runiverse result params 122 locals stacksize code entry exit. 123 cases daemon (* XXX *) 124 qed. 125 126 definition erase_lin_program: lin_program → lin_program ≝ 127 λprogram. 128 transform_program … program (transf_fundef … (pre_erase_lin_internal_function …)).
Note: See TracChangeset
for help on using the changeset viewer.