Changeset 1047 for src/common


Ignore:
Timestamp:
Jun 29, 2011, 5:38:27 PM (8 years ago)
Author:
mulligan
Message:

more work from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1046 r1047  
    5454  | size_array: nat → abstract_size → abstract_size.
    5555
     56definition abstract_offset ≝ abstract_size × nat. (* nth in size *)
     57
    5658inductive cast: Type[0] ≝
    5759  | cast_int: Byte → cast                     (* integer constant *)
    5860(*  | cast_float: float → cast                (* float constant *) *)
    59   | cast_addrsymbol of identifier → cast      (* address of a global symbol *)
     61  | cast_addrsymbol: Identifier → cast      (* address of a global symbol *)
    6062  | cast_stack: cast                          (* address of the stack *)
    6163  | cast_offset: abstract_offset → cast       (* offset *)
     
    119121  | ASTint : intsize → signedness → typ
    120122  | ASTptr : region → typ
     123  | ASToffset: typ
    121124  | ASTfloat : floatsize → typ.
    122125
     
    198201  [ ASTint sz _ ⇒ size_intsize sz
    199202  | ASTptr r ⇒ size_pointer r
     203  | ASToffset ⇒ 1 (* dpm: what!? need this for typesize pos --- not sure what correct size of an offset should be? *)
    200204  | ASTfloat sz ⇒ size_floatsize sz ].
    201205
    202206lemma typesize_pos: ∀ty. typesize ty > 0.
    203 * *; try * /2/ qed.
     207*; try *; try * /2/ qed.
    204208
    205209lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    206 * * * *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed.
     210* *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed.
    207211
    208212lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
     
    658662
    659663definition Trace ≝ list Identifier.
    660 
    661 (* dpm: how are floats represented? *)
    662 inductive cast: Type[0] ≝
    663   | cast_int: Byte → cast                    (* integer constant *)
    664   | cast_float: Byte → cast                  (* float constant *)
    665   | cast_addr_symbol: ident → cast      (* address of a global symbol *)
    666   | cast_stack_offset: Byte → cast.
    667664
    668665inductive op1: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.