einblicker

open System
open Microsoft.FSharp.Quotations
open Microsoft.FSharp.Quotations.ExprShape
open Microsoft.FSharp.Linq.QuotationEvaluation
 
module Util =
  let rnd = new Random()
  let (|Range|_|) min max x =
    if min <= x && x <= max then Some() else None
 

einblicker

Section CultOfLoveDoesNotExist.

Variable human : Set.
Variable P : human -> Prop. (* xは愛の教団に属する *)
Variable L : human -> human -> Prop. (* xはyを愛する *) 

Theorem CultOfLoveDoesNotExist
 (forall x : human, P x -> forall y : human, ~ L y y -> L x y) /\
 (forall x : human, P x -> forall y : human, L x y -> ~ L y y) ->
 ~ (exists x : human, P x).

einblicker

Section HungryIsImmutable.

CoInductive hungry := h : (nat -> hungry) -> hungry.

CoFixpoint f := h (fun _ => f).

Definition unH x :=
  match x with
  | h f => f 
  end.

einblicker

class Hungry(f: Int => Hungry) {
  def apply(n: Int) = f(n)
}

val f: Hungry = new Hungry(_ => f)

f(0)
f(0)(1)(2)
f(0)(1)(2)(3)(4)(5)

einblicker

import scalaz._
import Scalaz._

trait REQUAL[A, B] {
  def apply[C[_, _]](
    x: Forall[({type X[D]=C[D, D]})#X]
  ): C[A, B]
}

einblicker

Parameter A : Prop.

Goal (forall X : Prop, (A -> X)) -> (A -> (forall X : Prop, X)).
intros.
apply H.
assumption.
Qed.

Goal (A -> (forall X : Prop, X)) -> (forall X : Prop, (A -> X)).
intros.

einblicker

module FPStyle =

  [<AbstractClass>]
  type Eq<'A, 'B> private () =
    abstract F : 'A -> 'B
    abstract G : 'B -> 'A
    static member Id<'A>() =
      { new Eq<'A, 'A>() with
        member this.F(x) = x
        member this.G(x) = x }

einblicker

object RSEncoder {
  def encode(raw_code: Array[Int]) = {
    val gf = GaloisField.a8

    val g_index = Array(
      43, 139, 206, 78, 43, 239, 123, 206, 214,
      147, 24, 99, 150, 39, 243, 163, 136
    )

    val code =

einblicker

class GaloisField private (val gf_index: Int) {
  private val gf_bit: Int =
    if (gf_index == 4) (1 << 1) | 1
    else if (gf_index == 8) (1 << 4) | (1 << 3) | (1 << 2) | 1
    else sys.error("undefined")

  private val pow_table = Array.fill(256)(0)
  private val root_table = Array.fill(256)(0)

  locally {

einblicker

let dummyVal () = failwith "dummy";;

class virtual ['a] dir (dummy : (unit -> 'a)) = object
  method virtual format_aux : string -> 'a
end;;

class d_end = object
 inherit [string] dir dummyVal
 method format_aux =
  fun out -> out