Quelle VCParserSupp.vdmsl Sprache: VDM

module VCParserSupp
/***
VCParserSupp
Author: Tomohiro Oda and Paul Chisholm
Version: 0.01
License: the MIT License

Copyright (c) 2016 Tomohiro Oda, Paul Chisholm
                   and Software Research Associates, Inc.

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.

****************************************************************************

This module supplements the VCParser module with additional convenience functions.

Note this module depends on modules Char, Numeric and Seq that are in the ISO8601 example located at

    http://overturetool.org/download/examples/VDMSL/

***/
imports from VCParser values
                            digit renamed digit
                            lowerAlphabet renamed lowerAlphabet
                            upperAlphabet renamed upperAlphabet
                            alphabet renamed alphabet
                      types PARSER renamed PARSER
                            SOURCE renamed SOURCE
                            PARSED renamed PARSED
                            TREE   renamed TREE
                            ERROR  renamed ERROR
                            LABEL  renamed LABEL
                      functions label renamed label
                                either renamed either
                                concat renamed concat
                                iterate renamed iterate
                                takeChar renamed takeChar,
        from Seq all,
        from Numeric all,
        from Char all
exports values lowerAlphanum, upperAlphanum, alphanum, octal, hex: PARSER
        functions takeNumeric      : [nat1] * [nat1] -> PARSER
                  takeFixedNumeric : nat1 -> PARSER
                  takeBoundedString: seq1 of char * PARSER * nat * nat -> PARSER
                  takeUpto         : seq1 of char * [PARSER] +> PARSER
                  takeUptoOneOf    : seq of seq1 of char * [seq1 of char] * [PARSER] +> PARSER
                  getContent       : LABEL * TREE +> seq of char
                  getContentNat    : LABEL * TREE +> nat
                  getTrees         : LABEL * TREE +> seq of TREE
                  getTree          : LABEL * TREE +> TREE
                  isEmpty          : TREE +> bool
                  prune            : PARSED -> PARSED
                  pruneTree        : TREE -> TREE
                  format           : PARSED -> seq of char
                  formatTree       : TREE * nat -> seq of char

definitions

values

     TABSIZE = 2;

     -- Recognise a lower case alphanumeric character.
     lowerAlphanum =
        label("lowerAlphanum", either([lowerAlphabet, digit]));

     -- Recognise an upper case alphanumeric character.
     upperAlphanum =
        label("upperAlphanum", either([upperAlphabet, digit]));

     -- Recognise an alphanumeric character.
     alphanum =
        label("alphabet", either([alphabet, digit]));

     -- Recognise an octal digit.
     octal =
        label(
            "octal",
            either([takeChar("01234567"(index)) | index in set {1, ..., 8}]));

     -- Recognise a hexadecimal digit.
     hex =
        label(
            "hex",
            either([takeChar("0123456789ABCDEFabcdef"(index)) | index in set {1, ..., 22}]));

functions

    -- Recognise a numeric value optionally specifying the minimum and maximum digits.
    takeNumeric: [nat1] * [nat1] -> PARSER
    takeNumeric(m, n) == let m1 = if m = nil then 1 else m
                         in concat(iterate(digit, m1, n))
    pre m <> nil and n <> nil => m <= n;

    -- Recognise a fixed length numeric value.
    takeFixedNumeric: nat1 -> PARSER
    takeFixedNumeric(n) == takeNumeric(n, n);

    -- Recognise a string optionally specifying a minimum and maximum length.
    -- While the parser argument can be arbitrary, the intent is it recognises a single character.
    takeBoundedString: seq1 of char * PARSER * nat * nat -> PARSER
    takeBoundedString(lbl, parser, min, max) == label(lbl, concat(iterate(parser, min, max)))
    pre min <= max;

    -- Recognise characters in the source till a specified token is reached.
    -- If an optional parser is specified, use it to parse the recognised string.
    takeUpto: seq1 of char * [PARSER] +> PARSER
    takeUpto(word, parser) ==
        lambda source : SOURCE &
            cases Seq`indexOfSeqOpt[char](word, source):
                nil   -> mk_PARSED(mk_ERROR(word ^ " not found"), source),
                index -> let recognised = [ source(i) | i in set {1,...,index-1} ],
                             remainder = [ source(i) | i in set {index,...,len source} ] in
                             if parser = nil
                                 then mk_PARSED(mk_TREE(nil, recognised), remainder)
                                 else let mk_PARSED(tree, rest) = parser(recognised) in
                                          cases tree:
                                              mk_ERROR(-)  -> mk_PARSED(mk_ERROR("unrecognised"), source),
                                              mk_TREE(-,-) -> if Char`isWhiteSpaces(rest)
                                                                  then mk_PARSED(tree, remainder)
                                                                  else mk_PARSED(mk_ERROR("excess"), rest^remainder)
                                              end
                end;

    -- Recognise characters in the source till one of a specified sequence of tokens is reached.
    -- If no such token is found, and an optional terminator is provided, recognise characters up to the terminator.
    -- If a sequence is recognised and an optional parser is specified, use it to parse the recognised string.
    takeUptoOneOf: seq of seq1 of char * [seq1 of char] * [PARSER] +> PARSER
    takeUptoOneOf(tokens, term, parser) ==
        lambda source : SOURCE &
            cases tokens:
                []         -> if term = nil
                              then mk_PARSED(mk_ERROR("not found"), source)
                              else takeUpto(term, parser)(source),
                [tok]^rest -> let mk_PARSED(tree, source1) = takeUpto(tok, parser)(source) in
                                  cases tree:
                                      mk_ERROR(-)  -> takeUptoOneOf(rest, term, parser)(source),
                                      mk_TREE(-,-) -> mk_PARSED(tree, source1)
                                      end
                end;

    /*
       Convenience functions for extracting items from a parse tree.
    */

    -- Get the character content.
    getContent: LABEL * TREE +> seq of char
    getContent(lbl, mk_TREE(tlabel,content)) == content
    pre (lbl = nil or lbl = tlabel) and is_(content, seq of char);

    -- Get the character content as a natural number.
    getContentNat: LABEL * TREE +> nat
    getContentNat(lbl, tree) == Numeric`decodeNat(getContent(lbl,tree))
    pre pre_getContent(lbl, tree) and Char`isDigits(tree.contents);

    -- Get the sequence of sub trees.
    getTrees: LABEL * TREE +> seq of TREE
    getTrees(lbl, mk_TREE(tlabel,content)) == content
    pre (lbl = nil or lbl = tlabel) and is_(content, seq of TREE);

    -- Get the only sub tree.
    getTree: LABEL * TREE +> TREE
    getTree(lbl, tree) == tree.contents(1)
    pre pre_getTrees(lbl, tree) and len tree.contents = 1;

    -- Is a tree empty (has not label or content)?
    isEmpty : TREE +> bool
    isEmpty(mk_TREE(tlabel,content)) == tlabel = nil and content = [];

    /*
       Convenience functions for flattening out parse trees:
       - remove empty sub trees;
       - lift sub components up where a nil label is encountered.
    */

    -- Filter out empty subtrees from a parse result.
    prune : PARSED -> PARSED
    prune(mk_PARSED(parsed, remaining)) ==
        if
            is_ERROR(parsed)
        then
            mk_PARSED(parsed, remaining)
        else
            mk_PARSED(pruneTree(liftTree(parsed)), remaining);

    -- Filter out empty subtrees from a tree.
    pruneTree : TREE -> TREE
    pruneTree(mk_TREE(lbl, contents)) ==
        if
            is_(contents, seq of char)
        then
            mk_TREE(lbl, contents)
        else
            mk_TREE(lbl, pruneTrees(contents));

    -- Prune a sequence of trees.
    pruneTrees : seq of TREE -> seq of TREE
    pruneTrees(trees) == [ pruneTree(trees(i)) | i in set inds trees & not isEmpty(pruneTree(trees(i))) ];

    -- Lift subtrees with a nil label up a level.
    liftTree : TREE -> TREE
    liftTree(mk_TREE(lbl,contents)) ==
        if is_(contents, seq of char)
            then mk_TREE(lbl,contents)
        else let lifted = liftTrees(contents)
             in if lbl = nil and len lifted = 1
                then lifted(1)
                else mk_TREE(lbl,lifted);

    -- Lift a sequence of subtrees.
    liftTrees : seq of TREE -> seq of TREE
    liftTrees(trees) == conc [ liftTreeSeq(trees(i)) | i in set inds trees ];

    -- Auxiliary function for lifting subtrees.
    -- Produces a sequence of trees in case the top level tree has a nil label.
    liftTreeSeq : TREE -> seq of TREE
    liftTreeSeq(mk_TREE(lbl,contents)) ==
        if is_(contents, seq of char)
        then [mk_TREE(lbl,contents)]
        else let lifted = liftTrees(contents)
             in if lbl = nil
                then lifted
                else [mk_TREE(lbl,lifted)];

    /*
       Convenience functions for creating a pretty printed text version of a parse tree.
    */

    -- Format a parse result as text.
    format : PARSED -> seq of char
    format(mk_PARSED(parsed, remaining)) ==
        formatTreeOrError(parsed) ^ "Remaining: [" ^ remaining ^ "]";

    -- Format a parse tree or parse error as text.
    formatTreeOrError : TREE| ERROR -> seq of char
    formatTreeOrError(treeOrError) ==
        if
            is_ERROR(treeOrError)
        then
            "Error: " ^ treeOrError.message ^ "\n"
        else
            "Parse Tree:\n" ^ formatTree(treeOrError, TABSIZE);

    -- Format a parse tree as text.
    formatTree : TREE * nat -> seq of char
    formatTree(mk_TREE(lbl, contents), n) ==
        let lblstr = if lbl = nil then "" else lbl
        in indent(n) ^ "'" ^ lblstr ^ "'\n" ^ formatContent(contents, n + TABSIZE);

    -- Format as text the parse tree content (text or sequence of subtrees).
    formatContent : (seq of TREE | seq of char) * nat -> seq of char
    formatContent(tt, n) ==
        if
            is_(tt, seq of char)
        then
            indent(n) ^ "[" ^ tt ^ "]\n"
        else
            conc [formatTree(tt(i), n) | i in set inds tt];

    -- Create a sequence of spaces.
    indent : nat +> seq of char
    indent(n) == [' ' | i in set {1, ..., n}];

end VCParserSupp

quality99%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.