From: Markus Triska <triska@metalevel.at>
Date: Wed, 20 Apr 2022 18:41:11 +0000 (+0200)
Subject: ADDED: can_be(term, ...) and must_be(term, ...)
X-Git-Tag: v0.9.1~45^2
X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=eea83d9474c44cdb3ebf717d5fd894c23459b9d7;p=scryer-prolog.git

ADDED: can_be(term, ...) and must_be(term, ...)

This terminology is a bit harder to understand than that of the other
type checks.

Scryer Prolog comprises two individually consistent but incompatible
notions of terms, namely terms and rational trees (which are also
called "cyclic terms"). This leads to a confusion in terminology,
because cyclic terms are not terms in the former sense even though
they also contain the word "term" in their name.

This terminological confusion is not restricted to terms: We also find
it for example in the notion of lists. Lists are defined inductively:

    - The empty list (written as "" or [], called 'nil') is a list.
    - A term with principal functor '.'/2 is a list if its second argument
      is a list.

Note that a list may contain cyclic terms as elements, and still be
called a list. However, if we post:

    ?- Ls = [_|Ls].

then Ls is not a list, because it does not fit the inductive
definition. Still, it is sometimes referred to as a "cyclic list" or
"circular list", even though it is not a list. Even Prolog
implementors that aim for strict conformance to the Prolog ISO
standard and are deeply familiar with the standard use this
terminology when talking about such terms, see for example:

    https://github.com/ichiban/prolog/pull/198

Consequently, must_be(list, Ls) raises a *type error* in this case.

Terms are distinguished from cyclic terms completely analogously. This
leads to the counterintuitive consequence that *cyclic lists are not
terms*. The reason for this apparent contradiction in terminology is
the mutual incompatibility of different notions of terms. The notion
of "term" precludes rational trees, similar to the notion of "list"
which precludes cyclic lists.

We therefore introduce:

    * must_be(term, Term)
      - raises an instantiation error if Term contains variables (since
        it could still become a rational tree)
      - raises a type error if Term is a rational tree

    * can_be(term, Term)
      - raises a type error if Term is a rational tree

Note that using the notion of "cyclic term" and "acyclic term" in this
terminology would not be a good idea, because this confusion is
precisely what we want to eliminate: must_be(term, Term) should be
usable as a test that reliably determines whether Term can be treated
as a term with the logical properties we expect from terms.

This addresses #1428.
---

diff --git a/src/lib/error.pl b/src/lib/error.pl
index c5af6d7c..68d7d3ee 100644
--- a/src/lib/error.pl
+++ b/src/lib/error.pl
@@ -30,6 +30,7 @@
        - chars
        - integer
        - list
+       - term
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
 must_be(Type, Term) :-
@@ -58,6 +59,13 @@ must_be_(chars, Ls) :-
 must_be_(list, Term)    :- check_(error:ilist, list, Term).
 must_be_(type, Term)    :- check_(error:type, type, Term).
 must_be_(boolean, Term) :- check_(error:boolean, boolean, Term).
+must_be_(term, Term)    :-
+        (   \+ ground(Term) ->
+            instantiation_error(must_be/2)
+        ;   \+ acyclic_term(Term) ->
+            type_error(term, Term, must_be/2)
+        ;   true
+        ).
 
 % We cannot use maplist(must_be(character), Cs), because library(lists)
 % uses library(error), so importing it would create a cyclic dependency.
@@ -94,6 +102,7 @@ type(chars).
 type(list).
 type(var).
 type(boolean).
+type(term).
 
 /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
    can_be(Type, Term)
@@ -122,6 +131,11 @@ can_(character, T)  :- character(T).
 can_(chars, Ls)     :- '$is_partial_string'(Ls).
 can_(list, Term)    :- list_or_partial_list(Term).
 can_(boolean, Term) :- boolean(Term).
+can_(term, Term)    :-
+        (   acyclic_term(Term) ->
+            true
+        ;   type_error(term, Term, can_be/2)
+        ).
 
 list_or_partial_list(Ls) :-
         '$skip_max_list'(_, _, Ls, Rs),