kencoba

(ns fmf20101205
  (:use L5 L5.layout)
  (:import [java.awt Color]))

(defcontext
  {:width 640 :height 480
   :font-family "Gill Sans"
   :font-size 30
   :color (Color/darkGray)
   :background-color Color/white})

kencoba

(ns Verified_Programming_in_Guru
  (:use L5 L5.layout))

(defcontext
  {:width 640 :height 480
   :font-family "Gill Sans"
   :font-size 25})

(defmacro code [& body]
  `(with {:font-family "ＭＳ ゴシック" :font-size 14}

kencoba

(use 'clojure.contrib.str-utils)

(def digits {"零" 0 "一" 1 "二" 2 "三" 3 "四" 4 "五" 5 "六" 6 "七" 7 "八" 8 "九" 9})

(defn- str-first [s]
  (str (.charAt s 0)))

(defn- trans-ichi [s]
  (let [n (re-find #"[一二三四五六七八九]$" s)]
    (if (nil? n) 0 (digits n))))

kencoba

/*

http://d.hatena.ne.jp/a-san/20090626/p2
*/

abstract sig State {
	transient:set State
}
one sig O,A,B,C,D,E,F,G,H,I extends State {}

kencoba

(ns
    ^{:doc
      "Simple Theorem Prover 'Programming Language Theory and its Implementation' Michael J.C. Gordon"
      :author "Kenichi Kobayashi"}
  prover
  (:use [clojure.test])
  (:require [clojure.walk :as cw]))

(def constant #{'+ '- '< '<= '> '>= '* '= 'T 'F 'DIV 'not 'and 'or 'implies})

kencoba

;;; cells.clj -- simple data-flow extension for Clojure

;; by Stuart Sierra, http://stuartsierra.com/
;; September 20, 2008

;; Based on Ken Tilton's Cells package for Common Lisp,
;; http://common-lisp.net/project/cells/

;; Copyright (c) 2008 Stuart Sierra. All rights reserved.  The use and
;; distribution terms for this software are covered by the Common

kencoba

(ns n-indexed
  (:require [clojure.contrib.seq-utils :as s])
  (:use [clojure.test]))

(defn n-indexed [s]
  (cond (not (coll? s)) s
	(not (coll? (first s))) (s/indexed s)
	:else (reduce concat
		      (for [[i ls]  (s/indexed (map n-indexed s))]
			(map #(cons i %) ls)))))

kencoba

(use 'clojure.contrib.trace)

(defn fact-gen [fact-in]
  (fn [n]
    (if (= n 0)
      1
      (* n (fact-in (- n 1))))))

(defn Y [r]
  ((fn [f] (f f))

kencoba

(defn eval-expr [expr]
  (loop [f expr]
    (let [fst (nth f 0)
	  op1 (nth f 1)
	  scd (nth f 2)]
      (if (= (count f) 3) (op1 fst scd)
	  (let [op2 (nth f 3)
		thd (nth f 4)
		rst (drop 5 f)]
	    (if (or (= op2 #'+) (= op2 #'-))

kencoba

(use '[clojure.contrib.combinatorics :only (permutations)])

(for [pattern (permutations [1 2 3 4 5 6 7 8 9])      
      :when
      (let [a1 (nth pattern 0)
	    a2 (nth pattern 1)
	    a3 (nth pattern 2)
	    b1 (nth pattern 3)
	    b2 (nth pattern 4)
	    b3 (nth pattern 5)