Changeset 2946 for src/ERTL/ERTL.ma
 Timestamp:
 Mar 24, 2013, 11:29:01 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTL.ma
r2783 r2946 68 68 definition ERTL ≝ mk_graph_params (mk_uns_params ERTL_uns ERTL_functs). 69 69 definition ertl_program ≝ joint_program ERTL. 70 unification hint 0 ≔ ⊢ ertl_program ≡ joint_program ERTL. 70 71 71 72 interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)). … … 123 124 coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint 124 125 on _s : ertl_seq to joint_seq ERTL ?. 126 127 definition ERTL_premain : ∀p : ertl_program.joint_closed_internal_function ERTL (prog_var_names ?? p) ≝ 128 λp. 129 let l1 : label ≝ an_identifier … one in 130 let l2 : label ≝ an_identifier … (p0 one) in 131 let l3 : label ≝ an_identifier … (p1 one) in 132 let res ≝ 133 mk_joint_internal_function ERTL (prog_var_names … p) 134 (mk_universe … (p0 (p0 one))) 135 (mk_universe … one) 136 it 4 0 0 (empty_map …) l1 in 137 (* todo: args for main? *) 138 let res ≝ add_graph … l1 139 (sequential … (COST_LABEL … (init_cost_label … p)) l2) 140 res in 141 let res ≝ add_graph … l2 142 (sequential … (CALL ERTL ? (inl … (prog_main … p)) 4 it) l3) 143 res in 144 let res ≝ add_graph … l3 145 (GOTO ? l3) 146 res in 147 res. 148 % 149 [ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct 150 % 151 [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct 152 2: % 153 4,6: % whd in ⊢ (??%%→?); #EQ destruct 154 ] 155  ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} 156  ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // 157  ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I 158  %{l2} %{(init_cost_label … p)} % 159 ] 160 qed.
Note: See TracChangeset
for help on using the changeset viewer.