Merge pull request #203 from lukovdm/patch-1

Add foldr to the elpi builtins
LPCIC · Nov 7, 2023 · ce533c5 · ce533c5
2 parents 3cdb91a + 2ad3327
commit ce533c5
Show file tree

Hide file tree

Showing 6 changed files with 23 additions and 10 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,3 +1,8 @@
+# UNRELEASED
+
+Library:
+  - New `std.fold-right`
+
 # v1.18.0 (October 2023)
 
 Requires Menhir 20211230 and OCaml 4.08 or above.

diff --git a/src/builtin.elpi b/src/builtin.elpi
@@ -642,6 +642,10 @@ pred fold i:list B, i:A, i:(B -> A -> A -> prop), o:A.
 fold [] A _ A.
 fold [X|XS] A F R :- F X A A1, fold XS A1 F R.
 
+pred fold-right i:list B, i:A, i:(B -> A -> A -> prop), o:A.
+fold-right [] A _ A.
+fold-right [X|XS] A F R :- fold-right XS A F A', F X A' R.
+
 pred fold2 i:list C, i:list B, i:A, i:(C -> B -> A -> A -> prop), o:A.
 fold2 [] [_|_] _ _ _ :- fatal-error "fold2 on lists of different length".
 fold2 [_|_] [] _ _ _ :- fatal-error "fold2 on lists of different length".

diff --git a/src/builtin_stdlib.elpi b/src/builtin_stdlib.elpi
@@ -114,6 +114,10 @@ pred fold i:list B, i:A, i:(B -> A -> A -> prop), o:A.
 fold [] A _ A.
 fold [X|XS] A F R :- F X A A1, fold XS A1 F R.
 
+pred fold-right i:list B, i:A, i:(B -> A -> A -> prop), o:A.
+fold-right [] A _ A.
+fold-right [X|XS] A F R :- fold-right XS A F A', F X A' R.
+
 pred fold2 i:list C, i:list B, i:A, i:(C -> B -> A -> A -> prop), o:A.
 fold2 [] [_|_] _ _ _ :- fatal-error "fold2 on lists of different length".
 fold2 [_|_] [] _ _ _ :- fatal-error "fold2 on lists of different length".

diff --git a/tests/sources/trace_chr.json b/tests/sources/trace_chr.json
@@ -96,15 +96,15 @@
 {"step" : 13,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:newgoal","payload" : ["even X1"]}
 {"step" : 13,"kind" : ["Info"],"goal_id" : 18,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 2, column 3, character 25:"," \\ (even A0) (odd A0) | (odd z) <=> (true)"]}
-{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--482 []"]}
+{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--484 []"]}
 {"step" : 0,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["odd z"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["odd","odd z"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : []}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 1,"name" : "user:rule:backchain","payload" : ["fail"]}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:CHR:rule-failed","payload" : []}
 {"step" : 14,"kind" : ["Info"],"goal_id" : 19,"runtime_id" : 0,"name" : "user:CHR:try","payload" : ["File \"tests/sources/trace_chr.elpi\", line 3, column 3, character 71:"," \\ (even A0) (odd A0) | (odd (s z)) <=> (fail)"]}
-{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--483 []"]}
+{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--485 []"]}
 {"step" : 0,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["odd (s z)"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["odd","odd (s z)"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 23,"runtime_id" : 2,"name" : "user:rule","payload" : ["backchain"]}

diff --git a/tests/sources/trace_findall.elab.json b/tests/sources/trace_findall.elab.json
@@ -89,9 +89,9 @@
                     "File",
                     {
                       "filename": "builtin_stdlib.elpi",
-                      "line": 283,
+                      "line": 287,
                       "column": 0,
-                      "character": 9378
+                      "character": 9520
                     }
                   ]
                 }
@@ -117,9 +117,9 @@
                   "File",
                   {
                     "filename": "builtin_stdlib.elpi",
-                    "line": 283,
+                    "line": 287,
                     "column": 0,
-                    "character": 9378
+                    "character": 9520
                   }
                 ]
               }
@@ -442,9 +442,9 @@
                   "File",
                   {
                     "filename": "builtin_stdlib.elpi",
-                    "line": 283,
+                    "line": 287,
                     "column": 0,
-                    "character": 9378
+                    "character": 9520
                   }
                 ]
               }

diff --git a/tests/sources/trace_findall.json b/tests/sources/trace_findall.json
@@ -10,8 +10,8 @@
 {"step" : 1,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]}
 {"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["std.findall","std.findall (p _) X0"]}
 {"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin_stdlib.elpi\", line 283, column 0, character 9378:"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin_stdlib.elpi\", line 283, column 0, character 9378:","(std.findall A0 A1) :- (findall_solutions A0 A1)."]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin_stdlib.elpi\", line 287, column 0, character 9520:"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin_stdlib.elpi\", line 287, column 0, character 9520:","(std.findall A0 A1) :- (findall_solutions A0 A1)."]}
 {"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := p _"]}
 {"step" : 2,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A1 := X0"]}
 {"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:subgoal","payload" : ["7"]}