Changeset 736 for src/RTLabs/import.ma


Ignore:
Timestamp:
Apr 4, 2011, 5:13:08 PM (9 years ago)
Author:
campbell
Message:

Extra type safety for identifiers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/import.ma

    r727 r736  
    22include "RTLabs/RTLabs-sem.ma".
    33
    4 definition 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)
    7             (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    8 
    9 definition 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)
    12             (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    13 
    14 definition new_statement : internal_function → label → statement → internal_function ≝
    15 λf,l,s. mk_internal_function (f_labgen f) (f_reggen f) (f_sig f) (f_result f) (f_params f)
    16             (f_locals f) (f_stacksize f)
    17             (graph_add ? (f_graph f) l s) (f_entry f) (f_exit f).
    18 
    19 let rec n_labels (n:nat) (g:label_generation) : res (Vector label n × label_generation) ≝
     4let rec n_idents (n:nat) (tag:String) (g:Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝
    205match n with
    216[ 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''〉
    25 ].
    26 
    27 let rec n_regs (n:nat) (g:register_generation) : res (Vector label n × register_generation) ≝
    28 match n with
    29 [ O ⇒ OK ? 〈[[ ]], g〉
    30 | S m ⇒ do 〈ls, g'〉 ← n_regs m g;
    31         do 〈l, g''〉 ← register_new g';
     7| S m ⇒ do 〈ls, g'〉 ← n_idents m tag g;
     8        do 〈l, g''〉 ← fresh ? g';
    329        OK ? 〈l:::ls, g''〉
    3310].
     
    4118; pf_locals    : list pre_registers
    4219; pf_stacksize : nat
    43 ; pf_graph     : list (nat × ((nat → res label) → (nat → res register) → res statement))
     20; pf_graph     : list (nat × ((nat → res register) → (nat → res label) → res statement))
    4421; pf_entry     : nat
    4522; pf_exit      : nat
     
    5229
    5330definition make_registers :
    54   (nat → option register) → pre_registers → register_generation
    55   res ((nat → option register) × register_generation × registers) ≝
     31  (nat → option register) → pre_registers → Universe RegisterTag
     32  res ((nat → option register) × (Universe RegisterTag) × registers) ≝
    5633λm,rs0,g.
    5734match rs0 with [ dp n rs ⇒
     
    6138                  match m r with
    6239                  [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉
    63                   | None ⇒ do 〈r',g'〉 ← register_new g;
     40                  | None ⇒ do 〈r',g'〉 ← fresh ? g;
    6441                           OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉
    6542                  ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs;
     
    6946
    7047definition make_registers_list :
    71   (nat → option register) → list pre_registers → register_generation
    72   res ((nat → option register) × register_generation × (list registers)) ≝
     48  (nat → option register) → list pre_registers → Universe RegisterTag
     49  res ((nat → option register) × (Universe RegisterTag) × (list registers)) ≝
    7350λm,lrs,g.
    7451foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;
     
    7956definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
    8057λpre_f.
    81   let rgen0 ≝ register_gen_new in
     58  let rgen0 ≝ new_universe RegisterTag in
    8259  do 〈rmapgen1, result〉 ← make_registers (λ_.None ?) (pf_result pre_f) rgen0;
    8360  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
     
    8865  let rmap ≝ λn. opt_to_res … (rmap3 n) in
    8966  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    90   do 〈labels, gen〉 ← n_labels (S max_stmt) label_gen_new;
     67  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
    9168  let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in
    9269  do graph ← foldr ?? (λp,g0. do g ← g0;
     
    9471                              do l' ← get_label l;
    9572                              do s' ← s rmap get_label;
    96                               OK ? (graph_add ? g l' s')) (OK ? (empty_graph ?)) (pf_graph pre_f);
     73                              OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
    9774  do entry ← get_label (pf_entry pre_f);
    9875  do exit ← get_label (pf_exit pre_f);
Note: See TracChangeset for help on using the changeset viewer.