Ignore:
Timestamp:
Apr 19, 2011, 12:22:32 PM (9 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r757 r761  
    7070                              (match m with [ an_id_map m' ⇒ m' ]).
    7171
     72(* Always adds the identifier to the map. *)
    7273definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
    7374λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    7475                                           (match m with [ an_id_map m' ⇒ m' ])).
    7576
     77(* Only updates an existing entry; fails with an error otherwise. *)
     78definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
     79λtag,A,m,l,a.
     80  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
     81                    (match m with [ an_id_map m' ⇒ m' ]) with
     82  [ None ⇒ Error ? (* missing identifier *)
     83  | Some m' ⇒ OK ? (an_id_map tag A m')
     84  ].
    7685
Note: See TracChangeset for help on using the changeset viewer.