Changeset 1359 for src/joint/BEValues.ma


Ignore:
Timestamp:
Oct 11, 2011, 6:00:03 PM (8 years ago)
Author:
sacerdot
Message:
  1. more work on the RTL semantics
  2. changes to joint/semantics to accomodate the RTL one
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEValues.ma

    r1213 r1359  
    121121  | _ ⇒ Error … [MSG BadByte]].
    122122
     123axiom NotAnInt32Val: String.
     124definition Word_of_list_beval: list beval → res int ≝
     125 λl.
     126  let first_byte ≝ λl.
     127   match l with
     128    [ nil ⇒ Error ? [MSG NotAnInt32Val]
     129    | cons hd tl ⇒ do b ← Byte_of_val hd ; OK ? 〈b,tl〉 ] in
     130  do 〈b1,l〉 ← first_byte l ;
     131  do 〈b2,l〉 ← first_byte l ;
     132  do 〈b3,l〉 ← first_byte l ;
     133  do 〈b4,l〉 ← first_byte l ;
     134   match l with
     135    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
     136    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
     137
    123138(* CSC: maybe we should introduce a type of 1-bit-sized values *)
    124139definition BVtrue: beval ≝ BVByte [[false;false;false;false;false;false;false;true]].
Note: See TracChangeset for help on using the changeset viewer.