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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLptr.ma
r2783 r2946 47 47 definition ERTLptr ≝ mk_graph_params (mk_uns_params ERTLptr_uns ERTLptr_functs). 48 48 definition ertlptr_program ≝ joint_program ERTLptr. 49 unification hint 0 ≔ ⊢ ertlptr_program ≡ joint_program ERTLptr. 49 50 50 51 definition ertlptr_seq_joint ≝ extension_seq ERTLptr. … … 52 53 on _s : ertlptr_seq to joint_seq ERTLptr ?. 53 54 55 definition ERTLptr_premain : ∀p : ertlptr_program.joint_closed_internal_function ERTLptr (prog_var_names ?? p) ≝ 56 λp. 57 let l1 : label ≝ an_identifier … one in 58 let l2 : label ≝ an_identifier … (p0 one) in 59 let l3 : label ≝ an_identifier … (p1 one) in 60 let res ≝ 61 mk_joint_internal_function ERTLptr (prog_var_names … p) 62 (mk_universe … (p0 (p0 one))) 63 (mk_universe … one) 64 it 4 0 0 (empty_map …) l1 in 65 (* todo: args for main? *) 66 let res ≝ add_graph … l1 67 (sequential … (COST_LABEL … (init_cost_label … p)) l2) 68 res in 69 let res ≝ add_graph … l2 70 (sequential … (CALL ERTLptr ? (inl … (prog_main … p)) 4 it) l3) 71 res in 72 let res ≝ add_graph … l3 73 (GOTO ? l3) 74 res in 75 res. 76 % 77 [ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct 78 % 79 [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct 80 2: % 81 4,6: % whd in ⊢ (??%%→?); #EQ destruct 82 ] 83  ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} 84  ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // 85  ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I 86  %{l2} %{(init_cost_label … p)} % 87 ] 88 qed.
Note: See TracChangeset
for help on using the changeset viewer.