[m-dev.] for review: add parsing/storing of assertions
Peter Ross
petdr at cs.mu.OZ.AU
Thu Jul 8 11:13:15 AEST 1999
Hi,
This is for DJ to review.
Pete.
===================================================================
Estimated hours taken: 40
Add the infrastructure for assertions into the compiler.
compiler/check_assertion.m:
Module that ensures that the form of an assertion is syntactically valid.
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_mercury.m:
Output assertions.
compiler/mercury_to_goedel.m:
compiler/module_qual.m:
Handle the assertion structure.
compiler/post_typecheck.m:
Add to comments about what happens when typechecking assertions.
compiler/prog_data.m:
Add assertion to the type goal_expr.
compiler/prog_io.m:
Call the parse_assertion for assertions.
compiler/prog_io_assertion.m:
Parse the assertions.
compiler/purity.m:
After finished typechecking assertions, remove the assertions from
further processing.
compiler/typecheck.m:
Don't output inference messages for assertions.
compiler/accumulator.m:
A minor code reordering.
Index: accumulator.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/accumulator.m,v
retrieving revision 1.3
diff -u -r1.3 accumulator.m
--- accumulator.m 1999/06/30 17:12:14 1.3
+++ accumulator.m 1999/07/05 07:09:17
@@ -1671,6 +1671,16 @@
mode_is_input(ModuleInfo, In),
mode_is_output(ModuleInfo, Out).
+assoc_fact(unqualified("list"), "append", 3, [TypeInfoIn, In, In, Out],
+ ModuleInfo, [TypeInfo, A, B, C],
+ [TypeInfo, B, A, C], PossibleStaticVars, yes) :-
+ set__list_to_set([A, B], PossibleStaticVars),
+ mode_is_input(ModuleInfo, TypeInfoIn),
+ mode_is_input(ModuleInfo, In),
+ mode_is_output(ModuleInfo, Out).
+
+
+
/* XXX introducing accumulators for floating point numbers can be bad.
assoc_fact(unqualified("float"), "+", 3, [In, In, Out], ModuleInfo,
[A, B, C], [A, B, C], PossibleStaticVars, no) :-
@@ -1684,15 +1694,6 @@
mode_is_input(ModuleInfo, In),
mode_is_output(ModuleInfo, Out).
*/
-
-assoc_fact(unqualified("list"), "append", 3, [TypeInfoIn, In, In, Out],
- ModuleInfo, [TypeInfo, A, B, C],
- [TypeInfo, B, A, C], PossibleStaticVars, yes) :-
- set__list_to_set([A, B], PossibleStaticVars),
- mode_is_input(ModuleInfo, TypeInfoIn),
- mode_is_input(ModuleInfo, In),
- mode_is_output(ModuleInfo, Out).
-
/*
XXX this no longer works, because set__insert isn't associative.
Index: check_assertion.m
===================================================================
RCS file: check_assertion.m
diff -N check_assertion.m
--- /dev/null Thu Jul 8 11:01:06 1999
+++ check_assertion.m Thu Jul 8 10:55:22 1999
@@ -0,0 +1,189 @@
+%-----------------------------------------------------------------------------%
+% Copyright (C) 1996-1999 The University of Melbourne.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%-----------------------------------------------------------------------------%
+%
+% File: check_assertion.m.
+% Main authors: petdr
+%
+% This module is responsible for ensuring that the form of the assertion
+% is valid.
+%
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- module check_assertion.
+
+:- interface.
+
+:- import_module hlds_module, prog_data.
+:- import_module list.
+
+:- pred check_assertion(goal::in, prog_varset::in, goal::out,
+ list(prog_term)::out, module_info::in, module_info::out,
+ io__state::di, io__state::uo) is det.
+
+:- implementation.
+
+:- import_module globals, options, prog_io_util, prog_out.
+:- import_module bool, io, set, std_util, term, term_io.
+
+ %
+ % check_assertion
+ %
+ % An assertion is valid, iff the assertion begins with the
+ % universally quantified variables and each variable is
+ % explicitly quantified before its use. At a later date these
+ % restrictions should be relaxed, once we work out how to
+ % correctly implicitly quantify the assertions.
+ %
+check_assertion(Goal, VarSet, NewGoal, HeadVars, Module0, Module) -->
+ (
+ { Goal = all(Vars, AllGoal) - _Context }
+ ->
+ { term__var_list_to_term_list(Vars, HeadVars) },
+ { NewGoal = AllGoal },
+ { set__list_to_set(Vars, InitialVarSet) },
+ check_assertion_quantification(AllGoal, InitialVarSet, VarSet,
+ Module0, Module)
+ ;
+ { HeadVars = [] },
+ { NewGoal = true - Context },
+ { Goal = _ - Context },
+ prog_out__write_context(Context),
+ io__write_string("Error: assertion doesn't begin with a universal quantifier\n"),
+ { module_info_incr_errors(Module0, Module) },
+ globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
+ ( { VerboseErrors = yes } ->
+ prog_out__write_context(Context),
+ io__write_string("Maybe you want all []\n")
+ ;
+ []
+ )
+ ).
+
+ % Make sure that each variable is explicitly quantified.
+:- pred check_assertion_quantification(goal::in, set(prog_var)::in,
+ prog_varset::in, module_info::in, module_info::out,
+ io__state::di, io__state::uo) is det.
+
+check_assertion_quantification(true - _, _, _, Module, Module) --> [].
+check_assertion_quantification(fail - _, _, _, Module, Module) --> [].
+check_assertion_quantification(unify(LHS, RHS) - Context, Quantified, VarSet,
+ Module0, Module) -->
+ { term__vars_list([LHS, RHS], Vars) },
+ check_assertion__atomic(Vars, Context, VarSet, Quantified,
+ Module0, Module).
+
+check_assertion_quantification(call(_, Args, _) - Context, Quantified, VarSet,
+ Module0, Module) -->
+ { term__vars_list(Args, Vars) },
+ check_assertion__atomic(Vars, Context, VarSet, Quantified,
+ Module0, Module).
+
+check_assertion_quantification((G1 , G2) - _, Quantified, VarSet,
+ Module0, Module) -->
+ check_assertion_quantification(G1, Quantified, VarSet,
+ Module0, Module1),
+ check_assertion_quantification(G2, Quantified, VarSet, Module1, Module).
+
+check_assertion_quantification((G1 & G2) - _, Quantified, VarSet,
+ Module0, Module) -->
+ check_assertion_quantification(G1, Quantified, VarSet,
+ Module0, Module1),
+ check_assertion_quantification(G2, Quantified, VarSet,
+ Module1, Module).
+
+check_assertion_quantification((G1 ; G2) - _, Quantified, VarSet,
+ Module0, Module) -->
+ check_assertion_quantification(G1, Quantified, VarSet,
+ Module0, Module1),
+ check_assertion_quantification(G2, Quantified, VarSet, Module1, Module).
+
+check_assertion_quantification(implies(G1, G2) - _, Quantified, VarSet,
+ Module0, Module) -->
+ check_assertion_quantification(G1, Quantified, VarSet,
+ Module0, Module1),
+ check_assertion_quantification(G2, Quantified, VarSet, Module1, Module).
+
+check_assertion_quantification(equivalent(G1, G2) - _, Quantified, VarSet,
+ Module0, Module) -->
+ check_assertion_quantification(G1, Quantified, VarSet,
+ Module0, Module1),
+ check_assertion_quantification(G2, Quantified, VarSet, Module1, Module).
+
+check_assertion_quantification(not(G) - _, Quantified, VarSet,
+ Module0, Module) -->
+ check_assertion_quantification(G, Quantified, VarSet, Module0, Module).
+
+check_assertion_quantification(if_then(Vars, G1, G2) - _, Quantified0,
+ VarSet, Module0, Module) -->
+ { set__insert_list(Quantified0, Vars, Quantified) },
+ check_assertion_quantification(G1, Quantified, VarSet,
+ Module0, Module1),
+ check_assertion_quantification(G2, Quantified, VarSet, Module1, Module).
+
+check_assertion_quantification(if_then_else(Vars, G1, G2, G3) - _, Quantified0,
+ VarSet, Module0, Module) -->
+ { set__insert_list(Quantified0, Vars, Quantified) },
+ check_assertion_quantification(G1, Quantified, VarSet,
+ Module0, Module1),
+ check_assertion_quantification(G2, Quantified, VarSet,
+ Module1, Module2),
+ check_assertion_quantification(G3, Quantified0, VarSet,
+ Module2, Module).
+
+check_assertion_quantification(some(Vars, G) - _, Quantified0, VarSet,
+ Module0, Module) -->
+ { set__insert_list(Quantified0, Vars, Quantified) },
+ check_assertion_quantification(G, Quantified, VarSet, Module0, Module).
+
+check_assertion_quantification(all(Vars, G) - _, Quantified0, VarSet,
+ Module0, Module) -->
+ { set__insert_list(Quantified0, Vars, Quantified) },
+ check_assertion_quantification(G, Quantified, VarSet, Module0, Module).
+
+
+
+ %
+ % check_assertion__atomic
+ %
+ % Ensure that for an atomic goal that all the variables have
+ % been quantified.
+ %
+:- pred check_assertion__atomic(prog_vars::in, prog_context::in,
+ prog_varset::in, set(prog_var)::in,
+ module_info::in, module_info::out,
+ io__state::di, io__state::uo) is det.
+
+check_assertion__atomic(GoalVars, Context, VarSet, Quantified,
+ Module0, Module) -->
+ { set__list_to_set(GoalVars, GoalVarsSet) },
+ { set__difference(GoalVarsSet, Quantified, Difference) },
+ (
+ { set__empty(Difference) }
+ ->
+ { Module = Module0 }
+ ;
+ { set__to_sorted_list(Difference, ProblemVars) },
+
+ prog_out__write_context(Context),
+ (
+ { list__length(ProblemVars, 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) }
+ ).
+
+ % 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: hlds_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_data.m,v
retrieving revision 1.34
diff -u -r1.34 hlds_data.m
--- hlds_data.m 1999/04/22 01:04:08 1.34
+++ hlds_data.m 1999/07/07 06:52:08
@@ -809,3 +809,60 @@
:- type superclass_table == multi_map(class_id, subclass_details).
%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- interface.
+
+:- import_module hlds_module.
+
+ %
+ % A table that records all the assertions in the system.
+ %
+:- 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_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).
+
+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_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).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
Index: 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 00:27:11
@@ -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: 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/07 07:59:25
@@ -299,6 +299,10 @@
->
io__write_string("type class method implementation")
;
+ { pred_info_get_goal_type(PredInfo, assertion) }
+ ->
+ io__write_string("the assertion")
+ ;
hlds_out__write_pred_or_func(PredOrFunc),
io__write_string(" `"),
prog_out__write_sym_name(Module),
Index: hlds_pred.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_pred.m,v
retrieving revision 1.59
diff -u -r1.59 hlds_pred.m
--- hlds_pred.m 1999/06/30 17:12:25 1.59
+++ hlds_pred.m 1999/07/07 15:37:21
@@ -179,6 +179,7 @@
:- type goal_type ---> pragmas % pragma c_code(...)
; clauses
+ ; { assertion }
; none.
% The evaluation method that should be used for a pred.
Index: make_hlds.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/make_hlds.m,v
retrieving revision 1.296
diff -u -r1.296 make_hlds.m
--- make_hlds.m 1999/06/30 17:12:27 1.296
+++ make_hlds.m 1999/07/08 00:30:29
@@ -62,6 +62,7 @@
:- 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.
@@ -219,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) } ->
@@ -513,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,12 +609,12 @@
Status, Context, Module0, Module, Info0, Info) -->
check_not_exported(Status, Context, "clause"),
module_add_func_clause(Module0, VarSet, PredName, Args, Result, Body,
- Status, Context, Module, Info0, Info).
+ Status, Context, no, 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"),
module_add_pred_clause(Module0, VarSet, PredName, Args, Body, Status,
- Context, Module, Info0, Info).
+ Context, no, Module, Info0, Info).
add_item_clause(type_defn(_, _, _), Status, Status, _,
Module, Module, Info, Info) --> [].
add_item_clause(inst_defn(_, _, _), Status, Status, _,
@@ -686,6 +690,18 @@
{ Module = Module0 },
{ Info = Info0 }
).
+add_item_clause(assertion(Goal0, VarSet),
+ Status, Status, Context, Module0, Module, Info0, Info) -->
+ check_assertion(Goal0, VarSet, Goal, HeadVars, Module0, Module1),
+
+ { 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,
+ Info0, Info).
+
add_item_clause(nothing, Status, Status, _, Module, Module, Info, Info) --> [].
add_item_clause(typeclass(_, _, _, _, _),
Status, Status, _, Module, Module, Info, Info) --> [].
@@ -2670,12 +2686,12 @@
:- 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, Assertion, ModuleInfo, Info0, Info) -->
% print out a progress message
globals__io_lookup_bool_option(very_verbose, VeryVerbose),
( { VeryVerbose = yes } ->
@@ -2687,16 +2703,16 @@
[]
),
module_add_clause(ModuleInfo0, ClauseVarSet, PredName, Args, Body,
- Status, Context, predicate, ModuleInfo, Info0, Info).
+ Status, Context, predicate, Assertion, 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, Assertion, ModuleInfo, Info0, Info) -->
% print out a progress message
globals__io_lookup_bool_option(very_verbose, VeryVerbose),
( { VeryVerbose = yes } ->
@@ -2709,16 +2725,17 @@
),
{ list__append(Args0, [Result], Args) },
module_add_clause(ModuleInfo0, ClauseVarSet, FuncName, Args, Body,
- Status, Context, function, ModuleInfo, Info0, Info).
+ Status, Context, function, Assertion, 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, Assertion, 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.)
@@ -2730,11 +2747,30 @@
PredOrFunc, PredName, Arity, [PredId0]) }
->
{ PredId = PredId0 },
- { PredicateTable1 = PredicateTable0 }
+ { PredicateTable1 = PredicateTable0 },
+ (
+ { Assertion = 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.
+ { Assertion = yes }
+ ;
+ { Assertion = no },
+ maybe_undefined_pred_error(PredName, Arity, PredOrFunc,
+ Context, "clause")
+ ),
{ preds_add_implicit(ModuleInfo0, PredicateTable0,
ModuleName, PredName, Arity, Status, Context,
PredOrFunc,
@@ -2786,7 +2822,13 @@
VarSet, TVarSet, Clauses, Warnings, Info0, Info),
{
pred_info_set_clauses_info(PredInfo2, Clauses, PredInfo3),
- pred_info_set_goal_type(PredInfo3, clauses, PredInfo4),
+ (
+ Assertion = 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),
@@ -2810,7 +2852,7 @@
module_info_set_predicate_table(ModuleInfo0, PredicateTable,
ModuleInfo)
},
- ( { Status \= opt_imported } ->
+ ( { Status \= opt_imported, Assertion = no } ->
% warn about singleton variables
maybe_warn_singletons(VarSet,
PredOrFunc - PredName/Arity, ModuleInfo, Goal),
@@ -5355,7 +5397,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),
Index: 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: mercury_to_mercury.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.157
diff -u -r1.157 mercury_to_mercury.m
--- mercury_to_mercury.m 1999/06/09 16:39:34 1.157
+++ mercury_to_mercury.m 1999/07/08 00:46:16
@@ -422,6 +422,14 @@
"check_termination")
).
+mercury_output_item(assertion(Goal, VarSet), _) -->
+ io__write_string(":- assertion "),
+ { Indent = 1 },
+ mercury_output_newline(Indent),
+ mercury_output_goal(Goal, VarSet, Indent, yes),
+ io__write_string("."),
+ io__nl.
+
mercury_output_item(nothing, _) --> [].
mercury_output_item(typeclass(Constraints, ClassName, Vars, Methods,
VarSet), _) -->
@@ -1703,7 +1711,7 @@
[]
;
io__write_string(" :-\n\t"),
- mercury_output_goal(Body, VarSet, 1)
+ mercury_output_goal(Body, VarSet, 1, no)
),
io__write_string(".\n").
@@ -1733,130 +1741,154 @@
;
mercury_output_term(Result, VarSet, no),
io__write_string(" :-\n\t"),
- mercury_output_goal(Body, VarSet, 1)
+ mercury_output_goal(Body, VarSet, 1, no)
),
io__write_string(".\n").
-:- pred mercury_output_goal(goal, prog_varset, int, io__state, io__state).
-:- mode mercury_output_goal(in, in, in, di, uo) is det.
+:- 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.
-mercury_output_goal(Goal - _Context, VarSet, Indent) -->
- mercury_output_goal_2(Goal, VarSet, Indent).
+mercury_output_goal(Goal - _Context, VarSet, Indent, InAssertion) -->
+ mercury_output_goal_2(Goal, VarSet, Indent, InAssertion).
-:- pred mercury_output_goal_2(goal_expr, prog_varset, int,
+:- pred mercury_output_goal_2(goal_expr, prog_varset, int, bool,
io__state, io__state).
-:- mode mercury_output_goal_2(in, in, in, di, uo) is det.
+:- mode mercury_output_goal_2(in, 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
-mercury_output_goal_2(implies(_G1,_G2), _VarSet, _Indent) -->
+ % 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) -->
+ { Indent1 is Indent + 1 },
+ io__write_string("("),
+ mercury_output_newline(Indent1),
+ mercury_output_goal(G1, VarSet, Indent1, yes),
+ mercury_output_newline(Indent),
+ io__write_string("=>"),
+ mercury_output_newline(Indent1),
+ mercury_output_goal(G2, VarSet, Indent1, yes),
+ mercury_output_newline(Indent),
+ io__write_string(")").
-mercury_output_goal_2(equivalent(_G1,_G2), _VarSet, _Indent) -->
+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) -->
+ { Indent1 is Indent + 1 },
+ io__write_string("("),
+ mercury_output_newline(Indent1),
+ mercury_output_goal(G1, VarSet, Indent1, yes),
+ mercury_output_newline(Indent),
+ io__write_string("<=>"),
+ mercury_output_newline(Indent1),
+ mercury_output_goal(G2, VarSet, Indent1, yes),
+ mercury_output_newline(Indent),
+ io__write_string(")").
-mercury_output_goal_2(some(Vars, Goal), VarSet, Indent) -->
+mercury_output_goal_2(some(Vars, Goal), VarSet, Indent, InAssertion) -->
( { Vars = [] } ->
- mercury_output_goal(Goal, VarSet, Indent)
+ mercury_output_goal(Goal, VarSet, Indent, InAssertion)
;
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),
+ mercury_output_goal(Goal, VarSet, Indent1, InAssertion),
mercury_output_newline(Indent),
io__write_string(")")
).
-mercury_output_goal_2(all(Vars, Goal), VarSet, Indent) -->
+mercury_output_goal_2(all(Vars, Goal), VarSet, Indent, InAssertion) -->
( { Vars = [] } ->
- mercury_output_goal(Goal, VarSet, Indent)
+ mercury_output_goal(Goal, VarSet, Indent, InAssertion)
;
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),
+ mercury_output_goal(Goal, VarSet, Indent1, InAssertion),
mercury_output_newline(Indent),
io__write_string(")")
).
-mercury_output_goal_2(if_then_else(Vars, A, B, C), VarSet, Indent) -->
+mercury_output_goal_2(if_then_else(Vars, A, B, C), VarSet, Indent,
+ InAssertion) -->
io__write_string("(if"),
mercury_output_some(Vars, VarSet),
{ Indent1 is Indent + 1 },
mercury_output_newline(Indent1),
- mercury_output_goal(A, VarSet, Indent1),
+ mercury_output_goal(A, VarSet, Indent1, InAssertion),
mercury_output_newline(Indent),
io__write_string("then"),
mercury_output_newline(Indent1),
- mercury_output_goal(B, VarSet, Indent1),
+ mercury_output_goal(B, VarSet, Indent1, InAssertion),
mercury_output_newline(Indent),
io__write_string("else"),
mercury_output_newline(Indent1),
- mercury_output_goal(C, VarSet, Indent1),
+ mercury_output_goal(C, VarSet, Indent1, InAssertion),
mercury_output_newline(Indent),
io__write_string(")").
-mercury_output_goal_2(if_then(Vars, A, B), VarSet, Indent) -->
+mercury_output_goal_2(if_then(Vars, A, B), VarSet, Indent, InAssertion) -->
io__write_string("(if"),
mercury_output_some(Vars, VarSet),
{ Indent1 is Indent + 1 },
mercury_output_newline(Indent1),
- mercury_output_goal(A, VarSet, Indent1),
+ mercury_output_goal(A, VarSet, Indent1, InAssertion),
mercury_output_newline(Indent),
io__write_string("then"),
mercury_output_newline(Indent1),
- mercury_output_goal(B, VarSet, Indent1),
+ mercury_output_goal(B, VarSet, Indent1, InAssertion),
mercury_output_newline(Indent),
io__write_string(")").
-mercury_output_goal_2(not(Goal), VarSet, Indent) -->
+mercury_output_goal_2(not(Goal), VarSet, Indent, InAssertion) -->
io__write_string("\\+ ("),
{ Indent1 is Indent + 1 },
mercury_output_newline(Indent1),
- mercury_output_goal(Goal, VarSet, Indent1),
+ mercury_output_goal(Goal, VarSet, Indent1, InAssertion),
mercury_output_newline(Indent),
io__write_string(")").
-mercury_output_goal_2((A,B), VarSet, Indent) -->
- mercury_output_goal(A, VarSet, Indent),
+mercury_output_goal_2((A,B), VarSet, Indent, InAssertion) -->
+ mercury_output_goal(A, VarSet, Indent, InAssertion),
io__write_string(","),
mercury_output_newline(Indent),
- mercury_output_goal(B, VarSet, Indent).
+ mercury_output_goal(B, VarSet, Indent, InAssertion).
-mercury_output_goal_2((A & B), VarSet, Indent) -->
+mercury_output_goal_2((A & B), VarSet, Indent, InAssertion) -->
io__write_string("("),
{ Indent1 is Indent + 1 },
mercury_output_newline(Indent1),
- mercury_output_goal(A, VarSet, Indent1),
- mercury_output_par_conj(B, VarSet, Indent),
+ mercury_output_goal(A, VarSet, Indent1, InAssertion),
+ mercury_output_par_conj(B, VarSet, Indent, InAssertion),
mercury_output_newline(Indent),
io__write_string(")").
-mercury_output_goal_2((A;B), VarSet, Indent) -->
+mercury_output_goal_2((A;B), VarSet, Indent, InAssertion) -->
io__write_string("("),
{ Indent1 is Indent + 1 },
mercury_output_newline(Indent1),
- mercury_output_goal(A, VarSet, Indent1),
- mercury_output_disj(B, VarSet, Indent),
+ mercury_output_goal(A, VarSet, Indent1, InAssertion),
+ mercury_output_disj(B, VarSet, Indent, InAssertion),
mercury_output_newline(Indent),
io__write_string(")").
-mercury_output_goal_2(call(Name, Term, Purity), VarSet, Indent) -->
+mercury_output_goal_2(call(Name, Term, Purity), VarSet, Indent,
+ _InAssertion) -->
write_purity_prefix(Purity),
mercury_output_call(Name, Term, VarSet, Indent).
-mercury_output_goal_2(unify(A, B), VarSet, _Indent) -->
+mercury_output_goal_2(unify(A, B), VarSet, _Indent, _InAssertion) -->
mercury_output_term(A, VarSet, no),
io__write_string(" = "),
mercury_output_term(B, VarSet, no, next_to_graphic_token).
@@ -1882,10 +1914,10 @@
Term, Context0), VarSet, no, next_to_graphic_token)
).
-:- pred mercury_output_disj(goal, prog_varset, int, io__state, io__state).
-:- mode mercury_output_disj(in, in, in, di, uo) is det.
+:- 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.
-mercury_output_disj(Goal, VarSet, Indent) -->
+mercury_output_disj(Goal, VarSet, Indent, InAssertion) -->
mercury_output_newline(Indent),
io__write_string(";"),
{ Indent1 is Indent + 1 },
@@ -1893,16 +1925,17 @@
(
{ Goal = (A;B) - _Context }
->
- mercury_output_goal(A, VarSet, Indent1),
- mercury_output_disj(B, VarSet, Indent)
+ mercury_output_goal(A, VarSet, Indent1, InAssertion),
+ mercury_output_disj(B, VarSet, Indent, InAssertion)
;
- mercury_output_goal(Goal, VarSet, Indent1)
+ mercury_output_goal(Goal, VarSet, Indent1, InAssertion)
).
-:- 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.
+:- pred mercury_output_par_conj(goal, prog_varset, int, bool,
+ io__state, io__state).
+:- mode mercury_output_par_conj(in, in, in, in, di, uo) is det.
-mercury_output_par_conj(Goal, VarSet, Indent) -->
+mercury_output_par_conj(Goal, VarSet, Indent, InAssertion) -->
mercury_output_newline(Indent),
io__write_string("&"),
{ Indent1 is Indent + 1 },
@@ -1910,10 +1943,10 @@
(
{ Goal = (A & B) - _Context }
->
- mercury_output_goal(A, VarSet, Indent1),
- mercury_output_par_conj(B, VarSet, Indent)
+ mercury_output_goal(A, VarSet, Indent1, InAssertion),
+ mercury_output_par_conj(B, VarSet, Indent, InAssertion)
;
- mercury_output_goal(Goal, VarSet, Indent1)
+ mercury_output_goal(Goal, VarSet, Indent1, InAssertion)
).
:- pred mercury_output_some(list(var(T)), varset(T), io__state, io__state).
@@ -2801,6 +2834,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: 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: 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/06 06:25:28
@@ -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).
Index: prog_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_data.m,v
retrieving revision 1.45
diff -u -r1.45 prog_data.m
--- prog_data.m 1999/04/23 01:02:58 1.45
+++ prog_data.m 1999/06/30 06:28:26
@@ -79,6 +79,8 @@
; pragma(pragma_type)
+ ; assertion(goal, prog_varset)
+
; typeclass(list(class_constraint), class_name, list(tvar),
class_interface, tvarset)
% Constraints, ClassName, ClassParams,
Index: 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/06/30 07:40:42
@@ -183,7 +183,7 @@
:- implementation.
:- import_module prog_io_goal, prog_io_dcg, prog_io_pragma, prog_io_util.
-:- import_module prog_io_typeclass.
+:- import_module prog_io_typeclass, prog_io_assertion.
:- import_module hlds_data, hlds_pred, prog_util, prog_out.
:- import_module globals, options, (inst).
:- import_module purity.
@@ -1041,6 +1041,10 @@
process_decl(ModuleName, VarSet, "pragma", Pragma, Attributes, Result):-
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):-
Index: prog_io_assertion.m
===================================================================
RCS file: prog_io_assertion.m
diff -N prog_io_assertion.m
--- /dev/null Thu Jul 8 11:01:06 1999
+++ prog_io_assertion.m Wed Jun 30 17:19:33 1999
@@ -0,0 +1,31 @@
+%-----------------------------------------------------------------------------%
+% Copyright (C) 1996-1999 The University of Melbourne.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%-----------------------------------------------------------------------------%
+%
+% File: prog_io_assertion.m.
+% Main authors: petdr
+%
+% This module handles the parsing of assertion directives.
+
+:- module prog_io_assertion.
+
+:- interface.
+
+:- import_module prog_data, prog_io_util.
+:- import_module list, varset, term.
+
+ % parse the assertion declaration.
+:- pred parse_assertion(module_name, varset, list(term), maybe1(item)).
+:- mode parse_assertion(in, in, in, out) is semidet.
+
+:- implementation.
+
+:- import_module prog_io, prog_io_goal.
+:- import_module term_util, term_errors.
+
+parse_assertion(_ModuleName, VarSet, [AssertionTerm], Result) :-
+ varset__coerce(VarSet, ProgVarSet),
+ parse_goal(AssertionTerm, ProgVarSet, AssertGoal, AssertVarSet),
+ Result = ok(assertion(AssertGoal, AssertVarSet)).
Index: purity.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/purity.m,v
retrieving revision 1.14
diff -u -r1.14 purity.m
--- purity.m 1999/06/30 17:12:38 1.14
+++ purity.m 1999/07/06 06:38:03
@@ -290,7 +290,15 @@
{ 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) }
+ ->
+ { module_info_remove_predid(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: typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/typecheck.m,v
retrieving revision 1.259
diff -u -r1.259 typecheck.m
--- typecheck.m 1999/06/30 17:12:42 1.259
+++ typecheck.m 1999/07/06 06:57:53
@@ -3829,7 +3829,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).
@@ -3842,7 +3843,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)
;
----
+----------------------------------------------------------------------+
| Peter Ross M Sci/Eng Melbourne Uni |
| petdr at cs.mu.oz.au WWW: www.cs.mu.oz.au/~petdr/ ph: +61 3 9344 9158 |
+----------------------------------------------------------------------+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the developers
mailing list