From 9e62b1a8876289d6eec21ace2b4cfed65823f681 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Mon, 1 Nov 2021 12:36:49 +0100
Subject: [PATCH] better dummies generation
---
.github/workflows/check_encoding.yml | 2 +-
specs/tools/README.md | 1 +
specs/tools/prelude/Makefile | 20 ++++++++++------
specs/tools/prelude/README.md | 11 ++++-----
specs/tools/prelude/mk_dummy.sh | 12 ----------
specs/tools/prelude/theories | 4 ++--
specs/tools/purify.pl | 36 ++++++++++++++++++++++++++++
7 files changed, 58 insertions(+), 28 deletions(-)
delete mode 100755 specs/tools/prelude/mk_dummy.sh
create mode 100755 specs/tools/purify.pl
diff --git a/.github/workflows/check_encoding.yml b/.github/workflows/check_encoding.yml
index 8485b7a..1a12ddf 100644
--- a/.github/workflows/check_encoding.yml
+++ b/.github/workflows/check_encoding.yml
@@ -44,7 +44,7 @@ jobs:
# Runs a set of commands using the runners shell
- name: install lambdapi and deps
run: |
- sudo apt install --yes bmake
+ sudo apt install --yes bmake ksh perl
(cd "${GITHUB_WORKSPACE}/lambdapi/" || exit 1
opam install .)
eval $(opam env)
diff --git a/specs/tools/README.md b/specs/tools/README.md
index ff257bf..2637ab6 100644
--- a/specs/tools/README.md
+++ b/specs/tools/README.md
@@ -6,6 +6,7 @@ to Dedukti files.
- `pvs2dk.sh`: translate a theory to a lambdapi file.
- `lambdapi.pkg`: the module file for lambdapi (required to type check files).
+- `purify.pl`: trims unneeded data from theory specification files
- `lambdapi.mk`: some targets and rules to typecheck lambdapi files.
- `prelude_patches/*.diff`: patches that may be apply to the Prelude to
translate it.
diff --git a/specs/tools/prelude/Makefile b/specs/tools/prelude/Makefile
index 2e1b329..975170c 100644
--- a/specs/tools/prelude/Makefile
+++ b/specs/tools/prelude/Makefile
@@ -1,19 +1,25 @@
PVS2DK = ../pvs2dk.sh
LP = lambdapi
-THEORIES != grep -v -E '^-|\#' theories
PVSPATH ?=
-all: dummy ${THEORIES:C/$/.lpo/}
+_THEORIES != ../purify.pl -p < theories
+_DUMMIES != ../purify.pl -n < theories
+# We cannot cat _THEORIES and _DUMMIES because order is important
+_ALL != ../purify.pl < theories
-.PHONY: dummy
-dummy:
- ./mk_dummy.sh
+all: ${_ALL:C/$/.lpo/}
+translate: ${_ALL:C/$/.lp/}
-translate: dummy ${THEORIES:C/$/.lp/}
+.for d in ${_DUMMIES}
+${d}.lp:
+ set -o noclobber && printf '// Dummy theory\n' > ${d}.lp
+${d}.lisp:
+ set -o noclobber && printf '(:context nil :decls nil)' > ${d}.lisp
+.endfor
# For each theory, translate it and apply a patch if it exists
-.for th in ${THEORIES}
+.for th in ${_THEORIES}
${th}.lp:
PVSPATH=${PVSPATH} ${PVS2DK} -f ${PVSPATH}/lib/prelude.pvs -t ${.TARGET:R} \
-o ${PWD}/${.TARGET} > /dev/null
diff --git a/specs/tools/prelude/README.md b/specs/tools/prelude/README.md
index 1afc718..8c4aea5 100644
--- a/specs/tools/prelude/README.md
+++ b/specs/tools/prelude/README.md
@@ -24,10 +24,9 @@ make functions.lpo
```
The theories of the Prelude are registered in the file `theories`. In this file,
-each line is a theory. One-line comments can be inserted with character `#` *at
-the beginning of the line*.
+each line is a theory. One-line comments can be inserted with character `#`.
If a theory name is prefixed with a dash `-`, the theory is not translated nor
-type-checked. Instead, an empty file is created with the name of the theory by
-`mk_dummy.sh`. This allows to translate and type check theories that are
-defined further in the prelude, but do not depend on them, as theories of
-prelude require (syntactically) all previous prelude theories.
+type-checked. Instead, an empty file is created with the name of the theory by.
+This allows to translate and type check theories that are defined further in
+the prelude, but do not depend on them, as theories of prelude require
+(syntactically) all previous prelude theories.
diff --git a/specs/tools/prelude/mk_dummy.sh b/specs/tools/prelude/mk_dummy.sh
deleted file mode 100755
index b18503d..0000000
--- a/specs/tools/prelude/mk_dummy.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/ksh
-set -euo pipefail -o noclobber
-
-while read -r line; do
- # Remove comments from line
- nocom=$(print -f "$line" | sed -e 's/^\([^#]*\).*$/\1/' | tr -d '[:space:]')
- if (print -f "${nocom}" | grep -E -q '^-'); then
- fname="${nocom:1}"
- [ -r "${fname}.lp" ] || printf '// Dummy theory\n' > "${fname}.lp"
- [ -r "${fname}.lisp" ] || printf '(:context nil :decls nil)' > "${fname}.lisp"
- fi
-done < 'theories'
diff --git a/specs/tools/prelude/theories b/specs/tools/prelude/theories
index 319511d..79a1031 100644
--- a/specs/tools/prelude/theories
+++ b/specs/tools/prelude/theories
@@ -44,7 +44,7 @@ function_props
-function_props_alt # Only overloading
function_props2
relation_defs
--relation_props
+-relation_props # Overload the composition operator
-relation_props2
relation_converse_props
indexed_sets
@@ -82,7 +82,7 @@ nat_fun_props
-restrict_set_props # Depends on finite_sets
-extend_set_props # Depends on finite_sets
-function_image_aux # Depends on finite_sets
--function_iterate # Recursive function definition
+function_iterate
sequences
seq_functions
-finite_sequences # Use dependent records
diff --git a/specs/tools/purify.pl b/specs/tools/purify.pl
new file mode 100755
index 0000000..2b65652
--- /dev/null
+++ b/specs/tools/purify.pl
@@ -0,0 +1,36 @@
+#!/usr/bin/perl
+use strict;
+use warnings;
+
+=pod
+
+=head1 Theory specification sanitiser
+
+This script sanitises a theory specification. The flag C<-n> selects negative
+lines (lines preceded with a -) while the flac C<-p> selects positive lines
+(not preceded with a -). If no flag is given, all lines are printed and
+sanitised.
+
+=cut
+
+use Getopt::Std;
+getopts('np');
+our($opt_n, $opt_p);
+
+map {
+ $_ =~ s/#.*$//;
+ $_ =~ s/^\s+//;
+ $_ =~ s/\s+$//;
+ if ($opt_n && /^-/) {
+ # Print negative theories
+ $_ =~ s/^-(.*)$/$1/;
+ print "$_\n";
+ } elsif ($opt_p) {
+ # Print positive theories
+ print "$_\n" if /^[^-]/;
+ } elsif (! ($opt_n || $opt_p)) {
+ # Print all theories
+ $_ =~ s/^-?(.*)$/$1/;
+ print "$_\n";
+ }
+} <>;
--
GitLab