Changeset 3022 for src/compiler.ma


Ignore:
Timestamp:
Mar 28, 2013, 7:49:22 PM (7 years ago)
Author:
campbell
Message:

Make a couple of tests monadic for easier inversion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r3021 r3022  
    6969  let p ≝ cminor_to_rtlabs p in
    7070  let i ≝ observe rtlabs_pass p in
    71   if check_cost_program p then
    72     if check_program_cost_injectivity p then
    73       (return 〈init_cost,p',p〉)
    74     else
    75       (Error ? (msg RepeatedCostLabel))
    76   else
    77     (Error ? (msg BadCostLabelling)).
     71  ! WCL ← check_cost_program_prf p;
     72  ! INJ ← check_program_cost_injectivity_prf p;
     73  return 〈init_cost,p',p〉.
    7874
    7975(* The compiler back-end *)
Note: See TracChangeset for help on using the changeset viewer.