Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Feat: Dafny-to-Rust code indentation and identifiers #4974

Merged
merged 43 commits into from
Feb 7, 2024
Merged

Feat: Dafny-to-Rust code indentation and identifiers #4974

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
0628309
Added initial tests to support allocation
MikaelMayer Dec 21, 2023
7649600
Implemented codatatypes
MikaelMayer Dec 21, 2023
06c65ba
Sequences now defined. Only need to define more methods
MikaelMayer Dec 22, 2023
5fc5bf4
Support for traits and mutable variables without dynamic dispatch(?)
MikaelMayer Dec 22, 2023
b72cec9
Arguments always borrowed, deallocation more general now
MikaelMayer Dec 25, 2023
c2f8b24
Conversion to/from Rust strings, better handling of is_string
MikaelMayer Dec 26, 2023
bed8f90
Got rid of DafnyClone
MikaelMayer Dec 26, 2023
79f1503
Immutable lazy maps
MikaelMayer Dec 26, 2023
4b0fae7
Support to subtype testing
MikaelMayer Dec 27, 2023
754022c
Make sure StreamReaders are closed after use
MikaelMayer Dec 27, 2023
22a2897
Formatting fix 2
MikaelMayer Dec 27, 2023
ae3081c
Needed to updated GeneratedFromDafny apparently
MikaelMayer Dec 27, 2023
705b1ca
Aligning with existing runtime
MikaelMayer Dec 27, 2023
13defc6
More idiomatic rust identifiers, started to deal with indentation
MikaelMayer Dec 27, 2023
ded93a3
Allow dead code + finished all trivial impl
MikaelMayer Dec 27, 2023
70e1dcf
Added standard library
MikaelMayer Dec 27, 2023
6c6236a
Support for subset of standard libraries
MikaelMayer Dec 28, 2023
aa3e84a
much better Rust output
MikaelMayer Dec 28, 2023
eccae5e
Proof that ID encoding is bijective so that there is no collision
MikaelMayer Dec 30, 2023
5ba5c93
Constant initialization for datatypes and tests with closures
MikaelMayer Jan 10, 2024
c7fb7c0
Merge branch 'master' into feat-rust
MikaelMayer Jan 10, 2024
770da14
Fixed the merge build
MikaelMayer Jan 10, 2024
1cb67f2
Merge branch 'master' into feat-rust-indentation
MikaelMayer Jan 18, 2024
be32004
Fixed the build
MikaelMayer Jan 19, 2024
d0d51db
Merge branch 'master' into feat-rust-indentation
MikaelMayer Jan 19, 2024
a02d416
Merge branch 'master' into feat-rust-indentation
MikaelMayer Jan 19, 2024
4ace3fc
Fixed CI test issue
MikaelMayer Jan 22, 2024
8d0e038
Merge branch 'feat-rust-indentation' of https://github.com/dafny-lang…
MikaelMayer Jan 22, 2024
a8e39f3
Merge branch 'master' into feat-rust-indentation
MikaelMayer Jan 22, 2024
3bd7222
Merge branch 'master' into feat-rust-indentation
MikaelMayer Jan 23, 2024
3de581a
fixed makefile
MikaelMayer Jan 23, 2024
98fd9a1
Merge branch 'master' into feat-rust-indentation
MikaelMayer Jan 23, 2024
e44508e
Merge branch 'feat-rust-indentation' of https://github.com/dafny-lang…
MikaelMayer Jan 23, 2024
f017545
Formatting
MikaelMayer Jan 23, 2024
6e8c650
Merge branch 'master' into feat-rust-indentation
MikaelMayer Jan 23, 2024
965b7bd
should review comment
MikaelMayer Feb 1, 2024
69aeac1
Merge branch 'feat-rust-indentation' of https://github.com/dafny-lang…
MikaelMayer Feb 1, 2024
65cdcc5
Removed is_string and node_count
MikaelMayer Feb 1, 2024
ac460b1
Removed experimentation file
MikaelMayer Feb 1, 2024
037b54a
Merge branch 'master' into feat-rust-indentation
MikaelMayer Feb 2, 2024
837ff9b
Fixed the merge build
MikaelMayer Feb 2, 2024
79fcfb9
Fixed CI
MikaelMayer Feb 6, 2024
32b8ee8
Merge branch 'master' into feat-rust-indentation
MikaelMayer Feb 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 18 additions & 7 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
DIR=$(dir $(realpath $(firstword $(MAKEFILE_LIST))))
DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST))))

default: exe

Expand All @@ -7,9 +7,20 @@ all: exe refman
exe:
(cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser

dfydev:
(cd ${DIR}/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
(cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
dfyprodformat:
(cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .)

dfyprodinit:
(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)

dfyprod: dfyprodformat dfyprodinit
(cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser

dfydevinit:
(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify --no-format)

dfydev: dfydevinit
(cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser

boogie: ${DIR}/boogie/Binaries/Boogie.exe

Expand All @@ -29,7 +40,7 @@ refman-release: exe
make -C ${DIR}/docs/DafnyRef release

z3-mac:
mkdir -p ${DIR}Binaries/z3/bin
mkdir -p ${DIR}/Binaries/z3/bin
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip
unzip z3-4.12.1-x64-macos-11-bin.zip
rm z3-4.12.1-x64-macos-11-bin.zip
Expand All @@ -40,7 +51,7 @@ z3-mac:
chmod +x ${DIR}/Binaries/z3/bin/z3-*

z3-mac-arm:
mkdir -p ${DIR}Binaries/z3/bin
mkdir -p ${DIR}/Binaries/z3/bin
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-arm64-macos-11-bin.zip
unzip z3-4.12.1-arm64-macos-11-bin.zip
rm z3-4.12.1-arm64-macos-11-bin.zip
Expand All @@ -51,7 +62,7 @@ z3-mac-arm:
chmod +x ${DIR}/Binaries/z3/bin/z3-*

z3-ubuntu:
mkdir -p ${DIR}Binaries/z3/bin
mkdir -p ${DIR}/Binaries/z3/bin
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
rm z3-4.12.1-x64-ubuntu-20.04-bin.zip
Expand Down
29 changes: 17 additions & 12 deletions Source/DafnyCore/Compilers/Dafny/AST.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,14 @@
module {:extern "DAST"} DAST {
import opened Std.Wrappers

datatype Module = Module(name: string, isExtern: bool, body: seq<ModuleItem>)

datatype ModuleItem = Module(Module) | Class(Class) | Trait(Trait) | Newtype(Newtype) | Datatype(Datatype)
datatype ModuleItem =
| Module(Module)
| Class(Class)
| Trait(Trait)
| Newtype(Newtype)
| Datatype(Datatype)

datatype Type =
Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) |
Expand Down Expand Up @@ -30,29 +37,27 @@ module {:extern "DAST"} DAST {

datatype DatatypeCtor = DatatypeCtor(name: string, args: seq<Formal>, hasAnyArgs: bool /* includes ghost */)

datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Optional<Expression>)
datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>)

datatype ClassItem = Method(Method)

datatype Field = Field(formal: Formal, defaultValue: Optional<Expression>)
datatype Field = Field(formal: Formal, defaultValue: Option<Expression>)

datatype Formal = Formal(name: string, typ: Type)

datatype Method = Method(isStatic: bool, hasBody: bool, overridingPath: Optional<seq<Ident>>, name: string, typeParams: seq<Type>, params: seq<Formal>, body: seq<Statement>, outTypes: seq<Type>, outVars: Optional<seq<Ident>>)

datatype Optional<T> = Some(T) | None
datatype Method = Method(isStatic: bool, hasBody: bool, overridingPath: Option<seq<Ident>>, name: string, typeParams: seq<Type>, params: seq<Formal>, body: seq<Statement>, outTypes: seq<Type>, outVars: Option<seq<Ident>>)

datatype Statement =
DeclareVar(name: string, typ: Type, maybeValue: Optional<Expression>) |
DeclareVar(name: string, typ: Type, maybeValue: Option<Expression>) |
Assign(lhs: AssignLhs, value: Expression) |
If(cond: Expression, thn: seq<Statement>, els: seq<Statement>) |
Labeled(lbl: string, body: seq<Statement>) |
While(cond: Expression, body: seq<Statement>) |
Foreach(boundName: string, boundType: Type, over: Expression, body: seq<Statement>) |
Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Optional<seq<Ident>>) |
Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) |
Return(expr: Expression) |
EarlyReturn() |
Break(toLabel: Optional<string>) |
Break(toLabel: Option<string>) |
TailRecursive(body: seq<Statement>) |
JumpTailCallStart() |
Halt() |
Expand All @@ -70,9 +75,9 @@ module {:extern "DAST"} DAST {
Neq(referential: bool, nullable: bool) |
Div() | EuclidianDiv() |
Mod() | EuclidianMod() |
Implies() |
Implies() | // TODO: REplace by Not Or
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That seems like a good idea to me, but it assumes that the goal of the DAST is to be as simple as possible, rather than retaining extra information that might produce better output in some contexts. I think that's a good design goal personally, but this file should be more explicit about documenting that.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ideally I want:

  • The Compiled Dafny AST to be minimal
  • We want the generated code to look idiomatic and close to the original Dafny file if possible.

I was able to accomplish both goals the following way, as this step has already been accomplished in the next PR. The design is the following:

  1. We keep only the minimum amount of operators (so BinaryOp(Implies, x, y) becomes BinaryOp(Or, Not(x), y), same for all the variants of <= and < and != and == etc.
  2. I added a "format" attribute to BinaryOp and UnaryOp so that compilers can decide to enhance the rendering of the operators based on original Dafny information, but that should only be an optional idiomatic rendering step or a transformation of the target language AST to another more idiomatic target language AST.
    This ensures conversions are done minimally .

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ideally I want:

  • The Compiled Dafny AST to be minimal
  • We want the generated code to look idiomatic and close to the original Dafny file if possible.

Both good goals to have, but there will be times when they conflict. :)

Sounds like you're saying in this case we might annotate the AST further if we decided we need to know when the original Dafny source was A ==> B as opposed to !A || B. I think that's a reasonable general approach: keep the AST itself minimal so getting to simple correct translation is easier, but add more additional information when you feel the need to improve the output.

I think it's worth stating that tenet in or around this file somewhere.

Copy link
Member Author

@MikaelMayer MikaelMayer Jan 25, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just added to the top of AST.dfy for the next PR:

  // Dafny AST compilation tenets:
  // - The Compiled Dafny AST should be minimal
  // - The generated code should look idiomatic and close to the original Dafny file if possible
  // Since the two might conflict, the second one is taken care of by adding formatting information

In() |
NotIn() |
NotIn() | // TODO: Replace by Not In
SetDifference() |
Concat() |
Passthrough(string)
Expand All @@ -98,7 +103,7 @@ module {:extern "DAST"} DAST {
Select(expr: Expression, field: string, isConstant: bool, onDatatype: bool) |
SelectFn(expr: Expression, field: string, onDatatype: bool, isStatic: bool, arity: nat) |
Index(expr: Expression, collKind: CollKind, indices: seq<Expression>) |
IndexRange(expr: Expression, isArray: bool, low: Optional<Expression>, high: Optional<Expression>) |
IndexRange(expr: Expression, isArray: bool, low: Option<Expression>, high: Option<Expression>) |
TupleSelect(expr: Expression, index: nat) |
Call(on: Expression, name: Ident, typeArgs: seq<Type>, args: seq<Expression>) |
Lambda(params: seq<Formal>, retType: Type, body: seq<Statement>) |
Expand Down
24 changes: 13 additions & 11 deletions Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,9 @@
using System.Collections.Generic;
using Dafny;
using DAST;
using Microsoft.CodeAnalysis;
using Microsoft.Dafny.Compilers;
using Std.Wrappers;

namespace Microsoft.Dafny.Compilers {

Expand Down Expand Up @@ -97,7 +99,7 @@ public void AddMethod(DAST.Method item) {
body.Add(item);
}

public void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue) {
public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
fields.Add((DAST.Field)DAST.Field.create_Field(item, defaultValue));
}

Expand Down Expand Up @@ -146,7 +148,7 @@ public void AddMethod(DAST.Method item) {
body.Add(item);
}

public void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue) {
public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
}

Expand Down Expand Up @@ -189,7 +191,7 @@ public void AddMethod(DAST.Method item) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
}

public void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue) {
public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
}

Expand All @@ -199,7 +201,7 @@ public object Finish() {
Sequence<DAST.Type>.FromArray(this.typeParams.ToArray()),
this.baseType,
Sequence<DAST.Statement>.FromArray(this.witnessStmts.ToArray()),
this.witness == null ? Optional<DAST._IExpression>.create_None() : Optional<DAST._IExpression>.create_Some(this.witness)
this.witness == null ? Option<DAST._IExpression>.create_None() : Option<DAST._IExpression>.create_Some(this.witness)
));
return parent;
}
Expand Down Expand Up @@ -235,7 +237,7 @@ public void AddMethod(DAST.Method item) {
body.Add(item);
}

public void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue) {
public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
}

Expand All @@ -255,7 +257,7 @@ public object Finish() {
interface ClassLike {
void AddMethod(DAST.Method item);

void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue);
void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue);

public MethodBuilder Method(
bool isStatic, bool hasBody,
Expand Down Expand Up @@ -324,13 +326,13 @@ public DAST.Method Build() {
return (DAST.Method)DAST.Method.create(
isStatic,
hasBody,
overridingPath != null ? Optional<ISequence<ISequence<Rune>>>.create_Some(overridingPath) : Optional<ISequence<ISequence<Rune>>>.create_None(),
overridingPath != null ? Option<ISequence<ISequence<Rune>>>.create_Some(overridingPath) : Option<ISequence<ISequence<Rune>>>.create_None(),
Sequence<Rune>.UnicodeFromString(this.name),
Sequence<DAST.Type>.FromArray(typeArgs.ToArray()),
Sequence<DAST.Formal>.FromArray(params_.ToArray()),
Sequence<DAST.Statement>.FromArray(builtStatements.ToArray()),
Sequence<DAST.Type>.FromArray(outTypes.ToArray()),
outVars != null ? Optional<ISequence<ISequence<Rune>>>.create_Some(Sequence<ISequence<Rune>>.FromArray(outVars.ToArray())) : Optional<ISequence<ISequence<Rune>>>.create_None()
outVars != null ? Option<ISequence<ISequence<Rune>>>.create_Some(Sequence<ISequence<Rune>>.FromArray(outVars.ToArray())) : Option<ISequence<ISequence<Rune>>>.create_None()
);
}
}
Expand Down Expand Up @@ -473,11 +475,11 @@ public void AddBuildable(BuildableExpr value) {

public DAST.Statement Build() {
if (this.value == null) {
return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, DAST.Optional<DAST._IExpression>.create_None());
return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, Option<DAST._IExpression>.create_None());
} else {
var builtValue = new List<DAST.Expression>();
ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, DAST.Optional<DAST._IExpression>.create_Some(builtValue[0]));
return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, Option<DAST._IExpression>.create_Some(builtValue[0]));
}
}
}
Expand Down Expand Up @@ -820,7 +822,7 @@ public DAST.Statement Build() {
Sequence<Rune>.UnicodeFromString(name),
Sequence<DAST.Type>.FromArray(typeArgs.ToArray()),
Sequence<DAST.Expression>.FromArray(builtArgs.ToArray()),
outs == null ? DAST.Optional<ISequence<ISequence<Rune>>>.create_None() : DAST.Optional<ISequence<ISequence<Rune>>>.create_Some(Sequence<ISequence<Rune>>.FromArray(outs.ToArray()))
outs == null ? Option<ISequence<ISequence<Rune>>>.create_None() : Option<ISequence<ISequence<Rune>>>.create_Some(Sequence<ISequence<Rune>>.FromArray(outs.ToArray()))
);
}
}
Expand Down
31 changes: 16 additions & 15 deletions Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
using Microsoft.BaseTypes;
using System.Linq;
using System.Diagnostics.Contracts;
using Std.Wrappers;

namespace Microsoft.Dafny.Compilers {

Expand Down Expand Up @@ -519,7 +520,7 @@ public ConcreteSyntaxTree CreateGetterSetter(string name, Type resultType, IToke

public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, bool isConst, Type type,
IToken tok, string rhs, Field field) {
_IOptional<DAST._IExpression> rhsExpr = null;
_IOption<DAST._IExpression> rhsExpr = null;
if (rhs != null) {
rhsExpr = compiler.bufferedInitializationValue;
compiler.bufferedInitializationValue = null;
Expand All @@ -528,7 +529,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic,
throw new InvalidOperationException();
}
} else {
rhsExpr = Optional<DAST._IExpression>.create_None();
rhsExpr = Option<DAST._IExpression>.create_None();
}

builder.AddField((DAST.Formal)DAST.Formal.create_Formal(
Expand Down Expand Up @@ -571,7 +572,7 @@ protected override void EmitReturnExpr(string returnExpr, ConcreteSyntaxTree wr)

if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
var returnBuilder = stmtContainer.Builder.Return();
returnBuilder.AddExpr((DAST.Expression)rhsValue.dtor_Some_a0);
returnBuilder.AddExpr((DAST.Expression)rhsValue.dtor_value);
} else {
throw new InvalidOperationException();
}
Expand Down Expand Up @@ -615,7 +616,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok,

// sometimes, the compiler generates the initial value before the declaration,
// so we buffer it here
_IOptional<DAST._IExpression> bufferedInitializationValue = null;
_IOption<DAST._IExpression> bufferedInitializationValue = null;

protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok,
bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) {
Expand All @@ -624,38 +625,38 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
} else {
type = type.NormalizeExpandKeepConstraints();
if (usePlaceboValue) {
bufferedInitializationValue = Optional<DAST._IExpression>.create_None();
bufferedInitializationValue = Option<DAST._IExpression>.create_None();
} else {
if (type.AsNewtype != null && type.AsNewtype.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var buf = new ExprBuffer(null);
EmitExpr(type.AsNewtype.Witness, false, new BuilderSyntaxTree<ExprContainer>(buf), null);
bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(buf.Finish());
bufferedInitializationValue = Option<DAST._IExpression>.create_Some(buf.Finish());
} else if (type.AsSubsetType != null && type.AsSubsetType.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var buf = new ExprBuffer(null);
EmitExpr(type.AsSubsetType.Witness, false, new BuilderSyntaxTree<ExprContainer>(buf), null);
bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(buf.Finish());
bufferedInitializationValue = Option<DAST._IExpression>.create_Some(buf.Finish());
} else if (type.AsDatatype != null && type.AsDatatype.Ctors.Count == 1 && type.AsDatatype.Ctors[0].EnclosingDatatype is TupleTypeDecl tupleDecl) {
var elems = new List<DAST._IExpression>();
for (var i = 0; i < tupleDecl.Ctors[0].Formals.Count; i++) {
if (!tupleDecl.Ctors[0].Formals[i].IsGhost) {
TypeInitializationValue(type.TypeArgs[i], wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
elems.Add(bufferedInitializationValue.dtor_Some_a0);
elems.Add(bufferedInitializationValue.dtor_value);
bufferedInitializationValue = null;
}
}

if (elems.Count == 1) {
bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(elems[0]);
bufferedInitializationValue = Option<DAST._IExpression>.create_Some(elems[0]);
} else {
bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(
bufferedInitializationValue = Option<DAST._IExpression>.create_Some(
DAST.Expression.create_Tuple(Sequence<DAST._IExpression>.FromArray(elems.ToArray()))
);
}
} else if (type.IsArrowType) {
throwGeneralUnsupported();
throw new InvalidOperationException();
} else {
bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(
bufferedInitializationValue = Option<DAST._IExpression>.create_Some(
DAST.Expression.create_InitializationValue(GenType(type))
);
}
Expand Down Expand Up @@ -958,7 +959,7 @@ protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool creat
protected override void EmitBreak(string label, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_Break(
label == null ? Optional<ISequence<Rune>>.create_None() : Optional<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString("goto_" + label))
label == null ? Option<ISequence<Rune>>.create_None() : Option<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString("goto_" + label))
));
} else {
throw new InvalidOperationException();
Expand All @@ -968,7 +969,7 @@ protected override void EmitBreak(string label, ConcreteSyntaxTree wr) {
protected override void EmitContinue(string label, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_Break(
Optional<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString("continue_" + label))
Option<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString("continue_" + label))
));
} else {
throw new InvalidOperationException();
Expand Down Expand Up @@ -1781,8 +1782,8 @@ protected override void EmitSeqSelectRange(Expression source, Expression lo, Exp
builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_IndexRange(
sourceExpr,
fromArray,
loExpr != null ? Optional<DAST._IExpression>.create_Some(loExpr) : Optional<DAST._IExpression>.create_None(),
hiExpr != null ? Optional<DAST._IExpression>.create_Some(hiExpr) : Optional<DAST._IExpression>.create_None()
loExpr != null ? Option<DAST._IExpression>.create_Some(loExpr) : Option<DAST._IExpression>.create_None(),
hiExpr != null ? Option<DAST._IExpression>.create_Some(hiExpr) : Option<DAST._IExpression>.create_None()
));
} else {
throw new InvalidOperationException();
Expand Down
Loading
Loading