arademaker

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

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

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

arademaker

% 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

{-# 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

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"

arademaker

-- 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']

arademaker

ar@leme udp % awk '$3 ~ /^(irmã|irmão|pai|mãe|tio|tia|bisavô|bisavó|primo|prima|avô|avó|sobrinho|sobrinha|cunhado|cunhada|parente)$/ {print $2,$3}' *.conllu | sort | uniq -c | sort -nr
1622 pai pai
1283 irmão irmão
 336 tio tio
 336 irmãos irmão
 315 Sobrinho sobrinho
 277 avô avô
 272 primo primo
 256 mãe mãe
 188 sobrinho sobrinho

arademaker

ar@leme workspace % echo $SIGMA_CP
/Users/ar/workspace/sigmakee/build/classes:/Users/ar/workspace/sigmakee/build/lib/*:/Users/ar/workspace/sigmakee/lib/*

ar@leme workspace % java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.InferenceTestSuite -t SP01.kif.tq
Info in KBmanager.initializeOnce()
Info in KBmanager.initializeOnce(): initializing with /Users/ar/.sigmakee/KBs
KBmanager.readConfiguration()
KBmanager.serializedExists(): true
KBmanager.serializedOld(config):
KBmanager.serializedOld(config): save date: Thu May 28 01:48:33 BRT 2020

arademaker

open set

variable {U : Type}

example (A B : set U) : A ∈ powerset (A ∪ B) :=
assume x,
assume : x ∈ A,
show x ∈ A ∪ B, from or.inl ‹x ∈ A›