Skip to content

Commit 77262a5

Browse files
garesgares
authored
Merge pull request #863 from LPCIC/kill-fprop
Kill fprop
2 parents 7aecc41 + fab462c commit 77262a5

File tree

7 files changed

+55
-55
lines changed

7 files changed

+55
-55
lines changed

‎apps/tc/elpi/ho_compile.elpi‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -227,7 +227,7 @@ namespace tc {
227227
compile-ty L L1 P {neg IsPositive} PTy [] [] NewPrem,
228228
if (tc.class TC _ tc.deterministic _)
229229
(NewPrem' = std.once NewPrem)
230-
(NewPrem' = NewPrem),
230+
(NewPrem' = NewPrem), !,
231231
compile-ty L1 L2 ProofHd IsPositive ITy ProofTlR [NewPrem' | PremR] Clause.
232232
compile-premise L L1 _ _ ProofHd IsPositive ITy ProofTlR PremR Clause :-
233233
compile-ty L L1 ProofHd IsPositive ITy ProofTlR PremR Clause.
@@ -255,7 +255,7 @@ namespace tc {
255255
compile-ty L L1 ProofHd IsPositive (let _ Ty T Bo) ProofTlR PremR Clause :- !,
256256
if (IsPositive = tt)
257257
(Clause = (pi x\ C x), E = is-uvar)
258-
(clean-term Ty Ty', Clause = (pi x\ decl x N Ty' => C x), E = is-name),
258+
(clean-term Ty Ty', Clause = (pi x\ decl x N Ty' => C x), E = is-name), !,
259259
pi p\ sigma F NewPrem\
260260
(decl p N Ty' :- !) => (E p :- !) => (
261261
NewPrem = tc.link.unif-eq T p,

‎apps/tc/elpi/ho_link.elpi‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ namespace tc {
7171
(copy Y X :- !) => relocate Xs Ys T T'.
7272

7373
pred collect-store o:list prop.
74-
pred collect-store-aux i:list prop, o:list prop.
74+
func collect-store-aux list prop -> list prop.
7575

7676
collect-store L :- collect-store-aux [] L.
7777
collect-store-aux X L :- declare_constraint (collect-store-aux X L) [_].

‎builtin-doc/coq-builtin-synterp.elpi‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11,29 +11,29 @@ kind upoly-decl-cumul type.
1111
% -- Misc ---------------------------------------------------------
1212

1313
% [coq.info ...] Prints an info message
14-
external type coq.info variadic any fprop.
14+
external type coq.info variadic any (func).
1515

1616
% [coq.notice ...] Prints a notice message
17-
external type coq.notice variadic any fprop.
17+
external type coq.notice variadic any (func).
1818

1919
% [coq.say ...] Prints a notice message
20-
external type coq.say variadic any fprop.
20+
external type coq.say variadic any (func).
2121

2222
% [coq.debug ...] Prints a debug message
23-
external type coq.debug variadic any fprop.
23+
external type coq.debug variadic any (func).
2424

2525
% [coq.warn ...] Prints a generic warning message
26-
external type coq.warn variadic any fprop.
26+
external type coq.warn variadic any (func).
2727

2828
% [coq.warning Category Name ...]
2929
% Prints a warning message with a Name and Category which can be used
3030
% to silence this warning or turn it into an error. See coqc -w command
3131
% line option
32-
external type coq.warning string -> string -> variadic any fprop.
32+
external type coq.warning string -> string -> variadic any (func).
3333

3434
% [coq.error ...] Prints and *aborts* the program. It is a fatal error for
3535
% Elpi and Ltac
36-
external type coq.error variadic any fprop.
36+
external type coq.error variadic any (func).
3737

3838
% [coq.version VersionString Major Minor Patch] Fetches the version of Coq,
3939
% as a string and as 3 numbers

‎builtin-doc/coq-builtin.elpi‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -546,29 +546,29 @@ external symbol off : coercion-status = "1".
546546
% -- Misc ---------------------------------------------------------
547547

548548
% [coq.info ...] Prints an info message
549-
external type coq.info variadic any fprop.
549+
external type coq.info variadic any (func).
550550

551551
% [coq.notice ...] Prints a notice message
552-
external type coq.notice variadic any fprop.
552+
external type coq.notice variadic any (func).
553553

554554
% [coq.say ...] Prints a notice message
555-
external type coq.say variadic any fprop.
555+
external type coq.say variadic any (func).
556556

557557
% [coq.debug ...] Prints a debug message
558-
external type coq.debug variadic any fprop.
558+
external type coq.debug variadic any (func).
559559

560560
% [coq.warn ...] Prints a generic warning message
561-
external type coq.warn variadic any fprop.
561+
external type coq.warn variadic any (func).
562562

563563
% [coq.warning Category Name ...]
564564
% Prints a warning message with a Name and Category which can be used
565565
% to silence this warning or turn it into an error. See coqc -w command
566566
% line option
567-
external type coq.warning string -> string -> variadic any fprop.
567+
external type coq.warning string -> string -> variadic any (func).
568568

569569
% [coq.error ...] Prints and *aborts* the program. It is a fatal error for
570570
% Elpi and Ltac
571-
external type coq.error variadic any fprop.
571+
external type coq.error variadic any (func).
572572

573573
% [coq.version VersionString Major Minor Patch] Fetches the version of Coq,
574574
% as a string and as 3 numbers
@@ -1613,7 +1613,7 @@ kind ltac1-tactic type.
16131613
% [coq.ltac.fail Level ...] Interrupts the Elpi program and calls Ltac's
16141614
% fail Level Msg, where Msg is the printing of the remaining arguments.
16151615
% Level can be left unspecified and defaults to 0
1616-
external type coq.ltac.fail int -> variadic any fprop.
1616+
external type coq.ltac.fail int -> variadic any (func).
16171617

16181618
% [coq.ltac.collect-goals T Goals ShelvedGoals]
16191619
% Turns the holes in T into Goals.
@@ -1989,7 +1989,7 @@ external func coq.gref.set.cardinal coq.gref.set -> int.
19891989

19901990
% [coq.gref.set.filter M F M1] Filter M w.r.t. the predicate F
19911991
external func coq.gref.set.filter coq.gref.set,
1992-
(gref -> prop) -> coq.gref.set.
1992+
(gref -> (func)) -> coq.gref.set.
19931993

19941994
% [coq.gref.set.map M F M1] Map M w.r.t. the predicate F
19951995
external func coq.gref.set.map coq.gref.set,
@@ -2002,7 +2002,7 @@ external func coq.gref.set.fold coq.gref.set, A,
20022002
% [coq.gref.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
20032003
% is where F holds
20042004
external func coq.gref.set.partition coq.gref.set,
2005-
(gref -> prop) -> coq.gref.set,
2005+
(gref -> (func)) -> coq.gref.set,
20062006
coq.gref.set.
20072007

20082008
% CAVEAT: the type parameter of coq.gref.map must be a closed term
@@ -2088,7 +2088,7 @@ external func coq.univ.set.cardinal coq.univ.set -> int.
20882088

20892089
% [coq.univ.set.filter M F M1] Filter M w.r.t. the predicate F
20902090
external func coq.univ.set.filter coq.univ.set,
2091-
(univ -> prop) -> coq.univ.set.
2091+
(univ -> (func)) -> coq.univ.set.
20922092

20932093
% [coq.univ.set.map M F M1] Map M w.r.t. the predicate F
20942094
external func coq.univ.set.map coq.univ.set,
@@ -2101,7 +2101,7 @@ external func coq.univ.set.fold coq.univ.set, A,
21012101
% [coq.univ.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
21022102
% is where F holds
21032103
external func coq.univ.set.partition coq.univ.set,
2104-
(univ -> prop) -> coq.univ.set,
2104+
(univ -> (func)) -> coq.univ.set,
21052105
coq.univ.set.
21062106

21072107
% CAVEAT: the type parameter of coq.univ.map must be a closed term
@@ -2192,7 +2192,7 @@ external func coq.univ.variable.set.cardinal coq.univ.variable.set -> int.
21922192

21932193
% [coq.univ.variable.set.filter M F M1] Filter M w.r.t. the predicate F
21942194
external func coq.univ.variable.set.filter coq.univ.variable.set,
2195-
(univ.variable -> prop) -> coq.univ.variable.set.
2195+
(univ.variable -> (func)) -> coq.univ.variable.set.
21962196

21972197
% [coq.univ.variable.set.map M F M1] Map M w.r.t. the predicate F
21982198
external func coq.univ.variable.set.map coq.univ.variable.set,
@@ -2205,7 +2205,7 @@ external func coq.univ.variable.set.fold coq.univ.variable.set, A,
22052205
% [coq.univ.variable.set.partition M F M1 M2] Partitions M w.r.t. the
22062206
% predicate F, M1 is where F holds
22072207
external func coq.univ.variable.set.partition coq.univ.variable.set,
2208-
(univ.variable -> prop) -> coq.univ.variable.set,
2208+
(univ.variable -> (func)) -> coq.univ.variable.set,
22092209
coq.univ.variable.set.
22102210

22112211
% CAVEAT: the type parameter of coq.univ.variable.map must be a closed

‎builtin-doc/elpi-builtin.elpi‎

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -37,23 +37,23 @@ external symbol (;) prop -> prop -> prop.
3737

3838
(_ ; B) :- B.
3939

40-
external symbol (:-) : fprop -> fprop -> fprop = "core".
40+
external symbol (:-) : (func) -> (func) -> (func) = "core".
4141

42-
external symbol (:-) : fprop -> list prop -> fprop = "core".
42+
external symbol (:-) : (func) -> list prop -> (func) = "core".
4343

44-
external symbol (,) : variadic fprop fprop.
44+
external symbol (,) : variadic (func) (func).
4545

4646
external symbol uvar : A = "core".
4747

4848
external symbol (as) : A -> A -> A = "core".
4949

50-
external symbol (=>) : prop -> fprop -> fprop = "core".
50+
external symbol (=>) : prop -> (func) -> (func) = "core".
5151

52-
external symbol (=>) : list prop -> fprop -> fprop = "core".
52+
external symbol (=>) : list prop -> (func) -> (func) = "core".
5353

54-
external symbol (==>) : prop -> fprop -> fprop.
54+
external symbol (==>) : prop -> (func) -> (func).
5555

56-
external symbol (==>) : list prop -> fprop -> fprop.
56+
external symbol (==>) : list prop -> (func) -> (func).
5757

5858
% -- Control --
5959

@@ -73,7 +73,7 @@ external func declare_constraint (func) -> any .. .
7373
external func print_constraints.
7474

7575
% [halt ...] halts the program and print the terms
76-
external type halt variadic any fprop.
76+
external type halt variadic any (func).
7777

7878
func stop.
7979

@@ -294,10 +294,10 @@ external symbol error : string -> diagnostic = "1". % Failure
294294
% == Elpi builtins =====================================
295295

296296
% [dprint ...] prints raw terms (debugging)
297-
external type dprint variadic any fprop.
297+
external type dprint variadic any (func).
298298

299299
% [print ...] prints terms
300-
external type print variadic any fprop.
300+
external type print variadic any (func).
301301

302302
% Deprecated, use trace.counter
303303
func counter string -> int.
@@ -341,7 +341,7 @@ rex_split Rx S L :- rex.split Rx S L.
341341

342342
% [var V ...] checks if the term V is a variable. When used with tree
343343
% arguments it relates an applied variable with its head and argument list.
344-
external type var any -> variadic any fprop.
344+
external func var -> any, any.. .
345345

346346

347347
% [prune V L] V is pruned to L (V is unified with a variable that only sees
@@ -374,11 +374,11 @@ external func cmp_term any, any -> cmp.
374374

375375
% [name T ...] checks if T is a eigenvariable. When used with tree arguments
376376
% it relates an applied name with its head and argument list.
377-
external type name any -> variadic any fprop.
377+
external func name -> any, any.. .
378378

379379
% [constant T ...] checks if T is a (global) constant. When used with tree
380380
% arguments it relates an applied constant with its head and argument list.
381-
external type constant any -> variadic any fprop.
381+
external func constant -> any, any.. .
382382

383383
external func names % generates the list of eigenvariable
384384
-> list any. % list of eigenvariables in order of age (young first)
@@ -428,12 +428,12 @@ external func open_safe safe -> list A.
428428

429429
% [if C T E] picks the first success of C then runs T (never E).
430430
% if C has no success it runs E.
431-
func if prop, fprop, fprop.
431+
func if prop, (func), (func).
432432
if B T _ :- B, !, T.
433433
if _ _ E :- E.
434434

435435
% [if2 C1 B1 C2 B2 E] like if but with 2 then branches (and one else branch).
436-
func if2 prop, fprop, prop, fprop, fprop.
436+
func if2 prop, (func), prop, (func), (func).
437437
if2 G1 P1 _ _ _ :- G1, !, P1.
438438
if2 _ _ G2 P2 _ :- G2, !, P2.
439439
if2 _ _ _ _ E :- !, E.
@@ -734,7 +734,7 @@ intersperse Sep [X|XS] [X,Sep|YS] :- intersperse Sep XS YS.
734734
func flip (func A, B), B, A.
735735
flip P X Y :- P Y X.
736736

737-
func time fprop -> float.
737+
func time (func) -> float.
738738
time P T :- gettimeofday Before, P, gettimeofday After, T is After - Before.
739739

740740
func do! list prop.
@@ -929,7 +929,7 @@ external func std.string.set.cardinal std.string.set -> int.
929929

930930
% [std.string.set.filter M F M1] Filter M w.r.t. the predicate F
931931
external func std.string.set.filter std.string.set,
932-
(string -> prop) -> std.string.set.
932+
(string -> (func)) -> std.string.set.
933933

934934
% [std.string.set.map M F M1] Map M w.r.t. the predicate F
935935
external func std.string.set.map std.string.set,
@@ -942,7 +942,7 @@ external func std.string.set.fold std.string.set, A,
942942
% [std.string.set.partition M F M1 M2] Partitions M w.r.t. the predicate F,
943943
% M1 is where F holds
944944
external func std.string.set.partition std.string.set,
945-
(string -> prop) -> std.string.set,
945+
(string -> (func)) -> std.string.set,
946946
std.string.set.
947947

948948
kind std.int.set type.
@@ -991,7 +991,7 @@ external func std.int.set.cardinal std.int.set -> int.
991991

992992
% [std.int.set.filter M F M1] Filter M w.r.t. the predicate F
993993
external func std.int.set.filter std.int.set,
994-
(int -> prop) -> std.int.set.
994+
(int -> (func)) -> std.int.set.
995995

996996
% [std.int.set.map M F M1] Map M w.r.t. the predicate F
997997
external func std.int.set.map std.int.set,
@@ -1004,7 +1004,7 @@ external func std.int.set.fold std.int.set, A,
10041004
% [std.int.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
10051005
% is where F holds
10061006
external func std.int.set.partition std.int.set,
1007-
(int -> prop) -> std.int.set,
1007+
(int -> (func)) -> std.int.set,
10081008
std.int.set.
10091009

10101010
kind std.loc.set type.
@@ -1053,7 +1053,7 @@ external func std.loc.set.cardinal std.loc.set -> int.
10531053

10541054
% [std.loc.set.filter M F M1] Filter M w.r.t. the predicate F
10551055
external func std.loc.set.filter std.loc.set,
1056-
(loc -> prop) -> std.loc.set.
1056+
(loc -> (func)) -> std.loc.set.
10571057

10581058
% [std.loc.set.map M F M1] Map M w.r.t. the predicate F
10591059
external func std.loc.set.map std.loc.set,
@@ -1066,7 +1066,7 @@ external func std.loc.set.fold std.loc.set, A,
10661066
% [std.loc.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
10671067
% is where F holds
10681068
external func std.loc.set.partition std.loc.set,
1069-
(loc -> prop) -> std.loc.set,
1069+
(loc -> (func)) -> std.loc.set,
10701070
std.loc.set.
10711071

10721072
#line 1 "builtin_map.elpi"

‎elpi/coq-lib.elpi‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -630,7 +630,7 @@ coq.bind-ind-parameters.aux I T Vs Ts K O :- I > 0, whd1 T T', !,
630630

631631
% coq.with-TC Class Instance->Clause Code: runs Code under a context augmented with
632632
% all instances for Class transformed by Instance->Clause.
633-
func coq.with-TC term, (func tc-instance -> prop), fprop ->.
633+
func coq.with-TC term, (func tc-instance -> prop), (func) ->.
634634
coq.with-TC Class Instance->Clause Code :-
635635
coq.TC.db-for {coq.term->gref Class} Instances,
636636
map Instances Instance->Clause Hyps, !,

‎examples/tutorial_elpi_lang.v‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1067,10 +1067,10 @@ kind nat type.
10671067
type z nat.
10681068
type s nat -> nat.
10691069

1070-
pred sum i:nat, i:nat, o:nat.
1070+
func sum nat, nat -> nat.
10711071

1072-
sum (s X) Y (s Z) :- sum X Y Z.
1073-
sum z X X.
1072+
sum (s X) Y (s Z) :- !, sum X Y Z.
1073+
sum z X X :- !.
10741074
sum X Y Z :-
10751075
% the head of the rule always unifies with the query, so
10761076
% we double check X is a variable (we could also be
@@ -1137,12 +1137,12 @@ and we would like to be able to fail early.
11371137

11381138
Elpi Accumulate lp:{{
11391139

1140-
pred even i:nat.
1141-
pred odd i:nat.
1140+
func even nat.
1141+
func odd nat.
11421142

1143-
even z.
1144-
even (s X) :- odd X.
1145-
odd (s X) :- even X.
1143+
even z :- !.
1144+
even (s X) :- !, odd X.
1145+
odd (s X) :- !, even X.
11461146

11471147
odd X :- var X, declare_constraint (odd X) [X].
11481148
even X :- var X, declare_constraint (even X) [X].

0 commit comments

Comments
 (0)