Algebraic Datatypes

  Algebraic datatypes are defined using the datatype construct. Its syntax is as follows.

Datatype_Decl	::=	datatype
		[ Datatype_Spec and ¼ and Datatype_Spec ]
		[ where type Type_Spec and ¼ and Type_Spec ]
		[ law Law_Spec and ¼ and Law_Spec ]
		;

Each datatype declaration specifies a set of (potentially mutually recursive) types, a set of type abbreviations, and a set of pattern matching abbreviations called laws.

Datatype_Spec	::=	Id [ < Id, ¼ , Id > ]
		[ : Inherit_List ]
		[ :: Datatype_Qualifiers ]
		[ = Cons_Specs ]
Cons_Specs	::=	Cons_Spec  - ¼ - Cons_Spec
		[ public: Datatype_Body ]
Cons_Spec	::=	Simple_Cons_Spec
		[ with { Class_Decl } ]
Simple_Cons_Spec	::=	Id [ String ]	unit constructor
	|	String	unit constructor
	|	Id [ of ] Type_Exp	constructor with arguments
	|	#[ ]	unit list constructor
	|	#{ }	unit list constructor
	|	#( )	unit list constructor
	|	#[ Type_Exp ... Type_Exp ]	list constructor
	|	#{ Type_Exp ... Type_Exp }	list constructor
	|	#( Type_Exp ... Type_Exp )	list constructor
	|	[ - Type_Exp  - ]	vector constructor
	|	( - Type_Exp  - )	vector constructor
	|	{ - Type_Exp  - }	vector constructor

Datatypes can be annotated with qualifiers. They tell the Prop translator to generate additional code for each datatype to provide additional functionality.

Datatype_Qualifiers	::=	Datatype_Qualifier ¼ Datatype_Qualifier
Datatype_Qualifier	::=	collectable	garbage collectable
	|	rewrite	optimized for tree rewriting
	|	persistent	generate persistence interface
	|	lexeme	used for parser/lexer tokens
	|	inline	use inlined implementation
	|	extern	use non-inlined implementation

Type specifications assign abbreviations to commonly used type expressions. They act like typedef's in C++, except that Prop can make use of the type information provided by these specifications.

Type_Spec	::=	Id = Type_Exp

Law specifications are used to define abbreviations to datatype patterns⁵. They behave like macros in some sense, except that unlike macros, they are properly type checked by Prop. In addition, if the keyword inline is used, then Prop will treat the lhs as an expression and generate a function of the same name that can be used to construct the datatype term.

Law_Spec	::=	[ inline ] Id [ Law_Arg ] = Pat
Law_Arg	::=	Id
	|	( Id, ¼ , Id )

Prop recognizes the following set of type expressions.

Type_Exp	::=	Type_Id	type name
	|	Type_Exp *	pointer type
	|	Type_Exp &	reference type
	|	Type_Qualifier Type_Id	qualified type
	|	Datatype_Qualifier Type_Exp	annotation
	|	( Type_Exp )	grouping
	|	( Type_Exp , TypeExp, ¼ , TypeExp )	tuple type
	|	( Type_Exp , TypeExp, ¼ , TypeExp )	tuple class
	|	{ Lab_Type_Exp, ¼ , Lab_Type_Exp }	record type
	|	Type_Exp = Exp	default value
Lab_Type_Exp	::=	Id : Type_Exp
Type_Qualifier	::=	class	a class type
	|	const	constant type
	|	rewrite	rewritable
	|	collectable	garbage collected
	|	persistent	persistent object

In general, four different types of datatype constructors can be defined:

nullary constructors

These are constructors without an argument. Prop maps these into small integers and no heap space will be consumed.

tuple argument constructors

These are constructors with one or more unamed arguments.

record argument constructors

These are constructors with one or more named arguments written within braces. For example, in the following datatype definition a record argument constructor called Add is defined:

  datatype Exp = Add { left : Exp, right : Exp }
	       | ...

To construct an Add expression, we can use any one of the following forms:

     Exp e1 = Add(x,y);
     Exp e2 = Add'{ left = x, right = y };
     Exp e3 = Add'{ right = y, left = x };

Note that we are allowed to rearrange the labels in any order if the record expression form is used.

empty constructors

These are constructors written with an empty argument (). For example, in the following definition an empty constructor called NONE is defined:

    datatype Exp : public AST
	= NONE ()
	| NONE2
        | ...

Here, the constructor NONE will inherit from the class AST, while the nullay constructor NONE2 will not.

 
• Instantiating a datatype