*** ___________________________________________________________________________
***
***  file: ~/Teaching/COMP317/Maude/simple.maude
*** ___________________________________________________________________________
***
***  Author: Grant Malcolm
***
***   This code may be freely used, distributed or modified,
***   provided due credit be given.
***
*** ___________________________________________________________________________
***
***
***   Syntax of a simple imperative programming language,
***   used in teaching COMP317, Semantics of Programming Languages,
***   at the University of Liverpool.
***
***   The semantics of this language is specified in a separate file,
***   simpleSemantics.maude.
***
***   The language is specified by the following BNF:
***
***      <Variable>  ::=  'a | 'b | 'c | ...
***
***      <Digit>  ::=  0 | 1 | ... | 9
***
***      <Numeral>  ::=  <Digit> | <Numeral><Digit>
***
***      <Assignable>  ::=  <Variable>
***
***      <Expression>  ::=
***          <Assignable>
***       |  <Numeral>
***       |  - <Expression> 
***       |  <Expression> + <Expression> 
***       |  <Expression> - <Expression> 
***       |  <Expression> * <Expression> 
***
***      <BooleanExpression>  ::=
***          true
***       |  false
***       |  <Expression> < <Expression>
***       |  <Expression> == <Expression>
***       |  not <BooleanExp>
***       |  <BooleanExp> and <BooleanExp>
***
***      <BasicProgram>  ::=
***          <Assignable> := <Expression>
***
***      <Program>  ::=
***          skip
***       |  <BasicProgram>
***       |  <Program> ; <Program>
***       |  if <BooleanExpression> then <Program> else <Program> fi
***       |  while <BooleanExpression> do <Program> od
***
*** ___________________________________________________________________________
***
***  Created:       2009/01/07
***  Last modified: 2011/02/27
*** ___________________________________________________________________________
***


*** *************************************************************************
*** Decimal numerals.
***
***  Numerals are non-empty strings of Digits,
***  and Digits are the symbols 0, 1, ..., 9.
***  The drawback of using Numerals as specified in Maude
***  is that Maude requires spaces (or brackets)
***  between operators and their arguments.
***  This means that a numeral such as 1692 has to be written
***  with spaces as 1 6 9 2.
***
fmod  NUMERAL  is

  sort  Digit .

  ops  0 1 2 3 4 5 6 7 8 9  :  -> Digit
  [
     ctor
  ] .


  sort  Numeral .

  subsort  Digit < Numeral .

  op  _ _  : Numeral  Digit -> Numeral
  [
     ctor
     prec 2
  ] .

endfm


*** *************************************************************************
***  Expressions in SIMPLE.
***
***   These are "integer" expressions, built up from numerals and variables,
***   with operations for addition, multiplication, subtraction, and a
***   unary minus operation.
***
***

fmod  EXPRESSIONS  is

    *** Use "Quoted Identifiers" for variables.
    ***  The module QID in the standard prelude declares a sort Qid
    ***  of LISP-like quoted identifiers.  These are just strings preceded
    ***  by a closing single-quote (').  For example, 'a, 'b, 'ab, etc.
    ***  We rename the sort name "Qid" to "Variable", as this name is more
    ***  appropriate for defining a programming language.
    ***
  protecting  QID *(sort Qid to Variable) .

    *** Use Numerals as expressions
    ***
  protecting NUMERAL .


    *** The syntactic category of Expressions in the language.
    ***
  sort  Expression .


    *** Things that can be assigned integer values.
    *** These will include Variables (see below),
    *** and, later, array components.
    ***
  sort Assignable .


    *** Variables can be assigned integer values
    ***
    ***   <Assignable>  ::=  <Variable>
    ***
  subsort Variable < Assignable .


    *** All assignables and numerals are expressions:
    ***
    ***   <Expression>  ::=  <Assignable> | <Numeral>
    ***
  subsort  Assignable Numeral < Expression .



    *** Binary infix addition operation.
    ***
    ***   <Expression>  ::=  <Expression> + <Expression>
    ***
    ***
  op  _+_  : Expression Expression -> Expression [ ctor prec 20 ] .


    *** Binary infix multiplication operation.
    ***
    ***   <Expression>  ::=  <Expression> * <Expression>
    ***
    ***
  op  _*_  : Expression Expression -> Expression [ ctor prec 16 ] .


    *** Binary infix subtraction operation.
    ***
    ***   <Expression>  ::=  <Expression> - <Expression>
    ***
  op  _-_  : Expression Expression -> Expression [ ctor prec 19 ] .


    *** Unary prefix minus operation.
    ***
    ***   <Expression>  ::=  - <Expression>
    ***
  op  -_  : Expression -> Expression [ ctor prec 3 ] .

endfm



*** *************************************************************************
***  Boolean expressions of the SIMPLE language.
***
***   These are the "tests" or "guards" of the language: expressions that
***   are either true or false.  We can compare the values of two integer
***   expressions (equal, less-than, less-than-or-equal, etc.), and we can
***   conjoin tests with logical operations (and, or, not, etc.).  We also
***   have constant expressions "true" and "false".
***

fmod  BOOLEAN_EXPRESSIONS  is


    *** Using expressions of SIMPLE.
    ***
  protecting  EXPRESSIONS .


    *** The syntactic category of Tests.
    ***
  sort  BooleanExpression .


    ***  Constants:
    ***
    ***    <BooleanExpression>  ::=  true | false
    ***
  ops  true false  : -> BooleanExpression  [ ctor ] .

    *** Comparison: equality test.
    ***
    ***    <BooleanExpression>  ::=  <Expression> == <Expression>
    ***
  op  _==_  : Expression Expression -> BooleanExpression
  [
    ctor
    prec 25
  ] .


    *** Comparison: less-than.
    ***
    ***    <BooleanExpression>  ::=  <Expression> < <Expression>
    ***
    ***
  op  _<_  : Expression Expression -> BooleanExpression
  [
    ctor
    prec 25
  ] .


    *** Comparison: less-than-or-equal.
    ***
    ***    <BooleanExpression>  ::=  <Expression> <= <Expression>
    ***
  op  _<=_  : Expression Expression -> BooleanExpression
  [
    ctor
    prec 25
  ] .


    *** Logical and.
    ***
    ***   <BooleanExpression>  ::=  <BooleanExpression> and <BooleanExpression>
    ***
  op  _and_  : BooleanExpression BooleanExpression -> BooleanExpression
  [
    ctor
    prec 30
  ] .


    *** Logical or.
    ***
    ***    <BooleanExpression>  ::=  <BooleanExpression> or <BooleanExpression>
    ***
  op  _or_  : BooleanExpression BooleanExpression -> BooleanExpression
  [
    ctor
    prec 32
  ] .


    *** Logical not.
    ***
    ***    <BooleanExpression>  ::=  not <BooleanExpression>
    ***
  op  not_  : BooleanExpression -> BooleanExpression
  [
    ctor
    prec 29
  ] .

endfm



*** *************************************************************************
*** Basic programs of the SIMPLE language.
***
***
fmod  BASIC_PROGRAMS  is


    *** Using expressions of SIMPLE
    ***
  protecting  EXPRESSIONS .


    *** Basic programs are assignments.
    ***
  sort  BasicProgram .


    *** Assignment
    ***
    ***   <BasicProgram>  ::=  <Variable> := <Expression>
    ***
  op  _:=_  : Assignable Expression -> BasicProgram
            [ ctor
              prec 50
             ] .

endfm



*** *************************************************************************
*** Programs of the SIMPLE language.
***
***
fmod  PROGRAMS  is


    *** Using boolean expressions of SIMPLE
    ***
  protecting  BOOLEAN_EXPRESSIONS .


    *** Using basic programs
    ***
  protecting  BASIC_PROGRAMS .


    *** Programs in the language.
    ***
  sort  Program .


    *** All basic programs are programs.
    ***
    ***   <Program>  ::=  <BasicProgram>
    ***
  subsort  BasicProgram < Program .


    *** The "do nothing" program.  The equivalent of {} in Java or C.
    ***
    ***   <Program>  ::=  skip
    ***
  op  skip : -> Program  [ ctor ] .


    *** Sequential composition.
    ***
    ***   <Program>  ::=  <Program> ; <Program>
    ***
  op  _;_  : Program Program -> Program
           [ ctor assoc prec 60 ] .


    *** Conditionals.
    ***
    ***  <Program> ::=  if <BooleanExpression> then <Program> else <Program> fi
    ***
    *** but "fi" is a keyword in Maude,
    *** so we make a small change to the syntax,
    *** and use "endif" instead.
    ***
  op  if_then_else_endif : BooleanExpression Program Program -> Program
                           [ ctor prec 65 ] .

    *** While-loops.
    ***
    ***   <Program>  ::=  while <BooleanExpression> do <Program> od
    ***
  op  while_do_od : BooleanExpression Program -> Program
                    [ ctor prec 62 ] .

endfm