[m-dev.] for review: add parsing/storing of assertions

[Peter Ross]

Hi,

This is for Fergus or DJ to review, whoever gets there first.

Pete.

===================================================================


Estimated hours taken: 50

Add the infrastructure for assertions into the compiler.

compiler/error_util.m:
    Output the correct pred name for assertions.

compiler/hlds_data.m:
    Add the assertion_table structure.

compiler/hlds_module.m:
    Get/set the assertion_table from the module_info.

compiler/hlds_out.m:
    Modify hlds_out__write_pred_id to identify assertions.

compiler/hlds_pred.m:
    Add the goal_type assertion.

compiler/make_hlds.m:
    Transform the assertion to a HLDS data structure that can be
    typechecked.

compiler/mercury_to_goedel.m:
compiler/module_qual.m:
    Handle the assertion structure.

compiler/mercury_to_mercury.m:
    Output assertions.

compiler/post_typecheck.m:
    Add a predicate which must be called after typechecking of
    assertions has been finished.  Also document some possible problems
    with typechecking assertions.

compiler/prog_data.m:
    Add assertion to the type item.

compiler/prog_io.m:
    Add the ability to parse assertions.

compiler/purity.m:
    After finished typechecking assertions call
    post_typecheck__finish_assertion.

compiler/typecheck.m:
    Don't output inference messages for assertions.

compiler/notes/compiler_design.html:
    Update documentation about exactly where quantification is done.

compiler/notes/glossary.html:
    Define what an assertion is.

doc/.ispell_words:
    Some more commonly spelt words.

doc/reference_manual.texi:
    Add a small section about how to declare assertions.

doc/transition_guide.texi:
    Mention the new :- assertion op.

library/ops.m:
    Declare the :- assertion op.


*** Relative DIFF ***

===================================================================
RCS file: RCS/accumulator.m,v
retrieving revision 1.10
diff -u -r1.10 accumulator.m
===================================================================
RCS file: RCS/check_assertion.m,v
retrieving revision 1.2
diff -u -r1.2 check_assertion.m
===================================================================
RCS file: RCS/hlds_data.m,v
retrieving revision 1.2
diff -u -r1.2 hlds_data.m
--- hlds_data.m	1999/07/08 00:56:46	1.2
+++ hlds_data.m	1999/07/08 08:11:28
@@ -813,24 +813,24 @@
 
 :- interface.
 
-:- import_module hlds_module.
-
 	%
 	% A table that records all the assertions in the system.
+	% An assertion is a goal that will always evaluate to true,
+	% subject to the constraints imposed by the quantifiers.
+	%
+	% ie :- assertion all [A] some [B] (B > A)
 	% 
+	% The above assertion states that for all possible values of A,
+	% there will exist at least one value, B, such that B is greater
+	% then A.
+	%
 :- type assert_id.
 :- type assertion_table.
 
 :- pred assertion_table_init(assertion_table::out) is det.
 
-	%
-	% After typechecking is finished the pred_info describing the
-	% assertion should be removed from further processing and the
-	% pred_id which describes the assertion stored in the
-	% assertion_table.
-	%
-:- pred remove_assertion_from_further_processing(pred_id::in,
-		module_info::in, module_info::out) is det.
+:- pred assertion_table_add_assertion(pred_id::in,
+		assertion_table::in, assertion_table::out) is det.
 
 :- pred assertion_table_lookup(assertion_table::in, assert_id::in,
 		pred_id::out) is det.
@@ -846,23 +846,14 @@
 assertion_table_init(assertion_table(0, AssertionMap)) :-
 	map__init(AssertionMap).
 
-remove_assertion_from_further_processing(PredId, Module0, Module) :-
-	module_info_assertion_table(Module0, AssertionTable0),
-	assertion_table_add_assertion(PredId, AssertionTable0, AssertionTable),
-	module_info_set_assertion_table(Module0, AssertionTable, Module1),
-	module_info_remove_predid(Module1, PredId, Module).
+assertion_table_add_assertion(Assertion, AssertionTable0, AssertionTable) :-
+	AssertionTable0 = assertion_table(Id, AssertionMap0),
+	map__det_insert(AssertionMap0, Id, Assertion, AssertionMap),
+	AssertionTable = assertion_table(Id + 1, AssertionMap).
 
 assertion_table_lookup(AssertionTable, Id, Assertion) :-
 	AssertionTable = assertion_table(_MaxId, AssertionMap),
 	map__lookup(AssertionMap, Id, Assertion).
-
-:- pred assertion_table_add_assertion(pred_id::in,
-		assertion_table::in, assertion_table::out) is det.
-
-assertion_table_add_assertion(Assertion, AssertionTable0, AssertionTable) :-
-	AssertionTable0 = assertion_table(Id, AssertionMap0),
-	map__det_insert(AssertionMap0, Id, Assertion, AssertionMap),
-	AssertionTable = assertion_table(Id+1, AssertionMap).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
===================================================================
RCS file: RCS/hlds_module.m,v
retrieving revision 1.2
diff -u -r1.2 hlds_module.m
===================================================================
RCS file: RCS/hlds_pred.m,v
retrieving revision 1.2
diff -u -r1.2 hlds_pred.m
--- hlds_pred.m	1999/07/08 00:56:46	1.2
+++ hlds_pred.m	1999/07/08 06:54:45
@@ -179,7 +179,7 @@
 
 :- type goal_type 	--->	pragmas		% pragma c_code(...)
 			;	clauses		
-			;	{ assertion }
+			;	(assertion)
 			;	none.
 
 	% The evaluation method that should be used for a pred.
===================================================================
RCS file: RCS/make_hlds.m,v
retrieving revision 1.4
diff -u -r1.4 make_hlds.m
--- make_hlds.m	1999/07/08 00:56:46	1.4
+++ make_hlds.m	1999/07/08 09:43:11
@@ -62,7 +62,6 @@
 :- import_module code_util, unify_proc, special_pred, type_util, mode_util.
 :- import_module mercury_to_mercury, passes_aux, clause_to_proc, inst_match.
 :- import_module fact_table, purity, goal_util, term_util, export, llds, rl.
-:- import_module check_assertion.
 
 :- import_module string, char, int, set, bintree, map, multi_map, require.
 :- import_module term, varset, getopt, assoc_list, term_io.
@@ -608,13 +607,15 @@
 add_item_clause(func_clause(VarSet, PredName, Args, Result, Body), Status,
 		Status, Context, Module0, Module, Info0, Info) -->
 	check_not_exported(Status, Context, "clause"),
+	{ IsAssertion = no },
 	module_add_func_clause(Module0, VarSet, PredName, Args, Result, Body,
-		Status, Context, no, Module, Info0, Info).
+		Status, Context, IsAssertion, Module, Info0, Info).
 add_item_clause(pred_clause(VarSet, PredName, Args, Body), Status, Status,
 		Context, Module0, Module, Info0, Info) -->
 	check_not_exported(Status, Context, "clause"),
+	{ IsAssertion = no },
 	module_add_pred_clause(Module0, VarSet, PredName, Args, Body, Status,
-		Context, no, Module, Info0, Info).
+		Context, IsAssertion, Module, Info0, Info).
 add_item_clause(type_defn(_, _, _), Status, Status, _,
 				Module, Module, Info, Info) --> [].
 add_item_clause(inst_defn(_, _, _), Status, Status, _,
@@ -692,14 +693,44 @@
 	).
 add_item_clause(assertion(Goal0, VarSet),
 		Status, Status, Context, Module0, Module, Info0, Info) -->
-	check_assertion(Goal0, VarSet, Goal, HeadVars, Module0, Module1),
+
+		%
+		% If the outermost existentially quantified variables
+		% are placed in the head of the assertion, the
+		% typechecker will avoid warning about unbound
+		% type variables as this implicity adds a universal
+		% quantification of the typevariables needed.
+		%
+	(
+		{ Goal0 = all(Vars, AllGoal) - _Context }
+	->
+		{ term__var_list_to_term_list(Vars, HeadVars) },
+		{ Goal = AllGoal }
+	;
+		{ HeadVars = [] },
+		{ Goal = Goal0 }
+	),
 
 	{ term__context_line(Context, Line) },
 	{ term__context_file(Context, File) },
 	{ string__format("assertion__%d__%s", [i(Line), s(File)], Name) },
 
-	module_add_pred_clause(Module1, VarSet, unqualified(Name),
-			HeadVars, Goal, Status, Context, yes, Module,
+		%
+		% The assertions are recorded as a predicate whose
+		% goal_type is set to assertion.  This allows us to
+		% leverage off all the other checks in the compiler that
+		% operate on predicates.
+		%
+		% :- assertion all [A,B,R] ( R = A + B <=> R = B + A ).
+		%
+		% becomes
+		%
+		% assertion__lineno_filename(A, B, R) :-
+		% 	( R = A + B <=> R = B + A ).
+		%
+	{ IsAssertion = yes },
+	module_add_pred_clause(Module0, VarSet, unqualified(Name),
+			HeadVars, Goal, Status, Context, IsAssertion, Module,
 			Info0, Info).
 
 add_item_clause(nothing, Status, Status, _, Module, Module, Info, Info) --> [].
@@ -2691,7 +2722,8 @@
 		in, out, di, uo) is det.
 
 module_add_pred_clause(ModuleInfo0, ClauseVarSet, PredName, Args, Body,
-			Status, Context, Assertion, ModuleInfo, Info0, Info) -->
+			Status, Context, IsAssertion, ModuleInfo,
+			Info0, Info) -->
 		% print out a progress message
 	globals__io_lookup_bool_option(very_verbose, VeryVerbose),
 	( { VeryVerbose = yes } ->
@@ -2703,7 +2735,8 @@
 		[]
 	),
 	module_add_clause(ModuleInfo0, ClauseVarSet, PredName, Args, Body,
-		Status, Context, predicate, Assertion, ModuleInfo, Info0, Info).
+		Status, Context, predicate, IsAssertion, ModuleInfo,
+		Info0, Info).
 
 :- pred module_add_func_clause(module_info, prog_varset, sym_name,
 		list(prog_term), prog_term, goal, import_status, prog_context,
@@ -2712,7 +2745,8 @@
 	in, in, in, in, out, in, out, di, uo) is det.
 
 module_add_func_clause(ModuleInfo0, ClauseVarSet, FuncName, Args0, Result, Body,
-			Status, Context, Assertion, ModuleInfo, Info0, Info) -->
+			Status, Context, IsAssertion, ModuleInfo,
+			Info0, Info) -->
 		% print out a progress message
 	globals__io_lookup_bool_option(very_verbose, VeryVerbose),
 	( { VeryVerbose = yes } ->
@@ -2725,7 +2759,8 @@
 	),
 	{ list__append(Args0, [Result], Args) },
 	module_add_clause(ModuleInfo0, ClauseVarSet, FuncName, Args, Body,
-		Status, Context, function, Assertion, ModuleInfo, Info0, Info).
+		Status, Context, function, IsAssertion, ModuleInfo,
+		Info0, Info).
 
 :- pred module_add_clause(module_info, prog_varset, sym_name, list(prog_term),
 		goal, import_status, prog_context, pred_or_func, bool,
@@ -2734,7 +2769,7 @@
 		out, in, out, di, uo) is det.
 
 module_add_clause(ModuleInfo0, ClauseVarSet, PredName, Args, Body, Status,
-			Context, PredOrFunc, Assertion, ModuleInfo,
+			Context, PredOrFunc, IsAssertion, ModuleInfo,
 			Info0, Info) -->
 		% Lookup the pred declaration in the predicate table.
 		% (If it's not there, call maybe_undefined_pred_error
@@ -2749,7 +2784,7 @@
 		{ PredId = PredId0 },
 		{ PredicateTable1 = PredicateTable0 },
 		(
-			{ Assertion = yes }
+			{ IsAssertion = yes }
 		->
 			{ prog_out__sym_name_to_string(PredName, NameString) },
 			{ string__format("%s %s %s (%s).\n",
@@ -2765,9 +2800,9 @@
 		(
 				% An assertion will not have a
 				% corresponding pred declaration.
-			{ Assertion = yes }
+			{ IsAssertion = yes }
 		;
-			{ Assertion = no },
+			{ IsAssertion = no },
 			maybe_undefined_pred_error(PredName, Arity, PredOrFunc,
 					Context, "clause")
 		),
@@ -2818,12 +2853,14 @@
 		map__keys(Procs, ModeIds)
 		},
 		clauses_info_add_clause(Clauses0, PredId, ModeIds,
-			ClauseVarSet, TVarSet0, Args, Body, Context, Goal,
-			VarSet, TVarSet, Clauses, Warnings, Info0, Info),
+			ClauseVarSet, TVarSet0, Args, Body, Context,
+			IsAssertion, Goal,
+			VarSet, TVarSet, Clauses, Warnings,
+			ModuleInfo0, ModuleInfo1, Info0, Info),
 		{
 		pred_info_set_clauses_info(PredInfo2, Clauses, PredInfo3),
 		(
-			Assertion = yes
+			IsAssertion = yes
 		->
 			pred_info_set_goal_type(PredInfo3, assertion, PredInfo4)
 		;
@@ -2849,10 +2886,10 @@
 		map__det_update(Preds0, PredId, PredInfo, Preds),
 		predicate_table_set_preds(PredicateTable1, Preds,
 			PredicateTable),
-		module_info_set_predicate_table(ModuleInfo0, PredicateTable,
+		module_info_set_predicate_table(ModuleInfo1, PredicateTable,
 			ModuleInfo)
 		},
-		( { Status \= opt_imported, Assertion = no } ->
+		( { Status \= opt_imported } ->
 			% warn about singleton variables 
 			maybe_warn_singletons(VarSet,
 				PredOrFunc - PredName/Arity, ModuleInfo, Goal),
@@ -4230,21 +4267,23 @@
 
 :- pred clauses_info_add_clause(clauses_info::in, pred_id::in, 
 		list(proc_id)::in, prog_varset::in, tvarset::in,
-		list(prog_term)::in, goal::in, prog_context::in,
+		list(prog_term)::in, goal::in, prog_context::in, bool::in,
 		hlds_goal::out, prog_varset::out, tvarset::out,
-		clauses_info::out, list(quant_warning)::out, qual_info::in,
+		clauses_info::out, list(quant_warning)::out, 
+		module_info::in, module_info::out, qual_info::in,
 		qual_info::out, io__state::di, io__state::uo) is det.
 
 clauses_info_add_clause(ClausesInfo0, PredId, ModeIds, CVarSet, TVarSet0,
-		Args, Body, Context, Goal, VarSet, TVarSet0,
-		ClausesInfo, Warnings, Info0, Info) -->
+		Args, Body, Context, IsAssertion, Goal, VarSet, TVarSet0,
+		ClausesInfo, Warnings, Module0, Module, Info0, Info) -->
 	{ ClausesInfo0 = clauses_info(VarSet0, VarTypes0, VarTypes1,
 					HeadVars, ClauseList0,
 					TI_VarMap, TCI_VarMap) },
 	{ update_qual_info(Info0, TVarSet0, VarTypes0, PredId, Info1) },
 	{ varset__merge_subst(VarSet0, CVarSet, VarSet1, Subst) },
-	transform(Subst, HeadVars, Args, Body, VarSet1, Context,
-				Goal, VarSet, Warnings, Info1, Info),
+	transform(Subst, HeadVars, Args, Body, VarSet1, Context, IsAssertion,
+				Goal, VarSet, Warnings, Module0, Module,
+				Info1, Info),
 		% XXX we should avoid append - this gives O(N*N)
 	{ list__append(ClauseList0, [clause(ModeIds, Goal, Context)],
 							ClauseList) },
@@ -4317,22 +4356,71 @@
 %-----------------------------------------------------------------------------
 
 :- pred transform(prog_substitution, list(prog_var), list(prog_term), goal,
-		prog_varset, prog_context, hlds_goal, prog_varset, 
-		list(quant_warning), qual_info, qual_info,
-		io__state, io__state).
-:- mode transform(in, in, in, in, in, in, out, out, out,
+		prog_varset, prog_context, bool, hlds_goal, prog_varset, 
+		list(quant_warning), module_info, module_info,
+		qual_info, qual_info, io__state, io__state).
+:- mode transform(in, in, in, in, in, in, in, out, out, out, in, out,
 			in, out, di, uo) is det.
 
-transform(Subst, HeadVars, Args0, Body, VarSet0, Context,
-		Goal, VarSet, Warnings, Info0, Info) -->
+transform(Subst, HeadVars, Args0, Body, VarSet0, Context, IsAssertion,
+		Goal, VarSet, Warnings, Module0, Module, Info0, Info) -->
 	transform_goal(Body, VarSet0, Subst, Goal1, VarSet1, Info0, Info1),
 	{ term__apply_substitution_to_list(Args0, Subst, Args) },
 	insert_arg_unifications(HeadVars, Args, Context, head, no,
 		Goal1, VarSet1, Goal2, VarSet2, Info1, Info),
 	{ map__init(Empty) },
+		
+		%
+		% Currently every variable in an assertion must be
+		% explicitly quantified, as it has not been determined
+		% what the correct implicit quantification should be for
+		% assertions.
+		%
+	(
+		{ IsAssertion = yes }
+	->
+			% Use Goal1, since HeadVar__* not yet
+			% introduced.
+		{ quantification__goal_vars(Goal1, Unquantified) },
+		{ set__to_sorted_list(Unquantified, ProblemVars0) },
+
+			% The Args are implicitly universally
+			% quantified.
+		{ term__term_list_to_var_list(Args, ArgVars) },
+		{ list__delete_elems(ProblemVars0, ArgVars, ProblemVars) },
+
+		{ list__length(ProblemVars, L) },
+		(
+			{ L > 0 }
+		->
+			prog_out__write_context(Context),
+			(
+				{ L = 1 }
+			->
+				io__write_string("Error: the variable `")
+			;
+				io__write_string("Error: the variables `")
+			),
+			io__write_list(ProblemVars, ",", write_var(VarSet)),
+			io__write_string("' were not explicitly quantified.\n"),
+			{ module_info_incr_errors(Module0, Module) }
+		;
+			{ Module = Module0 }
+		)
+
+	;
+		{ Module = Module0 }
+	),
 	{ implicitly_quantify_clause_body(HeadVars, Goal2, VarSet2, Empty,
 				Goal, VarSet, _, Warnings) }.
 
+	% Allow use of term_io__write_variable in io__write_list
+:- pred write_var(prog_varset::in, prog_var::in,
+		io__state::di, io__state::uo) is det.
+
+write_var(VarSet, Var) -->
+	term_io__write_variable(Var, VarSet).
+
 %-----------------------------------------------------------------------------%
 
 	% Convert goals from the prog_data `goal' structure into the
@@ -5397,7 +5485,7 @@
 
 % This is not considered an unconditional error anymore:
 % if there is no :- pred declaration, we just infer one,
-% unless the `--no-infer-types' option was specified
+% unless the `--no-infer-types' option was specified.
 
 maybe_undefined_pred_error(Name, Arity, PredOrFunc, Context, Description) -->
 	globals__io_lookup_bool_option(infer_types, InferTypes),
===================================================================
RCS file: RCS/mercury_to_goedel.m,v
retrieving revision 1.2
diff -u -r1.2 mercury_to_goedel.m
===================================================================
RCS file: RCS/mercury_to_mercury.m,v
retrieving revision 1.2
diff -u -r1.2 mercury_to_mercury.m
--- mercury_to_mercury.m	1999/07/08 00:56:46	1.2
+++ mercury_to_mercury.m	1999/07/08 07:09:58
@@ -426,9 +426,8 @@
 	io__write_string(":- assertion "),
 	{ Indent = 1 },
 	mercury_output_newline(Indent),
-	mercury_output_goal(Goal, VarSet, Indent, yes),
-	io__write_string("."),
-	io__nl.
+	mercury_output_goal(Goal, VarSet, Indent),
+	io__write_string(".\n").
 
 mercury_output_item(nothing, _) --> [].
 mercury_output_item(typeclass(Constraints, ClassName, Vars, Methods, 
@@ -1711,7 +1710,7 @@
 		[]
 	;
 		io__write_string(" :-\n\t"),
-		mercury_output_goal(Body, VarSet, 1, no)
+		mercury_output_goal(Body, VarSet, 1)
 	),
 	io__write_string(".\n").
 
@@ -1741,154 +1740,146 @@
 	;
 		mercury_output_term(Result, VarSet, no),
 		io__write_string(" :-\n\t"),
-		mercury_output_goal(Body, VarSet, 1, no)
+		mercury_output_goal(Body, VarSet, 1)
 	),
 	io__write_string(".\n").
 
-:- pred mercury_output_goal(goal, prog_varset, int, bool, io__state, io__state).
-:- mode mercury_output_goal(in, in, in, in, di, uo) is det.
+:- pred mercury_output_goal(goal, prog_varset, int, io__state, io__state).
+:- mode mercury_output_goal(in, in, in, di, uo) is det.
 
-mercury_output_goal(Goal - _Context, VarSet, Indent, InAssertion) -->
-	mercury_output_goal_2(Goal, VarSet, Indent, InAssertion).
+mercury_output_goal(Goal - _Context, VarSet, Indent) -->
+	mercury_output_goal_2(Goal, VarSet, Indent).
 
-:- pred mercury_output_goal_2(goal_expr, prog_varset, int, bool,
+:- pred mercury_output_goal_2(goal_expr, prog_varset, int,
 		io__state, io__state).
-:- mode mercury_output_goal_2(in, in, in, in, di, uo) is det.
+:- mode mercury_output_goal_2(in, in, in, di, uo) is det.
 
-mercury_output_goal_2(fail, _, _, _) -->
+mercury_output_goal_2(fail, _, _) -->
 	io__write_string("fail").
 
-mercury_output_goal_2(true, _, _, _) -->
+mercury_output_goal_2(true, _, _) -->
 	io__write_string("true").
 
-	% Implication and equivalence should have been transformed out
-	% by now, unless they are in an assertion.
-mercury_output_goal_2(implies(_G1,_G2), _VarSet, _Indent, no) -->
-	{ error("mercury_to_mercury: implies/2 in mercury_output_goal")}.
-mercury_output_goal_2(implies(G1,G2), VarSet, Indent, yes) -->
+mercury_output_goal_2(implies(G1,G2), VarSet, Indent) -->
 	{ Indent1 is Indent + 1 },
 	io__write_string("("),
 	mercury_output_newline(Indent1),
-	mercury_output_goal(G1, VarSet, Indent1, yes),
+	mercury_output_goal(G1, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string("=>"),
 	mercury_output_newline(Indent1),
-	mercury_output_goal(G2, VarSet, Indent1, yes),
+	mercury_output_goal(G2, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string(")").
 
-mercury_output_goal_2(equivalent(_G1,_G2), _VarSet, _Indent, no) -->
-	{ error("mercury_to_mercury: equivalent/2 in mercury_output_goal")}.
-mercury_output_goal_2(equivalent(G1,G2), VarSet, Indent, yes) -->
+mercury_output_goal_2(equivalent(G1,G2), VarSet, Indent) -->
 	{ Indent1 is Indent + 1 },
 	io__write_string("("),
 	mercury_output_newline(Indent1),
-	mercury_output_goal(G1, VarSet, Indent1, yes),
+	mercury_output_goal(G1, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string("<=>"),
 	mercury_output_newline(Indent1),
-	mercury_output_goal(G2, VarSet, Indent1, yes),
+	mercury_output_goal(G2, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string(")").
 
-mercury_output_goal_2(some(Vars, Goal), VarSet, Indent, InAssertion) -->
+mercury_output_goal_2(some(Vars, Goal), VarSet, Indent) -->
 	( { Vars = [] } ->
-		mercury_output_goal(Goal, VarSet, Indent, InAssertion)
+		mercury_output_goal(Goal, VarSet, Indent)
 	;
 		io__write_string("some ["),
 		mercury_output_vars(Vars, VarSet, no),
 		io__write_string("] ("),
 		{ Indent1 is Indent + 1 },
 		mercury_output_newline(Indent1),
-		mercury_output_goal(Goal, VarSet, Indent1, InAssertion),
+		mercury_output_goal(Goal, VarSet, Indent1),
 		mercury_output_newline(Indent),
 		io__write_string(")")
 	).
 
-mercury_output_goal_2(all(Vars, Goal), VarSet, Indent, InAssertion) -->
+mercury_output_goal_2(all(Vars, Goal), VarSet, Indent) -->
 	( { Vars = [] } ->
-		mercury_output_goal(Goal, VarSet, Indent, InAssertion)
+		mercury_output_goal(Goal, VarSet, Indent)
 	;
 		io__write_string("all ["),
 		mercury_output_vars(Vars, VarSet, no),
 		io__write_string("] ("),
 		{ Indent1 is Indent + 1 },
 		mercury_output_newline(Indent1),
-		mercury_output_goal(Goal, VarSet, Indent1, InAssertion),
+		mercury_output_goal(Goal, VarSet, Indent1),
 		mercury_output_newline(Indent),
 		io__write_string(")")
 	).
 
-mercury_output_goal_2(if_then_else(Vars, A, B, C), VarSet, Indent,
-		InAssertion) -->
+mercury_output_goal_2(if_then_else(Vars, A, B, C), VarSet, Indent) -->
 	io__write_string("(if"),
 	mercury_output_some(Vars, VarSet),
 	{ Indent1 is Indent + 1 },
 	mercury_output_newline(Indent1),
-	mercury_output_goal(A, VarSet, Indent1, InAssertion),
+	mercury_output_goal(A, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string("then"),
 	mercury_output_newline(Indent1),
-	mercury_output_goal(B, VarSet, Indent1, InAssertion),
+	mercury_output_goal(B, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string("else"),
 	mercury_output_newline(Indent1),
-	mercury_output_goal(C, VarSet, Indent1, InAssertion),
+	mercury_output_goal(C, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string(")").
 
-mercury_output_goal_2(if_then(Vars, A, B), VarSet, Indent, InAssertion) -->
+mercury_output_goal_2(if_then(Vars, A, B), VarSet, Indent) -->
 	io__write_string("(if"),
 	mercury_output_some(Vars, VarSet),
 	{ Indent1 is Indent + 1 },
 	mercury_output_newline(Indent1),
-	mercury_output_goal(A, VarSet, Indent1, InAssertion),
+	mercury_output_goal(A, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string("then"),
 	mercury_output_newline(Indent1),
-	mercury_output_goal(B, VarSet, Indent1, InAssertion),
+	mercury_output_goal(B, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string(")").
 
-mercury_output_goal_2(not(Goal), VarSet, Indent, InAssertion) -->
+mercury_output_goal_2(not(Goal), VarSet, Indent) -->
 	io__write_string("\\+ ("),
 	{ Indent1 is Indent + 1 },
 	mercury_output_newline(Indent1),
-	mercury_output_goal(Goal, VarSet, Indent1, InAssertion),
+	mercury_output_goal(Goal, VarSet, Indent1),
 	mercury_output_newline(Indent),
 	io__write_string(")").
 
-mercury_output_goal_2((A,B), VarSet, Indent, InAssertion) -->
-	mercury_output_goal(A, VarSet, Indent, InAssertion),
+mercury_output_goal_2((A,B), VarSet, Indent) -->
+	mercury_output_goal(A, VarSet, Indent),
 	io__write_string(","),
 	mercury_output_newline(Indent),
-	mercury_output_goal(B, VarSet, Indent, InAssertion).
+	mercury_output_goal(B, VarSet, Indent).
 
-mercury_output_goal_2((A & B), VarSet, Indent, InAssertion) -->
+mercury_output_goal_2((A & B), VarSet, Indent) -->
 	io__write_string("("),
 	{ Indent1 is Indent + 1 },
 	mercury_output_newline(Indent1),
-	mercury_output_goal(A, VarSet, Indent1, InAssertion),
-	mercury_output_par_conj(B, VarSet, Indent, InAssertion),
+	mercury_output_goal(A, VarSet, Indent1),
+	mercury_output_par_conj(B, VarSet, Indent),
 	mercury_output_newline(Indent),
 	io__write_string(")").
 
 
-mercury_output_goal_2((A;B), VarSet, Indent, InAssertion) -->
+mercury_output_goal_2((A;B), VarSet, Indent) -->
 	io__write_string("("),
 	{ Indent1 is Indent + 1 },
 	mercury_output_newline(Indent1),
-	mercury_output_goal(A, VarSet, Indent1, InAssertion),
-	mercury_output_disj(B, VarSet, Indent, InAssertion),
+	mercury_output_goal(A, VarSet, Indent1),
+	mercury_output_disj(B, VarSet, Indent),
 	mercury_output_newline(Indent),
 	io__write_string(")").
 
-mercury_output_goal_2(call(Name, Term, Purity), VarSet, Indent,
-		_InAssertion) -->
+mercury_output_goal_2(call(Name, Term, Purity), VarSet, Indent) -->
 	write_purity_prefix(Purity),
 	mercury_output_call(Name, Term, VarSet, Indent).
 
-mercury_output_goal_2(unify(A, B), VarSet, _Indent, _InAssertion) -->
+mercury_output_goal_2(unify(A, B), VarSet, _Indent) -->
 	mercury_output_term(A, VarSet, no),
 	io__write_string(" = "),
 	mercury_output_term(B, VarSet, no, next_to_graphic_token).
@@ -1914,10 +1905,10 @@
 			Term, Context0), VarSet, no, next_to_graphic_token)
 	).
 
-:- pred mercury_output_disj(goal, prog_varset, int, bool, io__state, io__state).
-:- mode mercury_output_disj(in, in, in, in, di, uo) is det.
+:- pred mercury_output_disj(goal, prog_varset, int, io__state, io__state).
+:- mode mercury_output_disj(in, in, in, di, uo) is det.
 
-mercury_output_disj(Goal, VarSet, Indent, InAssertion) -->
+mercury_output_disj(Goal, VarSet, Indent) -->
 	mercury_output_newline(Indent),
 	io__write_string(";"),
 	{ Indent1 is Indent + 1 },
@@ -1925,17 +1916,17 @@
 	(
 		{ Goal = (A;B) - _Context }
 	->
-		mercury_output_goal(A, VarSet, Indent1, InAssertion),
-		mercury_output_disj(B, VarSet, Indent, InAssertion)
+		mercury_output_goal(A, VarSet, Indent1),
+		mercury_output_disj(B, VarSet, Indent)
 	;
-		mercury_output_goal(Goal, VarSet, Indent1, InAssertion)
+		mercury_output_goal(Goal, VarSet, Indent1)
 	).
 
-:- pred mercury_output_par_conj(goal, prog_varset, int, bool,
+:- pred mercury_output_par_conj(goal, prog_varset, int,
 		io__state, io__state).
-:- mode mercury_output_par_conj(in, in, in, in, di, uo) is det.
+:- mode mercury_output_par_conj(in, in, in, di, uo) is det.
 
-mercury_output_par_conj(Goal, VarSet, Indent, InAssertion) -->
+mercury_output_par_conj(Goal, VarSet, Indent) -->
 	mercury_output_newline(Indent),
 	io__write_string("&"),
 	{ Indent1 is Indent + 1 },
@@ -1943,10 +1934,10 @@
 	(
 		{ Goal = (A & B) - _Context }
 	->
-		mercury_output_goal(A, VarSet, Indent1, InAssertion),
-		mercury_output_par_conj(B, VarSet, Indent, InAssertion)
+		mercury_output_goal(A, VarSet, Indent1),
+		mercury_output_par_conj(B, VarSet, Indent)
 	;
-		mercury_output_goal(Goal, VarSet, Indent1, InAssertion)
+		mercury_output_goal(Goal, VarSet, Indent1)
 	).
 
 :- pred mercury_output_some(list(var(T)), varset(T), io__state, io__state).
===================================================================
RCS file: RCS/module_qual.m,v
retrieving revision 1.1
diff -u -r1.1 module_qual.m
===================================================================
RCS file: RCS/post_typecheck.m,v
retrieving revision 1.1
diff -u -r1.1 post_typecheck.m
--- post_typecheck.m	1999/07/06 06:41:11	1.1
+++ post_typecheck.m	1999/07/08 07:24:34
@@ -84,11 +84,19 @@
 		pred_info, pred_info, io__state, io__state).
 :- mode post_typecheck__finish_ill_typed_pred(in, in, in, out, di, uo) is det.
 
+	% Now that the assertion has finished being typechecked,
+	% remove it from further processing and store it in the
+	% assertion_table.
+:- pred post_typecheck__finish_assertion(module_info, pred_id,
+		module_info) is det.
+:- mode post_typecheck__finish_assertion(in, in, out) is det.
+
 %-----------------------------------------------------------------------------%
+
 :- implementation.
 
 :- import_module typecheck, clause_to_proc, mode_util, inst_match.
-:- import_module mercury_to_mercury, prog_out, hlds_out, type_util.
+:- import_module mercury_to_mercury, prog_out, hlds_data, hlds_out, type_util.
 :- import_module globals, options.
 
 :- import_module map, set, assoc_list, bool, std_util, term.
@@ -366,6 +374,13 @@
 		PredInfo0, PredInfo) -->
 	post_typecheck__propagate_types_into_modes(ModuleInfo, PredId,
 		PredInfo0, PredInfo).
+
+post_typecheck__finish_assertion(Module0, PredId, Module) :-
+	module_info_assertion_table(Module0, AssertionTable0),
+	assertion_table_add_assertion(PredId, AssertionTable0, AssertionTable),
+	module_info_set_assertion_table(Module0, AssertionTable, Module1),
+	module_info_remove_predid(Module1, PredId, Module).
+	
 
 	% 
 	% Ensure that all constructors occurring in predicate mode
===================================================================
RCS file: RCS/prog_data.m,v
retrieving revision 1.1
diff -u -r1.1 prog_data.m
===================================================================
RCS file: RCS/prog_io.m,v
retrieving revision 1.1
diff -u -r1.1 prog_io.m
--- prog_io.m	1999/07/06 06:41:11	1.1
+++ prog_io.m	1999/07/08 07:02:35
@@ -183,7 +183,7 @@
 :- implementation.
 
 :- import_module prog_io_goal, prog_io_dcg, prog_io_pragma, prog_io_util.
-:- import_module prog_io_typeclass, prog_io_assertion.
+:- import_module prog_io_typeclass.
 :- import_module hlds_data, hlds_pred, prog_util, prog_out.
 :- import_module globals, options, (inst).
 :- import_module purity.
@@ -1097,6 +1097,17 @@
 attribute_description(constraints(univ, _), "type class constraint (`<=')").
 attribute_description(constraints(exist, _),
 	"existentially quantified type class constraint (`=>')").
+
+%-----------------------------------------------------------------------------%
+
+	% parse the assertion declaration. 
+:- pred parse_assertion(module_name, varset, list(term), maybe1(item)).
+:- mode parse_assertion(in, in, in, out) is semidet.
+
+parse_assertion(_ModuleName, VarSet, [AssertionTerm], Result) :-
+	varset__coerce(VarSet, ProgVarSet),
+	parse_goal(AssertionTerm, ProgVarSet, AssertGoal, AssertVarSet),
+	Result = ok(assertion(AssertGoal, AssertVarSet)).
 
 %-----------------------------------------------------------------------------%
 
===================================================================
RCS file: RCS/prog_io_assertion.m,v
retrieving revision 1.1
diff -u -r1.1 prog_io_assertion.m
===================================================================
RCS file: RCS/purity.m,v
retrieving revision 1.1
diff -u -r1.1 purity.m
--- purity.m	1999/07/06 06:41:11	1.1
+++ purity.m	1999/07/08 07:28:17
@@ -135,7 +135,7 @@
 
 :- implementation.
 
-:- import_module make_hlds, hlds_data, hlds_pred, prog_io_util.
+:- import_module make_hlds, hlds_pred, prog_io_util.
 :- import_module type_util, mode_util, code_util, prog_data, unify_proc.
 :- import_module globals, options, mercury_to_mercury, hlds_out.
 :- import_module passes_aux, typecheck, module_qual, clause_to_proc.
@@ -294,7 +294,8 @@
 	(
 		{ pred_info_get_goal_type(PredInfo0, assertion) }
 	->
-		{ module_info_remove_predid(ModuleInfo1, PredId, ModuleInfo2) }
+		{ post_typecheck__finish_assertion(ModuleInfo1,
+				PredId, ModuleInfo2) }
 	;
 		{ ModuleInfo2 = ModuleInfo1 }
 	),
===================================================================
RCS file: RCS/typecheck.m,v
retrieving revision 1.1
diff -u -r1.1 typecheck.m

*** Full DIFF vs update source ***

Index: compiler/error_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/error_util.m,v
retrieving revision 1.8
diff -u -r1.8 error_util.m
--- error_util.m	1999/06/16 00:38:16	1.8
+++ error_util.m	1999/07/08 06:48:56
@@ -323,16 +323,22 @@
 		PredOrFuncPart = "function",
 		OrigArity is Arity - 1
 	),
-	string__int_to_string(OrigArity, ArityPart),
-	string__append_list([
-		PredOrFuncPart,
-		" `",
-		ModuleNameString,
-		":",
-		PredName,
-		"/",
-		ArityPart,
-		"'"], Piece).
+	(
+		pred_info_get_goal_type(PredInfo, assertion)
+	->
+		Piece = "assertion"
+	;
+		string__int_to_string(OrigArity, ArityPart),
+		string__append_list([
+			PredOrFuncPart,
+			" `",
+			ModuleNameString,
+			":",
+			PredName,
+			"/",
+			ArityPart,
+			"'"], Piece)
+	).
 
 error_util__describe_one_proc_name(Module, proc(PredId, ProcId), Piece) :-
 	error_util__describe_one_pred_name(Module, PredId, PredPiece),
Index: compiler/hlds_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_data.m,v
retrieving revision 1.35
diff -u -r1.35 hlds_data.m
--- hlds_data.m	1999/07/08 05:08:50	1.35
+++ hlds_data.m	1999/07/08 09:48:39
@@ -805,3 +805,51 @@
 :- type superclass_table == multi_map(class_id, subclass_details).
 
 %-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- interface.
+
+	%
+	% A table that records all the assertions in the system.
+	% An assertion is a goal that will always evaluate to true,
+	% subject to the constraints imposed by the quantifiers.
+	%
+	% ie :- assertion all [A] some [B] (B > A)
+	% 
+	% The above assertion states that for all possible values of A,
+	% there will exist at least one value, B, such that B is greater
+	% then A.
+	%
+:- type assert_id.
+:- type assertion_table.
+
+:- pred assertion_table_init(assertion_table::out) is det.
+
+:- pred assertion_table_add_assertion(pred_id::in,
+		assertion_table::in, assertion_table::out) is det.
+
+:- pred assertion_table_lookup(assertion_table::in, assert_id::in,
+		pred_id::out) is det.
+
+:- implementation.
+
+:- import_module int.
+
+:- type assert_id == int.
+:- type assertion_table 
+	---> 	assertion_table(assert_id, map(assert_id, pred_id)).
+
+assertion_table_init(assertion_table(0, AssertionMap)) :-
+	map__init(AssertionMap).
+
+assertion_table_add_assertion(Assertion, AssertionTable0, AssertionTable) :-
+	AssertionTable0 = assertion_table(Id, AssertionMap0),
+	map__det_insert(AssertionMap0, Id, Assertion, AssertionMap),
+	AssertionTable = assertion_table(Id + 1, AssertionMap).
+
+assertion_table_lookup(AssertionTable, Id, Assertion) :-
+	AssertionTable = assertion_table(_MaxId, AssertionMap),
+	map__lookup(AssertionMap, Id, Assertion).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
Index: compiler/hlds_module.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_module.m,v
retrieving revision 1.44
diff -u -r1.44 hlds_module.m
--- hlds_module.m	1999/04/30 08:23:46	1.44
+++ hlds_module.m	1999/07/08 07:24:05
@@ -198,6 +198,13 @@
 	module_info).
 :- mode module_info_set_superclasses(in, in, out) is det.
 
+:- pred module_info_assertion_table(module_info, assertion_table).
+:- mode module_info_assertion_table(in, out) is det.
+
+:- pred module_info_set_assertion_table(module_info, assertion_table,
+	module_info).
+:- mode module_info_set_assertion_table(in, in, out) is det.
+
 	% The cell count is used as a unique cell number for
 	% constants in the generated C code.
 :- pred module_info_get_cell_count(module_info, int).
@@ -555,6 +562,7 @@
 			class_table,
 			instance_table,
 			superclass_table,
+			assertion_table,
 			int		% cell count, passed into code_info
 					% and used to generate unique label
 					% numbers for constant terms in the
@@ -622,12 +630,15 @@
 	map__init(InstanceTable),
 	map__init(SuperClassTable),
 	set__init(ModuleNames),
+
+	assertion_table_init(AssertionTable),
+
 	ModuleSubInfo = module_sub(Name, Globals, [], [], no, 0, 0, [], 
 		[], [], StratPreds, UnusedArgInfo, 0, ModuleNames,
 		no_aditi_compilation, TypeSpecInfo),
 	ModuleInfo = module(ModuleSubInfo, PredicateTable, Requests,
 		UnifyPredMap, GlobalData, Types, Insts, Modes, Ctors,
-		ClassTable, SuperClassTable, InstanceTable, 0).
+		ClassTable, SuperClassTable, InstanceTable, AssertionTable, 0).
 
 %-----------------------------------------------------------------------------%
 
@@ -798,7 +809,8 @@
 % J			class_table,
 % K			instance_table,
 % L			superclass_table,
-% M			int		% cell count, passed into code_info
+% M			assertion_table
+% N			int		% cell count, passed into code_info
 %					% and used to generate unique label
 %					% numbers for constant terms in the
 %					% generated C code
@@ -809,99 +821,106 @@
 	% Various predicates which access the module_info data structure.
 
 module_info_get_sub_info(MI0, A) :-
-	MI0 = module(A, _, _, _, _, _, _, _, _, _, _, _, _).
+	MI0 = module(A, _, _, _, _, _, _, _, _, _, _, _, _, _).
 
 module_info_get_predicate_table(MI0, B) :-
-	MI0 = module(_, B, _, _, _, _, _, _, _, _, _, _, _).
+	MI0 = module(_, B, _, _, _, _, _, _, _, _, _, _, _, _).
 
 module_info_get_proc_requests(MI0, C) :-
-	MI0 = module(_, _, C, _, _, _, _, _, _, _, _, _, _).
+	MI0 = module(_, _, C, _, _, _, _, _, _, _, _, _, _, _).
 
 module_info_get_special_pred_map(MI0, D) :-
-	MI0 = module(_, _, _, D, _, _, _, _, _, _, _, _, _).
+	MI0 = module(_, _, _, D, _, _, _, _, _, _, _, _, _, _).
 
 module_info_get_global_data(MI0, E) :-
-	MI0 = module(_, _, _, _, E, _, _, _, _, _, _, _, _).
+	MI0 = module(_, _, _, _, E, _, _, _, _, _, _, _, _, _).
 
 module_info_types(MI0, F) :-
-	MI0 = module(_, _, _, _, _, F, _, _, _, _, _, _, _).
+	MI0 = module(_, _, _, _, _, F, _, _, _, _, _, _, _, _).
 
 module_info_insts(MI0, G) :-
-	MI0 = module(_, _, _, _, _, _, G, _, _, _, _, _, _).
+	MI0 = module(_, _, _, _, _, _, G, _, _, _, _, _, _, _).
 
 module_info_modes(MI0, H) :-
-	MI0 = module(_, _, _, _, _, _, _, H, _, _, _, _, _).
+	MI0 = module(_, _, _, _, _, _, _, H, _, _, _, _, _, _).
 
 module_info_ctors(MI0, I) :-
-	MI0 = module(_, _, _, _, _, _, _, _, I, _, _, _, _).
+	MI0 = module(_, _, _, _, _, _, _, _, I, _, _, _, _, _).
 
 module_info_classes(MI0, J) :-
-	MI0 = module(_, _, _, _, _, _, _, _, _, J, _, _, _).
+	MI0 = module(_, _, _, _, _, _, _, _, _, J, _, _, _, _).
 
 module_info_instances(MI0, K) :-
-	MI0 = module(_, _, _, _, _, _, _, _, _, _, K, _, _).
+	MI0 = module(_, _, _, _, _, _, _, _, _, _, K, _, _, _).
 
 module_info_superclasses(MI0, L) :-
-	MI0 = module(_, _, _, _, _, _, _, _, _, _, _, L, _).
+	MI0 = module(_, _, _, _, _, _, _, _, _, _, _, L, _, _).
+
+module_info_assertion_table(MI0, M) :-
+	MI0 = module(_, _, _, _, _, _, _, _, _, _, _, _, M, _).
 
-module_info_get_cell_count(MI0, M) :-
-	MI0 = module(_, _, _, _, _, _, _, _, _, _, _, _, M).
+module_info_get_cell_count(MI0, N) :-
+	MI0 = module(_, _, _, _, _, _, _, _, _, _, _, _, _, N).
 
 %-----------------------------------------------------------------------------%
 
 	% Various predicates which modify the module_info data structure.
 
 module_info_set_sub_info(MI0, A, MI) :-
-	MI0 = module(_, B, C, D, E, F, G, H, I, J, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(_, B, C, D, E, F, G, H, I, J, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_predicate_table(MI0, B, MI) :-
-	MI0 = module(A, _, C, D, E, F, G, H, I, J, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, _, C, D, E, F, G, H, I, J, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_proc_requests(MI0, C, MI) :-
-	MI0 = module(A, B, _, D, E, F, G, H, I, J, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, _, D, E, F, G, H, I, J, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_special_pred_map(MI0, D, MI) :-
-	MI0 = module(A, B, C, _, E, F, G, H, I, J, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, C, _, E, F, G, H, I, J, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_global_data(MI0, E, MI) :-
-	MI0 = module(A, B, C, D, _, F, G, H, I, J, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, C, D, _, F, G, H, I, J, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_types(MI0, F, MI) :-
-	MI0 = module(A, B, C, D, E, _, G, H, I, J, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, C, D, E, _, G, H, I, J, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_insts(MI0, G, MI) :-
-	MI0 = module(A, B, C, D, E, F, _, H, I, J, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, C, D, E, F, _, H, I, J, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_modes(MI0, H, MI) :-
-	MI0 = module(A, B, C, D, E, F, G, _, I, J, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, C, D, E, F, G, _, I, J, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_ctors(MI0, I, MI) :-
-	MI0 = module(A, B, C, D, E, F, G, H, _, J, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, C, D, E, F, G, H, _, J, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_classes(MI0, J, MI) :-
-	MI0 = module(A, B, C, D, E, F, G, H, I, _, K, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, C, D, E, F, G, H, I, _, K, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_instances(MI0, K, MI) :-
-	MI0 = module(A, B, C, D, E, F, G, H, I, J, _, L, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, C, D, E, F, G, H, I, J, _, L, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 module_info_set_superclasses(MI0, L, MI) :-
-	MI0 = module(A, B, C, D, E, F, G, H, I, J, K, _, M),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+	MI0 = module(A, B, C, D, E, F, G, H, I, J, K, _, M, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
-module_info_set_cell_count(MI0, M, MI) :-
-	MI0 = module(A, B, C, D, E, F, G, H, I, J, K, L, _),
-	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M).
+module_info_set_assertion_table(MI0, M, MI) :-
+	MI0 = module(A, B, C, D, E, F, G, H, I, J, K, L, _, N),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
+
+module_info_set_cell_count(MI0, N, MI) :-
+	MI0 = module(A, B, C, D, E, F, G, H, I, J, K, L, M, _),
+	MI  = module(A, B, C, D, E, F, G, H, I, J, K, L, M, N).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_out.m,v
retrieving revision 1.221
diff -u -r1.221 hlds_out.m
--- hlds_out.m	1999/06/30 17:12:24	1.221
+++ hlds_out.m	1999/07/08 06:45:33
@@ -271,7 +271,7 @@
 	io__write_string("<tabling_pointer>").
 
 	% The code of this predicate duplicates the functionality of
-	% term_errors__describe_one_pred_name. Changes here should be made
+	% error_util__describe_one_pred_name. Changes here should be made
 	% there as well.
 
 hlds_out__write_pred_id(ModuleInfo, PredId) -->
@@ -298,6 +298,10 @@
 			check_typeclass__introduced_pred_name_prefix) } 
 	->
 		io__write_string("type class method implementation")
+	;
+		{ pred_info_get_goal_type(PredInfo, assertion) }
+	->
+		io__write_string("assertion")
 	;
 		hlds_out__write_pred_or_func(PredOrFunc),
 		io__write_string(" `"),
Index: compiler/hlds_pred.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_pred.m,v
retrieving revision 1.60
diff -u -r1.60 hlds_pred.m
--- hlds_pred.m	1999/07/08 05:08:51	1.60
+++ hlds_pred.m	1999/07/08 09:48:43
@@ -179,6 +179,7 @@
 
 :- type goal_type 	--->	pragmas		% pragma c_code(...)
 			;	clauses		
+			;	(assertion)
 			;	none.
 
 	% Note: `liveness' and `liveness_info' record liveness in the sense
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/make_hlds.m,v
retrieving revision 1.297
diff -u -r1.297 make_hlds.m
--- make_hlds.m	1999/07/08 05:08:53	1.297
+++ make_hlds.m	1999/07/08 09:48:59
@@ -220,6 +220,8 @@
 
 add_item_decl_pass_1(pragma(_), _, Status, Module, Status, Module) --> [].
 
+add_item_decl_pass_1(assertion(_, _), _, Status, Module, Status, Module) --> [].
+
 add_item_decl_pass_1(module_defn(_VarSet, ModuleDefn), Context,
 		Status0, Module0, Status, Module) -->
 	( { module_defn_update_import_status(ModuleDefn, Status1) } ->
@@ -514,6 +516,7 @@
 		{ error("make_hlds.m: can't find func declaration") }
 	).
 
+add_item_decl_pass_2(assertion(_, _), _, Status, Module, Status, Module) --> [].
 add_item_decl_pass_2(func_clause(_, _, _, _, _), _, Status, Module, Status,
 		Module) --> [].
 add_item_decl_pass_2(pred_clause(_, _, _, _), _, Status, Module, Status, Module)
@@ -605,13 +608,15 @@
 add_item_clause(func_clause(VarSet, PredName, Args, Result, Body), Status,
 		Status, Context, Module0, Module, Info0, Info) -->
 	check_not_exported(Status, Context, "clause"),
+	{ IsAssertion = no },
 	module_add_func_clause(Module0, VarSet, PredName, Args, Result, Body,
-		Status, Context, Module, Info0, Info).
+		Status, Context, IsAssertion, Module, Info0, Info).
 add_item_clause(pred_clause(VarSet, PredName, Args, Body), Status, Status,
 		Context, Module0, Module, Info0, Info) -->
 	check_not_exported(Status, Context, "clause"),
+	{ IsAssertion = no },
 	module_add_pred_clause(Module0, VarSet, PredName, Args, Body, Status,
-		Context, Module, Info0, Info).
+		Context, IsAssertion, Module, Info0, Info).
 add_item_clause(type_defn(_, _, _), Status, Status, _,
 				Module, Module, Info, Info) --> [].
 add_item_clause(inst_defn(_, _, _), Status, Status, _,
@@ -687,6 +692,48 @@
 		{ Module = Module0 },
 		{ Info = Info0 }	
 	).
+add_item_clause(assertion(Goal0, VarSet),
+		Status, Status, Context, Module0, Module, Info0, Info) -->
+
+		%
+		% If the outermost existentially quantified variables
+		% are placed in the head of the assertion, the
+		% typechecker will avoid warning about unbound
+		% type variables as this implicity adds a universal
+		% quantification of the typevariables needed.
+		%
+	(
+		{ Goal0 = all(Vars, AllGoal) - _Context }
+	->
+		{ term__var_list_to_term_list(Vars, HeadVars) },
+		{ Goal = AllGoal }
+	;
+		{ HeadVars = [] },
+		{ Goal = Goal0 }
+	),
+
+	{ term__context_line(Context, Line) },
+	{ term__context_file(Context, File) },
+	{ string__format("assertion__%d__%s", [i(Line), s(File)], Name) },
+
+		%
+		% The assertions are recorded as a predicate whose
+		% goal_type is set to assertion.  This allows us to
+		% leverage off all the other checks in the compiler that
+		% operate on predicates.
+		%
+		% :- assertion all [A,B,R] ( R = A + B <=> R = B + A ).
+		%
+		% becomes
+		%
+		% assertion__lineno_filename(A, B, R) :-
+		% 	( R = A + B <=> R = B + A ).
+		%
+	{ IsAssertion = yes },
+	module_add_pred_clause(Module0, VarSet, unqualified(Name),
+			HeadVars, Goal, Status, Context, IsAssertion, Module,
+			Info0, Info).
+
 add_item_clause(nothing, Status, Status, _, Module, Module, Info, Info) --> [].
 add_item_clause(typeclass(_, _, _, _, _),
 	Status, Status, _, Module, Module, Info, Info) --> [].
@@ -2679,12 +2726,13 @@
 
 :- pred module_add_pred_clause(module_info, prog_varset, sym_name,
 		list(prog_term), goal, import_status, prog_context,
-		module_info, qual_info, qual_info, io__state, io__state).
-:- mode module_add_pred_clause(in, in, in, in, in, in, in, out,
+		bool, module_info, qual_info, qual_info, io__state, io__state).
+:- mode module_add_pred_clause(in, in, in, in, in, in, in, in, out,
 		in, out, di, uo) is det.
 
 module_add_pred_clause(ModuleInfo0, ClauseVarSet, PredName, Args, Body,
-			Status, Context, ModuleInfo, Info0, Info) -->
+			Status, Context, IsAssertion, ModuleInfo,
+			Info0, Info) -->
 		% print out a progress message
 	globals__io_lookup_bool_option(very_verbose, VeryVerbose),
 	( { VeryVerbose = yes } ->
@@ -2696,16 +2744,18 @@
 		[]
 	),
 	module_add_clause(ModuleInfo0, ClauseVarSet, PredName, Args, Body,
-		Status, Context, predicate, ModuleInfo, Info0, Info).
+		Status, Context, predicate, IsAssertion, ModuleInfo,
+		Info0, Info).
 
 :- pred module_add_func_clause(module_info, prog_varset, sym_name,
 		list(prog_term), prog_term, goal, import_status, prog_context,
-		module_info, qual_info, qual_info, io__state, io__state).
+		bool, module_info, qual_info, qual_info, io__state, io__state).
 :- mode module_add_func_clause(in, in, in, in, in,
-	in, in, in, out, in, out, di, uo) is det.
+	in, in, in, in, out, in, out, di, uo) is det.
 
 module_add_func_clause(ModuleInfo0, ClauseVarSet, FuncName, Args0, Result, Body,
-			Status, Context, ModuleInfo, Info0, Info) -->
+			Status, Context, IsAssertion, ModuleInfo,
+			Info0, Info) -->
 		% print out a progress message
 	globals__io_lookup_bool_option(very_verbose, VeryVerbose),
 	( { VeryVerbose = yes } ->
@@ -2718,16 +2768,18 @@
 	),
 	{ list__append(Args0, [Result], Args) },
 	module_add_clause(ModuleInfo0, ClauseVarSet, FuncName, Args, Body,
-		Status, Context, function, ModuleInfo, Info0, Info).
+		Status, Context, function, IsAssertion, ModuleInfo,
+		Info0, Info).
 
 :- pred module_add_clause(module_info, prog_varset, sym_name, list(prog_term),
-		goal, import_status, prog_context, pred_or_func,
+		goal, import_status, prog_context, pred_or_func, bool,
 		module_info, qual_info, qual_info, io__state, io__state).
-:- mode module_add_clause(in, in, in, in, in, in, in, in,
+:- mode module_add_clause(in, in, in, in, in, in, in, in, in,
 		out, in, out, di, uo) is det.
 
 module_add_clause(ModuleInfo0, ClauseVarSet, PredName, Args, Body, Status,
-			Context, PredOrFunc, ModuleInfo, Info0, Info) -->
+			Context, PredOrFunc, IsAssertion, ModuleInfo,
+			Info0, Info) -->
 		% Lookup the pred declaration in the predicate table.
 		% (If it's not there, call maybe_undefined_pred_error
 		% and insert an implicit declaration for the predicate.)
@@ -2739,11 +2791,30 @@
 				PredOrFunc, PredName, Arity, [PredId0]) }
 	->
 		{ PredId = PredId0 },
-		{ PredicateTable1 = PredicateTable0 }
+		{ PredicateTable1 = PredicateTable0 },
+		(
+			{ IsAssertion = yes }
+		->
+			{ prog_out__sym_name_to_string(PredName, NameString) },
+			{ string__format("%s %s %s (%s).\n",
+				[s("Attempted to introduce a predicate"),
+				s("for an assertion with an identical"),
+				s("name to an existing predicate"),
+				s(NameString)], String) },
+			{ error(String) }
+		;
+			[]
+		)
 	;
-
-		maybe_undefined_pred_error(PredName, Arity, PredOrFunc,
-			Context, "clause"),
+		(
+				% An assertion will not have a
+				% corresponding pred declaration.
+			{ IsAssertion = yes }
+		;
+			{ IsAssertion = no },
+			maybe_undefined_pred_error(PredName, Arity, PredOrFunc,
+					Context, "clause")
+		),
 		{ preds_add_implicit(ModuleInfo0, PredicateTable0,
 				ModuleName, PredName, Arity, Status, Context,
 				PredOrFunc,
@@ -2791,11 +2862,19 @@
 		map__keys(Procs, ModeIds)
 		},
 		clauses_info_add_clause(Clauses0, PredId, ModeIds,
-			ClauseVarSet, TVarSet0, Args, Body, Context, Goal,
-			VarSet, TVarSet, Clauses, Warnings, Info0, Info),
+			ClauseVarSet, TVarSet0, Args, Body, Context,
+			IsAssertion, Goal,
+			VarSet, TVarSet, Clauses, Warnings,
+			ModuleInfo0, ModuleInfo1, Info0, Info),
 		{
 		pred_info_set_clauses_info(PredInfo2, Clauses, PredInfo3),
-		pred_info_set_goal_type(PredInfo3, clauses, PredInfo4),
+		(
+			IsAssertion = yes
+		->
+			pred_info_set_goal_type(PredInfo3, assertion, PredInfo4)
+		;
+			pred_info_set_goal_type(PredInfo3, clauses, PredInfo4)
+		),
 		pred_info_set_typevarset(PredInfo4, TVarSet, PredInfo5),
 		pred_info_arg_types(PredInfo5, _ArgTVarSet,
 				ExistQVars, ArgTypes),
@@ -2816,7 +2895,7 @@
 		map__det_update(Preds0, PredId, PredInfo, Preds),
 		predicate_table_set_preds(PredicateTable1, Preds,
 			PredicateTable),
-		module_info_set_predicate_table(ModuleInfo0, PredicateTable,
+		module_info_set_predicate_table(ModuleInfo1, PredicateTable,
 			ModuleInfo)
 		},
 		( { Status \= opt_imported } ->
@@ -4197,21 +4276,23 @@
 
 :- pred clauses_info_add_clause(clauses_info::in, pred_id::in, 
 		list(proc_id)::in, prog_varset::in, tvarset::in,
-		list(prog_term)::in, goal::in, prog_context::in,
+		list(prog_term)::in, goal::in, prog_context::in, bool::in,
 		hlds_goal::out, prog_varset::out, tvarset::out,
-		clauses_info::out, list(quant_warning)::out, qual_info::in,
+		clauses_info::out, list(quant_warning)::out, 
+		module_info::in, module_info::out, qual_info::in,
 		qual_info::out, io__state::di, io__state::uo) is det.
 
 clauses_info_add_clause(ClausesInfo0, PredId, ModeIds, CVarSet, TVarSet0,
-		Args, Body, Context, Goal, VarSet, TVarSet0,
-		ClausesInfo, Warnings, Info0, Info) -->
+		Args, Body, Context, IsAssertion, Goal, VarSet, TVarSet0,
+		ClausesInfo, Warnings, Module0, Module, Info0, Info) -->
 	{ ClausesInfo0 = clauses_info(VarSet0, VarTypes0, VarTypes1,
 					HeadVars, ClauseList0,
 					TI_VarMap, TCI_VarMap) },
 	{ update_qual_info(Info0, TVarSet0, VarTypes0, PredId, Info1) },
 	{ varset__merge_subst(VarSet0, CVarSet, VarSet1, Subst) },
-	transform(Subst, HeadVars, Args, Body, VarSet1, Context,
-				Goal, VarSet, Warnings, Info1, Info),
+	transform(Subst, HeadVars, Args, Body, VarSet1, Context, IsAssertion,
+				Goal, VarSet, Warnings, Module0, Module,
+				Info1, Info),
 		% XXX we should avoid append - this gives O(N*N)
 	{ list__append(ClauseList0, [clause(ModeIds, Goal, Context)],
 							ClauseList) },
@@ -4284,21 +4365,70 @@
 %-----------------------------------------------------------------------------
 
 :- pred transform(prog_substitution, list(prog_var), list(prog_term), goal,
-		prog_varset, prog_context, hlds_goal, prog_varset, 
-		list(quant_warning), qual_info, qual_info,
-		io__state, io__state).
-:- mode transform(in, in, in, in, in, in, out, out, out,
+		prog_varset, prog_context, bool, hlds_goal, prog_varset, 
+		list(quant_warning), module_info, module_info,
+		qual_info, qual_info, io__state, io__state).
+:- mode transform(in, in, in, in, in, in, in, out, out, out, in, out,
 			in, out, di, uo) is det.
 
-transform(Subst, HeadVars, Args0, Body, VarSet0, Context,
-		Goal, VarSet, Warnings, Info0, Info) -->
+transform(Subst, HeadVars, Args0, Body, VarSet0, Context, IsAssertion,
+		Goal, VarSet, Warnings, Module0, Module, Info0, Info) -->
 	transform_goal(Body, VarSet0, Subst, Goal1, VarSet1, Info0, Info1),
 	{ term__apply_substitution_to_list(Args0, Subst, Args) },
 	insert_arg_unifications(HeadVars, Args, Context, head, no,
 		Goal1, VarSet1, Goal2, VarSet2, Info1, Info),
 	{ map__init(Empty) },
+		
+		%
+		% Currently every variable in an assertion must be
+		% explicitly quantified, as it has not been determined
+		% what the correct implicit quantification should be for
+		% assertions.
+		%
+	(
+		{ IsAssertion = yes }
+	->
+			% Use Goal1, since HeadVar__* not yet
+			% introduced.
+		{ quantification__goal_vars(Goal1, Unquantified) },
+		{ set__to_sorted_list(Unquantified, ProblemVars0) },
+
+			% The Args are implicitly universally
+			% quantified.
+		{ term__term_list_to_var_list(Args, ArgVars) },
+		{ list__delete_elems(ProblemVars0, ArgVars, ProblemVars) },
+
+		{ list__length(ProblemVars, L) },
+		(
+			{ L > 0 }
+		->
+			prog_out__write_context(Context),
+			(
+				{ L = 1 }
+			->
+				io__write_string("Error: the variable `")
+			;
+				io__write_string("Error: the variables `")
+			),
+			io__write_list(ProblemVars, ",", write_var(VarSet)),
+			io__write_string("' were not explicitly quantified.\n"),
+			{ module_info_incr_errors(Module0, Module) }
+		;
+			{ Module = Module0 }
+		)
+
+	;
+		{ Module = Module0 }
+	),
 	{ implicitly_quantify_clause_body(HeadVars, Goal2, VarSet2, Empty,
 				Goal, VarSet, _, Warnings) }.
+
+	% Allow use of term_io__write_variable in io__write_list
+:- pred write_var(prog_varset::in, prog_var::in,
+		io__state::di, io__state::uo) is det.
+
+write_var(VarSet, Var) -->
+	term_io__write_variable(Var, VarSet).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/mercury_to_goedel.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mercury_to_goedel.m,v
retrieving revision 1.66
diff -u -r1.66 mercury_to_goedel.m
--- mercury_to_goedel.m	1998/11/20 04:08:20	1.66
+++ mercury_to_goedel.m	1999/07/08 00:30:59
@@ -200,7 +200,12 @@
 goedel_output_item(pragma(_Pragma), _Context) -->
 	io__stderr_stream(Stderr),
 	io__write_string(Stderr, 
-			"warning: C header declarations not allowed. Ignoring\n").
+			"warning: pragma declarations not allowed. Ignoring\n").
+
+goedel_output_item(assertion(_, _), _Context) -->
+	io__stderr_stream(Stderr),
+	io__write_string(Stderr, 
+			"warning: assertion declarations not allowed. Ignoring\n").
 
 goedel_output_item(nothing, _) --> [].
 goedel_output_item(typeclass(_, _, _, _, _), _) -->
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.158
diff -u -r1.158 mercury_to_mercury.m
--- mercury_to_mercury.m	1999/07/08 05:08:54	1.158
+++ mercury_to_mercury.m	1999/07/08 09:49:04
@@ -427,6 +427,13 @@
 			"check_termination")
 	).
 
+mercury_output_item(assertion(Goal, VarSet), _) -->
+	io__write_string(":- assertion "),
+	{ Indent = 1 },
+	mercury_output_newline(Indent),
+	mercury_output_goal(Goal, VarSet, Indent),
+	io__write_string(".\n").
+
 mercury_output_item(nothing, _) --> [].
 mercury_output_item(typeclass(Constraints, ClassName, Vars, Methods, 
 		VarSet), _) --> 
@@ -1758,13 +1765,29 @@
 mercury_output_goal_2(true, _, _) -->
 	io__write_string("true").
 
-	% Implication and equivalence should have been transformed out
-	% by now
-mercury_output_goal_2(implies(_G1,_G2), _VarSet, _Indent) -->
-	{ error("mercury_to_mercury: implies/2 in mercury_output_goal")}.
+mercury_output_goal_2(implies(G1,G2), VarSet, Indent) -->
+	{ Indent1 is Indent + 1 },
+	io__write_string("("),
+	mercury_output_newline(Indent1),
+	mercury_output_goal(G1, VarSet, Indent1),
+	mercury_output_newline(Indent),
+	io__write_string("=>"),
+	mercury_output_newline(Indent1),
+	mercury_output_goal(G2, VarSet, Indent1),
+	mercury_output_newline(Indent),
+	io__write_string(")").
 
-mercury_output_goal_2(equivalent(_G1,_G2), _VarSet, _Indent) -->
-	{ error("mercury_to_mercury: equivalent/2 in mercury_output_goal")}.
+mercury_output_goal_2(equivalent(G1,G2), VarSet, Indent) -->
+	{ Indent1 is Indent + 1 },
+	io__write_string("("),
+	mercury_output_newline(Indent1),
+	mercury_output_goal(G1, VarSet, Indent1),
+	mercury_output_newline(Indent),
+	io__write_string("<=>"),
+	mercury_output_newline(Indent1),
+	mercury_output_goal(G2, VarSet, Indent1),
+	mercury_output_newline(Indent),
+	io__write_string(")").
 
 mercury_output_goal_2(some(Vars, Goal), VarSet, Indent) -->
 	( { Vars = [] } ->
@@ -1904,7 +1927,8 @@
 		mercury_output_goal(Goal, VarSet, Indent1)
 	).
 
-:- pred mercury_output_par_conj(goal, prog_varset, int, io__state, io__state).
+:- pred mercury_output_par_conj(goal, prog_varset, int,
+		io__state, io__state).
 :- mode mercury_output_par_conj(in, in, in, di, uo) is det.
 
 mercury_output_par_conj(Goal, VarSet, Indent) -->
@@ -2805,6 +2829,7 @@
 mercury_unary_prefix_op("?-").
 mercury_unary_prefix_op("\\").
 mercury_unary_prefix_op("\\+").
+mercury_unary_prefix_op("assertion").
 mercury_unary_prefix_op("delete").
 mercury_unary_prefix_op("dynamic").
 mercury_unary_prefix_op("end_module").
Index: compiler/module_qual.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/module_qual.m,v
retrieving revision 1.44
diff -u -r1.44 module_qual.m
--- module_qual.m	1999/04/23 01:02:52	1.44
+++ module_qual.m	1999/06/30 07:01:35
@@ -144,6 +144,7 @@
 collect_mq_info_2(pred_mode(_,_,_,_,_), Info, Info).
 collect_mq_info_2(func_mode(_,_,_,_,_,_), Info, Info).
 collect_mq_info_2(pragma(_), Info, Info).
+collect_mq_info_2(assertion(_, _), Info, Info).
 collect_mq_info_2(nothing, Info, Info).
 collect_mq_info_2(typeclass(_, Name, Vars, _, _), Info0, Info) :-
 	add_typeclass_defn(Name, Vars, Info0, Info).
@@ -329,6 +330,8 @@
 						Info0, Info, yes) -->
 	{ mq_info_set_error_context(Info0, (pragma) - Context, Info1) },
 	qualify_pragma(Pragma0, Pragma, Info1, Info).
+module_qualify_item(assertion(G, V) - Context, assertion(G, V) - Context,
+						Info, Info, yes) --> [].
 module_qualify_item(nothing - Context, nothing - Context,
 						Info, Info, yes) --> [].
 module_qualify_item(typeclass(Constraints0, Name, Vars, Interface0, VarSet) -
Index: compiler/post_typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/post_typecheck.m,v
retrieving revision 1.7
diff -u -r1.7 post_typecheck.m
--- post_typecheck.m	1999/06/30 17:12:37	1.7
+++ post_typecheck.m	1999/07/08 07:24:34
@@ -50,6 +50,9 @@
 	% constraints, and if ReportErrors = yes, print appropriate
 	% warning/error messages.
 	% Also bind any unbound type variables to the type `void'.
+	% Note that when checking assertions we take the conservative
+	% approach of warning about unbound type variables.  There may
+	% be cases for which this doesn't make sense.
 	%
 :- pred post_typecheck__check_type_bindings(pred_id, pred_info, module_info,
 		bool, pred_info, int, io__state, io__state).
@@ -81,11 +84,19 @@
 		pred_info, pred_info, io__state, io__state).
 :- mode post_typecheck__finish_ill_typed_pred(in, in, in, out, di, uo) is det.
 
+	% Now that the assertion has finished being typechecked,
+	% remove it from further processing and store it in the
+	% assertion_table.
+:- pred post_typecheck__finish_assertion(module_info, pred_id,
+		module_info) is det.
+:- mode post_typecheck__finish_assertion(in, in, out) is det.
+
 %-----------------------------------------------------------------------------%
+
 :- implementation.
 
 :- import_module typecheck, clause_to_proc, mode_util, inst_match.
-:- import_module mercury_to_mercury, prog_out, hlds_out, type_util.
+:- import_module mercury_to_mercury, prog_out, hlds_data, hlds_out, type_util.
 :- import_module globals, options.
 
 :- import_module map, set, assoc_list, bool, std_util, term.
@@ -363,6 +374,13 @@
 		PredInfo0, PredInfo) -->
 	post_typecheck__propagate_types_into_modes(ModuleInfo, PredId,
 		PredInfo0, PredInfo).
+
+post_typecheck__finish_assertion(Module0, PredId, Module) :-
+	module_info_assertion_table(Module0, AssertionTable0),
+	assertion_table_add_assertion(PredId, AssertionTable0, AssertionTable),
+	module_info_set_assertion_table(Module0, AssertionTable, Module1),
+	module_info_remove_predid(Module1, PredId, Module).
+	
 
 	% 
 	% Ensure that all constructors occurring in predicate mode
Index: compiler/prog_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_data.m,v
retrieving revision 1.46
diff -u -r1.46 prog_data.m
--- prog_data.m	1999/07/08 05:08:55	1.46
+++ prog_data.m	1999/07/08 09:49:08
@@ -83,6 +83,8 @@
 
 	;	pragma(pragma_type)
 
+	;	assertion(goal, prog_varset)
+
 	;	typeclass(list(class_constraint), class_name, list(tvar),
 			class_interface, tvarset)
 		%	Constraints, ClassName, ClassParams, 
Index: compiler/prog_io.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_io.m,v
retrieving revision 1.181
diff -u -r1.181 prog_io.m
--- prog_io.m	1999/03/15 08:47:49	1.181
+++ prog_io.m	1999/07/08 07:02:35
@@ -1043,6 +1043,10 @@
 	parse_pragma(ModuleName, VarSet, Pragma, Result0),
 	check_no_attributes(Result0, Attributes, Result).
 
+process_decl(ModuleName, VarSet, "assertion", Assertion, Attributes, Result):-
+	parse_assertion(ModuleName, VarSet, Assertion, Result0),
+	check_no_attributes(Result0, Attributes, Result).
+
 process_decl(ModuleName, VarSet, "typeclass", Args, Attributes, Result):-
 	parse_typeclass(ModuleName, VarSet, Args, Result0),
 	check_no_attributes(Result0, Attributes, Result).
@@ -1093,6 +1097,17 @@
 attribute_description(constraints(univ, _), "type class constraint (`<=')").
 attribute_description(constraints(exist, _),
 	"existentially quantified type class constraint (`=>')").
+
+%-----------------------------------------------------------------------------%
+
+	% parse the assertion declaration. 
+:- pred parse_assertion(module_name, varset, list(term), maybe1(item)).
+:- mode parse_assertion(in, in, in, out) is semidet.
+
+parse_assertion(_ModuleName, VarSet, [AssertionTerm], Result) :-
+	varset__coerce(VarSet, ProgVarSet),
+	parse_goal(AssertionTerm, ProgVarSet, AssertGoal, AssertVarSet),
+	Result = ok(assertion(AssertGoal, AssertVarSet)).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/purity.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/purity.m,v
retrieving revision 1.15
diff -u -r1.15 purity.m
--- purity.m	1999/07/08 05:08:57	1.15
+++ purity.m	1999/07/08 09:49:11
@@ -135,7 +135,7 @@
 
 :- implementation.
 
-:- import_module make_hlds, hlds_data, hlds_pred, prog_io_util.
+:- import_module make_hlds, hlds_pred, prog_io_util.
 :- import_module type_util, mode_util, code_util, prog_data, unify_proc.
 :- import_module globals, options, mercury_to_mercury, hlds_out.
 :- import_module passes_aux, typecheck, module_qual, clause_to_proc.
@@ -290,7 +290,16 @@
 	{ predicate_table_set_preds(PredTable0, Preds, PredTable) },
 	{ module_info_set_predicate_table(ModuleInfo0, PredTable,
 					  ModuleInfo1) },
-	check_preds_purity_2(PredIds, FoundTypeError, ModuleInfo1, ModuleInfo,
+
+	(
+		{ pred_info_get_goal_type(PredInfo0, assertion) }
+	->
+		{ post_typecheck__finish_assertion(ModuleInfo1,
+				PredId, ModuleInfo2) }
+	;
+		{ ModuleInfo2 = ModuleInfo1 }
+	),
+	check_preds_purity_2(PredIds, FoundTypeError, ModuleInfo2, ModuleInfo,
 				  NumErrors1, NumErrors).
 
 	% Purity-check the code for single predicate, reporting any errors.
Index: compiler/typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/typecheck.m,v
retrieving revision 1.260
diff -u -r1.260 typecheck.m
--- typecheck.m	1999/07/08 08:15:18	1.260
+++ typecheck.m	1999/07/08 09:49:15
@@ -3885,7 +3885,8 @@
 %-----------------------------------------------------------------------------%
 
 	% write out the inferred `pred' or `func' declarations
-	% for a list of predicates.
+	% for a list of predicates.  Don't write out the inferred types
+	% for assertions.
 
 :- pred write_inference_messages(list(pred_id), module_info,
 				io__state, io__state).
@@ -3898,7 +3899,8 @@
 	(
 		{ check_marker(Markers, infer_type) },
 		{ module_info_predids(ModuleInfo, ValidPredIds) },
-		{ list__member(PredId, ValidPredIds) }
+		{ list__member(PredId, ValidPredIds) },
+		{ \+ pred_info_get_goal_type(PredInfo, assertion) }
 	->
 		write_inference_message(PredInfo)
 	;
Index: compiler/notes/compiler_design.html
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/notes/compiler_design.html,v
retrieving revision 1.26
diff -u -r1.26 compiler_design.html
--- compiler_design.html	1999/06/30 17:13:13	1.26
+++ compiler_design.html	1999/07/08 06:21:24
@@ -202,7 +202,8 @@
 
 	<dd>
 	quantification.m handles implicit quantification and computes
-	the set of non-local variables for each sub-goal
+	the set of non-local variables for each sub-goal.
+    This is done in transform in make_hlds.m
 
 <dt> checking typeclass instances (check_typeclass.m)
 	<dd>
Index: compiler/notes/glossary.html
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/notes/glossary.html,v
retrieving revision 1.2
diff -u -r1.2 glossary.html
--- glossary.html	1997/12/19 03:10:05	1.2
+++ glossary.html	1999/07/08 05:41:37
@@ -15,6 +15,11 @@
 
 <dl>
 
+<dt> assertion
+	<dd>
+    A declaration that specifies a law that holds for the
+    predicates/functions in the declaration.
+
 <dt> class context 
 	<dd>
 	The typeclass constraints on a predicate or function.
Index: doc/.ispell_words
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/.ispell_words,v
retrieving revision 1.1
diff -u -r1.1 .ispell_words
--- .ispell_words	1999/07/08 04:58:07	1.1
+++ .ispell_words	1999/07/08 08:45:40
@@ -65,6 +65,7 @@
 debuggable
 decl
 decls
+deconstruct
 deconstruction
 demangler
 Demoen
@@ -110,6 +111,7 @@
 fixpoint
 foldl
 foo
+fooable
 fpic
 fr
 fulljumps
@@ -211,6 +213,8 @@
 mindepth
 minimize
 MKINIT
+mkshowable
+mkuniv
 MLFLAGS
 MLLIBS
 MLOBJS
@@ -319,6 +323,7 @@
 rla
 rlo
 rm
+RTTI
 Sagonas
 samp
 Schachte
@@ -332,6 +337,7 @@
 settitle
 sh
 shar
+showable
 sicstus
 skel
 SLDNF
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/reference_manual.texi,v
retrieving revision 1.142
diff -u -r1.142 reference_manual.texi
--- reference_manual.texi	1999/07/08 08:48:05	1.142
+++ reference_manual.texi	1999/07/08 08:49:42
@@ -49,6 +49,7 @@
 @author Peter Schachte
 @author Simon Taylor
 @author Chris Speirs
+ at author Peter Ross
 @page
 @vskip 0pt plus 1filll
 Copyright @copyright{} 1995-1999 The University of Melbourne.
@@ -82,6 +83,8 @@
                       safely use destructive update to modify that value
 * Determinism::       Determinism declarations let you specify that a predicate
                       should never fail or should never succeed more than once
+* Assertions::        Assertion declarations allow you to declare laws
+                      that hold.
 * Equality preds::    User-defined types can have user-defined equality
                       predicates.
 * Higher-order::      Mercury supports higher-order predicates and functions,
@@ -349,6 +352,7 @@
 :- typeclass
 :- instance
 :- pragma
+:- assertion
 :- module
 :- interface
 :- implementation
@@ -2098,6 +2102,46 @@
 And there are a variety of other applications.
 
 @c XXX fix semantics for I/O + committed choice + mode inference 
+
+ at node Assertions
+ at chapter Assertions
+
+Mercury supports the declaration of laws that hold for predicates and
+functions.  
+These laws are only checked for type-correctness,
+it is the responsibility of the programmer to ensure overall correctness.
+The behaviour of programs with incorrect laws is undefined.
+
+A new law is introduced with the @samp{:- assertion} declaration.
+
+Here are some examples of @samp{:- assertion} declarations.
+The following example declares the function @samp{+} to be commutative.
+
+ at example
+:- assertion
+    all [A,B,R] (
+        R = A + B
+    <=>
+        R = B + A
+    ).
+ at end example
+
+Note that each variable in the declaration was explicitly quantified.
+The current Mercury compiler requires that each assertion begins with
+an @samp{all} quantification, and that every variable is explicitly
+quantified.
+
+Here is a more complicated declaration. It declares that @samp{append} is
+associative.
+
+ at example
+:- assertion
+    all [A,B,C,ABC] (
+        (some [AB] (append(A, B, AB), append(AB, C, ABC)))
+    <=>
+        (some [BC] (append(B, C, BC), append(A, BC, ABC)))
+    ).
+ at end example
 
 @node Equality preds
 @chapter User-defined equality predicates
Index: doc/transition_guide.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/transition_guide.texi,v
retrieving revision 1.27
diff -u -r1.27 transition_guide.texi
--- transition_guide.texi	1999/03/24 13:09:02	1.27
+++ transition_guide.texi	1999/07/08 05:48:19
@@ -146,6 +146,7 @@
 ~               fy              900
 all             fxy             950
 and             xfy             720
+assertion       fx              1199
 div             yfx             400
 else            xfy             1170
 end_module      fx              1199
Index: library/ops.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/library/ops.m,v
retrieving revision 1.23
diff -u -r1.23 ops.m
--- ops.m	1998/03/03 17:26:02	1.23
+++ ops.m	1999/06/30 07:41:26
@@ -167,6 +167,7 @@
 ops__op_table("^", after, xfy, 200).		% standard ISO Prolog
 ops__op_table("all", before, fxy, 950).		% Mercury/NU-Prolog extension
 ops__op_table("and", after, xfy, 720).		% NU-Prolog extension
+ops__op_table("assertion", before, fx, 1199).	% Mercury extension
 ops__op_table("div", after, yfx, 400).		% standard ISO Prolog
 ops__op_table("else", after, xfy, 1170).	% Mercury/NU-Prolog extension
 ops__op_table("end_module", before, fx, 1199).	% Mercury extension

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------