myuon

lemma nat_inducts_all:
  "⋀P n. P 0 ⟹ (⋀n :: nat. (⋀m :: nat. m ≤ n ⟹ P m) ⟹ P (Suc n)) ⟹ P n"
proof-
  fix P and n :: nat
  assume a: "P 0" "⋀n :: nat. (⋀m :: nat. m ≤ n ⟹ P m) ⟹ P (Suc n)"
  show "P n"
    proof (rule nat_less_induct)
      fix na
      assume a2: "∀m<na. P m"
      show "P na"

myuon

lemma ceval_deterministic_lemma: "c %: st ⇓ st' ⟹ (⋀u. c %: st ⇓ u ⟹ st' = u)"
using ceval.induct [of c st st' "λc0 st0 st'0. ((c0 %: st0 ⇓ st'0) ⟶ (∀u. (c0 %: st0 ⇓ u) ⟶ (st'0 = u)))"]
apply rule
apply simp
proof-
  fix u sta
  assume "c %: st ⇓ st'" "c %: st ⇓ u"
  show "(SKIP %: sta ⇓ sta) ⟶ (∀u. (SKIP %: sta ⇓ u) ⟶ sta = u)"
    by (auto, erule ceval.cases, auto, erule ceval.cases, auto)
next

myuon

theory Lambda
imports Main
begin

section {* Lambda Calculus *}
subsection {* Definitions *}

type_synonym var = nat
datatype lambda_p = Var var | Abs' var lambda_p | App' lambda_p lambda_p

myuon

{-# LANGUAGE DataKinds, GADTs, EmptyCase, ViewPatterns, TypeFamilies, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

import Control.Monad
import Test.QuickCheck
import Debug.Trace

data Nat = Z | S Nat deriving (Show)
type N0 = Z
type N1 = S N0

myuon

{-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies, UndecidableInstances, PartialTypeSignatures #-}

-- Nat

data Zero
data Succ n
data Nat n where
  Zero :: Nat Zero
  Succ :: Nat n -> Nat (Succ n)

myuon

module HitBlow where

import System.Random
import Control.Monad
import Data.List

decideNums :: IO [Int]
decideNums = do
  ixs <- forM [0..3] $ \i -> randomRIO (0,9-i)
  return $ fst $ foldl (\(a,a') i -> ((a'!!i):a,delete i a')) ([],[0..9]) ixs

myuon

	Sun Feb 22 21:07 2015 Time and Allocation Profiling Report  (Final)

	   main +RTS -p -RTS

	total time  =       43.20 secs   (43204 ticks @ 1000 us, 1 processor)
	total alloc = 17,430,883,416 bytes  (excludes profiling overheads)

COST CENTRE       MODULE                    %time %alloc

main.paintOf.area Main                       33.6    0.8

myuon

D-Island

ようこそ "D-Island" へ！ あなたはとても楽しいゲームに参加する権利を得た幸運な人です. ゲームは簡単, 相手を欺いて生き残るだけです. さらに幸運なことに, あなたには特別な武器まで差し上げます. もちろん, たださし上げるだけでは面白くありませんから, キチンと条件もつけておいてあげます. あなたほどの人なら, ペナルティなど受けるはずもありませんね.

そうそう, まだ不確定な情報なのですが, 手違いでゲームにはミュータント(突然変異種)が紛れ込んでいるようです. くれぐれもお気をつけて.

myuon

theory MonMonoid
imports Main
begin

locale Monad =
  fixes mreturn and mbind (infixl ">>-" 60)
  assumes left_return: "mreturn a >>- f = f a"
  and     right_return: "m >>- mreturn = m"
  and     assoc: "(m >>- f) >>- g = m >>- (λx. f x >>- g)"

myuon

{-# LANGUAGE GADTs, KindSignatures, DataKinds, FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts, RankNTypes, ConstraintKinds #-}
import GHC.TypeLits
import GHC.Prim (Constraint)
import Control.Monad.State

data SList (k :: Symbol -> Constraint) (a :: Symbol -> *) where
  Nil :: SList k a
  Cons :: k s => a s -> SList k a -> SList k a