add_nr(Nr1,ToAdd,Nr2) :- number(Nr1),!, Nr2 is Nr1+ToAdd.
add_nr(minus(Expr,Nr1),ToAdd,Res) :- number(Nr1),!, Nr2 is Nr1-ToAdd,
(Nr2=0 -> Res=Expr ; Res= minus(Expr,Nr2)).
add_nr(add(Expr,Nr1),ToAdd,Res) :- number(Nr1),!, Nr2 is Nr1+ToAdd,
(Nr2=0 -> Res=Expr ; Res= add(Expr,Nr2)).
add_nr(add(Nr1,Expr),ToAdd,Res) :- number(Nr1),!, Nr2 is Nr1+ToAdd,
(Nr2=0 -> Res=Expr ; Res= add(Expr,Nr2)).
Calls:
Name: =/2 |
|
Name: ->/3 |
|
Name: is/2 |
|
Name: ! |
|
Name: number/1 |
Called:
Name: add_to_value_set/3 |
Module: well_def_prover |
add_to_value_set(interval(L,U),Nr,interval(L2,U2)) :-
add_nr(L,Nr,L2),
(add_nr(U,Nr,U2) -> true ; Nr =< 0, U2=U). % e.g., if U = size(x) we create an over-approximation
add_to_value_set('NATURAL',1,'NATURAL1'). % TO DO: extend
Calls:
Name: =/2 |
|
Name: =</2 |
|
Name: true |
|
Name: add_nr/3 |
Module: well_def_prover |
Name: ->/3 |
Called:
| Module: well_def_prover |
add_with_number(add(A,B),X,Nr) :- (number(A) -> Nr=A, X=B ; number(B) -> Nr=B, X=A).
add_with_number(minus(A,B),A,Nr) :- number(B), Nr is -B.
Calls:
Name: is/2 |
|
Name: number/1 |
|
Name: =/2 |
|
Name: ->/2 |
|
Name: ->/3 |
Called:
Name: check_leq/3 |
Module: well_def_prover |
Name: check_leq_nr/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: match_parameter/2 |
Module: well_def_prover |
Name: check_not_equal/3 |
Module: well_def_prover |
all_in_non_empty_sequence(interval(A,B),E,Hyps) :-
index_in_non_empty_sequence(A,E,Hyps),
index_in_non_empty_sequence(B,E,Hyps).
Calls:
| Module: well_def_prover |
Called:
| Module: well_def_prover |
avl_can_fetch(El,Res) :- number(El),!, Res=int(El).
avl_can_fetch(boolean_true,pred_true).
avl_can_fetch(boolean_false,pred_false).
avl_can_fetch(real(Atom),R) :- construct_real(Atom,R).
avl_can_fetch(string(S),string(S)) :- ground(S).
avl_can_fetch(couple(A,B),(VA,VB)) :- avl_can_fetch(A,VA), avl_can_fetch(B,VB).
Calls:
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
Name: ground/1 |
|
Name: construct_real/2 |
Module: kernel_reals |
Name: =/2 |
|
Name: ! |
|
Name: number/1 |
Called:
Name: check_member_of_set/4 |
Module: well_def_prover |
avl_fetch_binop_from_hyps(ID,BinOp,hyp_rec(AVL,HInfos),Value,hyp_rec(AVL,HInfos2)) :-
avl_fetch_bin(ID,BinOp,AVL,Value),
(avl_fetch(prevent_cycle_count,HInfos,CycleCount) % avoid cycles x=y, y=x
-> (CycleCount < 5 -> true ; % print(prevented_cycle(ID,CycleCount)),nl,
% in test 2018: :wd target = [2,1,1,2,1] & n=size(target) & i:1..n & target(i)=res requires cycle count < 5
!, fail),
C1 is CycleCount+1
; C1 is 1
),
avl_store(prevent_cycle_count,HInfos,C1,HInfos2).
Calls:
Name: avl_store/4 |
Module: foo_error |
Name: is/2 |
|
Name: fail |
|
Name: ! |
|
Name: true |
|
Name: </2 |
|
Name: ->/3 |
|
Name: avl_fetch/3 |
Module: foo_error |
Name: avl_fetch_bin/4 |
Module: avl_tools |
Called:
avl_fetch_binop_from_hyps_no_loop_check(ID,BinOp,hyp_rec(AVL,_),Value) :-
avl_fetch_bin(ID,BinOp,AVL,Value).
Calls:
Name: avl_fetch_bin/4 |
Module: avl_tools |
Called:
| Module: well_def_prover |
avl_fetch_equal_from_hyps(ID,Hyps,Value,Hyps2) :-
avl_fetch_binop_from_hyps(ID,equal,Hyps,Value,Hyps2).
Calls:
| Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: check_equal_h/6 |
Module: well_def_prover |
Name: check_not_empty_set/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_is_injective/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: get_explicit_value/3 |
Module: well_def_prover |
Name: check_finite/3 |
Module: well_def_prover |
Name: compute_card_of_set/4 |
Module: well_def_prover |
Name: hyp_repl/2 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_leq_nr/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover |
avl_fetch_from_hyps(Term,hyp_rec(AVL,_)) :- avl_fetch(Term,AVL).
Calls:
Name: avl_fetch/2 |
Module: foo_error |
Called:
Name: check_equal_h/6 |
Module: well_def_prover |
Name: check_empty_set/3 |
Module: well_def_prover |
Name: check_not_empty_set/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_finite/3 |
Module: well_def_prover |
Name: check_disjoint_aux/3 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
| Module: well_def_prover |
avl_fetch_mem_from_hyps(ID,Hyps,Value,Hyps2) :-
avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2).
Calls:
| Module: well_def_prover |
Called:
Name: check_member_of_union/5 |
Module: well_def_prover |
Name: get_type_from_hyps/4 |
Module: well_def_prover |
avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1) :-
get_type_from_hyps(Func,Hyps,Function,Hyps1).
avl_fetch_mem_or_struct(record_field(Rec,Field),Hyps,FieldType,Hyps2) :-
get_record_type_fields(Rec,Fields,Hyps,Hyps2),
(member(field(Field,FieldType),Fields) -> true).
Calls:
Name: true |
|
Name: member/2 |
|
Name: ->/2 |
|
Name: get_record_type_fields/4 |
Module: well_def_prover |
Name: get_type_from_hyps/4 |
Module: well_def_prover |
Called:
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: check_is_sequence/3 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Name: check_finite/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: compute_exact_range/4 |
Module: well_def_prover |
avl_fetch_not_equal(N1,N2,hyp_rec(AVL,_)) :-
(avl_fetch(not_equal(N1,N2),AVL) -> true
; avl_fetch(not_equal(N2,N1),AVL)). % we do not store both directions for not_equal
Calls:
Name: avl_fetch/2 |
Module: foo_error |
Name: true |
|
Name: ->/3 |
Called:
Name: check_not_equal/3 |
Module: well_def_prover |
Name: check_leq_nr/3 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
avl_fetch_worthwhile_equal_from_hyps(ID,Hyps,Value,Hyps2) :-
worth_rewriting_with_equal(ID),
avl_fetch_binop_from_hyps(ID,equal,Hyps,Value,Hyps2),
quick_not_occurs_check(ID,Value).
Calls:
Name: quick_not_occurs_check/2 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover |
Called:
Name: check_not_equal/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_member_of_range/4 |
Module: well_def_prover |
Name: check_subset_interval/5 |
Module: well_def_prover |
Name: check_subset_avl/3 |
Module: well_def_prover |
Name: check_disjoint_aux/3 |
Module: well_def_prover |
Name: check_is_sequence/3 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: compute_exact_range/4 |
Module: well_def_prover |
Name: compute_exact_domain/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: get_range_or_superset/4 |
Module: well_def_prover |
avl_fetch_worthwhile_mem_from_hyps(ID,Hyps,Value,Hyps2) :-
avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2),
\+ maximal_set(Value,Hyps).
Calls:
Name: maximal_set/2 |
Module: well_def_prover |
Name: not/1 |
|
| Module: well_def_prover |
Called:
| Module: well_def_prover | |
| Module: well_def_prover |
cdiv(N1,N2,Res) :-
(N1 mod N2 =:= 0 -> Res is N1//N2
; Res is (N1 div N2)+1).
Calls:
Name: is/2 |
|
Name: =:=/2 |
|
Name: ->/3 |
Called:
Name: check_leq_nr/3 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
check_all_finite(empty_set,_).
check_all_finite(empty_sequence,_).
check_all_finite(value(avl_set(_AVL)),_Hyp) :- % currently avl_set can only contain finite values for normalisation
true.
check_all_finite(intersection(A,B),Hyps) :-
(check_all_finite(A,Hyps) -> true ; check_all_finite(B,Hyps)).
check_all_finite(union(A,B),Hyps) :-
(check_all_finite(A,Hyps) -> check_all_finite(B,Hyps)).
check_all_finite(sorted_set_extension(L),Hyps) :- !, check_all_finite(set_extension(L),Hyps).
check_all_finite(set_extension(L),Hyps) :-
(member(Val,L), \+ check_finite(Val,Hyps,_) -> fail % CHECK
; true).
check_all_finite('$'(ID),Hyps) :-
(Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyp
avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2),
not_occurs(Set2,ID), % avoid silly, cyclic rewrites
rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3),
check_all_finite(Set2,Hyps3),!.
check_all_finite(Op,Hyps) :- pow_subset_operator(Op,Set),!,
% if Set is finite then all subsets of it are finite and there are only finitely many
check_finite(Set,Hyps,_PT).
check_all_finite(Op,Hyps) :- iseq_operator(Op,Set),!,
% if Set is finite then all injective sequences of it are finite and there are only finitely many
check_finite(Set,Hyps,_PT).
Calls:
Name: check_finite/3 |
Module: well_def_prover |
Name: ! |
|
Name: iseq_operator/2 |
Module: well_def_prover |
Name: pow_subset_operator/2 |
Module: well_def_prover |
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: not_occurs/2 |
Module: foo_error |
| Module: well_def_prover | |
Name: =/2 |
|
Name: true |
|
Name: fail |
|
Name: not/1 |
|
Name: member/2 |
|
Name: ->/3 |
|
Name: ->/2 |
Called:
Name: check_finite/3 |
Module: well_def_prover |
check_all_values_geq_val(intersection(A,B),Nr,Hyps) :-
(check_all_values_geq_val(A,Nr,Hyps) -> true ; check_all_values_geq_val(B,Nr,Hyps)).
check_all_values_geq_val(union(A,B),Nr,Hyps) :-
(check_all_values_geq_val(A,Nr,Hyps) -> check_all_values_geq_val(B,Nr,Hyps)).
check_all_values_geq_val(set_subtraction(A,_),Nr,Hyps) :-
check_all_values_geq_val(A,Nr,Hyps).
check_all_values_geq_val(interval(From,_),Nr,Hyps) :- check_leq(Nr,From,Hyps).
check_all_values_geq_val(value(avl_set(AVL)),Nr,Hyps) :- avl_min(AVL,int(Min)), check_leq(Nr,Min,Hyps).
check_all_values_geq_val('NATURAL',Nr,Hyps) :- check_leq(Nr,0,Hyps).
check_all_values_geq_val('NATURAL1',Nr,Hyps) :- check_leq(Nr,1,Hyps).
check_all_values_geq_val(domain(Func),Nr,Hyps) :-
get_domain_or_superset(Func,Hyps,DomFunc,Hyps2),
check_all_values_geq_val(DomFunc,Nr,Hyps2).
check_all_values_geq_val(range(Func),Nr,Hyps) :-
get_range_or_superset(Func,Hyps,RanFunc,Hyps2),
check_all_values_geq_val(RanFunc,Nr,Hyps2).
check_all_values_geq_val(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_geq_val(set_extension(L),Nr,Hyps).
check_all_values_geq_val(set_extension(L),Nr,Hyps) :-
(member(Val,L), \+ check_leq(Nr,Val,Hyps) -> fail ; true).
check_all_values_geq_val('$'(X),Nr,Hyps) :-
avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
rewrite_local_loop_check(X,check_all_values_geq_val,Y,Hyps2,Hyps3),
check_all_values_geq_val(Y,Nr,Hyps3).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: true |
|
Name: fail |
|
Name: check_leq/3 |
Module: well_def_prover |
Name: not/1 |
|
Name: member/2 |
|
Name: ->/3 |
|
Name: ! |
|
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Name: avl_min/2 |
Module: foo_error |
Name: ->/2 |
Called:
Name: check_leq/3 |
Module: well_def_prover |
check_all_values_leq_val(intersection(A,B),Nr,Hyps) :-
(check_all_values_leq_val(A,Nr,Hyps) -> true ; check_all_values_leq_val(B,Nr,Hyps)).
check_all_values_leq_val(union(A,B),Nr,Hyps) :-
(check_all_values_leq_val(A,Nr,Hyps) -> check_all_values_leq_val(B,Nr,Hyps)).
check_all_values_leq_val(set_subtraction(A,_),Nr,Hyps) :-
check_all_values_leq_val(A,Nr,Hyps).
check_all_values_leq_val(interval(_,To),Nr,Hyps) :- check_leq(To,Nr,Hyps).
check_all_values_leq_val(value(avl_set(AVL)),Nr,Hyps) :- avl_max(AVL,int(Max)), check_leq(Max,Nr,Hyps).
check_all_values_leq_val(domain(Func),Nr,Hyps) :-
get_domain_or_superset(Func,Hyps,DomFunc,Hyps2),
check_all_values_leq_val(DomFunc,Nr,Hyps2).
check_all_values_leq_val(range(Func),Nr,Hyps) :-
get_range_or_superset(Func,Hyps,RanFunc,Hyps2),
check_all_values_leq_val(RanFunc,Nr,Hyps2).
check_all_values_leq_val(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_leq_val(set_extension(L),Nr,Hyps).
check_all_values_leq_val(set_extension(L),Nr,Hyps) :-
(member(Val,L), \+ check_leq(Val,Nr,Hyps) -> fail ; true).
check_all_values_leq_val('$'(X),Nr,Hyps) :-
avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
rewrite_local_loop_check(X,check_all_values_leq_val,Y,Hyps2,Hyps3),
check_all_values_leq_val(Y,Nr,Hyps3).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: true |
|
Name: fail |
|
Name: check_leq/3 |
Module: well_def_prover |
Name: not/1 |
|
Name: member/2 |
|
Name: ->/3 |
|
Name: ! |
|
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Name: avl_max/2 |
Module: foo_error |
Name: ->/2 |
Called:
Name: check_leq/3 |
Module: well_def_prover |
check_all_values_neq_nr(intersection(A,B),Nr,Hyps) :-
(check_all_values_neq_nr(A,Nr,Hyps) -> true ; check_all_values_neq_nr(B,Nr,Hyps)).
check_all_values_neq_nr(union(A,B),Nr,Hyps) :-
(check_all_values_neq_nr(A,Nr,Hyps) -> check_all_values_neq_nr(B,Nr,Hyps)).
check_all_values_neq_nr(set_subtraction(A,_),Nr,Hyps) :-
check_all_values_neq_nr(A,Nr,Hyps).
check_all_values_neq_nr(interval(From,_),Nr,Hyps) :- number(From),F1 is From-1, check_leq(Nr,F1,Hyps).
check_all_values_neq_nr(interval(_,To),Nr,Hyps) :- number(To),T1 is To+1, check_leq(T1,Nr,Hyps).
check_all_values_neq_nr('NATURAL',Nr,Hyps) :- check_leq(Nr,-1,Hyps).
check_all_values_neq_nr('NATURAL1',Nr,Hyps) :- check_leq(Nr,0,Hyps).
check_all_values_neq_nr(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_neq_nr(set_extension(L),Nr,Hyps).
check_all_values_neq_nr(set_extension(L),Nr,Hyps) :-
(member(Val,L), \+ check_not_equal(Val,Nr,Hyps) -> fail ; true).
check_all_values_neq_nr('$'(X),Nr,Hyps) :-
avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
rewrite_local_loop_check(X,check_all_values_neq_nr,Y,Hyps2,Hyps3),
check_all_values_neq_nr(Y,Nr,Hyps3).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: true |
|
Name: fail |
|
Name: check_not_equal/3 |
Module: well_def_prover |
Name: not/1 |
|
Name: member/2 |
|
Name: ->/3 |
|
Name: ! |
|
Name: check_leq/3 |
Module: well_def_prover |
Name: is/2 |
|
Name: number/1 |
|
Name: ->/2 |
Called:
Name: check_not_equal/3 |
Module: well_def_prover |
check_disjoint(A,B,Hyps) :- %print(disj(A,B)),nl, portray_hyps(Hyps),nl,
(check_disjoint_aux(A,B,Hyps) -> true ; check_disjoint_aux(B,A,Hyps)).
Calls:
Name: check_disjoint_aux/3 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
Called:
Name: check_domain_disjoint/4 |
Module: well_def_prover |
Name: check_empty_set/3 |
Module: well_def_prover |
Name: check_disjoint_aux/3 |
Module: well_def_prover |
check_disjoint_aux(S,_,Hyps) :- check_equal_empty_set(S,Hyps,_),!.
check_disjoint_aux(A,B,Hyps) :-
avl_fetch_from_hyps(equal(intersection(A,B),empty_set),Hyps),!.
check_disjoint_aux(domain_subtraction(A,_),B,Hyps) :- !, % A <<| f /\ B = {} if dom(B) <: A
get_domain_or_superset(B,Hyps,DomB,Hyps2),
check_is_subset(DomB,A,Hyps2,_).
check_disjoint_aux(set_subtraction(AA,A),B,Hyps) :- !,
(check_is_subset(B,A,Hyps,_) -> true % x \ A /\ B = {} if B <: A
; check_disjoint(AA,B,Hyps) -> true). % AA-A /\ B ={} if AA /\ B = {}
check_disjoint_aux(set_extension(As),B,Hyps) :- !, l_check_not_member_of_set(As,B,Hyps).
check_disjoint_aux(sorted_set_extension(As),B,Hyps) :- !, l_check_not_member_of_set(As,B,Hyps).
check_disjoint_aux(A,B,Hyps) :-
avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A1,Hyps1),
check_disjoint(A1,B,Hyps1).
Calls:
Name: check_disjoint/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ! |
|
Name: true |
|
Name: ->/2 |
|
Name: check_is_subset/4 |
Module: well_def_prover |
Name: ->/3 |
|
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Name: avl_fetch_from_hyps/2 |
Module: well_def_prover |
Name: check_equal_empty_set/3 |
Module: well_def_prover |
Called:
Name: check_disjoint/3 |
Module: well_def_prover |
check_domain_disjoint(F1,F2,Hyps,Hyps2) :-
compute_exact_domain(F1,Hyps,DF1,Hyps2),
% example: :prove f:BOOL +-> BOOL & x /: dom(f) => f \/ {x|->TRUE} : BOOL +-> BOOL
is_set_extension(DF1,List1),!,
l_check_not_member_of_set(List1,domain(F2),Hyps2). % we could try and compute domain(F2) first
check_domain_disjoint(F2,F1,Hyps,Hyps2) :-
compute_exact_domain(F1,Hyps,DF1,Hyps2),
is_set_extension(DF1,List1),!,
l_check_not_member_of_set(List1,domain(F2),Hyps2).
check_domain_disjoint(F1,F2,Hyps,Hyps2) :-
get_domain_or_superset(F1,Hyps,DomFunc1,Hyps1),
get_domain_or_superset(F2,Hyps1,DomFunc2,Hyps2),
check_disjoint(DomFunc1,DomFunc2,Hyps2).
Calls:
Name: check_disjoint/3 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: ! |
|
Name: is_set_extension/2 |
Module: well_def_prover |
Name: compute_exact_domain/4 |
Module: well_def_prover |
Called:
| Module: well_def_prover |
check_empty_set(Set,_,empty_set) :- is_empty_set_direct(Set),!.
check_empty_set(A,Hyps,hyp) :- avl_fetch_from_hyps(equal(A,empty_set),Hyps),!.
check_empty_set(set_subtraction(A,B),Hyp,subset(PT)) :- !, % see SIMP_SETMINUS_EQUAL_EMPTY Rodin proof rule
check_is_subset(A,B,Hyp,PT).
check_empty_set(intersection(A,B),Hyps,inter_disjoint) :- !,
check_disjoint(A,B,Hyps).
check_empty_set(union(A,B),Hyps,union_empty(P1,P2)) :- !, % SIMP_BUNION_EQUAL_EMPTY
check_equal_empty_set(A,Hyps,P1),!,
check_equal_empty_set(B,Hyps,P2).
check_empty_set(cartesian_product(A,B),Hyps,cart_empty(PT)) :- !, % SIMP_CPROD_EQUAL_EMPTY
(check_equal_empty_set(A,Hyps,PT) -> true ; check_equal_empty_set(B,Hyps,PT)).
check_empty_set(pow1_subset(A),Hyps,pow1_empty(PT)) :- !, % SIMP_POW1_EQUAL_EMPTY
check_equal_empty_set(A,Hyps,PT).
check_empty_set(interval(From,To),Hyps,interval_empty) :- !, % SIMP_UPTO_EQUAL_EMPTY
check_less(To,From,Hyps).
check_empty_set(domain(A),Hyps,domain_empty(PT)) :- !, % SIMP_DOM_EQUAL_EMPTY
check_equal_empty_set(A,Hyps,PT).
check_empty_set(range(A),Hyps,range_empty(PT)) :- !, % SIMP_RAN_EQUAL_EMPTY
check_equal_empty_set(A,Hyps,PT).
check_empty_set(reverse(A),Hyps,reverse_empty(PT)) :- !, % SIMP_CONVERSE_EQUAL_EMPTY (relational inverse)
check_equal_empty_set(A,Hyps,PT).
check_empty_set(domain(A),Hyps,domain_empty(PT)) :- !, % SIMP_DOM_EQUAL_EMPTY
check_equal_empty_set(A,Hyps,PT).
check_empty_set(total_relation(A,B),Hyp,trel_empty(PTA,PTB)) :- !, % SIMP_SPECIAL_EQUAL_RELDOM
check_not_equal_empty_set(A,Hyp,PTA), check_equal_empty_set(B,Hyp,PTB).
check_empty_set(total_function(A,B),Hyp,tfun_empty(PTA,PTB)) :- !, % SIMP_SPECIAL_EQUAL_RELDOM
check_not_equal_empty_set(A,Hyp,PTA), check_equal_empty_set(B,Hyp,PTB).
check_empty_set(A,Hyps,subset_strict_singleton) :-
avl_fetch_binop_from_hyps(A,subset_strict,Hyps,B,_), % A <<: {Single} => A={}
singleton_set(B,_).
Calls:
Name: singleton_set/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_equal_empty_set/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: ! |
|
Name: check_less/3 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: check_disjoint/3 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
Name: avl_fetch_from_hyps/2 |
Module: well_def_prover |
Name: is_empty_set_direct/1 |
Module: well_def_prover |
Called:
Name: check_equal_h/6 |
Module: well_def_prover |
check_equal(A,Target,Hyps,Hyps1) :-
check_equal_h(A,Target,ground,[],Hyps,Hyps1).
Calls:
Name: check_equal_h/6 |
Module: well_def_prover |
Called:
Name: check_member_of_set/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_not_empty_set/2 |
Module: well_def_prover |
Name: check_equal_empty_set/3 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
Name: prove_po/3 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_member_of_range/4 |
Module: well_def_prover |
check_equal_empty_set(Set,Hyps,PT) :-
check_equal(Set,empty_set,Hyps,PT). % will also call this below:
Calls:
Name: check_equal/4 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: check_is_subset/4 |
Module: well_def_prover |
Name: maximal_set/2 |
Module: well_def_prover |
Name: check_finite/3 |
Module: well_def_prover |
Name: check_is_subset_strict/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_empty_set/3 |
Module: well_def_prover |
Name: check_disjoint_aux/3 |
Module: well_def_prover |
Name: check_not_empty_set/2 |
Module: well_def_prover |
| Module: well_def_prover |
check_equal_h(A,Target,_,_,Hyps,Hyps1) :- A=Target,!, Hyps1=Hyps.
check_equal_h(union(A1,A2),union(B1,B2),TGr,History,Hyps,Hyps2) :-
check_equal_h(A1,B1,TGr,History,Hyps,Hyps1),!, % TO DO: add other rules, e.g., check A1 and B2
check_equal_h(A2,B2,TGr,History,Hyps1,Hyps2).
check_equal_h(couple(A1,A2),couple(B1,B2),TGr,History,Hyps,Hyps2) :- % TO DO: records, ...
check_equal_h(A1,B1,TGr,History,Hyps,Hyps1),!,
check_equal_h(A2,B2,TGr,History,Hyps1,Hyps2).
check_equal_h(A,Target,TGr,History,Hyps,Hyps2) :-
avl_fetch_equal_from_hyps(A,Hyps,A2,Hyps1), nonmember(A2,History),
check_equal_h(A2,Target,TGr,[A|History],Hyps1,Hyps2).
check_equal_h(A,Target,TGr,History,Hyps,Hyps2) :- Target = '$'(_),
avl_fetch_equal_from_hyps(Target,Hyps,T2,Hyps1), nonmember(T2,History),
check_equal_h(A,T2,TGr,[A|History],Hyps1,Hyps2).
check_equal_h(A,Target,ground,_,Hyps,Hyps) :-
avl_fetch_from_hyps(subset(A,Target),Hyps),
avl_fetch_from_hyps(subset(Target,A),Hyps).
check_equal_h(A,Empty,ground,_,Hyps,Hyps) :- is_empty_set_direct(Empty), !, check_empty_set(A,Hyps,_).
check_equal_h(Empty,A,ground,_,Hyps,Hyps) :- is_empty_set_direct(Empty), !, check_empty_set(A,Hyps,_).
Calls:
Name: check_empty_set/3 |
Module: well_def_prover |
Name: ! |
|
Name: is_empty_set_direct/1 |
Module: well_def_prover |
Name: avl_fetch_from_hyps/2 |
Module: well_def_prover |
Name: RECURSIVE_CALL/6 |
Module: well_def_prover |
Name: nonmember/2 |
|
| Module: well_def_prover | |
Name: =/2 |
Called:
Name: check_equal/4 |
Module: well_def_prover |
Name: check_equal_pattern/4 |
Module: well_def_prover |
check_equal_pattern(A,Target,Hyps,Hyps1) :-
check_equal_h(A,Target,not_ground,[],Hyps,Hyps1).
Calls:
Name: check_equal_h/6 |
Module: well_def_prover |
Called:
Name: get_record_type_fields/4 |
Module: well_def_prover |
Name: get_type_from_hyps/4 |
Module: well_def_prover |
| Module: well_def_prover |
check_finite(bool_set,_,bool_set) :- !.
check_finite(empty_set,_,empty_set) :- !.
check_finite(empty_sequence,_,empty_sequence) :- !.
check_finite(float_set,_,float_set) :- !.
check_finite(set_extension(_),_,set_extension) :- !.
check_finite(sorted_set_extension(_),_,set_extension) :- !.
check_finite(sequence_extension(_),_,seq_extension) :- !.
check_finite(fin_subset(X),Hyps,fin(PT)) :- !, check_finite(X,Hyps,PT).
check_finite(fin1_subset(X),Hyps,fin1(PT)) :- !, check_finite(X,Hyps,PT).
check_finite(pow_subset(X),Hyps,pow(PT)) :- !, check_finite(X,Hyps,PT).
check_finite(pow1_subset(X),Hyps,pow1(PT)) :- !, check_finite(X,Hyps,PT).
check_finite(iseq(X),Hyps,iseq(PT)) :- !, check_finite(X,Hyps,PT).
check_finite(iseq1(X),Hyps,iseq1(PT)) :- !, check_finite(X,Hyps,PT).
check_finite(mu(Set),Hyps,mu) :- !, has_finite_elements(Set,Hyps).
check_finite(perm(X),Hyps,perm(PT)) :- !, check_finite(X,Hyps,PT).
check_finite(Set,Hyps,hyp) :-
avl_fetch_from_hyps(finite(Set),Hyps),!.
check_finite(domain(A),Hyp,dom(PT)) :- !,
(check_finite(A,Hyp,PT) -> true ; finite_domain(A,Hyp,PT)).
check_finite(range(A),Hyp,ran(PT)) :- !,
(check_finite(A,Hyp,PT) -> true ; finite_range(A,Hyp,PT)).
check_finite(reverse(A),Hyp,rev(PT)) :- !, check_finite(A,Hyp,PT).
check_finite(identity(A),Hyp,id(PT)) :- !,check_finite(A,Hyp,PT). % finite(id(A)) if finite(A)
check_finite(function(Func,_),Hyps,function_finite_elements) :- !,
get_range_or_superset(Func,Hyps,RanFunc,Hyps2),
has_finite_elements(RanFunc,Hyps2).
check_finite(image(Func,B),Hyp,image(PT)) :- !,
(check_finite(Func,Hyp,PT) -> true % finite(Func[.]) <= finite(Func)
; check_finite(B,Hyp,PTB)
-> PT = pfun(PTB), check_is_partial_function(Func,Hyp) % finite(Func[B]) <= finite(B) & Func : TD +-> TR
).
check_finite(union(A,B),Hyp,union(PTA,PTB)) :- !, (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)).
check_finite(if_then_else(_,A,B),Hyps,if(PTA,PTB)) :- !, (check_finite(A,Hyps,PTA) -> check_finite(B,Hyps,PTB)).
check_finite(intersection(A,B),Hyps,intersection(D,PT)) :- !,
(D=left,check_finite(A,Hyps,PT) -> true ; D=right,check_finite(B,Hyps,PT)).
check_finite(cartesian_product(A,B),Hyp,cart(PT)) :-
(check_finite(A,Hyp,PT) -> (check_equal_empty_set(A,Hyp,_PT2) -> true ; check_finite(B,Hyp,_PT2))
; check_equal_empty_set(B,Hyp,PT)).
check_finite(Rel,Hyp,rel(PTA,PTB)) :- is_relations_type(Rel,A,B),!,
(check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). % add other relations
check_finite(direct_product(A,B),Hyp,direct_product(PTA,PTB)) :- !,
(check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)).
check_finite(parallel_product(A,B),Hyp,parallel_product(PTA,PTB)) :- !,
(check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)).
check_finite(overwrite(A,B),Hyp,overwrite(PTA,PTB)) :- !, (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)).
check_finite(set_subtraction(A,_),Hyps,set_subtraction(PT)) :- !, check_finite(A,Hyps,PT).
check_finite(domain_restriction(A,BRel),Hyp,domain_restriction(PT)) :- !,
(check_finite(BRel,Hyp,PT) -> true
; check_is_partial_function(BRel,Hyp), check_finite(A,Hyp,PT)
; finite_range(BRel,Hyp,_) -> check_finite(A,Hyp,PT) % finite(a <| brel) if finite(a) & finite(ran(brel))
).
check_finite(domain_subtraction(_,B),Hyp,domain_subtraction(PT)) :- !, check_finite(B,Hyp,PT).
check_finite(range_restriction(ARel,B),Hyp,range_restriction(PT)) :- !,
(check_finite(ARel,Hyp,PT) -> true
; check_is_injective(ARel,Hyp) -> check_finite(B,Hyp,PT)
; finite_domain(ARel,Hyp,_) -> check_finite(B,Hyp,PT) % finite(arel |> b) if finite(b) & finite(dom(arel))
).
check_finite(image(A,B),Hyp,image(PT)) :- % A[B] is finite if A is finite or if B is finite and A a function
(check_finite(A,Hyp,PT) -> true ; check_is_partial_function(A,Hyp), check_finite(B,Hyp,PT)).
check_finite(range_subtraction(A,_),Hyp,range_subtraction(PT)) :- check_finite(A,Hyp,PT).
check_finite(interval(_,_),_,interval) :- !.
check_finite(value(V),_,empty_set_value) :- V==[], !.
check_finite(value(X),_,avl_set) :- nonvar(X),X=avl_set(_),!.
check_finite('$'(ID),Hyps,finite_type) :-
get_hyp_var_type(ID,Hyps,Type), %print(chk_fin(ID,Type)),nl,
(is_finite_type_for_wd(Type,Hyps) -> true
; Type = set(couple(DomType,_)), % in principle an infinite relation type
is_finite_type_for_wd(DomType,Hyps), % we have something like set(couple(boolean,integer))
% note: we treat this here in addition to the case is_partial_function below, as
% sometimes we loose the typing information in the term, e.g., in comprehension_set
avl_fetch_equal_from_hyps('$'(ID),Hyps,Func,_),
is_lambda_function(Func) % we have a function, it is finite if the domain is finite
),!.
check_finite('$'(ID),Hyps,enumerated_set) :-
enumerated_set(ID),
\+ is_hyp_var(ID,Hyps),!. % global enumerated set visible
check_finite('$'(ID),Hyps,rewrite(Operator,PT)) :-
(Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyp
avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2),
not_occurs(Set2,ID), % avoid silly, cyclic rewrites $x -> reverse(reverse($x)) (FunLawsStrings.mch)
% however, in SetLawsNatural this prevents proving 2 POs due to SS <: min(SS)..max(SS)
rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3),
check_finite(Set2,Hyps3,PT),!.
check_finite(Set,Hyp,finite_elements) :- id_or_record_field(Set),
avl_fetch_mem_or_struct(Set,Hyp,Set2,Hyp2),
Set2 \= Set,
has_finite_elements(Set2,Hyp2).
check_finite(Func,Hyp,pfun(PTA,PTB)) :- is_partial_function(Func,A,B),!,
% a set of partial functions from A to B is finite if both A and B are finite
(check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)),!.
check_finite(Seq,Hyp,seq_type) :- infer_sequence_type_of_expr(Seq,Hyp,_),!. % a sequence is always finite
check_finite(comprehension_set(Paras,Body),Hyp,comprehension_set) :-
finite_comprehension_set(Paras,Body,Hyp),!.
check_finite(struct(rec(Fields)),Hyp,struct) :- maplist(check_finite_field(Hyp),Fields).
check_finite(general_union(SetOfSets),Hyp,general_union) :-
check_all_finite(SetOfSets,Hyp).
check_finite(general_intersection(SetOfSets),Hyp,general_intersection(PT)) :-
check_some_finite(SetOfSets,Hyp,PT).
Calls:
Called:
Name: prove_po/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: finite_domain/3 |
Module: well_def_prover |
Name: l_check_finite/2 |
Module: well_def_prover |
Name: finite_range/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_some_finite/3 |
Module: well_def_prover |
Name: has_finite_elements/2 |
Module: well_def_prover |
Name: check_finite_field/2 |
Module: well_def_prover |
Name: check_all_finite/2 |
Module: well_def_prover |
check_finite_field(Hyp,field(_,Set)) :- check_finite(Set,Hyp,_PT).
Calls:
Name: check_finite/3 |
Module: well_def_prover |
check_in_interval(El,Min,Max,Hyps,PT) :-
check_subset_interval(interval(Min,Max),El,El,Hyps,PT). % calls check_sub_intervals(Min,Max,El,El,Hyps)
Calls:
Name: check_subset_interval/5 |
Module: well_def_prover |
Called:
Name: check_member_of_set/4 |
Module: well_def_prover |
check_integer(A,PP) :- not_integer(A),!, add_error(PP,'Not an integer: ',A),fail.
check_integer(_,_).
Calls:
Name: fail |
|
Name: add_error/3 |
Module: error_manager |
Name: ! |
|
Name: not_integer/1 |
Module: well_def_prover |
Called:
Name: check_member_of_set/4 |
Module: well_def_prover |
check_is_injective(Func,Hyps) :-
get_type_from_hyps(Func,Hyps,Function,Hyps1),
%print(check_rev_fun(Func,Function)),nl,
is_injective_function_type(Function,Hyps1,_).
check_is_injective(value(avl_set(AVL)),_) :- !,
nonvar(AVL), invert_explicit_set(avl_set(AVL),Inv),
Inv=avl_set(AVL2), is_avl_partial_function(AVL2).
check_is_injective(identity(_),_).
check_is_injective(Set,_) :- singleton_set(Set,_). % TO DO: extend to more than singleton set_extension
check_is_injective(sequence_extension([_]),_). % TO DO: check all elements are different
check_is_injective(Func, Hyps) :-
avl_fetch_equal_from_hyps(Func,Hyps,Value,Hyps2),
%print(check_inj_value(Func,Value)),nl,
check_is_injective(Value,Hyps2).
Calls:
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: singleton_set/2 |
Module: well_def_prover |
| Module: custom_explicit_sets | |
Name: =/2 |
|
Name: invert_explicit_set/2 |
Module: custom_explicit_sets |
Name: nonvar/1 |
|
Name: ! |
|
| Module: well_def_prover | |
Name: get_type_from_hyps/4 |
Module: well_def_prover |
Called:
Name: check_finite/3 |
Module: well_def_prover |
| Module: well_def_prover |
check_is_non_empty_sequence(El,Hyps) :- check_is_sequence(El,Hyps,seq1).
Calls:
Name: check_is_sequence/3 |
Module: well_def_prover |
Called:
Name: check_member_of_domain/4 |
Module: well_def_prover |
Name: check_leq_nr_size/3 |
Module: well_def_prover |
Name: check_subset_interval/5 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
check_is_partial_function(Func,Hyps) :-
avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1),
% also deals with function(_) f : _ +-> ( _ +-> _ ) => f(_) : _ +-> _
is_partial_function_type(Function,Hyps1,_),!.
check_is_partial_function(reverse(Func),Hyps) :-
check_is_injective(Func,Hyps),!.
check_is_partial_function(value(avl_set(AVL)),_) :- !,
nonvar(AVL),
is_avl_partial_function(AVL).
check_is_partial_function(composition(F1,F2),Hyp) :- !,
% composition of two partial functions is a partial function
(check_is_partial_function(F1,Hyp)
-> check_is_partial_function(F2,Hyp)
).
check_is_partial_function(overwrite(F1,F2),Hyp) :- !,
% overwrite of two partial functions is a partial function
(check_is_partial_function(F1,Hyp)
-> check_is_partial_function(F2,Hyp)
).
check_is_partial_function(direct_product(F1,F2),Hyp) :- !,
% direct_product of two partial functions is a partial function a:A+->B & b:A+->C => a>(B*C)
(check_is_partial_function(F1,Hyp)
-> check_is_partial_function(F2,Hyp)
).
check_is_partial_function(identity(_),_Hyp) :- !.
check_is_partial_function(Func,Hyp) :- function_restriction(Func,LargerFunc), !,
check_is_partial_function(LargerFunc,Hyp).
check_is_partial_function(intersection(F1,F2),Hyp) :- !,
(check_is_partial_function(F1,Hyp) -> true ; check_is_partial_function(F2,Hyp)).
check_is_partial_function(sorted_set_extension(List),Hyp) :- !,
check_set_extension_is_partial_function(List,Hyp).
check_is_partial_function(set_extension(List),Hyp) :- !,
check_set_extension_is_partial_function(List,Hyp).
check_is_partial_function(Expr,_) :-
is_lambda_function(Expr),!. % also treats cartesian_product and sequence_extension
check_is_partial_function(Expr,Hyps) :-
infer_sequence_type_of_expr(Expr,Hyps,_),!. % any sequence expression is a partial function; e.g. a <- b, front(.)
check_is_partial_function(Func,Hyps) :- rewrite_set_expression_exact(Func,Hyps,NewFunc,Hyps2),!,
check_is_partial_function(NewFunc,Hyps2).
check_is_partial_function(union(F1,F2),Hyps) :-
check_is_subset(F1,F2,Hyps,_),!,
check_is_partial_function(F2,Hyps).
check_is_partial_function(union(F1,F2),Hyps) :-
check_is_subset(F2,F1,Hyps,_),!,
check_is_partial_function(F1,Hyps).
check_is_partial_function(union(F1,F2),Hyps) :- !,
check_domain_disjoint(F1,F2,Hyps,Hyps2), % domain must be disjoint, not F1 and F2
check_is_partial_function(F1,Hyps2),
check_is_partial_function(F2,Hyps2).
check_is_partial_function(Func,Hyps) :- % f<:g & g: A +-> B => f : A +-> B
(Op = equal ; Op = subset),
avl_fetch_binop_from_hyps(Func,Op,Hyps,Func2,Hyps1),
quick_not_occurs_check(Func,Func2),
check_is_partial_function(Func2,Hyps1).
Calls:
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
Name: quick_not_occurs_check/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: =/2 |
|
Name: check_domain_disjoint/4 |
Module: well_def_prover |
Name: ! |
|
Name: check_is_subset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: is_lambda_function/1 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: true |
|
Name: ->/3 |
|
Name: function_restriction/2 |
Module: well_def_prover |
Name: ->/2 |
|
| Module: custom_explicit_sets | |
Name: nonvar/1 |
|
Name: check_is_injective/2 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover |
Called:
Name: check_finite/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover |
check_is_partial_function_with_type(Func,_,_,Hyps,empty_set(PT)) :- check_equal_empty_set(Func,Hyps,PT),!.
check_is_partial_function_with_type(Func,Domain,Range,Hyps,pfun(PTD,PTR)) :-
check_is_partial_function(Func,Hyps),!,
(maximal_set(Domain,Hyps) -> PTD=maximal_domain ; check_is_subset(domain(Func),Domain,Hyps,PTD)),!,
(maximal_set(Range,Hyps) -> PTR=maximal_range ; check_is_subset(range(Func),Range,Hyps,PTR)).
Calls:
Name: check_is_subset/4 |
Module: well_def_prover |
Name: =/2 |
|
Name: maximal_set/2 |
Module: well_def_prover |
Name: ->/3 |
|
Name: ! |
|
| Module: well_def_prover | |
Name: check_equal_empty_set/3 |
Module: well_def_prover |
Called:
Name: check_member_of_set/4 |
Module: well_def_prover |
check_is_sequence(El,Hyps) :- check_is_sequence(El,Hyps,_).
Calls:
Name: check_is_sequence/3 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: check_is_sequence/2 |
Module: well_def_prover |
check_is_sequence(S,_,seq) :- is_empty_set_direct(S),!.
check_is_sequence(El,Hyps,RequiredType) :-
infer_sequence_type_of_expr(El,Hyps,Type),
(Type=seq1 -> true ; RequiredType=seq -> true
; check_not_equal_empty_set(El,Hyps,_)).
check_is_sequence(A,Hyps,RequiredType) :-
avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),
check_is_sequence(Value,Hyps2,RequiredType).
check_is_sequence(domain_restriction(Dom,S),Hyps,Res) :- !,
is_interval(Dom,Hyps,1,N),
check_is_sequence(S,Hyps,SeqType),
(SeqType=seq1, check_leq(1,N,Hyps) -> Res=seq1 ; Res=seq).
check_is_sequence(El,Hyps,RequiredType) :-
avl_fetch_mem_or_struct(El,Hyps,Set,Hyps2),
is_set_of_sequences_type(Set,Hyps2,Type), % should we move this to subset? dealt with in subset_transitivity_rule
% required for :wd Right:seq(BOOL) & (Right/=[] => tail(Right)=res) in test 2018
(Type=seq1 -> true ; RequiredType=seq -> true
; check_not_equal_empty_set(El,Hyps2,_)),
!.
check_is_sequence(X,Hyps,RequiredType) :- try_get_set_of_possible_values(X,Hyps,XSet,Hyps2),
(RequiredType==seq1 -> check_is_subset(XSet,seq1(typeset),Hyps2,_PT)
; check_is_subset(XSet,seq(typeset),Hyps2,_PT)).
Calls:
Name: check_is_subset/4 |
Module: well_def_prover |
Name: ==/2 |
|
Name: ->/3 |
|
| Module: well_def_prover | |
Name: ! |
|
| Module: well_def_prover | |
Name: true |
|
Name: =/2 |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_leq/3 |
Module: well_def_prover |
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: is_interval/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: is_empty_set_direct/1 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: check_is_sequence/2 |
Module: well_def_prover |
check_is_subset(H,H,_,equal).
check_is_subset(A,B,Hyps,hyp) :-
avl_fetch_from_hyps(subset(A,B),Hyps),!. % hyp
check_is_subset(_,MAX,Hyps,maximal_set) :- maximal_set(MAX,Hyps),!.
check_is_subset(S,_,Hyps,empty_set(PT)) :- check_equal_empty_set(S,Hyps,PT),!. % {} <: B
check_is_subset(cartesian_product(A,B),cartesian_product(A2,B2),Hyps,cart(PTA,PTB)) :- !,
% A <: A2 & B <: B2 => (A*B) <: (A2*B2)
(check_is_subset(A,A2,Hyps,PTA)
-> check_is_subset(B,B2,Hyps,PTB)).
check_is_subset('NATURAL1','NATURAL',_,nat1_nat) :- !.
check_is_subset(interval(L,U),B,Hyps,interval(PT)) :- !, check_subset_interval(B,L,U,Hyps,PT).
check_is_subset(intersection(A,B),Super,Hyps,intersection(PT)) :- !,
( check_is_subset(A,Super,Hyps,PT) -> true ; check_is_subset(B,Super,Hyps,PT)).
check_is_subset(union(A,B),Super,Hyps,union(PTA,PTB)) :- !,
( check_is_subset(A,Super,Hyps,PTA) -> check_is_subset(B,Super,Hyps,PTB)).
check_is_subset(domain_subtraction(_,B),Super,Hyps,dom_sub(PT)) :- !,check_is_subset(B,Super,Hyps,PT).
check_is_subset(domain_restriction(_,B),Super,Hyps,dom_res(PT)) :- !,check_is_subset(B,Super,Hyps,PT).
check_is_subset(range_subtraction(A,_),Super,Hyps,ran_sub(PT)) :- !,check_is_subset(A,Super,Hyps,PT).
check_is_subset(range_restriction(A,_),Super,Hyps,ran_res(PT)) :- !,check_is_subset(A,Super,Hyps,PT).
check_is_subset(set_subtraction(A,_),Super,Hyps,set_sub(PT)) :- !,check_is_subset(A,Super,Hyps,PT).
check_is_subset(value(avl_set(AVL)),B,Hyps,avl) :- !,check_subset_avl(B,AVL,Hyps).
check_is_subset(A,B,Hyps,subset_eq(PT)) :-
(Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyps
% TO DO: similar rule for B
avl_fetch_binop_from_hyps(A,Operator,Hyps,S2,Hyps2),
rewrite_local_loop_check(A,check_is_subset,S2,Hyps2,Hyps3),
check_is_subset(S2,B,Hyps3,PT),!.
check_is_subset('$'(ID),B,Hyps,eq(ID,PT)) :-
get_type_from_hyps('$'(ID),Hyps,Set,Hyps2),
extract_element_super_set_type(Set,Hyps2,S2),
rewrite_local_loop_check(ID,check_is_subset,S2,Hyps2,Hyps3),
check_is_subset(S2,B,Hyps3,PT),!.
check_is_subset(domain(Func),B,Hyps,domain(PT)) :-
get_domain_or_superset(Func,Hyps,DomFunc,Hyps2),
%rewrite_local_loop_check(domain(Func),check_is_subset,DomFunc,Hyps2,Hyps3),
check_is_subset(DomFunc,B,Hyps2,PT),!.
check_is_subset(range(Func),B,Hyps,range(PT)) :-
get_range_or_superset(Func,Hyps,RanFunc,Hyps2),
%rewrite_local_loop_check(range(Func),check_is_subset,RanFunc,Hyps2,Hyps3),
check_is_subset(RanFunc,B,Hyps2,PT),!.
check_is_subset(function(Func,_),B,Hyps,function_range(PT)) :- !,
get_range_or_superset(Func,Hyps,RanFunc,Hyps2), % f : _ +-> POW(Ran) & Ran <: B => f(.) <: B
subset_transitivity_rule(RanFunc,pow_subset(B),A2,B2), % extract pow_subset from Range
check_is_subset(A2,B2,Hyps2,PT).
check_is_subset(image(Func,_),B,Hyps,image(PT)) :- % or B=range(Range)
(B = range(FuncB),check_equal(Func,FuncB,Hyps,_) -> !, PT=range_of_same_func % f[.] <: ran(f)
; get_range_or_superset(Func,Hyps,Range,Hyps2) -> !, check_is_subset(Range,B,Hyps2,PT)).
check_is_subset(A,B,Hyps,transitivity(PT)) :- subset_transitivity_rule(A,B,A2,B2),
!, % unary subset rules like POW(A2) <: POW(B2) if A2 <: B2
check_is_subset(A2,B2,Hyps,PT).
check_is_subset(A,B,Hyps,transitivity(PT1,PT2)) :- subset_bin_transitivity_rule(A,B,A1,A2,B1,B2),
!, % binary subset rules like A1+->B1 <: A2+->B2 if A1 <:B1 & A2 <: B2
(check_is_subset(A1,B1,Hyps,PT1) -> check_is_subset(A2,B2,Hyps,PT2)).
check_is_subset(sorted_set_extension(List),B,Hyps,PT) :- !,
check_is_subset(set_extension(List),B,Hyps,PT).
check_is_subset(set_extension(List),B,Hyps,set_extension) :-
simplify_expr(B,Hyps,BS), % simplify expression once
%portray_hyps(Hyps),nl,
l_check_is_member(List,BS,Hyps).
check_is_subset(Sub,union(A,B),Hyps,sub_union(PT)) :- !,
( check_is_subset(Sub,A,Hyps,PT) -> true ; check_is_subset(Sub,B,Hyps,PT)).
Calls:
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: ! |
|
Name: l_check_is_member/3 |
Module: well_def_prover |
Name: simplify_expr/3 |
Module: well_def_prover |
Name: ->/2 |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: =/2 |
|
Name: check_equal/4 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: get_type_from_hyps/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_subset_avl/3 |
Module: well_def_prover |
Name: check_subset_interval/5 |
Module: well_def_prover |
Name: check_equal_empty_set/3 |
Module: well_def_prover |
Name: maximal_set/2 |
Module: well_def_prover |
Name: avl_fetch_from_hyps/2 |
Module: well_def_prover |
Called:
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_empty_set/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: prove_po/3 |
Module: well_def_prover |
Name: check_is_subset_strict/4 |
Module: well_def_prover |
Name: check_is_sequence/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_disjoint_aux/3 |
Module: well_def_prover |
Name: check_member_of_union/5 |
Module: well_def_prover |
check_is_subset_strict(A,B,Hyp,empty_singleton(PT)) :- % x <<: {A} <=> x={}
singleton_set(B,_),!,
check_equal_empty_set(A,Hyp,PT).
check_is_subset_strict(A,B,Hyp,PT) :- % A <<: B <=> A <: B & A /= B
check_is_subset(A,B,Hyp,PT),!,
check_not_equal(A,B,Hyp).
Calls:
Name: check_not_equal/3 |
Module: well_def_prover |
Name: ! |
|
Name: check_is_subset/4 |
Module: well_def_prover |
Name: check_equal_empty_set/3 |
Module: well_def_prover |
Name: singleton_set/2 |
Module: well_def_prover |
Called:
Name: prove_po/3 |
Module: well_def_prover |
check_leq(I,I,_) :- !.
check_leq(if_then_else(_,A1,A2),B,Hyp) :- !, % TODO?: treat if-then-else for B
(check_leq(A1,B,Hyp) -> check_leq(A2,B,Hyp)).
check_leq(N1,N2,_) :- number(N1), number(N2), !, N1 =< N2.
check_leq(N1,N2,hyp_rec(AVL,_)) :-
(avl_fetch(less_equal(N1,N2),AVL)
-> true
; avl_fetch(equal(N1,N2),AVL)),!.
check_leq(min(List),N2,Hyps) :- !,
member(N1,List), check_leq(N1,N2,Hyps),!.
check_leq(min_int,N2,Hyps) :- !, % we could look up the value of MININT; but largest possible value is -1
MININT is -1,
check_leq(MININT,N2,Hyps).
check_leq(N1,max_int,Hyps) :- !, % we could look up the value of MAXINT; but smallest possible value is 1
MAXINT = 1,
check_leq(N1,MAXINT,Hyps).
check_leq(N1,N2,Hyps) :-
rewrite_integer(N2,Hyps,RN2,Hyps2),!,
check_leq(N1,RN2,Hyps2).
check_leq(add(N1,1),N2,Hyps) :-
check_not_equal(N1,N2,Hyps),
!, % N1+1 <= N2 if N1 <= N2 & N1 \= N2 ; happens quite often in array traversals
check_leq(N1,N2,Hyps).
check_leq(N1,minus(N2,1),Hyps) :- % variation of rule above
check_not_equal(N1,N2,Hyps),
!, % N1 <= N2-1 if N1 <= N2 & N1 \= N2 ; happens in array traversals
check_leq(N1,N2,Hyps).
check_leq(Nr,X,Hyps) :-
\+ number(X),
try_get_set_of_possible_values(X,Hyps,SetX,Hyps2),
check_all_values_geq_val(SetX,Nr,Hyps2),!.
check_leq(Nr,X,Hyps) :- number(Nr), !,
check_leq_nr(Nr,X,Hyps).
check_leq(N1,N2,Hyps) :- rewrite_integer(N1,Hyps,RN1,Hyps2),!,
check_leq(RN1,N2,Hyps2).
check_leq(Add,N2,Hyps) :- % A+N1 <= N2 <=> A <= N2-N1
number(N2),
add_with_number(Add,A,N1),!,
N21 is N2-N1,
check_leq(A,N21,Hyps).
check_leq(Mul,N2,Hyps) :- % A*N1 <= N2 if A <= N2/N1 if N1>0 and N2 mod N1=0
number(N2),
mul_with_number(Mul,A,N1),
% symmetrical case to check_leq_nr(N1,Mul,Hyps), with N1=-N2
!,
( N1=0 -> check_leq(0,N2,Hyps)
; N1>0 -> N21 is N2 div N1, % A <= 1.5 means we have to have A <= 1;
% A <= -1.5 means we have to have A <= -2 -3 div 2 =:= -2
check_leq(A,N21,Hyps)
; cdiv(N2,N1,N21), % A >= 1.5 means we have to have A >= 2 ; cdiv
check_leq(N21,A,Hyps)
).
check_leq(div(A,N1),N2,Hyps) :- % A/N1 <= N2 <=> A <= (N1+1)*N2-1
number(N1),number(N2), N1>0,
!,
N12 is (N2+1)*N1-1,
check_leq(A,N12,Hyps).
check_leq(div(A1,N1),A2,Hyps) :- number(N1), N1>0, % A/N1 <= A if N1>0 & A>=0
check_equal(A1,A2,Hyps,Hyps1),!,
check_leq(0,A1,Hyps1).
check_leq(modulo(A1,A2),B,Hyps) :-
\+ z_or_tla_minor_mode, % args to mod must be non-negative, modulo is between 0..A2-1
((number(A2),A21 is A2-1 -> check_leq(A21,B,Hyps)
; B=minus(B1,1) -> check_leq(A2,B1,Hyps)
; check_leq(A2,B,Hyps)
) -> true
; check_leq(A1,B,Hyps)).
check_leq(unary_minus(A),unary_minus(B),Hyps) :- !, % -A <= -B ---> A >= B
check_leq(B,A,Hyps).
check_leq(X,Nr,Hyps) :- \+ number(X),
try_get_set_of_possible_values(X,Hyps,SetX,Hyps2),
check_all_values_leq_val(SetX,Nr,Hyps2),!. % cut here; get set of possible values can give multiple solutions
check_leq(Minus,N2,Hyps) :- minus_with_number(Minus,N1,Nr),
Nr >= 0,!, % N1-Nr <= N2 if N1 <= N2
% Both N1 and N2 are usually not numbers here
check_leq(N1,N2,Hyps).
check_leq(N1,Add,Hyps) :-
add_with_number(Add,N2,Nr),Nr >= 0,!, % N1 <= N2+Nr if N1 <= N2
% Both N1 and N2 are usually not numbers here
check_leq(N1,N2,Hyps).
check_leq(add(A,B),E,Hyps) :- decompose_floor(E,X,Y), % e.g. divide a number E by 2
check_leq(A,X,Hyps), % TO DO: other combinations like A <= 0, B <= Nr; or we could try_get_set_of_possible_values
check_leq(B,Y,Hyps).
check_leq('$'(X),N2,Hyps) :-
avl_fetch_binop_from_hyps('$'(X),less_equal,Hyps,Y,Hyps2),
(number(N2),avl_fetch_not_equal('$'(X),Y,Hyps) % as we know X and Y we can use regular avl_fetch
-> N21 is N2+1 % we have X
; N21=N2),
check_leq(Y,N21,Hyps2).
check_leq(Nr,'$'(X),Hyps) :-
( avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
rewrite_local_loop_check(X,check_leq,Y,Hyps2,Hyps3),
check_leq(Nr,Y,Hyps3) -> true
% ; avl_fetch_binop_from_hyps('$'(X),greater,Hyps,Y,Hyps2), N1 is Nr-1, check_leq(N1,Y,Hyps2) -> true
; avl_fetch_binop_from_hyps('$'(X),greater_equal,Hyps,Y,Hyps2),
% note: Nr is not a number, hence probably not useful to check not_equal in Hyps, as we cannot compute Nr-1
check_leq(Nr,Y,Hyps2)
-> true
),
!.
Calls:
Name: ! |
|
Name: true |
|
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: ->/2 |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ->/3 |
|
Name: =/2 |
|
Name: is/2 |
|
Name: avl_fetch_not_equal/3 |
Module: well_def_prover |
Name: number/1 |
|
Name: decompose_floor/3 |
Module: well_def_prover |
Name: >=/2 |
|
Name: add_with_number/3 |
Module: well_def_prover |
Name: minus_with_number/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: not/1 |
|
Name: z_or_tla_minor_mode/0 |
Module: specfile |
Name: check_equal/4 |
Module: well_def_prover |
Name: >/2 |
|
Name: cdiv/3 |
Module: well_def_prover |
Name: mul_with_number/3 |
Module: well_def_prover |
Name: rewrite_integer/4 |
Module: well_def_prover |
Name: check_leq_nr/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_not_equal/3 |
Module: well_def_prover |
Name: member/2 |
|
Name: avl_fetch/2 |
Module: foo_error |
Name: =</2 |
Called:
Name: prove_po/3 |
Module: well_def_prover |
Name: check_is_sequence/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_not_empty_set/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_not_equal/3 |
Module: well_def_prover |
Name: check_subset_interval/5 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_sub_intervals/5 |
Module: well_def_prover |
Name: check_leq_nr/3 |
Module: well_def_prover |
Name: check_less/3 |
Module: well_def_prover |
| Module: well_def_prover |
check_leq_nr(N1,Add,Hyps) :- % N1 <= A+N2 <=> N1-N2 <= A
add_with_number(Add,A,N2), !,
N12 is N1-N2,
check_leq(N12,A,Hyps).
check_leq_nr(Nr,add(N1,N2),Hyps) :- !, % 0 <= A+B if 0 <= A & 0 <= B
% Both N1 and N2 are usually not numbers here
cdiv(Nr,2,Nr2), % Note: cdiv(-3,2) = 1, cdiv(3,2)=2
check_leq(Nr2,N1,Hyps),
check_leq(Nr2,N2,Hyps).
check_leq_nr(N1,minus(N2,B),Hyps) :- % N1 <= N2-B <=> B <= N2-N1
number(N2), !,
N21 is N2-N1,
check_leq(B,N21,Hyps).
check_leq_nr(N1,Mul,Hyps) :- % N1 <= A*N2 if N1/N2 <= A and N2>0
mul_with_number(Mul,A,N2),
!,
( N2=0 -> check_leq(N1,0,Hyps)
; N2>0 -> cdiv(N1,N2,N12), % cdiv
% if 1.5 <= A --> 2 <= A ; if -1.5 <= A --> -1 <= A
check_leq(N12,A,Hyps)
; N12 is N1 div N2,
% if A <= 1.5 --> A <= 1 ; if -1.5 <= A --> -1 <= A
% A <= -1.5 means we have to have A <= -2 -3 div 2 =:= -2
check_leq(A,N12,Hyps)
).
check_leq_nr(0,multiplication(A,B),Hyps) :- !, % 0 <= A*B if A and B have same parity
(check_leq(0,A,Hyps) -> check_leq(0,B,Hyps)
; check_leq(A,0,Hyps) -> check_leq(B,0,Hyps)).
check_leq_nr(N1,div(A,N2),Hyps) :- % N1 <= A/N2 <=> N1*N2 <= A
number(N2), N2>0,
!,
N12 is N1*N2,
check_leq(N12,A,Hyps).
check_leq_nr(0,div(A,B),Hyps) :- !, % 0 <= A/B if A and B have same parity
(check_leq(0,A,Hyps) -> check_leq(0,B,Hyps) % B \= 0 checked by other WD condition
; check_leq(A,0,Hyps) -> check_leq(B,0,Hyps)). % ditto
check_leq_nr(Nr,'$'(X),Hyps) :-
( avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
rewrite_local_loop_check(X,check_leq,Y,Hyps2,Hyps3),
check_leq(Nr,Y,Hyps3) -> true
% ; avl_fetch_binop_from_hyps('$'(X),greater,Hyps,Y,Hyps2), N1 is Nr-1, check_leq(N1,Y,Hyps2) -> true
; avl_fetch_binop_from_hyps('$'(X),greater_equal,Hyps,Y,Hyps2),
(avl_fetch_not_equal('$'(X),Y,Hyps2) % we have X < Y => sufficient to prove N-1 <= Y
-> N1 is Nr-1, check_leq(N1,Y,Hyps2)
; check_leq(Nr,Y,Hyps2)
)
),
!.
check_leq_nr(Nr,modulo(A,B),Hyps) :- \+ z_or_tla_minor_mode, % A and B must be non-negative, modulo is between 0..B-1
(Nr =< 0 -> true % modulo always positive or 0
; % Nr <= A mod B if Nr <= A and A < B
check_leq_nr(Nr,A,Hyps), % Nr <= A
check_less(A,B,Hyps)). % and A < B so that modulo does not take effect
check_leq_nr(Nr,size(Seq),Hyps) :- check_leq_nr_size(Nr,Seq,Hyps).
check_leq_nr(1,power_of(A,_),Hyps) :- check_leq(1,A,Hyps). % Nr <= 1 <= x**y if x >= 1
check_leq_nr(Nr,power_of(A,_),Hyps) :- number(Nr), Nr =< 0,
check_leq(0,A,Hyps). % 0 <= x**y if x >= 0
Calls:
Name: check_leq/3 |
Module: well_def_prover |
Name: =</2 |
|
Name: number/1 |
|
Name: check_leq_nr_size/3 |
Module: well_def_prover |
Name: check_less/3 |
Module: well_def_prover |
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: z_or_tla_minor_mode/0 |
Module: specfile |
Name: not/1 |
|
Name: ! |
|
Name: is/2 |
|
Name: avl_fetch_not_equal/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ->/2 |
|
Name: >/2 |
|
Name: cdiv/3 |
Module: well_def_prover |
Name: =/2 |
|
Name: mul_with_number/3 |
Module: well_def_prover |
Name: add_with_number/3 |
Module: well_def_prover |
Called:
Name: check_leq/3 |
Module: well_def_prover |
Name: check_leq_nr_size/3 |
Module: well_def_prover |
check_leq_nr_size(Nr,restrict_front(_,RestrN),Hyps) :- !, % X <= size( Seq /|\ N) if X <= N as WD condition implies N : 0..size(Seq)
check_leq_nr(Nr,RestrN,Hyps).
check_leq_nr_size(1,Seq,Hyps) :- check_is_non_empty_sequence(Seq,Hyps).
Calls:
| Module: well_def_prover | |
Name: check_leq_nr/3 |
Module: well_def_prover |
Name: ! |
Called:
Name: check_leq_nr/3 |
Module: well_def_prover |
check_less(A,B,Hyps) :-
check_leq(A,B,Hyps),!,
check_not_equal(A,B,Hyps).
Calls:
Name: check_not_equal/3 |
Module: well_def_prover |
Name: ! |
|
Name: check_leq/3 |
Module: well_def_prover |
Called:
Name: check_leq_nr/3 |
Module: well_def_prover |
Name: check_empty_set/3 |
Module: well_def_prover |
check_member_of_domain(El,reverse(Func2),Hyps,reverse(PT)) :- !,check_member_of_range(El,Func2,Hyps,PT).
check_member_of_domain(Index,Func,Hyps,size_in_dom_seq) :- % x:seq1(T) => size(x) : dom(x)
index_in_non_empty_sequence(Index,Func,Hyps),
check_is_non_empty_sequence(Func,Hyps),!.
check_member_of_domain(El,union(A,B),Hyps,dom_of_union(PT)) :-
check_member_of_union(domain(A),domain(B),El,Hyps,PT).
check_member_of_domain(El,overwrite(A,B),Hyps,dom_of_overwrite(PT)) :-
check_member_of_union(domain(A),domain(B),El,Hyps,PT).
check_member_of_domain(El,direct_product(A,B),Hyps,dom_of_direct_product(PT)) :- % dom(A >< B) = dom(A) /\ dom (B)
check_member_of_set(domain(A),El,Hyps,PT),
check_member_of_set(domain(B),El,Hyps,PT).
check_member_of_domain(El,Func,Hyps,dom_of_subset(PT)) :- % Func2 <: Func & El:dom(Func2) => El:dom(Func)
% counter part of rule with superset for check_member_of_set
(Op = equal ; Op = superset),
avl_fetch_binop_from_hyps(Func,Op,Hyps,Func2,Hyps1),
rewrite_local_loop_check(Func,check_member_of_domain,Func2,Hyps1,Hyps2),
check_member_of_set(domain(Func2),El,Hyps2,PT).
check_member_of_domain(El,comprehension_set(IDS,Body),Hyps,dom_of_lambda(PTs)) :-
get_lambda_args_and_body(IDS,Body,_,_,Args,RestBodyList),
%nl,print(lambda(Args,El,RestBodyList)),nl,
generate_funapp_binding(Args,El,Subst),
% we rename the local variables of the comprehension set; no need to call add_new_hyp_any_vars
l_rename_and_prove_goals(RestBodyList,Subst,Hyps,PTs).
Calls:
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_member_of_set/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: =/2 |
|
Name: check_member_of_union/5 |
Module: well_def_prover |
Name: ! |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_member_of_range/4 |
Module: well_def_prover |
Called:
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_member_of_range/4 |
Module: well_def_prover |
check_member_of_range(El,reverse(Func2),Hyps,reverse(PT)) :- !,check_member_of_domain(El,Func2,Hyps,PT).
check_member_of_range('$'(ID),Func2,Hyps,PT) :-
avl_fetch_worthwhile_equal_from_hyps('$'(ID),Hyps,Value,Hyps2),
check_member_of_range(Value,Func2,Hyps2,PT).
check_member_of_range(function(Func1,_),Func2,Hyps,func_app_in_range) :- % f(.) : ran(f)
check_equal(Func1,Func2,Hyps,_).
Calls:
Name: check_equal/4 |
Module: well_def_prover |
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_member_of_domain/4 |
Module: well_def_prover |
Name: ! |
Called:
Name: check_member_of_domain/4 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
check_member_of_set(Set,_,Hyps,maximal_set) :- maximal_set(Set,Hyps), !.
check_member_of_set(Set,if_then_else(_,A,B),Hyps,if(P1,P2)) :- !, % if-then-else exprssion
(check_member_of_set(Set,A,Hyps,P1) -> check_member_of_set(Set,B,Hyps,P2)).
check_member_of_set(Set,El,Hyps,hyp) :-
% we could do avl_fetch_binop_from_hyps(El,member,Hyps,Set2,Hyps2), and check_subset(Set2,Set)
avl_fetch_from_hyps(member(El,Set),Hyps),!. % hyp
check_member_of_set(sorted_set_extension(List),El,Hyps,PT) :- !, % ordsets:ord_member(El,List),!.
check_member_of_set(set_extension(List),El,Hyps,PT).
check_member_of_set(set_extension(List),El,Hyps,set_extension) :- member(El2,List),
check_equal(El,El2,Hyps,_),!. % TO DO: avoid multiple equality rewriting of El for long lists ?
check_member_of_set(partial_function(T1,T2),El,Hyps,partial_function(PT)) :-
check_is_partial_function_with_type(El,T1,T2,Hyps,PT).
check_member_of_set(range(Func),El,Hyps,mem_range(PT)) :-
check_member_of_range(El,Func,Hyps,PT),!. % check before function application below, can do symbolic range check
check_member_of_set(image(Func,set_extension([S1|_])),El,Hyps,mem_range_for_image(PT0,PT1)) :-
% El:ran(F) & S /\ dom(F) \= {} => El:F[S]
check_member_of_set(range(Func),El,Hyps,PT0),!,
check_member_of_set(domain(Func),S1,Hyps,PT1). % TO DO: more general check S /\ dom(F) \= {}
check_member_of_set(A,ElFunc,Hyps,typing_membership(PT)) :-
get_type_from_hyps(ElFunc,Hyps,Range,Hyps2), % !, % moving cut later proves on additional PO for test 2039
% e.g. f(.) : A if ran(f) <: Range & Range <: A
%rewrite_local_loop_check(A,check_member_of_set,Range,Hyps2,Hyps3),
check_is_subset(Range,A,Hyps2,PT),!.
check_member_of_set(A,El,Hyps,eq(ProofTree)) :-
avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),
rewrite_local_loop_check(A,check_member_of_set,Value,Hyps2,Hyps3),
check_member_of_set(Value,El,Hyps3,ProofTree).
check_member_of_set(interval(L,U),El,Hyps,interval(PT)) :- !, check_in_interval(El,L,U,Hyps,PT).
check_member_of_set('NATURAL1',El,Hyps,nat1(PT)) :- !, check_subset_interval('NATURAL1',El,El,Hyps,PT).
check_member_of_set('NATURAL',El,Hyps,nat(PT)) :- !, check_subset_interval('NATURAL',El,El,Hyps,PT).
check_member_of_set(union(A,B),El,Hyps,union(PTA,PTB)) :- !,
(check_member_of_set(A,El,Hyps,PTA) -> true ; check_member_of_set(B,El,Hyps,PTB)).
check_member_of_set(intersection(A,B),El,Hyps,intersection(PTA,PTB)) :- !,
(check_member_of_set(A,El,Hyps,PTA) -> check_member_of_set(B,El,Hyps,PTB)).
check_member_of_set(set_subtraction(A,B),El,Hyps,set_subtraction(PTA,PTB)) :- !,
(check_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)).
check_member_of_set(pow_subset(T1),El,Hyps,pow(PT)) :- !,
check_is_subset(El,T1,Hyps,PT).
check_member_of_set(fin_subset(T1),El,Hyps,fin(PT1,PT2)) :- !,
check_is_subset(El,T1,Hyps,PT1),!,
check_finite(El,Hyps,PT2).
check_member_of_set(pow1_subset(T1),El,Hyps,pow1(PT)) :- !,
check_not_empty_set(El,Hyps),!,
check_is_subset(El,T1,Hyps,PT).
check_member_of_set(fin1_subset(T1),El,Hyps,fin1(PT1,PT2)) :- !,
check_not_empty_set(El,Hyps),!,
check_is_subset(El,T1,Hyps,PT1),!,
check_finite(El,Hyps,PT2).
check_member_of_set(seq(T1),El,Hyps,seq(PT)) :- !,
check_is_sequence(El,Hyps),
check_is_subset(range(El),T1,Hyps,PT).
check_member_of_set(seq1(T1),El,Hyps,seq1(PT)) :- !,
check_is_non_empty_sequence(El,Hyps),
check_is_subset(range(El),T1,Hyps,PT).
check_member_of_set(cartesian_product(T1,T2),couple(El1,El2),Hyps,cart(PT1,PT2)) :- !,
check_member_of_set(T1,El1,Hyps,PT1),
check_member_of_set(T2,El2,Hyps,PT2).
check_member_of_set(value(avl_set(AVL)),El,Hyps,PT) :-
(avl_can_fetch(El,BVal) -> !,PT=avl_fetch(El),avl_fetch(BVal,AVL)
; avl_is_interval(AVL,Min,Max) -> !, PT=avl_interval(PT2),
% useful is El is not a number, but e.g. an arithmetic expression
% print(avl_interval(Min,Max,El)),nl,
check_integer(El,check_member_of_set_avl_interval),
check_in_interval(El,Min,Max,Hyps,PT2)
).
check_member_of_set(A,El,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!,
check_member_of_set(A2,El,Hyps2,PT).
check_member_of_set(domain(Func),Index,Hyps,mem_domain(PT)) :-
check_member_of_domain(Index,Func,Hyps,PT),!.
check_member_of_set(Set,X,Hyps,value_set(PT)) :- try_get_set_of_possible_values(X,Hyps,XSet,Hyps2),
check_is_subset(XSet,Set,Hyps2,PT),!.
check_member_of_set(Set,X,Hyps,trans(PT)) :-
avl_fetch_binop_from_hyps(Set,superset,Hyps,SubSet,Hyps2), % X:B & B <: A => X:A
check_member_of_set(SubSet,X,Hyps2,PT),!.
check_member_of_set(Set2,max(Set1),Hyps,mem_max(PT)) :- !, check_is_subset(Set1,Set2,Hyps,PT).
check_member_of_set(Set2,min(Set1),Hyps,mem_min(PT)) :- !, check_is_subset(Set1,Set2,Hyps,PT).
Calls:
Called:
Name: prove_po/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_member_of_domain/4 |
Module: well_def_prover |
Name: l_check_is_member/3 |
Module: well_def_prover |
Name: check_member_of_union/5 |
Module: well_def_prover |
Name: check_not_empty_set/2 |
Module: well_def_prover |
check_member_of_union(Set1,_,El,Hyps,PT) :- check_member_of_set(Set1,El,Hyps,PT),!.
check_member_of_union(_,Set2,El,Hyps,PT) :- check_member_of_set(Set2,El,Hyps,PT),!.
check_member_of_union(Set1,Set2,El,Hyps,union(PT1,PT2)) :-
% x : A \/ B & A <: S1 & B <: S2 => x : S1 \/ S2
avl_fetch_mem_from_hyps(El,Hyps,union(A,B),Hyps2), % TO DO: other conditions ?
(check_is_subset(A,Set1,Hyps2,PT1) -> check_is_subset(B,Set2,Hyps2,PT2)
; check_is_subset(A,Set2,Hyps2,PT1) -> check_is_subset(B,Set1,Hyps2,PT2)).
Calls:
Name: check_is_subset/4 |
Module: well_def_prover |
Name: ->/2 |
|
Name: ->/3 |
|
| Module: well_def_prover | |
Name: ! |
|
Name: check_member_of_set/4 |
Module: well_def_prover |
Called:
Name: check_member_of_domain/4 |
Module: well_def_prover |
check_not_empty_elements(fin1_subset(_),_).
check_not_empty_elements(pow1_subset(_),_).
check_not_empty_elements(seq1(_),_).
check_not_empty_elements(iseq1(_),_).
check_not_empty_elements(perm(A),Hyps) :- check_not_empty_set(A,Hyps).
check_not_empty_elements(total_function(A,_),Hyps) :- check_not_empty_set(A,Hyps).
check_not_empty_elements(total_injection(A,_),Hyps) :- check_not_empty_set(A,Hyps).
check_not_empty_elements(total_surjection(A,B),Hyps) :-
(check_not_empty_set(A,Hyps) -> true ; check_not_empty_set(B,Hyps)).
check_not_empty_elements(total_bijection(A,B),Hyps) :-
(check_not_empty_set(A,Hyps) -> true ; check_not_empty_set(B,Hyps)).
check_not_empty_elements(total_relation(A,_),Hyps) :- check_not_empty_set(A,Hyps).
check_not_empty_elements(total_surjection_relation(A,_),Hyps) :- check_not_empty_set(A,Hyps).
check_not_empty_elements(partial_surjection(_,B),Hyps) :- check_not_empty_set(B,Hyps).
check_not_empty_elements(partial_bijection(_,B),Hyps) :- check_not_empty_set(B,Hyps).
check_not_empty_elements(surjection_relation(_,B),Hyps) :- check_not_empty_set(B,Hyps).
Calls:
Name: check_not_empty_set/2 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
Called:
Name: check_not_empty_set/2 |
Module: well_def_prover |
check_not_empty_set(A,Hyps) :- avl_fetch_from_hyps(not_equal(A,empty_set),Hyps),!.
check_not_empty_set(A,Hyps) :- %Note: size(A) should be changed to card(A) in normalization
(CardA = card(A) ; CardA = size(A)),
avl_fetch_binop_from_hyps(CardA,greater_equal,Hyps,Nr,Hyps2), %Nr \= 0,
check_leq(1,Nr,Hyps2),!. % cut here, relevant for test 2043
check_not_empty_set(set_extension([_|_]),_Hyps).
check_not_empty_set(sorted_set_extension([_|_]),_Hyps).
check_not_empty_set(sequence_extension([_|_]),_Hyps).
check_not_empty_set(cartesian_product(A,B),Hyps) :- % SIMP_CPROD_EQUAL_EMPTY
(check_not_empty_set(A,Hyps) -> check_not_empty_set(B,Hyps)).
check_not_empty_set(interval(A,B),Hyps) :- check_leq(A,B,Hyps).
check_not_empty_set(value(avl_set(AVL)),_) :- AVL \= empty.
check_not_empty_set(union(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)).
check_not_empty_set(general_union(A),Hyp) :- !, % SIMP_KUNION_EQUAL_EMPTY
check_not_subset(A,set_extension([empty_set]),Hyp,_PT).
check_not_empty_set(set_subtraction(A,B),Hyp) :- !, % see SIMP_SETMINUS_EQUAL_EMPTY Rodin proof rule
check_not_subset(A,B,Hyp,_PT).
check_not_empty_set(overwrite(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)).
check_not_empty_set(domain(A),Hyp) :- !, % SIMP_DOM_EQUAL_EMPTY
check_not_empty_set(A,Hyp).
check_not_empty_set(range(A),Hyp) :- !, % SIMP_RAN_EQUAL_EMPTY
check_not_empty_set(A,Hyp).
check_not_empty_set(identity(A),Hyp) :- !, check_not_empty_set(A,Hyp).
check_not_empty_set(image(R,interval(L,U)),Hyp) :- !,
check_not_empty_set(interval(L,U),Hyp),
(check_member_of_set(domain(R),L,Hyp,_) -> true
; check_member_of_set(domain(R),U,Hyp,_)
).
check_not_empty_set(reverse(A),Hyp) :- !, % SIMP_CONVERSE_EQUAL_EMPTY (relational inverse)
check_not_empty_set(A,Hyp).
check_not_empty_set(rev(A),Hyp) :- !, check_not_empty_set(A,Hyp).
check_not_empty_set(concat(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)).
check_not_empty_set(bool_set,_Hyp) :- !.
check_not_empty_set(float_set,_Hyp) :- !.
check_not_empty_set(real_set,_Hyp) :- !.
check_not_empty_set(string_set,_Hyp) :- !.
check_not_empty_set('NATURAL1',_Hyp) :- !. % SIMP_NATURAL1_EQUAL_EMPTY
check_not_empty_set('NATURAL',_Hyp) :- !. % SIMP_NATURAL_EQUAL_EMPTY
check_not_empty_set(typeset,_Hyp) :- !. % SIMP_TYPE_EQUAL_EMPTY, all basic sets are non empty in B and Event-B
check_not_empty_set(relations(_,_),_Hyp) :- !. % SIMP_SPECIAL_EQUAL_REL
check_not_empty_set(total_function(A,B),Hyp) :- !, % SIMP_SPECIAL_EQUAL_RELDOM
( check_equal_empty_set(A,Hyp,_) -> true
; check_not_equal_empty_set(B,Hyp,_) -> true
; check_equal(A,B,Hyp,_)). % implicit proof by case distinction
check_not_empty_set(total_relation(A,B),Hyp) :- !, % SIMP_SPECIAL_EQUAL_RELDOM
check_not_empty_set(total_function(A,B),Hyp).
check_not_empty_set(Expr,Hyps) :-
is_lambda_function_with_domain(Expr,Domain),!,
check_not_empty_set(Domain,Hyps).
check_not_empty_set('$'(ID),Hyps) :-
enumerated_set(ID),
\+ is_hyp_var(ID,Hyps),!. % global enumerated set visible
check_not_empty_set(Eq,Hyps) :-
(Eq='$'(_) ; Eq=interval(_,_)),
avl_fetch_equal_from_hyps(Eq,Hyps,Value,Hyps2),
rewrite_local_loop_check(Eq,check_not_empty_set,Value,Hyps2,Hyps3),
check_not_empty_set(Value,Hyps3),!.
check_not_empty_set(Seq,Hyp) :- infer_sequence_type_of_expr(Seq,Hyp,seq1),!.
check_not_empty_set(Func,Hyps) :- Func = '$'(_),
avl_fetch_binop_from_hyps(Func,member,Hyps,FunctionType,Hyps2), % Func : . --> .
check_not_empty_elements(FunctionType,Hyps2),!.
check_not_empty_set(function(Func2,_),Hyps) :-
get_range_or_superset(Func2,Hyps,Range,Hyps2),
check_not_empty_elements(Range,Hyps2),!.
check_not_empty_set(tail(A),Hyps) :- rewrite_card_of_set(A,Hyps,CardA,Hyps1),!,
check_leq(2,CardA,Hyps1).
check_not_empty_set(front(A),Hyps) :- rewrite_card_of_set(A,Hyps,CardA,Hyps1),!,
check_leq(2,CardA,Hyps1).
check_not_empty_set(A,Hyps) :-
avl_fetch_binop_from_hyps(A,not_subset_strict,Hyps,B,_), % A <<: {Single} <=> A={}
singleton_set(B,_),!.
check_not_empty_set(A,Hyps) :-
( Lookup = A, Operator = superset
;
(Lookup=domain(A) ; Lookup=range(A)),
(Operator = superset ; Operator = equal)
),
avl_fetch_binop_from_hyps(Lookup,Operator,Hyps,B,Hyps2), % B /= {} & B <: A => A /= {}
rewrite_local_loop_check(A,check_not_empty_set,B,Hyps2,Hyps3),
check_not_empty_set(B,Hyps3),!.
Calls:
Name: ! |
|
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: =/2 |
|
Name: singleton_set/2 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
Name: rewrite_card_of_set/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: get_range_or_superset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: is_hyp_var/2 |
Module: foo_error |
Name: not/1 |
|
Name: enumerated_set/1 |
Module: b_global_sets |
| Module: well_def_prover | |
Name: check_equal/4 |
Module: well_def_prover |
Name: true |
|
| Module: well_def_prover | |
Name: ->/3 |
|
Name: check_equal_empty_set/3 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_not_subset/4 |
Module: well_def_prover |
Name: \=/2 |
|
Name: ->/2 |
|
Name: avl_fetch_from_hyps/2 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: check_sub_intervals/5 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_not_equal/3 |
Module: well_def_prover |
| Module: well_def_prover |
check_not_equal(A,B,Hyp) :-
is_explicit_value(A,AV,Hyp), is_explicit_value(B,BV,Hyp), !, AV \= BV.
check_not_equal(X,Y,Hyp) :- sym_unify(X,Y,if_then_else(_,A1,A2),B),!,
(check_not_equal(A1,B,Hyp) -> check_not_equal(A2,B,Hyp)).
check_not_equal(N1,N2,Hyps) :-
avl_fetch_not_equal(N1,N2,Hyps),!.
check_not_equal(couple(A1,A2),couple(B1,B2),Hyps) :- !,
(check_not_equal(A1,B1,Hyps) -> true ; check_not_equal(A2,B2,Hyps)).
check_not_equal(X,B,Hyps) :- number(B),
try_get_set_of_possible_values(X,Hyps,SetX,Hyps2),
check_all_values_neq_nr(SetX,B,Hyps2),!.
check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,unary_minus(A),B),number(B),!, BM is -B,
check_not_equal(A,BM,Hyps).
check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,multiplication(A,B),0),!, % A*B /= 0 if A/=0 & B/=0
check_not_equal(A,0,Hyps),check_not_equal(B,0,Hyps).
check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,power_of(A,_),0),!, % A**B /= 0 if A/=0
check_not_equal(A,0,Hyps).
check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,Add,B),
add_with_number(Add,A,Nr),!,
(Nr>0 -> check_leq(B,A,Hyps) % A >= B => A+Nr > B => A+Nr /= B
; Nr=0 -> check_not_equal(A,B,Hyps)
; check_leq(A,B,Hyps)
).
check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,A,B),number(B),!,
B1 is B+1,
(check_leq(B1,A,Hyps) -> true % B < A
; B2 is B-1,
check_leq(A,B2,Hyps)). % A < B
check_not_equal(XX,YY,Hyps) :- sym_unify(XX,YY,'$'(A),B),
avl_fetch_binop_from_hyps('$'(A),less_equal,Hyps,Y,Hyps2),
(number(B) -> (B1 is B-1, check_leq(Y,B1,Hyps2) -> true)
; avl_fetch_not_equal('$'(A),Y,Hyps) % we have $(A) < Y => prove Y <= B
-> check_leq(Y,B,Hyps2) % we can prove x
).
check_not_equal(XX,YY,Hyps) :- sym_unify(XX,YY,'$'(A),B),
avl_fetch_binop_from_hyps('$'(A),greater_equal,Hyps,Y,Hyps2),
(number(B) -> (B1 is B+1, check_leq(B1,Y,Hyps2) -> true)
; avl_fetch_not_equal('$'(A),Y,Hyps) % we have $(A) < Y => prove Y <= B
-> check_leq(B,Y,Hyps2) % see comments above
).
check_not_equal(A,Empty,Hyp) :- is_empty_set_direct(Empty), !, check_not_empty_set(A,Hyp).
check_not_equal(Empty,A,Hyp) :- is_empty_set_direct(Empty), !, check_not_empty_set(A,Hyp).
check_not_equal(value(avl_set(A)),value(avl_set(B)),_) :- nonvar(A), nonvar(B),!, % nonvar should always be true
\+ equal_avl_tree(A,B).
check_not_equal(A,B,Hyps) :-
(A=set_extension(LA) -> check_not_equal_set_extension(B,LA,Hyps)
; B=set_extension(LB) -> check_not_equal_set_extension(A,LB,Hyps)).
check_not_equal(A,B,Hyps) :-
avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),!,
check_not_equal(Value,B,Hyps2).
check_not_equal(A,B,Hyps) :-
avl_fetch_worthwhile_equal_from_hyps(B,Hyps,Value,Hyps2),!,
check_not_equal(A,Value,Hyps2).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: ! |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: =/2 |
|
Name: ->/2 |
|
Name: ->/3 |
|
Name: equal_avl_tree/2 |
Module: custom_explicit_sets |
Name: not/1 |
|
Name: nonvar/1 |
|
Name: check_not_empty_set/2 |
Module: well_def_prover |
Name: is_empty_set_direct/1 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
Name: avl_fetch_not_equal/3 |
Module: well_def_prover |
Name: true |
|
Name: is/2 |
|
Name: number/1 |
|
| Module: well_def_prover | |
Name: sym_unify/4 |
Module: well_def_prover |
Name: >/2 |
|
Name: add_with_number/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: \=/2 |
|
Name: is_explicit_value/3 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_less/3 |
Module: well_def_prover |
Name: check_not_subset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: prove_po/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_is_subset_strict/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_leq/3 |
Module: well_def_prover |
check_not_equal_empty_set(Set,Hyps,not_equal_empty_set) :-
check_not_equal(Set,empty_set,Hyps).
Calls:
Name: check_not_equal/3 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: check_is_sequence/3 |
Module: well_def_prover |
Name: check_empty_set/3 |
Module: well_def_prover |
Name: check_not_empty_set/2 |
Module: well_def_prover |
| Module: well_def_prover |
check_not_equal_set_extension(set_extension([B|TB]),[A|TA],Hyps) :- (TA=[];TB=[]),!,
check_not_equal(A,B,Hyps). % TO DO: we can generalize this treatment to find one element in one set not in the other
check_not_equal_set_extension(value(avl_set(AVL)),LA,Hyps) :- length(LA,MaxSizeA),
(avl_size(AVL,Sze),Sze>MaxSizeA -> true % AVL has at least one element more
; is_one_element_avl(AVL,B), LA=[A|_], check_not_equal(A,B,Hyps)).
Calls:
Name: check_not_equal/3 |
Module: well_def_prover |
Name: =/2 |
|
Name: is_one_element_avl/2 |
Module: custom_explicit_sets |
Name: true |
|
Name: >/2 |
|
Name: avl_size/2 |
Module: foo_error |
Name: ->/3 |
|
Name: length/2 |
|
Name: ! |
Called:
Name: check_not_equal/3 |
Module: well_def_prover |
check_not_is_subset_strict(A,B,Hyps,hyp) :-
avl_fetch_from_hyps(not_subset_strict(A,B),Hyps),!. % hyp; currently not marked as useful by default!
check_not_is_subset_strict(A,B,Hyps,hyp2) :-
avl_fetch_from_hyps(not_subset(A,B),Hyps),!. % not(A <: B) => not (A<<:B)
check_not_is_subset_strict(A,B,Hyps,equal(PT)) :-
check_equal(A,B,Hyps,PT),!. % A=B => not (A<<:B)
check_not_is_subset_strict(_,B,Hyps,empty_set(PT)) :- % A /<<: {}
check_equal_empty_set(B,Hyps,PT).
check_not_is_subset_strict(MAX,_,Hyps,maximal_set) :- % MAX /<<: B
maximal_set(MAX,Hyps),!.
check_not_is_subset_strict(A,B,Hyps,not_empty_singleton(PT)) :- % x <<: {A} <=> x={}
singleton_set(B,_),!,
check_not_equal_empty_set(A,Hyps,PT).
check_not_is_subset_strict(A,B,Hyps,superset_eq1(PT)) :-
(Operator = equal ; Operator = superset), % A :> S2 & S2 /<<: B => A /<<: B
avl_fetch_binop_from_hyps(A,Operator,Hyps,S2,Hyps2),
rewrite_local_loop_check(A,check_not_is_subset_strict,S2,Hyps2,Hyps3),
check_not_is_subset_strict(S2,B,Hyps3,PT),!.
check_not_is_subset_strict(A,B,Hyps,subset_eq2(PT)) :-
(Operator = equal ; Operator = subset), % B <: S2 & A /<<: S2 => A /<<: B
avl_fetch_binop_from_hyps(B,Operator,Hyps,S2,Hyps2),
rewrite_local_loop_check(B,check_not_is_subset_strict,S2,Hyps2,Hyps3),
check_not_is_subset_strict(A,S2,Hyps3,PT),!.
Calls:
Name: ! |
|
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: =/2 |
|
| Module: well_def_prover | |
Name: singleton_set/2 |
Module: well_def_prover |
Name: maximal_set/2 |
Module: well_def_prover |
Name: check_equal_empty_set/3 |
Module: well_def_prover |
Name: check_equal/4 |
Module: well_def_prover |
Name: avl_fetch_from_hyps/2 |
Module: well_def_prover |
Called:
Name: check_not_subset/4 |
Module: well_def_prover |
Name: prove_po/3 |
Module: well_def_prover |
check_not_member_of_domain(domain_subtraction(DS,Func),El,Hyps,not_dom_sub(PT)) :-
(check_member_of_set(DS,El,Hyps,PT) -> true
; check_not_member_of_domain(Func,El,Hyps,PT)).
check_not_member_of_domain(domain_restriction(DS,Func),El,Hyps,not_dom_sub(PT)) :-
(check_not_member_of_set(DS,El,Hyps,PT) -> true
; check_not_member_of_domain(Func,El,Hyps,PT)).
check_not_member_of_domain(Func,El,Hyps,PT) :-
get_domain_or_superset(Func,Hyps,DomFunc,Hyps1),!,
check_not_member_of_set(DomFunc,El,Hyps1,PT).
Calls:
| Module: well_def_prover | |
Name: ! |
|
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: check_member_of_set/4 |
Module: well_def_prover |
Called:
| Module: well_def_prover |
check_not_member_of_list([],_,_).
check_not_member_of_list([H|T],El,Hyps) :-
check_not_equal(H,El,Hyps),
check_not_member_of_list(T,El,Hyps).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: check_not_equal/3 |
Module: well_def_prover |
Called:
| Module: well_def_prover |
check_not_member_of_range(range_subtraction(Func,DS),El,Hyps,not_dom_sub(PT)) :-
(check_member_of_set(DS,El,Hyps,PT) -> true
; check_not_member_of_range(Func,El,Hyps,PT)).
check_not_member_of_range(range_restriction(Func,DS),El,Hyps,not_dom_sub(PT)) :-
(check_not_member_of_set(DS,El,Hyps,PT) -> true
; check_not_member_of_range(Func,El,Hyps,PT)).
check_not_member_of_range(Func,El,Hyps,PT) :-
get_range_or_superset(Func,Hyps,RanFunc,Hyps1),!,
check_not_member_of_set(RanFunc,El,Hyps1,PT).
Calls:
| Module: well_def_prover | |
Name: ! |
|
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: check_member_of_set/4 |
Module: well_def_prover |
Called:
| Module: well_def_prover |
check_not_member_of_set(Set,_,Hyps,empty_set) :- check_equal_empty_set(Set,Hyps,_),!.
check_not_member_of_set(Set,El,Hyps,hyp) :-
avl_fetch_from_hyps(not_member(El,Set),Hyps),!. % hyp
check_not_member_of_set(if_then_else(_,A,B),El,Hyps,if_then_else(PTA,PTB)) :-
(check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!.
check_not_member_of_set(intersection(A,B),El,Hyps,inter(PT)) :-
(check_not_member_of_set(A,El,Hyps,PT) -> true ; check_not_member_of_set(B,El,Hyps,PT)),!.
check_not_member_of_set(set_subtraction(A,B),El,Hyps,inter(PT)) :-
(check_not_member_of_set(A,El,Hyps,PT) -> true ; check_member_of_set(B,El,Hyps,PT)),!.
check_not_member_of_set(union(A,B),El,Hyps,inter(PTA,PTB)) :-
(check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!.
check_not_member_of_set(overwrite(A,B),El,Hyps,overwrite(PTA,PTB)) :-
(check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!.
check_not_member_of_set('NATURAL1',El,Hyps,nat1) :-
check_leq(El,0,Hyps).
check_not_member_of_set('NATURAL',El,Hyps,nat1) :-
check_leq(El,-1,Hyps).
check_not_member_of_set(interval(From,To),El,Hyps,interval) :-
(check_leq(El,minus(From,1),Hyps) -> true
; check_leq(add(To,1),El,Hyps) -> true). % TODO: or interval empty
check_not_member_of_set(domain(Func),El,Hyps,not_in_domain(PT)) :-
check_not_member_of_domain(Func,El,Hyps,PT),!.
check_not_member_of_set(range(Func),El,Hyps,not_in_range(PT)) :-
check_not_member_of_range(Func,El,Hyps,PT),!.
check_not_member_of_set(Set,couple(From,_),Hyps,not_in_dom(PT)) :-
% x /: dom(f) => x|->y /: f
avl_fetch_binop_from_hyps(From,not_member,Hyps,Set2,Hyps2),
check_is_subset(domain(Set),Set2,Hyps2,PT),
!.
check_not_member_of_set(Set,couple(_,To),Hyps,not_in_range) :-
avl_fetch_from_hyps(not_member(To,range(Set)),Hyps), % y /: ran(f) => x|->y /: f
!. % TODO: generalise this rule somewhat, see domain above
check_not_member_of_set(A,El,Hyps,eq(ProofTree)) :-
avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),
rewrite_local_loop_check(A,check_member_of_set,Value,Hyps2,Hyps3),
check_not_member_of_set(Value,El,Hyps3,ProofTree).
check_not_member_of_set(Set,El,Hyps,not_in_set_extension) :-
is_set_extension(Set,List),
check_not_member_of_list(List,El,Hyps).
Calls:
| Module: well_def_prover | |
Name: is_set_extension/2 |
Module: well_def_prover |
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ! |
|
Name: avl_fetch_from_hyps/2 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: true |
|
Name: check_leq/3 |
Module: well_def_prover |
Name: ->/2 |
|
Name: ->/3 |
|
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_equal_empty_set/3 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: prove_po/3 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
check_not_subset(A,B,Hyps,PT) :-
check_not_is_subset_strict(A,B,Hyps,PT),!,
check_not_equal(A,B,Hyps).
Calls:
Name: check_not_equal/3 |
Module: well_def_prover |
Name: ! |
|
| Module: well_def_prover |
Called:
Name: prove_po/3 |
Module: well_def_prover |
Name: check_not_empty_set/2 |
Module: well_def_prover |
check_set_ext_pf([],_,_).
check_set_ext_pf([couple(Next,_)|TS],Last,Hyp) :-
Next \= Last,
check_set_ext_pf(TS,Next,Hyp).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: \=/2 |
Called:
| Module: well_def_prover |
check_set_extension_is_partial_function([_],_) :- !. % one element set extension is a function
check_set_extension_is_partial_function(List,Hyps) :-
maplist(get_explicit_dom_value(Hyps),List,VList),!,
sort(VList,SList),
SList = [couple(First,_)|TS],
check_set_ext_pf(TS,First,Hyps).
check_set_extension_is_partial_function([couple(A,_),couple(B,_)],Hyps) :-
check_not_equal(A,B,Hyps). % TO DO: all_different for longer lists
Calls:
Name: check_not_equal/3 |
Module: well_def_prover |
Name: check_set_ext_pf/3 |
Module: well_def_prover |
Name: =/2 |
|
Name: sort/2 |
|
Name: ! |
|
Name: maplist/3 |
Module: foo_error |
Called:
| Module: well_def_prover |
check_some_finite(sorted_set_extension(L),Hyps,PT) :- !, check_some_finite(set_extension(L),Hyps,PT).
check_some_finite(set_extension(L),Hyps,set_extension(PT)) :-
(member(Val,L), check_finite(Val,Hyps,PT) -> true).
check_some_finite('$'(ID),Hyps,rewrite_id(ID,PT)) :-
(Operator = equal ; Operator = superset), % Note: superset not subset as for check_all_finite
avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2),
not_occurs(Set2,ID), % avoid silly, cyclic rewrites
rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3),
check_some_finite(Set2,Hyps3,PT),!.
check_some_finite(union(A,B),Hyps,union(PT)) :-
(check_some_finite(A,Hyps,PT) -> true ; check_some_finite(B,Hyps,PT)).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: ! |
|
| Module: well_def_prover | |
Name: not_occurs/2 |
Module: foo_error |
| Module: well_def_prover | |
Name: =/2 |
|
Name: check_finite/3 |
Module: well_def_prover |
Name: member/2 |
|
Name: ->/2 |
Called:
Name: check_finite/3 |
Module: well_def_prover |
check_sub_intervals(L1,L1,L2,U2,Hyps) :- (L1=L2 ; L1=U2),!,
check_not_empty_set(interval(L2,U2),Hyps).
check_sub_intervals(L1,U1,L2,U2,Hyps) :- % L1..U1 <: L2..U2 if L2 <= L1 & U1 <= U2
check_leq(L2,L1,Hyps),!,
check_leq(U1,U2,Hyps).
Calls:
Name: check_leq/3 |
Module: well_def_prover |
Name: ! |
|
Name: check_not_empty_set/2 |
Module: well_def_prover |
Name: =/2 |
Called:
Name: check_subset_interval/5 |
Module: well_def_prover |
check_subset_avl(union(A,B),AVL1,Hyps) :- !, % TO DO: try and merge A,B
(check_subset_avl(A,AVL1,Hyps) -> true ; check_subset_avl(B,AVL1,Hyps)).
check_subset_avl(intersection(A,B),AVL1,Hyps) :- !, % AVL <: A /\ B if AVL <: A & AVL <: B
(check_subset_avl(A,AVL1,Hyps) -> check_subset_avl(B,AVL1,Hyps)).
check_subset_avl(interval(L2,U2),AVL,_) :- number(L2),number(U2),!,
check_avl_in_interval(AVL,L2,U2).
check_subset_avl(value(avl_set(AVL2)),AVL1,_) :- !, check_avl_subset(AVL1,AVL2).
check_subset_avl(seq(MAX),AVL,Hyps) :- maximal_set(MAX,Hyps), !, is_avl_set_of_sequences(AVL,seq).
check_subset_avl(seq1(MAX),AVL,Hyps) :- maximal_set(MAX,Hyps), !, is_avl_set_of_sequences(AVL,seq1).
check_subset_avl(seq(seq(MAX)),AVL,Hyps) :- maximal_set(MAX,Hyps),
% comes from general concat
custom_explicit_sets:is_one_element_avl(AVL,Element), % usually one value from try_get_set_of_possible_values
is_sequence(Element,seq),
expand_custom_set_to_list(Element,ListOfSeqs),
maplist(is_subsequence,ListOfSeqs).
check_subset_avl(A,AVL,Hyps) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!,
check_subset_avl(A2,AVL,Hyps2).
check_subset_avl(A,AVL,Hyps) :-
avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A2,Hyps2),
rewrite_local_loop_check(A,check_subset_avl,A2,Hyps2,Hyps3),
check_subset_avl(A2,AVL,Hyps3).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ! |
|
| Module: well_def_prover | |
Name: maplist/2 |
Module: foo_error |
| Module: custom_explicit_sets | |
Name: is_sequence/2 |
Module: well_def_prover |
Name: is_one_element_avl/2 |
Module: custom_explicit_sets |
Name: maximal_set/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_avl_subset/2 |
Module: custom_explicit_sets |
Name: check_avl_in_interval/3 |
Module: custom_explicit_sets |
Name: number/1 |
|
Name: ->/2 |
|
Name: true |
|
Name: ->/3 |
Called:
Name: check_is_subset/4 |
Module: well_def_prover |
check_subset_interval(union(A,B),L1,U1,Hyps,union(PT)) :- !,
% TO DO: try and merge A,B : union(interval(1,10),set_extension([11]))
(check_subset_interval(A,L1,U1,Hyps,PT) -> true ; check_subset_interval(B,L1,U1,Hyps,PT)).
check_subset_interval(sorted_set_extension(L),L1,U1,Hyps,PT) :- !,
check_subset_interval(set_extension(L),L1,U1,Hyps,PT).
check_subset_interval(set_extension(L),L1,U1,Hyps,set_extension(Nr)) :- !,
% TO DO: maybe merge L into an interval
nth1(Nr,L,El), check_sub_intervals(L1,U1,El,El,Hyps),!.
check_subset_interval(intersection(A,B),L1,U1,Hyps,inter(PTA,PTB)) :- !,
% L1..U1 <: A /\ B if L1..U1 <: A & L1..U1 <: B
(check_subset_interval(A,L1,U1,Hyps,PTA) -> check_subset_interval(B,L1,U1,Hyps,PTB)).
check_subset_interval(interval(L2,U2),L1,U1,Hyps,interval) :-
!,check_sub_intervals(L1,U1,L2,U2,Hyps).
check_subset_interval('NATURAL',L1,_,Hyps,nat) :- !, check_leq(0,L1,Hyps).
check_subset_interval('NATURAL1',L1,_,Hyps,nat1) :- !, check_leq(1,L1,Hyps).
check_subset_interval(value(avl_set(A)),L1,U1,Hyps,avl(PT)) :- !,
(number(L1), number(U1)
-> PT=in(L1,U1),
check_interval_in_custom_set(L1,U1,avl_set(A),no_wf_available)
; avl_min(A,int(L2)), avl_max(A,int(U2)), PT=min_max(L2,U2,PT2),
check_subset_interval(interval(L2,U2),L1,U1,Hyps,PT2)
).
check_subset_interval(A,L1,U1,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!,
check_subset_interval(A2,L1,U1,Hyps2,PT).
check_subset_interval(domain(Expr),Low,Up,Hyps,dom_seq1) :- % a special rule when using SEQ(1) rather than first(SEQ)
(check_leq(1,Low,Hyps), check_leq(Up,size(Expr),Hyps) % 1..size(s) <: dom(s)
-> check_is_sequence(Expr,Hyps)
; index_in_non_empty_sequence(Low,Expr,Hyps),
index_in_non_empty_sequence(Up,Expr,Hyps) % 1..1 or size(s)..size(s) <: dom(s) if s:seq1(.)
-> check_is_non_empty_sequence(Expr,Hyps)
).
check_subset_interval(range(reverse(Expr)),Low,Up,Hyps,PT) :- !,
check_subset_interval(domain(Expr),Low,Up,Hyps,PT).
check_subset_interval(A,Low,Up,Hyps,eq(PT)) :-
avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A2,Hyps2),
rewrite_local_loop_check(A,check_subset_interval,A2,Hyps2,Hyps3),
check_subset_interval(A2,Low,Up,Hyps3,PT).
Calls:
Name: RECURSIVE_CALL/5 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ! |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ->/2 |
|
Name: check_is_sequence/2 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
Name: ->/3 |
|
| Module: well_def_prover | |
Name: =/2 |
|
Name: avl_max/2 |
Module: foo_error |
Name: avl_min/2 |
Module: foo_error |
| Module: custom_explicit_sets | |
Name: number/1 |
|
Name: check_sub_intervals/5 |
Module: well_def_prover |
Name: nth1/3 |
Module: foo_error |
Name: true |
Called:
Name: check_in_interval/5 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
compute_card_of_set(empty_set,Hyps,0,Hyps).
compute_card_of_set(empty_sequence,Hyps,0,Hyps).
compute_card_of_set(bool_set,Hyps,2,Hyps).
compute_card_of_set(interval(L,U),Hyps,Size,Hyps) :- number(L), number(U), Size is U+1-L.
compute_card_of_set(value(Val),Hyps,Size,Hyps) :- get_set_val_size(Val,Size).
compute_card_of_set(sequence_extension(List),Hyps,Size,Hyps) :- length(List,Size).
compute_card_of_set(set_extension([_]),Hyps,Size,Hyps) :- Size=1. % to do check if all elements definitely different
compute_card_of_set(sorted_set_extension([_]),Hyps,Size,Hyps) :- Size=1. % ditto
compute_card_of_set(rev(A),Hyps,Size,Hyps2) :- !, compute_card_of_set(A,Hyps,Size,Hyps2).
compute_card_of_set(front(A),Hyps,Size,Hyps2) :- !, compute_card_of_set(tail(A),Hyps,Size,Hyps2).
compute_card_of_set(tail(A),Hyps,Size,Hyps2) :- !,
compute_card_of_set(A,Hyps,Size1,Hyps2), number(Size1), Size1>0,
Size is Size1-1.
compute_card_of_set(concat(A,B),Hyps,Size,Hyps2) :-
compute_card_of_set(A,Hyps,SA,Hyps1),!,
compute_card_of_set(B,Hyps1,SB,Hyps2),
Size is SA+SB.
compute_card_of_set('$'(ID),Hyps,Size,Hyps) :- is_enumerated_set(ID,Hyps),
!,
b_global_set_cardinality(ID,Size).
compute_card_of_set('$'(ID),Hyps,Size,Hyps2) :-
avl_fetch_equal_from_hyps('$'(ID),Hyps,X2,Hyps1),
compute_card_of_set(X2,Hyps1,Size,Hyps2),!.
compute_card_of_set('$'(ID),Hyps,Size,Hyps4) :- % e.g., f:1..10 --> BOOL --> card(f) = 10
avl_fetch_binop_from_hyps('$'(ID),member,Hyps,FunctionType,Hyps1),
is_partial_function_type(FunctionType,Hyps1,Hyps2),
get_exact_domain_of_func_or_rel_type(FunctionType,Hyps2,Dom,Hyps3),
compute_card_of_set(Dom,Hyps3,Size,Hyps4).
Calls:
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ! |
|
| Module: well_def_prover | |
| Module: b_global_sets | |
Name: is_enumerated_set/2 |
Module: well_def_prover |
Name: is/2 |
|
Name: >/2 |
|
Name: number/1 |
|
Name: =/2 |
|
Name: length/2 |
|
Name: get_set_val_size/2 |
Module: well_def_prover |
Called:
Name: rewrite_card_of_set/4 |
Module: well_def_prover |
Name: rewrite_integer/4 |
Module: well_def_prover |
| Module: well_def_prover |
compute_exact_domain(reverse(Func),Hyps,Res,Hyps2) :- !,
compute_exact_range(Func,Hyps,Res,Hyps2).
compute_exact_domain(rev(Func),Hyps,Res,Hyps2) :- !, % reverse of a sequence; domain identical
compute_exact_domain(Func,Hyps,Res,Hyps2).
compute_exact_domain(identity(Domain),Hyps,Res,Hyps2) :- !, Hyps2=Hyps, Res=Domain.
compute_exact_domain(restrict_front(_Seq,N),Hyps,Res,Hyps2) :- !,
% WD Condition requires N : 0..size(Seq)
Hyps2=Hyps, Res = interval(1,N). % TODO: similar rule for restrict_tail
compute_exact_domain(Func,Hyps,Res,Hyps2) :-
compute_exact_domain_direct(Func,Hyps,Res,Hyps2),!. % No recursive application of equal or hyp
compute_exact_domain(Func,Hyps,Domain,Hyps2) :-
avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
compute_exact_domain(Func2,Hyps1,Domain,Hyps2).
Calls:
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: ! |
|
| Module: well_def_prover | |
Name: =/2 |
|
Name: compute_exact_range/4 |
Module: well_def_prover |
Called:
Name: check_domain_disjoint/4 |
Module: well_def_prover |
Name: compute_exact_range/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover |
compute_exact_domain_direct(Func,Hyps,Res,Hyps2) :-
avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1), % look for Func : Res --> Range ; e.g. Func:perm(1..10) -> DomSet=1..10
% f : _ +-> ( Dom --> _ ) & x:Dom ==> x:dom(f(_))
% f : _ +-> ( Dom --> _ ) => dom(f(_)) = Dom
get_exact_domain_of_func_or_rel_type(Function,Hyps1,Res,Hyps2),!. % is thus also minimal domain
compute_exact_domain_direct(Func,Hyps,Res,Hyps3) :- Func = '$'(_), % Look for Func = Value definition
avl_fetch_equal_from_hyps(Func,Hyps,Value,Hyps2),
compute_exact_domain(Value,Hyps2,Res,Hyps3).
compute_exact_domain_direct(value(CS),Hyps,value(Res),Hyps) :- !, nonvar(CS),
domain_of_explicit_set_wf(CS,Res,no_wf_available).
compute_exact_domain_direct(overwrite(F1,F2),Hyps,D12,Hyps2) :- !, % dom(F1 <+ F2) = dom(F1) \/ dom(F2)
compute_exact_domain(F1,Hyps,D1,Hyps1), compute_exact_domain(F2,Hyps1,D2,Hyps2),
construct_union(D1,D2,Hyps2,D12).
compute_exact_domain_direct(domain_restriction(S,F),Hyps,intersection(S,D),Hyps2) :- !, % dom(S <| F) = S /\ dom(F)
compute_exact_domain(F,Hyps,D,Hyps2).
compute_exact_domain_direct(domain_subtraction(S,F),Hyps,set_subtraction(D,S),Hyps2) :- !, % dom(S <<| F) = dom(F) - S
compute_exact_domain(F,Hyps,D,Hyps2).
compute_exact_domain_direct(direct_product(F,G),Hyps,intersection(DF,DG),Hyps2) :- !, % dom(F>
compute_exact_domain(F,Hyps,DF,Hyps1),
compute_exact_domain(G,Hyps1,DG,Hyps2).
compute_exact_domain_direct(composition(F1,F2),Hyps,Domain,Hyps4) :- !, % dom((F1;F2)) = dom(F1) if ran(F1) <: dom(F2)
compute_exact_domain(F1,Hyps,Domain,Hyps2),
compute_exact_domain(F2,Hyps2,D2,Hyps3), % or_subset would also be ok
(maximal_set(D2,Hyps3) -> Hyps4=Hyps3
; get_range_or_superset(F1,Hyps3,R1,Hyps4),
check_is_subset(R1,D2,Hyps4,_PT)
).
compute_exact_domain_direct(union(F,G),Hyps,UnionDFDG,Hyps2) :- !, % dom(F \/ G) = dom(F) \/ dom(G)
compute_exact_domain(F,Hyps,DF,Hyps1),
compute_exact_domain(G,Hyps1,DG,Hyps2),
construct_union(DF,DG,Hyps2,UnionDFDG).
compute_exact_domain_direct(sorted_set_extension(List),Hyps,Res,Hyps2) :- !,
compute_exact_domain_direct(set_extension(List),Hyps,Res,Hyps2).
compute_exact_domain_direct(set_extension(List),Hyps,Res,Hyps) :- !, maplist(get_dom_el,List,Domain),
construct_set_extension(Domain,Hyps,Res).
compute_exact_domain_direct(Expr,Hyps,Domain,Hyps) :- is_lambda_function_with_domain(Expr,Domain),!.
compute_exact_domain_direct(Func,Hyps,Domain,Hyps2) :-
avl_fetch_equal_from_hyps(domain(Func),Hyps,Domain,Hyps2).
Calls:
| Module: well_def_prover | |
Name: ! |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: maplist/3 |
Module: foo_error |
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: construct_union/4 |
Module: well_def_prover |
Name: compute_exact_domain/4 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: =/2 |
|
Name: maximal_set/2 |
Module: well_def_prover |
Name: ->/3 |
|
| Module: custom_explicit_sets | |
Name: nonvar/1 |
|
| Module: well_def_prover | |
| Module: well_def_prover |
Called:
Name: compute_exact_domain/4 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
compute_exact_range(reverse(Func),Hyps,Res,Hyps2) :-
compute_exact_domain(Func,Hyps,Res,Hyps2).
compute_exact_range(rev(Func),Hyps,Res,Hyps2) :- % reverse of a sequence: same range
compute_exact_range(Func,Hyps,Res,Hyps2).
compute_exact_range(identity(Domain),Hyps,Res,Hyps2) :- !, Hyps2=Hyps, Res=Domain.
compute_exact_range(Func,Hyps,Res,Hyps2) :-
compute_exact_range_direct(Func,Hyps,Res,Hyps2),!. % No recursive application of equal or hyp
compute_exact_range(Func,Hyps,Res,Hyps2) :- Func = '$'(_),
avl_fetch_mem_or_struct(Func,Hyps,FunctionType,Hyps2), % Func : _ --> Res
get_exact_range_of_func_type_direct(FunctionType,Res).
compute_exact_range(Func,Hyps,Range,Hyps2) :-
avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
compute_exact_range(Func2,Hyps1,Range,Hyps2).
Calls:
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: =/2 |
|
Name: ! |
|
| Module: well_def_prover | |
Name: compute_exact_domain/4 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: compute_exact_domain/4 |
Module: well_def_prover |
| Module: well_def_prover |
compute_exact_range_direct(S,Hyps,empty_set,Hyps) :- is_empty_set_direct(S),!.
compute_exact_range_direct(function(Func2,_),Hyps,Res,Hyps2) :-
% f : _ +-> ( _ --> Ran ) & x:Ran ==> x:ran(f(_))
% f : _ +-> ( _ -->> Ran ) => ran(f(_)) = Ran
get_range_or_superset(Func2,Hyps,Range,Hyps2),
get_exact_range_of_func_type_direct(Range,Res). % is thus also minimal domain
compute_exact_range_direct(value(CS),Hyps,value(Res),Hyps) :- !, nonvar(CS), % TO DO: maybe only if small enough
range_of_explicit_set_wf(CS,Res,no_wf_available).
compute_exact_range_direct(sequence_extension(L),Hyps,Res,Hyps) :- !,
construct_set_extension(L,Hyps,Res).
compute_exact_range_direct(union(F,G),Hyps,UnionRFRG,Hyps2) :- !, % ran(F \/ G) = ran(F) \/ ran(G)
compute_exact_range(F,Hyps,RF,Hyps1),
compute_exact_range(G,Hyps1,RG,Hyps2),
construct_union(RF,RG,Hyps2,UnionRFRG).
compute_exact_range_direct(sorted_set_extension(List),Hyps,Res,Hyps2) :- !,
compute_exact_range_direct(set_extension(List),Hyps,Res,Hyps2).
compute_exact_range_direct(set_extension(List),Hyps,Res,Hyps) :- !, maplist(get_ran_el,List,Domain),
construct_set_extension(Domain,Hyps,Res).
compute_exact_range_direct(Func,Hyps,Range,Hyps2) :-
avl_fetch_equal_from_hyps(range(Func),Hyps,Range,Hyps2).
Calls:
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: maplist/3 |
Module: foo_error |
Name: ! |
|
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: construct_union/4 |
Module: well_def_prover |
Name: compute_exact_range/4 |
Module: well_def_prover |
| Module: custom_explicit_sets | |
Name: nonvar/1 |
|
| Module: well_def_prover | |
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: is_empty_set_direct/1 |
Module: well_def_prover |
Called:
Name: compute_exact_range/4 |
Module: well_def_prover |
Name: get_range_or_superset/4 |
Module: well_def_prover |
compute_integer(A,H,A,H) :- number(A),!.
compute_integer(A,H,Res,H2) :- rewrite_integer(A,H,Res,H2).
Calls:
Name: rewrite_integer/4 |
Module: well_def_prover |
Name: ! |
|
Name: number/1 |
Called:
Name: rewrite_integer/4 |
Module: well_def_prover |
conj_to_list(conjunct(A,B)) --> !, conj_to_list(A),conj_to_list(B).
conj_to_list(X) --> [X].
Calls:
Name: =/2 |
|
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: ! |
Called:
| Module: well_def_prover |
construct_set_extension([],_,Res) :- !, Res=empty_set.
construct_set_extension(L,Hyps,Res) :- maximal_set_extension(L,Hyps),!, Res='typeset'.
construct_set_extension(L,_,sorted_set_extension(SL)) :-
%length(L,Len), format('Construct set_extension ~w~n',[Len]),
sort(L,SL).
Calls:
Name: sort/2 |
|
Name: =/2 |
|
Name: ! |
|
Name: maximal_set_extension/2 |
Module: well_def_prover |
Called:
Name: construct_union/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover |
construct_union(empty_set,B,_Hyps,Res) :- !,Res=B.
construct_union(set_extension(A),set_extension(B),Hyps,Res) :- !,
append(A,B,AB),
construct_set_extension(AB,Hyps,Res).
construct_union(A,empty_set,_,Res) :- !,Res=A.
construct_union(A,B,_,union(A,B)).
Calls:
Name: =/2 |
|
Name: ! |
|
| Module: well_def_prover | |
Name: append/3 |
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: get_range_or_superset/4 |
Module: well_def_prover |
| Module: well_def_prover |
create_cartesian_product([Type],Res) :- !, Res=Type.
create_cartesian_product([Type|T],Res) :- create_cartesian_product3(T,Type,Res).
Calls:
| Module: well_def_prover | |
Name: =/2 |
|
Name: ! |
Called:
| Module: well_def_prover |
create_cartesian_product3([],Res,Res).
create_cartesian_product3([Type|T],Acc,Res) :-
create_cartesian_product3(T,cartesian_product(Acc,Type),Res).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Called:
| Module: well_def_prover |
create_intersection([],typeset). % no constraints on identifier: use typeset
create_intersection([A],Res) :- !, Res=A.
create_intersection([A|T],intersection(A,Rest)) :- create_intersection(T,Rest).
Calls:
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
Name: =/2 |
|
Name: ! |
Called:
Name: get_argument_types/4 |
Module: well_def_prover |
decompose_floor(Nr,A,B) :- number(Nr),!,
A is Nr div 2, B=A. % -11 div 2 -> -6, -1 div 2 = -1, 11 div 2 = 5
decompose_floor(add(A,B),A,B). % TO DO: we could try other order
decompose_floor(Mul,A,A) :- mul_with_number(Mul,A,Nr), Nr>=2. % we could divide Nr by 2
Calls:
Name: >=/2 |
|
Name: mul_with_number/3 |
Module: well_def_prover |
Name: =/2 |
|
Name: is/2 |
|
Name: ! |
|
Name: number/1 |
Called:
Name: check_leq/3 |
Module: well_def_prover |
extract_element_super_set_type(FuncType,Hyps,cartesian_product(A,B)) :-
get_possible_domain_of_func_or_rel_type(FuncType,Hyps,A,_),!,
get_possible_range_of_func_or_rel_type_direct(FuncType,B,_).
extract_element_super_set_type(fin_subset(A),_,A).
extract_element_super_set_type(fin1_subset(A),_,A).
extract_element_super_set_type(pow_subset(A),_,A).
extract_element_super_set_type(pow1_subset(A),_,A).
Calls:
| Module: well_def_prover | |
Name: ! |
|
| Module: well_def_prover |
Called:
Name: check_is_subset/4 |
Module: well_def_prover |
finite_comprehension_set(Paras,Body,Hyp) :-
% first exclude the parameters which can be proven finite on their own
% now deal with the rest; we do not pass AllParas as second arg; as all references to excluded IDs is ok (only finitely many values possible)
finite_comprehension_set_rest(Paras,Body,Hyp,[],Rest),
Rest \= Paras,
finite_comprehension_set_rest(Rest,Body,Hyp,[],[]). % do a second pass, e.g., for {x,y|x:{y,y+1} & y:1..2 & x:INTEGER}
Calls:
| Module: well_def_prover | |
Name: \=/2 |
Called:
Name: check_finite/3 |
Module: well_def_prover |
finite_comprehension_set_rest([],_,_,_,[]).
finite_comprehension_set_rest([ParaID1|TID],Body,Hyp,UnProven,Rest) :-
get_parameter_superset_in_body(ParaExpr,[ParaID1|TID],Body,Values),
l_not_occurs(Values,UnProven), % do not rely on not yet finitely proven paras; e.g. for {x,y|x:INTEGER & y=x}
match_parameter(ParaExpr,ParaID1),
check_finite(Values,Hyp,_PT),!,
finite_comprehension_set_rest(TID,Body,Hyp,UnProven,Rest).
finite_comprehension_set_rest([ParaID1|TID],Body,Hyp,UnProven,[ParaID1|Rest]) :-
finite_comprehension_set_rest(TID,Body,Hyp,[ParaID1|UnProven],Rest).
Calls:
Name: RECURSIVE_CALL/5 |
Module: well_def_prover |
Name: ! |
|
Name: check_finite/3 |
Module: well_def_prover |
Name: match_parameter/2 |
Module: well_def_prover |
Name: l_not_occurs/2 |
Module: well_def_prover |
| Module: well_def_prover |
Called:
| Module: well_def_prover |
finite_domain('$'(ID),Hyps,finite_type) :-
get_hyp_var_type(ID,Hyps,Type),
is_set_type(Type,couple(DomType,_)),
is_finite_type_for_wd(DomType,Hyps),!.
finite_domain(domain_restriction(A,Rel),Hyps,domain_restriction(PT)) :- !,
(check_finite(A,Hyps,PT) -> true ; finite_domain(Rel,Hyps,PT)).
finite_domain(A,Hyp,PT) :- get_domain_or_superset(A,Hyp,DA,Hyp2),!, check_finite(DA,Hyp2,PT).
Calls:
Name: check_finite/3 |
Module: well_def_prover |
Name: ! |
|
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: is_finite_type_for_wd/2 |
Module: foo_error |
Name: is_set_type/2 |
Module: bsyntaxtree |
Name: get_hyp_var_type/3 |
Module: foo_error |
Called:
Name: check_finite/3 |
Module: well_def_prover |
finite_range('$'(ID),Hyps,finite_type) :-
get_hyp_var_type(ID,Hyps,Type),
is_set_type(Type,couple(_,RanType)),
is_finite_type_for_wd(RanType,Hyps),!.
finite_range(A,Hyp,PT) :- get_range_or_superset(A,Hyp,RA,Hyp2),!, check_finite(RA,Hyp2,PT).
Calls:
Name: check_finite/3 |
Module: well_def_prover |
Name: ! |
|
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: is_finite_type_for_wd/2 |
Module: foo_error |
Name: is_set_type/2 |
Module: bsyntaxtree |
Name: get_hyp_var_type/3 |
Module: foo_error |
Called:
Name: check_finite/3 |
Module: well_def_prover |
function_restriction(domain_subtraction(_,F),F).
function_restriction(domain_restriction(_,F),F).
function_restriction(range_subtraction(F,_),F).
function_restriction(range_restriction(F,_),F).
function_restriction(set_subtraction(F,_),F).
Called:
| Module: well_def_prover | |
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
generate_funapp_binding(['$'(X)],El,[rename(X,El)]).
generate_funapp_binding(['$'(X),'$'(Y)],couple(El1,El2),[rename(X,El1),rename(Y,El2)]).
generate_funapp_binding(['$'(X),'$'(Y),'$'(Z)],couple(couple(El1,El2),El3),[rename(X,El1),rename(Y,El2),rename(Z,El3)]).
Called:
Name: check_member_of_domain/4 |
Module: well_def_prover |
get_argument_types([],_,[],[]). % no other conjuncts remain in body
get_argument_types(['$'(ID1)|T],AllArgs,BodyList,[Set1|TS]) :-
map_split_list(typing_predicate_for(ID1,AllArgs),BodyList,TypingSetList,RestBody),
create_intersection(TypingSetList,Set1),
get_argument_types(T,AllArgs,RestBody,TS).
Calls:
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: create_intersection/2 |
Module: well_def_prover |
Name: map_split_list/4 |
Module: tools |
Called:
| Module: well_def_prover |
get_domain_or_superset(reverse(Func),Hyps,Res,Hyps2) :- !,
get_range_or_superset(Func,Hyps,Res,Hyps2).
get_domain_or_superset(Func,Hyps,Res,Hyps3) :-
compute_exact_domain_direct(Func,Hyps,Res,Hyps2),
rewrite_local_loop_check(Func,get_domain_or_superset,Res,Hyps2,Hyps3),
!.
get_domain_or_superset(domain_restriction(A,_),Hyps,Res,Hyps) :- Res=A. % in case compute_exact_domain_direct fails
get_domain_or_superset(Func,Hyps,Res,Hyps1) :-
function_restriction(Func,LargerFunc),
get_domain_or_superset(LargerFunc,Hyps,Res,Hyps1).
get_domain_or_superset(direct_product(A,B),Hyps,Res,Hyps2) :- % dom(A >< B) = dom(A) /\ dom (B)
(get_domain_or_superset(A,Hyps,Res,Hyps2) -> true
; get_domain_or_superset(B,Hyps,Res,Hyps2) -> true).
get_domain_or_superset(Func,Hyps,DomSet,Hyps2) :- simple_value(Func),
avl_fetch_mem_or_struct(Func,Hyps,FunctionType,Hyps1),
get_domain_or_superset_of_func_or_rel_type(FunctionType,Hyps1,DomSet,Hyps2).
get_domain_or_superset(Func,Hyps,Domain,Hyps2) :-
avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
get_domain_or_superset(Func2,Hyps1,Domain,Hyps2).
get_domain_or_superset(Func,Hyps,DomSuperSet,Hyps2) :-
avl_fetch_binop_from_hyps(domain(Func),subset,Hyps,DomSuperSet,Hyps2).
Calls:
| Module: well_def_prover | |
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: simple_value/1 |
Module: well_def_prover |
Name: true |
|
Name: ->/2 |
|
Name: ->/3 |
|
Name: function_restriction/2 |
Module: well_def_prover |
Name: =/2 |
|
Name: ! |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: get_range_or_superset/4 |
Module: well_def_prover |
Called:
Name: finite_domain/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_domain_disjoint/4 |
Module: well_def_prover |
Name: get_type2/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: check_disjoint_aux/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_is_subset/4 |
Module: well_def_prover |
get_domain_or_superset_of_func_or_rel_type(sorted_set_extension(List),Hyps,Dom,Hyps2) :- !,
get_domain_or_superset_of_func_or_rel_type(set_extension(List),Hyps,Dom,Hyps2).
get_domain_or_superset_of_func_or_rel_type(set_extension(List),Hyps,Dom,Hyps2) :- !,
% if we have f: {f1,f2,...} => dom(f) <: dom(f1) \/ dom(f2) \/ ...
merge_possible_domains_of_list(List,Hyps,empty_set,Dom,Hyps2).
get_domain_or_superset_of_func_or_rel_type(Func,Hyps,Res,Hyps) :-
get_possible_domain_of_func_or_rel_type(Func,Hyps,D,_),!,Res=D.
Calls:
Name: =/2 |
|
Name: ! |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Called:
Name: get_domain_or_superset/4 |
Module: well_def_prover |
get_exact_domain_of_func_or_rel_type(FunType,Hyps,A,Hyps) :-
get_possible_domain_of_func_or_rel_type(FunType,Hyps,A,exact),!.
get_exact_domain_of_func_or_rel_type(FunType,Hyps,Domain,Hyps2) :-
avl_fetch_worthwhile_equal_from_hyps(FunType,Hyps,FunType2,Hyps1), % in case we have a definition like X = 1..n --> R
get_exact_domain_of_func_or_rel_type(FunType2,Hyps1,Domain,Hyps2).
get_exact_domain_of_func_or_rel_type(sorted_set_extension(F),Hyps,Domain,Hyps2) :- !,
get_exact_domain_of_func_or_rel_type(set_extension(F),Hyps,Domain,Hyps2).
get_exact_domain_of_func_or_rel_type(set_extension([Func|TF]),Hyps,Domain,Hyps2) :-
compute_exact_domain(Func,Hyps,Domain,Hyps2), % now check that all other functions have the same domain
(member(Func2,TF), \+ compute_exact_domain(Func2,Hyps2,Domain,_) -> fail
; true).
Calls:
Name: true |
|
Name: fail |
|
Name: compute_exact_domain/4 |
Module: well_def_prover |
Name: not/1 |
|
Name: member/2 |
|
Name: ->/3 |
|
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: ! |
|
| Module: well_def_prover | |
| Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: compute_card_of_set/4 |
Module: well_def_prover |
| Module: well_def_prover |
get_exact_range_of_func_type_direct(Func,R) :-
get_possible_range_of_func_or_rel_type_direct(Func,R,exact).
Calls:
| Module: well_def_prover |
Called:
Name: compute_exact_range/4 |
Module: well_def_prover |
| Module: well_def_prover |
get_explicit_dom_value(Hyps,couple(Val,RanVal),couple(Val2,RanVal)) :- get_explicit_value(Val,Hyps,Val2).
Calls:
Name: get_explicit_value/3 |
Module: well_def_prover |
get_explicit_value(couple(A,B),Hyps,couple(A2,B2)) :- !,
get_explicit_value(A,Hyps,A2), get_explicit_value(B,Hyps,B2).
get_explicit_value(rec(Fields),Hyps,rec(SFields2)) :- !,
maplist(get_field_value(Hyps),Fields,Fields2),
sort(Fields2,SFields2).
get_explicit_value(Val,Hyps,R) :- is_explicit_value(Val,AVal,Hyps),!,R=AVal.
get_explicit_value('$'(ID),Hyps,Res) :-
avl_fetch_equal_from_hyps('$'(ID),Hyps,Val2,Hyps2),
is_explicit_value(Val2,Res,Hyps2). % should we allow recursion through multiple equations?
Calls:
Name: is_explicit_value/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: =/2 |
|
Name: ! |
|
Name: sort/2 |
|
Name: maplist/3 |
Module: foo_error |
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Called:
Name: get_field_value/3 |
Module: well_def_prover |
Name: get_explicit_dom_value/3 |
Module: well_def_prover |
get_field_value(Hyps,field(Name,Val),field(Name,Val2)) :- get_explicit_value(Val,Hyps,Val2).
Calls:
Name: get_explicit_value/3 |
Module: well_def_prover |
get_lambda_args_and_body(IDS,Body,LambdaID,LambdaExpr,RestArgs,RestBodyList) :-
LambdaID='$'(Lambda),
append(RestArgs,[LambdaID],IDS), % TO DO: pass lambda info from typed unnormalized expression!
conj_to_list(Body,BodyList,[]),
select(equal(A,B),BodyList,RestBodyList),
( A=LambdaID, not_occurs(B,Lambda), LambdaExpr=B
; B=LambdaID, not_occurs(A,Lambda), LambdaExpr=A
).
Calls:
Name: =/2 |
|
Name: not_occurs/2 |
Module: foo_error |
Name: select/3 |
Module: foo_error |
Name: conj_to_list/3 |
Module: well_def_prover |
Name: append/3 |
Called:
Name: check_member_of_domain/4 |
Module: well_def_prover |
Name: is_lambda_function/1 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: get_range_or_superset/4 |
Module: well_def_prover |
get_parameter_superset_in_body(ParaID,AllParas,Body,Values) :-
( member_in_norm_conjunction(Body,member(ParaID,Values))
; member_in_norm_conjunction(Body,subset(ParaID,Values)) % there are only finitely many subsets of a finite set
; member_in_norm_conjunction(Body,subset_strict(ParaID,Values))
; member_in_norm_conjunction(Body,equal(X,Y)),
sym_unify(X,Y,ParaID,Value), Values=set_extension([Value]) ),
l_not_occurs(Values,AllParas). % as an alternative: check for finite_type of set elements; e.g., detect ID=bool(...)
Calls:
Name: l_not_occurs/2 |
Module: well_def_prover |
Name: =/2 |
|
Name: sym_unify/4 |
Module: well_def_prover |
Name: member_in_norm_conjunction/2 |
Module: foo_error |
Called:
Name: get_superset/4 |
Module: well_def_prover |
| Module: well_def_prover |
get_possible_domain_of_func_or_rel_type(iseq(_),_,'NATURAL1',subset).
get_possible_domain_of_func_or_rel_type(iseq1(_),_,'NATURAL1',subset).
get_possible_domain_of_func_or_rel_type(partial_bijection(A,_),_,A,subset).
get_possible_domain_of_func_or_rel_type(partial_function(A,_),_,A,subset).
get_possible_domain_of_func_or_rel_type(partial_injection(A,_),_,A,subset).
get_possible_domain_of_func_or_rel_type(partial_surjection(A,_),_,A,subset).
get_possible_domain_of_func_or_rel_type(perm(A),Hyps,Domain,Type) :-
(compute_card_of_set(A,Hyps,CardA,_) % we could do check_finite and use card(A) instead of CardA
-> Domain = interval(1,CardA), Type=exact
; check_finite(A,Hyps,_) -> Domain = interval(1,card(A)), Type=exact
; %print(could_not_compute_card_for_perm(A)),nl,
Domain = 'NATURAL1', Type=subset
).
get_possible_domain_of_func_or_rel_type(relations(A,_),_,A,subset).
get_possible_domain_of_func_or_rel_type(seq(_),_,'NATURAL1',subset).
get_possible_domain_of_func_or_rel_type(seq1(_),_,'NATURAL1',subset).
get_possible_domain_of_func_or_rel_type(surjection_relation(A,_),_,A,subset).
get_possible_domain_of_func_or_rel_type(total_bijection(A,_),_,A,exact).
get_possible_domain_of_func_or_rel_type(total_function(A,_),_,A,exact).
get_possible_domain_of_func_or_rel_type(total_injection(A,_),_,A,exact).
get_possible_domain_of_func_or_rel_type(total_relation(A,_),_,A,exact).
get_possible_domain_of_func_or_rel_type(total_surjection_relation(A,_),_,A,exact).
get_possible_domain_of_func_or_rel_type(total_surjection(A,_),_,A,exact).
Calls:
Name: =/2 |
|
Name: check_finite/3 |
Module: well_def_prover |
Name: ->/3 |
|
Name: compute_card_of_set/4 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover |
get_possible_range_of_func_or_rel_type(Func,Hyps,Range,ResType,Hyps2) :-
get_possible_range_of_func_or_rel_type_direct(Func,Range,Type),!, ResType=Type,Hyps2=Hyps.
get_possible_range_of_func_or_rel_type(Func,Hyps,Range,ResType,Hyps2) :-
avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
get_possible_range_of_func_or_rel_type(Func2,Hyps1,Range,ResType,Hyps2).
Calls:
Name: RECURSIVE_CALL/5 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: =/2 |
|
Name: ! |
|
| Module: well_def_prover |
Called:
Name: get_range_or_superset/4 |
Module: well_def_prover |
get_possible_range_of_func_or_rel_type_direct(total_function(_,B),B,subset).
get_possible_range_of_func_or_rel_type_direct(total_injection(_,B),B,subset).
get_possible_range_of_func_or_rel_type_direct(total_surjection(_,B),B,exact).
get_possible_range_of_func_or_rel_type_direct(total_bijection(_,B),B,exact).
get_possible_range_of_func_or_rel_type_direct(total_relation(_,B),B,subset).
get_possible_range_of_func_or_rel_type_direct(total_surjection_relation(_,B),B,exact).
get_possible_range_of_func_or_rel_type_direct(partial_function(_,B),B,subset).
get_possible_range_of_func_or_rel_type_direct(partial_injection(_,B),B,subset).
get_possible_range_of_func_or_rel_type_direct(partial_surjection(_,B),B,exact).
get_possible_range_of_func_or_rel_type_direct(partial_bijection(_,B),B,exact).
get_possible_range_of_func_or_rel_type_direct(perm(B),B,exact).
get_possible_range_of_func_or_rel_type_direct(iseq(B),B,subset).
get_possible_range_of_func_or_rel_type_direct(iseq1(B),B,subset).
get_possible_range_of_func_or_rel_type_direct(seq(B),B,subset).
get_possible_range_of_func_or_rel_type_direct(seq1(B),B,subset).
get_possible_range_of_func_or_rel_type_direct(relations(_,B),B,subset).
get_possible_range_of_func_or_rel_type_direct(surjection_relation(_,B),B,exact).
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover |
get_range_or_superset(reverse(Func),Hyps,Res,Hyps2) :- !,
get_domain_or_superset(Func,Hyps,Res,Hyps2).
get_range_or_superset(Func,Hyps,Res,Hyps3) :-
compute_exact_range_direct(Func,Hyps,Res,Hyps2),
rewrite_local_loop_check(Func,get_range_or_superset,Res,Hyps2,Hyps3),
!. % can be a loop dom(f) = ran(g)
get_range_or_superset(function(Func2,_),Hyps,Res,Hyps2) :-
% f2 : _ +-> ( _ --> Res ) ==> ran(f2(.)) <: Res
get_range_or_superset(Func2,Hyps,Range,Hyps1),
get_possible_range_of_func_or_rel_type(Range,Hyps1,Res,_,Hyps2).
get_range_or_superset(range_restriction(_,B),Hyps,Res,Hyps) :- Res=B. % in case compute_exact_range_direct fails
get_range_or_superset(Func,Hyps,Res,Hyps1) :-
function_restriction(Func,LargerFunc),
get_range_or_superset(LargerFunc,Hyps,Res,Hyps1).
get_range_or_superset(Func,Hyps,RangeSet,Hyps2) :- simple_value(Func),
avl_fetch_mem_or_struct(Func,Hyps,FunctionType,Hyps1),
get_possible_range_of_func_or_rel_type(FunctionType,Hyps1,RangeSet,_,Hyps2).
get_range_or_superset(tail(Seq),Hyps,Res,Hyps2) :- !, % ran(tail(S)) <: ran(S)
get_range_or_superset(Seq,Hyps,Res,Hyps2).
get_range_or_superset(front(Seq),Hyps,Res,Hyps2) :- !, % ran(front(S)) <: ran(S)
get_range_or_superset(Seq,Hyps,Res,Hyps2).
get_range_or_superset(restrict_front(Seq,_),Hyps,Res,Hyps2) :- !,
get_range_or_superset(Seq,Hyps,Res,Hyps2).
get_range_or_superset(restrict_tail(Seq,_),Hyps,Res,Hyps2) :- !,
get_range_or_superset(Seq,Hyps,Res,Hyps2).
get_range_or_superset(concat(Seq1,Seq2),Hyps,Res12,Hyps2) :- !, % ran(S1^S2) = ran(S1) \/ ran(S2)
get_range_or_superset(Seq1,Hyps,Res1,Hyps2),
get_range_or_superset(Seq2,Hyps,Res2,Hyps2),
construct_union(Res1,Res2,Hyps2,Res12).
get_range_or_superset(composition(_,Func2),Hyps,Res2,Hyps2) :- !, % ran((F1;F2)) <: ran(F2)
get_range_or_superset(Func2,Hyps,Res2,Hyps2).
get_range_or_superset(Func,Hyps,Range,Hyps2) :-
avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
get_range_or_superset(Func2,Hyps1,Range,Hyps2).
get_range_or_superset(Func,Hyps,RangeSuperSet,Hyps2) :-
avl_fetch_binop_from_hyps(range(Func),subset,Hyps,RangeSuperSet,Hyps2).
get_range_or_superset(comprehension_set(IDS,Body),Hyps,RangeSuperSet,Hyps2) :-
get_lambda_args_and_body(IDS,Body,_,Expr,RestIDs,_), % TO DO: add RestIDs and typing to hyps
add_new_hyp_any_vars(Hyps,RestIDs,Hyps1), % do not infer anything about lambda vars; TO DO: push RestBody
get_clash_renaming_subst(Hyps1,Renaming),
rename_norm_term(Expr,Renaming,RNExpr),
try_get_set_of_possible_values(RNExpr,Hyps1,RangeSuperSet,Hyps2).
Calls:
| Module: well_def_prover | |
Name: rename_norm_term/3 |
Module: foo_error |
Name: get_clash_renaming_subst/2 |
Module: foo_error |
Name: add_new_hyp_any_vars/3 |
Module: foo_error |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: ! |
|
Name: construct_union/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: simple_value/1 |
Module: well_def_prover |
Name: function_restriction/2 |
Module: well_def_prover |
Name: =/2 |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Called:
Name: check_finite/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: get_type2/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: get_type_from_hyps/4 |
Module: well_def_prover |
Name: get_record_type_fields/4 |
Module: well_def_prover |
Name: check_not_empty_set/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_is_subset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: finite_range/3 |
Module: well_def_prover |
get_record_type_fields(function(Func,_),Fields,Hyps,Hyps2) :-
get_range_or_superset(Func,Hyps,Range,Hyps1),
check_equal_pattern(Range,struct(rec(Fields)),Hyps1,Hyps2).
get_record_type_fields(Rec,Fields,Hyps,Hyps2) :-
get_type_from_hyps(Rec,Hyps,RecType,Hyps1),
check_equal_pattern(RecType,struct(rec(Fields)),Hyps1,Hyps2).
Calls:
Name: check_equal_pattern/4 |
Module: well_def_prover |
Name: get_type_from_hyps/4 |
Module: well_def_prover |
Name: get_range_or_superset/4 |
Module: well_def_prover |
Called:
| Module: well_def_prover |
get_set_val_size([],0).
get_set_val_size(avl_set(AVL),Size) :- avl_size(AVL,Size).
Calls:
Name: avl_size/2 |
Module: foo_error |
Called:
Name: compute_card_of_set/4 |
Module: well_def_prover |
get_superset(comprehension_set([ID],Body),Hyps,Set,Hyps) :-
get_parameter_superset_in_body(ID,[ID],Body,Set).
get_superset(set_subtraction(A,_),Hyps,A,Hyps).
get_superset(intersection(A,B),Hyps,R,Hyps) :- (R=A ; R=B).
Calls:
Name: =/2 |
|
| Module: well_def_prover |
Called:
| Module: well_def_prover |
get_type2(domain(Func),Hyps,XType,Hyps2) :- !,
get_domain_or_superset(Func,Hyps,XType,Hyps2).
get_type2(range(Func),Hyps,XType,Hyps2) :- !,
get_range_or_superset(Func,Hyps,XType,Hyps2).
get_type2(Type,Hyps,Type,Hyps).
Calls:
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: ! |
|
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Called:
Name: get_type_from_hyps/4 |
Module: well_def_prover |
get_type_from_hyps(X,Hyps,XType,Hyps2) :-
avl_fetch_mem_from_hyps(X,Hyps,XSet,Hyps1),
get_type2(XSet,Hyps1,XType,Hyps2).
get_type_from_hyps(function(Func2,_),Hyps,Range,Hyps2) :-
% f : _ +-> ( _ >-> _ ) => f(_) : _ >-> _
get_range_or_superset(Func2,Hyps,Range,Hyps2).
get_type_from_hyps(second_of_pair(X),Hyps,Type,Hyps2) :- %prj2
get_type_from_hyps(X,Hyps,XType,Hyps1),
check_equal_pattern(XType,cartesian_product(_,Type),Hyps1,Hyps2).
get_type_from_hyps(first_of_pair(X),Hyps,Type,Hyps2) :- %prj1
get_type_from_hyps(X,Hyps,XType,Hyps1),
check_equal_pattern(XType,cartesian_product(Type,_),Hyps1,Hyps2).
get_type_from_hyps(assertion_expression(_,_,X),Hyps,XType,Hyps1) :-
get_type_from_hyps(X,Hyps,XType,Hyps1).
Calls:
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: check_equal_pattern/4 |
Module: well_def_prover |
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: get_type2/4 |
Module: well_def_prover |
| Module: well_def_prover |
Called:
Name: check_is_subset/4 |
Module: well_def_prover |
Name: get_record_type_fields/4 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_is_injective/2 |
Module: well_def_prover |
has_finite_elements(fin_subset(_),_) :- !.
has_finite_elements(fin1_subset(_),_) :- !.
has_finite_elements(pow_subset(X),Hyps) :- !, check_finite(X,Hyps,_).
has_finite_elements(pow1_subset(X),Hyps) :- !, check_finite(X,Hyps,_).
has_finite_elements(seq(_),_) :- !. % every sequence is always finite (of finite length)
has_finite_elements(seq1(_),_) :- !.
has_finite_elements(iseq(_),_) :- !.
has_finite_elements(iseq1(_),_) :- !.
has_finite_elements(perm(_),_) :- !.
has_finite_elements(union(A,B),Hyps) :- !, has_finite_elements(A,Hyps), has_finite_elements(B,Hyps).
has_finite_elements(intersection(A,B),Hyps) :- !, (has_finite_elements(A,Hyps) -> true ; has_finite_elements(B,Hyps)).
has_finite_elements(set_subtraction(A,_),Hyps) :- !, has_finite_elements(A,Hyps).
has_finite_elements(sorted_set_extension(L),Hyps) :- !, l_check_finite(L,Hyps).
has_finite_elements(set_extension(L),Hyps) :- !, l_check_finite(L,Hyps).
has_finite_elements(S,_) :- is_empty_set_direct(S),!. % has no elements
has_finite_elements(Func,Hyps) :- is_partial_function(Func,A,B),!,
(check_finite(A,Hyps,_) -> true ; is_injective(Func), check_finite(B,Hyps,_)).
has_finite_elements(Rel,Hyps) :- is_relations_type(Rel,A,B),!,check_finite(A,Hyps,_),check_finite(B,Hyps,_).
Calls:
Name: check_finite/3 |
Module: well_def_prover |
Name: ! |
|
Name: is_relations_type/3 |
Module: well_def_prover |
Name: is_injective/1 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: is_partial_function/3 |
Module: well_def_prover |
Name: is_empty_set_direct/1 |
Module: well_def_prover |
Name: l_check_finite/2 |
Module: well_def_prover |
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
Called:
Name: check_finite/3 |
Module: well_def_prover |
hyp_repl(Hyps) :- hyp_repl_prompt(Hyps),read(Term), !, hyp_repl(Term,Hyps).
hyp_repl(_).
Calls:
Name: hyp_repl/2 |
Module: well_def_prover |
Name: ! |
|
Name: read/1 |
|
Name: hyp_repl_prompt/1 |
Module: well_def_prover |
Called:
Name: hyp_repl/1 |
Module: well_def_prover |
hyp_repl(end_of_file,_).
hyp_repl(quit,_).
hyp_repl(exit,_).
hyp_repl(help,Hyps) :- write('Use quit to exit, print to portray_hyps, or type an identifier to lookup in hyps'),nl,
hyp_repl(Hyps).
hyp_repl(print,Hyps) :- portray_hyps(Hyps), hyp_repl(Hyps).
hyp_repl(ID,Hyps) :- avl_fetch_equal_from_hyps($(ID),Hyps,Value,_),
format('Value for ~w:~n ~w~n',[ID,Value]),
hyp_repl(Hyps).
Calls:
Name: hyp_repl/1 |
Module: well_def_prover |
Name: format/2 |
|
| Module: well_def_prover | |
Name: portray_hyps/1 |
Module: foo_error |
Name: nl |
|
Name: write/1 |
Called:
Name: hyp_repl/1 |
Module: well_def_prover |
hyp_repl_prompt(hyp_rec(AVL,HInfos)) :-
avl_size(AVL,Size),
avl_size(HInfos,ISize),!,
format('hyp_rec(#~w,#~w) >>>',[Size,ISize]).
hyp_repl_prompt(_) :- write('ILLEGAL HYP_REC >>>').
Calls:
Name: write/1 |
|
Name: format/2 |
|
Name: ! |
|
Name: avl_size/2 |
Module: foo_error |
Called:
Name: hyp_repl/1 |
Module: well_def_prover |
id_or_record_field('$'(_)).
id_or_record_field(record_field(_,_)).
Called:
Name: check_finite/3 |
Module: well_def_prover |
improve_integer_set_precision(X,XSet1,Hyps1,NewSet,Hyps3) :-
is_integer_set(XSet1),
avl_fetch_worthwhile_mem_from_hyps(X,Hyps1,XSet2,Hyps2),
XSet2 \= XSet1,
!,
intersect_sets(XSet1,XSet2,XSet12),
try_improve_interval(XSet12,X,Hyps2,NewSet,Hyps3). % TO DO: we could try and find another member
improve_integer_set_precision(X,XSet1,Hyps1,NewSet,Hyps3) :-
is_infinite__or_large_integer_set(XSet1,Low,LargeUp),
avl_fetch_binop_from_hyps(X,less_equal,Hyps1,Up,Hyps2),
Up \= LargeUp, % we really improve upon earlier value
!,
try_improve_interval(interval(Low,Up),X,Hyps2,NewSet,Hyps3).
improve_integer_set_precision(X,XSet1,Hyps1,NewSet,Hyps2) :-
try_improve_interval(XSet1,X,Hyps1,NewSet,Hyps2).
Calls:
Name: try_improve_interval/5 |
Module: well_def_prover |
Name: ! |
|
Name: \=/2 |
|
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: intersect_sets/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: is_integer_set/1 |
Module: well_def_prover |
Called:
| Module: well_def_prover |
improve_interval(X,OldLow,OldUp,Hyps1,NewLow,NewUp,Hyps3) :-
improve_upper_bound(X,OldUp,Hyps1,NewUp1,Hyps2),!,
improve_interval(X,OldLow,NewUp1,Hyps2,NewLow,NewUp,Hyps3).
improve_interval(X,OldLow,Up,Hyps1,NewLow,Up,Hyps2) :-
improve_interval2(X,OldLow,Hyps1,NewLow,Hyps2).
Calls:
Name: improve_interval2/5 |
Module: well_def_prover |
Name: RECURSIVE_CALL/7 |
Module: well_def_prover |
Name: ! |
|
Name: improve_upper_bound/5 |
Module: well_def_prover |
Called:
Name: try_improve_interval/5 |
Module: well_def_prover |
improve_interval2(X,OldLow,Hyps1,NewLow,Hyps3) :-
improve_lower_bound(X,OldLow,Hyps1,Low1,Hyps2),!,
improve_interval2(X,Low1,Hyps2,NewLow,Hyps3).
improve_interval2(_,Low,Hyps,Low,Hyps).
Calls:
Name: RECURSIVE_CALL/5 |
Module: well_def_prover |
Name: ! |
|
Name: improve_lower_bound/5 |
Module: well_def_prover |
Called:
Name: improve_interval/7 |
Module: well_def_prover |
improve_lower_bound(X,OldLow,Hyps1,NewLow,Hyps2) :-
avl_fetch_binop_from_hyps(X,greater_equal,Hyps1,Low,Hyps2),
order_values(Low,OldLow,OldLow,NewLow),
NewLow \= OldLow.
Calls:
Name: \=/2 |
|
Name: order_values/4 |
Module: well_def_prover |
| Module: well_def_prover |
Called:
Name: improve_interval2/5 |
Module: well_def_prover |
improve_upper_bound(X,OldUp,Hyps1,NewUp,Hyps2) :-
avl_fetch_binop_from_hyps(X,less_equal,Hyps1,Up,Hyps2),
order_values(OldUp,Up,NewUp,OldUp),
NewUp \= OldUp.
Calls:
Name: \=/2 |
|
Name: order_values/4 |
Module: well_def_prover |
| Module: well_def_prover |
Called:
Name: improve_interval/7 |
Module: well_def_prover |
index_in_non_empty_sequence(1,_,_).
index_in_non_empty_sequence(card(E),E,_).
index_in_non_empty_sequence(size(E),E,_).
index_in_non_empty_sequence('$'(X),E,Hyps) :-
avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
rewrite_local_loop_check(X,index_in_non_empty_sequence,Y,Hyps2,Hyps3),
index_in_non_empty_sequence(Y,E,Hyps3).
index_in_non_empty_sequence(X,E,Hyps) :- \+ useful_value(X), % do not rewrite 10 to interval(10,10)
try_get_set_of_possible_values(X,Hyps,XSet,Hyps2),
rewrite_local_loop_check(X,index_in_non_empty_sequence,XSet,Hyps2,Hyps3),
all_in_non_empty_sequence(XSet,E,Hyps3).
Calls:
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: useful_value/1 |
Module: well_def_prover |
Name: not/1 |
|
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
| Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: check_member_of_domain/4 |
Module: well_def_prover |
Name: check_subset_interval/5 |
Module: well_def_prover |
infer_sequence_type_of_expr(sequence_extension([_|_]),_,seq1).
infer_sequence_type_of_expr(sorted_set_extension(SList),_,seq1) :-
sorted_set_extension_is_seq(SList,1).
infer_sequence_type_of_expr(set_extension(List),_,seq1) :- sort(List,SList),
sorted_set_extension_is_seq(SList,1).
infer_sequence_type_of_expr(insert_tail(_,_),_,seq1).
infer_sequence_type_of_expr(insert_front(_,_),_,seq1).
infer_sequence_type_of_expr(concat(A,B),Hyps,R) :-
( infer_sequence_type_of_expr(A,Hyps,seq1) -> R=seq1
; infer_sequence_type_of_expr(B,Hyps,seq1) -> R=seq1
; R=seq).
infer_sequence_type_of_expr(restrict_front(_,_),_,seq).
infer_sequence_type_of_expr(restrict_tail(_,_),_,seq).
infer_sequence_type_of_expr(rev(A),Hyps,R) :-
(infer_sequence_type_of_expr(A,Hyps,seq1) -> R=seq1 ; R=seq).
infer_sequence_type_of_expr(front(_),_,seq). % we could call check_not_empty_set(front(A),Hyps)
infer_sequence_type_of_expr(tail(_),_,seq). % ditto
infer_sequence_type_of_expr(general_concat(_),_,seq).
infer_sequence_type_of_expr(value(avl_set(SeqAVL)),_,seq1) :- !, SeqAVL \= empty,
safe_is_avl_sequence(SeqAVL).
infer_sequence_type_of_expr(if_then_else(_,A,B),Hyps,Type) :- !,
(infer_sequence_type_of_expr(A,Hyps,S1)
-> infer_sequence_type_of_expr(B,Hyps,S2), lub_seq(S1,S2,Type)).
infer_sequence_type_of_expr(S,_,seq) :- is_empty_set_direct(S).
infer_sequence_type_of_expr(Expr,Hyps,R) :-
is_lambda_function_with_domain(Expr,Domain),
Domain = interval(1,N),
(check_leq(1,N,Hyps) -> R = seq1 ; R=seq).
Calls:
Name: =/2 |
|
Name: check_leq/3 |
Module: well_def_prover |
Name: ->/3 |
|
| Module: well_def_prover | |
Name: is_empty_set_direct/1 |
Module: well_def_prover |
Name: lub_seq/3 |
Module: well_def_prover |
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: ->/2 |
|
Name: ! |
|
Name: safe_is_avl_sequence/1 |
Module: custom_explicit_sets |
Name: \=/2 |
|
| Module: well_def_prover | |
Name: sort/2 |
Called:
Name: check_finite/3 |
Module: well_def_prover |
Name: check_is_sequence/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_not_empty_set/2 |
Module: well_def_prover |
| Module: well_def_prover |
intersect_interval(interval(L2,U2),L1,U1,interval(L3,U3)) :-
order_values(L1,L2,_,L3), % choose larger value as lower bound
order_values(U1,U2,U3,_). % choose smaller value as upper bound
intersect_interval('NATURAL1',L1,U1,interval(L3,U1)) :- order_values(L1,1,L3,_).
intersect_interval('NATURAL',L1,U1,interval(L3,U1)) :- order_values(L1,0,L3,_).
Calls:
Name: order_values/4 |
Module: well_def_prover |
Called:
Name: intersect_sets/3 |
Module: well_def_prover |
intersect_sets(interval(L1,U1),B,Res) :- !, intersect_interval(B,L1,U1,Res).
intersect_sets(B,interval(L1,U1),Res) :- intersect_interval(B,L1,U1,Res).
intersect_sets('NATURAL1','NATURAL','NATURAL1').
intersect_sets('NATURAL','NATURAL1','NATURAL1').
Calls:
Name: intersect_interval/4 |
Module: well_def_prover |
Name: ! |
Called:
| Module: well_def_prover | |
| Module: well_def_prover |
is_avl_set_of_sequences(AVL,SeqType) :- avl_height(AVL,Height), Height<7,
expand_custom_set_to_list(avl_set(AVL),ListOfSeqs),
l_is_sequence(ListOfSeqs,SeqType).
Calls:
Name: l_is_sequence/2 |
Module: well_def_prover |
| Module: custom_explicit_sets | |
Name: </2 |
|
Name: avl_height/2 |
Module: foo_error |
Called:
Name: check_subset_avl/3 |
Module: well_def_prover |
is_empty_set_direct(empty_set).
is_empty_set_direct(empty_sequence).
is_empty_set_direct(value(X)) :- X==[].
Calls:
Name: ==/2 |
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_equal_h/6 |
Module: well_def_prover |
Name: check_is_sequence/3 |
Module: well_def_prover |
Name: check_empty_set/3 |
Module: well_def_prover |
Name: check_not_equal/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: has_finite_elements/2 |
Module: well_def_prover |
is_enumerated_set(ID,Hyp) :-
enumerated_set(ID),
\+ is_hyp_var(ID,Hyp). % global enumerated set constant visible
Calls:
Name: is_hyp_var/2 |
Module: foo_error |
Name: not/1 |
|
Name: enumerated_set/1 |
Module: b_global_sets |
Called:
Name: compute_card_of_set/4 |
Module: well_def_prover |
is_explicit_value(boolean_true,pred_true,_).
is_explicit_value(boolean_false,pred_false,_).
is_explicit_value(Nr,Nr,_) :- number(Nr). % integers and floats
is_explicit_value(integer(Nr),Nr,_) :- integer(Nr). % normally already replaced by norm_expr2
is_explicit_value(string(Atom),Atom,_).
is_explicit_value(real(Atom),Res,_) :- atom(Atom),
construct_real(Atom,term(floating(Res))). % c.f. is_real/1 in kernel_reals
is_explicit_value(couple(A,B),(AV,BV),Hyp) :- is_explicit_value(A,AV,Hyp), is_explicit_value(B,BV,Hyp).
is_explicit_value('$'(ID),'$'(ID),Hyp) :- is_global_constant_id(ID,Hyp).
is_explicit_value(value(R),Nr,_) :- nonvar(R),R=int(Nr), integer(Nr). % TODO: more values, strings, reals, ...
Calls:
Name: integer/1 |
|
Name: =/2 |
|
Name: nonvar/1 |
|
Name: is_global_constant_id/2 |
Module: well_def_prover |
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: construct_real/2 |
Module: kernel_reals |
Name: atom/1 |
|
Name: number/1 |
Called:
Name: check_not_equal/3 |
Module: well_def_prover |
Name: get_explicit_value/3 |
Module: well_def_prover |
is_glob_const_id(Hyps,'$'(ID)) :- is_global_constant_id(ID,Hyps).
Calls:
Name: is_global_constant_id/2 |
Module: well_def_prover |
is_global_constant_id(ID,Hyp) :-
lookup_global_constant(ID,_),
\+ is_hyp_var(ID,Hyp). % global enumerated set constant visible
Calls:
Name: is_hyp_var/2 |
Module: foo_error |
Name: not/1 |
|
Name: lookup_global_constant/2 |
Module: b_global_sets |
Called:
Name: is_explicit_value/3 |
Module: well_def_prover |
Name: maximal_set_extension/2 |
Module: well_def_prover |
Name: is_glob_const_id/2 |
Module: well_def_prover |
is_global_set_id(ID,Hyps) :-
b_global_set(ID),
\+ is_hyp_var(ID,Hyps). % global enumerated set visible
Calls:
Name: is_hyp_var/2 |
Module: foo_error |
Name: not/1 |
|
Name: b_global_set/1 |
Module: b_global_sets |
Called:
Name: maximal_set/2 |
Module: well_def_prover |
is_infinite__or_large_integer_set('NATURAL',0,inf).
is_infinite__or_large_integer_set('NATURAL1',1,inf).
is_infinite__or_large_integer_set(interval(Low,max_int),Low,max_int). % one cannot prove a lot with max_int anyway!?
Called:
| Module: well_def_prover |
is_injective(total_injection(_,_)).
is_injective(partial_injection(_,_)).
is_injective(total_bijection(_,_)).
is_injective(partial_bijection(_,_)).
is_injective(iseq(_)).
is_injective(iseq1(_)).
Called:
| Module: well_def_prover | |
Name: has_finite_elements/2 |
Module: well_def_prover |
is_injective_function_type(PF,Hyps,Hyps1) :- is_injective(PF),!,Hyps1=Hyps.
is_injective_function_type(PF,Hyps,Hyps2) :-
avl_fetch_worthwhile_equal_from_hyps(PF,Hyps,PF2,Hyps1), % in case we have a definition like X = 1..n --> R
is_injective_function_type(PF2,Hyps1,Hyps2).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: =/2 |
|
Name: ! |
|
Name: is_injective/1 |
Module: well_def_prover |
Called:
Name: check_is_injective/2 |
Module: well_def_prover |
is_integer_set(interval(_,_)).
is_integer_set('NATURAL').
is_integer_set('NATURAL1').
is_integer_set('INTEGER').
Called:
| Module: well_def_prover |
is_interval(Expr,Hyps,A,B) :- simplify_expr(Expr,Hyps,SE), is_interval_aux(SE,A,B).
Calls:
Name: is_interval_aux/3 |
Module: well_def_prover |
Name: simplify_expr/3 |
Module: well_def_prover |
Called:
Name: check_is_sequence/3 |
Module: well_def_prover |
is_interval_aux(interval(A,B),A,B).
is_interval_aux(value(CS),A,B) :- nonvar(CS), CS= avl_set(AVL), avl_is_interval(AVL,A,B).
Calls:
Name: avl_is_interval/3 |
Module: custom_explicit_sets |
Name: =/2 |
|
Name: nonvar/1 |
Called:
Name: is_interval/4 |
Module: well_def_prover |
is_lambda_function(comprehension_set(IDS,Body)) :- !,
get_lambda_args_and_body(IDS,Body,_,_,_,_).
is_lambda_function(Expr) :- is_lambda_function_with_domain(Expr,_).
Calls:
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ! |
Called:
| Module: well_def_prover | |
Name: check_finite/3 |
Module: well_def_prover |
is_lambda_function_with_domain(comprehension_set(IDS,Body),Set) :-
get_lambda_args_and_body(IDS,Body,_,_,Args,RestBodyList),
get_argument_types(Args,Args,RestBodyList,ArgTypes),
create_cartesian_product(ArgTypes,Set).
is_lambda_function_with_domain(cartesian_product(Domain,Set),Domain) :-
singleton_set(Set,_).
is_lambda_function_with_domain(set_extension([couple(El,_)]),set_extension([El])).
is_lambda_function_with_domain(Set,singleton_set([El])) :- singleton_set(Set,couple(El,_)). % TO DO: longer lists and check no multiple domain elements
is_lambda_function_with_domain(sequence_extension(List),interval(1,Len)) :- length(List,Len).
Calls:
Name: length/2 |
|
Name: singleton_set/2 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: get_argument_types/4 |
Module: well_def_prover |
| Module: well_def_prover |
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_not_empty_set/2 |
Module: well_def_prover |
Name: is_lambda_function/1 |
Module: well_def_prover |
is_partial_function(total_function(A,B),A,B).
is_partial_function(partial_function(A,B),A,B).
is_partial_function(total_injection(A,B),A,B).
is_partial_function(partial_injection(A,B),A,B).
is_partial_function(total_surjection(A,B),A,B).
is_partial_function(partial_surjection(A,B),A,B).
is_partial_function(total_bijection(A,B),A,B).
is_partial_function(partial_bijection(A,B),A,B).
is_partial_function(perm(A),'NATURAL1',A).
is_partial_function(seq(B),'NATURAL1',B).
is_partial_function(seq1(B),'NATURAL1',B).
is_partial_function(iseq(B),'NATURAL1',B).
is_partial_function(iseq1(B),'NATURAL1',B).
Called:
Name: check_finite/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: has_finite_elements/2 |
Module: well_def_prover |
is_partial_function_type(PF,Hyps,Hyps1) :- is_partial_function(PF,_,_),!,Hyps1=Hyps.
is_partial_function_type(range(Func),Hyps,Hyps2) :-
get_range_or_superset(Func,Hyps,RanFunc,Hyps1),!,
is_partial_function_type(RanFunc,Hyps1,Hyps2).
is_partial_function_type(domain(Func),Hyps,Hyps2) :-
get_domain_or_superset(Func,Hyps,DomFunc,Hyps1),!,
is_partial_function_type(DomFunc,Hyps1,Hyps2).
is_partial_function_type(sorted_set_extension(Funcs),Hyps,Hyps2) :- !,
is_partial_function_type(set_extension(Funcs),Hyps,Hyps2).
is_partial_function_type(set_extension(Funcs),Hyps,Hyps2) :- !,
(member(F,Funcs), \+ check_is_partial_function(F,Hyps) -> fail
; Hyps2=Hyps). % all elements of Funcs are partial functions
is_partial_function_type(Func,Hyps,Hyps2) :-
get_superset(Func,Hyps,SuperSet,Hyps1),!,
is_partial_function_type(SuperSet,Hyps1,Hyps2).
is_partial_function_type(PF,Hyps,Hyps2) :-
avl_fetch_worthwhile_equal_from_hyps(PF,Hyps,PF2,Hyps1), % in case we have a definition like X = 1..n --> R
is_partial_function_type(PF2,Hyps1,Hyps2).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: ! |
|
Name: get_superset/4 |
Module: well_def_prover |
Name: =/2 |
|
Name: fail |
|
| Module: well_def_prover | |
Name: not/1 |
|
Name: member/2 |
|
Name: ->/3 |
|
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: is_partial_function/3 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
Name: compute_card_of_set/4 |
Module: well_def_prover |
| Module: well_def_prover |
is_relations_type(relations(A,B),A,B).
is_relations_type(surjection_relation(A,B),A,B).
is_relations_type(total_relation(A,B),A,B).
is_relations_type(total_surjection_relation(A,B),A,B).
Called:
Name: has_finite_elements/2 |
Module: well_def_prover |
Name: check_finite/3 |
Module: well_def_prover |
is_sequence(avl_set(SeqAVL),_) :- safe_is_avl_sequence(SeqAVL).
is_sequence([],seq).
Calls:
Name: safe_is_avl_sequence/1 |
Module: custom_explicit_sets |
Called:
Name: l_is_sequence/2 |
Module: well_def_prover |
Name: is_subsequence/1 |
Module: well_def_prover |
Name: check_subset_avl/3 |
Module: well_def_prover |
is_set_extension(set_extension(List),List).
is_set_extension(sorted_set_extension(List),List).
Called:
| Module: well_def_prover | |
Name: check_domain_disjoint/4 |
Module: well_def_prover |
is_set_of_sequences_type(seq1(_),_,seq1) :- !.
is_set_of_sequences_type(seq(_),_,seq) :- !.
is_set_of_sequences_type(iseq(_),_,seq) :- !.
is_set_of_sequences_type(iseq1(_),_,seq) :- !.
is_set_of_sequences_type(perm(A),Hyps,Type) :- !,
(check_not_equal_empty_set(A,Hyps,_) -> Type=seq1 ; Type=seq).
is_set_of_sequences_type(Func,Hyps,Type) :- % a total function 1..Up --> Range is a sequence
get_exact_domain_of_func_or_rel_type(Func,Hyps,Dom,Hyps1),
check_equal_pattern(Dom,interval(1,Up),Hyps1,Hyps2),
% we could call check_equal for Low; relevant for :wd BV=16 & II=1 & BIdx = II..BV & s:BIdx --> BOOL & res=size(s)
is_partial_function_type(Func,Hyps2,_),
(number(Up), Up>0 % we could call check_leq
-> Type=seq1 ; Type=seq).
Calls:
Name: =/2 |
|
Name: >/2 |
|
Name: number/1 |
|
Name: ->/3 |
|
| Module: well_def_prover | |
Name: check_equal_pattern/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: ! |
Called:
Name: check_is_sequence/3 |
Module: well_def_prover |
is_subsequence((int(_Index),Sequence)) :- is_sequence(Sequence,seq).
Calls:
Name: is_sequence/2 |
Module: well_def_prover |
iseq_operator(perm(Set),Set).
iseq_operator(iseq(Set),Set).
iseq_operator(iseq1(Set),Set).
Called:
Name: check_all_finite/2 |
Module: well_def_prover |
l_check_finite([],_).
l_check_finite([H|T],Hyp) :- (check_finite(H,Hyp,_) -> l_check_finite(T,Hyp)).
Calls:
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
Name: check_finite/3 |
Module: well_def_prover |
Name: ->/2 |
Called:
Name: has_finite_elements/2 |
Module: well_def_prover |
l_check_is_member([],_,_).
l_check_is_member([El|T],B,Hyps) :- check_member_of_set(B,El,Hyps,_ProofTree), l_check_is_member(T,B,Hyps).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
Called:
Name: check_is_subset/4 |
Module: well_def_prover |
l_check_not_member_of_set([],_,_).
l_check_not_member_of_set([El|T],Set,Hyps) :-
check_not_member_of_set(Set,El,Hyps,_PT),
l_check_not_member_of_set(T,Set,Hyps).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
| Module: well_def_prover |
Called:
Name: check_disjoint_aux/3 |
Module: well_def_prover |
Name: check_domain_disjoint/4 |
Module: well_def_prover |
l_is_sequence([],_).
l_is_sequence([S1|T],SeqType) :- is_sequence(S1,SeqType), l_is_sequence(T,SeqType).
Calls:
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
Name: is_sequence/2 |
Module: well_def_prover |
Called:
| Module: well_def_prover |
l_not_occurs(Expr,AllArgs) :- member('$'(ID),AllArgs), occurs(Expr,ID),!,fail.
l_not_occurs(_,_).
Calls:
Name: fail |
|
Name: ! |
|
Name: occurs/2 |
Module: foo_error |
Name: member/2 |
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: typing_predicate_for/4 |
Module: well_def_prover |
l_rename_and_prove_goals([],_,_,[]).
l_rename_and_prove_goals([H|T],Subst,Hyps,[PTH|PTT]) :-
rename_norm_term(H,Subst,RH),!,
prove_po(RH,Hyps,PTH),!, % TO DO: use version of prove_po that does not print info
l_rename_and_prove_goals(T,Subst,Hyps,PTT).
Calls:
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: ! |
|
Name: prove_po/3 |
Module: well_def_prover |
Name: rename_norm_term/3 |
Module: foo_error |
Called:
Name: check_member_of_domain/4 |
Module: well_def_prover |
lub_seq(seq1,seq1,seq1).
lub_seq(seq1,seq,seq).
lub_seq(seq,seq1,seq).
lub_seq(seq,seq,seq).
Called:
| Module: well_def_prover |
match_parameter(ParaID,ParaID).
match_parameter(couple(ParaID,_),ParaID). % x|->y : Values finite implies finitely many values for x
match_parameter(couple(_,ParaID),ParaID).
match_parameter(set_extension(Ext),ParaID) :-
member(El,Ext), match_parameter(El,ParaID). % {x,..} : Values finite implies finitely many values for x
match_parameter(sorted_set_extension(Ext),ParaID) :- match_parameter(set_extension(Ext),ParaID).
match_parameter(sequence_extension(Ext),ParaID) :- member(ParaID,Ext).
match_parameter(rev(RF),ParaID) :- match_parameter(RF,ParaID).
match_parameter(reverse(RF),ParaID) :- match_parameter(RF,ParaID).
match_parameter(unary_minus(RF),ParaID) :- match_parameter(RF,ParaID).
match_parameter(concat(RF1,RF2),ParaID) :- (match_parameter(RF1,ParaID) -> true ; match_parameter(RF2,ParaID)).
match_parameter(union(RF1,RF2),ParaID) :- (match_parameter(RF1,ParaID) -> true ; match_parameter(RF2,ParaID)).
match_parameter(overwrite(_,RF),ParaID) :- match_parameter(RF,ParaID). % f <+ RF = (... <<| f ) \/ RF
match_parameter(Add,ParaID) :- add_with_number(Add,A,_Number), match_parameter(A,ParaID).
match_parameter(Mul,ParaID) :- mul_with_number(Mul,A,Number), Number \= 0, match_parameter(A,ParaID).
Calls:
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
Name: \=/2 |
|
Name: mul_with_number/3 |
Module: well_def_prover |
Name: add_with_number/3 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: member/2 |
Called:
| Module: well_def_prover |
maximal_set('INTEGER',_). % integer_set('INTEGER') ?
maximal_set(real_set,_).
maximal_set(string_set,_).
maximal_set(bool_set,_).
maximal_set('typeset',_).
maximal_set(cartesian_product(A,B),Hyps) :- % SIMP_CPROD_EQUAL_TYPE
maximal_set(A,Hyps), maximal_set(B,Hyps).
maximal_set(relations(A,B),Hyps) :- % SIMP_TYPE_EQUAL_REL
maximal_set(A,Hyps), maximal_set(B,Hyps).
maximal_set(set_subtraction(A,B),Hyps) :- % SIMP_SETMINUS_EQUAL_TYPE
maximal_set(A,Hyps), check_equal_empty_set(B,Hyps,_).
maximal_set(pow_subset(A),Hyps) :- maximal_set(A,Hyps).
maximal_set('$'(ID),Hyps) :- is_global_set_id(ID,Hyps).
maximal_set(value(avl_set(AVL)),_) :-
quick_definitely_maximal_set_avl(AVL).
maximal_set(set_extension(A),Hyps) :- maximal_set_extension(A,Hyps).
maximal_set(comprehension_set(_,truth),_).
Calls:
Name: maximal_set_extension/2 |
Module: well_def_prover |
| Module: custom_explicit_sets | |
Name: is_global_set_id/2 |
Module: well_def_prover |
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
Name: check_equal_empty_set/3 |
Module: well_def_prover |
Called:
Name: check_subset_avl/3 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover |
maximal_set_extension([boolean_true|T],_) :- !, member(boolean_false,T).
maximal_set_extension([boolean_false|T],_) :- !, member(boolean_true,T).
maximal_set_extension(['$'(ID)|T],Hyps) :-
is_global_constant_id(ID,Hyps),
sort(['$'(ID)|T],Sorted),
maplist(is_glob_const_id(Hyps),Sorted), % all elements are global constants
lookup_global_constant(ID,fd(_,GlobalSet)),
enumerated_set(GlobalSet),b_global_set_cardinality(GlobalSet,Size),
length(Sorted,Size).
Calls:
Name: length/2 |
|
| Module: b_global_sets | |
Name: enumerated_set/1 |
Module: b_global_sets |
Name: lookup_global_constant/2 |
Module: b_global_sets |
Name: maplist/2 |
Module: foo_error |
Name: sort/2 |
|
Name: is_global_constant_id/2 |
Module: well_def_prover |
Name: member/2 |
|
Name: ! |
Called:
| Module: well_def_prover | |
Name: maximal_set/2 |
Module: well_def_prover |
maximal_value(interval(_,Up),Up).
maximal_value(value(avl_set(A)),Up) :- avl_max(A,int(Up)).
Calls:
Name: avl_max/2 |
Module: foo_error |
Called:
| Module: well_def_prover |
merge_possible_domains_of_list([],Hyps,Acc,Acc,Hyps).
merge_possible_domains_of_list([H|T],Hyps,Acc,Res,Hyps2) :-
get_domain_or_superset(H,Hyps,Domain,Hyps1),!,
construct_union(Acc,Domain,Hyps1,Acc1),
merge_possible_domains_of_list(T,Hyps1,Acc1,Res,Hyps2).
Calls:
Name: RECURSIVE_CALL/5 |
Module: well_def_prover |
Name: construct_union/4 |
Module: well_def_prover |
Name: ! |
|
Name: get_domain_or_superset/4 |
Module: well_def_prover |
Called:
| Module: well_def_prover |
merge_set_extensions(empty_set) --> [].
merge_set_extensions(empty_sequence) --> [].
merge_set_extensions(set_extension(L)) --> L.
merge_set_extensions(sorted_set_extension(L)) --> L.
merge_set_extensions(union(A,B)) --> merge_set_extensions(A), merge_set_extensions(B).
Calls:
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: phrase/3 |
|
Name: =/2 |
Called:
| Module: well_def_prover |
minus_with_number(add(A,B),A,Nr) :- number(B), Nr is -B.
minus_with_number(minus(A,Nr),A,Nr) :- number(Nr).
Calls:
Name: number/1 |
|
Name: is/2 |
Called:
Name: check_leq/3 |
Module: well_def_prover |
mul_with_number(multiplication(A,B),X,Nr) :- (number(A) -> Nr=A, X=B ; number(B) -> Nr=B, X=A).
mul_with_number(unary_minus(A),A,Nr) :- Nr is -1.
Calls:
Name: is/2 |
|
Name: =/2 |
|
Name: number/1 |
|
Name: ->/2 |
|
Name: ->/3 |
Called:
Name: decompose_floor/3 |
Module: well_def_prover |
Name: match_parameter/2 |
Module: well_def_prover |
Name: check_leq_nr/3 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
not_integer(empty_set).
not_integer(empty_sequence).
not_integer(interval(_,_)).
not_integer(couple(_,_)).
not_integer(union(_,_)).
not_integer(intersection(_,_)).
not_integer(domain(_)).
not_integer(range(_)).
Called:
Name: check_integer/2 |
Module: well_def_prover |
order_aux_nr(N2,N1,R1,R2) :- number(N2),!,
(N2>N1 -> R1=N1,R2=N2 ; R1=N2,R2=N1).
order_aux_nr(max_int,N1,R1,R2) :- N1 < 1, !, R1=N1, R2=max_int.
order_aux_nr(_N2,N1,N1,N1). % choose the number as the bound
Calls:
Name: =/2 |
|
Name: ! |
|
Name: </2 |
|
Name: >/2 |
|
Name: ->/3 |
|
Name: number/1 |
Called:
Name: order_values/4 |
Module: well_def_prover |
order_values(N1,N2,R1,R2) :- number(N1),!, order_aux_nr(N2,N1,R1,R2).
order_values(N1,N2,R1,R2) :- number(N2),!, order_aux_nr(N1,N2,R1,R2).
order_values(min_int,N2,R1,R2) :- !, R1=min_int,R2=N2.
order_values(max_int,N2,R1,R2) :- !, R1=N2,R2=max_int.
order_values(N1,N2,N1,N2). % just choose N1
Calls:
Name: =/2 |
|
Name: ! |
|
Name: order_aux_nr/4 |
Module: well_def_prover |
Name: number/1 |
Called:
Name: improve_lower_bound/5 |
Module: well_def_prover |
Name: improve_upper_bound/5 |
Module: well_def_prover |
Name: intersect_interval/4 |
Module: well_def_prover |
pow_subset_operator(fin_subset(X),X).
pow_subset_operator(fin1_subset(X),X).
pow_subset_operator(pow_subset(X),X).
pow_subset_operator(pow1_subset(X),X).
Called:
Name: check_all_finite/2 |
Module: well_def_prover |
prove_negated_po(falsity,_,falsity) :- !.
prove_negated_po(disjunct(A,B),Hyp,negdisj(T1,T2)) :- !,
(prove_negated_po(A,Hyp,T1) -> prove_negated_po(B,Hyp,T2)).
prove_negated_po(conjunct(A,B),Hyp,negconj(T1,T2)) :- !, % could be generated by Rodin
(prove_negated_po(A,Hyp,T1) -> true
; prove_negated_po(B,Hyp,T2)). % we could add not(A) as hypothesis,
prove_negated_po(negation(Goal),Hyp,negation(PT)) :-!, prove_po(Goal,Hyp,PT).
prove_negated_po(OP,Hyp,negated_op(PT)) :- negate_op(OP,NOP), prove_po(NOP,Hyp,PT).
Calls:
Name: prove_po/3 |
Module: well_def_prover |
Name: negate_op/2 |
Module: foo_error |
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: true |
|
Name: ->/3 |
|
Name: ->/2 |
Called:
Name: prove_po/3 |
Module: well_def_prover |
prove_po(truth,_,truth).
prove_po(_NormTarget,hyp_rec(AVL,_),false_hyp) :- avl_fetch(falsity,AVL).
prove_po(NormTarget,hyp_rec(AVL,_),hyp) :- avl_fetch(NormTarget,AVL).
prove_po(member(X,Y),Hyps,mem(PT)) :- % Y is usually domain(Func)
simplify_expr(Y,Hyps,SY),
simplify_expr(X,Hyps,SX),
check_member_of_set(SY,SX,Hyps,PT).
prove_po(not_member(X,Y),Hyps,mem(PT)) :-
simplify_expr(Y,Hyps,SY),
simplify_expr(X,Hyps,SX),
check_not_member_of_set(SY,SX,Hyps,PT).
prove_po(finite(Set),Hyp,finite_set(PT)) :- check_finite(Set,Hyp,PT).
prove_po(not_equal(A,B),Hyp,not_equal) :-
simplify_expr(A,Hyp,SA),
simplify_expr(B,Hyp,SB),
check_not_equal(SA,SB,Hyp).
prove_po(equal(A,B),Hyp,equal) :- % not generated by our POG
simplify_expr(A,Hyp,SA),
simplify_expr(B,Hyp,SB),
check_equal(SA,SB,Hyp,_).
prove_po(greater(A,B),Hyp,PT) :- prove_po(less(B,A),Hyp,PT).
prove_po(greater_equal(A,B),Hyp,greater_equal) :- % print(check_leq(B,A)),nl,
check_leq(B,A,Hyp).
prove_po(less_equal(A,B),Hyp,less_equal) :-
check_leq(A,B,Hyp).
prove_po(less(A,B),Hyp,less) :-
check_leq(A,B,Hyp),!,
check_not_equal(A,B,Hyp).
prove_po(subset(A,B),Hyp,PT) :-
check_is_subset(A,B,Hyp,PT).
prove_po(subset_strict(A,B),Hyp,subset_strict(PT)) :-
check_is_subset_strict(A,B,Hyp,PT).
prove_po(not_subset_strict(A,B),Hyp,not_subset_strict(PT)) :-
check_not_is_subset_strict(A,B,Hyp,PT).
prove_po(not_subset(A,B),Hyp,not_subset(PT)) :-
check_not_subset(A,B,Hyp,PT).
prove_po(conjunct(A,B),Hyp,conj(T1,T2)) :- % generated by Rodin
prove_po(A,Hyp,T1),
!,
prove_po(B,Hyp,T2).
prove_po(disjunct(A,B),Hyp,conj(T1,T2)) :- % could be generated by Rodin
(% push_normalized_hyp(NotB,Hyp,Hyp2), % % OR_R rule allows to add not(B) as hypothesis
prove_po(A,Hyp,T1) -> true
; prove_po(B,Hyp,T2)). % OR_R rule allows to add not(A) as hypothesis, this is done in prove_sequent_goal
prove_po(implication(A,B),Hyp,imply(T2)) :- % generated by Rodin; now treated in prove_sequent_goal
% also generated for power_of_real
(prove_negated_po(A,Hyp,PT) -> T2=false_lhs(PT)
; debug_println(19,not_pushing_lhs_for_implication(A)),
%push_normalized_hyp(A,Hyp,Hyp2), % TODO: activate this
prove_po(B,Hyp,T2)
).
prove_po(exists([$(B0)],forall([$(X)],member($(X),Set),less_equal($(X),$(B0)))),Hyp,finite_max(PT)) :- X \= B0,
% generated by Rodin for max(Set)
debug_println(19,checking_finite_for_max(Set)),
check_finite(Set,Hyp,PT).
prove_po(exists([$(B0)],forall([$(X)],member($(X),Set),less_equal($(B0),$(X)))),Hyp,finite_min(PT)) :- X \= B0,
% generated by Rodin for min(Set)
debug_println(19,checking_finite_for_min(Set)),
check_finite(Set,Hyp,PT).
prove_po(negation(Goal),Hyp,negation(PT)) :- prove_negated_po(Goal,Hyp,PT).
Calls:
Name: prove_negated_po/3 |
Module: well_def_prover |
Name: check_finite/3 |
Module: well_def_prover |
Name: debug_println/2 |
Module: foo_error |
Name: \=/2 |
|
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: =/2 |
|
Name: ->/3 |
|
Name: true |
|
Name: ! |
|
Name: check_not_subset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_is_subset_strict/4 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
Name: check_not_equal/3 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
Name: check_equal/4 |
Module: well_def_prover |
Name: simplify_expr/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: avl_fetch/2 |
Module: foo_error |
Called:
| Module: well_def_prover | |
Name: prove_proof_obligation/5 |
Module: well_def_analyser |
Name: create_po/6 |
Module: well_def_analyser |
Name: prove_negated_po/3 |
Module: well_def_prover |
quick_not_occurs_check('$'(ID),Value) :- !, not_occurs(Value,ID).
quick_not_occurs_check(_,_).
Calls:
Name: not_occurs/2 |
Module: foo_error |
Name: ! |
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover |
rewrite_card_of_set(Set,Hyps,Size,Hyps2) :-
compute_card_of_set(Set,Hyps,Size,Hyps2),!.
rewrite_card_of_set(interval(1,Up),Hyps,Size,Hyps) :- !, % useful if Up is a symbolic expression
Size=Up.
rewrite_card_of_set(Set,Hyps,Size,Hyps2) :- rewrite_set_expression_exact(Set,Hyps,S2,Hyps1),
rewrite_card_of_set(S2,Hyps1,Size,Hyps2).
Calls:
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: =/2 |
|
Name: ! |
|
Name: compute_card_of_set/4 |
Module: well_def_prover |
Called:
Name: check_not_empty_set/2 |
Module: well_def_prover |
Name: rewrite_integer/4 |
Module: well_def_prover |
rewrite_integer(size(Seq),Hyps,Size,Hyps2) :- % can happen for sequence POs, like restrict_front,tail
compute_card_of_set(Seq,Hyps,Size,Hyps2),!.
rewrite_integer(card(Seq),Hyps,Size,Hyps2) :- !, rewrite_card_of_set(Seq,Hyps,Size,Hyps2).
rewrite_integer(assertion_expression(_,_,Expr),Hyps,Expr,Hyps). % TO DO: add Predicate to Hyps?
rewrite_integer(add(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),
compute_integer(B,Hyps1,B1,Hyps2), number(B1),
Res is A1+B1.
rewrite_integer(unary_minus(A),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps2), number(A1),
Res is -A1.
rewrite_integer(minus(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),
compute_integer(B,Hyps1,B1,Hyps2), number(B1),
Res is A1-B1.
rewrite_integer(power_of(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),
compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 >=0,
% check if not too large:
(abs(A1) < 2 -> true
; A1=2 -> B1 =< 64
; A1 < 4294967296 -> B1 =< 2
; B1 =< 0
),
Res is A1 ^ B1.
rewrite_integer(modulo(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1),number(A1),
A1 >= 0,
compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 >0,
Res is A1 mod B1.
rewrite_integer(division(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),
compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 \= 0,
Res is A1 // B1. % Prolog division corresponds to B division
rewrite_integer(integer(X),Hyps,X,Hyps) :- integer(X), write(wd_unnormalised_integer(X)),nl. % should not happen
rewrite_integer(real(X),Hyps,Res,Hyps) :- atom(X), construct_real(X,term(floating(Res))).
rewrite_integer(convert_int_floor(RX),Hyps,X,Hyps1) :-
compute_integer(RX,Hyps,RX1,Hyps1), number(RX1), X is floor(RX1). %, print(rewr_floor(RX,X)),nl.
rewrite_integer(convert_int_ceiling(RX),Hyps,X,Hyps1) :-
compute_integer(RX,Hyps,RX1,Hyps1), number(RX1), X is ceiling(RX1).
rewrite_integer(convert_real(A),Hyps,RX,Hyps1) :-
compute_integer(A,Hyps,A1,Hyps1), integer(A1), RX is float(A1).
Calls:
Name: is/2 |
|
Name: integer/1 |
|
Name: compute_integer/4 |
Module: well_def_prover |
Name: number/1 |
|
Name: construct_real/2 |
Module: kernel_reals |
Name: atom/1 |
|
Name: nl |
|
Name: write/1 |
|
Name: \=/2 |
|
Name: >/2 |
|
Name: >=/2 |
|
Name: =</2 |
|
Name: </2 |
|
Name: ->/3 |
|
Name: =/2 |
|
Name: true |
|
Name: rewrite_card_of_set/4 |
Module: well_def_prover |
Name: ! |
|
Name: compute_card_of_set/4 |
Module: well_def_prover |
Called:
Name: compute_integer/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_leq/3 |
Module: well_def_prover |
Name: simplify_expr/3 |
Module: well_def_prover |
rewrite_local_loop_check(_,_,Value,HI,HI1) :- useful_value(Value),!,HI1=HI.
rewrite_local_loop_check(Term,ProverPredicate,_,Hyps,_) :- var(Hyps),!,
add_internal_error('Var hyps: ',rewrite_local_loop_check(Term,ProverPredicate,_,Hyps,_)),fail.
rewrite_local_loop_check(Term,ProverPredicate,_,hyp_rec(AVL,HInfos),hyp_rec(AVL,HInfos1)) :- !,
(Term='$'(ID) -> true ; ID=Term),
%(avl_fetch(rewritten(Term,ProverPredicate),HInfos) -> print(loop(Term,ProverPredicate)),nl,fail ; true),
\+ avl_fetch(rewritten(ID,ProverPredicate),HInfos),
avl_store(rewritten(ID,ProverPredicate),HInfos,true,HInfos1).
Calls:
Name: avl_store/4 |
Module: foo_error |
Name: avl_fetch/2 |
Module: foo_error |
Name: not/1 |
|
Name: =/2 |
|
Name: true |
|
Name: ->/3 |
|
Name: ! |
|
Name: fail |
|
Name: add_internal_error/2 |
Module: error_manager |
Name: var/1 |
|
Name: useful_value/1 |
Module: well_def_prover |
Called:
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_subset_interval/5 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: check_some_finite/3 |
Module: well_def_prover |
Name: check_leq_nr/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_member_of_domain/4 |
Module: well_def_prover |
Name: get_range_or_superset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_leq/3 |
Module: well_def_prover |
Name: check_finite/3 |
Module: well_def_prover |
Name: check_all_finite/2 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
Name: check_not_empty_set/2 |
Module: well_def_prover |
Name: check_subset_avl/3 |
Module: well_def_prover |
rewrite_set_expression_exact(domain(A),Hyps,Res,Hyps2) :- compute_exact_domain(A,Hyps,Dom,Hyps2),!,
%print(rewrote(domain(A))),nl, print(Dom),nl,
(A='$'(ID) -> not_occurs(Dom,ID) ; true), % prevent silly rewrites
Res=Dom.
rewrite_set_expression_exact(range(A),Hyps,Res,Hyps2) :- compute_exact_range(A,Hyps,Ran,Hyps2),!,
%print(rewrote(range(A))),nl, print(Ran),nl,
(A='$'(ID) -> not_occurs(Ran,ID) ; true), % prevent silly rewrites
Res=Ran.
rewrite_set_expression_exact(intersection(A,B),Hyps,Res,Hyps) :-
(is_empty_set_direct(A) -> Res=empty_set ; is_empty_set_direct(B) -> Res=empty_set).
rewrite_set_expression_exact(set_subtraction(A,B),Hyps,Res,Hyps) :-
(is_empty_set_direct(A) -> Res=empty_set ; is_empty_set_direct(B) -> Res=A).
rewrite_set_expression_exact(union(A,B),Hyps,Res,Hyps1) :-
(check_equal(A,B,Hyps,Hyps1) -> Res=A
; Hyps1=Hyps, merge_set_extensions(union(A,B),List,[]),
construct_set_extension(List,Hyps,Res)).
rewrite_set_expression_exact(value(closure(P,T,B)),Hyps,Res,Hyps) :- nonvar(P),
is_interval_closure(P,T,B,LOW,UP), number(LOW),number(UP),!,
Res = interval(LOW,UP).
rewrite_set_expression_exact(assertion_expression(_,_,Expr),Hyps,Expr,Hyps). % TO DO: add Predicate to Hyps ?
Calls:
Name: =/2 |
|
Name: ! |
|
Name: number/1 |
|
Name: is_interval_closure/5 |
Module: custom_explicit_sets |
Name: nonvar/1 |
|
| Module: well_def_prover | |
Name: merge_set_extensions/3 |
Module: well_def_prover |
Name: check_equal/4 |
Module: well_def_prover |
Name: ->/3 |
|
Name: is_empty_set_direct/1 |
Module: well_def_prover |
Name: ->/2 |
|
Name: true |
|
Name: not_occurs/2 |
Module: foo_error |
Name: compute_exact_range/4 |
Module: well_def_prover |
Name: compute_exact_domain/4 |
Module: well_def_prover |
Called:
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: rewrite_card_of_set/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: check_subset_avl/3 |
Module: well_def_prover |
Name: simplify_expr/3 |
Module: well_def_prover |
Name: check_subset_interval/5 |
Module: well_def_prover |
simple_value(Nr) :- number(Nr).
simple_value('$'(_)).
simple_value(boolean_true).
simple_value(boolean_false).
simple_value(record_field('$'(_),_)).
simple_value(value(_)).
simple_value(string(_)).
simple_value(function(F,_)) :- simple_value(F).
simple_value(couple(A,B)) :- simple_value(A), simple_value(B).
Calls:
Name: RECURSIVE_CALL/1 |
Module: well_def_prover |
Name: number/1 |
Called:
Name: get_range_or_superset/4 |
Module: well_def_prover |
Name: get_domain_or_superset/4 |
Module: well_def_prover |
simplify_expr(A,Hyps,Res) :-
rewrite_set_expression_exact(A,Hyps,A2,_),!, Res=A2.
simplify_expr(A,Hyps,Res) :-
rewrite_integer(A,Hyps,A2,_),!, Res=A2.
simplify_expr(record_field(rec(Fields),Field),Hyps,SExpr) :-
member(field(Field,Expr),Fields),!,
simplify_expr(Expr,Hyps,SExpr).
simplify_expr(domain(reverse(A)),_,range(A)) :- !.
simplify_expr(range(reverse(A)),_,domain(A)) :- !.
simplify_expr(E,_,E).
Calls:
Name: ! |
|
Name: RECURSIVE_CALL/3 |
Module: well_def_prover |
Name: member/2 |
|
Name: =/2 |
|
Name: rewrite_integer/4 |
Module: well_def_prover |
| Module: well_def_prover |
Called:
Name: prove_po/3 |
Module: well_def_prover |
Name: is_interval/4 |
Module: well_def_prover |
Name: check_is_subset/4 |
Module: well_def_prover |
singleton_set(set_extension([El]),El).
singleton_set(sorted_set_extension([El]),El).
Called:
Name: check_is_subset_strict/4 |
Module: well_def_prover |
Name: check_empty_set/3 |
Module: well_def_prover |
Name: check_not_empty_set/2 |
Module: well_def_prover |
Name: check_is_injective/2 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover |
sorted_set_extension_is_seq([],_).
sorted_set_extension_is_seq([couple(Nr,_)|T],Nr) :- N1 is Nr+1, sorted_set_extension_is_seq(T,N1).
Calls:
Name: RECURSIVE_CALL/2 |
Module: well_def_prover |
Name: is/2 |
Called:
| Module: well_def_prover |
subset_bin_transitivity_rule(partial_function(A1,A2),partial_function(B1,B2),A1,A2,B1,B2).
subset_bin_transitivity_rule(partial_injection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2).
subset_bin_transitivity_rule(partial_surjection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2).
subset_bin_transitivity_rule(partial_bijection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2).
subset_bin_transitivity_rule(total_function(A1,A2),partial_function(B1,B2),A1,A2,B1,B2).
subset_bin_transitivity_rule(total_injection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2).
subset_bin_transitivity_rule(total_surjection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2).
subset_bin_transitivity_rule(total_bijection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2).
subset_bin_transitivity_rule(image(A1,A2),image(B1,B2),A1,A2,B1,B2). % A1[A2] <: B1[B2] if A1 <: B1 & A2 <: B2
subset_bin_transitivity_rule(domain_restriction(A1,A2),domain_restriction(B1,B2),A1,A2,B1,B2). % A1 <| A2 <: B1 <| B2 if A1 <: B1 & A2 <: B2
subset_bin_transitivity_rule(range_restriction(A1,A2),range_restriction(B1,B2),A1,A2,B1,B2).
subset_bin_transitivity_rule(domain_subtraction(A1,A2),domain_subtraction(B1,B2),B1,A2,A1,B2). % A1 <<| A2 <: B1 <<| B2 if B1 <: A1 & A2 <: B2
subset_bin_transitivity_rule(range_subtraction(A1,A2),range_subtraction(B1,B2),A1,B2,A2,B1). % A1 |>> A2 <: B1|>> B2 if A1 <: B1 & B2 <: A2
Called:
Name: check_is_subset/4 |
Module: well_def_prover |
subset_transitivity_rule(pow_subset(A),pow_subset(B),A,B).
subset_transitivity_rule(pow1_subset(A),pow1_subset(B),A,B).
subset_transitivity_rule(pow1_subset(A),pow_subset(B),A,B).
subset_transitivity_rule(fin_subset(A),fin_subset(B),A,B).
subset_transitivity_rule(fin_subset(A),pow_subset(B),A,B).
subset_transitivity_rule(fin1_subset(A),fin1_subset(B),A,B).
subset_transitivity_rule(fin1_subset(A),fin_subset(B),A,B).
subset_transitivity_rule(fin1_subset(A),pow1_subset(B),A,B).
subset_transitivity_rule(fin1_subset(A),pow_subset(B),A,B).
subset_transitivity_rule(seq(A),seq(B),A,B).
subset_transitivity_rule(seq(A),partial_function(typeset,B),A,B).
subset_transitivity_rule(seq1(A),seq1(B),A,B).
subset_transitivity_rule(seq1(A),seq(B),A,B).
subset_transitivity_rule(seq1(A),partial_function(typeset,B),A,B).
subset_transitivity_rule(iseq(A),iseq(B),A,B).
subset_transitivity_rule(iseq(A),seq(B),A,B).
subset_transitivity_rule(iseq(A),partial_function(typeset,B),A,B).
subset_transitivity_rule(iseq1(A),iseq1(B),A,B).
subset_transitivity_rule(iseq1(A),iseq(B),A,B).
subset_transitivity_rule(iseq1(A),seq1(B),A,B).
subset_transitivity_rule(iseq1(A),seq(B),A,B).
subset_transitivity_rule(iseq1(A),partial_function(typeset,B),A,B).
subset_transitivity_rule(perm(A),perm(B),A,B).
subset_transitivity_rule(perm(A),iseq(B),A,B).
subset_transitivity_rule(perm(A),seq(B),A,B).
subset_transitivity_rule(perm(A),partial_function(typeset,B),A,B).
subset_transitivity_rule(range(A),domain(reverse(B)),A,B).
subset_transitivity_rule(range(A),range(B),A,B).
subset_transitivity_rule(range(reverse(A)),domain(B),A,B).
subset_transitivity_rule(domain(reverse(A)),range(B),A,B).
subset_transitivity_rule(domain(A),domain(B),A,B). % dom(A) <: dom(B) if A <:B
subset_transitivity_rule(domain(A),range(reverse(B)),A,B).
subset_transitivity_rule(reverse(A),reverse(B),A,B).
subset_transitivity_rule(rev(A),rev(B),A,B).
subset_transitivity_rule(identity(A),identity(B),A,B).
Called:
Name: check_is_subset/4 |
Module: well_def_prover |
sym_unify(A,B,A,B).
sym_unify(A,B,B,A).
Called:
| Module: well_def_prover | |
Name: check_not_equal/3 |
Module: well_def_prover |
try_get_set_of_possible_values(Nr,Hyps,R,Hyps) :- number(Nr),!,R=interval(Nr,Nr).
try_get_set_of_possible_values(X,Hyps,R,Hyps) :-
avl_fetch_binop_from_hyps_no_loop_check(X,equal,Hyps,Nr), number(Nr),!, % TODO: also treat is_explicit_value
R=interval(Nr,Nr).
try_get_set_of_possible_values(X,Hyps,XSet,Hyps2) :-
avl_fetch_worthwhile_mem_from_hyps(X,Hyps,XSet1,Hyps1),
(improve_integer_set_precision(X,XSet1,Hyps1,XSet,Hyps2)
-> true ; Hyps2=Hyps1, XSet=XSet1).
try_get_set_of_possible_values(X,Hyps,Res,Hyps3) :-
avl_fetch_equal_from_hyps(X,Hyps,X2,Hyps1),
quick_not_occurs_check(X,X2),
rewrite_local_loop_check(X,try_get_set_of_possible_values,X2,Hyps1,Hyps2),
(X2='$'(_) -> X = '$'(_) ; true), % avoid rewriting x -> card(...) -> x; TO DO: better cyclic equality prevention
try_get_set_of_possible_values(X2,Hyps2,Res,Hyps3), !.
try_get_set_of_possible_values(function(Func,_),Hyps,RangeSet,Hyps2) :- !,
get_range_or_superset(Func,Hyps,RangeSet,Hyps2).
try_get_set_of_possible_values(first(Seq),Hyps,RangeSet,Hyps2) :- !, % first(S) === S(1)
get_range_or_superset(Seq,Hyps,RangeSet,Hyps2).
try_get_set_of_possible_values(last(Seq),Hyps,RangeSet,Hyps2) :- !, % last(S) === S(size(S))
get_range_or_superset(Seq,Hyps,RangeSet,Hyps2).
try_get_set_of_possible_values(couple(A,B),Hyps,cartesian_product(SA,SB),Hyps2) :- !,
try_get_set_of_possible_values(A,Hyps,SA,Hyps1),
try_get_set_of_possible_values(B,Hyps1,SB,Hyps2).
try_get_set_of_possible_values(max(set_extension([V1,V2|_])),H,'NATURAL',H) :- % max({x,-x}) >= 0
( V1 = unary_minus(V2), \+ number(V1) -> true
; V2 = unary_minus(V1), \+ number(V2) -> true), !. % instead of NATURAL we could try and infer values for V1/V2
try_get_set_of_possible_values(max(Set),H,Set,H).
try_get_set_of_possible_values(min(Set),H,Set,H).
try_get_set_of_possible_values(mu(Set),H,Set,H).
try_get_set_of_possible_values(max_int,H,'NATURAL1',H).
try_get_set_of_possible_values(value(avl_set(A1)),Hyps,value(avl_set(A2)),Hyps) :- !,
expand_and_convert_to_avl_set([avl_set(A1)],A2,get_set_of_possible_values,'WD(?)').
try_get_set_of_possible_values(add(X,Y),Hyps,Set,Hyps2) :-
add_with_number(add(X,Y),A,Nr),
try_get_set_of_possible_values(A,Hyps,ValA,Hyps2),
add_to_value_set(ValA,Nr,Set),!.
try_get_set_of_possible_values(minus(A,Nr),Hyps,Set,Hyps2) :- number(Nr), Nr1 is -Nr,
try_get_set_of_possible_values(A,Hyps,ValA,Hyps2),
add_to_value_set(ValA,Nr1,Set),!.
try_get_set_of_possible_values(Seq,Hyps,Set,Hyps) :-
infer_sequence_type_of_expr(Seq,Hyps,SeqType),!,
(SeqType=seq1 -> Set=seq1(typeset) ; Set=seq(typeset)). % TO DO: examine type of list elements
try_get_set_of_possible_values(X,Hyps,XSet,Hyps2) :-
avl_fetch_binop_from_hyps(X,greater_equal,Hyps,Low,Hyps1), !,
(avl_fetch_binop_from_hyps(X,less_equal,Hyps1,Up,Hyps2) -> XSet = interval(Low,Up)
; Low=0 -> XSet = 'NATURAL', Hyps2=Hyps1
; number(Low),Low>0 -> XSet= 'NATURAL1', Hyps2=Hyps1). % TO DO: improve precision
try_get_set_of_possible_values(X,Hyps,XSet,Hyps2) :-
rewrite_integer(X,Hyps,X2,Hyps1),!,
try_get_set_of_possible_values(X2,Hyps1,XSet,Hyps2).
try_get_set_of_possible_values(size(A),Hyps,XSet,Hyps) :-
(check_not_empty_set(A,Hyps) -> XSet = 'NATURAL1' ; XSet='NATURAL').
try_get_set_of_possible_values(card(A),Hyps,XSet,Hyps) :-
(check_not_empty_set(A,Hyps) -> XSet = 'NATURAL1' ; XSet='NATURAL').
try_get_set_of_possible_values(if_then_else(_,A,B),Hyps,R,Hyps) :-
(try_get_set_of_possible_values(A,Hyps,AV,Hyps1)
-> try_get_set_of_possible_values(B,Hyps1,BV,Hyps2)),
construct_union(AV,BV,Hyps2,R).
try_get_set_of_possible_values(modulo(A,B),Hyps1,XSet,Hyps2) :-
number(B), B>0,
B1 is B-1,
XSet1 = interval(0,B1), % value of A mod B must be in 0..B1
% note: this also holds in z_or_tla_minor_mode, we have (-3) mod 2 = 1
(try_get_set_of_possible_values(A,Hyps1,XSet2,Hyps2),
maximal_value(XSet2,Up)
-> intersect_sets(XSet1,interval(0,Up),XSet)
% we were able to reduce the interval further by finding possible upper-bound for A
% we could call improve_upper_bound
; Hyps2=Hyps1, XSet=XSet1).
Calls:
Name: =/2 |
|
Name: intersect_sets/3 |
Module: well_def_prover |
Name: maximal_value/2 |
Module: well_def_prover |
Name: RECURSIVE_CALL/4 |
Module: well_def_prover |
Name: ->/3 |
|
Name: is/2 |
|
Name: >/2 |
|
Name: number/1 |
|
Name: construct_union/4 |
Module: well_def_prover |
Name: ->/2 |
|
Name: check_not_empty_set/2 |
Module: well_def_prover |
Name: ! |
|
Name: rewrite_integer/4 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
Name: add_to_value_set/3 |
Module: well_def_prover |
Name: add_with_number/3 |
Module: well_def_prover |
| Module: custom_explicit_sets | |
Name: true |
|
Name: not/1 |
|
Name: get_range_or_superset/4 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: quick_not_occurs_check/2 |
Module: well_def_prover |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover | |
| Module: well_def_prover |
Called:
Name: check_is_sequence/3 |
Module: well_def_prover |
Name: check_leq/3 |
Module: well_def_prover |
Name: check_member_of_set/4 |
Module: well_def_prover |
Name: check_not_equal/3 |
Module: well_def_prover |
| Module: well_def_prover | |
Name: get_range_or_superset/4 |
Module: well_def_prover |
try_improve_interval(interval(OldLow,OldUp),X,Hyps1,interval(NewLow,NewUp),Hyps2) :- !,
improve_interval(X,OldLow,OldUp,Hyps1,NewLow,NewUp,Hyps2).
try_improve_interval(Set,_,Hyps,Set,Hyps).
Calls:
Name: improve_interval/7 |
Module: well_def_prover |
Name: ! |
Called:
| Module: well_def_prover |
typing_predicate_for(ID1,AllArgs,member('$'(ID1),Set1),Set1) :- l_not_occurs(Set1,AllArgs).
typing_predicate_for(ID1,AllArgs,subset('$'(ID1),SSet1),pow_subset(SSet1)) :- l_not_occurs(SSet1,AllArgs).
Calls:
Name: l_not_occurs/2 |
Module: well_def_prover |
useful_value(Value) :- number(Value).
useful_value(interval(A,B)) :- number(A), number(B).
useful_value(value(_)).
Calls:
Name: number/1 |
Called:
| Module: well_def_prover | |
| Module: well_def_prover |
worth_rewriting_with_equal('$'(_)).
worth_rewriting_with_equal(record_field('$'(_),_)).
worth_rewriting_with_equal(couple(_,_)).
worth_rewriting_with_equal(size(_)).
worth_rewriting_with_equal(card(_)).
worth_rewriting_with_equal(function(_,_)).
Called:
| Module: well_def_prover |