test.v

Require Import Koika.Frontend.
Require Import Koika.Std.

Module Simple.
  Inductive reg_t := total.

  Definition R r :=
    match r with
    | total => bits_t 32
    end.

  Definition r idx : R idx :=
    match idx with
    | total => Bits.zero
    end.

  Inductive ext_fn_t := f1 | do_zero_i | total_o.

  Definition Sigma (fn: ext_fn_t) :=
    match fn with
    | f1 => {$ bits_t 1 ~> bits_t 32 $}
    | do_zero_i => {$ bits_t 1 ~> bits_t 1 $}
    | total_o => {$ bits_t 32 ~> bits_t 1 $}
    end.

  Inductive rule_name_t := add_to_total_o | zero_total_o | write_back.

  Definition _add_to_total_o : uaction reg_t ext_fn_t :=
    {{ let previous_total := read0(total) in
       let input := extcall f1( Ob~1 ) in
       write0(total, input + previous_total)
    }}.

  Definition _zero_total_o : uaction reg_t ext_fn_t :=
    {{ let do_zero := extcall do_zero_i( Ob~1 ) in
       if do_zero then
         write0(total, #(Bits.of_nat 32 0))
       else fail
    }}.

  Definition _write_back : uaction reg_t ext_fn_t :=
    {{ let previous_total := read0(total) in
       let drop := extcall total_o ( previous_total ) in pass
    }}.

  Definition simple_device : scheduler :=
    write_back |> zero_total_o |> add_to_total_o |> done.

  Definition rules :=
    tc_rules R Sigma
             (fun r => match r with
                    | add_to_total_o => _add_to_total_o
                    | zero_total_o => _zero_total_o
                    | write_back => _write_back
                    end).

  Definition cr := ContextEnv.(create) r.

  Definition test_sigma1 (fn: ext_fn_t) : Sig_denote (Sigma fn) :=
    match fn with
    | f1 => fun _ => Bits.of_nat 32 1
    | do_zero_i => fun _ => Bits.zero
    | total_o => fun _ => Bits.zero
    end.
  Definition test_sigma2 (fn: ext_fn_t) : Sig_denote (Sigma fn) :=
    match fn with
    | f1 => fun _ => Bits.of_nat 32 1
    | do_zero_i => fun _ => Bits.of_nat 1 1
    | total_o => fun _ => Bits.zero
    end.

  Definition ext_fn_specs (fn: ext_fn_t) :=
    match fn with
    | f1 => {| efr_name := "f1"; efr_internal := true |}
    | do_zero_i => {| efr_name := "f2"; efr_internal := true |}
    | total_o => {| efr_name := "f3"; efr_internal := true |}
    end.

  Definition package :=
    {| ip_koika := {| koika_reg_types := R;
                     koika_reg_init := r;
                     koika_ext_fn_types := Sigma;
                     koika_rules := rules;
                     koika_rule_external := (fun _ => false);
                     koika_scheduler := simple_device;
                     koika_module_name := "simple_device" |};

       ip_sim := {| sp_ext_fn_specs fn := {| efs_name := show fn; efs_method := false |};
                   sp_prelude := None |};

       ip_verilog := {| vp_ext_fn_specs := ext_fn_specs |} |}.
End Simple.

Definition prog := Interop.Backends.register Simple.package.
Extraction "simple.ml" prog.