Skip to content

Instantly share code, notes, and snippets.

View alpicola's full-sized avatar

Ryo Tanaka alpicola

View GitHub Profile
@alpicola
alpicola / TypeSystem.v
Last active June 23, 2016 22:42
Strong Normalization for STLC
Require Import Coq.Unicode.Utf8 Arith FunctionalExtensionality String Coq.Program.Equality.
Set Implicit Arguments.
Ltac invert H := inversion H; clear H; subst.
Ltac invert1 H := invert H; [].
Inductive star A (R : A -> A -> Prop) : A -> A -> Prop :=
| StarRefl : forall x,
star R x x
require 'fileutils'
Dir.glob('*_assignsubmission_file_*').each do |filename|
if m = /(.+)_\d+_assignsubmission_file_(.+)/.match(filename)
_, username, orig_filename = *m
FileUtils.mkdir_p(username) # if it exists, do nothing
FileUtils.mv(filename, username + '/' + orig_filename)
end
end
// inspired: http://journal.stuffwithstuff.com/2013/04/23/playing-with-generics-in-typescript-0.9.0/
class Base {
foo() : void {}
}
// If `Derived' has no addional method, we'll get different results
class Derived extends Base {
bar() : void {}
}
@alpicola
alpicola / BTM.scala
Created July 28, 2014 04:41
Biterm Topic Model
// X. Yan, J. Guo, Y. Lan, and X. Cheng, A Biterm Topic Model for Short Texts,
// in WWW. ACM, 2013, pp. 1445–145
import scala.collection._
import scala.io.Source
import scala.util.Random
import java.io._
class BTM(val alpha:Double, val beta:Double, val k:Int, val iterN:Int) {
private var words:Array[String] = null
Definition id {A} : A -> A := fun x => x.
Arguments id {A} / x.
Definition compose {A B C} : (B -> C) -> (A -> B) -> (A -> C)
:= fun g f x => g (f x).
Notation "g 'o' f" := (compose g f) (left associativity, at level 37).
Arguments compose {A B C} f g x /.
@alpicola
alpicola / loop2.egi
Last active December 15, 2015 02:19
(test (match {4 2 1 9} (List Integer)
{[(foldr (lambda [$i $l]
<cons $a_i l>)
<nil>
(between 1 4))
[a_1 a_2 a_3 a_4]]}))
#!/usr/bin/env ruby
require 'thor'
require 'mechanize'
USER = ''
PASS = ''
class Report < Thor
desc 'submit src1 src2 ...', 'Submit code'
@alpicola
alpicola / gist:2049035
Created March 16, 2012 07:53
ITpro Column
#sideNavi,
.leafThemeTitle,
.leafThemeTitleMap,
.themeTopic {
display: none !important;
}
.topTitleBar,
#kijiBox,
.kijiTitle,
#!/usr/bin/env ruby
require 'optparse'
require 'pathname'
require 'tmpdir'
libraries = %w|/Applications/Processing.app/Contents/Resources/Java/core.jar|
compiler = 'scalac'
OptionParser.new {|opt|
opt.on('-w', '--watch') { compiler = 'fsc' }
require 'open-uri'
require 'RMagick'
if ARGV.length != 2
puts 'Usage: ./ame.rb latitude longtitude'
exit
end
url = 'http://tokyo-ame.jwa.or.jp/mesh/100/%s.gif' %
Time.at((Time.now - 30).to_i / 300 * 300).strftime('%Y%m%d%H%M')