forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Compiler-dafny.cs
2380 lines (2081 loc) · 99.8 KB
/
Compiler-dafny.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
using System;
using System.Collections.Generic;
using Dafny;
using JetBrains.Annotations;
using DAST;
using System.Numerics;
using Microsoft.BaseTypes;
using System.Linq;
using System.Diagnostics.Contracts;
namespace Microsoft.Dafny.Compilers {
class BuilderSyntaxTree<T> : ConcreteSyntaxTree {
public readonly T Builder;
public BuilderSyntaxTree(T builder) {
if (builder == null) {
throw new ArgumentNullException(nameof(builder));
}
Builder = builder;
}
public override ConcreteSyntaxTree Fork(int relativeIndent = 0) {
if (Builder is StatementContainer statementContainer) {
return new BuilderSyntaxTree<StatementContainer>(statementContainer.Fork());
} else {
DafnyCompiler.throwGeneralUnsupported(); // Warning: this is an invalid operation: cannot fork builder of type Builder.GetType()
throw new InvalidOperationException();
}
}
public override ConcreteSyntaxTree ForkInParens() {
// TODO(shadaj): perhaps should check if we are an expr container
return new BuilderSyntaxTree<T>(Builder);
}
}
class DafnyCompiler : SinglePassCompiler {
ProgramBuilder items;
public object currentBuilder;
public void Start() {
if (items != null) {
throw new InvalidOperationException("");
}
items = new ProgramBuilder();
this.currentBuilder = items;
}
public List<Module> Build() {
var res = items.Finish();
items = null;
this.currentBuilder = null;
return res;
}
public DafnyCompiler(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
options.SystemModuleTranslationMode = CommonOptionBag.SystemModuleMode.Include;
if (Options?.CoverageLegendFile != null) {
Imports.Add("DafnyProfiling");
}
}
public static void throwGeneralUnsupported() {
// throw new InvalidOperationException(); // (useful for debugging)
throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
}
public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
Feature.Ordinals,
Feature.Iterators,
Feature.Multisets,
Feature.MapComprehensions,
Feature.MethodSynthesis,
Feature.ExternalClasses,
Feature.NewObject,
Feature.NonSequentializableForallStatements,
Feature.MapItems,
Feature.RunAllTests,
Feature.ExactBoundedPool,
Feature.SequenceDisplaysOfCharacters,
Feature.TypeTests,
Feature.SubsetTypeTests,
Feature.BitvectorRotateFunctions,
Feature.AssignSuchThatWithNonFiniteBounds,
Feature.SequenceUpdateExpressions,
Feature.SequenceConstructionsWithNonLambdaInitializers,
Feature.ExternalConstructors,
Feature.SubtypeConstraintsInQuantifiers,
Feature.TuplesWiderThan20,
Feature.ForLoops,
Feature.Traits,
Feature.RuntimeCoverageReport
};
private readonly List<string> Imports = new() { DafnyDefaultModule };
private const string DafnyRuntimeModule = "_dafny";
private const string DafnyDefaultModule = "module_";
protected override string AssignmentSymbol { get => null; }
protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
}
public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
throwGeneralUnsupported();
throw new InvalidOperationException();
}
protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) {
throwGeneralUnsupported();
throw new InvalidOperationException();
}
protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName, ConcreteSyntaxTree wr) {
if (currentBuilder is ModuleContainer moduleBuilder) {
currentBuilder = moduleBuilder.Module(moduleName, externModule != null);
} else {
throw new InvalidOperationException();
}
return wr;
}
protected override void FinishModule() {
if (currentBuilder is ModuleBuilder builder) {
currentBuilder = builder.Finish();
} else {
throw new InvalidOperationException();
}
}
protected override string GetHelperModuleName() => DafnyRuntimeModule;
private static string MangleName(string name) {
return name;
}
protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to, IToken tok, ConcreteSyntaxTree wr, Type toOrig = null) {
if (currentBuilder is ExprBuffer buf && wr is not BuilderSyntaxTree<ExprContainer>) {
// the writers are not currently wired properly for DatatypeValue
wr = new BuilderSyntaxTree<ExprContainer>(buf);
}
if (from == to) {
return wr;
}
if (from != null && to != null && from.IsNonNullRefType != to.IsNonNullRefType) {
if (wr is BuilderSyntaxTree<ExprContainer> stmt) {
var nullConvert = stmt.Builder.Convert(GenType(from), GenType(to));
if (from is UserDefinedType fromUdt && fromUdt.ResolvedClass is NonNullTypeDecl fromNonNull) {
from = fromNonNull.RhsWithArgument(fromUdt.TypeArgs);
}
if (to is UserDefinedType toUdt && toUdt.ResolvedClass is NonNullTypeDecl toNonNull) {
to = toNonNull.RhsWithArgument(toUdt.TypeArgs);
}
return EmitCoercionIfNecessary(from, to, tok, new BuilderSyntaxTree<ExprContainer>(nullConvert));
} else {
return base.EmitCoercionIfNecessary(from, to, tok, wr);
}
} else if (from != null && to != null && (from.AsSubsetType != null || to.AsSubsetType != null)) {
if (wr is BuilderSyntaxTree<ExprContainer> stmt) {
return new BuilderSyntaxTree<ExprContainer>(stmt.Builder.Convert(GenType(from), GenType(to)));
} else {
return base.EmitCoercionIfNecessary(from, to, tok, wr);
}
} else {
if (from == null || to == null || from.Equals(to, true)) {
return wr;
} else {
throwGeneralUnsupported();
throw new InvalidOperationException();
}
}
}
protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string fullPrintName,
List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type> superClasses, IToken tok, ConcreteSyntaxTree wr) {
if (currentBuilder is ClassContainer builder) {
List<DAST.Type> typeParams = new();
foreach (var tp in typeParameters) {
if (!isTpSupported(tp)) {
throwGeneralUnsupported(); //("Contravariance in type parameters");
}
typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(IdProtect(tp.GetCompileName(Options)))));
}
return new ClassWriter(this, typeParams.Count > 0, builder.Class(name, moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList()));
} else {
throw new InvalidOperationException();
}
}
protected override IClassWriter CreateTrait(string name, bool isExtern, List<TypeParameter> typeParameters,
TraitDecl trait, List<Type> superClasses, IToken tok, ConcreteSyntaxTree wr) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.Traits);
// traits need a bit more work
// if (currentBuilder is TraitContainer builder) {
// List<DAST.Type> typeParams = new();
// foreach (var tp in trait.TypeArgs) {
// typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(IdProtect(tp.GetCompileName(Options)))));
// }
// return new ClassWriter(this, builder.Trait(name, typeParams));
// } else {
// throw new InvalidOperationException();
// }
}
protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, ConcreteSyntaxTree wr) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.Iterators);
}
private static bool isTpSupported(TypeParameter tp) {
return tp.Variance == TypeParameter.TPVariance.Non &&
tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified;
}
protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxTree wr) {
if (currentBuilder is DatatypeContainer builder) {
List<DAST.Type> typeParams = new();
foreach (var tp in dt.TypeArgs) {
if (!isTpSupported(tp) && !(dt is TupleTypeDecl)) {
throwGeneralUnsupported(); //("Contravariance in type parameters");
}
typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(IdProtect(tp.GetCompileName(Options)))));
}
List<DAST.DatatypeCtor> ctors = new();
foreach (var ctor in dt.Ctors) {
List<DAST.Formal> args = new();
foreach (var arg in ctor.Formals) {
if (!arg.IsGhost) {
args.Add((DAST.Formal)DAST.Formal.create_Formal(Sequence<Rune>.UnicodeFromString(arg.CompileName), GenType(arg.Type)));
}
}
ctors.Add((DAST.DatatypeCtor)DAST.DatatypeCtor.create_DatatypeCtor(Sequence<Rune>.UnicodeFromString(ctor.GetCompileName(Options)), Sequence<DAST.Formal>.FromArray(args.ToArray()), ctor.Formals.Count > 0));
}
return new ClassWriter(this, typeParams.Count > 0, builder.Datatype(
dt.GetCompileName(Options),
dt.EnclosingModuleDefinition.GetCompileName(Options),
typeParams,
ctors,
dt is CoDatatypeDecl
));
} else {
throw new InvalidOperationException("Cannot declare datatype outside of a module: " + currentBuilder);
}
}
protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
if (currentBuilder is NewtypeContainer builder) {
List<DAST.Statement> witnessStmts = new();
DAST.Expression witness = null;
if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var buf = new ExprBuffer(null);
var statementBuf = new StatementBuffer();
EmitExpr(
nt.Witness, false,
EmitCoercionIfNecessary(nt.Witness.Type, nt.BaseType, null, new BuilderSyntaxTree<ExprContainer>(buf)),
new BuilderSyntaxTree<StatementContainer>(statementBuf)
);
witness = buf.Finish();
witnessStmts = statementBuf.PopAll();
}
return new ClassWriter(this, false, builder.Newtype(nt.GetCompileName(Options), new(), GenType(nt.BaseType), witnessStmts, witness));
} else {
throw new InvalidOperationException();
}
}
private DAST.Type GenType(Type typ) {
// TODO(shadaj): this is leaking Rust types into the AST, but we do need native types
var xType = DatatypeWrapperEraser.SimplifyType(Options, typ, true);
if (xType is BoolType) {
return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_Bool());
} else if (xType is IntType) {
return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_Int());
} else if (xType is RealType) {
return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_Real());
} else if (xType.IsStringType) {
return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_String());
} else if (xType.IsCharType) {
return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_Char());
} else if (xType is UserDefinedType udt) {
if (udt.ResolvedClass is TypeParameter tp) {
if (thisContext != null && thisContext.ParentFormalTypeParametersToActuals.TryGetValue(tp, out var instantiatedTypeParameter)) {
return GenType(instantiatedTypeParameter);
}
}
return FullTypeNameAST(udt, null);
} else if (AsNativeType(typ) != null) {
return (DAST.Type)(AsNativeType(typ).Sel switch {
NativeType.Selection.Byte => DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("u8")),
NativeType.Selection.SByte => DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("i8")),
NativeType.Selection.Short => DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("i16")),
NativeType.Selection.UShort => DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("u16")),
NativeType.Selection.Int => DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("i32")),
NativeType.Selection.UInt => DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("u32")),
NativeType.Selection.Long => DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("i64")),
NativeType.Selection.ULong => DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("u64")),
_ => throw new InvalidOperationException(),
});
} else if (xType is SeqType seq) {
var argType = seq.Arg;
return (DAST.Type)DAST.Type.create_Seq(GenType(argType));
} else if (xType is SetType set) {
var argType = set.Arg;
return (DAST.Type)DAST.Type.create_Set(GenType(argType));
} else if (xType is MultiSetType multiSet) {
var argType = multiSet.Arg;
return (DAST.Type)DAST.Type.create_Multiset(GenType(argType));
} else if (xType is MapType map) {
var keyType = map.Domain;
var valueType = map.Range;
return (DAST.Type)DAST.Type.create_Map(GenType(keyType), GenType(valueType));
} else if (xType is BitvectorType) {
throwGeneralUnsupported(); //("Bitvector types");
throw new InvalidOperationException();
} else {
throwGeneralUnsupported(); //("Type name for " + xType + " (" + typ.GetType() + ")");
throw new InvalidOperationException();
}
}
protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) {
if (currentBuilder is NewtypeContainer builder) {
var erasedType = EraseNewtypeLayers(sst);
List<DAST.Statement> witnessStmts = new();
DAST.Expression witness = null;
if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var statementBuf = new StatementBuffer();
var buf = new ExprBuffer(null);
EmitExpr(
sst.Witness, false,
EmitCoercionIfNecessary(sst.Witness.Type, erasedType, null, new BuilderSyntaxTree<ExprContainer>(buf)),
new BuilderSyntaxTree<StatementContainer>(statementBuf)
);
witness = buf.Finish();
witnessStmts = statementBuf.PopAll();
}
List<DAST.Type> typeParams = new();
foreach (var tp in sst.TypeArgs) {
if (!isTpSupported(tp)) {
throwGeneralUnsupported(); //("Contravariance in type parameters");
}
typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(tp.Name)));
}
builder.Newtype(sst.GetCompileName(Options), typeParams, GenType(erasedType), witnessStmts, witness).Finish();
} else {
throw new InvalidOperationException();
}
}
protected override void GetNativeInfo(NativeType.Selection sel, out string name, out string literalSuffix, out bool needsCastAfterArithmetic) {
name = null;
literalSuffix = null;
needsCastAfterArithmetic = false;
}
private class ClassWriter : IClassWriter {
private readonly DafnyCompiler compiler;
private readonly ClassLike builder;
private readonly bool hasTypeArgs;
private readonly List<MethodBuilder> methods = new();
public ClassWriter(DafnyCompiler compiler, bool hasTypeArgs, ClassLike builder) {
this.compiler = compiler;
this.hasTypeArgs = hasTypeArgs;
this.builder = builder;
}
public ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody,
bool forBodyInheritance, bool lookasideBody) {
if (m.IsStatic && this.hasTypeArgs) {
throwGeneralUnsupported(); //("Static methods with type arguments");
}
List<DAST.Type> astTypeArgs = new();
foreach (var typeArg in typeArgs) {
if (!isTpSupported(typeArg.Formal)) {
throwGeneralUnsupported(); //("Contravariance in type parameters")
}
astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options)))));
}
List<DAST.Formal> params_ = new();
foreach (var param in m.Ins) {
if (param is not ImplicitFormal && !param.IsGhost) {
params_.Add((DAST.Formal)DAST.Formal.create_Formal(Sequence<Rune>.UnicodeFromString(compiler.IdProtect(param.CompileName)), compiler.GenType(param.Type)));
}
}
List<ISequence<Rune>> outVars = new();
List<DAST.Type> outTypes = new();
foreach (var outVar in m.Outs) {
if (!outVar.IsGhost) {
outVars.Add(Sequence<Rune>.UnicodeFromString(compiler.IdProtect(outVar.CompileName)));
outTypes.Add(compiler.GenType(outVar.Type));
}
}
var overridingTrait = m.OverriddenMethod?.EnclosingClass;
var builder = this.builder.Method(
m.IsStatic, createBody,
overridingTrait != null ? compiler.PathFromTopLevel(overridingTrait) : null,
m.GetCompileName(compiler.Options),
astTypeArgs, params_,
outTypes, outVars
);
methods.Add(builder);
if (createBody) {
return new BuilderSyntaxTree<StatementContainer>(builder);
} else {
// TODO(shadaj): actually create a trait
return null;
}
}
public ConcreteSyntaxTree SynthesizeMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.MethodSynthesis);
}
public ConcreteSyntaxTree CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs,
List<Formal> formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member,
bool forBodyInheritance, bool lookasideBody) {
if (isStatic && this.hasTypeArgs) {
throwGeneralUnsupported(); //("Static methods with type arguments");
}
List<DAST.Type> astTypeArgs = new();
foreach (var typeArg in typeArgs) {
if (!isTpSupported(typeArg.Formal)) {
throwGeneralUnsupported(); //("Contravariance in type parameters");
}
astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options)))));
}
List<DAST.Formal> params_ = new();
foreach (var param in formals) {
if (!param.IsGhost) {
params_.Add((DAST.Formal)DAST.Formal.create_Formal(Sequence<Rune>.UnicodeFromString(compiler.IdProtect(param.CompileName)), compiler.GenType(param.Type)));
}
}
var overridingTrait = member.OverriddenMember?.EnclosingClass;
var builder = this.builder.Method(
isStatic, createBody,
overridingTrait != null ? compiler.PathFromTopLevel(overridingTrait) : null,
name,
astTypeArgs, params_,
new() {
compiler.GenType(resultType)
}, null
);
methods.Add(builder);
if (createBody) {
return new BuilderSyntaxTree<StatementContainer>(builder);
} else {
return null;
}
}
public ConcreteSyntaxTree CreateGetter(string name, TopLevelDecl enclosingDecl, Type resultType, IToken tok,
bool isStatic, bool isConst, bool createBody, MemberDecl member, bool forBodyInheritance) {
if (isStatic && this.hasTypeArgs) {
throwGeneralUnsupported(); //("Static fields with type arguments");
}
var overridingTrait = member.OverriddenMember?.EnclosingClass;
var builder = this.builder.Method(
isStatic, createBody,
overridingTrait != null ? compiler.PathFromTopLevel(overridingTrait) : null,
name,
new(), new(),
new() {
compiler.GenType(resultType)
}, null
);
methods.Add(builder);
if (createBody) {
return new BuilderSyntaxTree<StatementContainer>(builder);
} else {
return null;
}
}
public ConcreteSyntaxTree CreateGetterSetter(string name, Type resultType, IToken tok,
bool createBody, MemberDecl member, out ConcreteSyntaxTree setterWriter, bool forBodyInheritance) {
throwGeneralUnsupported();
throw new InvalidOperationException();
}
public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, bool isConst, Type type,
IToken tok, string rhs, Field field) {
_IOptional<DAST._IExpression> rhsExpr = null;
if (rhs != null) {
rhsExpr = compiler.bufferedInitializationValue;
compiler.bufferedInitializationValue = null;
if (rhsExpr == null) {
throw new InvalidOperationException();
}
} else {
rhsExpr = Optional<DAST._IExpression>.create_None();
}
builder.AddField((DAST.Formal)DAST.Formal.create_Formal(
Sequence<Rune>.UnicodeFromString(name),
compiler.GenType(type)
), rhsExpr);
}
public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) {
throw new cce.UnreachableException();
}
public ConcreteSyntaxTree ErrorWriter() => null;
public void Finish() {
foreach (var method in methods) {
builder.AddMethod(method.Build());
}
compiler.currentBuilder = builder.Finish();
}
}
protected override ConcreteSyntaxTree EmitReturnExpr(ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
return new BuilderSyntaxTree<ExprContainer>(stmtContainer.Builder.Return());
} else {
throw new InvalidOperationException();
}
}
protected override void EmitReturnExpr(string returnExpr, ConcreteSyntaxTree wr) {
if (returnExpr == "BUFFERED") {
if (bufferedInitializationValue == null) {
throw new InvalidOperationException("Expected a buffered value to have been populated because rhs != null");
}
var rhsValue = bufferedInitializationValue;
bufferedInitializationValue = null;
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
var returnBuilder = stmtContainer.Builder.Return();
returnBuilder.AddExpr((DAST.Expression)rhsValue.dtor_Some_a0);
} else {
throw new InvalidOperationException();
}
} else {
// TODO(shadaj): this may not be robust, we should use the writer version directly
EmitIdentifier(returnExpr, EmitReturnExpr(wr));
}
}
protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToken tok) {
type = DatatypeWrapperEraser.SimplifyType(Options, type);
return type.ToString();
}
protected override ConcreteSyntaxTree EmitMethodReturns(Method m, ConcreteSyntaxTree wr) {
var beforeReturnBlock = wr.Fork();
EmitReturn(m.Outs, wr);
return beforeReturnBlock;
}
protected override ConcreteSyntaxTree EmitTailCallStructure(MemberDecl member, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
var recBuilder = stmtContainer.Builder.TailRecursive();
return new BuilderSyntaxTree<StatementContainer>(recBuilder);
} else {
throw new InvalidOperationException();
}
}
protected override void EmitJumpToTailCallStart(ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_JumpTailCallStart());
} else {
throw new InvalidOperationException();
}
}
internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member = null) {
return "PLACEBO_TYPE";
}
// sometimes, the compiler generates the initial value before the declaration,
// so we buffer it here
_IOptional<DAST._IExpression> bufferedInitializationValue = null;
protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok,
bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) {
if (bufferedInitializationValue != null) {
throw new InvalidOperationException();
} else {
type = type.NormalizeExpandKeepConstraints();
if (usePlaceboValue) {
bufferedInitializationValue = Optional<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());
} 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());
} 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);
bufferedInitializationValue = null;
}
}
if (elems.Count == 1) {
bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(elems[0]);
} else {
bufferedInitializationValue = Optional<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(
DAST.Expression.create_InitializationValue(GenType(type))
);
}
}
return "BUFFERED"; // used by DeclareLocal(Out)Var
}
}
protected override string TypeName_UDT(string fullCompileName, List<TypeParameter.TPVariance> variance,
List<Type> typeArgs, ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments) {
return fullCompileName;
}
protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl member) {
ExprContainer actualBuilder;
if (wr is BuilderSyntaxTree<ExprContainer> st) {
actualBuilder = st.Builder;
} else {
throw new InvalidOperationException();
}
EmitTypeName_Companion(type, new BuilderSyntaxTree<ExprContainer>(actualBuilder), wr, tok, member);
return "";
}
protected override void EmitTypeName_Companion(Type type, ConcreteSyntaxTree wr, ConcreteSyntaxTree surrounding, IToken tok, MemberDecl member) {
if (wr is BuilderSyntaxTree<ExprContainer> container) {
type = UserDefinedType.UpcastToMemberEnclosingType(type, member);
if (type.NormalizeExpandKeepConstraints() is UserDefinedType udt && udt.ResolvedClass is DatatypeDecl dt &&
DatatypeWrapperEraser.IsErasableDatatypeWrapper(Options, dt, out _)) {
container.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Companion(PathFromTopLevel(udt.ResolvedClass)));
} else {
container.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Companion(PathFromTopLevel(type.AsTopLevelTypeWithMembers)));
}
} else {
throw new InvalidOperationException();
}
}
protected override void EmitNameAndActualTypeArgs(string protectedName, List<Type> typeArgs, IToken tok, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<ExprContainer> st && st.Builder is CallExprBuilder callExpr) {
callExpr.SetName(protectedName);
} else if (wr is BuilderSyntaxTree<ExprContainer> st2 && st2.Builder is CallStmtBuilder callStmt) {
callStmt.SetName(protectedName);
} else {
throwGeneralUnsupported();
}
base.EmitNameAndActualTypeArgs(protectedName, typeArgs, tok, wr);
}
protected override void TypeArgDescriptorUse(bool isStatic, bool lookasideBody, TopLevelDeclWithMembers cl, out bool needsTypeParameter, out bool needsTypeDescriptor) {
needsTypeParameter = false;
needsTypeDescriptor = false;
}
protected override bool DeclareFormal(string prefix, string name, Type type, IToken tok, bool isInParam, ConcreteSyntaxTree wr) {
throwGeneralUnsupported();
throw new InvalidOperationException();
}
protected override void DeclareLocalVar(string name, Type type, IToken tok, bool leaveRoomForRhs, string rhs,
ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
var typ = GenType(type);
if (rhs == null) {
// we expect an initializer to come *after* this declaration
var variable = stmtContainer.Builder.DeclareAndAssign(typ, name);
if (leaveRoomForRhs) {
throw new InvalidOperationException();
}
} else if (rhs == "BUFFERED") {
if (bufferedInitializationValue == null) {
throw new InvalidOperationException("Expected a buffered value to have been populated because rhs != null");
}
var rhsValue = bufferedInitializationValue;
bufferedInitializationValue = null;
stmtContainer.Builder.AddStatement(
(DAST.Statement)DAST.Statement.create_DeclareVar(
Sequence<Rune>.UnicodeFromString(name),
typ,
rhsValue
)
);
} else {
throw new InvalidOperationException();
}
} else {
throw new InvalidOperationException("Cannot declare local var outside of a statement container: " + wr);
}
}
protected override ConcreteSyntaxTree DeclareLocalVar(string name, Type type, IToken tok, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
var variable = stmtContainer.Builder.DeclareAndAssign(GenType(type), name);
return new BuilderSyntaxTree<ExprContainer>(variable);
} else {
throw new InvalidOperationException();
}
}
protected override bool UseReturnStyleOuts(Method m, int nonGhostOutCount) => true;
protected override bool SupportsMultipleReturns => true;
protected override void DeclareLocalOutVar(string name, Type type, IToken tok, string rhs, bool useReturnStyleOuts,
ConcreteSyntaxTree wr) {
DeclareLocalVar(name, type, tok, true, rhs, wr);
}
protected override void EmitCallReturnOuts(List<string> outTmps, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<ExprContainer> builder && builder.Builder is CallStmtBuilder call) {
call.SetOuts(outTmps.Select(i => Sequence<Rune>.UnicodeFromString(i)).ToList());
} else {
throw new InvalidOperationException();
}
}
protected override void TrCallStmt(CallStmt s, string receiverReplacement, ConcreteSyntaxTree wr, ConcreteSyntaxTree wrStmts, ConcreteSyntaxTree wrStmtsAfterCall) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
if (s.Method == enclosingMethod && enclosingMethod.IsTailRecursive) {
base.TrCallStmt(s, receiverReplacement, wr, wrStmts, wrStmtsAfterCall);
} else {
var callBuilder = stmtContainer.Builder.Call();
base.TrCallStmt(s, receiverReplacement, new BuilderSyntaxTree<ExprContainer>(callBuilder), wrStmts, wrStmtsAfterCall);
}
} else {
throw new InvalidOperationException("Cannot call statement in this context: " + currentBuilder);
}
}
protected override void EmitCallToInheritedMethod(Method method, [CanBeNull] TopLevelDeclWithMembers heir, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, ConcreteSyntaxTree wStmtsAfterCall) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
var callBuilder = stmtContainer.Builder.Call();
base.EmitCallToInheritedMethod(method, heir, new BuilderSyntaxTree<ExprContainer>(callBuilder), wStmts, wStmtsAfterCall);
} else {
throw new InvalidOperationException("Cannot call statement in this context: " + currentBuilder);
}
}
protected override void EmitMultiReturnTuple(List<Formal> outs, List<Type> outTypes, List<string> outTmps, IToken methodToken, ConcreteSyntaxTree wr) {
// nothing to do, we auto-emit a return for the method
}
protected override void CompileFunctionCallExpr(FunctionCallExpr e, ConcreteSyntaxTree wr, bool inLetExprBody,
ConcreteSyntaxTree wStmts, FCE_Arg_Translator tr, bool alreadyCoerced) {
var toType = thisContext == null ? e.Type : e.Type.Subst(thisContext.ParentFormalTypeParametersToActuals);
wr = EmitCoercionIfNecessary(e.Function.Original.ResultType, toType, e.tok, wr);
if (wr is BuilderSyntaxTree<ExprContainer> builder) {
var callBuilder = builder.Builder.Call();
base.CompileFunctionCallExpr(e, new BuilderSyntaxTree<ExprContainer>(callBuilder), inLetExprBody, wStmts, tr, true);
} else {
throw new InvalidOperationException("Cannot call function in this context: " + currentBuilder);
}
}
protected override void EmitActualTypeArgs(List<Type> typeArgs, IToken tok, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<ExprContainer> st && st.Builder is CallExprBuilder callExpr) {
callExpr.SetTypeArgs(typeArgs.Select(GenType).ToList());
} else if (wr is BuilderSyntaxTree<ExprContainer> st2 && st2.Builder is CallStmtBuilder callStmt) {
callStmt.SetTypeArgs(typeArgs.Select(GenType).ToList());
} else {
throw new InvalidOperationException("Cannot emit actual type args in this context: " + currentBuilder);
}
}
private class BuilderLvalue : ILvalue {
readonly string name;
public BuilderLvalue(string name) {
this.name = name;
}
public void EmitRead(ConcreteSyntaxTree wr) {
throw new InvalidOperationException();
}
public ConcreteSyntaxTree EmitWrite(ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
var assign = stmtContainer.Builder.Assign();
assign.AddLhs((DAST.AssignLhs)DAST.AssignLhs.create_Ident(Sequence<Rune>.UnicodeFromString(name)));
return new BuilderSyntaxTree<ExprContainer>(assign);
} else {
throw new InvalidOperationException();
}
}
}
private class ExprLvalue : ILvalue {
readonly DAST.Expression expr;
readonly DAST.AssignLhs assignExpr;
public ExprLvalue(DAST.Expression expr, DAST.AssignLhs assignExpr) {
this.expr = expr;
this.assignExpr = assignExpr;
}
public void EmitRead(ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<ExprContainer> exprContainer) {
exprContainer.Builder.AddExpr(expr);
} else {
throw new InvalidOperationException();
}
}
public ConcreteSyntaxTree EmitWrite(ConcreteSyntaxTree wr) {
if (assignExpr == null) {
throw new InvalidOperationException();
}
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
var assign = stmtContainer.Builder.Assign();
assign.AddLhs(assignExpr);
return new BuilderSyntaxTree<ExprContainer>(assign);
} else {
throw new InvalidOperationException();
}
}
}
protected override void EmitAssignment(string lhs, Type/*?*/ lhsType, string rhs, Type/*?*/ rhsType, ConcreteSyntaxTree wr) {
throw new InvalidOperationException("Cannot use stringified version of assignment");
}
protected override ILvalue IdentLvalue(string var) {
return new BuilderLvalue(var);
}
protected override ILvalue SeqSelectLvalue(SeqSelectExpr ll, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
var sourceBuf = new ExprBuffer(null);
EmitExpr(
ll.Seq, false,
EmitCoercionIfNecessary(
ll.Seq.Type,
ll.Seq.Type.IsNonNullRefType || !ll.Seq.Type.IsRefType ? null : UserDefinedType.CreateNonNullType((UserDefinedType)ll.Seq.Type.NormalizeExpand()),
null, new BuilderSyntaxTree<ExprContainer>(sourceBuf)
),
wStmts
);
var indexBuf = new ExprBuffer(null);
EmitExpr(ll.E0, false, new BuilderSyntaxTree<ExprContainer>(indexBuf), wStmts);
var source = sourceBuf.Finish();
var index = indexBuf.Finish();
DAST._ICollKind collKind;
if (ll.Seq.Type.IsArrayType) {
collKind = DAST.CollKind.create_Array();
} else if (ll.Seq.Type.IsMapType) {
collKind = DAST.CollKind.create_Map();
} else {
collKind = DAST.CollKind.create_Seq();
}
return new ExprLvalue(
(DAST.Expression)DAST.Expression.create_Index(source, collKind, Sequence<DAST.Expression>.FromElements(index)),
(DAST.AssignLhs)DAST.AssignLhs.create_Index(source, Sequence<DAST.Expression>.FromElements(index))
);
}
protected override ILvalue MultiSelectLvalue(MultiSelectExpr ll, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
throwGeneralUnsupported();
throw new InvalidOperationException();
}
protected override void EmitPrintStmt(ConcreteSyntaxTree wr, Expression arg) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
ExprBuffer buffer = new(null);
EmitExpr(arg, false, new BuilderSyntaxTree<ExprContainer>(buffer), wr);
stmtContainer.Builder.Print(buffer.Finish());
} else {
throw new InvalidOperationException("Cannot print outside of a statement container: " + currentBuilder);
}
}
protected override void EmitReturn(List<Formal> outParams, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_EarlyReturn());
} else {
throw new InvalidOperationException("Cannot return outside of a statement container: " + currentBuilder);
}
}
protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
var labelBuilder = stmtContainer.Builder.Labeled((createContinueLabel ? "continue_" : "goto_") + label);
return new BuilderSyntaxTree<StatementContainer>(labelBuilder);
} else {
throw new InvalidOperationException();
}
}
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))
));
} else {
throw new InvalidOperationException();
}
}
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))
));
} else {
throw new InvalidOperationException();
}
}
protected override void EmitYield(ConcreteSyntaxTree wr) {
throw new UnsupportedFeatureException(Token.NoToken, Feature.Iterators);
}
protected override void EmitAbsurd(string message, ConcreteSyntaxTree wr) {
// TODO(shadaj): emit correct message
if (wr is BuilderSyntaxTree<StatementContainer> container) {
container.Builder.AddStatement((DAST.Statement)DAST.Statement.create_Halt());
} else {
throw new InvalidOperationException();
}
}
protected override void EmitHalt(IToken tok, Expression messageExpr, ConcreteSyntaxTree wr) {
if (wr is BuilderSyntaxTree<StatementContainer> container) {
container.Builder.AddStatement((DAST.Statement)DAST.Statement.create_Halt());
} else {
throw new InvalidOperationException();
}
}
private readonly Stack<(ElseBuilder, StatementContainer)> elseBuilderStack = new();