mirror of
https://github.com/AleoHQ/leo.git
synced 2024-09-22 20:48:17 +03:00
Merge branch 'master' of github.com:AleoHQ/leo into bug/canonicalization-Self-fixes
This commit is contained in:
commit
c56a54c62e
1
.github/workflows/acl2.yml
vendored
1
.github/workflows/acl2.yml
vendored
@ -72,6 +72,7 @@ jobs:
|
|||||||
for dir in ${canonicalization_errors[@]};
|
for dir in ${canonicalization_errors[@]};
|
||||||
do
|
do
|
||||||
cat tmp/tgc/$dir/canonicalization_result.out
|
cat tmp/tgc/$dir/canonicalization_result.out
|
||||||
|
cat tmp/tgc/$dir/canonicalization-theorem.lisp
|
||||||
done;
|
done;
|
||||||
exit 1
|
exit 1
|
||||||
fi
|
fi
|
||||||
|
@ -28,7 +28,7 @@ Many programming languages provide the ability to create aliases (i.e. synonyms)
|
|||||||
The purpose may be to abbreviate a longer type,
|
The purpose may be to abbreviate a longer type,
|
||||||
such as an alias `matrix` for `[i32; (3, 3)]` in an application in which 3x3 matrices of 32-bit integers are relevant
|
such as an alias `matrix` for `[i32; (3, 3)]` in an application in which 3x3 matrices of 32-bit integers are relevant
|
||||||
(e.g. for 3-D rotations, even though fractional numbers may be more realistic).
|
(e.g. for 3-D rotations, even though fractional numbers may be more realistic).
|
||||||
The purpose may also be to clarify the purpose and use of an existing type,
|
The purpose may also be to clarify the intent and use of an existing type,
|
||||||
such as an alias `balance` for `u64` in an application that keeps track of balances.
|
such as an alias `balance` for `u64` in an application that keeps track of balances.
|
||||||
|
|
||||||
The initial motivation that inspired this RFC (along with other RFCs)
|
The initial motivation that inspired this RFC (along with other RFCs)
|
||||||
@ -42,7 +42,7 @@ With the array types of unspecified size proposed in RFC 006,
|
|||||||
## Syntax
|
## Syntax
|
||||||
|
|
||||||
The ABNF grammar changes as follows:
|
The ABNF grammar changes as follows:
|
||||||
```ts
|
```
|
||||||
; modified rule:
|
; modified rule:
|
||||||
keyword = ...
|
keyword = ...
|
||||||
/ %s"true"
|
/ %s"true"
|
||||||
@ -59,12 +59,63 @@ declaration = import-declaration
|
|||||||
/ circuit-declaration
|
/ circuit-declaration
|
||||||
/ constant-declaration
|
/ constant-declaration
|
||||||
/ type-alias-declaration ; new
|
/ type-alias-declaration ; new
|
||||||
|
|
||||||
|
|
||||||
```
|
```
|
||||||
|
|
||||||
A type alias declaration introduces the identifier to stand for the type.
|
A type alias declaration introduces the identifier to stand for the type.
|
||||||
Only top-level type alias declarations are supported;
|
Only top-level type alias declarations are supported;
|
||||||
they are not supported inside functions or circuit types.
|
they are not supported inside functions or circuit types.
|
||||||
|
|
||||||
|
In addition, the following changes to the grammar are appropriate.
|
||||||
|
|
||||||
|
First, the rule
|
||||||
|
```
|
||||||
|
circuit-type = identifier / self-type ; replace with the one below
|
||||||
|
```
|
||||||
|
should be replaced with the rule
|
||||||
|
```
|
||||||
|
circuit-or-alias-type = identifier / self-type
|
||||||
|
```
|
||||||
|
The reason is that, at parsing time, an identifier is not necessarily a circuit type;
|
||||||
|
it may be a type alias that may expand to a (circuit or non-circuit type).
|
||||||
|
Thus, the nomenclature `circuit-or-alias-type` is appropriate.
|
||||||
|
Consequently, references to `circuit-type` in the following rules must be replaced with `circuit-or-alias-type`:
|
||||||
|
```
|
||||||
|
; modified rule:
|
||||||
|
circuit-construction = circuit-or-alias-type "{" ; modified
|
||||||
|
circuit-inline-element
|
||||||
|
*( "," circuit-inline-element ) [ "," ]
|
||||||
|
"}"
|
||||||
|
|
||||||
|
; modified rule:
|
||||||
|
postfix-expression = primary-expression
|
||||||
|
/ postfix-expression "." natural
|
||||||
|
/ postfix-expression "." identifier
|
||||||
|
/ identifier function-arguments
|
||||||
|
/ postfix-expression "." identifier function-arguments
|
||||||
|
/ circuit-or-alias-type "::" identifier function-arguments ; modified
|
||||||
|
/ postfix-expression "[" expression "]"
|
||||||
|
/ postfix-expression "[" [expression] ".." [expression] "]"
|
||||||
|
```
|
||||||
|
|
||||||
|
Second, the rule
|
||||||
|
```
|
||||||
|
aggregate-type = tuple-type / array-type / circuit-type
|
||||||
|
```
|
||||||
|
should be removed, because if we replaced `circuit-type` with `circuit-or-alias-type` there,
|
||||||
|
the identifier could be a type alias, not necessarily an aggregate type.
|
||||||
|
(The notion of aggregate type remains at a semantic level, but has no longer a place in the grammar.)
|
||||||
|
Consequently, the rule
|
||||||
|
```
|
||||||
|
type = scalar-type / aggregate-type
|
||||||
|
```
|
||||||
|
should be rephrased as
|
||||||
|
```
|
||||||
|
type = scalar-type / tuple-type / array-type / circuit-or-alias-type
|
||||||
|
```
|
||||||
|
which "inlines" the previous `aggregate-type` with `circuit-type` replaced with `circuit-or-alias-type`.
|
||||||
|
|
||||||
## Semantics
|
## Semantics
|
||||||
|
|
||||||
There must be no direct or indirect circularity in the type aliases.
|
There must be no direct or indirect circularity in the type aliases.
|
||||||
|
@ -26,6 +26,6 @@ circuit Foo {
|
|||||||
function main(character: char) -> char {
|
function main(character: char) -> char {
|
||||||
let f = Foo { character };
|
let f = Foo { character };
|
||||||
|
|
||||||
let character = f.character == 'a' ? 'a' : f.character;
|
let character2 = f.character == 'a' ? 'a' : f.character;
|
||||||
return character;
|
return character2;
|
||||||
}
|
}
|
||||||
|
@ -37,7 +37,7 @@ function main(
|
|||||||
in30: char,
|
in30: char,
|
||||||
in31: char,
|
in31: char,
|
||||||
in32: char,
|
in32: char,
|
||||||
in32: char,
|
in33: char,
|
||||||
) -> ([char; 33], bool) {
|
) -> ([char; 33], bool) {
|
||||||
let str = [
|
let str = [
|
||||||
in1,
|
in1,
|
||||||
@ -72,8 +72,8 @@ function main(
|
|||||||
in30,
|
in30,
|
||||||
in31,
|
in31,
|
||||||
in32,
|
in32,
|
||||||
in32,
|
in33,
|
||||||
];
|
];
|
||||||
console.log("{}", str);
|
console.log("{}", str);
|
||||||
return (str, in1 == '\x00');
|
return (str, in1 == '\x00');
|
||||||
}
|
}
|
||||||
|
@ -100,6 +100,6 @@ outputs:
|
|||||||
r:
|
r:
|
||||||
type: char
|
type: char
|
||||||
value: "'\\u{1f62d}'"
|
value: "'\\u{1f62d}'"
|
||||||
initial_ast: 715a33d0032f02d69d13687ac98005a789b6bcb63ff619865b21f0c691f14a75
|
initial_ast: 41f5ad78f58a182b6b99dd22151fabb0dc621c4a45c39d087cbc05f89c99eccc
|
||||||
canonicalized_ast: 715a33d0032f02d69d13687ac98005a789b6bcb63ff619865b21f0c691f14a75
|
canonicalized_ast: 41f5ad78f58a182b6b99dd22151fabb0dc621c4a45c39d087cbc05f89c99eccc
|
||||||
type_inferenced_ast: d04164068277e88b5529f1072b512ffadc7eaaf704c8a3e394a409e783cc1e27
|
type_inferenced_ast: 0463676a90b25002f29b0c056e44945f9c461c535bdf11b47112ace4c3e0eac1
|
||||||
|
@ -4,21 +4,21 @@ expectation: Pass
|
|||||||
outputs:
|
outputs:
|
||||||
- circuit:
|
- circuit:
|
||||||
num_public_variables: 0
|
num_public_variables: 0
|
||||||
num_private_variables: 35
|
num_private_variables: 36
|
||||||
num_constraints: 3
|
num_constraints: 3
|
||||||
at: 27242eeb2faf33996c0329ac2ec3b337434f78d392ff29465d3508084de6c721
|
at: 25579220a31118007fe071d3083ad5a5503f7dc6bd4d51abf15f1a7778a99c86
|
||||||
bt: 4727127f178bb02895a615bf38a4aa3c5cb9d2b076eca15ebe6fea741b48ce98
|
bt: 8f5bf097224289e45b78e01a711900a993240585fe13744f9ab71a9c5c4d9111
|
||||||
ct: cae904ba23a045f4438177f10211a50ae29eee49d08211c731aee88353dc0cfb
|
ct: df019f90846f94966d481bfb6d579bee9c47d281176e210ccd973210afc957a1
|
||||||
output:
|
output:
|
||||||
- input_file: inputs/nonprinting.in
|
- input_file: inputs/nonprinting.in
|
||||||
output:
|
output:
|
||||||
registers:
|
registers:
|
||||||
r0:
|
r0:
|
||||||
type: "[char; 33]"
|
type: "[char; 33]"
|
||||||
value: "\"\\u{0}\\u{1}\\u{2}\\u{3}\\u{4}\\u{5}\\u{6}\\u{7}\\u{8}\\t\\n\\u{b}\\u{c}\\r\\u{e}\\u{f}\\u{10}\\u{11}\\u{12}\\u{13}\\u{14}\\u{15}\\u{16}\\u{17}\\u{18}\\u{19}\\u{1a}\\u{1b}\\u{1c}\\u{1d}\\u{1e}\\u{1f}\\u{1f}\""
|
value: "\"\\u{0}\\u{1}\\u{2}\\u{3}\\u{4}\\u{5}\\u{6}\\u{7}\\u{8}\\t\\n\\u{b}\\u{c}\\r\\u{e}\\u{f}\\u{10}\\u{11}\\u{12}\\u{13}\\u{14}\\u{15}\\u{16}\\u{17}\\u{18}\\u{19}\\u{1a}\\u{1b}\\u{1c}\\u{1d}\\u{1e}\\u{1f} \""
|
||||||
r1:
|
r1:
|
||||||
type: bool
|
type: bool
|
||||||
value: "true"
|
value: "true"
|
||||||
initial_ast: b03b0ea8ad821952fa64e477900b43c830e9fbd9693478018ad4b13abd12b027
|
initial_ast: 4e9ef2d8121eabed385e2d358e2d9ed1dc64d88894c3dbfc078d5da34902ce4c
|
||||||
canonicalized_ast: b03b0ea8ad821952fa64e477900b43c830e9fbd9693478018ad4b13abd12b027
|
canonicalized_ast: 4e9ef2d8121eabed385e2d358e2d9ed1dc64d88894c3dbfc078d5da34902ce4c
|
||||||
type_inferenced_ast: 4ded1909fcd3fa1edf7de8111d3f7b97fced37b5b2d18b316f9fee3aad246f5e
|
type_inferenced_ast: 489e02b2ed42362bf493fe2fb58cf03ab06cfb95abd49b7ba0329a8e8d7c3daa
|
||||||
|
Loading…
Reference in New Issue
Block a user