coq-cut.sh

#! /bin/sh

# Cut out some components from the rdf files exported from Coq [1]
# that GraphDB does not like. Right now I don't know if they
# are important or if they can be skipped, but I just want a working
# prototype first of all
#
# [1] https://gl.mathhub.info/Coqxml

set -eu

if [ ! $# -eq 1 ]; then
   echo "usage: $0 RDF_FILE" 1>&2
   exit 1
fi

rdf_file="$1"

grep -v -e IsConstructor -e IsInductiveType -e Name \
     -e Target -e Level \
     -e HasInHypothesis -e HasMainConclusion -e HasMainHypothesis \
     -e HasInConclusion -e Variable -e Module -e IsInductive < "$rdf_file"