Module unseq

Require Import Clight.
Require Import Errors.

Open Scope error_monad_scope.

Fixpoint context (k: cont): cont :=
  match k with
    | Kseq _ k => context k
    | _ => k
  end.

Fixpoint context' (k: cont): cont :=
  match k with
    | Kseq _ k => context' k
    | Kswitch k => context' k
    | _ => k
  end.

Fixpoint unseq (k: cont) (s: statement): res statement :=
  match s with
    | Ssequence Sskip s2 => unseq k s2
    | Ssequence s1 s2 =>
      do s1' <- unseq (Kseq s2 k) s1;
      do s2' <- unseq k s2;
      OK (Ssequence s1' s2')
    | Sifthenelse e s1 s2 =>
      do s1' <- unseq k s1;
      do s2' <- unseq k s2;
      OK (Sifthenelse e s1' s2')
    | Sloop s1 s2 =>
      do s1' <- unseq (Kloop1 s1 s2 k) s1;
      do s2' <- unseq (Kloop2 s1 s2 k) s2;
      OK (Sloop s1' s2')
    | Slabel lbl s' =>
      do ss <- unseq k s';
      OK (Slabel lbl ss)
    | Sswitch e ls =>
      do ls' <- unseq_ls (Kswitch k) ls;
      OK (Sswitch e ls')
    | Sskip => OK Sskip
    | Sbreak =>
      match context k with
        | Kloop1 _ _ _ | Kloop2 _ _ _ | Kswitch _ => OK Sbreak
        | _ => Error (msg "break")
      end
    | Scontinue =>
      match context' k with
        | Kloop1 _ _ _ => OK Scontinue
        | _ => Error (msg "continue")
      end
    | Sassign _ _ => OK s
    | Sset _ _ => OK s
    | Scall _ _ _ => OK s
    | Sbuiltin _ _ _ _ => OK s
    | Sreturn _ => OK s
    | Sgoto _ => OK s
  end
with unseq_ls (k: cont) (ls: labeled_statements): res labeled_statements :=
       match ls with
         | LSnil => OK LSnil
         | LScons lbl s ls' =>
           do lss <- unseq_ls k ls';
           do s' <- unseq (Kseq (seq_of_labeled_statement ls') k) s;
           OK (LScons lbl s' lss)
       end.

Definition transf_function (f: function): res function :=
  do body <- unseq Kstop (fn_body f);
  OK {| fn_return := f.(fn_return);
        fn_callconv := f.(fn_callconv);
        fn_params := f.(fn_params);
        fn_vars := f.(fn_vars);
        fn_temps := f.(fn_temps);
        fn_body := body |}.

Definition transf_fundef (fd: fundef) : res fundef :=
  match fd with
  | Internal f => do tf <- transf_function f; OK (Internal tf)
  | External ef targs tres cconv => OK (External ef targs tres cconv)
  end.

Definition transf_program (p: program) : res program :=
  do p1 <- AST.transform_partial_program transf_fundef p;
  OK {| prog_defs := AST.prog_defs p1;
        prog_public := AST.prog_public p1;
        prog_main := AST.prog_main p1;
        prog_types := prog_types p;
        prog_comp_env := prog_comp_env p;
        prog_comp_env_eq := prog_comp_env_eq p |}.