juvix/tests/negative/Iterators2.juvix

module Iterators2;

syntax iterator bind {range := 1};
bind : {A B : Type} → (A → B) → A → B
| f x := f x;

builtin bool
type Bool :=
  | true : Bool
  | false : Bool;

main : Bool := bind (x in true; y in false) x;
Iterator syntax (#2126) * Closes #1992 A function identifier `fun` can be declared as an iterator with ``` syntax iterator fun; ``` For example: ```haskell syntax iterator for; for : {A B : Type} -> (A -> B -> A) -> A -> List B -> List A; for f acc nil := acc; for f acc (x :: xs) := for (f acc x) xs; ``` Iterator application syntax allows for a finite number of initializers `acc := a` followed by a finite number of ranges `x in xs`. For example: ``` for (acc := 0) (x in lst) acc + x ``` The number of initializers plus the number of ranges must be non-zero. An iterator application ``` fun (acc1 := a1; ..; accn := an) (x1 in b1; ..; xk in bk) body ``` gets desugared to ``` fun \{acc1 .. accn x1 .. xk := body} a1 .. an b1 .. bk ``` The `acc1`, ..., `accn`, `x1`, ..., `xk` can be patterns. The desugaring works on a purely syntactic level. Without further restrictions, it is not checked if the number of initializers/ranges matches the type of the identifier. The restrictions on the number of initializers/ranges can be specified in iterator declaration: ``` syntax iterator fun {init: n, range: k}; syntax iterator for {init: 1, range: 1}; syntax iterator map {init: 0, range: 1}; ``` The attributes (`init`, `range`) in between braces are parsed as YAML to avoid inventing and parsing a new attribute language. Both attributes are optional. 2023-05-30 16:30:11 +03:00			`module Iterators2;`

New fixity/iterator syntax (#2332) - Closes #2330 - Closes #2329 This pr implements the syntax changes described in #2330. It drops support for the old yaml-based syntax. Some valid examples: ``` syntax iterator for {init := 1; range := 1}; syntax fixity cons := binary {assoc := right}; syntax fixity cmp := binary; syntax fixity cmp := binary {}; -- debatable whether we want to accept empty {} or not. I think we should ``` # Future work This pr creates an asymmetry between iterators and operators definitions. Iterators definition do not require a constructor. We could add it to make it homogeneous, but it looks a bit redundant: ``` syntax iterator for := mkIterator {init := 1; range := 1}; ``` We could consider merging iterator and fixity declarations with this alternative syntax. ``` syntax XXX for := iterator {init := 1; range := 1}; syntax XXX cons := binary {assoc := right}; ``` where `XXX` is a common keyword. Suggestion by @lukaszcz XXX = declare --------- Co-authored-by: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com> Co-authored-by: Lukasz Czajka <lukasz@heliax.dev> 2023-09-14 11:57:38 +03:00			`syntax iterator bind {range := 1};`
Remove old function syntax (#2305) * Enables new function syntax in local let-declarations * Closes #2251 2023-08-24 12:20:09 +03:00			`bind : {A B : Type} → (A → B) → A → B`
			`\| f x := f x;`
Iterator syntax (#2126) * Closes #1992 A function identifier `fun` can be declared as an iterator with ``` syntax iterator fun; ``` For example: ```haskell syntax iterator for; for : {A B : Type} -> (A -> B -> A) -> A -> List B -> List A; for f acc nil := acc; for f acc (x :: xs) := for (f acc x) xs; ``` Iterator application syntax allows for a finite number of initializers `acc := a` followed by a finite number of ranges `x in xs`. For example: ``` for (acc := 0) (x in lst) acc + x ``` The number of initializers plus the number of ranges must be non-zero. An iterator application ``` fun (acc1 := a1; ..; accn := an) (x1 in b1; ..; xk in bk) body ``` gets desugared to ``` fun \{acc1 .. accn x1 .. xk := body} a1 .. an b1 .. bk ``` The `acc1`, ..., `accn`, `x1`, ..., `xk` can be patterns. The desugaring works on a purely syntactic level. Without further restrictions, it is not checked if the number of initializers/ranges matches the type of the identifier. The restrictions on the number of initializers/ranges can be specified in iterator declaration: ``` syntax iterator fun {init: n, range: k}; syntax iterator for {init: 1, range: 1}; syntax iterator map {init: 0, range: 1}; ``` The attributes (`init`, `range`) in between braces are parsed as YAML to avoid inventing and parsing a new attribute language. Both attributes are optional. 2023-05-30 16:30:11 +03:00
			`builtin bool`
			`type Bool :=`
			`\| true : Bool`
			`\| false : Bool;`

Remove old function syntax (#2305) * Enables new function syntax in local let-declarations * Closes #2251 2023-08-24 12:20:09 +03:00			`main : Bool := bind (x in true; y in false) x;`