1 % (c) 2019-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(kernel_lists,[ not_element_of_list_wf/3, element_of_list_wf/4]).
6
7 :- use_module(module_information,[module_info/2]).
8 :- module_info(group,kernel).
9 :- module_info(description,'This module provides operations for lists of B objects.').
10 % with possible repetitions, as, e.g., for set_extensions
11
12 :- use_module(kernel_objects,[not_equal_object_wf/3]).
13 :- use_module(error_manager).
14
15 not_element_of_list_wf(Element,List,WF) :- not_el_wf(List,Element,WF).
16
17 :- block not_el_wf(-,?,?).
18 not_el_wf([],_,_WF) :- !.
19 not_el_wf([H|T],X,WF) :- !,
20 not_equal_object_wf(H,X,WF),
21 not_el_wf(T,X,WF).
22 not_el_wf(Other,X,WF) :-
23 add_internal_error('Not a list: ',not_el_wf(Other,X,WF)),fail.
24
25 % Questions: does it make sense to call clpfd_interface:clpfd_not_inlist ?
26
27
28
29 % test code below with: i1=1 & j1:0..6 & mid1:0..7 & mid2 : {mid1/2, mid1}
30
31 :- use_module(kernel_mappings,[kernel_call/4,kernel_call_predicate_check_element_of_wf/4]).
32 :- use_module(clpfd_lists,[try_in_fd_value_list_check/4]).
33 :- use_module(preferences,[get_preference/2]).
34
35 element_of_list_wf(ElementVal,TypeOfElement,List,WF) :-
36 % temporary solution: use code from interpreter to evaluate set_extension:
37 kernel_call(b_interpreter:convert_list_of_expressions_into_set_wf(List,ValueSet,set(TypeOfElement),WF),
38 List,WF, set_extension(List)), % do we need real AST Expression ? List contains values
39 % temporary solution: use check_element_of_wf; to do: use custom version just for lists
40 kernel_call_predicate_check_element_of_wf(ElementVal,ValueSet,WF,unknown), %trace,
41 %print_term_summary(prop(ExValue,ElementVal,WF)),nl,
42 % TO DO: avoid calling check_element_of version when CLPFD complete check possible
43 (get_preference(use_clpfd_solver,false) -> true
44 ; get_fd_type_from_b_type(TypeOfElement,FDType),
45 try_in_fd_value_list_check(List,ElementVal,FDType,WF)
46 % TO DO: provide cleaner API for this
47 ),
48 tools_printing:print_term_summary(finished_element_of_list_wf(ElementVal,List)),nl.
49
50 get_fd_type_from_b_type(integer,T) :- !, T=integer.
51 get_fd_type_from_b_type(global(G),T) :- !, T=global(G).
52 get_fd_type_from_b_type(_,_). % otherwise type could be couple_left,...
53