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 () -> () >.

keigoi

Require Import Nat.
Require Import Omega. (* fixme *)

Fixpoint sum (n:nat) : nat :=
  match n with
  | O => O
  | S n => S n + sum n
  end.

Lemma sum_double : forall (n:nat), sum n * 2 = n * (n + 1).

keigoi

(* check the behaviour of Coq's rewrite tactics *)

Parameter T : Type.

Lemma mmm1 : forall (x y:T) (p : x = y),
    existT (fun (y':T) => x = y') y p = existT (fun (y':T) => x = y') x (eq_refl x).
Proof.
  intros.
  rewrite p.
  reflexivity.

keigoi

(* compile with ppx_implicits ab783d180c35 (0.3.1) *)
(* ocamlfind ocamlc -c -package ppx_implicits implicit_polyvar.ml *)

module Read = struct
  type 'a t = (string -> 'a, [%imp Readers]) Ppx_implicits.t
  let unpack : 'a t -> string -> 'a = fun d -> Ppx_implicits.imp ~d
end

let read ?(_reader:'a Read.t option) = match _reader with Some x -> Read.unpack x | None -> failwith "no instance"