Interpreter

Correct term interpreter

module CorrectTermInterpreter
  use import int.Int
  use import list.List
  use import list.Append
  use import list.Nth
  use import list.NthHdTl (* needed for the proof for AsString and AsList *)
  use import option.Option
  use import ref.Ref
  use import mystrings.String

  use HighOrd
  use import base.Syntax
  use import base.CommonSemantics
  use import base.Semantics

  exception EFatal context
  exception EReturn (bool, context)
  exception EExit (bool, context)

Interpreter for builtins

  let interp_builtin (f: string) (gamma: context) (stdout: ref string) : (bool, context)
    returns { (b, gamma')        -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_builtin f gamma = (sigma, BNormal b, gamma') }
    raises { EFatal gamma'       -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_builtin f gamma = (sigma, BFatal,    gamma') }
    raises { EReturn (b, gamma') -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_builtin f gamma = (sigma, BReturn b, gamma') }
    raises { EExit (b, gamma')   -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_builtin f gamma = (sigma, BExit b,   gamma') }
  =
    let (sigma, b, gamma') = eval_builtin f gamma in
    stdout := concat !stdout sigma;
    match b with
    | BNormal b' -> (b', gamma')
    | BFatal -> raise (EFatal gamma')
    | BReturn b' -> raise (EReturn (b', gamma'))
    | BExit b' -> raise (EExit (b', gamma'))
    end

Interpreter for terms

  let rec interp_term (t: term) (gamma: context) (stdout : ref string) : (bool, context)
    diverges
    returns { (b, gamma')         -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term t gamma sigma (BNormal b)  gamma' }
    raises  { EFatal gamma'       -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term t gamma sigma  BFatal      gamma' }
    raises  { EReturn (b, gamma') -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term t gamma sigma (BReturn b)  gamma' }
    raises  { EExit (b, gamma')   -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term t gamma sigma (BExit   b)  gamma' }
  =
    match t with
    (* Literals *)

    | TTrue  -> (true,  gamma)
    | TFalse -> (false, gamma)
    | TFatal -> raise (EFatal gamma)

    (* Return, Exit *)

    | TReturn t ->
      raise (EReturn (interp_term t gamma stdout))

    | TExit t ->
      raise (EExit (interp_term t gamma stdout))

    (* Assign *)

    | TAsString xs s ->
      let (sigma, b, gamma') = interp_sexpr s gamma in
      let gamma'' = update_senv gamma' xs sigma in
      if b then
        (true, gamma'')
      else
        raise (EFatal gamma'')   (* It is really gamma''! *)

    | TAsList x_l l ->
      let (lambda, b, gamma') = interp_lexpr l gamma in
      let gamma'' = update_lenv gamma' x_l lambda in
      if b then
        (true, gamma'')
      else
        raise (EFatal gamma'')   (* it is really gamma''! *)

    (* Sequence *)

    | TSeq t_1 t_2 ->
      let (_, gamma_1) = interp_term t_1 gamma stdout in
      interp_term t_2 gamma_1 stdout

    (* Conditional *)

    | TIf t_1 t_2 t3 ->
      let (b_1, gamma_1) =
        try
	  interp_term t_1 gamma stdout
        with
	  EFatal gamma' -> (false, gamma')
        end
      in
      interp_term (if b_1 then t_2 else t3) gamma_1 stdout

    (* For loop *)

    | TFor xs l t ->
      let (lambda, _, gamma') = interp_lexpr l gamma in  (* return code of the list is ignored in the for *)
      interp_for xs lambda t gamma' stdout

    (* Do-While loop *)

    | TDoWhile t_1 t_2 ->
      let (b_1, gamma_1) = interp_term t_1 gamma stdout in
      let (b_2, gamma_2) =
        try
          interp_term t_2 gamma_1 stdout
	with
	  EFatal gamma_2 -> (false, gamma_2)
	end
      in
      if b_2 then
        interp_term (TDoWhile t_1 t_2) gamma_2 stdout
      else
        (b_1, gamma_2)

    (* Process *)

    | TProcess t ->
      let (sigma, b, fs, input) = interp_process t gamma in
      stdout := concat !stdout sigma;
      let gamma' = {gamma with c_fs = fs; c_input = input} in
      if b then
        (true, gamma')
      else
        raise (EFatal gamma')

    (* Call *)

    | TCall l ->
      let (lambda, _, gamma') = interp_lexpr l gamma in (* return code of the list is ignored in the call *)
      interp_call lambda gamma' stdout

    (* Shift *)

    | TShift ->
      match gamma.c_args with
      | Nil -> (false, gamma)
      | Cons _ args' -> (true, {gamma with c_args=args'})
      end

    | TPipe t_1 t_2 ->
      let stdout_1 = ref empty_string in
      let gamma_1 =
        try
          let _, gamma_1 = interp_term t_1 gamma stdout_1 in
	  gamma_1
        with
        | EFatal gamma_1 -> gamma_1
        | EReturn (_, gamma_1) -> gamma_1
        | EExit (_, gamma_1) -> gamma_1
        end
      in
      try
        let (b_2, gamma_2) = interp_term t_2 {gamma_1 with c_input = (!stdout_1)} stdout in
        (b_2, {gamma_2 with c_input=gamma_1.c_input})
      with
      | EFatal gamma_2 -> raise (EFatal {gamma_2 with c_input = gamma_1.c_input})
      | EReturn (b_2, gamma_2) -> raise (EReturn (b_2, {gamma_2 with c_input = gamma_1.c_input}))
      | EExit (b_2, gamma_2) -> raise (EExit (b_2, {gamma_2 with c_input = gamma_1.c_input}))
      end

    | _ -> absurd
    end

Interpreter for the for

  with interp_for (x_s: svar) (l: list string) (t: term) (gamma: context) (stdout: ref string) : (bool, context)
    diverges
    returns { (b, gamma')        -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tfor x_s l t gamma sigma (BNormal b)  gamma' }
    raises { EFatal gamma'       -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tfor x_s l t gamma sigma  BFatal      gamma' }
    raises { EReturn (b, gamma') -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tfor x_s l t gamma sigma (BReturn b)  gamma' }
    raises { EExit (b, gamma')   -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tfor x_s l t gamma sigma (BExit b)    gamma' }
   =
     match l with
     | Nil -> (true, gamma)
     | Cons sigma Nil ->
       interp_term t (update_senv gamma x_s sigma) stdout
     | Cons sigma (Cons sigma' l'') ->
       let (_, gamma') = interp_term t (update_senv gamma x_s sigma) stdout in
       interp_for x_s (Cons sigma' l'') t gamma' stdout
     end

Interpreter for function call

  with interp_call (l: list string) (gamma: context) (stdout: ref string) : (bool, context)
    diverges
    returns { (b, gamma')      -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tcall l gamma sigma (BNormal b) gamma' }
    raises { EFatal gamma'     -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tcall l gamma sigma  BFatal     gamma' }
    raises { EExit (b, gamma') -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tcall l gamma sigma (BExit b)   gamma' }
  =
    match l with
    | Nil -> (true, gamma)
    | Cons sigma lt ->
      let (b, gamma') =
        try
          match gamma.c_penv sigma with
          | None -> interp_builtin sigma {gamma with c_args = lt} stdout
          | Some t -> interp_term t {gamma with c_args = lt} stdout
          end
        with
	| EFatal gamma' -> (false, gamma')
	| EReturn (b, gamma') -> (b, gamma')
	| EExit (b, gamma') -> raise (EExit (b, {gamma' with c_args = gamma.c_args}))
        end
      in
      let gamma' = {gamma' with c_args = gamma.c_args} in
      if b then
        (true, gamma')
      else
        raise (EFatal gamma')
    end

Interpreter for the strings

  with interp_sexpr (s: sexpr) (gamma: context) : (string, bool, context)
    diverges
    returns { (sigma, beta, gamma') -> eval_sexpr s gamma sigma beta gamma' }
  =
    interp_sexpr_aux s gamma true

  with interp_sexpr_aux (s: sexpr) (gamma: context) (previous: bool) : (string, bool, context)
    diverges
    returns { (sigma, b, gamma') -> (eval_sexpr_opt s gamma sigma None gamma' /\ b = previous) \/ (eval_sexpr_opt s gamma sigma (Some b) gamma') }
  =
    match s with
    | Nil -> (empty_string, previous, gamma)
    | Cons f_s s' ->
       let (sigma_1, b, gamma') = interp_sfrag_aux f_s gamma previous in
       let (sigma_2, b', gamma'') = interp_sexpr_aux s' gamma' b in
       (concat sigma_1 sigma_2, b', gamma'')
    end

  with interp_sfrag_aux (f_s: sfrag) (gamma: context) (previous: bool) : (string, bool, context)
    diverges
    returns { (sigma, b, gamma') -> (eval_sfrag_opt f_s gamma sigma None gamma' /\ b = previous) \/ (eval_sfrag_opt f_s gamma sigma (Some b) gamma') }
  =
    match f_s with
    | SLiteral sigma -> (sigma, previous, gamma)   (* literals keep the previous return code *)
    | SVar x_s -> (gamma.c_senv x_s, previous, gamma)
    | SArg n ->
      match nth n gamma.c_args with
      | None -> (empty_string, previous, gamma)
      | Some sigma -> (sigma, previous, gamma)
      end
    | SProcess t ->
      let (sigma, b, fs, input) = interp_process t gamma in
      (sigma, b, {gamma with c_fs = fs; c_input = input})
    end

Interpreter for lists

  with interp_lexpr (l: lexpr) (gamma: context) : (list string, bool, context)
    diverges
    returns { (lambda, beta, gamma') -> eval_lexpr l gamma lambda beta  gamma' }
  =
    interp_lexpr_aux l gamma true

  with interp_lexpr_aux (l: lexpr) (gamma: context) (previous: bool) : (list string, bool, context)
    diverges
    returns { (lambda, b, gamma') -> (eval_lexpr_opt l gamma lambda None gamma' /\ b = previous) \/ (eval_lexpr_opt l gamma lambda (Some b) gamma') }
  =
    match l with
    | Nil -> (Nil, previous, gamma)
    | Cons fl l' ->
       let (lambda_1, b, gamma') = interp_lfrag_aux fl gamma previous in
       let (lambda_2, b', gamma'') = interp_lexpr_aux l' gamma' b in
       (lambda_1 ++ lambda_2, b', gamma'')
    end

  with interp_lfrag_aux (f_l: lfrag) (gamma: context) (previous: bool) : (list string, bool, context)
    diverges
    returns { (lambda, b, gamma') -> (eval_lfrag_opt f_l gamma lambda None gamma' /\ b = previous) \/ (eval_lfrag_opt f_l gamma lambda (Some b) gamma') }
  =
    match f_l with
    | LSingleton s ->
      let (sigma, b, gamma') = interp_sexpr_aux s gamma previous in
      (Cons sigma Nil, b, gamma')
    | LSplit s ->
      let (sigma, b, gamma') = interp_sexpr_aux s gamma previous in
      (split sigma, b, gamma')
    | LVar x_l -> (gamma.c_lenv x_l, previous, gamma)
    end

Interpreter for processes

  with interp_process (t: term) (gamma: context) : (string, bool, filesystem, string)
    diverges
    returns { (sigma, b, fs, input) -> eval_term (TProcess t) gamma sigma (match b with True -> BNormal True | False -> BFatal end) {gamma with c_fs = fs ; c_input = input} }
  =
    let stdout = ref empty_string in
    let (b, gamma') =
      try
        interp_term t gamma stdout
      with
        | EFatal gamma' -> (false, gamma')
        | EReturn (b, gamma) -> (b, gamma)
        | EExit (b, gamma) -> (b, gamma)
      end
    in
    (!stdout, b, gamma'.c_fs, gamma'.c_input)
end

Terminating term interpreter

module TerminatingTermInterpreter
  use import int.Int
  use import list.List
  use import list.Append
  use import list.Nth
  use import list.NthHdTl (* needed for the proof for AsString and AsList *)
  use import option.Option
  use import ref.Ref
  use import mystrings.String
  use import skeleton.Skeleton

  use HighOrd
  use import base.Syntax
  use import base.CommonSemantics
  use import base.SemanticsWithSkeleton

  use import lemmas.FunctionnalSemanticsWithSkeleton

  exception EFatal context
  exception EReturn (bool, context)
  exception EExit (bool, context)

Interpreter for builtins

  let interp_builtin (f: string) (gamma: context) (stdout: ref string) : (bool, context)
    returns { (b, gamma')        -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_builtin f gamma = (sigma, BNormal b, gamma') }
    raises { EFatal gamma'       -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_builtin f gamma = (sigma, BFatal,    gamma') }
    raises { EReturn (b, gamma') -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_builtin f gamma = (sigma, BReturn b, gamma') }
    raises { EExit (b, gamma')   -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_builtin f gamma = (sigma, BExit b,   gamma') }
  =
    let (sigma, b, gamma') = eval_builtin f gamma in
    stdout := concat !stdout sigma;
    match b with
    | BNormal b' -> (b', gamma')
    | BFatal -> raise (EFatal gamma')
    | BReturn b' -> raise (EReturn (b', gamma'))
    | BExit b' -> raise (EExit (b', gamma'))
    end

Interpreter for terms

  let rec interp_term (t: term) (g: context) (stdout : ref string) (ghost sk: skeleton) : (bool, context)
    requires { exists s b g'. eval_term t g s b g' sk }
    variant { sk }
    returns { (b, g')         -> exists s. !stdout = concat (old !stdout) s /\ eval_term t g s (BNormal b)  g' sk }
    raises  { EFatal g'       -> exists s. !stdout = concat (old !stdout) s /\ eval_term t g s  BFatal      g' sk }
    raises  { EReturn (b, g') -> exists s. !stdout = concat (old !stdout) s /\ eval_term t g s (BReturn b)  g' sk }
    raises  { EExit (b, g')   -> exists s. !stdout = concat (old !stdout) s /\ eval_term t g s (BExit   b)  g' sk }
  =
    match t with
    (* Literals *)

    | TTrue  -> (true,  g)
    | TFalse -> (false, g)
    | TFatal -> raise (EFatal g)

    (* Return, Exit *)

    | TReturn t ->
      let ghost sk' = skeleton1 sk in
      raise (EReturn (interp_term t g stdout sk'))

    | TExit t ->
      let ghost sk' = skeleton1 sk in
      raise (EExit (interp_term t g stdout sk'))

    (* Assign *)

    | TAsString xs s ->
      let ghost sk' = skeleton1 sk in
      let (sigma, b, g') = interp_sexpr s g sk' in
      let g'' = update_senv g' xs sigma in
      if b then
        (true, g'')
      else
        raise (EFatal g'')   (* It is really g''! *)

    | TAsList x_l l ->
      let ghost sk' = skeleton1 sk in
      let (lambda, b, g') = interp_lexpr l g sk' in
      let g'' = update_lenv g' x_l lambda in
      if b then
        (true, g'')
      else
        raise (EFatal g'')   (* it is really g''! *)

    (* Sequence *)

    | TSeq t1 t2 ->
      let ghost sk1 = skeleton12 sk in
      let (_, g1) = interp_term t1 g stdout sk1 in
      let ghost (_, sk2) = skeleton2 sk in
      interp_term t2 g1 stdout sk2

    (* Conditional *)

    | TIf t1 t2 t3 ->
      let (b1, g1) =
        try
	  let ghost sk1 = skeleton12 sk in
	  interp_term t1 g stdout sk1
        with
	  EFatal g' -> (false, g')
        end
      in
      let ghost (_, s2) = skeleton2 sk in
      interp_term (if b1 then t2 else t3) g1 stdout s2

    (* For loop *)

    | TFor xs l t ->
      let ghost (sk1, sk2) = skeleton2 sk in
      let (lambda, _, g') = interp_lexpr l g sk1 in  (* return code of the list is ignored in the for *)
      interp_for xs lambda t g' stdout sk2

    (* Do-While loop *)

    | TDoWhile t_1 t_2 ->
      let ghost sk1 = skeleton123 sk in
      let (b_1, g_1) = interp_term t_1 g stdout sk1 in
      let (b_2, g_2) =
        try
	  let ghost (_, sk2) = skeleton23 sk in
          interp_term t_2 g_1 stdout sk2
	with
	  EFatal g_2 -> (false, g_2)
	end
      in
      if b_2 then
        let _, _, sk3 = skeleton3 sk in
        interp_term (TDoWhile t_1 t_2) g_2 stdout sk3
      else
        (b_1, g_2)

    (* Process *)

    | TProcess t ->
      let (b, g') =
        try
          let ghost sk1 = skeleton1 sk in
          interp_term t g stdout sk1
        with
          | EFatal g' -> (false, g')
          | EReturn (b, g) -> (b, g)
          | EExit (b, g) -> (b, g)
        end
      in
      let g' = {g with c_fs = g'.c_fs; c_input = g'.c_input} in
      if b then
        (true, g')
      else
        raise (EFatal g')

    (* Call *)

    | TCall l ->
      let ghost (sk1, sk2) = skeleton2 sk in
      let (lambda, _, g') = interp_lexpr l g sk1 in (* return code of the list is ignored in the call *)
      interp_call lambda g' stdout sk2

    (* Shift *)

    | TShift ->
      match g.c_args with
      | Nil -> (false, g)
      | Cons _ args' -> (true, {g with c_args=args'})
      end

    | TPipe t_1 t_2 ->
      let ghost (sk1, sk2) = skeleton2 sk in
      let stdout_1 = ref empty_string in
      let g_1 =
        try
          let _, g_1 = interp_term t_1 g stdout_1 sk1 in
	  g_1
        with
        | EFatal g_1 -> g_1
        | EReturn (_, g_1) -> g_1
        | EExit (_, g_1) -> g_1
        end
      in
      try
        let (b_2, g_2) = interp_term t_2 {g_1 with c_input = (!stdout_1)} stdout sk2 in
        (b_2, {g_2 with c_input=g_1.c_input})
      with
      | EFatal g_2 -> raise (EFatal {g_2 with c_input = g_1.c_input})
      | EReturn (b_2, g_2) -> raise (EReturn (b_2, {g_2 with c_input = g_1.c_input}))
      | EExit (b_2, g_2) -> raise (EExit (b_2, {g_2 with c_input = g_1.c_input}))
      end

    | _ -> absurd
    end

Interpreter for the for

  with interp_for (x_s: svar) (l: list string) (t: term) (g: context) (stdout: ref string) (ghost sk: skeleton) : (bool, context)
    requires { exists sigma b g'. eval_term_tfor x_s l t g sigma b g' sk }
    variant { sk }
    returns { (b, g')        -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tfor x_s l t g sigma (BNormal b)  g' sk }
    raises { EFatal g'       -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tfor x_s l t g sigma  BFatal      g' sk }
    raises { EReturn (b, g') -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tfor x_s l t g sigma (BReturn b)  g' sk }
    raises { EExit (b, g')   -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tfor x_s l t g sigma (BExit b)    g' sk }
   =
     match l with
     | Nil -> (true, g)

     | Cons sigma Nil ->
       let ghost sk1 = skeleton1 sk in
       interp_term t (update_senv g x_s sigma) stdout sk1

     | Cons sigma (Cons sigma' l'') ->
       let ghost sk1 = skeleton12 sk in
       let (_, g') = interp_term t (update_senv g x_s sigma) stdout sk1 in
       let ghost (_, sk2) = skeleton2 sk in
       interp_for x_s (Cons sigma' l'') t g' stdout sk2
     end

Interpreter for function call

  with interp_call (l: list string) (g: context) (stdout: ref string) (ghost sk: skeleton) : (bool, context)
    requires { exists sigma b g'. eval_term_tcall l g sigma b g' sk }
    variant { sk }
    returns { (b, g')      -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tcall l g sigma (BNormal b) g' sk }
    raises { EFatal g'     -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tcall l g sigma  BFatal     g' sk }
    raises { EExit (b, g') -> exists sigma. !stdout = concat (old !stdout) sigma /\ eval_term_tcall l g sigma (BExit b)   g' sk }
  =
    match l with
    | Nil -> (true, g)

    | Cons sigma lt ->
      let (b, g') =
        try
          match g.c_penv sigma with
          | None -> interp_builtin sigma {g with c_args = lt} stdout
          | Some t ->
	    let ghost sk1 = skeleton1 sk in
	    interp_term t {g with c_args = lt} stdout sk1
          end
        with
	| EFatal g' -> (false, g')
	| EReturn (b, g') -> (b, g')
	| EExit (b, g') -> raise (EExit (b, {g' with c_args = g.c_args}))
        end
      in
      let g' = {g' with c_args = g.c_args} in
      if b then
        (true, g')
      else
        raise (EFatal g')
    end

Interpreter for the strings

  with interp_sexpr (s: sexpr) (g: context) (ghost sk: skeleton) : (string, bool, context)
    requires { exists sigma beta g'. eval_sexpr s g sigma beta g' sk }
    variant { sk }
    returns { (sigma, beta, g') -> eval_sexpr s g sigma beta g' sk }
  =
    let ghost sk1 = skeleton1 sk in
    interp_sexpr_aux s g true sk1

  with interp_sexpr_aux (s: sexpr) (g: context) (previous: bool) (ghost sk: skeleton) : (string, bool, context)
    requires { exists sigma b g'. eval_sexpr_opt s g sigma b g' sk }
    variant { sk }
    returns { (sigma, b, g') -> (eval_sexpr_opt s g sigma None g' sk /\ b = previous) \/ (eval_sexpr_opt s g sigma (Some b) g' sk) }
  =
    match s with
    | Nil -> (empty_string, previous, g)
    | Cons f_s s' ->
      let ghost (sk1, sk2) = skeleton2 sk in
      let (sigma_1, b, g') = interp_sfrag_aux f_s g previous sk1 in
      let (sigma_2, b', g'') = interp_sexpr_aux s' g' b sk2 in
      (concat sigma_1 sigma_2, b', g'')
    end

  with interp_sfrag_aux (f_s: sfrag) (g: context) (previous: bool) (ghost sk: skeleton) : (string, bool, context)
    requires { exists sigma b g'. eval_sfrag_opt f_s g sigma b g' sk }
    variant { sk }
    returns { (sigma, b, g') -> (eval_sfrag_opt f_s g sigma None g' sk /\ b = previous) \/ (eval_sfrag_opt f_s g sigma (Some b) g' sk) }
  =
    match f_s with
    | SLiteral sigma -> (sigma, previous, g)   (* literals keep the previous return code *)
    | SVar x_s -> (g.c_senv x_s, previous, g)
    | SArg n ->
      match nth n g.c_args with
      | None -> (empty_string, previous, g)
      | Some sigma -> (sigma, previous, g)
      end

    | SProcess t ->
      let stdout = ref empty_string in
      let (b, g') =
        try
          let ghost sk1 = skeleton1 sk in
          interp_term t g stdout sk1
        with
          | EFatal g' -> (false, g')
          | EReturn (b, g) -> (b, g)
          | EExit (b, g) -> (b, g)
        end
      in
      (!stdout, b, {g with c_fs = g'.c_fs; c_input = g'.c_input})
    end

Interpreter for lists

  with interp_lexpr (l: lexpr) (g: context) (ghost sk: skeleton) : (list string, bool, context)
    requires { exists lambda beta g'. eval_lexpr l g lambda beta g' sk }
    variant { sk }
    returns { (lambda, beta, g') -> eval_lexpr l g lambda beta  g' sk }
  =
    let ghost sk1 = skeleton1 sk in
    interp_lexpr_aux l g true sk1

  with interp_lexpr_aux (l: lexpr) (g: context) (previous: bool) (ghost sk: skeleton) : (list string, bool, context)
    requires { exists lambda b g'. eval_lexpr_opt l g lambda b g' sk }
    variant { sk }
    returns { (lambda, b, g') -> (eval_lexpr_opt l g lambda None g' sk /\ b = previous) \/ (eval_lexpr_opt l g lambda (Some b) g' sk) }
  =
    match l with
    | Nil -> (Nil, previous, g)
    | Cons fl l' ->
      let ghost (sk1, sk2) = skeleton2 sk in
      let (lambda_1, b, g') = interp_lfrag_aux fl g previous sk1 in
      let (lambda_2, b', g'') = interp_lexpr_aux l' g' b sk2 in
      (lambda_1 ++ lambda_2, b', g'')
    end

  with interp_lfrag_aux (f_l: lfrag) (g: context) (previous: bool) (ghost sk: skeleton) : (list string, bool, context)
    requires { exists lambda b g'. eval_lfrag_opt f_l g lambda b g' sk }
    variant { sk }
    returns { (lambda, b, g') -> (eval_lfrag_opt f_l g lambda None g' sk /\ b = previous) \/ (eval_lfrag_opt f_l g lambda (Some b) g' sk) }
  =
    match f_l with
    | LSingleton s ->
      let ghost sk1 = skeleton1 sk in
      let (sigma, b, g') = interp_sexpr_aux s g previous sk1 in
      (Cons sigma Nil, b, g')

    | LSplit s ->
      let ghost sk1 = skeleton1 sk in
      let (sigma, b, g') = interp_sexpr_aux s g previous sk1 in
      (split sigma, b, g')

    | LVar x_l -> (g.c_lenv x_l, previous, g)
    end

Interpreter for processes

  with interp_process (t: term) (g: context) (ghost sk: skeleton) : (string, bool, filesystem, string)
    requires { exists sigma b g'. eval_term (TProcess t) g sigma b g' sk }
    variant { sk }
    returns { (sigma, b, fs, input) -> eval_term (TProcess t) g sigma (match b with True -> BNormal True | False -> BFatal end) {g with c_fs = fs ; c_input = input} sk }
  =
    let stdout = ref empty_string in
    let (b, g') =
      try
        let ghost sk1 = skeleton1 sk in
        interp_term t g stdout sk1
      with
        | EFatal g' -> (false, g')
        | EReturn (b, g) -> (b, g)
        | EExit (b, g) -> (b, g)
      end
    in
    (!stdout, b, g'.c_fs, g'.c_input)
end

The Interpreter

And finally, the program interpreter.

module Interpreter
  use import list.List
  use import ref.Ref
  use import mystrings.String

  use import base.Syntax
  use import base.CommonSemantics
  use import base.Semantics
  use import CorrectTermInterpreter
  (* use import CompleteTermInterpreter *)

  let rec populate_penv (g: context) (pdecls: list (string, term)) : context
    variant { pdecls }
  =
    match pdecls with
    | Nil -> g
    | Cons (i, t) fd ->
      populate_penv (update_penv g i t) fd
    end

  let interp_program (p: program) (args: list string) (input: string) (stdout: ref string) : bool
    diverges
  =

    let g = empty_context in
    let g = {g with c_args = args ; c_input = input} in
    let g = populate_penv g p.p_pdecls in
    try
      let (b, _) = interp_term p.p_term g stdout in b
    with
    | EFatal _ -> false
    | EReturn (b, _) -> b
    | EExit (b, _) -> b
    end
end