Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (7 years ago)
Author:
sacerdot
Message:
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2608 r2645  
    110110
    111111include alias "arithmetics/nat.ma".
    112 
    113 axiom CorruptedPointer: String.
    114112
    115113(* CSC: use vectors in place of lists? Or even better products of tuples
     
    203201qed.
    204202
    205 axiom NotATwoBytesPointer: String.
    206 
    207203(* Should fail if the address is not representable as a pair
    208204   As we only have 16 bit addresses atm, it never fails *)
     
    219215 λp. list_to_pair ? (bevals_of_pc p) (refl …).
    220216
    221 (* axiom NotACodePointer: String.
     217(*
    222218definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
    223219 λp.
     
    227223  [ Code ⇒ λE.OK ? (mk_Sig … p E)
    228224  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)
    229 
    230 axiom ValueNotABoolean: String.
    231225
    232226definition bool_of_beval: beval → res bool ≝
     
    244238  ].
    245239
    246 definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
     240definition Byte_of_val: ErrorMessage → beval → res Byte ≝ (*CSC: move elsewhere *)
    247241 λerr,b.match b with
    248242  [ BVByte b ⇒ OK … b
    249243  | _ ⇒ Error … [MSG err]].
    250244
    251 axiom NotAnInt32Val: String.
    252245definition Word_of_list_beval: list beval → res int ≝
    253246 λl.
     
    270263  (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.
    271264
    272 definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
     265definition Bit_of_val: ErrorMessage → bebit → res Bit ≝ (*CSC: move elsewhere *)
    273266 λerr,b.match b with
    274267  [ BBbit b ⇒ OK … b
Note: See TracChangeset for help on using the changeset viewer.