Changeset 1395 for src/joint/BEValues.ma


Ignore:
Timestamp:
Oct 17, 2011, 5:41:44 PM (8 years ago)
Author:
sacerdot
Message:

1) New versions of pointer_of_beval/beval_of_pointer with a stricter dependent

type. They allow to close several proof obligations.

2) Globalenvs no longer uses -1 as a valid function block. It starts with -2
3) joint/semantics.ma uses a -2 block for the fake address used to signal the

end of program execution. Differently from what happens in OCaml, the block
is not allocated.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEValues.ma

    r1359 r1395  
    33
    44include "common/Pointers.ma".
     5include "utilities/sigma.ma".
    56
    67record part (r: region): Type[0] ≝
     
    105106% qed.
    106107
     108definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝
     109 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒
     110  match pty return λpty. ? → pty = Code → ? with
     111   [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ?
     112   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
     113[@(pi2 … p) |7: // |8: %] destruct (abs)
     114qed.
     115
     116
     117axiom NotACodePointer: String.
     118definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
     119 λp.
     120  let 〈v1,v2〉 ≝ p in
     121  do p ← pointer_of_bevals [v1;v2] ;
     122  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
     123  [ Code ⇒ λE.OK ? (inject … p ?)
     124  | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?.
     125// qed.
     126
    107127axiom ValueNotABoolean: String.
    108128
Note: See TracChangeset for help on using the changeset viewer.