Changeset 2767 for src/common


Ignore:
Timestamp:
Mar 3, 2013, 2:03:58 PM (7 years ago)
Author:
mckinna
Message:

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r2645 r2767  
    1919include "basics/types.ma".
    2020include "common/Integers.ma".
     21include "common/Identifiers.ma".
    2122include "ASM/Arithmetic.ma".
    22 include "common/Identifiers.ma".
    2323
    2424
  • src/common/CostLabel.ma

    r2703 r2767  
    1 include "common/AST.ma".
    2 include "ASM/BitVectorTrie.ma".
     1include "common/Identifiers.ma".
    32
    43definition costlabel ≝ identifier CostTag.
     4
     5definition costlabel_eq : ∀x,y:costlabel. (x=y) + (x≠y) ≝ identifier_eq ?.
    56
    67(* For use in importing programs in intermediate languages. *)
    78definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
    89
    9 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    10 (* Costlabel Maps: the other distinguished instance of BitVectorTrie.         *)
    11 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    12 
    13 definition costlabel_map ≝ BitVectorTrie costlabel 16 (* ADDRESS_WIDTH *).
    14 
    15 definition costlabel_map0 : costlabel_map ≝ Stub ….
    16 
    17 definition costlabel_map_injective ≝
    18   λcost_labels: costlabel_map.
    19     ∀pc, pc',l.
    20       lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    21         pc = pc'.
    22        
  • src/common/LabelledObjects.ma

    r2133 r2767  
     1include "utilities/lists.ma".
    12include "common/Identifiers.ma".
    2 include "utilities/lists.ma".
     3
    34include alias "arithmetics/nat.ma".
    45
Note: See TracChangeset for help on using the changeset viewer.