11/* license: GNU Lesser General Public License Version 2.1 or later */
22/* ------------------------------------------------------------------------- */
3+ pred string->coq-mode i:string, o:hint-mode.
4+ string->coq-mode "bang" mode-ground :- !.
5+ string->coq-mode "plus" mode-input :- !.
6+ string->coq-mode "minus" mode-output :- !.
7+ string->coq-mode "i" mode-input :- !.
8+ string->coq-mode "o" mode-output :- !.
9+ string->coq-mode A _ :- coq.error A "is not a valid mode".
310
4- pred bool->mode-term i:bool, o:pair argument_mode string.
5- % TODO: here every mode is declared to O;term.
6- % If you want to make it work as intended,
7- % replace the output of tt with "i:term"
8- :name "bool->mode-term"
9- bool->mode-term tt (pr in "term").
10- bool->mode-term ff (pr out "term").
11-
12- pred modes->string i:list bool, o:list (pair argument_mode string).
13- modes->string L S :-
14- std.map L bool->mode-term S.
15-
16- pred make-tc-modes i:int, o:list (pair argument_mode string).
17- make-tc-modes NB_args ModesStr :-
18- list-init NB_args (x\r\ r = ff) ModesBool,
19- modes->string ModesBool ModesStr.
20-
21- pred build-modes i:gref, o:list (pair argument_mode string).
22- build-modes ClassGr Modes :-
23- is-option-active {oTC-addModes},
24- coq.hints.modes ClassGr "typeclass_instances" ModesProv,
25- not (ModesProv = []),
26- coq.hints.modes ClassGr "typeclass_instances" ModesProv,
27- std.assert! (ModesProv = [HintModes]) "At the moment we only allow TC with one Hint Mode",
28- std.map {std.append HintModes [mode-output]} (x\r\ if (x = mode-output) (r = ff) (r = tt)) ModesBool,
29- modes->string ModesBool Modes.
30- build-modes ClassGr Modes :-
11+ pred coq-mode->elpi i:hint-mode, o:pair argument_mode string.
12+ :name "coq-mode->elpi"
13+ coq-mode->elpi mode-ground (pr in "term"). % approximation
14+ coq-mode->elpi mode-input (pr in "term").
15+ coq-mode->elpi mode-output (pr out "term").
16+
17+ pred modes-of-class i:gref, o:list (pair argument_mode string).
18+ modes-of-class ClassGr Modes :-
19+ coq.hints.modes ClassGr "typeclass_instances" CoqModesList,
20+ not (CoqModesList = []),
21+ std.assert! (CoqModesList = [HintModesFst]) "At the moment we only allow TC with one Hint Mode",
22+ std.append {std.map HintModesFst coq-mode->elpi} [pr out "term"] Modes.
23+ modes-of-class ClassGr Modes :-
3124 coq.env.typeof ClassGr ClassTy,
32- coq.count-prods ClassTy N',
33- N is N' + 1, % Plus one for the solution
34- make-tc-modes N Modes.
25+ N is {coq.count-prods ClassTy} + 1, % + 1 for the solution
26+ list-init N (x\r\ r = (pr out "term")) Modes.
3527
3628pred add-class-gr i:search-mode, i:gref.
37- add-class-gr SearchMode ClassGr :-
38- std.assert! (coq.TC.class? ClassGr ) "Only gref of type classes can be added as new predicates",
39- if (class ClassGr _ _) true
40- (build- modes ClassGr Modes,
41- gref->pred-name ClassGr PredName,
29+ add-class-gr SearchMode ClassGR :-
30+ std.assert! (coq.TC.class? ClassGR ) "Only gref of type classes can be added as new predicates",
31+ if (class ClassGR _ _) true
32+ (modes-of-class ClassGR Modes,
33+ gref->pred-name ClassGR PredName,
4234 coq.elpi.add-predicate "tc.db" _ PredName Modes,
43- add-tc-db _ _ (tc-mode ClassGr Modes),
44- @global! => coq.elpi.accumulate _ "tc.db" (clause _ _ (class ClassGr PredName SearchMode :- !) )).
35+ add-tc-db _ _ (tc-mode ClassGR Modes),
36+ @global! => add-tc-db _ _ (class ClassGR PredName SearchMode)).
4537
4638pred add-class-str i:search-mode, i:string.
47- add-class-str SearchMode TC_Name :-
48- coq.locate TC_Name TC_Gr,
49- add-class-gr SearchMode TC_Gr.
39+ add-class-str SearchMode ClassStr :-
40+ coq.locate ClassStr ClassGR,
41+ add-class-gr SearchMode ClassGR.
42+
43+ % Following are predicates for TC.declare
44+
45+ pred attr->deterministic o:search-mode.
46+ attr->deterministic deterministic :- get-option "deterministic" tt, !.
47+ attr->deterministic classic.
48+
49+ pred attr->modes o:list hint-mode.
50+ attr->modes CoqModes :-
51+ get-option "mode" L,
52+ std.map L get-key-from-option RawModes,
53+ std.map RawModes string->coq-mode CoqModes, !.
54+ attr->modes [].
55+
56+ pred get-key-from-option i:prop, o:string.
57+ get-key-from-option (get-option A tt) A :- !.
58+ get-key-from-option (get-option "i" ff) "o" :- !.
59+ get-key-from-option (get-option "o" ff) "i" :- !.
60+ get-key-from-option A _ :- coq.error A "should be an option".
61+
62+ pred declare-class-in-coq i:gref.
63+ declare-class-in-coq ClassGR :-
64+ attr->modes CoqModes,
65+ if (CoqModes = []) true
66+ (@global! => coq.hints.add-mode ClassGR "typeclass_instances" CoqModes),
67+ % CAVEAT: this triggers the observer
68+ coq.TC.declare-class ClassGR,
69+ attr->deterministic SearchMode,
70+ gref->pred-name ClassGR PredName,
71+ % HACK: we override the clauses added by the observer, since it does not know
72+ % the SearchMode.
73+ @global! => add-tc-db _ (after "0") (class ClassGR PredName SearchMode :- !).
74+
75+ pred declare-class i:indt-decl.
76+ declare-class D :- !,
77+ coq.env.add-indt D I,
78+ coq.parse-attributes {attributes}
79+ [ att "mode" attlist, att "deterministic" bool ] Opts,
80+ Opts => declare-class-in-coq (indt I).
0 commit comments