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
|
/* Hierarchy Builder: algebraic hierarchies made easy
This software is released under the terms of the MIT license */
pred export.any i:id.
export.any S :-
coq.locate-all S L,
if (L = []) (coq.error "HB: cannot locate" S) true,
if (L = [X]) (export.any.aux S X) (coq.error "HB:" S "is ambiguous:" L).
export.any.aux S (loc-gref GR) :- export.abbrev S GR.
export.any.aux S (loc-modpath MP) :- export.module S MP.
export.any.aux S X :- coq.error "HB:" S "denotes" X "which is not supported for exporting".
% [export.module Module] exports a Module now adds it to the collection of
% modules to export in the end of the current enclosing module,
% by the command HB.Exports
% CAVEAT: "module" is a keyword, we put it in the namespace by hand
pred export.module i:id, i:modpath.
export.module NiceModule Module :- !,
log.coq.env.export-module NiceModule Module,
coq.env.current-library File,
acc-clause current (module-to-export File NiceModule Module).
pred export.abbrev i:id, i:gref.
export.abbrev NiceName GR :- !,
coq.env.current-library File,
acc-clause current (abbrev-to-export File NiceName GR).
pred export.clause i:prop.
export.clause Clause :- !,
coq.env.current-library File,
acc-clauses current [Clause, clause-to-export File Clause].
pred export.reexport-all-modules-and-CS i:option string.
export.reexport-all-modules-and-CS Filter :- std.do! [
coq.env.current-library File,
export.private.compute-filter Filter MFilter,
if-verbose (coq.say {header} "exporting under the module path" MFilter),
% NODE: std.list-uniq is for coq < 8.13
std.findall (module-to-export File NiceModule_ Module_) ModsCL,
std.filter {std.list-uniq ModsCL} (export.private.module-in-module MFilter) ModsCLFiltered,
std.map ModsCLFiltered module-to-export_module-nice NiceMods,
std.map ModsCLFiltered module-to-export_module Mods,
if-verbose (coq.say {header} "exporting modules" NiceMods),
std.forall2 NiceMods Mods log.coq.env.export-module,
std.findall (instance-to-export File NiceInstance_ Const_) InstCL,
std.filter {std.list-uniq InstCL} (export.private.instance-in-module MFilter) InstCLFiltered,
std.map InstCLFiltered instance-to-export_instance Insts,
if-verbose (coq.say {header} "exporting CS instances" Insts),
std.forall Insts log.coq.CS.declare-instance,
std.findall (abbrev-to-export File NiceAbbrev_ GR_) InstAbbL,
std.filter {std.list-uniq InstAbbL} (export.private.abbrev-in-module MFilter) InstAbbLFiltered,
std.map InstAbbLFiltered abbrev-to-export_name AbbNames,
std.map InstAbbLFiltered abbrev-to-export_body AbbBodies,
if-verbose (coq.say {header} "exporting Abbreviations" AbbNames),
std.forall2 AbbNames AbbBodies (n\b\@global! => log.coq.notation.add-abbreviation n 0 b ff _),
std.findall (clause-to-export File Clause_) ClausesL,
if-verbose (coq.say {header} "exporting Clauses" Clauses),
std.map ClausesL clause-to-export_clause Clauses,
acc-clauses current Clauses
].
namespace export.private {
pred abbrev-in-module i:list string, i:prop.
abbrev-in-module PM (abbrev-to-export _ _ GR) :-
coq.gref->path GR PC,
std.appendR PM _ PC. % sublist
pred module-in-module i:list string, i:prop.
module-in-module PM (module-to-export _ _ M) :-
coq.modpath->path M PC,
std.appendR PM _ PC. % sublist
pred instance-in-module i:list string, i:prop.
instance-in-module PM (instance-to-export _ _ C) :-
coq.gref->path (const C) PC,
std.appendR PM _ PC. % sublist
pred compute-filter i:option string, o:list string.
compute-filter none [].
compute-filter (some S) MFilter :- % S is a component of the current modpath
coq.env.current-path P,
rex_split "\\." S L,
compute-filter.aux P L MFilter, !.
compute-filter (some S) MFilter :-
coq.locate-module S M,
coq.modpath->path M MFilter.
compute-filter.aux [S|_] [S] [S] :- !.
compute-filter.aux [S|XS] [S|SS] [S|YS] :- compute-filter.aux XS SS YS.
compute-filter.aux [X|XS] L [X|YS] :- compute-filter.aux XS L YS.
}
|
