Ignore:
Timestamp:
Sep 15, 2011, 2:01:56 PM (8 years ago)
Author:
sacerdot
Message:

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r1181 r1213  
    1 
    21include "utilities/extralib.ma".
    32include "common/IOMonad.ma".
    43include "common/Integers.ma".
    54include "common/Events.ma".
    6 include "common/Mem.ma".
    75
    86record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    9 { genv  : Type[0]
     7{ mem : Type[0]
     8; genv  : Type[0]
    109; state : Type[0]
    1110; is_final : state → option int
     
    3534(* A (possibly non-terminating) execution.   *)
    3635coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
    37 | e_stop : trace → int → mem → execution state output input
     36| e_stop : trace → int → state → execution state output input
    3837| e_step : trace → state → execution state output input → execution state output input
    3938| e_wrong : errmsg → execution state output input
     
    5251| Value v ⇒ match v with [ pair t s' ⇒
    5352    match is_final ?? exec s' with
    54     [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     53    [ Some r ⇒ e_stop ??? t r s'
    5554    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    5655| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
     
    7069| Value v ⇒ match v with [ pair t s' ⇒
    7170    match is_final ?? exec s' with
    72     [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     71    [ Some r ⇒ e_stop ??? t r s'
    7372    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    7473| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
Note: See TracChangeset for help on using the changeset viewer.