Changeset 2217 for src/joint/TranslateUtils_paolo.ma
 Timestamp:
 Jul 19, 2012, 6:13:54 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils_paolo.ma
r2214 r2217 1 1 include "joint/Joint_paolo.ma". 2 2 include "joint/blocks.ma". 3 include "utilities/hide.ma". 3 4 4 5 (* 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〉. 6 definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g). 15 7 16 8 include 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. 9 let 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. 29 19 30 20 definition fresh_label: … … 126 116 ∀globals: list ident. 127 117 (* fresh register creation *) 128 freshT g lobals g_pars (localsT … g_pars) →118 freshT g_pars globals (localsT … g_pars) → 129 119 ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) + 130 120 bind_seq_block g_pars globals (joint_fin_step g_pars). … … 147 137 ∀globals: list ident. 148 138 (* fresh register creation *) 149 freshT globals dst_g_pars (localsT dst_g_pars) →139 freshT dst_g_pars globals (localsT dst_g_pars) → 150 140 (* initialized function definition with empty graph *) 151 141 joint_internal_function dst_g_pars globals →
Note: See TracChangeset
for help on using the changeset viewer.