takada-at

次につくるもの。

エクスポート画面。とりあえずダウンロードボタンがあって、以下のような形でzipでまとめてダウンロードできればOK

zip:
   master/
     <table name>.csv
     <table name>.csv
   sound_bank/
      xxx.bnk

takada-at

まえおき

TaPL24章に、存在型を使って全称型を表現できるか?という問題がある(演習24.3.3。邦訳p.297)。

解答には「このことをきちんと書き下したものは見たことがない。これは可能であるはずだが、その変形は局所的な構文糖衣では済まないだろう」としか書いてないので解答が気になっている。

参考: 全称型を使って存在型を表現する場合

これは教科書にある。

{Some X, T} =def All Y. (All X. T->Y) -> Y

takada-at

-- definition of Existential Type
data ∃ {A : Set} (B : A → Set) : Set where
     _,_ : (x₁ : A) → B x₁ → ∃ \(x : A) → B x


-- left projection
p : {A : Set} {B : A → Set} → (∃ \(x : A) → B x) → A
p {A} {B} (a , b) = a

-- right projection

takada-at

open Format
open Syntax
open Support.Error
open Support.Pervasive

(* ------------------------   EVALUATION  ------------------------ *)

exception NoRuleApplies

let rec isnumericval t = match t with

takada-at

open import Relation.Binary.PropositionalEquality

-- 存在型
data ∃ {A : Set} (B : A → Set) : Set where
     _,_ : (x₁ : A) → B x₁ → ∃ \(x : A) → B x

-- ORの定義
infixl 8  _∨_
data _∨_ (P Q : Set) : Set where
  or-introl : P → P ∨ Q

takada-at

• fullpoly
• fullomega

全称型

型適用

(λX.t)[T]→[X→T]t

takada-at

https://github.jp.klab.com/studio-management/boomerang/pull/325

二回目のアップロードの処理改善のメモ。

上のPRに関して、認識している問題。

1. アップロードしたExcelをダウンロードすると、色づけがおかしい。すべて「追加」になっている。
2. 削除されたシートが表示されない。差分表示としては、削除されたシートも含めるのが正解。
3. ダウンロード時にファイルが壊れて開けないことがある。

takada-at

from py4j.java_gateway import JavaGateway


class py4ApachePOI(object):
  def __init__(self):
    self.gateway = None
    self.process = None
    self.gateway = JavaGateway()

  def openFile(self, fileName):

takada-at

-- Definitions
module hm where

data ⊥ : Set where

data V : Set where
  i : V

data _∧_ (φ ψ : Set) : Set where
  and-intro : φ → ψ → φ ∧ ψ

takada-at

import os
import pwd
from subprocess import Popen
from optparse import OptionParser

myenv  = """alias pythonexec='time ionice -n 7 -c 2 nice -n 19 {workdir}/bin/python'
alias rsyncd='rsync --daemon  --verbose --port=11874 --config={home}/LOCAL/takada-at/rsync.conf --no-detach'
"""
screenrc = """escape  ^T^T
defutf8 on