diff --git a/CHANGES.md b/CHANGES.md index 882a8bf2c..4d0b576a0 100644 --- 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.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) diff --git a/src/builtin.elpi b/src/builtin.elpi index 4c243cefa..ca3d81c69 100644 --- 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 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) diff --git a/src/builtin_stdlib.elpi b/src/builtin_stdlib.elpi index 4d457d0a4..5d92a129b 100644 --- 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 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)