Changeset 1049


Ignore:
Timestamp:
Jul 1, 2011, 5:45:46 PM (8 years ago)
Author:
mulligan
Message:

more stuff added

Location:
src
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1047 r1049  
    33include "common/AssocList.ma".
    44include "common/Graphs.ma".
     5include "common/Maps.ma".
     6include "utilities/HMap.ma".
    57
    68definition add_graph ≝
     
    111113  ].
    112114
    113 definition concrete_size ≝ .
    114 
    115 definition concrete_offset ≝ .
    116 
    117115inductive register_type: Type[0] ≝
    118116  | register_int: register → register_type
    119117  | register_ptr: register → register → register_type.
    120118
    121 definition local_env ≝ assoc_list register register_type.
     119definition local_env ≝ map register (list register).
     120definition mem_local_env ≝ map_member register (list register) register_ord.
     121definition add_local_env ≝ map_insert register (list register) register_ord.
     122definition find_local_env ≝ map_lookup register (list register) register_ord.
    122123
    123124definition initialize_local_env_internal ≝
     
    134135      ]
    135136    in
    136     assoc_list_add ? ? 〈r, rt〉 lenv.
     137    add_local_env ? ? 〈r, rt〉 lenv.
    137138
    138139definition initialize_local_env ≝
  • src/common/Registers.ma

    r777 r1049  
    11
    22(* NB: this is essentially the same as Graphs! *)
    3 
    4 include "basics/types.ma".
    53
    64include "ASM/BitVectorTrie.ma".
    75include "common/Identifiers.ma".
    86include "ASM/I8051.ma".
     7include "common/Order.ma".
    98
    109axiom RegisterTag : String.
     
    1615definition register_env ≝ identifier_map RegisterTag.
    1716
     17axiom register_ord: register → register → order.
     18
    1819(* dpm: fix the Register/register mismatch *)
    1920axiom Register_of_register: register → Register.
  • src/utilities/HMap.ma

    r1048 r1049  
    55
    66include "arithmetics/nat.ma".
    7 include "basics/types.ma".
     7include "common/Order.ma".
    88
    99(* for eq_rect_Type0_r *)
     
    6464  | map_fork sz key elt l r ⇒ sz
    6565  ].
    66 
    67 inductive order: Type[0] ≝
    68   | order_lt: order
    69   | order_eq: order
    70   | order_gt: order.
    7166
    7267(* -------------------------------------------------------------------------- *)
Note: See TracChangeset for help on using the changeset viewer.