(****
 *
 * Module FMSL defines the formal semantics of FMSL, in FMSL.  The definitional
 * form is a combination of attribute grammars and denotational semantics.
 *
 * The grammar-based definition is organized in three major sections, following
 * the conventional organization of an attribute grammar:
 *
 *   (1) definition of the semantic attributes
 *   (2) definition of semantic functions used in attribute equations
 *   (3) definition of the grammar and associated attribute equations
 *
 * Concepts of denotational semantics are used in the definition of base data
 * types and the semantic interpretation functions.
 *
 * In defining FMSL reflexively in itself, the following FMSL features are
 * used as the basis of the definition:
 *
 *   (1) semantic attributes are defined as FMSL object attributes
 *   (2) semantic functions are defined as FMSL auxiliary functions
 *   (3) attributed grammar rules are defined using the grammar-style notation
 *       for FMSL object definitions with associated semantic actions
 *
 * Defining the semantics of FMSL in itself leads to some conceptually
 * insignificant but notationally annoying problems related to the would-be use
 * of keywords as identifiers.  Most particularly, since val and value are both
 * FMSL keywords, they cannot be used as identifiers in this definition.  Hence
 * the slightly obnoxious identifier "valu" is used as the name of the Value
 * component in a tagged value.  Other keyword avoidance gimmicks are "int",
 * "reel", "bool", and "str" as component names, instead of the keywords
 * "integer", "real", "boolean", and "string", respectively.
 *
 * Another notational overloading matter is due to the FMSL constraint that
 * attribute names must be distinct form all other identifiers.  To avoid
 * conflict between attribute names and object field names, all attribute names
 * are conventionally suffixed with an underscore.  Hence, for example, "type_"
 * is the name of the type attribute, whereas "type" is used as the name of the
 * type component of a tagged value.
 *
 * For conceptually simplicity, the representation of FMSL runtime values
 * includes a type tag.  However close examination of the semantics reveals
 * that runtime type checking is only required for union types.  This is a
 * reasonably traditional semantics, where union types, and the inherited types
 * which derive from unions, are checked at execution time to provide
 * polymorphic dynamic binding.  The actual implementation of an interpreter
 * (or heaven forbid, compiler,) need only store runtime type tags for union
 * values (including values of inherited types), not for values of atomic,
 * tuple, or list types.
 *
 * For any reflexive definitions of formal semantics, there is an issue of
 * "semantic bootstrapping".  Viz., certain functions are considered primitive
 * within the definition.  For example, in nearly all denotational and
 * attribute-grammar definitions of programming languages, arithmetic and
 * logical operators are considered primitive.  Also, the meta languages used
 * in denotational and attribute definitions contain certain operations that
 * are "taken on faith".  Since the meta notation in most programming language
 * definitions is something other than the language itself, the "on faith"
 * aspect of the definition may seem more acceptable than in this case, where
 * the meta notation for the semantics of FMSL is FMSL itself.  That said,
 * there are notable examples of languages defined in terms of themselves at
 * one level or another, Lisp in Lisp probably being the most well known.
 *
 * Of the built-in FMSL operators, those taken entirely "on faith" are
 * arithmetic, logical (including basic quantification), and list primitives.
 * To lessen the degree of faith taking, the attribute-grammar FMSL definition
 * is augmented with the equational definition of lists and tuples, since these
 * are used prominently in the meta-definition of auxiliary functions.  The
 * other operations (arithmetic and logical) are considered sufficiently
 * primitive as not to require explicit definition.  The point is that we
 * define as equational primitives those aspects of the meta notation that are
 * not entirely standard in normal mathematics.
 *
 * The general style of this semantic definition is that typical for
 * programming language semantics.  There are Environment and Store attributes
 * which model, respectively, the static and dynamic semantics of the language.
 * Conceptually, the semantics are quite similar to ML, but with explicit type
 * declarations and inheritance, and a considerably simpler version of type
 * inference.
 *
 * The general structure of this definition, as well as the structure of the
 * FMSL type system, is significantly influenced by R.D. Tennent's foundational
 * work on programming language semantics.  See in particular his book on
 * "Principles of Programming Languages", Prentice-Hall, 1981.
 *
 *)

module FMSL;

(**
 * Attribute definitions, including the definition of attribute types.
 *)
define obj attribute type_:Type;
define obj attribute value_:Value;
define obj attribute value_':Value;
define obj attribute store_:Store;
define obj attribute store_':Store;
define obj attribute env_:Environment;
define obj attribute env_':Environment;

(*
 * The representation of FMSL types, i.e., the types that objects define.
 *) 
obj Type is atomic:AtomicType or composite:CompositeType
    description: (*
        Type is the representation of an FMSL type, defined as atomic or
        composite.
    *);
end Type;

obj AtomicType is int:IntegerType or reel:RealType or bool:BooleanType or
        str:StringType or opaque:OpaqueType
    description: (*
        An atomic type is one if integer, real, boolean, string, or opaque.
    *);
end;
obj CompositeType is TupleType or UnionType or ListType;
obj IntegerType;
obj RealType;
obj BooleanType;
obj StringType;
obj OpaqueType;
obj NilValue;
obj TupleType is TupleField* and TupleTypeTag;
obj TupleField is FieldName and Type;
obj FieldName is string;
obj UnionType is TupleField* and UnionTypeTag;
obj ListType is Type and ListTypeTag;
obj TupleTypeTag;
obj UnionTypeTag;
obj ListTypeTag;

(*
 * The representation of FMSL values, i.e., the values bound to identifiers.
 *)
obj Value is type:Type and valu:(AtomicValue or CompositeValue);
obj AtomicValue is int:IntegerValue or reel:RealValue or bool:BooleanValue or
    str:StringValue or opaque:OpaqueValue or nl:NilValue;
obj CompositeValue is TupleValue or UnionValue or ListValue;
obj IntegerValue is integer;
obj RealValue is real;
obj BooleanValue is boolean;
obj StringValue is string;
obj OpaqueValue;
obj TupleValue is TupleFieldValue*;
obj UnionValue is Value;
obj ListValue is Value*;
obj TupleFieldValue is FieldName* and Value;

(*
 * The environment and store, as found typically in semantic definitions.
 *)
obj Environment is EnvironmentBinding*;
obj Store is ActivationRecord*;
obj EnvironmentBinding is ... ;
obj ActivationRecord is ... ;

(**
 * Auxiliary functions.
 *)
function IsAtomic(t:Type) = t isa atomic ;
function IsInteger(t:Type) = t.atomic isa int;
function Functionize(env:Environment, store:Store, tree:AttributedParseTree)->
    SemanticFunction =
        lambda (Environment, Store) -> (Store, Value)
            SynthesizeStore(env, store, tree);
obj AttributedParseTree is Root and Children;
obj Children is AttributedParseTree*;
obj Root is Symbol and AttributeValuePair*;
obj Symbol is string;
obj AttributeValuePair is name:AttributeName and valu:AttributeValue;
obj AttributeName is string;
obj AttributeValue is Value;
obj SemanticFunction is op(Environment, Store, Value)->(Store, Value);
function SynthesizedStore(env:Environment, store:Store, valu:Value,
    tree:AttributedParseTree) -> (store':Store, valu':Value) = ...
        (* Send env, store, valu into tree; extract the synthesized store_'
         * and valu_' that come up; return these as store' and value' resp. *);

(*
 * Semantic bootstrap definitions for primitive operations.
 *)
obj List
    operations: GetNth, GetMthThorughNth, ConstructList;
    equations:
	var l: ListType;
        var v,v': Value;
        var n: integer;
        var u: ValueUniverse;
        var va: Variable;
        var e: Expression;
        GetNth(nil, n) == nil;
	GetNth(ConstructList(l, v), n) == 
	    if n = 1 
            then v
            else GetNth(l, n-1);
	Forall(va, nil, e) == true;
        Forall(va, ConstructValueUniverse(u, v), e) ==
	    if Eval(BetaSubstitute(va, e))
	    then Forall(va, v, e)
	    else false;
    description: (* ... *);
end List;
op ConstructList(ListType, Value) -> ListType;
op GetNth(ListType, n:integer) -> Value
    pre: n >= 1;
end;
op Forall(Variable, ValueUniverse, Expression) -> boolean;
op BetaSubstitute(Variable, Expression) -> Expression;

obj ValueUniverse is Value*;

obj Tuple
    operations: Dot, ConstructTuple;
    equations:
        var t: Tupletype;
        var v,v': Value;
	var f: FieldName;
        Dot(nil) == nil;
        Dot(ConstructTuple(t, v), n) == ... ;
end;
op ConstructTuple(TupleType, Value)->TupleType;
op Dot(TupleType, FieldName) -> Value;

obj Union
    equations: ;
end Union;

(*
 * This is not necessary, according to the comments at the top, except perhaps
 * for quantifiers.
 *)
obj Expression
    operations: Plus, Minus, Times, Divide;
end Expression;
obj Variable;


(**
 * The syntax-directed semantic base.
 *)

obj spec_unit ::=
    h:module_heading e:entity_spec_list 'end' module_name_ender ';'
	{ h.:type_ == e.:value_; }
    ;

obj module_heading;

obj entity_spec_list;

obj module_name_ender;


end FMSL;

(*
 * For Emacs Ispell:
 * LocalWords:  FMSL Tennent val valu int bool str equational Tennent's
 * LocalWords:  foundational
 *)