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