Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (9 years ago)
Author:
tranquil
Message:
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils_paolo.ma

    r2182 r2214  
    55(* type T is the syntactic type of the generated things *)
    66(* (sig for RTLabs registers, unit in others ) *)
    7 definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).
     7definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g).
    88
    99definition rtl_ertl_fresh_reg:
     
    3939  (globals: list ident)
    4040  (insts: list (joint_seq g_pars globals))
    41   (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝
     41  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
    4242  match insts with
    4343  [ nil ⇒ return src
     
    4949  ].
    5050
     51definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     52  [ inl _ ⇒ true
     53  | inr _ ⇒ false
     54  ].
     55definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     56  [ inl _ ⇒ true
     57  | inr _ ⇒ false
     58  ].
     59
    5160definition adds_graph :
    5261  ∀g_pars : graph_params.
     
    5564       seq_block g_pars globals (joint_fin_step g_pars).
    5665  label → if is_inl … b then label else unit →
    57   joint_internal_function … g_pars → joint_internal_function … g_pars ≝
     66  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
    5867  λg_pars,globals,insts,src.
    5968  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     
    6978definition insert_prologue ≝
    7079  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
    71   λdef : joint_internal_function globals g_pars.
     80  λdef : joint_internal_function g_pars globals.
    7281  let entry ≝ joint_if_entry … def in
    7382  match stmt_at … entry
     
    99108definition insert_epilogue ≝
    100109  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
    101   λdef : joint_internal_function globals g_pars.
     110  λdef : joint_internal_function g_pars globals.
    102111  let exit ≝ joint_if_exit … def in
    103112  match stmt_at … exit
     
    121130       bind_seq_block g_pars globals (joint_fin_step g_pars).
    122131  label → if is_inl … b then label else unit →
    123   joint_internal_function globals g_pars
    124   joint_internal_function globals g_pars ≝
     132  joint_internal_function g_pars globals
     133  joint_internal_function g_pars globals ≝
    125134  λg_pars,globals,fresh_r,insts,src.
    126135  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     
    140149  freshT globals dst_g_pars (localsT dst_g_pars) →
    141150  (* initialized function definition with empty graph *)
    142   joint_internal_function globals dst_g_pars →
     151  joint_internal_function dst_g_pars globals →
    143152  (* functions dictating the translation *)
    144153  (label → joint_step src_g_pars globals →
     
    147156    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    148157  (* source function *)
    149   joint_internal_function globals src_g_pars →
     158  joint_internal_function src_g_pars globals →
    150159  (* destination function *)
    151   joint_internal_function globals dst_g_pars ≝
     160  joint_internal_function dst_g_pars globals ≝
    152161  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
    153162  let f : label → joint_statement (src_g_pars : params) globals →
    154     joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     163    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
    155164    λlbl,stmt,def.
    156165    match stmt with
     
    167176  ∀globals: list ident.
    168177  (* initialized function definition with empty graph *)
    169   joint_internal_function … dst_g_pars →
     178  joint_internal_function dst_g_pars globals →
    170179  (* functions dictating the translation *)
    171180  (label → joint_step src_g_pars globals →
     
    174183    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    175184  (* source function *)
    176   joint_internal_function … src_g_pars →
     185  joint_internal_function src_g_pars globals →
    177186  (* destination function *)
    178   joint_internal_function … dst_g_pars ≝
     187  joint_internal_function dst_g_pars globals ≝
    179188  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
    180189  let f : label → joint_statement (src_g_pars : params) globals →
    181     joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     190    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
    182191    λlbl,stmt,def.
    183192    match stmt with
Note: See TracChangeset for help on using the changeset viewer.