Changeset 736

Timestamp:

Apr 4, 2011, 5:13:08 PM (9 years ago)

Author:

campbell

Message:

Extra type safety for identifiers.

Location:

src

Files:

• RTLabs/RTLabs-sem.ma (modified) (4 diffs)
• RTLabs/RTLabs-syntax.ma (modified) (1 diff)
• RTLabs/import.ma (modified) (8 diffs)
• common/Graphs.ma (modified) (1 diff)
• common/Identifiers.ma (added)
• common/Registers.ma (modified) (1 diff)

src/RTLabs/RTLabs-sem.ma

@@ -51 +51 @@
 λrs,v,locals. match rs with [ dp n regs ⇒
   do vs ← break n v;
-  OK ? (fold_right2_i ??? (λ_. register_update split_val) locals n regs vs)
+  OK ? (fold_right2_i ??? (λ_.λr,v,lcls. add RegisterTag ? lcls r v) locals n regs vs)
 ].
 
@@ -64 +64 @@
 definition reg_retrieve : register_env ? → registers → res val ≝
 λlocals,rs. match rs with [ dp n regs ⇒
-  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;
+  do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (lookup ?? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;
   merge n vs
 ].
@@ -111 +111 @@
 match st with
 [ State f fs m ⇒
-  ! s ← graph_lookup ? (f_graph (func f)) (next f);
+  ! s ← lookup ?? (f_graph (func f)) (next f);
   match s with
   [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
@@ -194 +194 @@
     match fd with
     [ Internal fn ⇒
-        ! locals ← params_store (f_params fn) params (register_empty ?);
+        ! locals ← params_store (f_params fn) params (empty_map RegisterTag ?);
         let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
         ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉

src/RTLabs/RTLabs-syntax.ma

@@ -59 +59 @@
 
 record internal_function : Type[0] ≝
-{ f_labgen    : label_generation
-; f_reggen    : register_generation
+{ f_labgen    : Universe LabelTag
+; f_reggen    : Universe RegisterTag
 ; f_sig       : signature
 ; f_result    : registers

src/RTLabs/import.ma

@@ -2 +2 @@
 include "RTLabs/RTLabs-sem.ma".
 
-definition new_reg : internal_function → res (register × internal_function) ≝
-λf. do 〈r, g〉 ← register_new (f_reggen f);
-    OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f)
-            (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
-
-definition new_label : internal_function → res (label × internal_function) ≝
-λf. do 〈l, g〉 ← label_new (f_labgen f);
-    OK ? 〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f)
-            (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
-
-definition new_statement : internal_function → label → statement → internal_function ≝
-λf,l,s. mk_internal_function (f_labgen f) (f_reggen f) (f_sig f) (f_result f) (f_params f)
-            (f_locals f) (f_stacksize f)
-            (graph_add ? (f_graph f) l s) (f_entry f) (f_exit f).
-
-let rec n_labels (n:nat) (g:label_generation) : res (Vector label n × label_generation) ≝
+let rec n_idents (n:nat) (tag:String) (g:Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝
 match n with
 [ O ⇒ OK ? 〈[[ ]], g〉
-| S m ⇒ do 〈ls, g'〉 ← n_labels m g;
-        do 〈l, g''〉 ← label_new g';
-        OK ? 〈l:::ls, g''〉
-].
-
-let rec n_regs (n:nat) (g:register_generation) : res (Vector label n × register_generation) ≝
-match n with
-[ O ⇒ OK ? 〈[[ ]], g〉
-| S m ⇒ do 〈ls, g'〉 ← n_regs m g;
-        do 〈l, g''〉 ← register_new g';
+| S m ⇒ do 〈ls, g'〉 ← n_idents m tag g;
+        do 〈l, g''〉 ← fresh ? g';
         OK ? 〈l:::ls, g''〉
 ].
@@ -41 +18 @@
 ; pf_locals    : list pre_registers
 ; pf_stacksize : nat
-; pf_graph     : list (nat × ((nat → res label) → (nat → res register) → res statement))
+; pf_graph     : list (nat × ((nat → res register) → (nat → res label) → res statement))
 ; pf_entry     : nat
 ; pf_exit      : nat
@@ -52 +29 @@
 
 definition make_registers : 
-  (nat → option register) → pre_registers → register_generation →
-  res ((nat → option register) × register_generation × registers) ≝
+  (nat → option register) → pre_registers → Universe RegisterTag →
+  res ((nat → option register) × (Universe RegisterTag) × registers) ≝
 λm,rs0,g.
 match rs0 with [ dp n rs ⇒
@@ -61 +38 @@
                   match m r with
                   [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉
-                  | None ⇒ do 〈r',g'〉 ← register_new g;
+                  | None ⇒ do 〈r',g'〉 ← fresh ? g;
                            OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉
                   ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs;
@@ -69 +46 @@
 
 definition make_registers_list :
-  (nat → option register) → list pre_registers → register_generation →
-  res ((nat → option register) × register_generation × (list registers)) ≝
+  (nat → option register) → list pre_registers → Universe RegisterTag →
+  res ((nat → option register) × (Universe RegisterTag) × (list registers)) ≝
 λm,lrs,g.
 foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;
@@ -79 +56 @@
 definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
 λpre_f.
-  let rgen0 ≝ register_gen_new in
+  let rgen0 ≝ new_universe RegisterTag in
   do 〈rmapgen1, result〉 ← make_registers (λ_.None ?) (pf_result pre_f) rgen0;
   let 〈rmap1, rgen1〉 ≝ rmapgen1 in
@@ -88 +65 @@
   let rmap ≝ λn. opt_to_res … (rmap3 n) in
   let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
-  do 〈labels, gen〉 ← n_labels (S max_stmt) label_gen_new;
+  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
   let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in
   do graph ← foldr ?? (λp,g0. do g ← g0;
@@ -94 +71 @@
                               do l' ← get_label l;
                               do s' ← s rmap get_label;
-                              OK ? (graph_add ? g l' s')) (OK ? (empty_graph ?)) (pf_graph pre_f);
+                              OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
   do entry ← get_label (pf_entry pre_f);
   do exit ← get_label (pf_exit pre_f);

src/common/Graphs.ma

@@ -2 +2 @@
 
 include "ASM/BitVectorTrie.ma".
-include "Clight/AST.ma".
-include "common/Errors.ma".
+include "common/Identifiers.ma".
 
-definition label ≝ ident.
+axiom LabelTag : String.
 
-definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq.
+definition label ≝ Identifier LabelTag.
 
-record label_generation : Type[0] ≝ { lab_next : label }.
+definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
 
-definition label_gen_new : label_generation ≝ mk_label_generation (zero ?).
 
-definition label_new : label_generation → res (label × label_generation) ≝
-λg. let 〈gen, carries〉 ≝ add_with_carries ? (lab_next g) (zero ?) true in
-    if get_index_v ?? carries 0 ? then Error ? else
-      OK ? 〈lab_next g, mk_label_generation gen〉.
-// qed.
-
-definition graph : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
-definition empty_graph : ∀T. graph T ≝ λT. Stub T 16.
-definition graph_lookup : ∀T. graph T → label → option T ≝
-λT,g,l. lookup_opt T 16 l g.
-definition graph_add : ∀T. graph T → label → T → graph T ≝
-λT,g,l,v. insert T 16 l v g.
+definition graph : Type[0] → Type[0] ≝ IdentifierMap LabelTag.

src/common/Registers.ma

@@ -5 +5 @@
 
 include "ASM/BitVectorTrie.ma".
-include "Clight/AST.ma".
-include "common/Errors.ma".
+include "common/Identifiers.ma".
 
-definition register ≝ ident.
+axiom RegisterTag : String.
 
-definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq.
+definition register ≝ Identifier RegisterTag.
 
-record register_generation : Type[0] ≝ { reg_next : register }.
+definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
 
-definition register_gen_new : register_generation ≝ mk_register_generation (zero ?).
-
-definition register_new : register_generation → res (register × register_generation) ≝
-λg. let 〈gen, carries〉 ≝ add_with_carries ? (reg_next g) (zero ?) true in
-    if get_index_v ?? carries 0 ? then Error ? else
-      OK ? 〈reg_next g, mk_register_generation gen〉.
-// qed.
-
-definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
-definition register_empty : ∀T. register_env T ≝ λT. Stub T 16.
-definition register_lookup : ∀T. register_env T → register → option T ≝
-λT,g,l. lookup_opt T 16 l g.
-definition register_update : ∀T. register → T → register_env T → register_env T ≝
-λT,l,v,g. insert T 16 l v g.
+definition register_env ≝ IdentifierMap RegisterTag.