genTransMFormFunc.pl revision fbf66630978e9a8d85a130211628fe4694ba3664
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder# usage:
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder# genInlines.pl Modal/GeneratePatterns.inline.hs.in Modal/ModalSystems.hs
75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder# substitute ##<WORD> with Haskell code snippits
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederuse strict;
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederuse File::Basename;
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermy $disclaimer = '"Remove this trace when Results from map_sign are available\\n"';
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder# subtitutions with common parts of Modal- and CASL-formulas
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermy %substs =
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder ("�!modalAx" =>
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder "inlineAxioms Modal \"modality empty\\n".
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder"pred p,q:()\\n".
fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maeder". ",
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder "�!caslAx" =>
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder "inlineAxioms CASL \"sort world \\n".
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder"pred rel : world * world\\n".
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder"forall w1 : world \\n. ");
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maedermy $input = "";
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maedermy ($infile,$outfile) = @ARGV;
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder# Argument processing
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder###unless ($infile eq "DEBUG") {
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederdie "exactly one in- and one out-file needed!!" unless @ARGV == 2;
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maedermy $outfile1 = join "", (fileparse($infile,'\.in'))[1,0];
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederprint STDERR "Generating $outfile1\n";
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder# open the first two files
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederopen IN, "<$infile" or die "cannot read \"$infile\"";
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederopen OUT, ">$outfile1" or die "cannot write to \"$outfile1\"";
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder# perform the substitutions
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederwhile (<IN>) {
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder foreach my $key (keys %substs) {
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder s/$key\"/$substs{$key}/ge;
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder }
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder print OUT $_;
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder}
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
38775225cf810f5895cc03b4acbcfe8f84f2513aChristian Maederclose IN;
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederclose OUT;
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder# call outlineAxioms and get the result imidiately
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder$input = `utils/outlineAxioms $outfile1`;
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederif($? >> 8) {
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder print STDERR "outlineAxioms detected an error\n";
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder exit 5;
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder}
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder###}
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder###if ($input eq "") {
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder### $input = join("",<STDIN>);
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder###}
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder# process the output of outlineAxioms (further called input)
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder$input =~ s,^.*snip\s+><\s+Patterns(.*)snip\s+>/<\s+Patterns,$1,s;
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder$input =~ s/^\s*\[\(\[\[//s;
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder$input =~ s/(\})\]\]\)\]\s*$/$1/s;
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder# print "$input\n";
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder# split the input into pairs
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maedermy @input = split(/\]\]\),\s+?\(\[\[/s, $input);
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederprint STDERR "Generating $outfile\n";
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder# open the outputfile and print out the header
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederopen OUT, ">$outfile" or die "cannot write to \"$outfile\"";
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederprint OUT '{- look but don\'t touch !!
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maedergenerated by utils genFunction.pl -}
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maedermodule Modal.ModalSystems (transSchemaMFormula) where
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Debug.Trace
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Common.PrettyPrint
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederimport Common.AS_Annotation
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- CASL
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport CASL.Logic_CASL
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport CASL.AS_Basic_CASL
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder-- ModalCASL
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederimport Modal.AS_Modal
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Modal.Print_AS
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Modal.Utils
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedertransSchemaMFormula :: ([VAR] -> TERM M_FORMULA -> TERM ())
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -> SORT -> PRED_NAME -> [VAR]
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -> AnModFORM -> Maybe (Named CASLFORMULA)
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder',
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder'transSchemaMFormula mapT world rel vars anMF =
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder let '.
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder join("\n ",map {'w'.$_.' = vars !! '.($_-1);} (1,2,3,4,5)).
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ' in
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder case (getRLabel anMF,item anMF) of
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder';
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
797f811e57952d59e73b8cd03b667eef276db972Christian Maederforeach my $pair (@input) {
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder# print "Pair: $pair\n";
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder my $moda_i = 0;
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder # split each pair into raw pattern and raw result
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder my ($pattern,$result) = split /\]\],\s+?\[\[/s,$pair;
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder #print STDERR " $pattern => $result\n";
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder # pattern is the left hand side of the case '->'
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder # Each field of NamedSen is substituted by a variable
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder # And then NamedSen is transformend to a tuple
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder $pattern =~ s/""/_label/os;
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder # remove line breaks and spaces
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder $pattern =~ s/\n//gos;
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder $pattern =~ s/\s+/ /go;
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder # add variables foreach modality
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder $pattern =~ s/Simple_mod empty/'moda'.$moda_i++/goe;
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder # substitute formula variables with underscore
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder # only 'p','q' and 'r' are recognized
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder $pattern =~ s/ [pqr] / _ /go;
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder # remove all stuff that s not needed from the pattern
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder # closing brace
1738d16957389457347bee85075d3d33d002158fChristian Maeder $pattern =~ s/\}\s*$//o;
1738d16957389457347bee85075d3d33d002158fChristian Maeder # NamedSen Constructor, opening brace and first selector
1738d16957389457347bee85075d3d33d002158fChristian Maeder $pattern =~ s/NamedSen\{senName = //o;
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder #print STDERR "222: $pattern\n";
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder # new isAxiom field
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder $pattern =~ s/isAxiom = \w+,//o;
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder # sentence selctor
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder $pattern =~ s/ sentence = //o;
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder #print STDERR "223: $pattern\n";
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder # All empty lists in the pattern are substituted by underscores
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder $pattern =~ s/\[\]/_/go;
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder # the result is in the right format and only white spaces / line
# breaks are removed
$result =~ s/\n//gos;
$result =~ s/\s+/ /go;
my $list = "";
for (my $i = 0; $i < $moda_i; $list .= 'moda'.$i++.",") {};
$list = "[$list";
$list =~ s/,$/]/o;
unless ($result =~ m/^\s*Nothing\s*$/o) {
$result = "Just \$ ".$result;
}
print OUT
' ('.$pattern.") -> \n".
' addTerm mapT rel (map modToTerm '.$list.') vars ('.$result.")\n";
}
print OUT ' (_,f)'." -> \n".
' trace ('.$disclaimer.'++"Modal2CASL: unknown formula \\""++showPretty f "\\"\\n"++show f) Nothing
';
close OUT;