source: src/Clight/test/sum.test.ma

include "Clight/test/sum.c.ma".

example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
normalize  (* you can examine the result here *)
%
qed.

include "Clight/SimplifyCasts.ma".

example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
normalize  (* you can examine the result here *)
%
qed.

include "Clight/toCminor.ma".
include "Cminor/Cminor_semantics.ma".

example e1: finishes_with (repr I32 74) ?
  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
normalize
%
qed.

include "Cminor/toRTLabs.ma".
include "RTLabs/RTLabs_semantics.ma".
include "Clight/label.ma".

example e2: finishes_with (repr I32 74) ? (
let 〈p0,init〉 ≝ clight_label myprog in
bind ? (snapshot state) (clight_to_cminor (simplify_program p0))
(λp1. let p2 ≝ cminor_to_rtlabs p1 in
  exec_up_to RTLabs_fullexec p2 1000 [ ])).
normalize
%
qed.

include "RTLabs/CostCheck.ma".

definition readable_body ≝
λfn. insert_sort ?
       (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z]))
       (elements ?? (f_graph fn)).
(*
example c2: result ? (
  let 〈p0,init〉 ≝ clight_label myprog in
  ! p1 ← clight_to_cminor (simplify_program p0);
  let p2 ≝ cminor_to_rtlabs init p1 in
  match prog_funct … p2 with
  [ nil ⇒ Error ? (msg MISSING)
  | cons h _ ⇒
    match \snd h with
    [ External _ ⇒ Error ? (msg EXTERNAL)
    | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉
    ]
  ]).
normalize
*)
example c2: (
  let 〈p0,init〉 ≝ clight_label myprog in
  ! p1 ← clight_to_cminor (simplify_program p0);
  let p2 ≝ cminor_to_rtlabs p1 in
  return (check_cost_program p2)) = OK bool true.
normalize
%
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
*)