Theory PromelaLTLConv

theory PromelaLTLConv
imports 
  Promela
  LTL.LTL
begin
subsection ‹Proposition types and conversion›

text ‹LTL formulae and propositions are also generated by an SML parser.
Hence we have the same setup as for Promela itself: Mirror the data structures and
(sometimes) map them to new ones.›

text ‹This theory is intended purely to be used by frontend code to convert
from ‹propc› to ‹expr›. The other theories work on @{typ expr} directly.

While we could of course convert directly, that would introduce yet a semantic level.›

datatype binOp = Eq | Le | LEq | Gr | GEq

datatype ident = Ident "String.literal" "integer option"

datatype propc = CProp ident
               | BProp binOp ident ident
               | BExpProp binOp ident integer

fun identConv :: "ident ⇒ varRef" where
  "identConv (Ident name None) = VarRef True name None"
| "identConv (Ident name (Some i)) = VarRef True name (Some (ExprConst i))"

definition ident2expr :: "ident ⇒ expr" where
  "ident2expr = ExprVarRef ∘ identConv"

primrec binOpConv :: "binOp ⇒ PromelaDatastructures.binOp" where
  "binOpConv Eq = BinOpEq"
| "binOpConv Le = BinOpLe"
| "binOpConv LEq = BinOpLEq"
| "binOpConv Gr = BinOpGr"
| "binOpConv GEq = BinOpGEq"

primrec propc2expr :: "propc ⇒ expr" where
  "propc2expr (CProp ident) = 
     ExprBinOp BinOpEq (ident2expr ident) (ExprConst 1)"
| "propc2expr (BProp bop il ir) = 
     ExprBinOp (binOpConv bop) (ident2expr il) (ident2expr ir)"
| "propc2expr (BExpProp bop il ir) = 
     ExprBinOp (binOpConv bop) (ident2expr il) (ExprConst ir)"

definition ltl_conv :: "propc ltlc ⇒ expr ltlc" where
  "ltl_conv = map_ltlc propc2expr"

definition printPropc 
  :: "(integer ⇒ char list) ⇒ propc ⇒ char list"
where
  "printPropc f p = printExpr f (propc2expr p)" 

text ‹The semantics of a @{typ propc} is given just for reference.›
definition evalPropc :: "gState ⇒ propc ⇒ bool" where
  "evalPropc g p ⟷ exprArith g emptyProc (propc2expr p) ≠ 0"

end