begin work on between library
This commit is contained in:
Mark Thom
@@ -4,7 +4,6 @@
|
||||
'$add_to_list'/3, '$del_attr'/3, '$del_attr_step'/3,
|
||||
'$del_attr_buried'/4]).
|
||||
|
||||
:- use_module(library(control)).
|
||||
:- use_module(library(dcgs)).
|
||||
:- use_module(library(terms)).
|
||||
|
||||
|
||||
48
src/prolog/lib/between.pl
Normal file
48
src/prolog/lib/between.pl
Normal file
@@ -0,0 +1,48 @@
|
||||
:- module(between, [between/3, gen_int/1, gen_nat/1, numlist/2, repeat/1]).
|
||||
|
||||
%% TODO: numlist/3, numlist/5.
|
||||
|
||||
:- use_module(library(lists), [length/2]).
|
||||
|
||||
between(Lower, Upper, Lower) :-
|
||||
Lower =< Upper.
|
||||
between(Lower1, Upper, X) :-
|
||||
Lower1 < Upper,
|
||||
Lower2 is Lower1 + 1,
|
||||
between(Lower2, Upper, X).
|
||||
|
||||
enumerate_nats(I, I).
|
||||
enumerate_nats(I0, N) :-
|
||||
I1 is I0 + 1,
|
||||
enumerate_nats(I1, N).
|
||||
|
||||
gen_nat(N) :-
|
||||
integer(N), !, N >= 0.
|
||||
gen_nat(N) :-
|
||||
var(N), enumerate_nats(0, N).
|
||||
|
||||
enumerate_ints(I, I).
|
||||
enumerate_ints(I0, N) :-
|
||||
I0 > 0,
|
||||
N is -I0.
|
||||
enumerate_ints(I0, N) :-
|
||||
I1 is I0 + 1,
|
||||
enumerate_ints(I1, N).
|
||||
|
||||
gen_int(N) :-
|
||||
integer(N), !.
|
||||
gen_int(N) :-
|
||||
var(N), enumerate_ints(0, N).
|
||||
|
||||
repeat_integer(N) :-
|
||||
N > 0.
|
||||
repeat_integer(N0) :-
|
||||
N0 > 0, N1 is N0 - 1, repeat_integer(N1).
|
||||
|
||||
repeat(N) :-
|
||||
integer(N), N > 0, repeat_integer(N).
|
||||
|
||||
numlist(Upper, List) :-
|
||||
( integer(Upper) -> findall(X, between(1, Upper, X), List)
|
||||
; List = [_|_], length(List, Upper), findall(X, between(1, Upper, X), List)
|
||||
).
|
||||
@@ -1,13 +1,14 @@
|
||||
:- op(400, yfx, /).
|
||||
|
||||
:- module(builtins, [(=)/2, (+)/1, (+)/2, (**)/2, (*)/2, (-)/1, (-)/2,
|
||||
(/)/2, (/\)/2, (\/)/2, (is)/2, (xor)/2, (div)/2, (//)/2,
|
||||
(rdiv)/2, (<<)/2, (>>)/2, (mod)/2, (rem)/2, (>)/2, (<)/2,
|
||||
(=\=)/2, (=:=)/2, (-)/1, (>=)/2, (=<)/2, (,)/2, (->)/2, (;)/2,
|
||||
(=..)/2, (==)/2, (\==)/2, (@=<)/2, (@>=)/2, (@<)/2, (@>)/2,
|
||||
(=@=)/2, (\=@=)/2, (:)/2, bagof/3, call_with_inference_limit/3,
|
||||
catch/3, current_prolog_flag/2, expand_goal/2, expand_term/2,
|
||||
findall/3, findall/4, set_prolog_flag/2, setof/3, setup_call_cleanup/3,
|
||||
:- module(builtins, [(=)/2, (\=)/2, (\+)/1, (+)/1, (+)/2, (**)/2,
|
||||
(*)/2, (-)/1, (-)/2, (/)/2, (/\)/2, (\/)/2, (is)/2, (xor)/2,
|
||||
(div)/2, (//)/2, (rdiv)/2, (<<)/2, (>>)/2, (mod)/2, (rem)/2,
|
||||
(>)/2, (<)/2, (=\=)/2, (=:=)/2, (-)/1, (>=)/2, (=<)/2, (,)/2,
|
||||
(->)/2, (;)/2, (=..)/2, (==)/2, (\==)/2, (@=<)/2, (@>=)/2,
|
||||
(@<)/2, (@>)/2, (=@=)/2, (\=@=)/2, (:)/2, bagof/3,
|
||||
call_with_inference_limit/3, catch/3, current_prolog_flag/2,
|
||||
expand_goal/2, expand_term/2, findall/3, findall/4, once/1,
|
||||
repeat/0, set_prolog_flag/2, setof/3, setup_call_cleanup/3,
|
||||
term_variables/2, throw/1, true/0, false/0, write/1,
|
||||
write_canonical/1, writeq/1, write_term/2]).
|
||||
|
||||
@@ -44,7 +45,7 @@ expand_op_list([Op | OtherOps], Pred, Spec, [(:- op(Pred, Spec, Op)) | OtherResu
|
||||
:- op(1100, xfy, ;).
|
||||
|
||||
% control.
|
||||
:- op(700, xfx, [=, =..]).
|
||||
:- op(700, xfx, [=, =.., \=]).
|
||||
:- op(900, fy, \+).
|
||||
|
||||
% term comparison.
|
||||
@@ -116,6 +117,17 @@ set_prolog_flag(Flag, _) :-
|
||||
|
||||
% control operators.
|
||||
|
||||
\+ G :- G, !, false.
|
||||
\+ _.
|
||||
|
||||
X \= X :- !, false.
|
||||
_ \= _.
|
||||
|
||||
once(G) :- G, !.
|
||||
|
||||
repeat.
|
||||
repeat :- repeat.
|
||||
|
||||
','(G1, G2) :- '$get_b_value'(B), '$call_with_default_policy'(comma_errors(G1, G2, B)).
|
||||
|
||||
:- non_counted_backtracking comma_errors/3.
|
||||
@@ -154,9 +166,6 @@ G1 -> G2 :- '$get_b_value'(B), '$call_with_default_policy'(->(G1, G2, B)).
|
||||
|
||||
% univ.
|
||||
|
||||
\+ G :- G, !, false.
|
||||
\+ _.
|
||||
|
||||
:- non_counted_backtracking univ_errors/3.
|
||||
univ_errors(Term, List, N) :-
|
||||
'$skip_max_list'(N, -1, List, R),
|
||||
@@ -363,9 +372,8 @@ throw(Ball) :- '$set_ball'(Ball), '$unwind_stack'.
|
||||
|
||||
truncate_lh_to(LhLength) :- '$truncate_lh_to'(LhLength).
|
||||
|
||||
check_for_compat_list(L, PI) :-
|
||||
'$skip_max_list'(_, -1, L, R),
|
||||
( nonvar(R), R \== [], throw(error(type_error(list, L), PI))
|
||||
check_for_compat_list(L, PI) :-
|
||||
( nonvar(L), L \= [_|_], throw(error(type_error(list, L), PI))
|
||||
; true
|
||||
).
|
||||
|
||||
|
||||
@@ -1,24 +0,0 @@
|
||||
:- module(control, [(\=)/2, (\+)/1, between/3, call_cleanup/2, once/1, repeat/0]).
|
||||
|
||||
:- op(900, fy, \+).
|
||||
:- op(700, xfx, \=).
|
||||
|
||||
once(G) :- G, !.
|
||||
|
||||
\+ G :- G, !, false.
|
||||
\+ _.
|
||||
|
||||
X \= X :- !, false.
|
||||
_ \= _.
|
||||
|
||||
call_cleanup(G, C) :- setup_call_cleanup(true, G, C).
|
||||
|
||||
between(Lower, Upper, Lower) :-
|
||||
Lower =< Upper.
|
||||
between(Lower1, Upper, X) :-
|
||||
Lower1 < Upper,
|
||||
Lower2 is Lower1 + 1,
|
||||
between(Lower2, Upper, X).
|
||||
|
||||
repeat.
|
||||
repeat :- repeat.
|
||||
@@ -1,112 +0,0 @@
|
||||
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
|
||||
SICStus implementation of the Minato task.
|
||||
Written Sept. 2017 by Markus Triska (triska@metalevel.at)
|
||||
Public domain code.
|
||||
|
||||
For more information, please see:
|
||||
|
||||
https://www.metalevel.at/prolog/attributedvariables
|
||||
===================================================
|
||||
|
||||
A ZDD node is either:
|
||||
|
||||
-) a *leaf* of the form b(true) or b(false)
|
||||
-) an *inner node* of the form ( Var -> Then ; Else ).
|
||||
|
||||
In ZDDs, variables that are *not* encountered on a path to TRUE
|
||||
must be 0.
|
||||
|
||||
This module exports a single predicate:
|
||||
|
||||
* variables_set_zdd(Vs, ZDD)
|
||||
|
||||
It associates each variable in Vs with the given ZDD. For each
|
||||
variable, the ZDD is stored as an attribute zdd_vs(ZDD, Vs). This
|
||||
lets us reason about all variables that originally occurred.
|
||||
|
||||
The internal unification hooks must be implemented so that only
|
||||
admissible assignments of truth variables to variables succeed.
|
||||
|
||||
In particular, the Minato task:
|
||||
|
||||
?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ),
|
||||
Vs = [X,Y],
|
||||
variables_set_zdd(Vs, ZDD),
|
||||
Vs = [1,1].
|
||||
|
||||
no
|
||||
|
||||
Other examples:
|
||||
|
||||
?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ),
|
||||
Vs = [X,Y],
|
||||
variables_set_zdd(Vs, ZDD),
|
||||
X = 1.
|
||||
|
||||
X = 1,
|
||||
Y = 0,
|
||||
Vs = [1,0] ? ;
|
||||
|
||||
|
||||
?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ),
|
||||
Vs = [X,Y],
|
||||
variables_set_zdd(Vs, ZDD),
|
||||
X = 0.
|
||||
|
||||
X = 0,
|
||||
Vs = [0,Y] ? ;
|
||||
|
||||
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
|
||||
|
||||
:- module(zdd, [variables_set_zdd/2]).
|
||||
|
||||
:- use_module(library(atts)).
|
||||
:- use_module(library(dcgs)).
|
||||
:- use_module(library(lists)).
|
||||
|
||||
:- attribute zdd_vs/2.
|
||||
|
||||
variables_set_zdd(Vs, ZDD) :-
|
||||
maplist(set_zdd(ZDD, Vs), Vs).
|
||||
|
||||
set_zdd(ZDD, Vs, V) :-
|
||||
put_atts(V, +zdd_vs(ZDD, Vs)).
|
||||
|
||||
|
||||
verify_attributes(Var, Value, Goals) :-
|
||||
( get_atts(Var, +zdd_vs(ZDD0,Vs)) ->
|
||||
( integer(Value) ->
|
||||
zdd_restriction(ZDD0, Var, Value, ZDD)
|
||||
; throw(aliasing_not_implemented)
|
||||
),
|
||||
phrase(remaining_vars_0(ZDD, Var, Vs), Goals)
|
||||
; Goals = []
|
||||
).
|
||||
|
||||
remaining_vars_0(b(true), Var, Vs) --> all_others_0(Vs, Var).
|
||||
remaining_vars_0((_;_), _, _) --> [].
|
||||
|
||||
all_others_0([], _) --> [].
|
||||
all_others_0([V|Vs], Var) -->
|
||||
( { var(V), V \== Var } -> [V=0]
|
||||
; []
|
||||
),
|
||||
all_others_0(Vs, Var).
|
||||
|
||||
|
||||
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
|
||||
Compute the *restriction* of the ZDD.
|
||||
This means that Var has been instantiated to Value.
|
||||
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
|
||||
|
||||
zdd_restriction(b(T), _, _, b(T)).
|
||||
zdd_restriction(( Var0 -> Then0 ; Else0), Var, Value, ZDD) :-
|
||||
( Var0 == Var ->
|
||||
( Value =:= 0 -> ZDD = Else0
|
||||
; Value =:= 1 -> ZDD = Then0
|
||||
; throw(no_boolean)
|
||||
)
|
||||
; zdd_restriction(Then0, Var, Value, Then),
|
||||
zdd_restriction(Else0, Var, Value, Else),
|
||||
ZDD = ( Var0 -> Then ; Else )
|
||||
).
|
||||
Reference in New Issue
Block a user