Changeset 2681 for src/ERTLptr


Ignore:
Timestamp:
Feb 19, 2013, 6:48:32 PM (8 years ago)
Author:
tranquil
Message:
  • improvements to the graph translation function
  • fixed passes up to LTL
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2675 r2681  
    3939definition translate_step:
    4040 ∀globals.
    41  unit →
    4241 label
    4342  →joint_step ERTL globals
    4443   →bind_step_block ERTLptr globals ≝
    45  λglobals.λ_.λl.λs.
     44 λglobals.λl.λs.
    4645match s return λ_.bind_step_block ERTLptr globals with
    4746[ CALL called args dest ⇒
     
    6968definition translate_fin_step:
    7069 ∀globals.
    71  unit →
    7270 label
    7371  →joint_fin_step ERTL
    7472   →bind_fin_block ERTLptr globals ≝
    75  λglobals.λ_.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
     73 λglobals.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
     74
     75definition translate_data :
     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 …
     80    (* init_ret ≝ *) (joint_if_result … def)
     81    (* init_params ≝ *) (joint_if_params … def)
     82    (* init_stack_size ≝ *) (joint_if_stacksize … def)
     83    (* added_prologue ≝ *) [ ]
     84    (* f_step ≝ *) (translate_step globals)
     85    (* f_fin ≝ *) (translate_fin_step globals)
     86    ???).
     87@hide_prf
     88[ #l #c % ]
     89#l *
     90[ #l whd %{I} %{I} %1 %
     91| whd %{I I}
     92| #abs #called #args whd %{I I}
     93| * #called #args #dest whd in match translate_step; normalize nodelta whd
     94  [ %{I} %{I} #l %
     95  | #r whd %{I} %{(λ_.I)} % [| % [| % [| %{I} ]]] #l
     96    [1,3: %{I} %1 %
     97    |*: %
     98    ]
     99  ]
     100| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
     101| #s whd %{I} %{I} #l whd @(All_mp … (In ? (step_labels … s)))
     102  [ #l' #H %2{H} ] cases s -s //
     103]
     104qed.
    76105
    77106definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝
    78   b_graph_transform_program ERTL ERTLptr (λ_.unit)
    79   (λglobals,int_fun.
    80     〈〈joint_if_result … int_fun,
    81       joint_if_params … int_fun,
    82       joint_if_stacksize … int_fun〉,
    83     it〉)
    84   translate_step
    85   translate_fin_step.
     107  b_graph_transform_program ERTL ERTLptr translate_data.
Note: See TracChangeset for help on using the changeset viewer.