camlspotter

(*

OCaml translation of the ideas explained in http://fumieval.hatenablog.com/entry/2014/09/22/144401

To emulate the higher kinded polymorphism, the technique used explained in https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf

*)

module StateMonad = struct
  type ('s, 'a) m = 's -> 's * 'a

yamashita1238

:- use_module(library(socket)).

write_atom(Stream,Atom) :-
  atom_codes(Atom,Codes),
  write_codes(Stream,Codes).

write_codes(_,[]) :- !.
write_codes(Stream,[Code|Tail]) :-
  put_code(Stream,Code),
  write_codes(Stream,Tail).

fetburner

Require Import Arith Div2 Omega Recdef.

Function bsearch (p : nat -> bool) n { wf lt n } :=
  match n with
  | O => 0
  | _ =>
      let m := div2 n in
      if p m then bsearch p m
      else S m + bsearch (fun x => p (S m + x)) (n - S m)
  end.