Skip to content

Instantly share code, notes, and snippets.

View arademaker's full-sized avatar
🎯
Focusing

Alexandre Rademaker arademaker

🎯
Focusing
View GitHub Profile
@arademaker
arademaker / test.lean
Last active April 22, 2023 19:19
formal semantics example
View test.lean
section TEST
axiom x : Type
axiom e : Type
axiom _man_n_1 : x → Prop
axiom _walk_v_1 : e → x → Prop
-- a man is walking
def h1a : Prop := ∃ e2 x3, _man_n_1 x3 ∧ _walk_v_1 e2 x3
def h1b : Prop := ∃ x3, _man_n_1 x3 ∧ ∃ e2, _walk_v_1 e2 x3
@arademaker
arademaker / processing.hs
Created January 3, 2023 12:51
a Haskell code for parsing a json-lines file apply a simple transformation and serialize a simplified version
View processing.hs
{-# LANGUAGE OverloadedStrings, DeriveGeneric #-}
module Annotation (readData) where
import Data.Aeson
( genericToJSON,
object,
encode,
genericParseJSON,
defaultOptions,
@arademaker
arademaker / config.log
Created August 9, 2022 13:57
config.log from repp compilation
View config.log
This file contains any messages produced by compilers while
running configure, to aid debugging if configure makes a mistake.
It was created by repp configure beta, which was
generated by GNU Autoconf 2.71. Invocation command line was
$ ./configure
## --------- ##
## Platform. ##
@arademaker
arademaker / all-people.lean
Last active July 30, 2022 00:29
lean proof
View all-people.lean
section
constant u : Type
-- constants from MRS
constant named : u → String → Prop
constant compound : u → u → u → Prop
constant _electronics_n_1 : u → Prop
constant _people_n_of : u → u → Prop
constant _go_v_1 : u → u → Prop
constant _to_p_dir : u → u → u → Prop
@arademaker
arademaker / simple.lean
Created February 26, 2021 16:43
simple proof in Lean and show_term
View simple.lean
import tactic
example (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) :=
begin
show_term {
intro h,
have ha := h.left,
have hbc := h.right,
cases hbc with hb hc,
exact or.inl (and.intro ha hb),
@arademaker
arademaker / readme.org
Last active February 25, 2021 02:18
simple data work
View readme.org
pushd ../../raw
wc -l *.raw | awk '$1 < 6 {print $2}' > ../ner/wks/files.all
popd
jq -r '.[].name' documents.json | awk '{gsub(/txt/,"raw"); print}' > files.in
View mathlibtoos.log
% pipx install mathlibtools
ERROR: Command errored out with exit status 1:
command: /Users/ar/.local/pipx/venvs/mathlibtools/bin/python -u -c 'import sys, setuptools, tokenize; sys.argv[0] = '"'"'/private/var/folders/_t/t93k_3n17s916hfg0nb0hfb40000gn/T/pip-install-4zs2ysbb/pyyaml_c2e9947ee533476b87f4aeaa1aec081e/setup.py'"'"'; __file__='"'"'/private/var/folders/_t/t93k_3n17s916hfg0nb0hfb40000gn/T/pip-install-4zs2ysbb/pyyaml_c2e9947ee533476b87f4aeaa1aec081e/setup.py'"'"';f=getattr(tokenize, '"'"'open'"'"', open)(__file__);code=f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' bdist_wheel -d /private/var/folders/_t/t93k_3n17s916hfg0nb0hfb40000gn/T/pip-wheel-6kj_k65w
cwd: /private/var/folders/_t/t93k_3n17s916hfg0nb0hfb40000gn/T/pip-install-4zs2ysbb/pyyaml_c2e9947ee533476b87f4aeaa1aec081e/
Complete output (67 lines):
running bdist_wheel
running build
running build_py
creating build
creating build/lib.macosx-11-x86_64-3.9
@arademaker
arademaker / Merge.hs
Created October 31, 2020 20:59
Merge.hs
View Merge.hs
{-# LANGUAGE DeriveGeneric, OverloadedStrings #-}
import qualified Data.ByteString.Lazy as B
import Data.List
import System.FilePath.Posix
import System.IO
import System.Environment
import Data.Aeson
import Data.Text
import GHC.Generics
@arademaker
arademaker / merge.hs
Last active August 10, 2020 23:02
merge two files
View merge.hs
import Data.List
import System.FilePath.Posix
-- read the files into a list of strings (assuming they are an ordered list of pathnames)
-- convert the list of pathnames into a list of objs
-- merge the list of objs
-- produce the output
-- or http://hackage.haskell.org/package/multiset-0.2.2/docs/Data-MultiSet.html
line1 = "ontonotes-release-5.0/data/files/data/english/annotations/bc/cctv/00/cctv_0000.parse"
View cipher.hs
-- Excerpt From: Graham Hutton. “Programming in Haskell.”
import Data.Char
positions :: Eq a => a -> [a] -> [Int]
positions x xs = [i | (x',i) <- zip xs [0..], x == x']
lowers :: String -> Int
lowers xs = length [x | x <- xs, x >= 'a' && x <= 'z']