From SailStdpp Require Import -(notations) Base ConcurrencyInterfaceV2.

Module Type SailArch := Arch.
Module Type SailInterfaceT := InterfaceT.

From ASCommon Require Import Options.
From ASCommon Require Import Common FMon.

Require Import Interface.

#[export] Typeclasses Transparent choose_type.
#[export] Typeclasses Transparent mword.
#[export] Typeclasses Transparent MachineWord.MachineWord.word.
#[export] Typeclasses Transparent MachineWord.MachineWord.idx.
#[export] Typeclasses Transparent MachineWord.MachineWord.Z_idx.
#[export] Typeclasses Transparent Z.to_N.

Arguments MachineWord.MachineWord.word / _.
Arguments MachineWord.MachineWord.idx /.
Arguments MachineWord.MachineWord.Z_idx / _.

Remove Hints Decidable_eq_mword Countable_mword : typeclass_instances.

#[refine] Instance bitU_finite : Finite bitU := { enum := [B0; B1; BU] }.
Proof.
  - abstract(unshelve (auto with nodup); set_solver).
  - abstract(intros []; set_solver).
Defined.

Module Type ArchExtra (SA : SailArch).
  Import SA.

  Parameter pc_reg : reg.
  Parameter reg_of_string : string → option reg.
  Parameter reg_type_of_gen : ∀ r : reg, reg_gen_val → result string (reg_type r).
  Parameter reg_type_to_gen : ∀ r : reg, reg_type r → reg_gen_val.
End ArchExtra.

Module ArchFromSail (SA : SailArch) (AE : ArchExtra SA) <: Arch.
  Import (hints) SA.
  Definition reg := SA.reg.
  #[export] Typeclasses Transparent reg.
  Definition reg_eq : EqDecision reg := SA.reg_eq.
  #[export] Typeclasses Transparent reg_eq.
  Definition reg_countable : Countable reg := SA.reg_countable.
  #[export] Typeclasses Transparent reg_countable.
  Definition pretty_reg : Pretty reg := SA.reg_pretty.
  #[export] Typeclasses Transparent pretty_reg.
  Definition reg_of_string := AE.reg_of_string.
  #[export] Typeclasses Transparent reg_of_string.

  Definition pc_reg := AE.pc_reg.
  #[export] Typeclasses Transparent pc_reg.

  Definition reg_type := SA.reg_type.
  #[export] Typeclasses Transparent reg_type.
  Definition reg_type_eq := SA.reg_type_eq.
  #[export] Typeclasses Transparent reg_type_eq.
  Definition reg_type_countable := SA.reg_type_countable.
  #[export] Typeclasses Transparent reg_type_countable.
  Definition reg_type_inhabited := SA.reg_type_inhabited.
  #[export] Typeclasses Transparent reg_type_inhabited.

  #[export] Instance ctrans_reg_type : CTrans reg_type := @SA.regval_transport.
  #[export] Instance ctrans_reg_type_simpl : CTransSimpl reg_type :=
    @SA.regval_transport_sound.
  #[export] Instance reg_type_eq_dep_dec : EqDepDecision reg_type.
  Proof.
    intros ra rb Heq rva rvb.
    refine (dec_if (decide (ctrans Heq rva = rvb)));
      abstract (dependent destruction Heq; simp ctrans in *; by rewrite JMeq_simpl).
  Defined.

  Definition reg_type_of_gen := AE.reg_type_of_gen.
  #[export] Typeclasses Transparent reg_type_of_gen.
  Definition reg_type_to_gen := AE.reg_type_to_gen.
  #[export] Typeclasses Transparent reg_type_to_gen.

  Definition reg_acc := option SA.sys_reg_id.
  #[export] Typeclasses Transparent reg_acc.
  #[local] Existing Instance SA.sys_reg_id_eq.
  Definition reg_acc_eq : EqDecision reg_acc := _.

  Definition addr_size := SA.addr_size.
  #[export] Typeclasses Transparent addr_size.
  Definition addr_space := SA.addr_space.
  #[export] Typeclasses Transparent addr_space.
  Definition addr_space_eq := SA.addr_space_eq.
  #[export] Typeclasses Transparent addr_space_eq.
  Definition addr_space_countable := SA.addr_space_countable.
  #[export] Typeclasses Transparent addr_space_countable.

  Definition CHERI := SA.CHERI.
  #[export] Typeclasses Transparent CHERI.
  Definition cap_size_log := SA.cap_size_log.
  #[export] Typeclasses Transparent cap_size_log.

  Definition mem_acc := SA.mem_acc.
  #[export] Typeclasses Transparent mem_acc.
  Definition mem_acc_eq : EqDecision mem_acc := _.
  #[export] Typeclasses Transparent mem_acc_eq.
  Definition is_explicit := SA.mem_acc_is_explicit.
  #[export] Typeclasses Transparent is_explicit.
  Definition is_ifetch := SA.mem_acc_is_ifetch.
  #[export] Typeclasses Transparent is_ifetch.
  Definition is_ttw := SA.mem_acc_is_ttw.
  #[export] Typeclasses Transparent is_ttw.
  Definition is_relaxed := SA.mem_acc_is_relaxed.
  #[export] Typeclasses Transparent is_relaxed.
  Definition is_rel_acq_rcpc := SA.mem_acc_is_rel_acq_rcpc.
  #[export] Typeclasses Transparent is_rel_acq_rcpc.
  Definition is_rel_acq_rcsc := SA.mem_acc_is_rel_acq_rcsc.
  #[export] Typeclasses Transparent is_rel_acq_rcsc.
  Definition is_standalone := SA.mem_acc_is_standalone.
  #[export] Typeclasses Transparent is_standalone.
  Definition is_exclusive := SA.mem_acc_is_exclusive.
  #[export] Typeclasses Transparent is_exclusive.
  Definition is_atomic_rmw := SA.mem_acc_is_atomic_rmw.
  #[export] Typeclasses Transparent is_atomic_rmw.

  Definition abort := SA.abort.
  #[export] Typeclasses Transparent abort.

  Definition barrier := SA.barrier.
  #[export] Typeclasses Transparent barrier.
  Definition barrier_eq := SA.barrier_eq.
  #[export] Typeclasses Transparent barrier_eq.
  Definition cache_op := SA.cache_op.
  #[export] Typeclasses Transparent cache_op.
  Definition cache_op_eq := SA.cache_op_eq.
  #[export] Typeclasses Transparent cache_op_eq.
  Definition tlbi := SA.tlbi.
  #[export] Typeclasses Transparent tlbi.
  Definition tlbi_eq := SA.tlbi_eq.
  #[export] Typeclasses Transparent tlbi_eq.
  Definition exn := SA.exn.
  #[export] Typeclasses Transparent exn.
  Definition exn_eq := SA.exn_eq.
  #[export] Typeclasses Transparent exn_eq.
  Definition trans_start := SA.trans_start.
  #[export] Typeclasses Transparent trans_start.
  Definition trans_start_eq := SA.trans_start_eq.
  #[export] Typeclasses Transparent trans_start_eq.
  Definition trans_end := SA.trans_end.
  #[export] Typeclasses Transparent trans_end.
  Definition trans_end_eq := SA.trans_end_eq.
  #[export] Typeclasses Transparent trans_end_eq.
End ArchFromSail.

Module Type ArchFromSailT (SA : SailArch) (AE : ArchExtra SA).
  Include ArchFromSail SA AE.
End ArchFromSailT.

Module IMonFromSail (SA : SailArch) (SI : SailInterfaceT SA)
  (AE : ArchExtra SA) (Arch : ArchFromSailT SA AE) (I : InterfaceT Arch).
  Import Arch.
  Import I.
  Import (coercions) SA.

  Definition MemReq_from_sail (rr : SI.MemReq.t) : MemReq.t :=
    {|MemReq.address := rr.(SI.MemReq.address);
      MemReq.access_kind := rr.(SI.MemReq.access_kind);
      MemReq.address_space := rr.(SI.MemReq.address_space);
      MemReq.size := rr.(SI.MemReq.size);
      MemReq.num_tag := rr.(SI.MemReq.num_tag);
    |}.

  Definition Sail_choose (ct : ChooseType) : I.iMon (choose_type ct) :=
    match ct with
    | ChooseBool ⇒ mchoosef bool
    | ChooseBit ⇒ mchoosef _
    | ChooseInt ⇒ mthrow "Can't choose infinite Int"
    | ChooseNat ⇒ mthrow "Can't choose infinite Nat"
    | ChooseReal ⇒ mthrow "Can't choose infinite Real"
    | ChooseString ⇒ mthrow "Can't choose infinite String"
    | ChooseBitvector n ⇒
        if decide (n < 8)%Z then mchoosef _ else
          mthrow "Can't choose bitvector size over 8"
    | ChooseRange lo hi ⇒ mchoosel $ seqZ lo (hi - lo + 1)%Z
    end.

  Definition Sail_nochoose (ct : ChooseType) : I.iMon (choose_type ct) :=
    match ct with
    | ChooseBool ⇒ mret false
    | ChooseBit ⇒ mret B0
    | ChooseInt ⇒ mret 0%Z
    | ChooseNat ⇒ mret 0%Z
    | ChooseReal ⇒ mthrow "Can't choose Real"
    | ChooseString ⇒ mret ""
    | ChooseBitvector n ⇒ mret (bv_0 _)
    | ChooseRange lo hi ⇒ mret lo
    end.

  Definition Sail_outcome_interp (nondet : bool) {A eo} (out : SI.outcome eo A) : I.iMon A :=
    match out with
    | SI.RegRead reg acc ⇒ mcall (RegRead reg acc)
    | SI.RegWrite reg acc regval ⇒ mcall (RegWrite reg acc regval)
    | SI.MemRead rr ⇒
        mcall (MemRead (MemReq_from_sail rr))
          |$> (λ o, match o with
                    | Ok (val, tags) ⇒ inl (val, tags)
                    | Error a ⇒ inr a
                    end)
    | SI.MemWrite wr val tags ⇒
        mcall (MemWrite (MemReq_from_sail wr) val tags)
          |$> (λ o, match o with
                    | Ok () ⇒ inl (Some true)
                    | Error a ⇒ inr a
                    end)
    | SI.MemAddressAnnounce aa ⇒
        mcall (MemWriteAddrAnnounce (MemReq_from_sail aa))
    | SI.InstrAnnounce _ ⇒ mret ()
    | SI.BranchAnnounce _ _ ⇒ mret ()
    | SI.Barrier b ⇒ mcall (Barrier b)
    | SI.CacheOp cop ⇒ mcall (CacheOp cop)
    | SI.TlbOp top ⇒ mcall (TlbOp top)
    | SI.TakeException fault ⇒ mcall (TakeException fault)
    | SI.ReturnException ⇒ mcall ReturnException
    | SI.TranslationStart ts ⇒ mcall (TranslationStart ts)
    | SI.TranslationEnd te ⇒ mcall (TranslationEnd te)
    | SI.GenericFail msg ⇒ mthrow msg
    | SI.CycleCount ⇒ mret ()
    | SI.GetCycleCount ⇒ mthrow "GetCycleCount not supported"
    | SI.Choose ct ⇒ if nondet then Sail_choose ct else Sail_nochoose ct
    | SI.Discard ⇒ mdiscard
    | SI.Message _ ⇒ mret ()
    | SI.ExtraOutcome e ⇒ mthrow "ExtraOutcome not supported"
    end.

  Fixpoint iMon_from_Sail (nondet : bool) {A eo} (smon: SI.iMon eo A): I.iMon A :=
    match smon with
    | SI.Ret a ⇒ mret a
    | SI.Next out k ⇒
        r ← Sail_outcome_interp nondet out;
        iMon_from_Sail nondet (k r)
    end.
End IMonFromSail.