Changeset 702 for src/common


Ignore:
Timestamp:
Mar 21, 2011, 6:27:22 PM (9 years ago)
Author:
campbell
Message:

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

Location:
src/common
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r695 r702  
    1818(* *********************************************************************)
    1919
    20 include "Values.ma".
     20include "common/Values.ma".
    2121
    2222inductive constant : Type[0] ≝
  • src/common/Graphs.ma

    r695 r702  
    22include "basics/logic.ma".
    33
    4 include "binary/positive.ma".
    5 include "Maps.ma".
     4include "utilities/binary/positive.ma".
     5include "common/Maps.ma".
    66
    77definition label : Type[0] ≝ Pos.
  • src/common/Registers.ma

    r695 r702  
    33
    44include "basics/types.ma".
    5 include "binary/positive.ma".
     5include "utilities/binary/positive.ma".
    66
    7 include "Maps.ma".
     7include "common/Maps.ma".
    88
    99definition register ≝ Pos.
  • src/common/SmallstepExec.ma

    r700 r702  
    1111; output : Type[0]
    1212; input : output → Type[0]
    13 ; initial : state → Prop
    1413; is_final : state → option int
    1514; mem_of_state : state → mem
     
    7271*)
    7372
     73record execstep' : Type[1] ≝
     74{ es0 :> execstep
     75; initial : state es0 → Prop
     76}.
    7477
    7578
    7679alias symbol "and" (instance 2) = "logical and".
    7780record related_semantics : Type[1] ≝
    78 { sem1 : execstep
    79 ; sem2 : execstep
     81{ sem1 : execstep'
     82; sem2 : execstep'
    8083; ge1 : genv sem1
    8184; ge2 : genv sem2
Note: See TracChangeset for help on using the changeset viewer.