Changeset 761 for src/common/Identifiers.ma

Timestamp:

Apr 19, 2011, 12:22:32 PM (10 years ago)

Author:

campbell

Message:

Enforce the use of declared identifiers/registers in Cminor/RTLabs.

File:

• src/common/Identifiers.ma (modified) (1 diff)

src/common/Identifiers.ma

@@ -70 +70 @@
                               (match m with [ an_id_map m' ⇒ m' ]).
 
+(* Always adds the identifier to the map. *)
 definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
 λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
                                            (match m with [ an_id_map m' ⇒ m' ])).
 
+(* Only updates an existing entry; fails with an error otherwise. *)
+definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
+λtag,A,m,l,a.
+  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
+                    (match m with [ an_id_map m' ⇒ m' ]) with
+  [ None ⇒ Error ? (* missing identifier *)
+  | Some m' ⇒ OK ? (an_id_map tag A m')
+  ].