Ignore:
Timestamp:
Oct 30, 2012, 4:23:09 PM (8 years ago)
Author:
tranquil
Message:

adapted joint to cl_call f

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2286 r2422  
    652652  ∀p : unserialized_params.
    653653  ∀globals.
    654     joint_internal_function (mk_graph_params p) globals →
    655     joint_internal_function (mk_lin_params p) globals
     654    joint_closed_internal_function (mk_graph_params p) globals →
     655    joint_closed_internal_function (mk_lin_params p) globals
    656656     (* ∃sigma : identifier_map LabelTag ℕ.
    657657        let g ≝ joint_if_code ?? (pi1 … fin) in
     
    669669                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    670670                    (stmt_implicit_label … s)) (nth_opt … n c)*) ≝
    671   λp,globals,f_in.
    672   mk_joint_internal_function (mk_lin_params p) globals
     671  λp,globals,f_sig.let f_in ≝ pi1 … f_sig in
     672  «mk_joint_internal_function (mk_lin_params p) globals
    673673   (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in)
    674674   (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in)
    675675   (joint_if_stacksize ?? f_in)
    676    (linearise_code p globals (joint_if_code … f_in)
    677    (match daemon in False with [ ])
    678    (joint_if_entry … f_in))
    679    0 0 (* exit is dummy! *).
     676   (linearise_code p globals (joint_if_code … f_in) (pi2 … f_sig) (joint_if_entry … f_in))
     677   0 0 (* exit is dummy! *), ?».
    680678elim (linearise_code ?????) #c * #code_closed
     679[3: #_ assumption ]
    681680@hide_prf
    682681* #sigma * #O_in #sigma_prop
     
    688687]
    689688qed.
     689
     690definition linearise : ∀p : unserialized_params.
     691  program (joint_function (mk_graph_params p)) ℕ →
     692  program (joint_function (mk_lin_params p)) ℕ ≝
     693  λp,pr.transform_program ??? pr
     694    (λglobals.transf_fundef ?? (linearise_int_fun p globals)).
Note: See TracChangeset for help on using the changeset viewer.