arademaker

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

{-# LANGUAGE OverloadedStrings, DeriveGeneric #-}

module Annotation (readData) where

import Data.Aeson
    ( genericToJSON,
      object,
      encode,
      genericParseJSON,
      defaultOptions,

arademaker

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

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