Changeset 2162
 Timestamp:
 Jul 6, 2012, 5:53:01 PM (7 years ago)
 Location:
 src
 Files:

 3 added
 3 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL_paolo.ma
r2155 r2162 743 743 λr. tmpr ← tmpr .Or. r in 744 744 bret … 〈MOVE rtl_params globals 〈tmpr,srcr〉 :: 745 map ?? f srcrs', (COND ?tmpr lbl_true : joint_step ??) 〉745 map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉 746 746 ]. 747 747 … … 815 815 ❬(match retr with 816 816 [ Some retr ⇒ 817 CALL_ID rtl_params f (rtl_args args lenv ?) (find_local_env retr lenv ?)817 CALL_ID rtl_params ? f (rtl_args args lenv ?) (find_local_env retr lenv ?) 818 818  None ⇒ 819 CALL_ID rtl_params f (rtl_args args lenv ?) [ ]819 CALL_ID rtl_params ? f (rtl_args args lenv ?) [ ] 820 820 ] : bind_seq_block ???), lbl'❭ 821 821  St_call_ptr f args retr lbl' ⇒ 
src/joint/Joint_paolo.ma
r2155 r2162 78 78  LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals 79 79  STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals 80  extension_seq : ext_seq p → joint_seq p globals. 80  CALL_ID: ident → call_args p → call_dest p → joint_seq p globals 81  extension_seq : ext_seq p → joint_seq p globals 82  extension_call : ext_call p → joint_seq p globals. 81 83 82 84 axiom EmptyString : String. … … 96 98 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). 97 99 98 coercion extension_ to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝100 coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝ 99 101 extension_seq on _s : ext_seq ? to joint_seq ??. 100 101 inductive joint_call (p : step_params) : Type[0] ≝ 102  CALL_ID: ident → call_args p → call_dest p → joint_call p 103  extension_call : ext_call p → joint_call p. 104 105 coercion extension_to_call : ∀p.∀s : ext_call p.joint_call p ≝ 106 extension_call on _s : ext_call ? to joint_call ?. 102 coercion extension_call_to_seq : ∀p,globals.∀s : ext_call p.joint_seq p globals ≝ 103 extension_call on _s : ext_call ? to joint_seq ??. 107 104 108 inductive joint_branch (p : step_params) : Type[0] ≝105 (* inductive joint_branch (p : step_params) : Type[0] ≝ 109 106  COND: acc_a_reg p → label → joint_branch p 110 (* extension_branch : ext_branch p → joint_branch p*).107  extension_branch : ext_branch p → joint_branch p.*) 111 108 112 109 (*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝ … … 115 112 inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝ 116 113  step_seq : joint_seq p globals → joint_step p globals 117  step_call : joint_call p → joint_step p globals 118  step_branch : joint_branch p → joint_step p globals. 114  COND: acc_a_reg p → label → joint_step p globals. 119 115 120 116 coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝ 121 117 step_seq on _s : joint_seq ?? to joint_step ??. 122 coercion call_to_step : ∀p,globals.∀s : joint_call p.joint_step p globals ≝123 step_call on _s : joint_call ? to joint_step ??.124 coercion branch_to_step : ∀p,globals.∀s : joint_branch p.joint_step p globals ≝125 step_branch on _s : joint_branch ? to joint_step ??.126 118 127 119 definition step_flows ≝ λp,globals.λs : joint_step p globals. 128 120 match s with 129 [ step_seq _ ⇒ Labels … [ ] 130  step_call _ ⇒ Call 131  step_branch s ⇒ 121 [ step_seq s ⇒ 132 122 match s with 133 [ COND _ l ⇒ Labels … [l] 134 (* extension_branch s' ⇒ Labels … (ext_branch_labels … s')*) 123 [ CALL_ID _ _ _ ⇒ Call 124  extension_call _ ⇒ Call 125  _ ⇒ Labels … [ ] 135 126 ] 127  COND _ l ⇒ Labels … [l] 136 128 ]. 137 129 … … 151 143 joint_step p globals → status_class ≝ λp,g,s. 152 144 match s with 153 [ step_seq _ ⇒ cl_other 154  step_call _ ⇒ cl_call 155  step_branch _ ⇒ cl_jump 145 [ step_seq s ⇒ 146 match s with 147 [ CALL_ID _ _ _ ⇒ cl_call 148  extension_call _ ⇒ cl_call 149  _ ⇒ cl_other 150 ] 151  COND _ _ ⇒ cl_jump 156 152 ]. 157 153 
src/joint/TranslateUtils_paolo.ma
r2155 r2162 39 39 (globals: list ident) 40 40 (insts: list (joint_seq g_pars globals)) 41 (src : label) 42 (def: joint_internal_function … g_pars) on insts 43 : (joint_internal_function … g_pars) × label ≝ 41 (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝ 44 42 match insts with 45 [ nil ⇒ 〈def, src〉43 [ nil ⇒ return src 46 44  cons instr others ⇒ 47 let 〈def, mid〉 ≝ fresh_label … def in 48 let def ≝ add_graph … src (sequential … instr mid) def in 49 adds_graph_list g_pars globals others mid def 45 ! mid ← fresh_label … ; 46 ! def ← state_get … ; 47 !_ state_set … (add_graph … src (sequential … instr mid) def) ; 48 adds_graph_list g_pars globals others mid 50 49 ]. 51 50 … … 66 65 add_graph … mid (final … (\snd b)) def 67 66 ]. 67 68 (* preserves first statement if a cost label (should be an invariant) *) 69 definition insert_prologue ≝ 70 λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). 71 λdef : joint_internal_function globals g_pars. 72 let entry ≝ joint_if_entry … def in 73 match stmt_at … entry 74 return λx.match x with [None ⇒ false  Some _ ⇒ true] → ? 75 with 76 [ Some s ⇒ λ_. 77 match s with 78 [ sequential s' next ⇒ 79 match s' with 80 [ step_seq s'' ⇒ 81 match s'' with 82 [ COST_LABEL _ ⇒ 83 adds_graph ?? (inl … (s'' :: insts)) entry next def 84  _ ⇒ 85 let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in 86 add_graph … tmp s def' 87 ] 88  _ ⇒ 89 let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in 90 add_graph … tmp s def' 91 ] 92  _ ⇒ 93 let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in 94 add_graph … tmp s def' 95 ] 96  None ⇒ Ⓧ 97 ] (pi2 … entry). 98 99 definition insert_epilogue ≝ 100 λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). 101 λdef : joint_internal_function globals g_pars. 102 let exit ≝ joint_if_exit … def in 103 match stmt_at … exit 104 return λx.match x with [None ⇒ false  Some _ ⇒ true] → ? 105 with 106 [ Some s ⇒ λ_. 107 let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in 108 let def'' ≝ add_graph … tmp s def' in 109 set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp 110  None ⇒ Ⓧ 111 ] (pi2 … exit). 112 whd in match def''; >graph_code_has_point // 113 qed. 68 114 69 115 definition b_adds_graph :
Note: See TracChangeset
for help on using the changeset viewer.