[builtins] std.init and std.make

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.init N E L` builds a list `L = [E, ..., E]` with length `N`
+  - `std.make N F L` builds the list `L = [F 0, F 1, ..., F (N-1)]`
 
 # v1.20.0 (September 2024)
 

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 make i:int, i:A, o:list A.
+make 0 _ [] :- !.
+make N E [E|L] :- N' is N - 1, make N' E L.
+
+% [init N F L] L is [F 0, ..., F (N-1)]
+pred init i:int, i:(pred i:int, o:A), o:list A.
+init N F L :- init.aux 0 N F L', std.rev L' 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 init.aux i:int, i:int, i:(pred i:int, o:A), o:list A.
+init N N _ [] :- !.
+init N M F [E|L] :- F N E, N' is N + 1, init N' M F L.
+
+pred iota i:int, o:list int.
+iota N L :- init 0 N (x\x) L.
 
 % [intersperse X L R] R is [L0, X, ..., X, LN]
 :index(_ 1)

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 make i:int, i:A, o:list A.
+make 0 _ [] :- !.
+make N E [E|L] :- N' is N - 1, make N' E L.
+
+% [init N F L] L is [F 0, ..., F (N-1)]
+pred init i:int, i:(pred i:int, o:A), o:list A.
+init N F L :- 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 init.aux i:int, i:int, i:(pred i:int, o:A), o:list A.
+init.aux N N _ [] :- !.
+init.aux N M F [E|L] :- F N E, N' is N + 1, init.aux N' M F L.
+
+pred iota i:int, o:list int.
+iota N L :- init N (x\y\ x = y) L.
 
 % [intersperse X L R] R is [L0, X, ..., X, LN]
 :index(_ 1)