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-trm i:term, i:string, i:option int.
7+ main-trm T STgt Depth :- coq.term->gref T GR, main-gref GR STgt Depth.
8+
9+ pred main-str i:string, i:string, i:option int.
10+ main-str S STgt Depth :- coq.locate S GR, main-gref GR STgt Depth.
11+
12+ pred main-gref i:gref, i:string, i:option int.
13+ main-gref GR STgt Depth :- class-def (class _ GR _), !,
14+ private.mixins-in-structures [GR] MLSrc,
15+ main-from MLSrc STgt Depth.
16+ main-gref GR STgt Depth :-
17+ private.structures-on-gref GR SL,
18+ private.mixins-in-structures SL MLSrc,
19+ main-from MLSrc STgt Depth.
20+
21+ pred main-from i:list mixinname, i:string, i:option int.
22+ main-from MLSrc STgt Depth :-
23+ private.mixins-in-structures [{coq.locate STgt}] MLTgt,
24+ private.list-diff MLTgt MLSrc ML,
25+ if (ML = []) (coq.say "HB: nothing to do.") (main-from.aux MLSrc ML Depth).
26+ main-from.aux MLSrc ML (some Depth) :- main-increase-depth MLSrc ML Depth false.
27+ main-from.aux MLSrc ML none :- main-increase-depth MLSrc ML 3 true.
28+
29+ pred main-increase-depth i:list mixinname, i:list mixinname, i:int, i:prop.
30+ main-increase-depth MLSrc ML Depth AutoIncrease :-
31+ private.paths-from-for-step MLSrc ML Depth R,
32+ if (not (R = [])) (private.pp-solutions R)
33+ (if AutoIncrease
34+ (Depth' is Depth + 1,
35+ coq.say "HB: no solution found at depth" Depth "looking at depth" Depth',
36+ main-increase-depth MLSrc ML Depth' true)
37+ (coq.error "HB: no solution found, try to increase search depth.")).
38+
39+
40+ /* ------------------------------------------------------------------------- */
41+ /* ----------------------------- private code ------------------------------ */
42+ /* ------------------------------------------------------------------------- */
43+
44+ namespace private {
45+
46+ shorten coq.pp.{ v , hov , spc , str , box , glue }.
47+
48+ % L1 \subseteq L2
49+ pred incl i:list A, i:list A.
50+ incl L1 L2 :- std.forall L1 (std.mem L2).
51+
52+ % R = L1 \ L2
53+ pred list-diff i:list A, i:list A, o:list A.
54+ list-diff L1 L2 R :- std.filter L1 (about.not1 (std.mem L2)) R.
55+
56+ % R = L1 U L2
57+ pred union i:list A, i:list A, o:list A.
58+ union L1 L2 R :-
59+ std.fold L2 L1 (x\l\l'\if (std.mem l x) (l' = l) (l' = [x|l])) R.
60+
61+ pred insert-sorted i:(A -> A -> prop), i:A, i:list A, o:list A.
62+ insert-sorted _ X [] [X] :- !.
63+ insert-sorted Rel X [Y|T] [X,Y|T] :- Rel X Y, !.
64+ insert-sorted Rel X [Y|T] [Y|T'] :- insert-sorted Rel X T T', !.
65+
66+ pred lt-gref i:gref, i:gref.
67+ lt-gref X Y :-
68+ gref->modname_short X "." SX, gref->modname_short Y "." SY, !, SX s< SY.
69+
70+ pred size-order i:(list A -> list A -> prop), i:list A, i:list A.
71+ size-order Rel L1 L2 :-
72+ std.length L1 S1, std.length L2 S2, !, (S1 i< S2; (S1 = S2, !, Rel L1 L2)).
73+
74+ pred lexi-order i:list gref, i:list gref.
75+ lexi-order [] [].
76+ lexi-order [X1|_] [X2|_] :- lt-gref X1 X2.
77+ lexi-order [X|T1] [X|T2] :- lexi-order T1 T2.
78+
79+ % [structures-on-gref GR ML] list structures [GR] is equipped with
80+ pred structures-on-gref i:gref, o:list structure.
81+ structures-on-gref GR SL :-
82+ std.filter {coq.CS.db-for _ (cs-gref GR)} (about.not1 about.unif-hint?) LV,
83+ std.map LV structures-on-gref.aux SL.
84+ structures-on-gref.aux (cs-instance _ _ GR) F :-
85+ coq.prod-tgt->gref {coq.env.typeof GR} F, class-def (class _ F _).
86+
87+ % [mixins-in-structures SL ML] list mixins in structures [SL]
88+ pred mixins-in-structures i:list structure, o:list mixinname.
89+ mixins-in-structures SL ML :- std.fold SL [] mixins-in-structures.aux ML.
90+ mixins-in-structures.aux F L L' :-
91+ class-def (class _ F MLWP), union L {list-w-params_list MLWP} L'.
92+
93+ % a type to store a factory along with the mixins it depends on
94+ % and the mixins it provides
95+ kind factory_deps_prov type.
96+ type fdp factoryname -> list mixinname -> list mixinname -> factory_deps_prov.
97+
98+ % get all available factories in the above type
99+ pred list_factories o:list factory_deps_prov.
100+ list_factories FL :-
101+ std.map-filter {std.findall (factory-constructor _ _)} list_factories.aux FL.
102+ list_factories.aux (factory-constructor F _) (fdp F DML PML) :-
103+ list-w-params_list {gref-deps F} DML,
104+ list-w-params_list {factory-provides F} PML.
105+
106+ % [paths-from-for-step MLSrc ML K R] returns in [R] a list of sequences
107+ % of at most [K] factories that could, starting from mixins [MLSrc],
108+ % build exactly the mixins [ML]
109+ pred paths-from-for-step i:list mixinname, i:list mixinname, i:int,
110+ o:list (list factoryname).
111+ paths-from-for-step MLSrc ML K R :-
112+ std.filter {list_factories} (fd\sigma pml\fd = fdp _ _ pml, incl pml ML) FL,
113+ paths-from-for-step-using MLSrc ML K [] [] FL _ R.
114+
115+ % [paths-from-for-step-using MLSrc ML K Pre KnownPre FL KnownPre' R]
116+ % same as [paths-from-for-step MLSrc ML K R] using only factories in [FL]
117+ % [Pre] is a (sorted) prefix that is looked into the list of known (sorted)
118+ % prefixes [KnownPre] to avoid generating identical solutions up to permutations
119+ pred paths-from-for-step-using i:list mixinname, i:list mixinname, i:int,
120+ i:list factoryname, i:list (list factoryname), i:list factory_deps_prov,
121+ o:list (list factoryname), o:list (list factoryname).
122+ paths-from-for-step-using _ _ K _ KnownPre _ KnownPre [] :- K i< 0.
123+ paths-from-for-step-using _ _ _ Pre KnownPre _ KnownPre [] :-
124+ std.mem KnownPre Pre, !.
125+ paths-from-for-step-using _ [] _ Pre KnownPre _ [Pre|KnownPre] [[]] :- !.
126+ paths-from-for-step-using MLSrc ML K Pre KnownPre FL [Pre|KnownPre'] R :-
127+ K' is K - 1,
128+ std.filter FL (p\sigma dml\p = fdp _ dml _, incl dml MLSrc) FLdep,
129+ std.fold FLdep (pr KnownPre [])
130+ (paths-from-for-step-using.aux MLSrc ML FL K' Pre)
131+ (pr KnownPre' R).
132+ paths-from-for-step-using.aux MLSrc ML FL' K' Pre (fdp F _ MLF) (pr KnPre L)
133+ (pr KnPre' R) :-
134+ std.append MLSrc MLF MLSrc',
135+ list-diff ML MLF ML',
136+ insert-sorted lt-gref F Pre Pre',
137+ std.filter FL' (p\sigma pml\p = fdp _ _ pml, incl pml ML') FML',
138+ paths-from-for-step-using MLSrc' ML' K' Pre' KnPre FML' KnPre' R',
139+ std.map R' (l\r\r = [F|l]) R'',
140+ std.append L R'' R.
141+
142+ pred pp-solutions i:list (list factoryname).
143+ pp-solutions LLF :-
144+ std.sort LLF (size-order lexi-order) SLLF,
145+ % format
146+ PpSolutions = box (v 4) [
147+ str "HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):",
148+ {about.bulletize SLLF pp-solution}],
149+ % print
150+ coq.say {coq.pp->string PpSolutions},
151+ coq.say.
152+
153+ pred pp-solution i:list factoryname o:coq.pp.
154+ pp-solution L (box (hov 0) PLS) :-
155+ std.map L about.pp-module PL,
156+ std.intersperse (glue [str ";", spc]) PL PLS.
157+
158+ }}
0 commit comments