#! /usr/bin/perl -w

######################################################################
# simple perl script to perform the following tasks:                 #
# * remove (possibly nested) comments in C style /* */               #
# * put double quotes around strings which are not reserved          #
#   keywords in CAPSL                                                #
# * add spaces around special characters                             #
#                                                                    #
# Written by Thomas Boehne, April 2002                               #
######################################################################

# List of reserved keywords for CAPSL

@reserved = ("AND", "AGENT", "AGREE", "ASSUMPTIONS", "ASSUME",
             "AXIOMS", "BEGIN", "BELIEVES", "COLON", "COMMA",
             "CONSTANTS", "DENOTES", "ELSE", "ELSEIF", "END", "ENDIF",
             "ENVIRONMENT", "EQUALS", "EXPOSED", "FOR", "FUNCTIONS",
             "GOALS", "HAT", "HOLDS", "IF", "IMPORTS", "INCLUDE",
             "INVERT", "IS", "KNOWS", "LBRA", "LCRB", "LOWE", "LPAR",
             "MESSAGES", "NOT", "OBJECTS", "ORDER", "OR", "PAR",
             "BAR", "PERIOD", "PLUS", "PRECEDES", "PRIME", "PROTOCOL",
             "PROVE", "RANDOM", "RARR", "MINUS", "RBRA", "RCRB",
             "RPAR", "RUN", "SECRET", "SEM", "SESSEC", "SESSION",
             "SLASH", "STAR", "THEN", "TYPES", "TYPESPEC",
             "VARIABLES", "WITH ID");

# convert removes all comments and puts quotes in front of non-keywords
# The result remains in $_. 
sub convert {
    # read the whole input into $_
    $_ = "";
    while ($line = <>) { $_ = $_ . $line; }
    
    $first_close = 0;
    
    # as long as comments are started
    while (/\/\*/) {
        # quit if no end of comment is found
        if (!(/\*\//)) {
            print STDERR "syntax error - comment not closed\n";
            exit(1);
        }
        # find the first end of a comment
        $first_close = index($_, "*/", 0);
        # find the last start of comment before the first end of a comment
        $matching_open = rindex($_, "/*", $first_close);
        $comment_length = $first_close - $matching_open + 2;
        # quit if the comment has the form /*/
        if ($comment_length < 4) {
            print STDERR "syntax error - comment of form /*/ found\n";
            exit(1);
        }
        # remove the comment
        substr($_, $matching_open, $comment_length) = "";
    }
    
    if (/\*\//) {
        print STDERR "syntax error - comment not opened, but closed\n";
        exit(1);
    }

    # adding Maude specific stuff
    
    s/([^\s])([:;%.])/$1 $2/g;  # add space before 
    s/([:;%.])([^\s])/$1 $2/g;  # and after special characters
    s/([^\s])\|\|/$1 ||/g; # add spaces for ||
    s/\|\|([^\s])/|| $1/g;

    # single quotes confuse Maude...
    # s/\'/Quote/g;

    # put double quotes around all words
    s/([a-zA-Z0-9_]+)/\"$1\"/g;
    # remove the quotes if the word was a reserved word
    foreach $reservedword (@reserved) {
        s/\"$reservedword\"/$reservedword/g;
    }

    # object is already a predefined type in maude, so we rename it:
    s/Object/CapslObject/g;
    # we want to call principals principals, so we need to rename the data type
   s/Principal/CapslPrincipal/g;
}
 
if (@ARGV != 1) {
    print(STDERR "Error: capsl2maude requires exactly one parameter.\n");
    exit(1);
}


&convert;
print("$_");




