Merge pull request #278 from FissoreD/new-builtins

[builtins] std.list.init and std.list.make
LPCIC · Oct 28, 2024 · 3a5a2f9 · 3a5a2f9
2 parents 9419bc8 + fcd5dde
commit 3a5a2f9
Show file tree

Hide file tree

Showing 8 changed files with 219 additions and 200 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -18,8 +18,9 @@ Requires Menhir 20211230 and OCaml 4.08 or above.
     the `:functional` attributes can be passed to higher-order arguments
   - The piece of information likes modes and functionality is transmitted to the
     checker (currently this information is not taken into account) 
-
-
+- Builtins:
+  - `std.list.init N E L` builds a list `L = [E, ..., E]` with length `N`
+  - `std.list.make N F L` builds the list `L = [F 0, F 1, ..., F (N-1)]`
 
 # v1.20.0 (September 2024)
 

diff --git a/src/builtin.elpi b/src/builtin.elpi
@@ -776,12 +776,21 @@ flatten []     [].
 pred null i:list A.
 null [].
 
-pred iota i:int, o:list int.
-iota N L :- iota.aux 0 N L.
+% [make N E L] L is [E, ..., E] and L has length N
+pred list.make i:int, i:A, o:list A.
+list.make 0 _ [] :- !.
+list.make N E [E|L] :- N' is N - 1, list.make N' E L.
+
+% [init N F L] L is [F 0, ..., F (N-1)]
+pred list.init i:int, i:(pred i:int, o:A), o:list A.
+list.init N F L :- list.init.aux 0 N F L.
 
-pred iota.aux i:int, i:int, o:list int.
-iota.aux X X [] :- !.
-iota.aux N X [N|R] :- M is N + 1, iota.aux M X R.
+pred list.init.aux i:int, i:int, i:(pred i:int, o:A), o:list A.
+list.init.aux N N _ [] :- !.
+list.init.aux N M F [E|L] :- F N E, N' is N + 1, list.init.aux N' M F L.
+
+pred iota i:int, o:list int.
+iota N L :- list.init N (x\y\ x = y) L.
 
 % [intersperse X L R] R is [L0, X, ..., X, LN]
 :index(_ 1)

diff --git a/src/builtin_stdlib.elpi b/src/builtin_stdlib.elpi
@@ -243,12 +243,21 @@ flatten []     [].
 pred null i:list A.
 null [].
 
-pred iota i:int, o:list int.
-iota N L :- iota.aux 0 N L.
+% [make N E L] L is [E, ..., E] and L has length N
+pred list.make i:int, i:A, o:list A.
+list.make 0 _ [] :- !.
+list.make N E [E|L] :- N' is N - 1, list.make N' E L.
+
+% [init N F L] L is [F 0, ..., F (N-1)]
+pred list.init i:int, i:(pred i:int, o:A), o:list A.
+list.init N F L :- list.init.aux 0 N F L.
 
-pred iota.aux i:int, i:int, o:list int.
-iota.aux X X [] :- !.
-iota.aux N X [N|R] :- M is N + 1, iota.aux M X R.
+pred list.init.aux i:int, i:int, i:(pred i:int, o:A), o:list A.
+list.init.aux N N _ [] :- !.
+list.init.aux N M F [E|L] :- F N E, N' is N + 1, list.init.aux N' M F L.
+
+pred iota i:int, o:list int.
+iota N L :- list.init N (x\y\ x = y) L.
 
 % [intersperse X L R] R is [L0, X, ..., X, LN]
 :index(_ 1)

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 1, column 21, characters 21-66:"," \\ (even A0) (odd A0) | (odd z) <=> (true)"]}
-{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--518 []"]}
+{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--522 []"]}
 {"step" : 0,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["odd z"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:curgoal","payload" : ["odd","odd z"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:rule","payload" : ["backchain"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 20,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : []}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 20,"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 2, column 45, characters 67-116:"," \\ (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--519 []"]}
+{"step" : 0,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 2,"name" : "user:assign","payload" : ["A0 := uvar frozen--523 []"]}
 {"step" : 0,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:newgoal","payload" : ["odd (s z)"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 21,"runtime_id" : 2,"name" : "user:curgoal","payload" : ["odd","odd (s z)"]}
 {"step" : 1,"kind" : ["Info"],"goal_id" : 21,"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": 296,
+                      "line": 305,
                       "column": 0,
-                      "character": 9686
+                      "character": 10054
                     }
                   ]
                 }
@@ -117,9 +117,9 @@
                   "File",
                   {
                     "filename": "builtin_stdlib.elpi",
-                    "line": 296,
+                    "line": 305,
                     "column": 0,
-                    "character": 9686
+                    "character": 10054
                   }
                 ]
               }
@@ -442,9 +442,9 @@
                   "File",
                   {
                     "filename": "builtin_stdlib.elpi",
-                    "line": 296,
+                    "line": 305,
                     "column": 0,
-                    "character": 9686
+                    "character": 10054
                   }
                 ]
               }

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 296, column 0, characters 9686-9722:"]}
-{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin_stdlib.elpi\", line 296, column 0, characters 9686-9722:","(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 305, column 0, characters 10054-10090:"]}
+{"step" : 2,"kind" : ["Info"],"goal_id" : 5,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin_stdlib.elpi\", line 305, column 0, characters 10054-10090:","(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"]}