1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-12 14:28:08 +03:00
juvix/tests/Internal/positive
Paul Cadman feff86d576
Translate as-pattern binders to Core PatternBinders (#1789)
Before this change, nested as-patterns (i.e as-patterns binding
arguments to constructors) were not translated to Core pattern binders.

This meant that the following function would crash the compiler:

```
f : List Nat -> List Nat;
f  (x :: a@(x' :: xs)) := a;
f _ := nil;
```

i.e the nested as-pattern `a` was ignored in the internal to core
translation.

This commit translates each as-pattern to a Core `PatternBinder`.

* Fixes https://github.com/anoma/juvix/issues/1788
* Fixes https://github.com/anoma/juvix/issues/1738
2023-01-31 14:32:50 +00:00
..
Dependencies Support basic dependencies (#1622) 2022-12-20 13:05:40 +01:00
Import Add builtin nat and bool types as start nodes in reachability analysis (#1775) 2023-01-27 15:21:38 +00:00
out Translate as-pattern binders to Core PatternBinders (#1789) 2023-01-31 14:32:50 +00:00
AsPatterns.juvix Translate as-pattern binders to Core PatternBinders (#1789) 2023-01-31 14:32:50 +00:00
BuiltinAdd.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
BuiltinBool.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
BuiltinIf.juvix Lazy boolean operators (#1743) 2023-01-25 18:57:47 +01:00
BuiltinInductive.juvix Add types to Core functions and constructors when translating from Internal (#1617) 2022-11-11 12:38:48 +00:00
Church.juvix Adapt Juvix programs to the new pipeline (#1746) 2023-01-23 14:57:01 +01:00
FunctionReturnConstructor.juvix Change syntax for ind. data types and forbid the empty data type (#1684) 2023-01-03 13:49:04 +01:00
FunctionType.juvix Change syntax for ind. data types and forbid the empty data type (#1684) 2023-01-03 13:49:04 +01:00
HigherOrderLambda.juvix Pipes for lambda clauses (#1781) 2023-01-30 12:06:18 +01:00
IdenFunctionArgs.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
IdenFunctionArgsImplicit.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
IdenFunctionIntegerLiteral.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
Inductive.juvix Change syntax for ind. data types and forbid the empty data type (#1684) 2023-01-03 13:49:04 +01:00
IntegerLiteral.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
juvix.yaml Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
Lambda.juvix Pipes for lambda clauses (#1781) 2023-01-30 12:06:18 +01:00
LitInteger.juvix Convert Nat literals to Core integers (#1681) 2023-01-03 18:52:20 +01:00
LitIntegerToNat.juvix Add builtin nat and bool types as start nodes in reachability analysis (#1775) 2023-01-27 15:21:38 +00:00
LitString.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
LitStringIO Add printString and printBool support to legacy C backend (#1698) 2023-01-04 18:02:02 +01:00
LitStringIO.juvix Add printString and printBool support to legacy C backend (#1698) 2023-01-04 18:02:02 +01:00
MatchConstructor.juvix Change syntax for ind. data types and forbid the empty data type (#1684) 2023-01-03 13:49:04 +01:00
Mutual.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
NatMatch1.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
NatMatch2.juvix Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
PatternArgs.juvix Adapt Juvix programs to the new pipeline (#1746) 2023-01-23 14:57:01 +01:00
QuickSort.juvix Adapt Juvix programs to the new pipeline (#1746) 2023-01-23 14:57:01 +01:00
Universe.juvix Add types to Core functions and constructors when translating from Internal (#1617) 2022-11-11 12:38:48 +00:00