forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Compiler-js.cs
2565 lines (2376 loc) · 104 KB
/
Compiler-js.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
//-----------------------------------------------------------------------------
//
// Copyright by the contributors to the Dafny Project
// SPDX-License-Identifier: MIT
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Linq;
using System.Numerics;
using System.IO;
using System.Diagnostics.Contracts;
using System.Collections.ObjectModel;
using System.Diagnostics;
using System.Text;
using System.Threading.Tasks;
using JetBrains.Annotations;
namespace Microsoft.Dafny.Compilers {
class JavaScriptCompiler : SinglePassCompiler {
public JavaScriptCompiler(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
}
public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
Feature.MethodSynthesis,
Feature.ExternalConstructors,
Feature.SubsetTypeTests,
Feature.SeparateCompilation,
Feature.RuntimeCoverageReport
};
public override string ModuleSeparator => "_";
const string DafnySetClass = "_dafny.Set";
const string DafnyMultiSetClass = "_dafny.MultiSet";
const string DafnySeqClass = "_dafny.Seq";
const string DafnyMapClass = "_dafny.Map";
string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
Contract.Requires(tp is TypeParameter || tp is AbstractTypeDecl);
return $"_default_{tp.GetCompileName(Options)}";
}
protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
wr.WriteLine("// Dafny program {0} compiled into JavaScript", program.Name);
if (Options.IncludeRuntime) {
EmitRuntimeSource("DafnyRuntimeJs", wr, false);
}
}
public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
Coverage.EmitSetup(wr);
wr.WriteLine($"_dafny.HandleHaltExceptions(() => {mainMethod.EnclosingClass.GetFullCompileName(Options)}.{(mainMethod.IsStatic ? IdName(mainMethod) : "Main")}(_dafny.{CharMethodQualifier}FromMainArguments(require('process').argv)));");
Coverage.EmitTearDown(wr);
}
protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) {
var wr = (cw as JavaScriptCompiler.ClassWriter).MethodWriter;
return wr.NewBlock($"static Main({argsParameterName})");
}
protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName /*?*/, ConcreteSyntaxTree wr) {
moduleName = IdProtect(moduleName);
if (externModule == null || libraryName != null) {
wr.Write("let {0} = ", moduleName);
}
string footer = ")(); // end of module " + moduleName;
var block = wr.NewBlock("(function()", footer);
var beforeReturnBody = block.Fork(0);
if (externModule == null) {
// create new module here
beforeReturnBody.WriteLine("let $module = {};");
} else if (libraryName == null) {
// extend a module provided in another .js file
beforeReturnBody.WriteLine("let $module = {0};", moduleName);
} else {
// require a library
beforeReturnBody.WriteLine("let $module = require(\"{0}\");", libraryName);
}
block.WriteLine("return $module;");
return beforeReturnBody;
}
protected override string GetHelperModuleName() => "_dafny";
protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName,
List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IToken tok, ConcreteSyntaxTree wr) {
var w = wr.NewBlock(string.Format("$module.{0} = class {0}" + (isExtern ? " extends $module.{0}" : ""), name), ";");
w.Write("constructor (");
var sep = "";
if (typeParameters != null && WriteRuntimeTypeDescriptorsFormals(typeParameters, false, w) > 0) {
sep = ", ";
}
if (cls is NewtypeDecl { ParentTraits: { } parentTraits } && parentTraits.Count > 0) {
w.Write($"{sep}value");
}
var fieldWriter = w.NewBlock(")");
if (isExtern) {
fieldWriter.Write("super(");
if (typeParameters != null) {
WriteRuntimeTypeDescriptorsFormals(typeParameters, false, w);
}
fieldWriter.WriteLine(");");
}
if (fullPrintName != null) {
fieldWriter.WriteLine("this._tname = \"{0}\";", fullPrintName);
}
if (typeParameters != null) {
foreach (var tp in typeParameters) {
if (NeedsTypeDescriptor(tp)) {
fieldWriter.WriteLine("this.{0} = {0};", "rtd$_" + tp.GetCompileName(Options));
}
}
}
if (superClasses != null) {
superClasses = superClasses.Where(trait => !trait.IsObject).ToList();
var parentTraitsWriter = w.NewBlock("_parentTraits()");
parentTraitsWriter.WriteLine("return [{0}];", Util.Comma(superClasses, parent => TypeName(parent, parentTraitsWriter, tok)));
}
var methodWriter = w;
return new ClassWriter(this, methodWriter, fieldWriter);
}
protected override IClassWriter CreateTrait(string name, bool isExtern, List<TypeParameter> typeParameters /*?*/,
TraitDecl trait, List<Type> superClasses /*?*/, IToken tok, ConcreteSyntaxTree wr) {
var w = wr.NewBlock(string.Format("$module.{0} = class {0}", IdProtect(name)), ";");
var fieldWriter = w; // not used for traits, but we need a value to give to the ClassWriter
var methodWriter = w;
return new ClassWriter(this, methodWriter, fieldWriter);
}
protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, ConcreteSyntaxTree wr) {
// An iterator is compiled as follows:
// public class MyIteratorExample
// {
// public T q; // in-parameter
// public T x; // yield-parameter
// public int y; // yield-parameter
// IEnumerator<object> _iter;
//
// public void _MyIteratorExample(T q) {
// this.q = q;
// _iter = TheIterator();
// }
//
// public void MoveNext(out bool more) {
// more =_iter.MoveNext();
// }
//
// private IEnumerator<object> TheIterator() {
// // the translation of the body of the iterator, with each "yield" turning into a "yield return null;"
// yield break;
// }
// }
var cw = CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), IdName(iter), iter, wr) as JavaScriptCompiler.ClassWriter;
var w = cw.MethodWriter;
var instanceFieldsWriter = cw.FieldWriter;
// here come the fields
Constructor ct = null;
foreach (var member in iter.Members) {
var f = member as Field;
if (f != null && !f.IsGhost) {
DeclareField(IdName(f), false, false, f.Type, f.tok, PlaceboValue(f.Type, instanceFieldsWriter, f.tok, true), instanceFieldsWriter);
} else if (member is Constructor) {
Contract.Assert(ct == null); // we're expecting just one constructor
ct = (Constructor)member;
}
}
Contract.Assert(ct != null); // we do expect a constructor
instanceFieldsWriter.WriteLine("this._iter = undefined;");
// here's the initializer method
w.Write("{0}(", IdName(ct));
string sep = "";
foreach (var p in ct.Ins) {
if (!p.IsGhost) {
// here we rely on the parameters and the corresponding fields having the same names
w.Write("{0}{1}", sep, IdName(p));
sep = ", ";
}
}
{
var wBody = w.NewBlock(")");
foreach (var p in ct.Ins) {
if (!p.IsGhost) {
wBody.WriteLine("this.{0} = {0};", IdName(p));
}
}
wBody.WriteLine("this.__iter = this.TheIterator();");
}
// here are the enumerator methods
{
var wBody = w.NewBlock("MoveNext()");
wBody.WriteLine("let r = this.__iter.next();");
wBody.WriteLine("return !r.done;");
}
var wIter = w.NewBlock("*TheIterator()");
wIter.WriteLine("let _this = this;");
return wIter;
}
protected override IClassWriter/*?*/ DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxTree wr) {
// ===== For inductive datatypes:
//
// $module.Dt = class Dt {
// constructor(tag) {
// this.$tag = tag;
// }
// static create_Ctor0(field0, field1, ...) {
// let $dt = new Dt(0);
// $dt.field0 = field0;
// $dt.field1 = field1;
// ...
// return $dt;
// }
// static create_Ctor1(...) {
// let $dt = new Dt(1);
// ...
// }
// ...
//
// get is_Ctor0 { return this.$tag === 0; }
// get is_Ctor1 { return this.$tag === 1; }
// ...
//
// static get AllSingletonConstructors() {
// return this.AllSingletonConstructors_();
// }
// static *AllSingletonConstructors_() {
// yield Berry.create_Ctor0();
// ...
// }
//
// get dtor_Dtor0() { return this.Dtor0; }
// get dtor_Dtor1() { return this.Dtor1; }
// ...
//
// toString() {
// ...
// }
// equals(other) {
// ...
// }
// static Rtd(rtd...) {
// return class {
// static get Default() { return Dt.create_CtorK(...); }
// };
// }
// }
//
// ===== For co-inductive datatypes:
//
// $module.Dt = class Dt {
// constructor(tag) {
// this.$tag = tag;
// }
// _D() {
// if (this._d === undefined) {
// this._d = this._initializer(this);
// delete this._initializer;
// }
// return this._d;
// }
// static create_Ctor0($dt, field0, field1, ...) {
// if ($dt === null) {
// $dt = new Dt(0);
// $dt._d = $dt;
// }
// $dt.field0 = field0;
// $dt.field1 = field1;
// ...
// return $dt;
// }
// static lazy_Ctor0(initializer) {
// let dt = new Dt(0);
// dt._initializer = initializer;
// return dt;
// }
// static create_Ctor1(initializer) {
// let $dt = new Dt(1);
// ...
// }
// ...
//
// get is_Ctor0() { return this.$tag === 0; }
// get is_Ctor1() { return this.$tag === 1; }
// ...
//
// static get AllSingletonConstructors() {
// return this.AllSingletonConstructors_();
// }
// static *AllSingletonConstructors_() {
// yield Berry.create_Ctor0(null);
// ...
// }
//
// get dtor_Dtor0() { return this._D().Dtor0; }
// get dtor_Dtor1() { return this._D().Dtor1; }
// ...
//
// toString() {
// if ($tag == 0) {
// return "module.Dt.Ctor0";
// } else if ...
// }
// equals(other) {
// ...
// }
// static Rtd(rtd...) {
// return class {
// static get Default() { return Dt.create_CtorK(...); }
// };
// }
// }
if (dt is TupleTypeDecl) {
// Tuple types are declared once and for all in DafnyRuntime.js
return null;
}
string DtT = dt.GetCompileName(Options);
string DtT_protected = IdProtect(DtT);
var simplifiedType = DatatypeWrapperEraser.SimplifyType(Options, UserDefinedType.FromTopLevelDecl(dt.tok, dt));
// from here on, write everything into the new block created here:
var btw = wr.NewNamedBlock("$module.{0} = class {0}", DtT_protected);
wr = btw;
var wTypeDescriptors = new ConcreteSyntaxTree();
var typeDescriptorComma = WriteRuntimeTypeDescriptorsFormals(dt.TypeArgs, false, wTypeDescriptors) != 0 ? ", " : "";
var typeDescriptors = wTypeDescriptors.ToString();
var wBody = wr.NewBlock($"constructor(tag{typeDescriptorComma}{typeDescriptors})");
wBody.WriteLine("this.$tag = tag;");
foreach (var tp in dt.TypeArgs.Where(NeedsTypeDescriptor)) {
wBody.WriteLine("this.{0} = {0};", "rtd$_" + tp.GetCompileName(Options));
}
if (dt is CoDatatypeDecl) {
var w0 = wr.NewBlock("_D()");
var w1 = EmitIf("this._d === undefined", false, w0);
w1.WriteLine("this._d = this._initializer(this);");
w1.WriteLine("delete this._initializer;");
w0.WriteLine("return this._d");
}
// create methods
var i = 0;
foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) {
// collect the names of non-ghost arguments
var argNames = new List<string>();
var k = 0;
foreach (var formal in ctor.Formals) {
if (!formal.IsGhost) {
argNames.Add(FormalName(formal, k));
k++;
}
}
// datatype:
// static create_Ctor0(params) { let $dt = new Dt(tag); $dt.param0 = param0; ...; return $dt; }
// codatatype:
// static create_Ctor0(params) { if ($dt === null) { $dt = new Dt(tag); $dt._d = $dt; } $dt.param0 = param0; ...; return $dt; }
// static lazy_Ctor0(initializer) { let dt = new Dt(tag); dt._initializer = initializer; return dt; }
wr.Write($"static create_{ctor.GetCompileName(Options)}(");
wr.Write(typeDescriptors);
var sep = typeDescriptorComma;
if (dt is CoDatatypeDecl) {
wr.Write($"{sep}$dt");
sep = ", ";
}
if (argNames.Count != 0) {
wr.Write(sep);
}
wr.Write(Util.Comma(argNames, nm => nm));
var w = wr.NewBlock(")");
if (dt is CoDatatypeDecl) {
var wThen = EmitIf("$dt === null", false, w);
wThen.WriteLine($"$dt = new {DtT_protected}({i}{typeDescriptorComma}{typeDescriptors});");
wThen.WriteLine("$dt._d = $dt;");
} else {
w.WriteLine($"let $dt = new {DtT_protected}({i}{typeDescriptorComma}{typeDescriptors});");
}
foreach (var arg in argNames) {
w.WriteLine("$dt.{0} = {0};", arg);
}
w.WriteLine("return $dt;");
if (dt is CoDatatypeDecl) {
wBody = wr.NewNamedBlock("static lazy_{0}(initializer)", ctor.GetCompileName(Options));
wBody.WriteLine("let dt = new {0}({1});", DtT_protected, i);
wBody.WriteLine("dt._initializer = initializer;");
wBody.WriteLine("return dt;");
}
i++;
}
// query properties
i = 0;
foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) {
// get is_Ctor0() { return _D is Dt_Ctor0; }
wr.WriteLine("get is_{0}() {{ return this.$tag === {1}; }}", ctor.GetCompileName(Options), i);
i++;
}
if (dt.HasFinitePossibleValues) {
Contract.Assert(dt.TypeArgs.Count == 0);
{
var w = wr.NewNamedBlock("static get AllSingletonConstructors()");
w.WriteLine("return this.AllSingletonConstructors_();");
}
{
var w = wr.NewNamedBlock("static *AllSingletonConstructors_()");
foreach (var ctor in dt.Ctors) {
Contract.Assert(ctor.Formals.Count == 0);
if (ctor.IsGhost) {
w.WriteLine("yield {0};", ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), w, dt.tok));
} else {
w.WriteLine("yield {0}.create_{1}({2});", DtT_protected, ctor.GetCompileName(Options), dt is CoDatatypeDecl ? "null" : "");
}
}
}
}
// destructors
foreach (var ctor in dt.Ctors) {
foreach (var dtor in ctor.Destructors.Where(dtor => dtor.EnclosingCtors[0] == ctor)) {
var compiledConstructorCount = dtor.EnclosingCtors.Count(constructor => !constructor.IsGhost);
if (compiledConstructorCount != 0) {
var arg = dtor.CorrespondingFormals[0];
if (!arg.IsGhost && arg.HasName) {
// datatype: get dtor_Dtor0() { return this.Dtor0; }
// codatatype: get dtor_Dtor0() { return this._D().Dtor0; }
wr.WriteLine("get dtor_{0}() {{ return this{2}.{1}; }}", arg.CompileName, IdName(arg), dt is CoDatatypeDecl ? "._D()" : "");
}
}
}
}
if (dt is CoDatatypeDecl) {
// toString method
var w = wr.NewBlock("toString()");
i = 0;
foreach (var ctor in dt.Ctors) {
var thn = EmitIf(string.Format("this.$tag === {0}", i), true, w);
var nm = (dt.EnclosingModuleDefinition.TryToAvoidName ? "" : dt.EnclosingModuleDefinition.Name + ".") +
dt.Name + "." + ctor.Name;
thn.WriteLine("return \"{0}\";", nm);
i++;
}
var els = w.NewBlock("");
els.WriteLine("return \"{0}.{1}.unexpected\";", dt.EnclosingModuleDefinition.GetCompileName(Options), DtT);
} else if (dt is IndDatatypeDecl) {
// toString method
var w = wr.NewBlock("toString()");
i = 0;
foreach (var ctor in dt.Ctors) {
var cw = EmitIf(string.Format("this.$tag === {0}", i), true, w);
var nm = (dt.EnclosingModuleDefinition.TryToAvoidName ? "" : dt.EnclosingModuleDefinition.Name + ".") +
dt.Name + "." + ctor.Name;
cw.Write("return \"{0}\"", nm);
var sep = " + \"(\" + ";
var anyFormals = false;
var k = 0;
foreach (var arg in ctor.Formals) {
if (!arg.IsGhost) {
anyFormals = true;
if (arg.Type.IsStringType && UnicodeCharEnabled) {
cw.Write("{0}this.{1}.toVerbatimString(true)", sep, FormalName(arg, k));
} else {
cw.Write("{0}_dafny.toString(this.{1})", sep, FormalName(arg, k));
}
sep = " + \", \" + ";
k++;
}
}
if (anyFormals) {
cw.Write(" + \")\"");
}
cw.WriteLine(";");
i++;
}
var wElse = w.NewBlock("");
wElse.WriteLine("return \"<unexpected>\";");
}
// equals method
{
var w = wr.NewBlock("equals(other)");
{
var thn = EmitIf("this === other", true, w);
EmitReturnExpr("true", thn);
}
i = 0;
foreach (var ctor in dt.Ctors) {
var thn = EmitIf(string.Format("this.$tag === {0}", i), true, w);
var guard = EmitReturnExpr(thn);
guard.Write("other.$tag === {0}", i);
var k = 0;
foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
string nm = FormalName(arg, k);
if (IsDirectlyComparable(DatatypeWrapperEraser.SimplifyType(Options, arg.Type))) {
guard.Write(" && this.{0} === other.{0}", nm);
} else {
guard.Write(" && _dafny.areEqual(this.{0}, other.{0})", nm);
}
k++;
}
}
i++;
}
var els = w.NewBlock("");
els.WriteLine("return false; // unexpected");
}
// static Default(defaultValues...) { // where defaultValues are the parameters to the grounding constructor
// return Dt.create_GroundingCtor(defaultValues...);
// }
wr.Write($"static Default(");
var usedTypeParameters = UsedTypeParameters(dt);
if (WriteRuntimeTypeDescriptorsFormals(dt.TypeArgs, false, wr) != 0 && usedTypeParameters.Count != 0) {
wr.Write(", ");
}
wr.Write(usedTypeParameters.Comma(FormatDefaultTypeParameterValue));
{
var wDefault = wr.NewBlock(")");
wDefault.Write("return ");
var groundingCtor = dt.GetGroundingCtor();
if (groundingCtor.IsGhost) {
wDefault.Write(ForcePlaceboValue(simplifiedType, wDefault, dt.tok));
} else if (DatatypeWrapperEraser.GetInnerTypeOfErasableDatatypeWrapper(Options, dt, out var innerType)) {
wDefault.Write(DefaultValue(innerType, wDefault, dt.tok));
} else {
var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList();
var arguments = nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok));
EmitDatatypeValue(dt, groundingCtor, dt is CoDatatypeDecl, typeDescriptors, arguments, wDefault);
}
wDefault.WriteLine(";");
}
// Note: It is important that the following be a class with a static getter Default(), as opposed
// to a simple "{ Default: ... }" object, because we need for any recursive calls in the default
// expression to be evaluated lazily. (More precisely, not evaluated at all, but that will sort
// itself out due to the restrictions placed by the resolver.)
//
// static Rtd(rtd...) {
// return class {
// static get Default() { return Dt.create_CtorK(...); }
// };
// }
wr.Write("static Rtd(");
WriteRuntimeTypeDescriptorsFormals(UsedTypeParameters(dt, true), true, wr);
var wRtd = wr.NewBlock(")");
var wClass = wRtd.NewBlock("return class", ";");
{
var wDefault = wClass.NewBlock("static get Default()");
var sep = typeDescriptors.Length != 0 && usedTypeParameters.Count != 0 ? ", " : "";
var arguments = usedTypeParameters.Comma(
tp => DefaultValue(new UserDefinedType(tp), wDefault, dt.tok, true));
wDefault.WriteLine($"return {DtT_protected}.Default({typeDescriptors}{typeDescriptorComma}{arguments});");
}
return new ClassWriter(this, btw, btw);
}
protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), IdName(nt), nt, wr);
var w = cw.MethodWriter;
if (nt.NativeType != null) {
var wIntegerRangeBody = w.NewBlock("static *IntegerRange(lo, hi)");
var wLoopBody = wIntegerRangeBody.NewBlock("while (lo.isLessThan(hi))");
wLoopBody.WriteLine("yield lo.toNumber();");
EmitIncrementVar("lo", wLoopBody);
}
if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel);
var wStmts = w.Fork();
if (nt.NativeType == null) {
witness.Append(Expr(nt.Witness, false, wStmts));
} else {
TrParenExpr(nt.Witness, witness, false, wStmts);
witness.Write(".toNumber()");
}
DeclareField("Witness", true, true, nt.BaseType, nt.tok, witness.ToString(), w);
}
// In JavaScript, the companion class of a newtype (which is what is being declared here) doubles as a
// type descriptor for the newtype. The Default() method for that type descriptor is declared here.
var wDefault = w.NewBlock("static get Default()");
var udt = new UserDefinedType(nt.tok, nt.Name, nt, new List<Type>());
var d = TypeInitializationValue(udt, wr, nt.tok, false, false);
wDefault.WriteLine("return {0};", d);
if (nt.ParentTraits.Count != 0) {
// in constructor:
// this._value = value;
cw.FieldWriter.WriteLine("this._value = value;");
// toString() {
// return _dafny.toString(this._value)
// }
var wBody = cw.MethodWriter.NewNamedBlock("toString()");
wBody.WriteLine("return _dafny.toString(this._value)");
}
return cw;
}
protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) {
var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), IdName(sst), sst, wr);
var w = cw.MethodWriter;
var udt = UserDefinedType.FromTopLevelDecl(sst.tok, sst);
string d;
if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var sw = new ConcreteSyntaxTree(w.RelativeIndentLevel);
var wStmts = w.Fork();
sw.Append(Expr(sst.Witness, false, wStmts));
DeclareField("Witness", true, true, sst.Rhs, sst.tok, sw.ToString(), w);
d = TypeName_UDT(FullTypeName(udt), udt, wr, udt.tok) + ".Witness";
} else {
d = TypeInitializationValue(udt, wr, sst.tok, false, false);
}
w.NewBlock("static get Default()").WriteLine($"return {d};");
}
protected override void GetNativeInfo(NativeType.Selection sel, out string name, out string literalSuffix, out bool needsCastAfterArithmetic) {
literalSuffix = "";
needsCastAfterArithmetic = false;
switch (sel) {
case NativeType.Selection.Number:
name = "number";
break;
default:
Contract.Assert(false); // unexpected native type
throw new cce.UnreachableException(); // to please the compiler
}
}
protected class ClassWriter : IClassWriter {
public readonly JavaScriptCompiler Compiler;
public readonly ConcreteSyntaxTree MethodWriter;
public readonly ConcreteSyntaxTree FieldWriter;
public ClassWriter(JavaScriptCompiler compiler, ConcreteSyntaxTree methodWriter, ConcreteSyntaxTree fieldWriter) {
Contract.Requires(compiler != null);
Contract.Requires(methodWriter != null);
Contract.Requires(fieldWriter != null);
this.Compiler = compiler;
this.MethodWriter = methodWriter;
this.FieldWriter = fieldWriter;
}
public ConcreteSyntaxTree/*?*/ CreateMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) {
return Compiler.CreateMethod(m, typeArgs, createBody, MethodWriter, forBodyInheritance, lookasideBody);
}
public ConcreteSyntaxTree SynthesizeMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) {
throw new UnsupportedFeatureException(m.tok, 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) {
return Compiler.CreateFunction(name, typeArgs, formals, resultType, tok, isStatic, createBody, member, MethodWriter, forBodyInheritance, lookasideBody);
}
public ConcreteSyntaxTree/*?*/ CreateGetter(string name, TopLevelDecl enclosingDecl, Type resultType, IToken tok, bool isStatic, bool isConst, bool createBody, MemberDecl/*?*/ member, bool forBodyInheritance) {
return Compiler.CreateGetter(name, resultType, tok, isStatic, createBody, MethodWriter);
}
public ConcreteSyntaxTree/*?*/ CreateGetterSetter(string name, Type resultType, IToken tok, bool createBody, MemberDecl/*?*/ member, out ConcreteSyntaxTree setterWriter, bool forBodyInheritance) {
return Compiler.CreateGetterSetter(name, resultType, tok, createBody, out setterWriter, MethodWriter);
}
public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, bool isConst, Type type, IToken tok, string rhs, Field field) {
Compiler.DeclareField(name, isStatic, isConst, type, tok, rhs, FieldWriter);
}
public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) {
throw new cce.UnreachableException(); // InitializeField should be called only for those compilers that set ClassesRedeclareInheritedFields to false.
}
public ConcreteSyntaxTree/*?*/ ErrorWriter() => MethodWriter;
public void Finish() { }
}
protected override bool SupportsStaticsInGenericClasses => false;
protected ConcreteSyntaxTree/*?*/ CreateMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, ConcreteSyntaxTree wr, bool forBodyInheritance, bool lookasideBody) {
if (!createBody) {
return null;
}
var customReceiver = !forBodyInheritance && NeedsCustomReceiver(m);
wr.Write("{0}{1}(", m.IsStatic || customReceiver ? "static " : "", IdName(m));
var sep = "";
WriteRuntimeTypeDescriptorsFormals(ForTypeDescriptors(typeArgs, m.EnclosingClass, m, lookasideBody), wr, ref sep, tp => $"rtd$_{tp.GetCompileName(Options)}");
if (customReceiver) {
var nt = m.EnclosingClass;
var receiverType = UserDefinedType.FromTopLevelDecl(m.tok, nt);
DeclareFormal(sep, "_this", receiverType, m.tok, true, wr);
sep = ", ";
}
WriteFormals(sep, m.Ins, wr);
var w = wr.NewBlock(")");
if (!m.IsStatic && !customReceiver) {
w.WriteLine("let _this = this;");
}
return w;
}
protected override ConcreteSyntaxTree EmitMethodReturns(Method m, ConcreteSyntaxTree wr) {
var beforeReturnBlock = wr.Fork(0);
EmitReturn(m.Outs, wr);
return beforeReturnBlock;
}
protected ConcreteSyntaxTree/*?*/ CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member, ConcreteSyntaxTree wr, bool forBodyInheritance, bool lookasideBody) {
if (!createBody) {
return null;
}
var customReceiver = !forBodyInheritance && NeedsCustomReceiver(member);
wr.Write("{0}{1}(", isStatic || customReceiver ? "static " : "", name);
var sep = "";
WriteRuntimeTypeDescriptorsFormals(ForTypeDescriptors(typeArgs, member.EnclosingClass, member, lookasideBody), wr, ref sep,
tp => $"rtd$_{tp.GetCompileName(Options)}");
if (customReceiver) {
var nt = member.EnclosingClass;
var receiverType = UserDefinedType.FromTopLevelDecl(tok, nt);
DeclareFormal(sep, "_this", receiverType, tok, true, wr);
sep = ", ";
}
WriteFormals(sep, formals, wr);
var w = wr.NewBlock(")", ";");
if (!isStatic && !customReceiver) {
w.WriteLine("let _this = this;");
}
return w;
}
int WriteRuntimeTypeDescriptorsFormals(List<TypeParameter> typeParams, bool useAllTypeArgs, ConcreteSyntaxTree wr, string prefix = "") {
Contract.Requires(typeParams != null);
Contract.Requires(wr != null);
int c = 0;
foreach (var tp in typeParams) {
if (useAllTypeArgs || NeedsTypeDescriptor(tp)) {
wr.Write($"{prefix}rtd$_{tp.GetCompileName(Options)}");
prefix = ", ";
c++;
}
}
return c;
}
protected override void TypeArgDescriptorUse(bool isStatic, bool lookasideBody, TopLevelDeclWithMembers cl, out bool needsTypeParameter, out bool needsTypeDescriptor) {
if (cl is DatatypeDecl) {
needsTypeParameter = false;
needsTypeDescriptor = true;
} else if (cl is TraitDecl) {
needsTypeParameter = false;
needsTypeDescriptor = isStatic || lookasideBody;
} else {
Contract.Assert(cl is ClassDecl);
needsTypeParameter = false;
needsTypeDescriptor = isStatic;
}
}
protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToken tok) {
Contract.Requires(type != null);
Contract.Requires(tok != null);
Contract.Requires(wr != null);
var xType = DatatypeWrapperEraser.SimplifyType(Options, type, true);
if (xType is BoolType) {
return "_dafny.Rtd_bool";
} else if (xType is CharType) {
return UnicodeCharEnabled ? "_dafny.Rtd_codepoint" : "_dafny.Rtd_char";
} else if (xType is IntType) {
return "_dafny.Rtd_int";
} else if (xType is BigOrdinalType) {
return "_dafny.BigOrdinal";
} else if (xType is RealType) {
return "_dafny.BigRational";
} else if (xType is BitvectorType) {
var t = (BitvectorType)xType;
if (t.NativeType != null) {
return "_dafny.Rtd_number";
} else {
return "_dafny.Rtd_int";
}
} else if (xType is SetType) {
return DafnySetClass;
} else if (xType is MultiSetType) {
return DafnyMultiSetClass;
} else if (xType is SeqType) {
return DafnySeqClass;
} else if (xType is MapType) {
return DafnyMapClass;
} else if (xType.IsBuiltinArrowType) {
return "_dafny.Rtd_ref"; // null suffices as a default value, since the function will never be called
} else if (xType is UserDefinedType) {
var udt = (UserDefinedType)xType;
if (udt.ResolvedClass is TypeParameter tp) {
var receiver = thisContext != null && tp.Parent is TopLevelDeclWithMembers and not TraitDecl ? "this." : "";
return string.Format($"{receiver}rtd$_{tp.GetCompileName(Options)}");
}
var cl = udt.ResolvedClass;
Contract.Assert(cl != null);
if (cl is ClassLikeDecl) {
return "_dafny.Rtd_ref";
} else if (cl is DatatypeDecl) {
var dt = (DatatypeDecl)cl;
var w = new ConcreteSyntaxTree();
w.Write("{0}.Rtd(", dt is TupleTypeDecl ? "_dafny.Tuple" : FullTypeName(udt));
EmitTypeDescriptorsActuals(UsedTypeParameters(dt, udt.TypeArgs, true), udt.tok, w, true);
w.Write(")");
return w.ToString();
} else if (xType.IsNonNullRefType) {
// what we emit here will only be used to construct a dummy value that programmer-supplied code will overwrite later
return "_dafny.Rtd_ref/*not used*/";
} else {
Contract.Assert(cl is NewtypeDecl || cl is SubsetTypeDecl);
return TypeName_UDT(FullTypeName(udt), udt, wr, udt.tok);
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
protected ConcreteSyntaxTree/*?*/ CreateGetter(string name, Type resultType, IToken tok, bool isStatic, bool createBody, ConcreteSyntaxTree wr) {
if (createBody) {
wr.Write("{0}get {1}()", isStatic ? "static " : "", name);
var w = wr.NewBlock("", ";");
if (!isStatic) {
w.WriteLine("let _this = this;");
}
return w;
} else {
return null;
}
}
protected ConcreteSyntaxTree/*?*/ CreateGetterSetter(string name, Type resultType, IToken tok, bool createBody, out ConcreteSyntaxTree setterWriter, ConcreteSyntaxTree wr) {
if (createBody) {
wr.Write($"get {name}()");
var wGet = wr.NewBlock("", ";");
wGet.WriteLine("let _this = this;");
wr.Write($"set {name}(value)");
var wSet = wr.NewBlock("", ";");
wSet.WriteLine("let _this = this;");
setterWriter = wSet;
return wGet;
} else {
setterWriter = null;
return null;
}
}
protected override ConcreteSyntaxTree EmitTailCallStructure(MemberDecl member, ConcreteSyntaxTree wr) {
var block = wr.NewBlock("TAIL_CALL_START: while (true)");
if (member is Method m) {
var beforeReturnBlock = block.Fork(0);
EmitReturn(m.Outs, block);
return beforeReturnBlock;
}
return block;
}
protected override void EmitJumpToTailCallStart(ConcreteSyntaxTree wr) {
wr.WriteLine("continue TAIL_CALL_START;");
}
private string CharFromNumberMethodName() {
return UnicodeCharEnabled ? "new _dafny.CodePoint" : "String.fromCharCode";
}
internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl /*?*/ member = null) {
Contract.Ensures(Contract.Result<string>() != null);
Contract.Assume(type != null); // precondition; this ought to be declared as a Requires in the superclass
var xType = DatatypeWrapperEraser.SimplifyType(Options, type);
if (xType is BoolType) {
return "bool";
} else if (xType is CharType) {
return "char";
} else if (xType is IntType || xType is BigOrdinalType) {
return "BigNumber";
} else if (xType is RealType) {
return "Dafny.BigRational";
} else if (xType is BitvectorType) {
var t = (BitvectorType)xType;
return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "BigNumber";
} else if (xType.AsNewtype != null && member == null) { // when member is given, use UserDefinedType case below
NativeType nativeType = xType.AsNewtype.NativeType;
if (nativeType != null) {
return GetNativeTypeName(nativeType);
}
return TypeName(xType.AsNewtype.BaseType, wr, tok);
} else if (xType.IsObjectQ) {
return "object";
} else if (xType.IsArrayType) {
return "Array";
} else if (xType is UserDefinedType udt) {
var s = FullTypeName(udt, member);
return TypeName_UDT(s, udt, wr, udt.tok);
} else if (xType is SetType) {
Type argType = ((SetType)xType).Arg;
return DafnySetClass;
} else if (xType is SeqType) {
Type argType = ((SeqType)xType).Arg;
return DafnySeqClass;
} else if (xType is MultiSetType) {
Type argType = ((MultiSetType)xType).Arg;
return DafnyMultiSetClass;
} else if (xType is MapType) {
return DafnyMapClass;
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok, bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) {
if (usePlaceboValue) {
return "undefined";
}
var xType = type.NormalizeExpandKeepConstraints();
if (xType is BoolType) {
return "false";
} else if (xType is CharType) {
return $"{CharFromNumberMethodName()}({CharType.DefaultValueAsString}.codePointAt(0))";
} else if (xType is IntType || xType is BigOrdinalType) {
return IntegerLiteral(0);
} else if (xType is RealType) {
return "_dafny.BigRational.ZERO";
} else if (xType is BitvectorType) {
var t = (BitvectorType)xType;
return t.NativeType != null ? "0" : IntegerLiteral(0);
} else if (xType is SetType) {
return $"{DafnySetClass}.Empty";
} else if (xType is MultiSetType) {
return $"{DafnyMultiSetClass}.Empty";
} else if (xType is SeqType seq) {
if (seq.Arg.IsCharType) {
return "''";
}
return $"{DafnySeqClass}.of()";
} else if (xType is MapType) {
return $"{DafnyMapClass}.Empty";
}
var udt = (UserDefinedType)xType;
var cl = udt.ResolvedClass;
Contract.Assert(cl != null);
if (cl is TypeParameter) {
if (constructTypeParameterDefaultsFromTypeDescriptors) {
return string.Format("{0}.Default", TypeDescriptor(udt, wr, udt.tok));
} else {
return FormatDefaultTypeParameterValue((TypeParameter)udt.ResolvedClass);
}
} else if (cl is AbstractTypeDecl opaque) {
return FormatDefaultTypeParameterValue(opaque);
} else if (cl is NewtypeDecl) {
var td = (NewtypeDecl)cl;
if (td.Witness != null) {
return TypeName_UDT(FullTypeName(udt), udt, wr, udt.tok) + ".Witness";
} else if (td.NativeType != null) {
return "0";
} else {
return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
}
} else if (cl is SubsetTypeDecl) {
var td = (SubsetTypeDecl)cl;
if (td.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
return TypeName_UDT(FullTypeName(udt), udt, wr, udt.tok) + ".Default";
} else if (td.WitnessKind == SubsetTypeDecl.WKind.Special) {
// WKind.Special is only used with -->, ->, and non-null types:
Contract.Assert(ArrowType.IsPartialArrowTypeName(td.Name) || ArrowType.IsTotalArrowTypeName(td.Name) || td is NonNullTypeDecl);
if (ArrowType.IsPartialArrowTypeName(td.Name)) {
return "null";
} else if (ArrowType.IsTotalArrowTypeName(td.Name)) {
var rangeDefaultValue = TypeInitializationValue(udt.TypeArgs.Last(), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
// return the lambda expression ((Ty0 x0, Ty1 x1, Ty2 x2) => rangeDefaultValue)
return string.Format("function () {{ return {0}; }}", rangeDefaultValue);
} else if (((NonNullTypeDecl)td).Class is ArrayClassDecl) {
// non-null array type; we know how to initialize them
var arrayClass = (ArrayClassDecl)((NonNullTypeDecl)td).Class;
if (arrayClass.Dims == 1) {
return "[]";
} else {
return string.Format("_dafny.newArray(undefined, {0})", Util.Comma(arrayClass.Dims, _ => "_dafny.ZERO"));
}
} else {
// non-null (non-array) type