Changeset 1467


Ignore:
Timestamp:
Oct 26, 2011, 5:25:15 PM (8 years ago)
Author:
mulligan
Message:

small change, adding entry and exit labels into the internal function, as these are necessary in graph based languages, unlike lin

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/ProofUtils.ma

    r1466 r1467  
    249249  let stacksize ≝ joint_if_stacksize … int_fun in
    250250  let code ≝ joint_if_code … int_fun in
    251   let entry ≝ ? in
    252   let exit ≝ ? in
    253   let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in
    254   let code ≝ relabel_graph params1 sem_params globals state code maps in
    255       mk_joint_internal_function …
    256         luniverse runiverse result params
    257         locals stacksize code entry exit.
     251  match joint_if_entry … int_fun with
     252  [ dp entry entry_prf ⇒
     253    match joint_if_exit … int_fun with
     254    [ dp exit exit_prf ⇒
     255      let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in
     256      let code ≝ relabel_graph params1 sem_params globals state code maps in
     257        mk_joint_internal_function …
     258          luniverse runiverse result params
     259          locals stacksize code entry exit
     260    ]
     261  ].
    258262  cases daemon (* XXX *)
    259263qed.
Note: See TracChangeset for help on using the changeset viewer.