Changeset 1220 for src/joint/Joint.ma


Ignore:
Timestamp:
Sep 15, 2011, 6:05:31 PM (9 years ago)
Author:
sacerdot
Message:

ERTL ported to the new joint syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1182 r1220  
    6363}.
    6464
     65definition set_luniverse ≝
     66  λglobals  : list ident.
     67  λpre.
     68  λp: sem_params_ pre globals.
     69  λint_fun  : joint_internal_function globals … p.
     70  λluniverse: universe LabelTag.
     71  let runiverse ≝ joint_if_runiverse … int_fun in
     72  let params    ≝ joint_if_params … int_fun in
     73  let locals    ≝ joint_if_locals … int_fun in
     74  let result    ≝ joint_if_result … int_fun in
     75  let stacksize ≝ joint_if_stacksize … int_fun in
     76  let graph     ≝ joint_if_graph … int_fun in
     77  let entry     ≝ joint_if_entry … int_fun in
     78  let exit      ≝ joint_if_exit … int_fun in
     79    mk_joint_internal_function globals ? p
     80      luniverse runiverse result params locals
     81      stacksize graph entry exit.
     82
    6583definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
    6684
    67 record joint_program (globals: list ident) (pre) (p:sem_params_ pre globals) : Type[0] ≝
    68 {
    69   joint_pr_vars: list (ident × nat);
    70   joint_pr_functs: list (ident × (joint_function … p));
    71   joint_pr_main: option ident
    72 }.
     85definition joint_program :=
     86 λglobals:list ident.λpre.λp: sem_params_ pre globals.
     87  program (joint_function … p) nat.
    7388
    7489(****************************************************************************)
Note: See TracChangeset for help on using the changeset viewer.