(**************************************************************************)
(*     ARM/Power Multiprocessor Machine Code Semantics: HOL sources       *)
(*                                                                        *)
(*                                                                        *)
(*  Jade Alglave (2), Anthony Fox (1), Samin Isthiaq (3),                 *)
(*  Magnus Myreen (1), Susmit Sarkar (1), Peter Sewell (1),               *)
(*  Francesco Zappa Nardelli (2)                                          *)
(*                                                                        *)
(*   (1) Computer Laboratory, University of Cambridge                     *)
(*   (2) Moscova project, INRIA Paris-Rocquencourt                        *)
(*   (3) Microsoft Research Cambridge                                     *)
(*                                                                        *)
(*     Copyright 2007-2008                                                *)
(*                                                                        *)
(*  Redistribution and use in source and binary forms, with or without    *)
(*  modification, are permitted provided that the following conditions    *)
(*  are met:                                                              *)
(*                                                                        *)
(*  1. Redistributions of source code must retain the above copyright     *)
(*     notice, this list of conditions and the following disclaimer.      *)
(*  2. Redistributions in binary form must reproduce the above copyright  *)
(*     notice, this list of conditions and the following disclaimer in    *)
(*     the documentation and/or other materials provided with the         *)
(*     distribution.                                                      *)
(*  3. The names of the authors may not be used to endorse or promote     *)
(*     products derived from this software without specific prior         *)
(*     written permission.                                                *)
(*                                                                        *)
(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,          *)
(*  WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING             *)
(*  NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS    *)
(*  SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.          *)
(*                                                                        *)
(**************************************************************************)

open HolKernel boolLib bossLib Parse;

open ppc_coretypesTheory ppc_astTheory ppc_opsemTheory ppc_seq_monadTheory ppc_decoderTheory ;

open HolDoc;
val _ = new_theory "ppc_";

(* ---------------------------------------------------------------------------------- *>

  Here the decoder from ppc_decoderTheory is put together with ppc_exec_instr
  from ppc_opsemTheory and the sequential monad from ppc_seq_monadTheory.

<* ---------------------------------------------------------------------------------- *)

val iiid_dummy_def = Define `iiid_dummy = <| proc:=0; poi:=0 |>`;

val PPC_NEXT_def = Define `
  PPC_NEXT s = 
    let pc = PREAD_R PPC_PC s in
    let w0 = PREAD_M (pc + 0w) s in
    let w1 = PREAD_M (pc + 1w) s in
    let w2 = PREAD_M (pc + 2w) s in
    let w3 = PREAD_M (pc + 3w) s in
    let raw_instruction = w2bits (THE w0) ++ w2bits (THE w1) ++ w2bits (THE w2) ++ w2bits (THE w3) in
    let i = ppc_decode raw_instruction in
    let s' = ppc_exec_instr iiid_dummy (THE i) s in
      if ~(pc && 3w = 0w) \/ MEM NONE [w0;w1;w2;w3] \/ (i = NONE) \/ (s' = NONE) then NONE
      else SOME (SND (THE s'))`;


val _ = export_theory ();