(*
 * A potentially simplified version of value, compared to the def in fmsl.fmsl.
 * The point of the simplification is to provide a type that defines reflection
 * to the end users.  However, it's probably better just to use the same
 * definition in formal semantics and 
 *
 * Hence, this file needs to be reconciled fully with what's defined in
 * specl.specl.
 *)

obj Value = data:UnionOfAllValues and
	    type:Type;

obj UnionOfAllValues =
    b:boolean or
    i:integer or
    r:real or
    s:string or
    o:OpaqueValue or
    l:ListValue or
    t:TupleValue or
    u:UnionValue or
    f:FunctionValue;

obj OpaqueValue = string;

obj ListValue =
    elements:Value*;

obj TupleValue =
    elements:TupleElement*;

obj TupleElement =
    name:string and
    data:Value;

obj UnionValue =
    current:integer and
    elements:TupleElement*;

obj FunctionValue =
    op(Value)->(Value);

obj Type =
    name:TypeName and
    parents: Type* and
    rep:TypeRepresentation;

obj TypeName = string;

obj TypeRepresentation =
    a:AtomicType or
    l:ListType or
    t:TupleType or
    u:UnionType or
    f:FunctionType;

obj AtomicType;

obj ListType = 
    base_type:Type;

obj TupleType = 
    elements:Type*;

obj UnionType =
    element_tag:integer and
    elements:Type*;

obj FunctionType =
    arity: Type* and
    coarity: Type*;

obj TypeSpelling = string;

function SpellType(t:Type)->TypeSpelling =
    if      t.rep?.a then t.name
    else if t.rep?.l then "list of " + SpellType(t.rep.l.base_type)
    else if t.rep?.t then "tuple of " + SpellTypes(t.rep.t.elements)
    else if t.rep?.u then "union of " + SpellTypes(t.rep.u.elements)
    else if t.rep?.f then "function of " + SpellFunctionSignature(t.rep.f);

function SpellTypes(ts:Type*) =
    if ts = nil then ""
    else SpellType(ts[1]) + "," + SpellTypes(ts[2:#ts]);

function SpellFunctionSignature(ft:FunctionType) =
    "(" + SpellTypes(ft.arity) + ")" +
    "(" + SpellTypes(ft.coarity) + ")";


val IntType:Type = {
    "integer",		-- name
    nil,		-- parents
    'AtomicType'	-- rep
};

val TwoTupleType:Type = {
    "TwoTuple",		-- name
    nil,		-- parents
    [			-- rep
	IntType,		-- element #1
	IntType			-- element #2
    ]
};

val IntValue = {
    1,				-- data
    IntType			-- type
};

val TwoTupleValue = {
    [1, 2],			-- data
    TwoTupleType		-- type
};