Ignore:
Timestamp:
Sep 26, 2012, 6:14:38 PM (7 years ago)
Author:
campbell
Message:

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

File:
1 edited

Legend:

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

    r2253 r2353  
    2525include "Cminor/toRTLabs.ma".
    2626include "RTLabs/semantics.ma".
     27include "Clight/label.ma".
    2728
    2829example e2: finishes_with (repr I32 74) ? (
    29 bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
    30 (λp1. let p2 ≝ cminor_to_rtlabs p1 in
     30let 〈p0,init〉 ≝ clight_label myprog in
     31bind ? (snapshot state) (clight_to_cminor (simplify_program p0))
     32(λp1. let p2 ≝ cminor_to_rtlabs init p1 in
    3133  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    3234normalize
    3335%
    3436qed.
     37
     38include "RTLabs/CostCheck.ma".
     39
     40axiom MISSING:String.
     41axiom EXTERNAL:String.
     42
     43definition readable_body ≝
     44λfn. insert_sort ?
     45       (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z]))
     46       (elements ?? (f_graph fn)).
     47(*
     48example c2: result ? (
     49  let 〈p0,init〉 ≝ clight_label myprog in
     50  ! p1 ← clight_to_cminor (simplify_program p0);
     51  let p2 ≝ cminor_to_rtlabs init p1 in
     52  match prog_funct … p2 with
     53  [ nil ⇒ Error ? (msg MISSING)
     54  | cons h _ ⇒
     55    match \snd h with
     56    [ External _ ⇒ Error ? (msg EXTERNAL)
     57    | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉
     58    ]
     59  ]).
     60normalize
     61*)
     62example c2: (
     63  let 〈p0,init〉 ≝ clight_label myprog in
     64  ! p1 ← clight_to_cminor (simplify_program p0);
     65  let p2 ≝ cminor_to_rtlabs init p1 in
     66  return (check_cost_program p2)) = OK bool true.
     67normalize
     68%
     69qed.
     70
     71
     72
    3573(*
    3674include "RTLabs/RTLabsToRTL.ma".
Note: See TracChangeset for help on using the changeset viewer.