keigoi

(* Coroutine implementation in OCaml, with Oleg's delimited continuation *)
(* see http://okmij.org/ftp/continuations/implementations.html#caml-shift *)
module D = Delimcc

(* Coroutine yielded a value of type 'a, and will resume with some value of type 'b *)
type ('a, 'b) suspend =
  | Cont of 'a * ('b, ('a,'b) suspend) D.subcont
  | Finish

let start_coroutine f = 

keigoi

(* subtraction on church numerals in Coq *)
Set Printing Universes.
  
(* we always use universe polymorphism, which is later required to define subtraction *)
Polymorphic Definition church : Type := forall X:Type, (X->X) -> (X->X).

Polymorphic Definition zero : church := fun X s z => z.
Polymorphic Definition suc : church -> church := fun n X s z => s (n X s z).

(* as usual *)

keigoi

LOAD CSV WITH HEADERS FROM "https://docs.google.com/spreadsheets/u/0/d/1goCfip58Sq7Th_jVwc-wSAvlINxW2XHsxfh16SGHSro/export?format=csv&id=1goCfip58Sq7Th_jVwc-wSAvlINxW2XHsxfh16SGHSro&gid=0" AS line
FIELDTERMINATOR ','
CREATE (p:Patient {
  id:line.id, age:line.age, sex:line.sex, area:line.area,
  confirm_date:line.confirm_date, note:line.note
})
WITH line
MATCH (p:Patient {id:line.id}) MATCH (p0:Patient {id:line.source_id} )
WHERE line.source_id IS NOT NULL
CREATE (p) -[:FROM{link_kind:line.link_kind}]-> (p0);

keigoi

Scribble parallel loop example

keigoi

function id<A>(x:A): A {
    return x;
}


abstract class Lens<V1, V2, S1, S2> {
    abstract get(s: S1): V1;
    abstract put(s: S1, v:V2) : S2 
}

keigoi

(*
module fase16.adder.Adder;
type <ocaml> "int" from "stdlib" as Int;
global protocol Adder(role C, role S)
{
	choice at C
	{
		Add(Int, Int) from C to S;
		Res(Int) from S to C;
		do Adder(C, S);

keigoi

module type S = sig
  type _ mpst
  type _ sess
  type (_, _, _, _) lens
  type (_, _) label
  type (_, _, _, _) dlabel
  type ('a, 'b, 'c, 'd, 'e, 'f) role = ('a, 'b, 'c, 'd) lens * ('e, 'f) label

  type _ typ

keigoi

Some more details are here (in Japanese)

Students have their projects on the network drive. To optimise build time, we want to put build dir on the local drive. However, we cannot have separate source dirs and build dirs due to the following bug: https://issuetracker.google.com/issues/68936311

An workaround is to turn off AAPT2 (which is discouraged and will not be usable after 2019).

Anyway, the following will do that:

keigoi

module M : sig
  type 'a t
  val return : 'a code -> 'a t
  val (>>=) : 'a t -> ('a code -> 'b t) -> 'b t
  val go : unit t -> unit code
end = struct
  type 'a t = ('a -> unit) code -> unit code
  let return = fun a k -> .< .~k .~a  >.
  let (>>=) m f = fun k -> .< .~(m .< fun x -> .~(f .< x >. k) >. )  >.
  let go : unit t -> unit code = fun m -> m .< fun () -> () >.

keigoi

module M : sig
  type 'a t
  val return : 'a code -> 'a t
  val (>>=) : 'a t -> ('a code -> 'b t) -> 'b t
  val go : unit t -> unit code
end = struct
  type 'a t = ('a -> unit) code -> unit code
  let return = fun a k -> .< .~k .~a  >.
  let (>>=) m f = fun k -> .< .~(m .< fun x -> .~(f .< x >. k) >. )  >.
  let go : unit t -> unit code = fun m -> m .< fun () -> () >.