keigoi

abstract sig Digit {}
one sig One, Two, Three, Four, Five, Six, Seven, Eight, Nine extends Digit {}

sig Cell {
  content: Digit,
  adjacent : set Cell
}

abstract sig Group {
  cells: set Cell

keigoi

package session;

import java.util.function.Function;
import java.util.function.Supplier;

/**
 * Proof-of-concept implementation of session types (including delegation and
 * recursion) in Java. Session channels are assigned on slots _0, _1, _2, etc.
 * This is WIP; no accept/connect. A type Proc<Cons<C0,Cons<C1,..>>> means that
 * process uses session channel at _0 as C0, _1 as C1, ...

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

module Channel : sig
  type 'a t
  type _ gen = SendG : [`send of 'a] gen | RecvG : [`recv of 'a] gen
  type 'a u = U                                       
  (* val send : [`send of 'a] t -> 'a -> unit *)
  (* val receive : [`recv of 'a] t -> 'a *)
  (* val create : 'b u -> ([<`send of 'b | `recv of 'b] as 'a) gen -> 'a t *)
end = struct
  type _ t = Send : 'a Event.channel -> [`send of 'a] t | Recv : 'a Event.channel -> [`recv of 'a] t
  (* type 'a t = 'a Event.channel *)

keigoi

foobar

keigoi

(* compile with ppx_implicits 0.2.0 *)
(* ocamlfind ocamlc -c -package ppx_implicits implicit_read.ml *)
module Read = struct
  type 'v t = (string -> 'v option, [%imp Instances]) Ppx_implicits.t
                 
  let read ?(d:'v t option) x = Ppx_implicits.imp ?d x
end

module Instances = struct
  let _int : string -> int option = fun s ->

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"

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

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

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