Changeset 1599 for src/Clight/test

Timestamp:

Dec 13, 2011, 1:34:37 AM (9 years ago)

Author:

sacerdot

Message:

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

Location:

src/Clight/test

Files:

• search.c.ma (modified) (1 diff)
• sum.test.ma (modified) (1 diff)

src/Clight/test/search.c.ma

@@ -215 +215 @@
 @refl
 qed.
+
+example csc: True.
+letin yyy ≝ (
+let xxx ≝ (clight_to_cminor myprog) in
+do p ← xxx ; cminor_to_rtlabs p)
+normalize in yyy;
+include "RTLabs/RTLabsToRTL.ma".
+
+example csc: True.
+letin xxx ≝ (clight_to_cminor myprog)
+letin yyy ≝ (do p ← xxx ; cminor_to_rtlabs p)
+letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p)
+@⊥ normalize in xxx;

src/Clight/test/sum.test.ma

@@ -33 +33 @@
 @refl
 qed.
+
+include "RTLabs/RTLabsToRTL.ma".
+include alias "basics/lists/list.ma".
+
+definition take_out: ∀A. res A → A ≝
+ λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?].
+cases daemon
+qed.
+
+example CSC: True.
+letin xxx ≝
+ (let p ≝ take_out … (clight_to_cminor myprog) in
+  let p ≝ take_out … (cminor_to_rtlabs p) in
+(*   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)) *)
+  let p ≝ rtlabs_to_rtl p in
+   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ joint_if_code … f]) (prog_funct … p))
+ )
+[2: cases daemon]
+normalize in xxx;
+
+
+[2:
+  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)))
+(*  OK ? (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)))
+*)
+[2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon  ]
+normalize in xxx
+