Changeset 1600


Ignore:
Timestamp:
Dec 13, 2011, 1:41:08 PM (8 years ago)
Author:
sacerdot
Message:

utilities and ASM ported to the new standard library

Location:
src
Files:
6 deleted
9 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1553 r1600  
    11include "basics/types.ma".
    2 
    3 include "utilities/option.ma".
    42include "ASM/BitVector.ma".
    53
  • src/ASM/Erase.ma

    r1515 r1600  
    8484      Mov dptr located
    8585  ].
    86      
     86
    8787let rec relabel
    8888  (the_program: list labelled_instruction) (map: identifier_map ASMTag Identifier)
     
    9696      match label with
    9797      [ None ⇒ None …
    98       | Some label ⇒ Some … (lookup_def map ident ident)
     98      | Some label ⇒ Some … (lookup_def ?? map ident ident)
    9999      ]
    100100    in
  • src/ASM/Fetch.ma

    r1598 r1600  
    22include "ASM/Arithmetic.ma".
    33include "ASM/ASM.ma".
     4include "basics/russell.ma".
    45
    56definition bitvector_max_nat ≝
     
    89
    910definition code_memory_size ≝ bitvector_max_nat 16.
    10 
    11 include "ASM/JMCoercions.ma".
    1211
    1312axiom bitvector_lt_bitvector_max_nat:
  • src/ASM/FoldStuff.ma

    r1598 r1600  
    11include "ASM/Util.ma".
    2 include "ASM/JMCoercions.ma".
     2include "basics/russell.ma".
    33
    44let rec foldl_strong_internal
  • src/ASM/I8051.ma

    r1515 r1600  
    55include "ASM/ASM.ma".
    66include "ASM/Arithmetic.ma".
    7 include "utilities/Compare.ma".
    87include "joint/BEValues.ma".
    98include "ASM/BitVectorTrie.ma".
     
    118117  λregister.
    119118    bitvector_of_nat ? (nat_of_register register).
    120 
    121 definition compare_register: Register → Register → compare ≝
    122   λr, s: Register.
    123     let r_as_nat ≝ nat_of_register r in
    124     let s_as_nat ≝ nat_of_register s in
    125       match eqb r_as_nat s_as_nat with
    126       [ true ⇒ compare_equal
    127       | false ⇒
    128         match ltb r_as_nat s_as_nat with
    129         [ true ⇒ compare_less
    130         | false ⇒ compare_greater
    131         ]
    132       ].
    133119
    134120definition eq_Register: Register → Register → bool ≝
  • src/ASM/Interpret.ma

    r1588 r1600  
    11include "ASM/Status.ma".
    22include "ASM/Fetch.ma".
    3 include "ASM/JMCoercions.ma".
    43
    54definition sign_extension: Byte → Word ≝
  • src/ASM/Status.ma

    r1599 r1600  
    66include "ASM/Arithmetic.ma".
    77include "ASM/BitVectorTrie.ma".
    8 include "ASM/JMCoercions.ma".
     8include "basics/russell.ma".
    99
    1010definition Time ≝ nat.
     
    785785
    786786lemma set_arg_16_ok: ∀M,s,v,x. clock M s = clock … (set_arg_16 M s v x).
    787  #M #s #x #v whd in match set_arg_16; normalize nodelta @sig2
     787 #M #s #x #v whd in match set_arg_16; normalize nodelta @pi2
    788788qed.
    789789
     
    926926
    927927lemma set_arg_8_ok: ∀M,s,x,v. clock M s = clock … (set_arg_8 M s x v).
    928  #M #s #x #v whd in match set_arg_8; normalize nodelta @sig2
     928 #M #s #x #v whd in match set_arg_8; normalize nodelta @pi2
    929929qed.
    930930
     
    10841084
    10851085lemma set_arg_1_ok: ∀M,s,x,v. clock M s = clock … (set_arg_1 M s x v).
    1086  #M #s #x #v whd in match set_arg_1; normalize nodelta @sig2
     1086 #M #s #x #v whd in match set_arg_1; normalize nodelta @pi2
    10871087qed.
    10881088
  • src/ASM/Util.ma

    r1599 r1600  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
    4 include "ASM/JMCoercions.ma".
     4include "basics/russell.ma".
    55
    66(* let's implement a daemon not used by automation *)
     
    271271  [ 1: normalize %
    272272  | 2: normalize %
    273   | 3: normalize
    274        generalize in match (sig2 … (reduce_strong A B tl tl1));
    275        >p2 >p3 >p4 normalize in ⊢ (% → ?);
    276        #HYP //
    277   ]
    278 qed.
     273  | 3: normalize >p3 in p2; >p4 cases (reduce_strong … tl tl1) normalize
     274       #X #H #EQ destruct // ]
     275qed.
    279276   
    280277let rec map2_opt
  • src/utilities/Coqlib.ma

    r1599 r1600  
    599599(* * Mapping a function over an option type. *)
    600600
    601 include "utilities/option.ma".
    602 
    603601(*
    604602(** Mapping a function over a sum type. *)
Note: See TracChangeset for help on using the changeset viewer.