From 18706238fa3b1ba34dcc4fe5ef85dd783a6e885a Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Fri, 21 Feb 2020 13:52:39 +0100
Subject: [PATCH] script making top file
---
.gitignore | 2 ++
prelude/cert_f/prelude.lp | 2 --
prelude/core/prelude.lp | 2 --
tools/mk_top.sh | 12 ++++++++++++
4 files changed, 14 insertions(+), 4 deletions(-)
create mode 100644 .gitignore
delete mode 100644 prelude/cert_f/prelude.lp
delete mode 100644 prelude/core/prelude.lp
create mode 100755 tools/mk_top.sh
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..50f8e6f
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+# Ignore generated top files
+top.lp
diff --git a/prelude/cert_f/prelude.lp b/prelude/cert_f/prelude.lp
deleted file mode 100644
index 3aeb65a..0000000
--- a/prelude/cert_f/prelude.lp
+++ /dev/null
@@ -1,2 +0,0 @@
-require prelude.cert_f.booleans prelude.cert_f.equalities
-prelude.cert_f.naturalnumbers prelude.cert_f.notequal
diff --git a/prelude/core/prelude.lp b/prelude/core/prelude.lp
deleted file mode 100644
index 39bb6db..0000000
--- a/prelude/core/prelude.lp
+++ /dev/null
@@ -1,2 +0,0 @@
-require encodings.pvs_core prelude.core.booleans prelude.core.equalities
-prelude.core.notequal prelude.core.if_def
diff --git a/tools/mk_top.sh b/tools/mk_top.sh
new file mode 100755
index 0000000..9a00cdf
--- /dev/null
+++ b/tools/mk_top.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+## [./mk_top.sh d] creates a file [d/top.lp] importing all files in [d/]
+
+out="top.lp"
+
+( cd "$1" || exit
+ rm "${out}"
+ for f in *.lp; do
+ p=$(printf '%s/' "$1" | tr -s '/' '.')
+ printf 'require %s%s\n' "${p}" "${f%.lp}" >> "${out}"
+ done )
--
GitLab