Formalization of CoLiS language

Syntax

module Syntax
  use import list.List
  use import mystrings.String

  type svar = string
  type lvar = string

  type term =
    | TTrue                         (*                  | true                  *)
    | TFalse                        (*                  | false                 *)
    | TFatal                        (*                  | fatal                 *)
    | TReturn term                  (*                  | return t              *)
    | TExit term                    (*                  | exit t                *)
    | TAsString svar sexpr          (*       assignment | x := (string) t       *)
    | TAsList lvar lexpr            (*  list assignment | x :=  (list)  l       *)
    | TSeq term term                (*         sequence | t ; t                 *)
    | TIf term term term            (*      conditional | if t then t else t fi *)
    | TFor svar lexpr term          (*         for loop | for x in l do t done  *)
    | TDoWhile term term            (*    do-while loop | do t while t done     *)
    | TProcess term                 (*      parentheses | ( t )                 *)
    | TCall lexpr                   (*                  |                       *)
    | TShift                        (*                  |                       *)
    | TPipe term term               (*                  | t | t                 *)

  with sexpr = list sfrag

  with sfrag =
    | SLiteral string               (*          literal | "foobar"              *)
    | SVar svar                     (*  variable:string | "$var"                *)
    | SArg int                      (*  argument:string | "$n", n integer       *)
    | SProcess term                 (* processus:string | "$(t)"                *)

  with lexpr = list lfrag

  with lfrag =
    | LSingleton sexpr
    | LSplit sexpr
    | LVar lvar                     (*    variable:list | $var                  *)

Program

  type program =
    { p_sdecl  : list svar ;
      p_ldecl  : list lvar ;
      p_pdecls : list (string, term) ;
      p_term   : term }
end

Common semantic definitions

module CommonSemantics
  use import bool.Bool
  use import option.Option
  use import list.List
  use import mystrings.String
  use HighOrd
  use import Syntax

Behaviours

  type behaviour =
    | BNormal bool
    | BFatal
    | BReturn bool
    | BExit bool

Helpers to deal with options composition

  function bcompose (b: 'a) (beta: option 'a) : 'a =
    match beta with
    | None    -> b
    | Some b' -> b'
    end

  function bocompose (beta beta': option 'a) : option 'a =
    match beta' with
    | None -> beta
    | _    -> beta'
    end

  function getsome (beta: option 'a) (d: 'a) : 'a =
    match beta with
    | None   -> d
    | Some c -> c
    end

Context

  type filesystem = unit

  type senv = svar -> string
  type lenv = lvar -> list string
  type penv = string -> option term

  type context = {
    c_fs    : filesystem  ;
    c_senv  : senv        ;
    c_lenv  : lenv        ;
    c_args  : list string ;
    c_input : string      ;
    c_penv  : penv        ;
  }

  constant empty_context : context = {
    c_fs = () ;
    c_senv = \_. empty_string ;
    c_lenv = \_. Nil ;
    c_args = Nil ;
    c_input = empty_string ;
    c_penv = \_. None
  }

  function fun_upd (f: 'a -> 'b) (x: 'a) (v: 'b) : 'a -> 'b = \y. if y = x then v else f y

  function update_senv (g: context) (xs: svar) (sigma: string) : context =
    { g with c_senv = fun_upd g.c_senv xs sigma }

  function update_lenv (g: context) (xl: lvar) (lambda: list string) : context =
    { g with c_lenv = fun_upd g.c_lenv xl lambda }

  function update_penv (g: context) (f: string) (t: term) : context =
    { g with c_penv = fun_upd g.c_penv f (Some t) }

Builtins

  function eval_builtin string context : (string, behaviour, context)
  (* Do not give its body. *)
end

Semantics

module Semantics
  use import bool.Bool
  use import int.Int
  use import list.List
  use import list.Append
  use import list.Nth
  use import option.Option
  use import mystrings.String

  use HighOrd
  use import Syntax
  use import CommonSemantics

Semantics for term evaluation

  inductive eval_term term context string behaviour context =
    (* Literals *)

    | EvalT_True  : forall gamma.
      eval_term TTrue gamma empty_string (BNormal True) gamma

    | EvalT_False : forall gamma.
      eval_term TFalse gamma empty_string (BNormal False) gamma

    | EvalT_Fatal : forall gamma.
      eval_term TFatal gamma empty_string BFatal gamma

    (* Return, Exit *)

    | EvalT_Return : forall t gamma sigma b gamma'.
      eval_term t gamma sigma b gamma' ->
      eval_term (TReturn t) gamma sigma (match b with BNormal b' -> BReturn b' | _ -> b end) gamma'

    | EvalT_Exit : forall t gamma sigma b gamma'.
      eval_term t gamma sigma b gamma' ->
      eval_term (TExit t) gamma sigma (match b with BNormal b' -> BExit b' | _ -> b end) gamma'

    (* Assign *)

    | EvalT_AsString : forall s gamma sigma beta gamma' gamma'' x_s.
      eval_sexpr s gamma sigma beta gamma' ->
      gamma'' = update_senv gamma' x_s sigma ->
      eval_term (TAsString x_s s) gamma empty_string (if beta then BNormal True else BFatal) gamma''

    | EvalT_AsList : forall l gamma lambda beta gamma' x_l gamma''.
      eval_lexpr l gamma lambda beta gamma' ->
      gamma'' = update_lenv gamma' x_l lambda ->
      eval_term (TAsList x_l l) gamma empty_string (if beta then BNormal True else BFatal) gamma''

    (* Sequence *)

    | EvalT_Seq_Normal : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sigma_2 b_2 gamma_2.
      eval_term t_1 gamma sigma_1 (BNormal b_1) gamma_1 ->
      eval_term t_2 gamma_1 sigma_2 b_2 gamma_2 ->
      eval_term (TSeq t_1 t_2) gamma (concat sigma_1 sigma_2) b_2 gamma_2

    | EvalT_Seq_Error : forall t_1 gamma sigma_1 b_1 gamma_1 t_2.
      eval_term t_1 gamma sigma_1 b_1 gamma_1 ->
      (match b_1 with BNormal _ -> false | _ -> true end) ->
      eval_term (TSeq t_1 t_2) gamma sigma_1 b_1 gamma_1

    (* Conditional *)

    | EvalT_If_True : forall t_1 gamma sigma_1 gamma_1 t_2 sigma_2 b_2 gamma_2 t_3.
      eval_term t_1 gamma sigma_1 (BNormal True) gamma_1 ->
      eval_term t_2 gamma_1 sigma_2 b_2 gamma_2 ->
      eval_term (TIf t_1 t_2 t_3) gamma (concat sigma_1 sigma_2) b_2 gamma_2

    | EvalT_If_False : forall t_1 gamma sigma_1 b_1 gamma_1 t_3 sigma_3 b_3 gamma_3 t_2.
      eval_term t_1 gamma sigma_1 b_1 gamma_1 ->
      (match b_1 with BNormal False | BFatal -> true | _ -> false end) ->
      eval_term t_3 gamma_1 sigma_3 b_3 gamma_3 ->
      eval_term (TIf t_1 t_2 t_3) gamma (concat sigma_1 sigma_3) b_3 gamma_3

    | EvalT_If_Transmit : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 t_3.
      eval_term t_1 gamma sigma_1 b_1 gamma_1 ->
      (match b_1 with BReturn _ | BExit _ -> true | _ -> false end) ->
      eval_term (TIf t_1 t_2 t_3) gamma sigma_1 b_1 gamma_1

    (* For loop *)

    | EvalT_For : forall l gamma lambda b gamma' x_l t gamma'' sigma b'.
      eval_lexpr l gamma lambda b gamma' ->
      eval_term_tfor x_l lambda t gamma' sigma b' gamma'' ->
      eval_term (TFor x_l l t) gamma sigma b' gamma''

    (* Do-While loop *)

    | EvalT_DoWhile_True : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sigma_2 gamma_2 sigma_3 b_3 gamma_3.
      eval_term t_1 gamma sigma_1 (BNormal b_1) gamma_1 ->
      eval_term t_2 gamma_1 sigma_2 (BNormal True) gamma_2 ->
      eval_term (TDoWhile t_1 t_2) gamma_2 sigma_3 b_3 gamma_3 ->
      eval_term (TDoWhile t_1 t_2) gamma (concat (concat sigma_1 sigma_2) sigma_3) b_3 gamma_3

    | EvalT_DoWhile_False : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sigma_2 b_2 gamma_2.
      eval_term t_1 gamma sigma_1 (BNormal b_1) gamma_1 ->
      eval_term t_2 gamma_1 sigma_2 b_2 gamma_2 ->
      (match b_2 with BNormal False | BFatal -> true | _ -> false end) ->
      eval_term (TDoWhile t_1 t_2) gamma (concat sigma_1 sigma_2) (BNormal b_1) gamma_2

    | EvalT_DoWhile_Transmit_Body : forall t_1 gamma sigma_1 b_1 gamma_1 t_2.
      eval_term t_1 gamma sigma_1 b_1 gamma_1 ->
      (match b_1 with BNormal _ -> false | _ -> true end) ->
      eval_term (TDoWhile t_1 t_2) gamma sigma_1 b_1 gamma_1

    | EvalT_DoWhile_Transmit_Cond : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sigma_2 b_2 gamma_2.
      eval_term t_1 gamma sigma_1 (BNormal b_1) gamma_1 ->
      eval_term t_2 gamma_1 sigma_2 b_2 gamma_2 ->
      (match b_2 with BExit _ | BReturn _ -> true | _ -> false end) ->
      eval_term (TDoWhile t_1 t_2) gamma (concat sigma_1 sigma_2) b_2 gamma_2

    (* Process *)

    | EvalT_Process : forall t gamma sigma b gamma'.
      eval_term t gamma sigma b gamma' ->
      eval_term (TProcess t) gamma sigma
        (match b with BNormal True | BReturn True | BExit True -> BNormal True | _ -> BFatal end)
        {gamma with c_fs = gamma'.c_fs ; c_input = gamma'.c_input}

    (* Call *)

    | EvalT_Call : forall s gamma l beta gamma' sigma b' gamma''.
      eval_lexpr s gamma l beta gamma' -> (* beta is ignored *)
      eval_term_tcall l gamma' sigma b' gamma'' ->
      eval_term (TCall s) gamma sigma b' gamma''

    (* Shift *)

    (* Not the nicest way to write it, but this way helps Why3. *)

    | EvalT_Shift_Nil : forall f se le i fe.
      eval_term TShift {c_fs = f ; c_senv = se ; c_lenv = le ; c_args = Nil ; c_input = i ; c_penv = fe }
        empty_string (BNormal False) {c_fs = f ; c_senv = se ; c_lenv = le ; c_args = Nil ; c_input = i ; c_penv = fe }

    | EvalT_Shift_NonNil : forall f se le ah at i fe.
      eval_term TShift {c_fs = f ; c_senv = se ; c_lenv = le ; c_args = Cons ah at ; c_input = i ; c_penv = fe }
        empty_string (BNormal True) {c_fs = f ; c_senv = se ; c_lenv = le ; c_args = at ; c_input = i ; c_penv = fe }

    (* Pipe *)

    | EvalT_Pipe : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sigma_2 b_2 gamma_2.
      eval_term t_1 gamma sigma_1 b_1 gamma_1 -> (* b_1 ignored *)
      eval_term t_2 {gamma_1 with c_input = sigma_1} sigma_2 b_2 gamma_2 ->
      eval_term (TPipe t_1 t_2) gamma sigma_2 b_2 {gamma_2 with c_input = gamma_1.c_input}

Semantics for TCall evaluation with a clean list

  with eval_term_tcall (list string) context string behaviour context =

    | EvalT_Call_Nil : forall gamma.
      eval_term_tcall Nil gamma empty_string (BNormal True) gamma

    | EvalT_Call_NonNil_True : forall gamma h t sigma b gamma' f gamma''.
      gamma.c_penv h = Some f ->
      eval_term f {gamma with c_args = t} sigma b gamma' ->
      (match b with BNormal True | BReturn True -> true | _ -> false end) ->
      gamma'' = {gamma' with c_args = gamma.c_args} ->
      eval_term_tcall (Cons h t) gamma sigma (BNormal True) gamma''

    | EvalT_Call_NonNil_False : forall gamma h t sigma b gamma' f gamma''.
      gamma.c_penv h = Some f ->
      eval_term f {gamma with c_args = t} sigma b gamma' ->
      (match b with BNormal False | BFatal | BReturn False -> true | _ -> false end) ->
      gamma'' = {gamma' with c_args = gamma.c_args} ->
      eval_term_tcall (Cons h t) gamma sigma BFatal gamma''

    | EvalT_Call_NonNil_Transmit : forall gamma h t sigma b gamma' f gamma''.
      gamma.c_penv h = Some f ->
      eval_term f {gamma with c_args = t} sigma (BExit b) gamma' ->
      gamma'' = {gamma' with c_args = gamma.c_args} ->
      eval_term_tcall (Cons h t) gamma sigma (BExit b) gamma''

    | EvalT_Call_NonNil_Builtin_True : forall gamma h t sigma b gamma'.
      gamma.c_penv h = None ->
      eval_builtin h {gamma with c_args = t} = (sigma, b, gamma') ->
      (match b with BNormal True | BReturn True -> true | _ -> false end) ->
      eval_term_tcall (Cons h t) gamma sigma (BNormal True) {gamma' with c_args = gamma.c_args}

    | EvalT_Call_NonNil_Builtin_False : forall gamma h t sigma b gamma'.
      gamma.c_penv h = None ->
      eval_builtin h {gamma with c_args = t} = (sigma, b, gamma') ->
      (match b with BNormal False | BFatal | BReturn False -> true | _ -> false end) ->
      eval_term_tcall (Cons h t) gamma sigma BFatal {gamma' with c_args = gamma.c_args}

    | EvalT_Call_NonNil_Builtin_Transmit : forall gamma h t sigma b gamma'.
      gamma.c_penv h = None ->
      eval_builtin h {gamma with c_args = t} = (sigma, BExit b, gamma') ->
      eval_term_tcall (Cons h t) gamma sigma (BExit b) {gamma' with c_args = gamma.c_args}

Semantics for TFor evaluation with a clean list

  with eval_term_tfor svar (list string) term context string behaviour context =

    | EvalT_For_Nil : forall x_s t gamma.
      eval_term_tfor x_s Nil t gamma empty_string (BNormal True) gamma

    | EvalT_For_Cons_Nil : forall t gamma x_s sigma sigma' b gamma'.
      eval_term t (update_senv gamma x_s sigma) sigma' b gamma' ->
      eval_term_tfor x_s (Cons sigma Nil) t gamma sigma' b gamma'

    | EvalT_For_Cons_Cons : forall t gamma x_s sigma_1 sigma b gamma' sigma_2 l sigma' b' gamma''.
      eval_term t (update_senv gamma x_s sigma_1) sigma (BNormal b) gamma' ->
      eval_term_tfor x_s (Cons sigma_2 l) t gamma' sigma' b' gamma'' ->
      eval_term_tfor x_s (Cons sigma_1 (Cons sigma_2 l)) t gamma (concat sigma sigma') b' gamma''

    | EvalT_For_Cons_Cons_Transmit : forall t gamma x_s sigma_1 sigma_2 l sigma b gamma' .
      eval_term t (update_senv gamma x_s sigma_1) sigma b gamma' ->
      (match b with BNormal _ -> false | _ -> true end) ->
      eval_term_tfor x_s (Cons sigma_1 (Cons sigma_2 l)) t gamma sigma b gamma'

Semantics for string evaluation

  with eval_sexpr sexpr context string bool context =

    | EvalSE : forall s gamma sigma beta gamma'.
      eval_sexpr_opt s gamma sigma beta gamma' ->
      eval_sexpr s gamma sigma (match beta with Some False -> False | _ -> True end) gamma'

  with eval_sexpr_opt sexpr context string (option bool) context =

    | EvalSE_Nil : forall gamma.
      eval_sexpr_opt Nil gamma empty_string None gamma

    | EvalSE_Cons : forall f_s gamma sigma beta gamma' s sigma' beta' gamma''.
      eval_sfrag_opt f_s gamma sigma beta gamma' ->
      eval_sexpr_opt s gamma' sigma' beta' gamma'' ->
      eval_sexpr_opt (Cons f_s s) gamma (concat sigma sigma') (bocompose beta beta') gamma''

  with eval_sfrag_opt sfrag context string (option bool) context =

    | EvalSE_String : forall sigma gamma.
      eval_sfrag_opt (SLiteral sigma) gamma sigma None gamma

    | EvalSE_Var : forall x_s gamma.
      eval_sfrag_opt (SVar x_s) gamma (gamma.c_senv x_s) None gamma

    | EvalSE_Arg : forall n gamma.
      eval_sfrag_opt (SArg n) gamma
        (match nth n gamma.c_args with None -> empty_string | Some sigma -> sigma end)
	None gamma

    | EvalSE_Process : forall t gamma sigma b gamma'.
      eval_term t gamma sigma b gamma' ->
      eval_sfrag_opt (SProcess t) gamma sigma
        (Some (match b with BNormal True | BReturn True | BExit True -> True | _ -> False end))
        {gamma with c_fs = gamma'.c_fs ; c_input = gamma'.c_input}

Semantics for list evaluation

  with eval_lexpr lexpr context (list string) bool context =

    | EvalLE : forall l gamma lambda beta gamma'.
      eval_lexpr_opt l gamma lambda beta gamma' ->
      eval_lexpr l gamma lambda
        (match beta with Some False -> False | _ -> True end)
	gamma'

  with eval_lexpr_opt lexpr context (list string) (option bool) context =

    | EvalLE_Nil : forall gamma.
      eval_lexpr_opt Nil gamma Nil None gamma

    | EvalLE_Cons : forall f_l l gamma gamma' gamma'' lambda lambda' beta beta'.
      eval_lfrag_opt f_l gamma lambda beta gamma' ->
      eval_lexpr_opt l gamma' lambda' beta' gamma'' ->
      eval_lexpr_opt (Cons f_l l) gamma (lambda ++ lambda') (bocompose beta beta') gamma''

  with eval_lfrag_opt lfrag context (list string) (option bool) context =

    | EvalLF_Singleton : forall s gamma sigma beta gamma'.
      eval_sexpr_opt s gamma sigma beta gamma' ->
      eval_lfrag_opt (LSingleton s) gamma (Cons sigma Nil) beta gamma'

    | EvalLF_Split : forall s gamma sigma beta gamma'.
      eval_sexpr_opt s gamma sigma beta gamma' ->
      eval_lfrag_opt (LSplit s) gamma (split sigma) beta gamma'

    | EvalLF_Var : forall x_l gamma.
      eval_lfrag_opt (LVar x_l) gamma (gamma.c_lenv x_l) None gamma

end

Semantics with skeleton

module SemanticsWithSkeleton
  use import bool.Bool
  use import int.Int
  use import list.List
  use import list.Append
  use import list.Nth
  use import option.Option
  use import mystrings.String
  use import skeleton.Skeleton

  use HighOrd
  use import Syntax
  use import CommonSemantics

Semantics for term evaluation

  inductive eval_term term context string behaviour context skeleton =
    (* Literals *)

    | EvalT_True : forall gamma.
      eval_term TTrue gamma empty_string (BNormal True) gamma S0

    | EvalT_False : forall gamma.
      eval_term TFalse gamma empty_string (BNormal False) gamma S0

    | EvalT_Fatal : forall gamma.
      eval_term TFatal gamma empty_string BFatal gamma S0

    (* Return, Exit *)

    | EvalT_Return : forall t gamma sigma b gamma' sk.
      eval_term t gamma sigma b gamma' sk ->
      eval_term (TReturn t) gamma sigma (match b with BNormal b' -> BReturn b' | _ -> b end) gamma' (S1 sk)

    | EvalT_Exit : forall t gamma sigma b gamma' sk.
      eval_term t gamma sigma b gamma' sk ->
      eval_term (TExit t) gamma sigma (match b with BNormal b' -> BExit b' | _ -> b end) gamma' (S1 sk)

    (* Assign *)

    | EvalT_AsString : forall s gamma sigma beta gamma' gamma'' x_s sk.
      eval_sexpr s gamma sigma beta gamma' sk ->
      gamma'' = update_senv gamma' x_s sigma ->
      eval_term (TAsString x_s s) gamma empty_string (if beta then BNormal True else BFatal) gamma'' (S1 sk)

    | EvalT_AsList : forall l gamma lambda beta gamma' x_l gamma'' sk.
      eval_lexpr l gamma lambda beta gamma' sk ->
      gamma'' = update_lenv gamma' x_l lambda ->
      eval_term (TAsList x_l l) gamma empty_string (if beta then BNormal True else BFatal) gamma'' (S1 sk)

    (* Sequence *)

    | EvalT_Seq_Normal : forall t1 g s1 b1 g1 t2 s2 b2 g2 sk1 sk2.
      eval_term t1 g s1 (BNormal b1) g1 sk1 ->
      eval_term t2 g1 s2 b2 g2 sk2 ->
      eval_term (TSeq t1 t2) g (concat s1 s2) b2 g2 (S2 sk1 sk2)

    | EvalT_Seq_Error : forall t1 g s1 b1 g1 t2 sk.
      eval_term t1 g s1 b1 g1 sk ->
      (match b1 with BNormal _ -> false | _ -> true end) ->
      eval_term (TSeq t1 t2) g s1 b1 g1 (S1 sk)

    (* Conditional *)

    | EvalT_If_True : forall t1 g s1 g1 t2 s2 b2 g2 t3 sk1 sk2.
      eval_term t1 g s1 (BNormal True) g1 sk1 ->
      eval_term t2 g1 s2 b2 g2 sk2 ->
      eval_term (TIf t1 t2 t3) g (concat s1 s2) b2 g2 (S2 sk1 sk2)

    | EvalT_If_False : forall t1 g s1 b1 g1 t3 s3 b3 g3 t2 sk1 sk3.
      eval_term t1 g s1 b1 g1 sk1 ->
      (match b1 with BNormal False | BFatal -> true | _ -> false end) ->
      eval_term t3 g1 s3 b3 g3 sk3 ->
      eval_term (TIf t1 t2 t3) g (concat s1 s3) b3 g3 (S2 sk1 sk3)

    | EvalT_If_Transmit : forall t1 g s1 b1 g1 t2 t3 sk1.
      eval_term t1 g s1 b1 g1 sk1 ->
      (match b1 with BReturn _ | BExit _ -> true | _ -> false end) ->
      eval_term (TIf t1 t2 t3) g s1 b1 g1 (S1 sk1)

    (* For loop *)

    | EvalT_For : forall l gamma lambda b gamma' x_l t gamma'' sigma b' sk sk'.
      eval_lexpr l gamma lambda b gamma' sk ->
      eval_term_tfor x_l lambda t gamma' sigma b' gamma'' sk' ->
      eval_term (TFor x_l l t) gamma sigma b' gamma'' (S2 sk sk')

    (* Do-While loop *)

    | EvalT_DoWhile_True : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sigma_2 gamma_2 sigma_3 b_3 gamma_3 sk1 sk2 sk3.
      eval_term t_1 gamma sigma_1 (BNormal b_1) gamma_1 sk1 ->
      eval_term t_2 gamma_1 sigma_2 (BNormal True) gamma_2 sk2 ->
      eval_term (TDoWhile t_1 t_2) gamma_2 sigma_3 b_3 gamma_3 sk3 ->
      eval_term (TDoWhile t_1 t_2) gamma (concat (concat sigma_1 sigma_2) sigma_3) b_3 gamma_3 (S3 sk1 sk2 sk3)

    | EvalT_DoWhile_False : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sigma_2 b_2 gamma_2 sk1 sk2.
      eval_term t_1 gamma sigma_1 (BNormal b_1) gamma_1 sk1 ->
      eval_term t_2 gamma_1 sigma_2 b_2 gamma_2 sk2 ->
      (match b_2 with BNormal False | BFatal -> true | _ -> false end) ->
      eval_term (TDoWhile t_1 t_2) gamma (concat sigma_1 sigma_2) (BNormal b_1) gamma_2 (S2 sk1 sk2)

    | EvalT_DoWhile_Transmit_Body : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sk1.
      eval_term t_1 gamma sigma_1 b_1 gamma_1 sk1 ->
      (match b_1 with BNormal _ -> false | _ -> true end) ->
      eval_term (TDoWhile t_1 t_2) gamma sigma_1 b_1 gamma_1 (S1 sk1)

    | EvalT_DoWhile_Transmit_Cond : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sigma_2 b_2 gamma_2 sk1 sk2.
      eval_term t_1 gamma sigma_1 (BNormal b_1) gamma_1 sk1 ->
      eval_term t_2 gamma_1 sigma_2 b_2 gamma_2 sk2 ->
      (match b_2 with BExit _ | BReturn _ -> true | _ -> false end) ->
      eval_term (TDoWhile t_1 t_2) gamma (concat sigma_1 sigma_2) b_2 gamma_2 (S2 sk1 sk2)

    (* Process *)

    | EvalT_Process : forall t gamma sigma b gamma' sk.
      eval_term t gamma sigma b gamma' sk ->
      eval_term (TProcess t) gamma sigma
        (match b with BNormal True | BReturn True | BExit True -> BNormal True | _ -> BFatal end)
        {gamma with c_fs = gamma'.c_fs ; c_input = gamma'.c_input} (S1 sk)

    (* Call *)

    | EvalT_Call : forall s gamma l beta gamma' sigma b' gamma'' sk sk'.
      eval_lexpr s gamma l beta gamma' sk -> (* beta is ignored *)
      eval_term_tcall l gamma' sigma b' gamma'' sk' ->
      eval_term (TCall s) gamma sigma b' gamma'' (S2 sk sk')

    (* Shift *)

    (* Not the nicest way to write it, but this way helps Why3. *)

    | EvalT_Shift_Nil : forall f se le i fe.
      eval_term TShift {c_fs = f ; c_senv = se ; c_lenv = le ; c_args = Nil ; c_input = i ; c_penv = fe }
        empty_string (BNormal False) {c_fs = f ; c_senv = se ; c_lenv = le ; c_args = Nil ; c_input = i ; c_penv = fe } S0

    | EvalT_Shift_NonNil : forall f se le ah at i fe.
      eval_term TShift {c_fs = f ; c_senv = se ; c_lenv = le ; c_args = Cons ah at ; c_input = i ; c_penv = fe }
        empty_string (BNormal True) {c_fs = f ; c_senv = se ; c_lenv = le ; c_args = at ; c_input = i ; c_penv = fe } S0

    (* Pipe *)

    | EvalT_Pipe : forall t_1 gamma sigma_1 b_1 gamma_1 t_2 sigma_2 b_2 gamma_2 sk1 sk2.
      eval_term t_1 gamma sigma_1 b_1 gamma_1 sk1 -> (* b_1 ignored *)
      eval_term t_2 {gamma_1 with c_input = sigma_1} sigma_2 b_2 gamma_2 sk2 ->
      eval_term (TPipe t_1 t_2) gamma sigma_2 b_2 {gamma_2 with c_input = gamma_1.c_input} (S2 sk1 sk2)

Semantics for TCall evaluation with a clean list

  with eval_term_tcall (list string) context string behaviour context skeleton =

    | EvalT_Call_Nil : forall gamma.
      eval_term_tcall Nil gamma empty_string (BNormal True) gamma S0

    | EvalT_Call_NonNil_True : forall gamma h t sigma b gamma' f gamma'' sk.
      gamma.c_penv h = Some f ->
      eval_term f {gamma with c_args = t} sigma b gamma' sk ->
      (match b with BNormal True | BReturn True -> true | _ -> false end) ->
      gamma'' = {gamma' with c_args = gamma.c_args} ->
      eval_term_tcall (Cons h t) gamma sigma (BNormal True) gamma'' (S1 sk)

    | EvalT_Call_NonNil_False : forall gamma h t sigma b gamma' f gamma'' sk.
      gamma.c_penv h = Some f ->
      eval_term f {gamma with c_args = t} sigma b gamma' sk ->
      (match b with BNormal False | BFatal | BReturn False -> true | _ -> false end) ->
      gamma'' = {gamma' with c_args = gamma.c_args} ->
      eval_term_tcall (Cons h t) gamma sigma BFatal gamma'' (S1 sk)

    | EvalT_Call_NonNil_Transmit : forall gamma h t sigma b gamma' f gamma'' sk.
      gamma.c_penv h = Some f ->
      eval_term f {gamma with c_args = t} sigma (BExit b) gamma' sk ->
      gamma'' = {gamma' with c_args = gamma.c_args} ->
      eval_term_tcall (Cons h t) gamma sigma (BExit b) gamma'' (S1 sk)

    | EvalT_Call_NonNil_Builtin_True : forall gamma h t sigma b gamma'.
      gamma.c_penv h = None ->
      eval_builtin h {gamma with c_args = t} = (sigma, b, gamma') ->
      (match b with BNormal True | BReturn True -> true | _ -> false end) ->
      eval_term_tcall (Cons h t) gamma sigma (BNormal True) {gamma' with c_args = gamma.c_args} S0

    | EvalT_Call_NonNil_Builtin_False : forall gamma h t sigma b gamma'.
      gamma.c_penv h = None ->
      eval_builtin h {gamma with c_args = t} = (sigma, b, gamma') ->
      (match b with BNormal False | BFatal | BReturn False -> true | _ -> false end) ->
      eval_term_tcall (Cons h t) gamma sigma BFatal {gamma' with c_args = gamma.c_args} S0

    | EvalT_Call_NonNil_Builtin_Transmit : forall gamma h t sigma b gamma'.
      gamma.c_penv h = None ->
      eval_builtin h {gamma with c_args = t} = (sigma, BExit b, gamma') ->
      eval_term_tcall (Cons h t) gamma sigma (BExit b) {gamma' with c_args = gamma.c_args} S0

Semantics for TFor evaluation with a clean list

  with eval_term_tfor svar (list string) term context string behaviour context skeleton =

    | EvalT_For_Nil : forall x_s t gamma.
      eval_term_tfor x_s Nil t gamma empty_string (BNormal True) gamma S0

    | EvalT_For_Cons_Nil : forall t gamma x_s sigma sigma' b gamma' sk.
      eval_term t (update_senv gamma x_s sigma) sigma' b gamma' sk ->
      eval_term_tfor x_s (Cons sigma Nil) t gamma sigma' b gamma' (S1 sk)

    | EvalT_For_Cons_Cons : forall t gamma x_s sigma_1 sigma b gamma' sigma_2 l sigma' b' gamma'' sk sk'.
      eval_term t (update_senv gamma x_s sigma_1) sigma (BNormal b) gamma' sk ->
      eval_term_tfor x_s (Cons sigma_2 l) t gamma' sigma' b' gamma'' sk' ->
      eval_term_tfor x_s (Cons sigma_1 (Cons sigma_2 l)) t gamma (concat sigma sigma') b' gamma'' (S2 sk sk')

    | EvalT_For_Cons_Cons_Transmit : forall t gamma x_s sigma_1 sigma_2 l sigma b gamma' sk.
      eval_term t (update_senv gamma x_s sigma_1) sigma b gamma' sk ->
      (match b with BNormal _ -> false | _ -> true end) ->
      eval_term_tfor x_s (Cons sigma_1 (Cons sigma_2 l)) t gamma sigma b gamma' (S1 sk)

Semantics for string evaluation

  with eval_sexpr sexpr context string bool context skeleton =

    | EvalSE : forall s gamma sigma beta gamma' sk.
      eval_sexpr_opt s gamma sigma beta gamma' sk ->
      eval_sexpr s gamma sigma (match beta with Some False -> False | _ -> True end) gamma' (S1 sk)

  with eval_sexpr_opt sexpr context string (option bool) context skeleton =

    | EvalSE_Nil : forall gamma.
      eval_sexpr_opt Nil gamma empty_string None gamma S0

    | EvalSE_Cons : forall f_s gamma sigma beta gamma' s sigma' beta' gamma'' sk sk'.
      eval_sfrag_opt f_s gamma sigma beta gamma' sk ->
      eval_sexpr_opt s gamma' sigma' beta' gamma'' sk' ->
      eval_sexpr_opt (Cons f_s s) gamma (concat sigma sigma') (bocompose beta beta') gamma'' (S2 sk sk')

  with eval_sfrag_opt sfrag context string (option bool) context skeleton =

    | EvalSE_String : forall sigma gamma.
      eval_sfrag_opt (SLiteral sigma) gamma sigma None gamma S0

    | EvalSE_Var : forall x_s gamma.
      eval_sfrag_opt (SVar x_s) gamma (gamma.c_senv x_s) None gamma S0

    | EvalSE_Arg : forall n gamma.
      eval_sfrag_opt (SArg n) gamma
        (match nth n gamma.c_args with None -> empty_string | Some sigma -> sigma end)
	None gamma S0

    | EvalSE_Process : forall t gamma sigma b gamma' sk.
      eval_term t gamma sigma b gamma' sk ->
      eval_sfrag_opt (SProcess t) gamma sigma
        (Some (match b with BNormal True | BReturn True | BExit True -> True | _ -> False end))
        {gamma with c_fs = gamma'.c_fs ; c_input = gamma'.c_input} (S1 sk)

Semantics for list evaluation

  with eval_lexpr lexpr context (list string) bool context skeleton =

    | EvalLE : forall l gamma lambda beta gamma' sk.
      eval_lexpr_opt l gamma lambda beta gamma' sk ->
      eval_lexpr l gamma lambda
        (match beta with Some False -> False | _ -> True end)
	gamma' (S1 sk)

  with eval_lexpr_opt lexpr context (list string) (option bool) context skeleton =

    | EvalLE_Nil : forall gamma.
      eval_lexpr_opt Nil gamma Nil None gamma S0

    | EvalLE_Cons : forall f_l l gamma gamma' gamma'' lambda lambda' beta beta' sk sk'.
      eval_lfrag_opt f_l gamma lambda beta gamma' sk ->
      eval_lexpr_opt l gamma' lambda' beta' gamma'' sk' ->
      eval_lexpr_opt (Cons f_l l) gamma (lambda ++ lambda') (bocompose beta beta') gamma'' (S2 sk sk')

  with eval_lfrag_opt lfrag context (list string) (option bool) context skeleton =

    | EvalLF_Singleton : forall s gamma sigma beta gamma' sk.
      eval_sexpr_opt s gamma sigma beta gamma' sk ->
      eval_lfrag_opt (LSingleton s) gamma (Cons sigma Nil) beta gamma' (S1 sk)

    | EvalLF_Split : forall s gamma sigma beta gamma' sk.
      eval_sexpr_opt s gamma sigma beta gamma' sk ->
      eval_lfrag_opt (LSplit s) gamma (split sigma) beta gamma' (S1 sk)

    | EvalLF_Var : forall x_l gamma.
      eval_lfrag_opt (LVar x_l) gamma (gamma.c_lenv x_l) None gamma S0
end