1+ /* Hierarchy Builder: algebraic hierarchies made easy
2+ This software is released under the terms of the MIT license */
3+
4+ namespace howto {
5+
6+ pred main i:string, i:string, i:int.
7+ main ST STgt Depth :-
8+ private.mixins-on-string ST MLSrc,
9+ private.mixins-in-string STgt MLTgt,
10+ private.list-diff MLTgt MLSrc ML,
11+ if (ML = []) (coq.say "HB: nothing to do.")
12+ (private.paths-from-for-step MLSrc ML Depth R,
13+ if (R = [])
14+ (coq.error "HB: no solution found, try to increase search depth.")
15+ (private.pp-solutions R)).
16+
17+
18+ /* ------------------------------------------------------------------------- */
19+ /* ----------------------------- private code ------------------------------ */
20+ /* ------------------------------------------------------------------------- */
21+
22+ namespace private {
23+
24+ shorten coq.pp.{ v , hov , spc , str , box , glue }.
25+
26+ % L1 \subseteq L2
27+ pred incl i:list A, i:list A.
28+ incl L1 L2 :- std.forall L1 (std.mem L2).
29+
30+ % R = L1 \ L2
31+ pred list-diff i:list A, i:list A, o:list A.
32+ list-diff L1 L2 R :- std.filter L1 (about.not1 (std.mem L2)) R.
33+
34+ % R = L1 U L2
35+ pred union i:list A, i:list A, o:list A.
36+ union L1 L2 R :-
37+ std.fold L2 L1 (x\l\l'\if (std.mem l x) (l' = l) (l' = [x|l])) R.
38+
39+ % [mixins-on-string S ML] list mixins in structures [S] is equipped with
40+ pred mixins-on-string i:string, o:list mixinname.
41+ mixins-on-string S ML :-
42+ coq.locate S GR,
43+ std.filter {coq.CS.db-for _ (cs-gref GR)} (about.not1 about.unif-hint?) LV,
44+ std.fold LV [] mixins-on-string.aux ML.
45+ mixins-on-string.aux (cs-instance _ _ GR) L L' :-
46+ coq.prod-tgt->gref {coq.env.typeof GR} F,
47+ class-def (class _ F MLWP),
48+ union L {list-w-params_list MLWP} L'.
49+
50+ % [mixins-in-string S ML] list mixins contained in structure [S]
51+ pred mixins-in-string i:string, o:list mixinname.
52+ mixins-in-string S ML :-
53+ coq.locate S GR, class-def (class _ GR MLwP), list-w-params_list MLwP ML.
54+
55+ % a type to store a factory along with the mixins it depends on
56+ % and the mixins it provides
57+ kind factory_deps_prov type.
58+ type fdp factoryname -> list mixinname -> list mixinname -> factory_deps_prov.
59+
60+ % get all available factories in the above type
61+ pred list_factories o:list factory_deps_prov.
62+ list_factories FL :-
63+ std.map-filter {std.findall (factory-constructor _ _)} list_factories.aux FL.
64+ list_factories.aux (factory-constructor F _) (fdp F DML PML) :-
65+ list-w-params_list {gref-deps F} DML,
66+ list-w-params_list {factory-provides F} PML.
67+
68+ % [paths-from-for-step MLSrc ML K R] returns in [R] a list of sequences
69+ % of at most [K] factories that could, starting from mixins [MLSrc],
70+ % build exactly the mixins [ML]
71+ pred paths-from-for-step i:list mixinname, i:list mixinname, i:int,
72+ o:list (list factoryname).
73+ paths-from-for-step MLSrc ML K R :-
74+ std.filter {list_factories} (fd\sigma pml\fd = fdp _ _ pml, incl pml ML) FL,
75+ paths-from-for-step-using MLSrc ML K FL R.
76+
77+ % [paths-from-for-step-using MLSrc ML K FL R]
78+ % same as [paths-from-for-step MLSrc ML K R] using only factories in [FL]
79+ pred paths-from-for-step-using i:list mixinname, i:list mixinname, i:int,
80+ i:list factory_deps_prov, o:list (list factoryname).
81+ paths-from-for-step-using _ _ K _ [] :- K i< 0.
82+ paths-from-for-step-using _ [] _ _ [[]] :- !.
83+ paths-from-for-step-using MLSrc ML K FL R :-
84+ K' is K - 1,
85+ std.filter FL (p\sigma dml\p = fdp _ dml _, incl dml MLSrc) FLdep,
86+ std.fold FLdep [] (paths-from-for-step-using.aux MLSrc ML FL K') R.
87+ paths-from-for-step-using.aux MLSrc ML FL' K' (fdp F _ MLF) L R :-
88+ std.append MLSrc MLF MLSrc',
89+ list-diff ML MLF ML',
90+ std.filter FL' (p\sigma pml\p = fdp _ _ pml, incl pml ML') FML',
91+ paths-from-for-step-using MLSrc' ML' K' FML' R',
92+ std.map R' (l\r\r = [F|l]) R'',
93+ std.append L R'' R.
94+
95+ pred pp-solutions i:list (list factoryname).
96+ pp-solutions LLF :-
97+ std.sort LLF
98+ (l1\l2\sigma s1 s2\std.length l1 s1, std.length l2 s2, s1 i=< s2)
99+ SLLF,
100+ % format
101+ PpSolutions = box (v 4) [
102+ str "HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):",
103+ {about.bulletize SLLF pp-solution}],
104+ % print
105+ coq.say {coq.pp->string PpSolutions},
106+ coq.say.
107+
108+ pred pp-solution i:list factoryname o:coq.pp.
109+ pp-solution L (box (hov 0) PLS) :-
110+ std.map L about.pp-module PL,
111+ std.intersperse (glue [str ";", spc]) PL PLS.
112+
113+ }}
0 commit comments