[m-rev.] for review: parsing and pretty printing of promise ex declarations

[Lars Yencken]

Hi,

Since my last post, I've fixed the bug where assertions didn't output
universal quantification during pretty printing, updated the glossary and
todo list, and added a new file in compiler/notes called promise_ex.html.

Here's the relative diff:


diff -u compiler/mercury_to_mercury.m compiler/mercury_to_mercury.m
--- compiler/mercury_to_mercury.m	1 Feb 2002 01:17:40 -0000
+++ compiler/mercury_to_mercury.m	7 Feb 2002 04:00:44 -0000
@@ -613,17 +613,31 @@
 			"check_termination")
 	).
 
-mercury_output_item(_, promise(PromiseType, Goal, VarSet, UnivVars), _) -->
+mercury_output_item(_, promise(PromiseType, Goal0, VarSet, UnivVars), _) -->
 	{ Indent = 1 },
 	( { PromiseType = true } ->
-		io__write_string(":- promise ")
+			% for an assertion, we put back any universally
+			% quantified variables that were stripped off during
+			% parsing so that the clause will output correctly
+		io__write_string(":- promise "),
+		( { \+ UnivVars = [] } ->
+			{ Goal0 = _GoalExpr - Context },
+			{ Goal = all(UnivVars, Goal0) - Context }
+		;
+			{ Goal = Goal0 }
+		)
 	;
+			% a promise ex declaration has a slightly different
+			% standard formatting from an assertion; the universal
+			% quantification comes before the rest of the
+			% declaration
 		io__write_string(":- all ["),
 		{ AppendVarNum = no },
 		mercury_output_vars(UnivVars, VarSet, AppendVarNum),
 		io__write_string("]"),
 		mercury_output_newline(Indent),
-		prog_out__write_promise_type(PromiseType)
+		prog_out__write_promise_type(PromiseType),
+		{ Goal0 = Goal }
 	),
 	mercury_output_newline(Indent),
 	mercury_output_goal(Goal, VarSet, Indent),
diff -u compiler/prog_data.m compiler/prog_data.m
--- compiler/prog_data.m	1 Feb 2002 02:28:32 -0000
+++ compiler/prog_data.m	5 Feb 2002 23:36:52 -0000
@@ -91,12 +91,17 @@
 		% used for items that should be ignored (e.g.
 		% NU-Prolog `when' declarations, which are silently
 		% ignored for backwards compatibility).
-
+	
+	% indicates the type of information the compiler should get from the 
+	% declaration's clause
 :- type promise_type
-	--->	exclusive
-	;	exhaustive
-	;	exclusive_exhaustive
-	; 	(true).
+		% promise ex declarations
+	--->	exclusive		% each disjunct is mutually exclusive
+	;	exhaustive		% disjunction cannot fail
+	;	exclusive_exhaustive	% both of the above
+
+		% assertions
+	; 	true.			% promise expression is true
 
 :- type type_and_mode	
 	--->	type_only(type)
only in patch2:
--- compiler/notes/todo.html	2 May 2001 17:34:47 -0000	1.11
+++ compiler/notes/todo.html	6 Feb 2002 00:24:08 -0000
@@ -63,6 +63,23 @@
 
 <h2> determinism analysis </h2>
 
+<p>
+
+<ul>
+<li> add functionality for promise ex declarations:
+     <ul>
+     	<li> add error checking and type checking as for assertions
+	<li> include declaration information in the module_info
+	<li> take into account mutual exclusivity from promise_exclusive
+	     and promise_exclusive_exhaustive declarations during switch
+	     detection
+	<li> take into account exhaustiveness from promise_exhaustive and 
+	     promise_exclusive_exhaustive declarations during
+	     determinism analysis
+     </ul>
+</ul>
+     
+
 <h2> unique modes </h2>
 
 <ul>
only in patch2:
--- compiler/notes/glossary.html	9 Jan 2002 04:48:59 -0000	1.5
+++ compiler/notes/glossary.html	7 Feb 2002 02:18:34 -0000
@@ -15,10 +15,11 @@
 
 <dl>
 
-<dt> assertion/promise
+<dt> assertion
 	<dd>
-    A declaration that specifies a law that holds for the
-    predicates/functions in the declaration.
+	A particular form of promise which claims to the compiler 
+	that the expression given will always hold. If useful, the 
+	compiler may use this information to perform optimisations.
 
 <dt> class context 
 	<dd>
@@ -89,6 +90,22 @@
 	<dd>
 	the structure in HLDS which contains
 	information about a procedure.
+
+<dt> promise
+	<dd>
+    	A declaration that specifies a law that holds for the 
+	predicates/functions in the declaration. Thus, examples of promises
+	are assertions and promise ex declarations.  More generally, the term 
+	promise is often used for a declaration where extra information is 
+	given to the compiler which it cannot check itself, for example in
+	purity pragmas.
+
+<dt> promise ex
+	<dd>
+	A shorthand for promise_exclusive, promise_exhaustive, and
+	promise_exclusive_exhaustive declarations. These declarations 
+	are used to tell the compiler determinism properties of a 
+	disjunction.
 
 <dt> RTTI
 	<dd>

================================================================================
new file: compiler/notes/promise_ex.html
================================================================================

<html>
<head>
<title>
	Promise Ex Declarations
</title>
</head>

<body
	bgcolor="#ffffff"
	text="#000000"
>

<hr>
<!-------------------------->
<h1> Promise Ex Declarations</h1>

This document is a description of promise ex declarations,
which are currently unfinished and as such are undocumented 
in the reference manual.

<p>

<hr>
<!-------------------------->
<h2> Syntax </h2>

There are currently three promise ex declarations: promise_exclusive, 
promise_exhaustive, and promise_exclusive_exhaustive. They are used to 
denote determinism properties of a disjunction, and denote either exclusivity
exhaustiveness or both. The examples of each, given below, also show
the different ways that existential quantification can be handled.

<ul>
<li>	Mutual exclusivity:
	<pre>
	:- all [X, Y] promise_exclusive
		some [Z] ( 
			p(X, Y, Z) 
		; 
			q(X, Y, Z) 
		).
	</pre>
<li>	Exhaustiveness:
	<pre>
	:- all [X] promise_exhaustive 
		( 
			p(X, _) 
		; 
			q(X, _) 
		).  
	</pre>
<li>	Both together:
	<pre> 
	:- all [X] promise_exclusive_exhaustive  
		some [Y] ( 
			p(X, Y) 
		; 
			q(X, Y, Z)
		).
	</pre>
</ul>

All three declarations are restricted in the following ways:
<ol>
<li>	Any variable that occurs in more than one disjunct must be
	explicitly quantified.
<li>	Any variable occuring in only one disjunct is existentially quantified.
	This is similarly applicable when an underscore is used in place of a 
	variable.
</ol>
<p>

<hr>
<!--------------------------> 
<h2> Development </h2>

This tracks the use of promise ex declarations through the compiler, and
may be useful as a quick summary of the current state of development. Items
marked with an asterisk (*) are not yet implemented. Places where data 
structures etc. have been defined are in italics.

<ol>
<li>	the declarations enter the parse tree
	<ul>
	<li>	<i>the operators are defined</i> (library/ops.m)
	<li>	<i>the structure for promise ex declarations in the parse tree 
		is defined</i> (prog_data.m)
	<li>	they are parsed and entered into the parse tree (prog_io.m)
	</ul>
<li>	they may be pretty printed (mercury_to_mercury.m, prog_out.m).
<li> 	(*) they are error checked, and entered in to the HLDS as 
	dummy predicates
	<ul>
	<li>	<i>definition of promise ex table as part of HLDS </i> 
		(hlds_module.m)
	<li>	<i>operations on promise ex table</i> (hlds_data.m) 
	<li>	error checking (make_hlds.m)
	<li>	entering of declarations into the HLDS as dummy predicates 
		(make_hlds.m)
	</ul>
<li>	(*) go through typechecking as predicates; after typechecking they 
	are removed from processing as predicates and entered into the
	promise_ex_table of the HLDS
	<ul>
	<li>	<i>predicates for finishing promise ex declaration processing
		defined</i> (post_typecheck.m)
	<li>	post typechecking processing initiated for promise ex 
		declarations (purity.m)
	</ul>
<li>	(*) exclusivity information is used during switch detection, and 
	where it leads to a full switch being made, applicable exhaustiveness 
	information is also used (switch_detection.m)
<li>	(*) exhaustiveness information is used during determinism analysis
	(det_analysis.m)
</ol>

</body>
</html>
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------