Changeset 738 for src/RTLabs


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

Use lower case names for identifiers for consistency with CompCert? derived code
and to prevent confusion with the back-end equivalents until they're all merged.

Location:
src/RTLabs
Files:
2 edited

Legend:

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

    r736 r738  
    5959
    6060record internal_function : Type[0] ≝
    61 { f_labgen    : Universe LabelTag
    62 ; f_reggen    : Universe RegisterTag
     61{ f_labgen    : universe LabelTag
     62; f_reggen    : universe RegisterTag
    6363; f_sig       : signature
    6464; f_result    : registers
  • src/RTLabs/import.ma

    r736 r738  
    22include "RTLabs/RTLabs-sem.ma".
    33
    4 let rec n_idents (n:nat) (tag:String) (g:Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝
     4let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝
    55match n with
    66[ O ⇒ OK ? 〈[[ ]], g〉
     
    2929
    3030definition make_registers :
    31   (nat → option register) → pre_registers → Universe RegisterTag →
    32   res ((nat → option register) × (Universe RegisterTag) × registers) ≝
     31  (nat → option register) → pre_registers → universe RegisterTag →
     32  res ((nat → option register) × (universe RegisterTag) × registers) ≝
    3333λm,rs0,g.
    3434match rs0 with [ dp n rs ⇒
     
    4646
    4747definition make_registers_list :
    48   (nat → option register) → list pre_registers → Universe RegisterTag →
    49   res ((nat → option register) × (Universe RegisterTag) × (list registers)) ≝
     48  (nat → option register) → list pre_registers → universe RegisterTag →
     49  res ((nat → option register) × (universe RegisterTag) × (list registers)) ≝
    5050λm,lrs,g.
    5151foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;
Note: See TracChangeset for help on using the changeset viewer.