-
Notifications
You must be signed in to change notification settings - Fork 5
/
env_utils.pl
143 lines (115 loc) · 4.02 KB
/
env_utils.pl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
%%- -*-Mode: Prolog;-*--------------------------------------------------
%%
%% File : env_utils.pl
%%
%% Author: Josef Urban
%%
%% Prolog code for optimizing the MML order of articles,
%% tested only with SWI Prolog 5.2 now.
%% Top-level predicate is print_in_order/0.
%%------------------------------------------------------------------------
:- [utils].
%% Kind must be in theory_exts
load_theory_files1(Kind):-
atom(Kind),
theory_exts(Exts),
member(Kind, Exts),
mml_dir_atom(MMLDir),
concat_atom([MMLDir, '*.', Kind, '3'], Anames),
string_to_atom(WildCard, Anames),
expand_file_name(WildCard, Names),
load_files(Names,[silent(true)]).
:- abolish(dependents/2).
:- dynamic(dependents/2).
:- abolish(rec_dependents/2).
:- dynamic(rec_dependents/2).
make_dependents(A,D):-
theory(A,
[vocabularies(_),notations(X1),definitions(X2),
theorems(X3),schemes(X4),registrations(X5),
constructors(X6),requirements(X7)|_]),
flatten([X1,X2,X3,X4,X5,X6,X7],D1),
sort(D1,D), assert(dependents(A,D)).
depends(A,B):- dependents(A,D),member(B,D).
make_rec_dependents(A,R):- rec_dependents(A,R),!.
make_rec_dependents(A,R):-
dependents(A,D),
findall(BR,(member(B,D),make_rec_dependents(B,BR)),Rec),!,
flatten([D,Rec],R1),
sort(R1,R),
assert(rec_dependents(A,R)).
rec_depends(A,B):- rec_dependents(A,D),member(B,D).
date(A1,Date1):-
theory(A1,[_V1,_N1,_D1,_T1,_S1,_Reg1,_C1,_Req1,date([Date1|_])|_]),!.
date1(A1,Date1):-
theory(A1,[_V1,_N1,_D1,_T1,_S1,_Reg1,_C1,_Req1,date(Date1)|_]),!.
structural(cat_1):-!.
structural(graph_1):-!.
structural(incsp_1):-!.
structural(net_1):-!.
structural(petri):-!.
structural(qmax_1):-!.
structural(struct_0):-!.
structural(X):- flag(X,1,1),!.
structural(X):- flag(X,2,2),!,fail.
structural(X):-
flag(X,N,N),
% write(X:entered:N),nl,
% theory(X,Y),
% member(constructors(Cs),Y),
% member(A,Cs), % write(trying:A:for:X),nl,
rec_depends(X,A),
structural(A),!, % write(X:yes),nl,
flag(X,_,1),!.
structural(X):-
flag(X,_,2),!,
% write(X:no),nl,
fail.
assert_deps:-
all_articles(L),!,member(A,L), once(make_dependents(A,_)),fail.
assert_rec_deps:-
all_articles(L),!,member(A,L), once(make_rec_dependents(A,_)),fail.
assert_structural:-
all_articles(L),!,member(A,L), once(structural(A)),fail.
%% article A2 comes after A1, if it recursively depends on it
smaller1(A1,A2):- rec_dependents(A2,R1), member(A1,R1).
%% otherwise structural article A2 comes after nonstructural A1
smaller2(A1,A2):- structural(A2), not(structural(A1)).
%% otherwise article A2 comes after A1, if it is received later
smaller3(A1,A2):- date(A1,Date1), date(A2,Date2), Date1 < Date2.
%% otherwise article A2 comes after A1, if it has more recursive dependecies
smaller4(A1,A2):-
rec_dependents(A1,R1), rec_dependents(A2,R2),
length(R1,L1), length(R2,L2), L1 < L2.
%% otherwise do normal compare/3
smaller5(A1,A2):- compare(<,A1,A2).
%% A is minimal wrt a binary Pred among members of [H|T]
minimal(_,_,[]).
minimal(Pred,A,[H|T]):- G=..[Pred,H,A], not(G), minimal(Pred,A,T).
%% take minimal members of L1 wrt. smaller1, and put them to L2;
%% then select from L2 the minimal members wrt. smaller2, etc.
%% deterministic if only one element remains (this is true for smaller5)
least(L1,X):-
findall(A1,(member(A1,L1),minimal(smaller1,A1,L1)),L2),!,
findall(A2,(member(A2,L2),minimal(smaller2,A2,L2)),L3),!,
findall(A3,(member(A3,L3),minimal(smaller3,A3,L3)),L4),!,
findall(A4,(member(A4,L4),minimal(smaller4,A4,L4)),L5),!,
findall(A5,(member(A5,L5),minimal(smaller5,A5,L5)),L6),!,
% write([L2,L3,L4,L5,L6]),nl,
sort(L6,L7),member(X,L7),!.
order1([],[]):-!.
order1(In,[X|Rest]):-
least(In,X),!, write(X),nl,
delete(In,X,R1),!,
order1(R1,Rest).
initialize:-
declare_mptp_predicates,
load_theory_files1(evl),
(assert_deps;true),
(assert_rec_deps;true),
(assert_structural;true).
%% print all nonumerical articles, which are roots (nothing depends on them)
%% ##TEST: :- initialize,findall(A,(nonnumeric(A),not(depends(_,A))),S),length(S,N), print(S).
%% ##TEST: :- print_in_order.
print_in_order:-
initialize,all_articles(L),!,order1(L,_).