(*
 An _almost_ working attempt to emulate monads in MetaOcaml.
 It always worked. Alas, this approach lacks dynamism: hence error
 in test2 below.
 The reason is that .<let x = m in f x>. is not monadic bind.
 Bind will be something like .<let x = m in .! (f x)>.
 The reason is that in the former case [f: val->val] whereas in the second
 case [f:val->val code].

 The security kernel, the module Yield below, 
 is supposed to be part of MetaOCaml. MetaOCaml uses Obj.magic to cast
 between the concrete representation of a code value (which is 
 [Parsetree.expression] and the abstract representation, [('a,'b) code].
 We use the same Obj.magic to assign a more specific type to the environment
 qualifier. As far as OCaml is concerned, this is safe because the qualifier
 is purely phantom. If this security kernel were indeed part of MetaOCaml
 kernel, no casts would be needed then.

 Since the code that uses yield and irq_disable has less than fully polymorphic
 qualifier, we really need Yield.run to run the code.

 Joint work with Chung-chieh Shan.

 $Id: yield.ml 2380 2007-06-15 05:34:07Z oleg $
 *)

module Yield : sig
  type enabled
  type 'r disabled

  val yield : (enabled,unit) code

  val irq_disable : ('r disabled,'a) code -> ('r,'a) code

  val run : ('r,'v) code -> ('a,'v) code
  val join : ('r, ('r, 'v) code) code -> ('r,'v) code
end = struct
  type enabled
  type 'r disabled

  let yield = Obj.magic .<print_endline "yielding">.
    (* For simplicity and consistency with the Haskell code,
       we assume no exceptions arize during the execution of [db].
       See the discussion in  the paper. Placing a try block is trivial
       of course. *)
  let irq_disable db = Obj.magic 
      .<begin
        print_endline "Entering the disabled IRQ block";
        let res = .~db in
         print_endline "re-enabling interrupts";
         res
       end>.
  let run cde = Obj.magic cde
  let join cde = .<.! (run .~cde)>.
end;;

open Yield;;

let in_disabled m = 
   let a = .<print_endline "in disabled">. in
   .<begin
    .~a; .~m; 
    (* .~yield; *)
     end>.;;
   

let test1 = .! (run (.<begin
   print_endline "test1";
   .~yield;
   .~(irq_disable (in_disabled .<print_endline "passed action">.));
   (*
   .~(irq_disable (in_disabled .<(print_endline "passed action"; .~yield)>.));
   *)
   .~yield;
   end>.))
;;

(* If we uncomment the commented lines in either [in_disabled] or
   [test1], we get the following error:

This expression has type (Yield.enabled, unit) code
but is here used with type ('a Yield.disabled, 'b) code

Just as the error we get in the Haskell code, yield.hs
*)


let test2 = .! (run (.<begin
   print_endline "test2";
   .~yield;
   let r = ref .<()>. in
   let str = "in disabled" in
   .~(irq_disable (.<
                     let a = .<print_endline "in disabled">. in
		     .~(join .<a>.);
		     print_endline str;
		     (* r := a *)
		     (* r := .<()>. *)
		     >.));

   .~(join .<!r>.); (* here is the benefit of the direct style: cf yield.hs *)
   print_endline "done test2";
   end>.))
;;