scryer-prolog/src/lib/si.pl at master · mthom/scryer-prolog · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140

/** Safe type tests.

   "si" stands for "sufficiently instantiated". It can also be read as
   "safe inference", so possibly also other predicates are candidates
   for this library.

   A safe type test:

    - throws an *instantiation error* if the argument is
      not sufficiently instantiated to make a sound decision
    - *succeeds* if the argument is of the specified type
    - *fails* otherwise.

   For instance, `atom_si(A)` yields an *instantiation error* if `A` is a
   variable. This is logically sound, since in that case the argument
   is not sufficiently instantiated to make any decision.

   The definitions are taken from [Safer type tests in Prolog](https://stackoverflow.com/questions/27306453/safer-type-tests-in-prolog).

   Examples:

```
?- chars_si(Cs).
   error(instantiation_error,list_si/1).
?- chars_si([h|Cs]).
   error(instantiation_error,list_si/1).
?- chars_si("hello").
   true.
?- chars_si(hello).
   false.
```
*/

:- module(si, [atom_si/1,
               integer_si/1,
               atomic_si/1,
               list_si/1,
               character_si/1,
               term_si/1,
               chars_si/1,
               dif_si/2,
               not_si/1,
               when_si/2]).

:- use_module(library(lists)).

atom_si(A) :-
   functor(A, _, 0),    % for the instantiation error
   atom(A).

integer_si(I) :-
   functor(I, _, 0),
   integer(I).

atomic_si(AC) :-
   functor(AC,_,0).

% list_si(L) :-
%    \+ \+ length(L, _),
%    sort(L, _).

list_si(L0) :-
   '$skip_max_list'(_,_, L0,L),
   (  nonvar(L) -> L = []
   ;  throw(error(instantiation_error, list_si/1))
   ).

character_si(Ch) :-
   functor(Ch,Ch,0),
   atom(Ch),
   atom_length(Ch,1).

term_si(Term) :-
   (   ground(Term) -> acyclic_term(Term)
   ;   throw(error(instantiation_error, term_si/1))
   ).

chars_si(Chs0) :-
   '$skip_max_list'(_,_, Chs0,Chs),
   ( nonvar(Chs) -> Chs == [] ; true ), % fails for infinite lists too
   failnochars(Chs0, Uninstantiated),
   (  nonvar(Uninstantiated)
   -> throw(error(instantiation_error, chars_si/1))
   ;  true
   ).

failnochars(Chs0, U) :-
   (  var(Chs0) -> U = true
   ;  Chs0 == [] -> true
   ;  Chs0 = [Ch|Chs1],
      (  nonvar(Ch) -> atom(Ch), atom_length(Ch,1)
      ;  U = true
      ),
      failnochars(Chs1, U)
   ).

dif_si(X, Y) :-
   X \== Y,
   ( X \= Y -> true
   ; throw(error(instantiation_error,dif_si/2))
   ).

%% not_si(+Goal).
%
%  True if Goal is not provable. Instantiation error if Goal is not
%  ground.

:- meta_predicate(not_si(0)).

not_si(Goal) :-
   term_si(Goal),
   \+ Goal.

:- meta_predicate(when_si(+, 0)).

%% when_si(Condition, Goal).
%
% Executes Goal when Condition becomes true. Throws an instantiation error if
% it can't decide.
when_si(Condition, Goal) :-
    % Taken from https://stackoverflow.com/a/40449516
    (   when_condition_si(Condition) ->
        (   Condition ->
            Goal
        ;   throw(error(instantiation_error,when_si/2))
        )
    ;   throw(error(domain_error(when_condition_si, Condition),_))
    ).

when_condition_si(Cond) :-
    var(Cond), !, throw(error(instantiation_error,when_condition_si/2)).
when_condition_si(ground(_)).
when_condition_si(nonvar(_)).
when_condition_si((A, B)) :-
    when_condition_si(A),
    when_condition_si(B).
when_condition_si((A ; B)) :-
    when_condition_si(A),
    when_condition_si(B).