Changeset 2818
 Timestamp:
 Mar 7, 2013, 11:43:27 PM (7 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToERTLptr.ma
r2806 r2818 75 75 definition translate_data : 76 76 ∀globals.joint_closed_internal_function ERTL globals → 77 bind_new register (b_graph_translate_data ERTL ERTLptr globals)≝78 λglobals,def.bret … 79 (mk_b_graph_translate_data …77 bound_b_graph_translate_data ERTL ERTLptr globals ≝ 78 λglobals,def.bret …. 79 [try @(mk_b_graph_translate_data … 80 80 (* init_ret ≝ *) (joint_if_result … def) 81 81 (* init_params ≝ *) (joint_if_params … def) … … 85 85 (* f_step ≝ *) (translate_step globals) 86 86 (* f_fin ≝ *) (translate_fin_step globals) 87 ????). 88 @hide_prf 87 ????) 88  cases daemon ] 89 @hide_prf cases daemon (* 89 90 [ #l * [ #c'  * #f #args #dest  #a #ltrue  #s ] #c whd 90 91 [3: #r1 ] #l' #EQ destruct try % … … 108 109 [ #X #l1 #l2 #EQ destruct elim l2 [ % ] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #H %2{H} ] 109 110 #aux @aux cases s // 110 ] 111 ]*) 111 112 qed. 112 113 
src/ERTLptr/ERTLptrToLTL.ma
r2808 r2818 463 463 let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in 464 464 〈ltlprog, stack_cost … ltlprog, 2^16  first_free_stack_addr ltlprog〉. 465 cases daemon 466 qed.
Note: See TracChangeset
for help on using the changeset viewer.