Skip to content

Instantly share code, notes, and snippets.

View DreamLinuxer's full-sized avatar

Chao-Hong Chen DreamLinuxer

26 followers · 72 following
View GitHub Profile
@DreamLinuxer
DreamLinuxer / self_rep.c
Created November 15, 2012 02:21
self reproduce maker
char s[]={109,97,105,110,40,41,10,123,10,105,110,116,32,105,59,10,112,114,105,110,116,102,40,34,99,104,97,114,32,115,91,93,61,123,34,41,59,10,102,111,114,40,105,61,48,59,115,91,105,93,59,43,43,105,41,112,114,105,110,116,102,40,34,37,100,44,34,44,115,91,105,93,41,59,10,112,114,105,110,116,102,40,34,48,125,59,37,99,34,44,49,48,41,59,10,112,114,105,110,116,102,40,34,37,115,34,44,115,41,59,10,125,0};
main()
{
int i;
printf("char s[]={");
for(i=0;s[i];++i)printf("%d,",s[i]);
printf("0};%c",10);
printf("%s",s);
}
@DreamLinuxer
DreamLinuxer / debug.log
Created November 15, 2012 08:09
GDB script example
Reading symbols from ~/gist/gist-4077328/gdb_test...done.
Breakpoint 1 at 0x4005cf: file gdb_test.c, line 7.
Breakpoint 1, output (val=91652772) at gdb_test.c:7
7 printf("OUTPUT: %X\n",val);
#0 output (val=91652772) at gdb_test.c:7
#1 0x0000000000400632 in rand_output (prev=4294967295, mid=1073741824, mask=2147483647) at gdb_test.c:16
#2 0x000000000040066a in main () at gdb_test.c:23
Breakpoint 1, output (val=4481602) at gdb_test.c:7
@DreamLinuxer
DreamLinuxer / c-num.scm
Last active December 19, 2015 23:49
Church numeral
(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
(lambda (f) (lambda (x) (f ((n f) x)))))
; n := apply f to x n times
(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))
(define (add a b)
(lambda (f) (lambda (x)
@DreamLinuxer
DreamLinuxer / filter.agda
Last active January 14, 2016 05:14
module filter where
data Bool : Set where
true false : Bool
data List (A : Set) : Set where
[] : List A
_::_ : A → List A → List A
infix 4 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
@DreamLinuxer
DreamLinuxer / compo.agda
Created January 15, 2016 03:02
_∘_ : ∀ {α β γ}
→ {A : Set α} {B : A → Set β} {C : {x : A} → B x → Set γ}
→ (f : {x : A} → (y : B x) → C y)
→ (g : (x : A) → B x)
→ ((x : A) → C (g x))
(f ∘ g) x = f (g x)
_∘′_ : ∀ {α β γ}
→ {A : Set α} {B : Set β} {C : Set γ}
→ (B → C) → (A → B) → (A → C)
@DreamLinuxer
DreamLinuxer / nat.agda
Created February 6, 2016 20:42
module nat where
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
indℕ : ∀ {ℓ} → (C : ℕ → Set ℓ) → C 0 → ((n : ℕ) → C n → C (suc n)) → (n : ℕ) → C n
indℕ C z f 0 = z
indℕ C z f (suc n) = f n (indℕ C z f n)
iter : ∀ {ℓ} (C : Set ℓ) → C → (C → C) → ℕ → C
@DreamLinuxer
DreamLinuxer / bench.plt
Created March 9, 2016 04:48
set datafile separator ","
set terminal postscript eps enhanced color font 'Helvetica,20'
set output 'cold-hot.eps'
set xrange [1:18]
set yrange [2000:20000]
set xlabel 'Thread number'
set ylabel 'ops/ms'
plot '1448725779_G0.5-I0.25_pure.csv' using 1:2:3 title 'PureMap' with yerrorlines pointtype 4 pointsize 2, '1448725779_G0.5-I0.25_ctrie.csv' using 1:2:3 title 'Ctrie' with yerrorlines pointtype 7 pointsize 2, '1448725779_G0.5-I0.25_adaptive.csv' using 1:2:3 title 'AdaptiveMap' with yerrorlines pointtype 8 pointsize 2
@DreamLinuxer
DreamLinuxer / T.agda
Created August 20, 2016 21:08
module T where
Ḳ : {X Y : Set} → X → Y → X
Ḳ x y = x
Ṣ : {X Y Z : Set} → (X → Y → Z) → (X → Y) → X → Z
Ṣ f g x = f x (g x)
_∘_ : {X Y Z : Set} → (Y → Z) → (X → Y) → (X → Z)
g ∘ f = λ x → g (f x)
@DreamLinuxer
DreamLinuxer / Prod.hs
Last active November 8, 2016 04:35
{-@ LIQUID "--higherorder" @-}
{-@ LIQUID "--totality" @-}
{-@ LIQUID "--exactdc" @-}
module Data.VerifiedMonoid.Instances.Prod ({-vmonoidProd-}) where
--import Data.VerifiedMonoid
import Language.Haskell.Liquid.ProofCombinators
{-@ axiomatize identProd @-}
@DreamLinuxer
DreamLinuxer / grade.py
Created September 27, 2017 17:47
#!/usr/bin/env python
import subprocess32 as subprocess
import sys
import os
test_inputs = [[4,1,1],[6,2,3],[8,4,4],[11,9,8],[15,7,2]]
def get_name(s):
return s[0:s.index('_')]