Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/sum.test.ma

    r1332 r1599  
    3333@refl
    3434qed.
     35
     36include "RTLabs/RTLabsToRTL.ma".
     37include alias "basics/lists/list.ma".
     38
     39definition take_out: ∀A. res A → A ≝
     40 λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?].
     41cases daemon
     42qed.
     43
     44example CSC: True.
     45letin 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]
     53normalize 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  ]
     61normalize in xxx
     62
Note: See TracChangeset for help on using the changeset viewer.