From 6a90e00d1b4c2974366b628af8766a5a6b354341 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas.schaertl@fau.de> Date: Mon, 27 Apr 2020 11:06:28 +0200 Subject: [PATCH] add coq-cut.sh --- ulo/coq-cut.sh | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100755 ulo/coq-cut.sh diff --git a/ulo/coq-cut.sh b/ulo/coq-cut.sh new file mode 100755 index 0000000..7490d98 --- /dev/null +++ b/ulo/coq-cut.sh @@ -0,0 +1,20 @@ +#! /bin/sh + +# cut out some components from the rdf files exported from Coq +# 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 + +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" -- GitLab