(****
 *
 * Module SpecL defines the formal semantics of SpecL.  The form of the
 * definition is a combination of attribute grammar and denotational semantics.
 *									    <p> 
 * The grammar-based definition is organized in three major sections, following
 * the conventional organization of an attribute grammar:
 *									    <p> 
 *   (1) definition of the semantic attributes				   <br>
 *   (2) definition of semantic functions used in attribute equations	   <br>
 *   (3) definition of the grammar and associated attribute equations	   <br>
 *									    <p> 
 * Concepts of denotational semantics are used in the definition of base data
 * types and the semantic interpretation functions.
 *									    <p> 
 * In defining SpecL reflexively in itself, the following SpecL features are
 * used as the basis of the definition:
 *									    <p> 
 *   (1) semantic attributes are defined as SpecL object attributes	   <br>
 *   (2) semantic functions are defined as SpecL auxiliary functions	   <br>
 *   (3) syntactic structure is defined using the SpecL rules,		   <br>
 *       with associated semantic actions				   <br>
 *									    <p> 
 * For any reflexive definition of formal semantics there is an issue of
 * "semantic bootstrapping", where 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 SpecL is SpecL 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.
 *									    <p> 
 * Of the built-in SpecL 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 SpecL 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.
 *									    <p> 
 * 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 a combination of Lisp and ML, with explicit
 * type declarations, the addition of inheritance, and a simplified form of
 * type inference.
 *									    <p> 
 * The general structure of this definition, as well as the structure of the
 * SpecL type system, is significantly influenced by R.D. Tennent's foundational
 * work on programming language semantics.  See in particular his book on the
 * "Principles of Programming Languages", Prentice-Hall, 1981.
 *
 *)

module SpecL;

export *;

(**
 * 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;

rule shit;
rule fuck = shit {};

(*
 * The representation of SpecL types, i.e., the types that objects define.
 *) 
obj Type = base:BaseType or composite:CompositeType
    description: (*
        Type is the representation of a SpecL type, defined as a base type or a
        composite type.
    *);
end Type;

obj BaseType = n:TypeName and v:Value
    description: (*
        A base type has a name and an optional value.  Optional means that the
        value field may be nil.  When non-nil, the value component of a type is
        used to represent value-restricted types, which subject is discussed at
        some length in the SpecL reference manual, and elaborated on further
        below.

        Built-in types and user-defined types are denoted with a string name
        and a nil value.  For example, the built-in type name "integer" denotes
        the conceptually infinite set of integer values.  This is represented
        as a BaseType with a TypeName component of "integer" and a nil Value
        component.  The other built-in type names are "real", "string", and
        "boolean", which denote the typical value sets found in specification
        and programming languages.
								             <p>
	A ground-up formal defintion can construct integer, real, and string as
        recursive composite types, as is done in Tennent, for example.  The
        ground-up definition of boolean is a simple union of literals for true
        and false.  The formal definition of SpecL assumes that such
        constructions are well understood, and so provides the standard types
        as built-in.  Literals for the built-in types are considered to be
        lexically-recognized regular expressions, with the lexical recognition
        process also considered to be built-in.
								             <p>
        With built-in types as a basis, object definitions are used to name and
        construct as many additional types as a specifier wants.  For example,
        the type named "IntegerTwoTuple" can be defined as
								        <p><pre>
	    object IntegerTwoTuple = integer and integer;
								       <p></pre>
	This is represented as a BaseType with a TypeName component =
        "IntegerTwoTuple" and a nil Value component.
								             <p>
	A non-nil Value component is used to denote the type of a specific
        literal value.  For example, the type of the integer literal 10 is not
        just "integer", but rather "the integer 10".  This is represented as a
        BaseType with a TypeName component of "integer" and Value component of
        10.  Such representations are useful for defining enumerated types,
        sub-range types, and tuples with one or more constant components.
        Examples of such uses are in the SpecL reference manual.
    *);
end BaseType;

obj CompositeType = t:TupleType or u:UnionType or l:ListType or f:FunctionType

    description: (*
        Formally, SpecL's composite type constructors are based directly on
        Scott and Strachey denotational data domain constructions.  These are
        described most elegantly by Tennent, in his 1981 "Principles of
        Programming Languages".  Tennent defines the four domain constructions
        of Product, Sum, Function, and Reursive.  These correspond respectively
        to the SpecL composite constructors for tuple, union, function, and
        recursive definitions.  In Tennent, the list domain can be derived from
        either the function or recursive domains.  In SpecL, list composition
        is included as fundamental, i.e., non-derived form.
									     <p>
	The concrete definition of composite types in SpecL is organaized
        pragmatically ... .  Nevertheless, the formal underpinning in
        denotational data domains is fundamentally important in providing a
        rigorous mathematical base on which the pragmatic definintions build.
    *);

end;

obj TypeName = string;

val IntegerType:Type = {"integer", nil};
val RealType:Type = {"real", nil};
val BooleanType = {"boolean", nil};
val StringType = {"string", nil};
obj OpaqueType;
obj NilValue;
obj TupleType = TupleField* and TupleTypeTag;
obj TupleField = FieldName and Type;
obj FieldName = string;
obj UnionType = TupleField* and UnionTypeTag;
obj ListType = Type and ListTypeTag;
obj TupleTypeTag;
obj UnionTypeTag;
obj ListTypeTag;
obj FunctionTypeTag;
obj FunctionType = Inputs and Outputs;
obj Inputs = Type*;
obj Outputs = Type*;

(*
 * The representation of SpecL values, i.e., the values bound to identifiers.
 *)
obj Value = data:(a:AtomicValue or c:CompositeValue) and type:Type;
obj AtomicValue = i:IntegerValue or r:RealValue or b:BooleanValue or
        s:StringValue or o:OpaqueValue or n:NilValue;
obj CompositeValue = t:TupleValue or u:UnionValue or l:ListValue or
        f:FunctionValue;
obj IntegerValue = integer;
obj RealValue = real;
obj BooleanValue = boolean;
obj StringValue = string;
obj OpaqueValue;
obj TupleValue = TupleFieldValue*;
obj UnionValue = Value;
obj ListValue = Value*;
obj TupleFieldValue = FieldName* and Value;
obj FunctionValue = ... ;

(*
 * The environment and store, as found typically in semantic definitions.
 *)
obj Environment = EnvironmentBinding*;
obj Store = ActivationRecord*;
obj EnvironmentBinding = n:Name and t:Type;
obj ActivationRecord = ... ;
obj Name = string;

(*
 * The pre-defined built-in environment.
 *)
value BuiltInEnvironment:Environment = [
    {"integer", IntegerType},
    {"real", RealType},
    {"string", StringType}
];


(**
 * Auxiliary functions.
 *)
function IsBaseType(t:Type) = t?.base;
function IsInteger(t:Type) = t = IntegerType;
function Functionize(env:Environment, store:Store, tree:AttributedParseTree)->
    SemanticFunction =
        lambda (Environment, Store) -> (Store, Value)
            SynthesizeStore(env, store, tree);
obj AttributedParseTree = Root and Children;
obj Children = AttributedParseTree*;
obj Root = Symbol and AttributeValuePair*;
obj Symbol = string;
obj AttributeValuePair = name:AttributeName and valu:AttributeValue;
obj AttributeName = string;
obj AttributeValue = Value;
obj SemanticFunction = 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 = 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;

function compat(t1:Type, t2:Type) =
    t1 = t2
	or
    ident_compat(t1, t2)
	or
    struct_compat(t1, t2);

function ident_compat(t1:Type, t2:Type) = ... ;

function struct_compat(t1:Type, t2:Type) = ... ;

function equiv(t1:Type, t2:Type) =
    compat(t1, t2) and compat(t2, t1);

function BuildLiteralIntegerType(v:Value)->Type =
    {"integer", v};

function BuildLiteralRealType(v:Value)->Type =
    {"real", v};

function BuildLiteralStringType(v:Value)->Type =
    {"string", v};

(**
 * Tokens.
 *)
val SET = "set";

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

rule start =
	top_level_item*
		;

rule top_level_item =
	d:declaration
		  {
			parsetree = d; undefined1 = undefined2;
	          }		
		|
	e:expression
		  {
			parsetree = e;
	          }		
		;

rule declaration = ...;
rule expression = ...;

rule set_expression =
	SET storage_designator "=" expression
		  {
		  }
		;

rule storage_designator;

rule spec_unit =
    h:module_heading e:entity_spec_list "end" module_name_ender ";"
	{ h.:type_ = e.:value_; }
    ;

rule module_heading;

rule entity_spec_list;

rule module_name_ender;


rule literal =
	sl:STRING_LITERAL
		  {
			this.:type_ = BuildLiteralStringTyep(sl.:value_);
			this.:value_ = sl.:value_;
		  }
		|
	INTEGER_LITERAL
		  {
			this.:type_ = BuildLiteralIntegerType(sl.:value_);
			this.:value_ = sl.:value_;
		  }
		|
	REAL_LITERAL
		  {
			this.:type_ = BuildLiteralRealType(sl.:value_);
			this.:value_ = sl.:value_;
		  }
		;

end SpecL;

object STRING_LITERAL;
object INTEGER_LITERAL;
object REAL_LITERAL;

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