Changeset 757 for src/common


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (9 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

Location:
src/common
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r747 r757  
    497497
    498498(* dpm: should go to standard library *)
    499 let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
    500                (g: list Identifier) on g: Prop ≝
     499let rec member (i: ident) (eq_i: ident → ident → bool)
     500               (g: list ident) on g: Prop ≝
    501501  match g with
    502502  [ nil ⇒ False
  • src/common/CostLabel.ma

    r747 r757  
    77(* For use in importing programs in intermediate languages. *)
    88definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
     9
     10(* dpm: fix identifier/costlabel mismatch *)
     11axiom Identifier_of_costlabel: costlabel → Identifier.
  • src/common/Identifiers.ma

    r753 r757  
    2424      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
    2525// qed.
     26
     27definition eq_identifier ≝
     28  λt.
     29  λl, r: identifier t.
     30  match l with
     31  [ an_identifier l' ⇒
     32    match r with
     33    [ an_identifier r' ⇒
     34      eq_bv ? l' r'
     35    ]
     36  ].
     37   
     38   
     39definition word_of_identifier ≝
     40  λt.
     41  λl: identifier t.
     42  match l with   
     43  [ an_identifier l' ⇒ l'
     44  ].
    2645
    2746definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
  • src/common/Registers.ma

    r738 r757  
    66include "ASM/BitVectorTrie.ma".
    77include "common/Identifiers.ma".
     8include "ASM/I8051.ma".
    89
    910axiom RegisterTag : String.
     
    1415
    1516definition register_env ≝ identifier_map RegisterTag.
     17
     18(* dpm: fix the Register/register mismatch *)
     19axiom Register_of_register: register → Register.
Note: See TracChangeset for help on using the changeset viewer.