Theory PiCore_Language

(*
Created by Yongwang Zhao (zhaoyw@buaa.edu.cn)
School of Computer Science & Engineering, Beihang University, China
*)

section ‹Abstract Syntax of PiCore Language›

theory PiCore_Language
imports Main begin

(* 'prog: the type of program command *)

type_synonym ('l,'s,'prog) event = "'l × ('s set × 'prog)"

definition guard :: "('l,'s,'prog) event ⇒ 's set" where
  "guard ev ≡ fst (snd ev)"

definition body :: "('l,'s,'prog) event ⇒ 'prog" where
  "body ev ≡ snd (snd ev)"

(* unused type parameter 'k required by definition of validity *)
datatype ('l,'k,'s,'p) esys =
      EAnon 'p                        (* used to represent the internal steps of the other two events *)
    | EBasic "('l,'s,'p) event"     (* general event def *)
    | EAtom  "('l,'s,'p) event"     (* atomic event: the execution of the whole event is atomic *)
    | ESeq "('l,'k,'s,'p) esys" "('l,'k,'s,'p) esys" ("_ NEXT _" [81,81] 80)
      (* sequence *)
    | EChc "('l,'k,'s,'p) esys" "('l,'k,'s,'p) esys" ("_ OR _" [81,81] 80)
      (* non-deterministic choice of one event *)
    | EJoin "('l,'k,'s,'p) esys" "('l,'k,'s,'p) esys" ("_ ⋈ _" [81,81] 80)
      (* require all events executed. its non-deterministic of the order *)
    | EWhile "'s set" "('l,'k,'s,'p) esys"
      (* recursive of an event system *)

primrec es_size :: ‹('l,'k,'s,'p) esys ⇒ nat› where
  ‹es_size (EAnon _) = 1› |
  ‹es_size (EBasic _) = 1› |
  ‹es_size (EAtom _) = 1› |
  ‹es_size (ESeq es1 es2) = Suc (es_size es1 + es_size es2)› |
  ‹es_size (EChc es1 es2) = Suc (es_size es1 + es_size es2)› |
  ‹es_size (EJoin es1 es2) = Suc (es_size es1 + es_size es2)› |
  ‹es_size (EWhile _ es) = Suc (es_size es)›


type_synonym ('l,'k,'s,'prog) paresys = "'k ⇒ ('l,'k,'s,'prog) esys"

end