Theory PromelaDatastructures

section "Data structures as used in Promela"
theory PromelaDatastructures
imports
  CAVA_Base.CAVA_Base
  CAVA_Base.Lexord_List
  PromelaAST
  "HOL-Library.IArray"
  Deriving.Compare_Instances
  CAVA_Base.CAVA_Code_Target
begin

subsection ‹Abstract Syntax Tree \emph{after} preprocessing›

text ‹
  From the plain AST stemming from the parser, we'd like to have one containing more information while also removing duplicated constructs. This is achieved in the preprocessing step.

  The additional information contains:
  \begin{itemize}
    \item variable type (including whether it represents a channel or not)
    \item global vs local variable
  \end{itemize}

  Also certain constructs are expanded (like for-loops) or different nodes in the
  AST are collapsed into one parametrized node (e.g.\ the different send-operations).

  This preprocessing phase also tries to detect certain static errors and will bail out with an exception if such is encountered.
›

datatype binOp = BinOpAdd
               | BinOpSub
               | BinOpMul
               | BinOpDiv
               | BinOpMod
               | BinOpGr
               | BinOpLe
               | BinOpGEq
               | BinOpLEq
               | BinOpEq
               | BinOpNEq
               | BinOpAnd
               | BinOpOr

datatype unOp = UnOpMinus
              | UnOpNeg

datatype expr = ExprBinOp binOp (*left*) expr (*right*) expr
              | ExprUnOp unOp expr
              | ExprCond (*cond*) expr (*exprTrue*) expr (*exprFalse*) expr
              | ExprLen chanRef
              | ExprVarRef varRef
              | ExprConst integer
              | ExprMConst integer String.literal (* MType replaced by constant *)
              | ExprTimeOut
              | ExprFull chanRef
              | ExprEmpty chanRef
              | ExprPoll chanRef "recvArg list" bool (* sorted *)

   and varRef = VarRef (*global*) bool 
                       (*name*) String.literal 
                       (*index*) "expr option"
   and chanRef = ChanRef varRef ― ‹explicit type for channels›
   and recvArg = RecvArgVar varRef
               | RecvArgEval expr
               | RecvArgConst integer
               | RecvArgMConst integer String.literal

datatype varType = VTBounded integer integer
                 | VTChan

text ‹Variable declarations at the beginning of a proctype or at global level.›
datatype varDecl = VarDeclNum (*bounds*) integer integer
                              (*name*) String.literal
                              (*size*) "integer option"
                              (*init*) "expr option"
                 | VarDeclChan (*name*) String.literal
                               (*size*) "integer option"
                               (*capacityTypes*) "(integer * varType list) option"

text ‹Variable declarations during a proctype.›
datatype procVarDecl = ProcVarDeclNum  (*bounds*) integer integer
                                       (*name*) String.literal
                                       (*size*) "integer option"
                                       (*init*) "expr option"
                     | ProcVarDeclChan (*name*) String.literal
                                       (*size*) "integer option"

datatype procArg = ProcArg varType String.literal

datatype stmnt = StmntIf "(step list) list"
               | StmntDo "(step list) list"
               | StmntAtomic "step list"
               | StmntSeq "step list"
               | StmntSend chanRef "expr list" bool (*sorted*)
               | StmntRecv chanRef "recvArg list" bool (*sorted*) bool (*remove?*)
               | StmntAssign varRef expr
               | StmntElse
               | StmntBreak
               | StmntSkip
               | StmntGoTo String.literal
               | StmntLabeled String.literal stmnt
               | StmntRun (*name*) String.literal
                          (*args*) "expr list"
               | StmntCond expr
               | StmntAssert expr
        
  and step = StepStmnt stmnt (*unless*) "stmnt option"
           | StepDecl "procVarDecl list"
           | StepSkip

datatype proc = ProcType (*active*) "(integer option) option"
                           (*name*)   String.literal
                           (*args*)  "procArg list"
                           (*decls*) "varDecl list"
                           (*seq*)    "step list"
              | Init "varDecl list" "step list"

type_synonym ltl = "― ‹name:› String.literal × ― ‹formula:› String.literal"
type_synonym promela = "varDecl list × proc list × ltl list"

subsection ‹Preprocess the AST of the parser into our variant›

text ‹We setup some functionality for printing warning or even errors.

All those constants are logically @{term undefined}, but replaced by the parser
for something meaningful.›
consts 
  warn :: "String.literal ⇒ unit"

abbreviation "with_warn msg e ≡ let _ = warn msg in e"
abbreviation "the_warn opt msg ≡ case opt of None ⇒ () | _ ⇒ warn msg"

text ‹‹usc›: "Unsupported Construct"›
definition [code del]: "usc (c :: String.literal) ≡ undefined"

definition  [code del]: "err (e :: String.literal) = undefined"
abbreviation "errv e v ≡ err (e + v)"

definition [simp, code del]: "abort (msg :: String.literal) f = f ()"
abbreviation "abortv msg v f ≡ abort (msg + v) f"

code_printing
  code_module PromelaUtils ⇀ (SML) ‹
    structure PromelaUtils = struct
      exception UnsupportedConstruct of string
      exception StaticError of string
      exception RuntimeError of string
      fun warn msg = TextIO.print ("Warning: " ^ msg ^ "\n")
      fun usc  c   = raise (UnsupportedConstruct c)
      fun err  e   = raise (StaticError e)
      fun abort msg _ = raise (RuntimeError msg)
    end›
| constant warn ⇀ (SML) "PromelaUtils.warn"
| constant usc ⇀ (SML) "PromelaUtils.usc"
| constant err ⇀ (SML) "PromelaUtils.err"
| constant abort ⇀ (SML) "PromelaUtils.abort"
code_reserved SML PromelaUtils


(*<*)
ML_val ‹@{code hd}› (* Test code-printing setup. If this fails, the setup is skewed. *)
(*>*)

text ‹The preprocessing is done for each type on its own.›

primrec ppBinOp :: "AST.binOp ⇒ binOp"
where
  "ppBinOp AST.BinOpAdd = BinOpAdd"
| "ppBinOp AST.BinOpSub = BinOpSub"
| "ppBinOp AST.BinOpMul = BinOpMul"
| "ppBinOp AST.BinOpDiv = BinOpDiv"
| "ppBinOp AST.BinOpMod = BinOpMod"
| "ppBinOp AST.BinOpGr = BinOpGr"
| "ppBinOp AST.BinOpLe = BinOpLe"
| "ppBinOp AST.BinOpGEq = BinOpGEq"
| "ppBinOp AST.BinOpLEq = BinOpLEq"
| "ppBinOp AST.BinOpEq = BinOpEq"
| "ppBinOp AST.BinOpNEq = BinOpNEq"
| "ppBinOp AST.BinOpAnd = BinOpAnd"
| "ppBinOp AST.BinOpOr = BinOpOr"
| "ppBinOp AST.BinOpBitAnd = usc STR ''BinOpBitAnd''"
| "ppBinOp AST.BinOpBitXor = usc STR ''BinOpBitXor''"
| "ppBinOp AST.BinOpBitOr = usc STR ''BinOpBitOr''"
| "ppBinOp AST.BinOpShiftL = usc STR ''BinOpShiftL''"
| "ppBinOp AST.BinOpShiftR = usc STR ''BinOpShiftR''"

primrec ppUnOp :: "AST.unOp ⇒ unOp"
where
  "ppUnOp AST.UnOpMinus = UnOpMinus"
| "ppUnOp AST.UnOpNeg = UnOpNeg"
| "ppUnOp AST.UnOpComp = usc STR ''UnOpComp''"

text ‹The data structure holding all information on variables we found so far.›
type_synonym var_data = "
     (String.literal, (integer option × bool)) lm ― ‹channels›
     × (String.literal, (integer option × bool)) lm ― ‹variables›
     × (String.literal, integer) lm ― ‹mtypes›
     × (String.literal, varRef) lm ― ‹aliases (used for inlines)›"

definition dealWithVar 
  :: "var_data ⇒ String.literal
      ⇒ (String.literal ⇒ integer option × bool ⇒ expr option ⇒ 'a) 
      ⇒ (String.literal ⇒ integer option × bool ⇒ expr option ⇒ 'a) 
      ⇒ (integer ⇒ 'a) ⇒ 'a"
where
  "dealWithVar cvm n fC fV fM ≡ ( 
    let (c,v,m,a) = cvm in
    let (n, idx) = case lm.lookup n a of 
                     None ⇒ (n, None) 
                   | Some (VarRef _ name idx) ⇒ (name, idx) 
    in
    case lm.lookup n m of 
      Some i ⇒ (case idx of None ⇒ fM i 
                           | _ ⇒ err STR ''Array subscript used on MType (via alias).'')
    | None ⇒ (case lm.lookup n v of
               Some g ⇒ fV n g idx
             | None ⇒ (case lm.lookup n c of
                   Some g ⇒ fC n g idx
                 | None ⇒ err (STR ''Unknown variable referenced: '' + n))))"

primrec enforceChan :: "varRef + chanRef ⇒ chanRef" where
  "enforceChan (Inl _) = err STR ''Channel expected. Got normal variable.''"
| "enforceChan (Inr c) = c"

fun liftChan :: "varRef + chanRef ⇒ varRef" where
  "liftChan (Inl v) = v"
| "liftChan (Inr (ChanRef v)) = v"

fun resolveIdx :: "expr option ⇒ expr option ⇒ expr option"
where
  "resolveIdx None None = None"
| "resolveIdx idx  None = idx"
| "resolveIdx None aliasIdx = aliasIdx"
| "resolveIdx _   _     = err STR ''Array subscript used twice (via alias).''"

fun ppExpr :: "var_data ⇒ AST.expr ⇒ expr"
and ppVarRef :: "var_data ⇒ AST.varRef ⇒ varRef + chanRef"
and ppRecvArg :: "var_data ⇒ AST.recvArg ⇒ recvArg"
where
  "ppVarRef cvm (AST.VarRef name idx None) = dealWithVar cvm name
                    (λname (_,g) aIdx. let idx = map_option (ppExpr cvm) idx in 
                         Inr (ChanRef (VarRef g name (resolveIdx idx aIdx))))
                    (λname (_,g) aIdx. let idx = map_option (ppExpr cvm) idx in 
                         Inl (VarRef g name (resolveIdx idx aIdx)))
                    (λ_. err STR ''Variable expected. Got MType.'')"
| "ppVarRef cvm (AST.VarRef _ _ (Some _)) = 
     usc STR ''next operation on variables''"

| "ppExpr cvm AST.ExprTimeOut = ExprTimeOut"
| "ppExpr cvm (AST.ExprConst c) = ExprConst c"

| "ppExpr cvm (AST.ExprBinOp bo l r) = 
     ExprBinOp (ppBinOp bo) (ppExpr cvm l) (ppExpr cvm r)"
| "ppExpr cvm (AST.ExprUnOp uo e) = 
     ExprUnOp (ppUnOp uo) (ppExpr cvm e)"
| "ppExpr cvm (AST.ExprCond c t f) = 
     ExprCond (ppExpr cvm c) (ppExpr cvm t) (ppExpr cvm f)"

| "ppExpr cvm (AST.ExprLen v) = 
     ExprLen (enforceChan (ppVarRef cvm v))"
| "ppExpr cvm (AST.ExprFull v) = 
     ExprFull (enforceChan (ppVarRef cvm v))"
| "ppExpr cvm (AST.ExprEmpty v) = 
     ExprEmpty (enforceChan (ppVarRef cvm v))"
(* the following two are special constructs in Promela for helping Partial Order Reductions
   we don't have such things (yet), so use simple negation *)
| "ppExpr cvm (AST.ExprNFull v) = 
     ExprUnOp UnOpNeg (ExprFull (enforceChan (ppVarRef cvm v)))"
| "ppExpr cvm (AST.ExprNEmpty v) = 
     ExprUnOp UnOpNeg (ExprEmpty (enforceChan (ppVarRef cvm v)))"

| "ppExpr cvm (AST.ExprVarRef v) = (
          let to_exp = λ_. ExprVarRef (liftChan (ppVarRef cvm v)) in
          case v of 
              AST.VarRef name None None ⇒ 
                 dealWithVar cvm name 
                     (λ_ _ _. to_exp())
                     (λ_ _ _. to_exp())
                     (λi. ExprMConst i name)
             | _ ⇒ to_exp())"

| "ppExpr cvm (AST.ExprPoll v es) = 
     ExprPoll (enforceChan (ppVarRef cvm v)) (map (ppRecvArg cvm) es) False"
| "ppExpr cvm (AST.ExprRndPoll v es) = 
     ExprPoll (enforceChan (ppVarRef cvm v)) (map (ppRecvArg cvm) es) True"

| "ppExpr cvm AST.ExprNP = usc STR ''ExprNP''"
| "ppExpr cvm (AST.ExprEnabled _) = usc STR ''ExprEnabled''"
| "ppExpr cvm (AST.ExprPC _) = usc STR ''ExprPC''"
| "ppExpr cvm (AST.ExprRemoteRef _ _ _) = usc STR ''ExprRemoteRef''"
| "ppExpr cvm (AST.ExprGetPrio _) = usc STR ''ExprGetPrio''"
| "ppExpr cvm (AST.ExprSetPrio _ _) = usc STR ''ExprSetPrio''"

| "ppRecvArg cvm (AST.RecvArgVar v) = (
          let to_ra = λ_. RecvArgVar (liftChan (ppVarRef cvm v)) in
          case v of 
              AST.VarRef name None None ⇒ 
                 dealWithVar cvm name 
                     (λ_ _ _. to_ra())
                     (λ_ _ _. to_ra())
                     (λi. RecvArgMConst i name)
             | _ ⇒ to_ra())"
| "ppRecvArg cvm (AST.RecvArgEval e) = RecvArgEval (ppExpr cvm e)"
| "ppRecvArg cvm (AST.RecvArgConst c) = RecvArgConst c"

primrec ppVarType :: "AST.varType ⇒ varType" where
  "ppVarType AST.VarTypeBit = VTBounded 0 1"
| "ppVarType AST.VarTypeBool = VTBounded 0 1"
| "ppVarType AST.VarTypeByte = VTBounded 0 255"
| "ppVarType AST.VarTypePid = VTBounded 0 255"
| "ppVarType AST.VarTypeShort = VTBounded (-(2^15)) ((2^15) - 1)"
| "ppVarType AST.VarTypeInt = VTBounded (-(2^31)) ((2^31) - 1)"
| "ppVarType AST.VarTypeMType = VTBounded 1 255"
| "ppVarType AST.VarTypeChan = VTChan"
| "ppVarType AST.VarTypeUnsigned = usc STR ''VarTypeUnsigned''"
| "ppVarType (AST.VarTypeCustom _) = usc STR ''VarTypeCustom''"

fun ppVarDecl 
  :: "var_data ⇒ varType ⇒ bool ⇒ AST.varDecl ⇒ var_data × varDecl" 
where
  "ppVarDecl (c,v,m,a) (VTBounded l h) g 
                       (AST.VarDeclNum name sze init) = (
     case lm.lookup name v of 
        Some _ ⇒ errv STR ''Duplicate variable '' name
       | _ ⇒ (case lm.lookup name a of 
               Some _ ⇒ errv
                         STR ''Variable name clashes with alias: '' name
               | _ ⇒ ((c, lm.update name (sze,g) v, m, a), 
                        VarDeclNum l h name sze 
                          (map_option (ppExpr (c,v,m,a)) init))))"
| "ppVarDecl _ _ g (AST.VarDeclNum name sze init) = 
     err STR ''Assiging num to non-num''"

| "ppVarDecl (c,v,m,a) VTChan g 
                       (AST.VarDeclChan name sze cap) = (
     let cap' = map_option (apsnd (map ppVarType)) cap in
     case lm.lookup name c of 
        Some _ ⇒ errv STR ''Duplicate variable '' name
       | _ ⇒ (case lm.lookup name a of 
               Some _ ⇒ errv 
                         STR ''Variable name clashes with alias: '' name
              | _ ⇒ ((lm.update name (sze, g) c, v, m, a), 
                     VarDeclChan name sze cap')))"
| "ppVarDecl _ _ g (AST.VarDeclChan name sze init) = 
     err STR ''Assiging chan to non-chan''"

| "ppVarDecl (c,v,m,a) (VTBounded l h) g 
                       (AST.VarDeclMType name sze init) = (
     let init = map_option (λmty. 
     case lm.lookup mty m of 
        None ⇒ errv STR ''Unknown MType '' mty
      | Some mval ⇒ ExprMConst mval mty) init in
            case lm.lookup name c of 
              Some _ ⇒ errv STR ''Duplicate variable '' name
             | _ ⇒ (case lm.lookup name a of Some _ 
                       ⇒ errv STR ''Variable name clashes with alias: '' name
             | _ ⇒ ((c, lm.update name (sze,g) v, m, a), 
                    VarDeclNum l h name sze init)))"

| "ppVarDecl _ _ g (AST.VarDeclMType name sze init) = 
     err STR ''Assiging num to non-num''"

| "ppVarDecl _ _ _ (AST.VarDeclUnsigned _ _ _) = 
     usc STR ''VarDeclUnsigned''"

definition ppProcVarDecl 
  :: "var_data ⇒ varType ⇒ bool ⇒ AST.varDecl ⇒ var_data × procVarDecl"
where
  "ppProcVarDecl cvm ty g v = (case ppVarDecl cvm ty g v of
       (cvm, VarDeclNum l h name sze init) ⇒ (cvm, ProcVarDeclNum l h name sze init)
     | (cvm, VarDeclChan name sze None) ⇒ (cvm, ProcVarDeclChan name sze)
     | _ ⇒ err STR ''Channel initilizations only allowed at the beginning of proctypes.'')"

fun ppProcArg 
  :: "var_data ⇒ varType ⇒ bool ⇒ AST.varDecl ⇒ var_data × procArg"
where
  "ppProcArg (c,v,m,a) (VTBounded l h) g 
                       (AST.VarDeclNum name None None) = (
     case lm.lookup name v of 
        Some _ ⇒ errv STR ''Duplicate variable '' name
      | _ ⇒ (case lm.lookup name a of 
               Some _ ⇒ errv 
                          STR ''Variable name clashes with alias: '' name
             | _ ⇒ ((c, lm.update name (None, g) v, m, a), 
                    ProcArg (VTBounded l h) name)))"
| "ppProcArg _ _ _ (AST.VarDeclNum _ _ _) = 
     err STR ''Invalid proctype arguments''"

| "ppProcArg (c,v,m,a) VTChan g 
                       (AST.VarDeclChan name None None) = (
     case lm.lookup name c of 
        Some _ ⇒ errv STR ''Duplicate variable '' name
      | _ ⇒ (case lm.lookup name a of 
               Some _ ⇒ errv
                          STR ''Variable name clashes with alias: '' name
             | _ ⇒ ((lm.update name (None, g) c, v, m, a), ProcArg VTChan name)))"
| "ppProcArg _ _ _ (AST.VarDeclChan _ _ _) = 
     err STR ''Invalid proctype arguments''"

| "ppProcArg (c,v,m,a) (VTBounded l h) g 
                       (AST.VarDeclMType name None None) = (
     case lm.lookup name v of 
        Some _ ⇒ errv STR ''Duplicate variable '' name
       | _ ⇒ (case lm.lookup name a of 
               Some _ ⇒ errv
                          STR ''Variable name clashes with alias: '' name
              | _ ⇒ ((c, lm.update name (None, g) v, m, a), 
                     ProcArg (VTBounded l h) name)))"
| "ppProcArg _ _ _ (AST.VarDeclMType _ _ _) = 
     err STR ''Invalid proctype arguments''"

| "ppProcArg _ _ _ (AST.VarDeclUnsigned _ _ _) = usc STR ''VarDeclUnsigned''"

text ‹Some preprocessing functions enrich the @{typ var_data} argument and hence return
a new updated one. When chaining multiple calls to such functions after another, we need to make
sure, the @{typ var_data} is passed accordingly. @{term cvm_fold} does exactly that for such a
function @{term g} and a list of nodes @{term ss}.›

definition cvm_fold where
  "cvm_fold g cvm ss = foldl (λ(cvm,ss) s. apsnd (λs'. ss@[s']) (g cvm s)) 
                             (cvm, []) ss"

lemma cvm_fold_cong[fundef_cong]:
  assumes "cvm = cvm'"
  and "stepss = stepss'"
  and "⋀x d. x ∈ set stepss ⟹ g d x = g' d x"
  shows "cvm_fold g cvm stepss = cvm_fold g' cvm' stepss'"
unfolding cvm_fold_def 
using assms
by (fastforce intro: foldl_cong split: prod.split)

fun liftDecl where
  "liftDecl f g cvm (AST.Decl vis t decls) = (
     let _ = the_warn vis STR ''Visibility in declarations not supported. Ignored.'' in
     let t = ppVarType t in
     cvm_fold (λcvm. f cvm t g) cvm decls)"

definition ppDecl 
  :: "bool ⇒ var_data ⇒ AST.decl ⇒ var_data × varDecl list" 
where
  "ppDecl = liftDecl ppVarDecl"

definition ppDeclProc 
  :: "var_data ⇒ AST.decl ⇒ var_data × procVarDecl list"
where
  "ppDeclProc = liftDecl ppProcVarDecl False"

definition ppDeclProcArg 
  :: "var_data ⇒ AST.decl ⇒ var_data × procArg list"
where
  "ppDeclProcArg = liftDecl ppProcArg False"

(* increment *)
definition incr :: "varRef ⇒ stmnt" where
  "incr v = StmntAssign v (ExprBinOp BinOpAdd (ExprVarRef v) (ExprConst 1))"

(* decrement *)
definition decr :: "varRef ⇒ stmnt" where
  "decr v = StmntAssign v (ExprBinOp BinOpSub (ExprVarRef v) (ExprConst 1))"

text ‹
   Transforms
     \verb+for (i : lb .. ub) steps+
   into 
\begin{verbatim} {
   i = lb;
   do
     :: i =< ub -> steps; i++
     :: else -> break
   od
} \end{verbatim}
›
definition forFromTo :: "varRef ⇒ expr ⇒ expr ⇒ step list ⇒ stmnt" where
  "forFromTo i lb ub steps = (
      let
        ― ‹‹i = lb››
        loop_pre = StepStmnt (StmntAssign i lb) None;
        ― ‹‹i ≤ ub››
        loop_cond = StepStmnt (StmntCond 
                                  (ExprBinOp BinOpLEq (ExprVarRef i) ub))
                                  None;
        ― ‹‹i++››
        loop_incr = StepStmnt (incr i) None;
        ― ‹‹i ≤ ub -> ...; i++››
        loop_body = loop_cond # steps @ [loop_incr];
        ― ‹‹else -> break››
        loop_abort = [StepStmnt StmntElse None, StepStmnt StmntBreak None];
        ― ‹‹do :: i ≤ ub -> ... :: else -> break od››
        loop = StepStmnt (StmntDo [loop_body, loop_abort]) None
      in
        StmntSeq [loop_pre, loop])"

text ‹
   Transforms (where @{term a} is an array with @{term N} entries)
     \verb+for (i in a) steps+
   into
\begin{verbatim}{
   i = 0;
   do
     :: i < N -> steps; i++
     :: else -> break
   od
}\end{verbatim}
›
definition forInArray :: "varRef ⇒ integer ⇒ step list ⇒ stmnt" where
  "forInArray i N steps = (
      let
        ― ‹‹i = 0››
        loop_pre = StepStmnt (StmntAssign i (ExprConst 0)) None;
        ― ‹‹i < N››
        loop_cond = StepStmnt (StmntCond 
                                 (ExprBinOp BinOpLe (ExprVarRef i) 
                                    (ExprConst N))) 
                                 None;
        ― ‹‹i++››
        loop_incr = StepStmnt (incr i) None;
        ― ‹‹i < N -> ...; i++››
        loop_body = loop_cond # steps @ [loop_incr];
        ― ‹‹else -> break››
        loop_abort = [StepStmnt StmntElse None, StepStmnt StmntBreak None];
        ― ‹‹do :: i < N -> ... :: else -> break od››
        loop = StepStmnt (StmntDo [loop_body, loop_abort]) None
      in
        StmntSeq [loop_pre, loop])"

text ‹
   Transforms (where @{term c} is a channel)
     \verb+for (msg in c) steps+
   into 
\begin{verbatim}{
   byte :tmp: = 0;
   do
     :: :tmp: < len(c) -> 
          c?msg; c!msg;
          steps; 
          :tmp:++
     :: else -> break
   od
}\end{verbatim}
›
definition forInChan :: "varRef ⇒ chanRef ⇒ step list ⇒ stmnt" where
  "forInChan msg c steps = (
      let  
        ― ‹‹byte :tmp: = 0››
        tmpStr = STR '':tmp:'';
        loop_pre = StepDecl 
                    [ProcVarDeclNum 0 255 tmpStr None (Some (ExprConst 0))];
        tmp = VarRef False tmpStr None; 
        ― ‹‹:tmp: < len(c)››
        loop_cond = StepStmnt (StmntCond 
                                 (ExprBinOp BinOpLe (ExprVarRef tmp) 
                                    (ExprLen c))) 
                              None;
        ― ‹‹:tmp:++››
        loop_incr = StepStmnt (incr tmp) None;
        ― ‹‹c?msg››
        recv = StepStmnt (StmntRecv c [RecvArgVar msg] False True) None;
        ― ‹‹c!msg››
        send = StepStmnt (StmntSend c [ExprVarRef msg] False) None;
        ― ‹‹:tmp: < len(c) -> c?msg; c!msg; ...; :tmp:++››
        loop_body = [loop_cond, recv, send] @ steps @ [loop_incr];
        ― ‹‹else -> break››
        loop_abort = [StepStmnt StmntElse None, StepStmnt StmntBreak None];
        ― ‹‹do :: :tmp: < len(c) -> ... :: else -> break od››
        loop = StepStmnt (StmntDo [loop_body, loop_abort]) None
      in
        StmntSeq [loop_pre, loop])"

text ‹
   Transforms
     \verb+select (i : lb .. ub)+
   into 
\begin{verbatim}{
   i = lb;
   do
     :: i < ub -> i++
     :: break
   od
}\end{verbatim}
›
definition select :: "varRef ⇒ expr ⇒ expr ⇒ stmnt" where
  "select i lb ub = (
      let
        ― ‹‹i = lb››
        pre = StepStmnt (StmntAssign i lb) None;
        ― ‹‹i < ub››
        cond = StepStmnt (StmntCond (ExprBinOp BinOpLe (ExprVarRef i) ub)) 
                         None;
        ― ‹‹i++››
        incr = StepStmnt (incr i) None;
        ― ‹‹i < ub -> i++››
        loop_body = [cond, incr];
        ― ‹‹break››
        loop_abort = [StepStmnt StmntBreak None];
        ― ‹‹do :: i < ub -> ... :: break od››
        loop = StepStmnt (StmntDo [loop_body, loop_abort]) None
      in
        StmntSeq [pre, loop])"

type_synonym inlines = 
  "(String.literal, String.literal list × (var_data ⇒ var_data × step list)) lm"
type_synonym stmnt_data = 
  " bool × varDecl list × inlines × var_data"

fun ppStep :: "stmnt_data ⇒ AST.step ⇒ stmnt_data * step"
and ppStmnt :: "stmnt_data ⇒ AST.stmnt ⇒ stmnt_data * stmnt"
where
  "ppStep cvm (AST.StepStmnt s u) = (
     let (cvm', s') = ppStmnt cvm s in
     case u of None ⇒ (cvm', StepStmnt s' None) 
             | Some u ⇒ let (cvm'',u') = ppStmnt cvm' u in
                            (cvm'', StepStmnt s' (Some u')))"
| "ppStep (False, ps, i, cvm) (AST.StepDecl d) = 
     map_prod (λcvm. (False, ps, i, cvm)) StepDecl (ppDeclProc cvm d)"
| "ppStep (True, ps, i, cvm) (AST.StepDecl d) = (
             let (cvm', ps') = ppDecl False cvm d 
             in ((True, ps@ps', i, cvm'), StepSkip))"
| "ppStep (_,cvm) (AST.StepXR _) = 
     with_warn STR ''StepXR not supported. Ignored.'' ((False,cvm), StepSkip)"
| "ppStep (_,cvm) (AST.StepXS _) = 
     with_warn STR ''StepXS not supported. Ignored.'' ((False,cvm), StepSkip)"

| "ppStmnt (_,cvm) (AST.StmntBreak) = ((False,cvm), StmntBreak)"
| "ppStmnt (_,cvm) (AST.StmntElse) = ((False,cvm), StmntElse)"
| "ppStmnt (_,cvm) (AST.StmntGoTo l) = ((False,cvm), StmntGoTo l)"
| "ppStmnt (_,cvm) (AST.StmntLabeled l s) = 
     apsnd (StmntLabeled l) (ppStmnt (False,cvm) s)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntCond e) = 
     ((False,ps,i,cvm), StmntCond (ppExpr cvm e))"
| "ppStmnt (_,ps,i,cvm) (AST.StmntAssert e) = 
     ((False,ps,i,cvm), StmntAssert (ppExpr cvm e))"
| "ppStmnt (_,ps,i,cvm) (AST.StmntAssign v e) = 
     ((False,ps,i,cvm), StmntAssign (liftChan (ppVarRef cvm v)) (ppExpr cvm e))"
| "ppStmnt (_,ps,i,cvm) (AST.StmntSend v es) = 
     ((False,ps,i,cvm), StmntSend (enforceChan (ppVarRef cvm v)) 
                                  (map (ppExpr cvm) es) False)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntSortSend v es) = 
     ((False,ps,i,cvm), StmntSend (enforceChan (ppVarRef cvm v)) 
                                  (map (ppExpr cvm) es) True)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRecv v rs) = 
     ((False,ps,i,cvm), StmntRecv (enforceChan (ppVarRef cvm v)) 
                                  (map (ppRecvArg cvm) rs) False True)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRecvX v rs) = 
     ((False,ps,i,cvm), StmntRecv (enforceChan (ppVarRef cvm v)) 
                                  (map (ppRecvArg cvm) rs) False False)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRndRecv v rs) = 
     ((False,ps,i,cvm), StmntRecv (enforceChan (ppVarRef cvm v)) 
                                  (map (ppRecvArg cvm) rs) True True)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRndRecvX v rs) = 
     ((False,ps,i,cvm), StmntRecv (enforceChan (ppVarRef cvm v)) 
                                  (map (ppRecvArg cvm) rs) True False)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRun n es p) = ( 
     let _ = the_warn p STR ''Priorities for 'run' not supported. Ignored.'' in
    ((False,ps,i,cvm), StmntRun n (map (ppExpr cvm) es)))"
| "ppStmnt (_,cvm) (AST.StmntSeq ss) = 
     apsnd StmntSeq (cvm_fold ppStep (False,cvm) ss)"
| "ppStmnt (_,cvm) (AST.StmntAtomic ss) = 
     apsnd StmntAtomic (cvm_fold ppStep (False,cvm) ss)"
| "ppStmnt (_,cvm) (AST.StmntIf sss) = 
     apsnd StmntIf (cvm_fold (cvm_fold ppStep) (False,cvm) sss)"
| "ppStmnt (_,cvm) (AST.StmntDo sss) = 
     apsnd StmntDo (cvm_fold (cvm_fold ppStep) (False,cvm) sss)"

(* Replace i++ and i-- by i = i + 1 / i = i - 1 *)
| "ppStmnt (_,ps,i,cvm) (AST.StmntIncr v) = 
     ((False,ps,i,cvm), incr (liftChan (ppVarRef cvm v)))"
| "ppStmnt (_,ps,i,cvm) (AST.StmntDecr v) = 
     ((False,ps,i,cvm), decr (liftChan (ppVarRef cvm v)))"

| "ppStmnt (_,cvm) (AST.StmntPrintF _ _) = 
     with_warn STR ''PrintF ignored'' ((False,cvm), StmntSkip)"
| "ppStmnt (_,cvm) (AST.StmntPrintM _) = 
     with_warn STR ''PrintM ignored'' ((False,cvm), StmntSkip)"

| "ppStmnt (_,ps,inl,cvm) (AST.StmntFor 
                              (AST.RangeFromTo i lb ub) 
                              steps) = (
     let 
       i = liftChan (ppVarRef cvm i);
       (lb,ub) = (ppExpr cvm lb, ppExpr cvm ub)
     in
       apsnd (forFromTo i lb ub) (cvm_fold ppStep (False,ps,inl,cvm) steps))"
| "ppStmnt (_,ps,inl,cvm) (AST.StmntFor 
                              (AST.RangeIn i v) 
                              steps) = (
     let
        i = liftChan (ppVarRef cvm i);
        (cvm',steps) = cvm_fold ppStep (False,ps,inl,cvm) steps
     in
        case ppVarRef cvm v of
         Inr c ⇒ (cvm', forInChan i c steps)
       | Inl (VarRef _ _ (Some _)) ⇒ err STR ''Iterating over array-member.''
       | Inl (VarRef _ name None) ⇒ (
             let (_,v,_) = cvm in
             case fst (the (lm.lookup name v)) of
              None ⇒ err STR ''Iterating over non-array variable.''
            | Some N ⇒ (cvm', forInArray i N steps)))"

| "ppStmnt (_,ps,inl,cvm) (AST.StmntSelect 
                              (AST.RangeFromTo i lb ub)) = (
     let
       i = liftChan (ppVarRef cvm i);
       (lb, ub) = (ppExpr cvm lb, ppExpr cvm ub)
     in
       ((False,ps,inl,cvm), select i lb ub))"
| "ppStmnt (_,cvm) (AST.StmntSelect (AST.RangeIn _ _)) = 
     err STR ''\"in\" not allowed in select''"

| "ppStmnt (_,ps,inl,cvm) (AST.StmntCall macro args) = (
     let 
       args = map (liftChan ∘ ppVarRef cvm) args;
       (c,v,m,a) = cvm
     in
       case lm.lookup macro inl of
        None ⇒ errv STR ''Calling unknown macro '' macro
      | Some (names,sF) ⇒
          if length names ≠ length args then 
             (err STR ''Called macro with wrong number of arguments.'') 
          else
             let a' = foldl (λa (k,v). lm.update k v a) a (zip names args) in
             let ((c,v,m,_),steps) = sF (c,v,m,a') in
             ((False,ps,inl,c,v,m,a), StmntSeq steps))"
         
| "ppStmnt cvm (AST.StmntDStep _) = usc STR ''StmntDStep''"

fun ppModule 
  :: "var_data × inlines ⇒ AST.module 
      ⇒ var_data × inlines × (varDecl list + proc + ltl)"
where
  "ppModule (cvm, inl) (AST.ProcType act name args prio prov steps) = (
     let 
        _ = the_warn prio STR ''Priorities for procs not supported. Ignored.'';
        _ = the_warn prov STR ''Priov (??) for procs not supported. Ignored.'';
        (cvm', args) = cvm_fold ppDeclProcArg cvm args;
        ((_, vars, _, _), steps) = cvm_fold ppStep (True,[],inl,cvm') steps
     in
        (cvm, inl, Inr (Inl (ProcType act name (concat args) vars steps))))"

| "ppModule (cvm,inl) (AST.Init prio steps) = (
     let _ = the_warn prio STR ''Priorities for procs not supported. Ignored.'' in
     let ((_, vars, _, _), steps) = cvm_fold ppStep (True,[],inl,cvm) steps in
     (cvm, inl, Inr (Inl (Init vars steps))))"

| "ppModule (cvm,inl) (AST.Ltl name formula) = 
     (cvm, inl, Inr (Inr (name, formula)))"

| "ppModule (cvm,inl) (AST.ModuDecl decl) = 
     apsnd (λds. (inl,Inl ds)) (ppDecl True cvm decl)"

| "ppModule (cvm,inl) (AST.MType mtys) = (
     let (c,v,m,a) = cvm in
     let num = integer_of_nat (lm.size m) + 1 in
     let (m',_) = foldr (λmty (m,num). 
                    let m' = lm.update mty num m 
                    in (m',num+1)) mtys (m,num)
     in
         ((c,v,m',a), inl, Inl []))"

| "ppModule (cvm,inl) (AST.Inline name args steps) = (
     let stepF = (λcvm. let ((_,_,_,cvm),steps) = 
                          cvm_fold ppStep (False,[],inl,cvm) steps 
                        in (cvm,steps))
     in let inl = lm.update name (args, stepF) inl
     in (cvm,inl, Inl[]))"

| "ppModule cvm (AST.DProcType _ _ _ _ _ _) = usc STR ''DProcType''"
| "ppModule cvm (AST.Never _) = usc STR ''Never''"
| "ppModule cvm (AST.Trace _) = usc STR ''Trace''"
| "ppModule cvm (AST.NoTrace _) = usc STR ''NoTrace''"
| "ppModule cvm (AST.TypeDef _ _) = usc STR ''TypeDef''"

definition preprocess :: "AST.module list ⇒ promela" where
  "preprocess ms = (
     let 
       dflt_vars = [(STR ''_pid'', (None, False)), 
                    (STR ''__assert__'', (None, True)), 
                    (STR ''_'', (None, True))];
       cvm = (lm.empty(), lm.to_map dflt_vars, lm.empty(), lm.empty());
       (_,_,pr) = (foldl (λ(cvm,inl,vs,ps,ls) m.
                            let (cvm', inl', m') = ppModule (cvm,inl) m in
                            case m' of
                              Inl v ⇒ (cvm',inl',vs@v,ps,ls)
                            | Inr (Inl p) ⇒ (cvm',inl',vs,ps@[p],ls)
                            | Inr (Inr l) ⇒ (cvm',inl',vs,ps,ls@[l])) 
                          (cvm, lm.empty(),[],[],[]) ms)
       in
         pr)"

fun extractLTL
  :: "AST.module ⇒ ltl option"
where
  "extractLTL (AST.Ltl name formula) = Some (name, formula)"
| "extractLTL _ = None"

primrec extractLTLs
  :: "AST.module list ⇒ (String.literal, String.literal) lm"
where
  "extractLTLs [] = lm.empty()"
| "extractLTLs (m#ms) = (case extractLTL m of 
                           None ⇒ extractLTLs ms
                         | Some (n,f) ⇒ lm.update n f (extractLTLs ms))"

definition lookupLTL
  :: "AST.module list ⇒ String.literal ⇒ String.literal option"
  where "lookupLTL ast k = lm.lookup k (extractLTLs ast)"

subsection ‹The transition system›

text ‹
  The edges in our transition system consist of a condition (evaluated under the current environment) and an effect (modifying the current environment). 
  Further they may be atomic, \ie a whole row of such edges is taken before yielding a new state. 
  Additionally, they carry a priority: the edges are checked from highest to lowest priority, and if one edge on a higher level can be taken, the lower levels are ignored.

  The states of the system do not carry any information.
›