Skip to content

Commit af8ef2a

Browse files
garesgares
authored
Merge pull request #387 from LPCIC/fix-pm
fix pattern_match arguments order
2 parents c44c0ce + e4d4b0e commit af8ef2a

File tree

13 files changed

+169
-150
lines changed

13 files changed

+169
-150
lines changed

‎CHANGES.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,11 @@
1+
# v3.4.5 (December 2025)
2+
3+
Requires Menhir 20211230 and OCaml 4.13 or above.
4+
5+
- Builtin:
6+
- Fix `pattern_match` builtin had the arguments in wrong order (w.r.t. the
7+
documentation). The pattern is now the second argument.
8+
19
# v3.4.4 (December 2025)
210

311
Requires Menhir 20211230 and OCaml 4.13 or above.

‎src/builtin.elpi‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,14 @@ func fail.
1414

1515
func false.
1616

17-
external func (=) -> A, A. % unification term term
1817

19-
external func pattern_match A -> A. % matching pattern term
18+
% [X = T] unifies X with Y, possibly assigning unification
19+
% variables in X and Y.
20+
external func (=) -> A, A.
21+
22+
% [pattern_matching T P] matches T against pattern P, only
23+
% variables in P are assigned.
24+
external func pattern_match A -> A.
2025

2126
external func (pi) (func A).
2227

‎src/builtin.ml‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -220,8 +220,14 @@ let core_builtins = let open BuiltIn in let open ContextualConversion in [
220220
LPCode "func fail.";
221221
LPCode "func false.";
222222

223-
LPCode "external func (=) -> A, A. % unification term term";
224-
LPCode "external func pattern_match A -> A. % matching pattern term";
223+
LPCode {|
224+
% [X = T] unifies X with Y, possibly assigning unification
225+
% variables in X and Y.
226+
external func (=) -> A, A.
227+
228+
% [pattern_matching T P] matches T against pattern P, only
229+
% variables in P are assigned.
230+
external func pattern_match A -> A.|};
225231

226232
LPCode "external func (pi) (func A).";
227233
LPCode "external func (sigma) (func A).";

‎src/runtime/runtime.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4084,7 +4084,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> executabl
40844084
[%spy "user:rule:eq" ~rid ~gid pp_string "fail"];
40854085
[%tcall next_alt alts]
40864086
end
4087-
| Builtin(Match,[p;r]) -> [%spy "user:rule" ~rid ~gid pp_string "eq"]; [%spy "user:rule:builtin:name" ~rid ~gid pp_string (show_builtin_predicate C.show Match)];
4087+
| Builtin(Match,[r;p]) -> [%spy "user:rule" ~rid ~gid pp_string "eq"]; [%spy "user:rule:builtin:name" ~rid ~gid pp_string (show_builtin_predicate C.show Match)];
40884088
if unif ~oc:true ~argsdepth:depth ~matching:true (gid[@trace]) depth empty_env depth r p then begin
40894089
[%spy "user:rule:eq" ~rid ~gid pp_string "success"];
40904090
match gs with

‎tests/sources/pm.elpi‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ type f int -> prop.
22
type a int.
33

44
main :-
5-
pattern_match (f X) (f 1),
5+
pattern_match (f 1) (f X),
66
print X,
7-
not(pattern_match (f a) (f Y)),
7+
not(pattern_match (f Y) (f a)),
88
print Y.

‎tests/sources/trace.elab.json‎

Lines changed: 34 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -86,9 +86,9 @@
8686
"File",
8787
{
8888
"filename": "builtin.elpi",
89-
"line": 36,
89+
"line": 41,
9090
"column": 0,
91-
"character": 460
91+
"character": 586
9292
}
9393
]
9494
}
@@ -110,9 +110,9 @@
110110
"File",
111111
{
112112
"filename": "builtin.elpi",
113-
"line": 36,
113+
"line": 41,
114114
"column": 0,
115-
"character": 460
115+
"character": 586
116116
}
117117
]
118118
}
@@ -208,9 +208,9 @@
208208
"File",
209209
{
210210
"filename": "builtin.elpi",
211-
"line": 36,
211+
"line": 41,
212212
"column": 0,
213-
"character": 460
213+
"character": 586
214214
}
215215
]
216216
}
@@ -263,9 +263,9 @@
263263
"File",
264264
{
265265
"filename": "builtin.elpi",
266-
"line": 86,
266+
"line": 91,
267267
"column": 0,
268-
"character": 1505
268+
"character": 1631
269269
}
270270
]
271271
}
@@ -289,9 +289,9 @@
289289
"File",
290290
{
291291
"filename": "builtin.elpi",
292-
"line": 86,
292+
"line": 91,
293293
"column": 0,
294-
"character": 1505
294+
"character": 1631
295295
}
296296
]
297297
}
@@ -327,9 +327,9 @@
327327
"File",
328328
{
329329
"filename": "builtin.elpi",
330-
"line": 36,
330+
"line": 41,
331331
"column": 0,
332-
"character": 460
332+
"character": 586
333333
}
334334
]
335335
}
@@ -397,9 +397,9 @@
397397
"File",
398398
{
399399
"filename": "builtin.elpi",
400-
"line": 86,
400+
"line": 91,
401401
"column": 0,
402-
"character": 1505
402+
"character": 1631
403403
}
404404
]
405405
}
@@ -435,9 +435,9 @@
435435
"File",
436436
{
437437
"filename": "builtin.elpi",
438-
"line": 36,
438+
"line": 41,
439439
"column": 0,
440-
"character": 460
440+
"character": 586
441441
}
442442
]
443443
}
@@ -506,9 +506,9 @@
506506
"File",
507507
{
508508
"filename": "builtin.elpi",
509-
"line": 86,
509+
"line": 91,
510510
"column": 0,
511-
"character": 1505
511+
"character": 1631
512512
}
513513
]
514514
}
@@ -544,9 +544,9 @@
544544
"File",
545545
{
546546
"filename": "builtin.elpi",
547-
"line": 36,
547+
"line": 41,
548548
"column": 0,
549-
"character": 460
549+
"character": 586
550550
}
551551
]
552552
}
@@ -646,9 +646,9 @@
646646
"File",
647647
{
648648
"filename": "builtin.elpi",
649-
"line": 36,
649+
"line": 41,
650650
"column": 0,
651-
"character": 460
651+
"character": 586
652652
}
653653
]
654654
}
@@ -735,9 +735,9 @@
735735
"File",
736736
{
737737
"filename": "builtin.elpi",
738-
"line": 36,
738+
"line": 41,
739739
"column": 0,
740-
"character": 460
740+
"character": 586
741741
}
742742
]
743743
}
@@ -824,9 +824,9 @@
824824
"File",
825825
{
826826
"filename": "builtin.elpi",
827-
"line": 36,
827+
"line": 41,
828828
"column": 0,
829-
"character": 460
829+
"character": 586
830830
}
831831
]
832832
}
@@ -909,9 +909,9 @@
909909
"File",
910910
{
911911
"filename": "builtin.elpi",
912-
"line": 36,
912+
"line": 41,
913913
"column": 0,
914-
"character": 460
914+
"character": 586
915915
}
916916
]
917917
}
@@ -964,9 +964,9 @@
964964
"File",
965965
{
966966
"filename": "builtin.elpi",
967-
"line": 38,
967+
"line": 43,
968968
"column": 0,
969-
"character": 475
969+
"character": 601
970970
}
971971
]
972972
}
@@ -988,9 +988,9 @@
988988
"File",
989989
{
990990
"filename": "builtin.elpi",
991-
"line": 38,
991+
"line": 43,
992992
"column": 0,
993-
"character": 475
993+
"character": 601
994994
}
995995
]
996996
}
@@ -1086,9 +1086,9 @@
10861086
"File",
10871087
{
10881088
"filename": "builtin.elpi",
1089-
"line": 38,
1089+
"line": 43,
10901090
"column": 0,
1091-
"character": 475
1091+
"character": 601
10921092
}
10931093
]
10941094
}

‎tests/sources/trace.json‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88
{"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]}
99
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : [";","p 1 X0 ; p 2 X1"]}
1010
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]}
11-
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 36, column 0, characters 460-472:","File \"builtin.elpi\", line 38, column 0, characters 475-487:"]}
12-
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 36, column 0, characters 460-472:","(A0 ; _) :- A0."]}
11+
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 41, column 0, characters 586-598:","File \"builtin.elpi\", line 43, column 0, characters 601-613:"]}
12+
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 41, column 0, characters 586-598:","(A0 ; _) :- A0."]}
1313
{"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := p 1 X0"]}
1414
{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["6"]}
1515
{"step" : 2,"kind" : ["Info"],"goal_id" : 6,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["p 1 X0"]}
@@ -24,8 +24,8 @@
2424
{"step" : 3,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]}
2525
{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["is","1 is 2 + 3"]}
2626
{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]}
27-
{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 86, column 0, characters 1505-1523:"]}
28-
{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 86, column 0, characters 1505-1523:","(A1 is A0) :- (calc A0 A1)."]}
27+
{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 91, column 0, characters 1631-1649:"]}
28+
{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 91, column 0, characters 1631-1649:","(A1 is A0) :- (calc A0 A1)."]}
2929
{"step" : 4,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A1 := 1"]}
3030
{"step" : 4,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := 2 + 3"]}
3131
{"step" : 4,"kind" : ["Info"],"goal_id" : 7,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["8"]}
@@ -71,8 +71,8 @@
7171
{"step" : 10,"kind" : ["Info"],"goal_id" : 12,"runtime_id" : 0,"name" : "user:rule:eq","payload" : ["fail"]}
7272
{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : [";","p 1 X0 ; p 2 X1"]}
7373
{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]}
74-
{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 38, column 0, characters 475-487:"]}
75-
{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 38, column 0, characters 475-487:","(_ ; A0) :- A0."]}
74+
{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin.elpi\", line 43, column 0, characters 601-613:"]}
75+
{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin.elpi\", line 43, column 0, characters 601-613:","(_ ; A0) :- A0."]}
7676
{"step" : 11,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := p 2 X1"]}
7777
{"step" : 11,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["13"]}
7878
{"step" : 11,"kind" : ["Info"],"goal_id" : 13,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["p 2 X1"]}

‎tests/sources/trace4.elab.json‎

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -86,9 +86,9 @@
8686
"File",
8787
{
8888
"filename": "builtin.elpi",
89-
"line": 36,
89+
"line": 41,
9090
"column": 0,
91-
"character": 460
91+
"character": 586
9292
}
9393
]
9494
}
@@ -110,9 +110,9 @@
110110
"File",
111111
{
112112
"filename": "builtin.elpi",
113-
"line": 36,
113+
"line": 41,
114114
"column": 0,
115-
"character": 460
115+
"character": 586
116116
}
117117
]
118118
}
@@ -250,9 +250,9 @@
250250
"File",
251251
{
252252
"filename": "builtin.elpi",
253-
"line": 36,
253+
"line": 41,
254254
"column": 0,
255-
"character": 460
255+
"character": 586
256256
}
257257
]
258258
}
@@ -325,9 +325,9 @@
325325
"File",
326326
{
327327
"filename": "builtin.elpi",
328-
"line": 36,
328+
"line": 41,
329329
"column": 0,
330-
"character": 460
330+
"character": 586
331331
}
332332
]
333333
}
@@ -461,9 +461,9 @@
461461
"File",
462462
{
463463
"filename": "builtin.elpi",
464-
"line": 36,
464+
"line": 41,
465465
"column": 0,
466-
"character": 460
466+
"character": 586
467467
}
468468
]
469469
}
@@ -516,9 +516,9 @@
516516
"File",
517517
{
518518
"filename": "builtin.elpi",
519-
"line": 38,
519+
"line": 43,
520520
"column": 0,
521-
"character": 475
521+
"character": 601
522522
}
523523
]
524524
}
@@ -540,9 +540,9 @@
540540
"File",
541541
{
542542
"filename": "builtin.elpi",
543-
"line": 38,
543+
"line": 43,
544544
"column": 0,
545-
"character": 475
545+
"character": 601
546546
}
547547
]
548548
}
@@ -638,9 +638,9 @@
638638
"File",
639639
{
640640
"filename": "builtin.elpi",
641-
"line": 38,
641+
"line": 43,
642642
"column": 0,
643-
"character": 475
643+
"character": 601
644644
}
645645
]
646646
}

0 commit comments

Comments
 (0)