Source

ocaml-logicm / logicM_cps.ml

Full commit
let dbg ?t fmt =
  (
   if t = Some `S then Printf.fprintf else Printf.ifprintf
  )
  stdout fmt


module type Monad
 =
  sig
    type 'a m
    val return : 'a -> 'a m
    val bind : ('a -> 'b m) -> 'a m -> 'b m
  end


let ( & ) f x = f x


module LogicT (M : Monad)
 =
  struct
    open M

    type 'a sfkt =
      { sfkt : 'ans . (('ans m), 'a) sk -> ('ans m) fk -> 'ans m }
    and 'ans fk = 'ans Lazy.t
    and ('ans, 'a) sk = 'a -> 'ans fk -> 'ans

    let return e = { sfkt = fun sk fk -> sk e fk }

    let bind f m =
      { sfkt = fun sk fk ->
          m.sfkt (fun a fk2 -> (f a).sfkt sk fk2) fk
      }

    let mzero = { sfkt = fun _sk fk -> Lazy.force fk }

    let mplusl m1 m2l =
      { sfkt = fun sk fk ->
          m1.sfkt sk (lazy ((Lazy.force m2l).sfkt sk fk))
      }

    let mplus m1 m2 =
      { sfkt = fun sk fk ->
          m1.sfkt sk (lazy (m2.sfkt sk fk))
      }

    let ( !! ) l = Lazy.lazy_from_val (Lazy.force l)

    let (liftl : 'a m Lazy.t -> 'a sfkt) = fun m ->
      { sfkt = fun sk fk ->
let () = dbg "lift.%!" in
 M.bind (fun a -> 
let () = dbg "lift-bind.%!" in
sk a fk) (Lazy.force m) }

    let lift m = liftl (Lazy.lazy_from_val m)

    let (reflect : ('a * 'a sfkt) option -> 'a sfkt) = fun r ->
let () = dbg "reflect.%!" in
      match r with
      | None -> mzero
      | Some (a, tmr) -> mplus (return a) tmr

    let (ssk : ('a, 'b) sk) = fun a fk ->
let () = dbg "ssk.%!" in
      M.return (Some (a, (bind reflect (
let () = dbg "ssk1.%!" in
let r = liftl fk in
let () = dbg "ssk2.%!" in
r
))))

    let (msplit : 'a sfkt -> ('a * 'a sfkt) option sfkt) = fun tma ->
let () = dbg "msplit.%!" in
      lift ( (
let () = dbg "lift-tma1.%!" in
            let r = tma.sfkt ssk (lazy (M.return None)) in
let () = dbg "lift-tma2.%!" in
            r
           ))

    let once tma =
      let retfirst r =
        match r with
        | None -> mzero
        | Some (h, _tm) -> return h
      in
        bind retfirst (msplit tma)


    let destruct_bindu tma th el =
      let db r =
        match r with
        | None -> el ()
        | Some (h, tma) -> th h tma
      in
        bind db (msplit tma)


    let destruct_bind tma th el =
      destruct_bindu tma th (fun () -> el)


    let ifteu tma th el =
      let inner r =
        match r with
        | None -> el ()
        | Some (h, t) -> bind th (mplus (return h) t)
      in 
        bind inner (msplit tma)


    let guard cond =
      if cond then return () else mzero

    (******************************************)

    type 'a m = 'a sfkt

    let ( >>= ) m f = bind f m

    let rec interleave m1 m2 =
let () = dbg "il.%!" in
      msplit m1 >>= fun r ->
let () = dbg "msplit-got.%!" in
      match r with
      | None -> m2
      | Some (h, m1') -> mplus (return h) (interleave m2 m1')

    let ( <+> ) = interleave

    let bagof optnum tma =
      let rec inner acc optnum tma =
        let more, optnum =
          match optnum with
          | None -> (true, None)
          | Some n -> (n > 0, Some (n-1))
        in
          dbg "bagof inner\n";
          if more
          then
            msplit tma >>= fun destr ->
              match destr with
              | None -> return acc
              | Some (hd, tma) -> inner (hd :: acc) optnum tma
          else
            return acc
      in
        inner [] optnum tma


    let observe tma =
      let r = ref None in
      ( ( try ignore (
           tma.sfkt (fun a _fk -> (r := Some a; raise Exit)) (lazy (M.return ())))
          with Exit -> ()
        );
        !r
      )

    let runL optnum tma =
      match observe (bagof optnum tma) with
      | None -> dbg "runL none\n"; []
      | Some lst -> dbg "runL some %i\n" (List.length lst); lst

(*
    let runL optnum tma =
      let rec inner optnum acc tma =
        let more, optnum =
          match optnum with
          | None -> (true, None)
          | Some n -> (n <= 0, Some (n-1))
        in
          if more
          then
            tma.sfkt
              (fun sk fk -> sk)
              acc
          else
            acc
      in
        inner [] optnum tma
*)


    (**************)

    open ExtStream

    let rec from_stream s =
let () = dbg "from_stream.%!" in
      match Stream.get_opt s with
      | None -> mzero
      | Some x -> mplusl (return x) (lazy (from_stream s))

    let filter p m =
      m >>= fun x -> if p x then return x else mzero


    let ifm m ~th ~el =
      match observe m with
      | None -> el ()
      | Some _ -> th m


    let impl_name = "cps"

  end