Changeset 1599 for src/Clight/test/sum.test.ma
 Timestamp:
 Dec 13, 2011, 1:34:37 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/test/sum.test.ma
r1332 r1599 33 33 @refl 34 34 qed. 35 36 include "RTLabs/RTLabsToRTL.ma". 37 include alias "basics/lists/list.ma". 38 39 definition take_out: ∀A. res A → A ≝ 40 λA,a. match a with [ OK x ⇒ x  Error _ ⇒ ?]. 41 cases daemon 42 qed. 43 44 example CSC: True. 45 letin xxx ≝ 46 (let p ≝ take_out … (clight_to_cminor myprog) in 47 let p ≝ take_out … (cminor_to_rtlabs p) in 48 (* (map … (λx. match (\snd x) with [External _ ⇒ ?  Internal f ⇒ f_graph … f]) (prog_funct … p)) *) 49 let p ≝ rtlabs_to_rtl p in 50 (map … (λx. match (\snd x) with [External _ ⇒ ?  Internal f ⇒ joint_if_code … f]) (prog_funct … p)) 51 ) 52 [2: cases daemon] 53 normalize in xxx; 54 55 56 [2: 57 OK (list (codeT (prog_var_names … p) (rtl_params (prog_var_names … p)))) (list_map … (λx. match (\snd x) return λ_.codeT (prog_var_names … p) (rtl_params ?) with [External _ ⇒ ?  Internal f ⇒ ?(*joint_if_code ? (rtl_params ?) f*)]) (prog_funct … p))) 58 (* OK ? (map … (λx. match (\snd x) with [External _ ⇒ ?  Internal f ⇒ f_graph … f]) (prog_funct … p))) 59 *) 60 [2: check (joint_if_code (prog_var_names … p) ? f) 3: cases daemon ] 61 normalize in xxx 62
Note: See TracChangeset
for help on using the changeset viewer.