Changeset 1059 for src/common/AST.ma


Ignore:
Timestamp:
Jul 6, 2011, 6:09:39 PM (8 years ago)
Author:
mulligan
Message:

work from today, bit of a mess at the moment

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1057 r1059  
    4343definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
    4444
     45(* dpm: not needed
    4546inductive quantity: Type[0] ≝
    4647  | q_int: Byte → quantity
     
    5354  | size_sum: list abstract_size → abstract_size
    5455  | size_array: nat → abstract_size → abstract_size.
    55 
    56 definition abstract_offset ≝ abstract_size × nat. (* nth in size *)
    57 
    58 inductive cast: Type[0] ≝
    59   | cast_int: Byte → cast                     (* integer constant *)
    60 (*  | cast_float: float → cast                (* float constant *) *)
    61   | cast_addrsymbol: ident → cast      (* address of a global symbol *)
    62   | cast_stack: cast                          (* address of the stack *)
    63   | cast_offset: abstract_offset → cast       (* offset *)
    64   | cast_sizeof: abstract_size → cast.        (* size of a type *)
     56*)
    6557
    6658(* Memory spaces *)
     
    191183definition repr : ∀sz:intsize. nat → bvint sz ≝
    192184λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
    193 
    194185
    195186definition size_floatsize : floatsize → nat ≝
Note: See TracChangeset for help on using the changeset viewer.