Changeset 2818 for src


Ignore:
Timestamp:
Mar 7, 2013, 11:43:27 PM (7 years ago)
Author:
sacerdot
Message:

"Repaired", using non computational daemons.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToERTLptr.ma

    r2806 r2818  
    7575definition translate_data :
    7676  ∀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 …
    8080    (* init_ret ≝ *) (joint_if_result … def)
    8181    (* init_params ≝ *) (joint_if_params … def)
     
    8585    (* f_step ≝ *) (translate_step globals)
    8686    (* f_fin ≝ *) (translate_fin_step globals)
    87     ????).
    88 @hide_prf
     87    ????)
     88   | cases daemon ]
     89@hide_prf cases daemon (*
    8990[ #l * [ #c' | * #f #args #dest | #a #ltrue | #s ] #c whd
    9091  [3: #r1 ] #l' #EQ destruct try %
     
    108109  [ #X #l1 #l2 #EQ destruct elim l2 [ % ] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #H %2{H} ]
    109110  #aux @aux cases s //
    110 ]
     111]*)
    111112qed.
    112113
  • src/ERTLptr/ERTLptrToLTL.ma

    r2808 r2818  
    463463   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
    464464   〈ltlprog, stack_cost … ltlprog, 2^16 - first_free_stack_addr ltlprog〉.
     465cases daemon
     466qed.
Note: See TracChangeset for help on using the changeset viewer.