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
142
143
144
145
146
147
148
149
150
151
152
|
/* Hierarchy Builder: algebraic hierarchies made easy
This software is released under the terms of the MIT license */
namespace builders {
pred begin i:context-decl.
begin CtxSkel :- std.do! [
std.assert!(coq.next-synterp-action (begin-module Name)) "synterp code did not open module",
if-verbose (coq.say {header} "begin module for builders"),
log.coq.env.begin-module Name none,
builders.private.factory CtxSkel IDF GRF,
% the Super module to access operations/axioms shadowed by the ones in the factory
if-verbose (coq.say {header} "begin module Super"),
log.coq.env.begin-module "Super" none,
if (GRF = indt FRecord) (std.do! [
std.forall {coq.env.projections FRecord}
builders.private.declare-shadowed-constant,
]) true,
if-verbose (coq.say {header} "ended module Super"),
log.coq.env.end-module-name "Super" _,
log.coq.env.begin-section Name,
if-verbose (coq.say {header} "postulating factories"),
builders.private.postulate-factories Name IDF CtxSkel,
].
}
% "end" is a keyword, be put it in the namespace by hand
pred builders.end.
builders.end :- std.do! [
current-mode (builder-from _ _ _ ModName),
log.coq.env.end-section-name ModName,
findall-builders LFIL,
std.fold LFIL [] builders.private.declare-1-builder Clauses,
if (Clauses = [])
(coq.error "No builders to declare, did you forget HB.instance?")
true,
std.findall (abbrev-to-export F_ N_ A_) ExportClauses,
coq.env.current-path CurModPath,
std.filter ExportClauses (export.private.abbrev-in-module CurModPath) ExportClausesFiltered,
% TODO: Do we need this module?
std.assert!(coq.next-synterp-action (begin-module Name)) "synterp code did not open module",
log.coq.env.begin-module Name none,
acc-clauses current Clauses,
acc-clauses current ExportClausesFiltered,
% Clauses => ExportClausesFiltered => current-mode no-builder =>
% instance.declare-factory-sort-factory GR,
log.coq.env.end-module-name Name Exports,
log.coq.env.end-module-name ModName _,
export.module {calc (ModName ^ "." ^ Name)} Exports,
].
/* ------------------------------------------------------------------------- */
/* ----------------------------- private code ------------------------------ */
/* ------------------------------------------------------------------------- */
pred factory.cdecl->w-mixins i:context-decl, o:w-mixins context-decl.
namespace builders.private {
% [declare-1-builder (builder _ F M B) From MoreFrom] Given B of type FB, it
% declares all the new builders F to M via B.
% From holds the (from F Mi Bi) new clauses during folding.
pred declare-1-builder i:builder, i:list prop, o:list prop.
declare-1-builder (builder _ SrcFactory TgtMixin _) FromClauses FromClauses :- (FromClauses => from SrcFactory TgtMixin _), !,
if-verbose (coq.say {header} "skipping duplicate builder from"
{nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}).
declare-1-builder (builder _ SrcFactory TgtMixin B) FromClauses [from SrcFactory TgtMixin B|FromClauses] :-
if-verbose (coq.say {header} "declare builder from"
{nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}).
% We add breviations for all constants what will be shadowed by projections
% if the factory.
pred declare-shadowed-constant i:option constant.
declare-shadowed-constant none.
declare-shadowed-constant (some C) :-
coq.gref->id (const C) Id,
std.forall {coq.locate-all Id} (declare-shadowed-located Id).
pred declare-shadowed-located i:string, i:located.
declare-shadowed-located Id (loc-gref GR) :-
@global! => log.coq.notation.add-abbreviation Id 0 (global GR) ff _.
declare-shadowed-located Id (loc-abbreviation Abbrev) :-
coq.notation.abbreviation-body Abbrev NArgs T,
@global! => log.coq.notation.add-abbreviation Id NArgs T ff _.
pred postulate-factory-abbrev i:term, i:list term, i:id, i:factoryname, o:term.
postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [
std.assert-ok! (factory-alias->gref Falias F) "HB",
phant-abbrev F _ Fabv,
coq.notation.abbreviation Fabv {std.append Params [TheType]} Package,
Msg is "Unable to declare factory " ^ Name,
std.assert-ok! (coq.typecheck-ty Package _) Msg,
log.coq.env.add-section-variable-noimplicits Name Package C,
TheFactory = global (const C),
].
% Only record fields can be exported as operations.
pred define-factory-operations i:term, i:list term, i:term, i:gref.
define-factory-operations TheType Params TheFactory (indt I) :- !,
coq.env.indt I _ NIParams _ _ _ _,
NHoles is NIParams - 1 - {std.length Params},
coq.env.projections I PL,
std.forall PL (define-factory-operation TheType Params TheFactory NHoles).
define-factory-operations _ _ _ _.
pred define-factory-operation i:term, i:list term, i:term, i:int, i:option constant.
define-factory-operation _ _ _ _ none.
define-factory-operation TheType Params TheFactory NHoles (some P) :-
coq.mk-n-holes NHoles Holes,
std.append Holes [TheFactory] Holes_Factory,
std.append Params [TheType|Holes_Factory] Args,
T = app[global (const P)|Args],
std.assert-ok! (coq.typecheck T _) "Illtyped applied factory operation",
coq.gref->id (const P) Name,
@local! => log.coq.notation.add-abbreviation Name 0 T ff _.
pred factory i:context-decl, o:string, o:gref.
factory (context-item IDF _ T _ _\ context-end) IDF GR :- !,
coq.safe-dest-app T (global GR) _.
factory (context-item _ _ _ _ R) IDF GR :- !, pi x\ factory (R x) IDF GR.
factory _ _ _ :- !, coq.error "the last context item is not a factory".
pred postulate-factories i:id, i:string, i:context-decl.
postulate-factories ModName IDF CDecl :- std.do! [
factory.cdecl->w-mixins CDecl (pr FLwP _),
context.declare.params-key FLwP ParamsSection FKey FLwA,
std.assert! (FLwA = [triple GRF _ _])
"HB: cannot declare builders for more than one factory at a time",
gref-deps GRF DepswPRaw,
context.declare.mixins FKey ParamsSection DepswPRaw _ _ _,
std.map ParamsSection triple_2 FParams,
postulate-factory-abbrev FKey FParams IDF GRF TheFactory,
define-factory-operations FKey FParams TheFactory GRF,
acc-clause current (current-mode (builder-from FKey TheFactory GRF ModName)),
].
}
|
