Ignore:
Timestamp:
Jul 19, 2012, 6:13:54 PM (9 years ago)
Author:
tranquil
Message:
  • collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
  • completed update of RTL, LTL and LIN semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils_paolo.ma

    r2214 r2217  
    11include "joint/Joint_paolo.ma".
    22include "joint/blocks.ma".
     3include "utilities/hide.ma".
    34
    45(* general type of functions generating fresh things *)
    5 (* type T is the syntactic type of the generated things *)
    6 (* (sig for RTLabs registers, unit in others ) *)
    7 definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g).
    8 
    9 definition rtl_ertl_fresh_reg:
    10  ∀inst_pars,funct_pars,globals.
    11   freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝
    12   λinst_pars,var_pars,globals,def.
    13     let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    14     〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
     6definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).
    157
    168include alias "basics/lists/list.ma".
    17 let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
    18   freshT globals (rtl_ertl_params inst_pars funct_pars)
    19     (Σl : list register. |l| = n) ≝
    20   let ret_type ≝ (Σl : list register. |l| = n) in
    21   match n  return λx.x = n → freshT … ret_type with
    22   [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
    23   | S n' ⇒ λeq'.
    24     ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
    25     ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
    26     return (mk_Sig … (reg :: regs') ?)
    27   ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
    28   qed.
     9let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
     10  on n :
     11  freshT pars globals (Σl : list A. |l| = n) ≝
     12  match n  return λx.freshT … (Σl.|l| = x) with
     13  [ O ⇒ return «[ ], ?»
     14  | S n' ⇒
     15    ! regs' ← repeat_fresh … fresh n';
     16    ! reg ← fresh ;
     17    return «reg::regs',?»
     18  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.
    2919
    3020definition fresh_label:
     
    126116  ∀globals: list ident.
    127117  (* fresh register creation *)
    128   freshT globals g_pars (localsT … g_pars) →
     118  freshT g_pars globals (localsT … g_pars) →
    129119  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
    130120       bind_seq_block g_pars globals (joint_fin_step g_pars).
     
    147137  ∀globals: list ident.
    148138  (* fresh register creation *)
    149   freshT globals dst_g_pars (localsT dst_g_pars) →
     139  freshT dst_g_pars globals (localsT dst_g_pars) →
    150140  (* initialized function definition with empty graph *)
    151141  joint_internal_function dst_g_pars globals →
Note: See TracChangeset for help on using the changeset viewer.