Changeset 726 for src/RTLabs


Ignore:
Timestamp:
Mar 30, 2011, 6:47:35 PM (9 years ago)
Author:
campbell
Message:

Change identifiers to Words in Clight and RTLabs semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/import.ma

    r710 r726  
    22include "RTLabs/RTLabs-sem.ma".
    33
    4 definition new_reg : internal_function → register × internal_function
    5 λf. let 〈r, g〉 ≝ register_new (f_reggen f) in
    6     〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f)
     4definition new_reg : internal_function → res (register × internal_function)
     5λf. do 〈r, g〉 ← register_new (f_reggen f);
     6    OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f)
    77            (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    88
    9 definition new_label : internal_function → label × internal_function
    10 λf. let 〈l, g〉 ≝ label_new (f_labgen f) in
    11     〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f)
     9definition new_label : internal_function → res (label × internal_function)
     10λf. do 〈l, g〉 ← label_new (f_labgen f);
     11    OK ? 〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f)
    1212            (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    1313
     
    1717            (graph_add ? (f_graph f) l s) (f_entry f) (f_exit f).
    1818
    19 let rec n_labels (n:nat) (g:label_generation) : Vector label n × label_generation
     19let rec n_labels (n:nat) (g:label_generation) : res (Vector label n × label_generation)
    2020match n with
    21 [ O ⇒ 〈[[ ]], g〉
    22 | S m ⇒ let 〈ls, g'〉 ≝ n_labels m g in
    23         let 〈l, g''〉 ≝ label_new g in
    24         〈l:::ls, g''〉
     21[ O ⇒ OK ? 〈[[ ]], g〉
     22| S m ⇒ do 〈ls, g'〉 ← n_labels m g;
     23        do 〈l, g''〉 ← label_new g;
     24        OK ? 〈l:::ls, g''〉
    2525].
    2626
    27 let rec n_regs (n:nat) (g:register_generation) : Vector label n × register_generation
     27let rec n_regs (n:nat) (g:register_generation) : res (Vector label n × register_generation)
    2828match n with
    29 [ O ⇒ 〈[[ ]], g〉
    30 | S m ⇒ let 〈ls, g'〉 ≝ n_regs m g in
    31         let 〈l, g''〉 ≝ register_new g in
    32         〈l:::ls, g''〉
     29[ O ⇒ OK ? 〈[[ ]], g〉
     30| S m ⇒ do 〈ls, g'〉 ← n_regs m g;
     31        do 〈l, g''〉 ← register_new g;
     32        OK ? 〈l:::ls, g''〉
    3333].
    3434
     
    6161                  match m r with
    6262                  [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉
    63                   | None ⇒ let 〈r',g'〉 ≝ register_new g in
     63                  | None ⇒ do 〈r',g'〉 ← register_new g;
    6464                           OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉
    6565                  ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs;
     
    8888  let rmap ≝ λn. opt_to_res … (rmap3 n) in
    8989  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    90   let 〈labels, gen〉 ≝ n_labels max_stmt label_gen_new in
     90  do 〈labels, gen〉 ← n_labels max_stmt label_gen_new;
    9191  let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in
    9292  do graph ← foldr ?? (λp,g0. do g ← g0;
Note: See TracChangeset for help on using the changeset viewer.