diff: bug fix for type_to_term failure for `char'

Fergus Henderson fjh at cs.mu.OZ.AU
Thu Jan 22 18:11:50 AEDT 1998


Estimated hours taken: 0.25

Fix a bug reported by Mark Brown that caused type_to_term
to fail when used for values of type `character'.

library/mercury_builtin.m:
	Fix a bug in the hand-coded base_type_info for the
	"character" type -- it had the type name as "char", not
	"character"

tests/hard_coded/Mmakefile:
tests/hard_coded/ground_dd.m:
tests/hard_coded/ground_dd.exp:
	Regression test.

cvs diff  library/mercury_builtin.m tests/hard_coded/Mmakefile tests/hard_coded/ground_dd.exp tests/hard_coded/ground_dd.m
Index: library/mercury_builtin.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/mercury_builtin.m,v
retrieving revision 1.89
diff -u -r1.89 mercury_builtin.m
--- mercury_builtin.m	1998/01/06 07:04:09	1.89
+++ mercury_builtin.m	1998/01/22 07:04:51
@@ -551,7 +551,7 @@
 	(const Word *) & mercury_data___base_type_layout_character_0,
 	(const Word *) & mercury_data___base_type_functors_character_0,
 	(const Word *) string_const(""mercury_builtin"", 15),
-	(const Word *) string_const(""char"", 4)
+	(const Word *) string_const(""character"", 4)
 #endif
 };
 
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.9
diff -u -r1.9 Mmakefile
--- Mmakefile	1998/01/22 02:26:48	1.9
+++ Mmakefile	1998/01/22 07:07:25
@@ -33,6 +33,7 @@
 	func_and_pred \
 	func_test \
 	getopt_test \
+	ground_dd \
 	higher_order_func_test \
 	higher_order_syntax \
 	higher_order_type_manip \
Index: tests/hard_coded/ground_dd.exp
===================================================================
RCS file: ground_dd.exp
diff -N ground_dd.exp
--- /dev/null	Thu Jan 22 17:59:15 1998
+++ ground_dd.exp	Thu Jan 22 18:07:51 1998
@@ -0,0 +1,28 @@
+n_append([a, b, c], [d, e], [a, b, c, d, e])
+	n_append([b, c], [d, e], [b, c, d, e])
+		n_append([c], [d, e], [c, d, e])
+			n_append([], [d, e], [d, e])
+n_length([a, b, c, d, e], 5)
+	n_length([b, c, d, e], 4)
+		n_length([c, d, e], 3)
+			n_length([d, e], 2)
+				n_length([e], 1)
+					n_length([], 0)
+n_isort([4, 2, 5, 3, 1], [1, 2, 3, 4, 5])
+	n_isort([2, 5, 3, 1], [1, 2, 3, 5])
+		n_isort([5, 3, 1], [1, 3, 5])
+			n_isort([3, 1], [1, 3])
+				n_isort([1], [1])
+					n_isort([], [])
+					n_insert(1, [], [1])
+				n_insert(3, [1], [1, 3])
+					n_insert(3, [], [3])
+			n_insert(5, [1, 3], [1, 3, 5])
+				n_insert(5, [3], [3, 5])
+					n_insert(5, [], [5])
+		n_insert(2, [1, 3, 5], [1, 2, 3, 5])
+			n_insert(2, [3, 5], [2, 3, 5])
+	n_insert(4, [1, 2, 3, 5], [1, 2, 3, 4, 5])
+		n_insert(4, [2, 3, 5], [2, 3, 4, 5])
+			n_insert(4, [3, 5], [3, 4, 5])
+				n_insert(4, [5], [4, 5])
Index: tests/hard_coded/ground_dd.m
===================================================================
RCS file: ground_dd.m
diff -N ground_dd.m
--- /dev/null	Thu Jan 22 17:59:15 1998
+++ ground_dd.m	Thu Jan 22 18:07:18 1998
@@ -0,0 +1,161 @@
+%-----------------------------------------------------------------%
+%
+%  Proof tree generator
+%
+%	This is an example of the result of a program transformation
+%	that builds a proof tree at the	same time as calculating the
+%	correct results.
+%
+%	The proof tree uses the ground representation provided by
+%	term.m in the Mercury standard library.  This is the simplest
+%	way to achieve this in Mercury because it avoids dealing with
+%	issues such as writing an explicit type and instantiation for
+%	the proof tree.  Unfortunately,	this means that many of
+%	Mercury's advantages with strong typing are lost.
+%
+%  21 January, 1998
+%  Mark Brown
+
+:- module ground_dd.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+:- import_module int, list, term, term_io, varset.
+
+:- type proof 
+	--->	node(term, proof)
+%	;	leaf(pred(proof))	% implicit representation
+	;	new_types(proof)	% currently a NOP
+	;	conj(list(proof))
+	;	disj(int, proof)
+	;	if_then(proof, proof)
+	;	else(disproof, proof)
+	;	not(disproof)
+	;	assumed.
+
+
+:- type disproof
+	--->	failed.
+
+:- type node
+	--->	n_isort(list(int), list(int))
+	;	n_insert(int, list(int), list(int))
+	;	n_sum_list(list(int), int).
+:- type node(T)
+	--->	n_append(list(T), list(T), list(T))
+	;	n_length(list(T), int).
+:- type node(T, S)
+	--->	n_map(proc_id, list(T), list(S))
+	;	n_foldl(proc_id, list(T), S, S).
+
+
+:- type proc_id == string.
+
+
+:- pred append_w(list(T), list(T), list(T), proof).
+:- mode append_w(in, in, out, out) is det.
+:- mode append_w(out, out, in, out) is multi.
+
+append_w([], Bs, Bs, node(Node, assumed)) :-
+	type_to_term(n_append([], Bs, Bs), Node).
+append_w(A.As, Bs, A.Cs, node(Node, Proof)) :-
+	append_w(As, Bs, Cs, Proof),
+	type_to_term(n_append(A.As, Bs, A.Cs), Node).
+
+
+:- pred length_w(list(T), int, proof).
+:- mode length_w(in, out, out) is det.
+
+length_w([], 0, node(N, assumed)) :-
+	type_to_term(n_length([], 0), N).
+length_w(A.As, N+1, node(Node, Proof)) :-
+	length_w(As, N, Proof),
+	type_to_term(n_length(A.As, N+1), Node).
+
+
+:- pred isort_w(list(int), list(int), proof).
+:- mode isort_w(in, out, out) is det.
+
+isort_w([], [], node(Node, assumed)) :-
+	type_to_term(n_isort([], []), Node).
+isort_w(A.As, Ss, node(Node, conj([Proof_1, Proof_2]))) :-
+	isort_w(As, Ss0, Proof_1),
+	insert_w(A, Ss0, Ss, Proof_2),
+	type_to_term(n_isort(A.As, Ss), Node).
+
+
+:- pred insert_w(int, list(int), list(int), proof).
+:- mode insert_w(in, in, out, out) is det.
+
+insert_w(N, [], [N], node(Node, assumed)) :-
+	type_to_term(n_insert(N, [], [N]), Node).
+insert_w(N, A.As, Ss, node(Node, Proof)) :-
+	( N =< A ->
+		Ss = N.A.As,
+		Proof = if_then(assumed, assumed)
+	;
+		insert_w(N, As, Ss0, Proof_1),
+		Ss = A.Ss0,
+		Proof = else(failed, Proof_1)
+	),
+	type_to_term(n_insert(N, A.As, Ss), Node).
+	
+
+%------------------------------------------------------------
+
+:- pred write_proof(int, proof, io__state, io__state).
+:- mode write_proof(in, in, di, uo) is det.
+
+write_proof(L, node(N, P)) -->
+	indent(L),
+	{ varset__init(V) },
+	write_term(V, N),
+	nl,
+	write_proof(L+1, P).
+% write_proof(L, leaf(Closure)) -->
+%	{ Closure(P) },
+%	write_proof(L, P).
+write_proof(L, new_types(P)) -->
+	write_proof(L, P).
+write_proof(L, conj(Ps)) -->
+	foldl(write_proof(L), Ps).
+write_proof(L, disj(_, P)) -->
+	write_proof(L, P).
+write_proof(L, if_then(P_1, P_2)) -->
+	write_proof(L, P_1),
+	write_proof(L, P_2).
+write_proof(L, else(_, P_2)) -->
+	write_proof(L, P_2).
+write_proof(_, not(_)) -->
+	[].
+write_proof(_, assumed) -->
+	[].
+
+
+:- pred indent(int, io__state, io__state).
+:- mode indent(in, di, uo) is det.
+
+indent(L) -->
+	( { L > 0 } ->
+		write_char('\t'),
+		indent(L-1)
+	;
+		[]
+	).
+
+
+main -->
+	{ append_w([a,b,c], [d,e], As, P_1) },
+	write_proof(0, P_1),
+
+	{ length_w(As, _, P_2) },
+	write_proof(0, P_2),
+
+	{ isort_w([4,2,5,3,1], _, P_3) },
+	write_proof(0, P_3).
+

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.



More information about the developers mailing list