better dummies generation

.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)

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.

specs/tools/prelude/Makefile

 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

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.

specs/tools/prelude/mk_dummy.sh

-#!/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'

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

specs/tools/purify.pl

+#!/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";
+	}
+} <>;