Changeset 736


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

Extra type safety for identifiers.

Location:
src
Files:
1 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs-sem.ma

    r731 r736  
    5151λrs,v,locals. match rs with [ dp n regs ⇒
    5252  do vs ← break n v;
    53   OK ? (fold_right2_i ??? (λ_. register_update split_val) locals n regs vs)
     53  OK ? (fold_right2_i ??? (λ_.λr,v,lcls. add RegisterTag ? lcls r v) locals n regs vs)
    5454].
    5555
     
    6464definition reg_retrieve : register_env ? → registers → res val ≝
    6565λlocals,rs. match rs with [ dp n regs ⇒
    66   do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (register_lookup ? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;
     66  do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (lookup ?? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;
    6767  merge n vs
    6868].
     
    111111match st with
    112112[ State f fs m ⇒
    113   ! s ← graph_lookup ? (f_graph (func f)) (next f);
     113  ! s ← lookup ?? (f_graph (func f)) (next f);
    114114  match s with
    115115  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
     
    194194    match fd with
    195195    [ Internal fn ⇒
    196         ! locals ← params_store (f_params fn) params (register_empty ?);
     196        ! locals ← params_store (f_params fn) params (empty_map RegisterTag ?);
    197197        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    198198        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
  • src/RTLabs/RTLabs-syntax.ma

    r720 r736  
    5959
    6060record internal_function : Type[0] ≝
    61 { f_labgen    : label_generation
    62 ; f_reggen    : register_generation
     61{ f_labgen    : Universe LabelTag
     62; f_reggen    : Universe RegisterTag
    6363; f_sig       : signature
    6464; f_result    : registers
  • 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);
  • src/common/Graphs.ma

    r728 r736  
    22
    33include "ASM/BitVectorTrie.ma".
    4 include "Clight/AST.ma".
    5 include "common/Errors.ma".
     4include "common/Identifiers.ma".
    65
    7 definition label ≝ ident.
     6axiom LabelTag : String.
    87
    9 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq.
     8definition label ≝ Identifier LabelTag.
    109
    11 record label_generation : Type[0] ≝ { lab_next : label }.
     10definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
    1211
    13 definition label_gen_new : label_generation ≝ mk_label_generation (zero ?).
    1412
    15 definition label_new : label_generation → res (label × label_generation) ≝
    16 λg. let 〈gen, carries〉 ≝ add_with_carries ? (lab_next g) (zero ?) true in
    17     if get_index_v ?? carries 0 ? then Error ? else
    18       OK ? 〈lab_next g, mk_label_generation gen〉.
    19 // qed.
    20 
    21 definition graph : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
    22 definition empty_graph : ∀T. graph T ≝ λT. Stub T 16.
    23 definition graph_lookup : ∀T. graph T → label → option T ≝
    24 λT,g,l. lookup_opt T 16 l g.
    25 definition graph_add : ∀T. graph T → label → T → graph T ≝
    26 λT,g,l,v. insert T 16 l v g.
     13definition graph : Type[0] → Type[0] ≝ IdentifierMap LabelTag.
  • src/common/Registers.ma

    r726 r736  
    55
    66include "ASM/BitVectorTrie.ma".
    7 include "Clight/AST.ma".
    8 include "common/Errors.ma".
     7include "common/Identifiers.ma".
    98
    10 definition register ≝ ident.
     9axiom RegisterTag : String.
    1110
    12 definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq.
     11definition register ≝ Identifier RegisterTag.
    1312
    14 record register_generation : Type[0] ≝ { reg_next : register }.
     13definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
    1514
    16 definition register_gen_new : register_generation ≝ mk_register_generation (zero ?).
    17 
    18 definition register_new : register_generation → res (register × register_generation) ≝
    19 λg. let 〈gen, carries〉 ≝ add_with_carries ? (reg_next g) (zero ?) true in
    20     if get_index_v ?? carries 0 ? then Error ? else
    21       OK ? 〈reg_next g, mk_register_generation gen〉.
    22 // qed.
    23 
    24 definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
    25 definition register_empty : ∀T. register_env T ≝ λT. Stub T 16.
    26 definition register_lookup : ∀T. register_env T → register → option T ≝
    27 λT,g,l. lookup_opt T 16 l g.
    28 definition register_update : ∀T. register → T → register_env T → register_env T ≝
    29 λT,l,v,g. insert T 16 l v g.
     15definition register_env ≝ IdentifierMap RegisterTag.
Note: See TracChangeset for help on using the changeset viewer.