From ba1fc5ef91bd0e62af5f444dc74c901b04781427 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 3 Nov 2023 07:07:04 -0700 Subject: [PATCH 1/7] Test passing, massive cleanup still to do --- Source/DafnyDriver/Commands/DafnyCli.cs | 5 +- Source/DafnyPipeline/DafnyPipeline.csproj | 4 + .../DafnyStdLibs/DafnyStdLibs.go | 23 + .../DafnyStdLibs_Functions.go | 17 + .../DafnyStdLibs_Relations.go | 19 + .../DafnyStdLibs_Wrappers.go | 756 ++++++++++++++++++ Source/DafnyRuntime/DafnyRuntimeGo/Makefile | 18 + Source/DafnyRuntime/DafnyRuntimeJava/Makefile | 13 + .../DafnyStdLibs/Wrappers/Option.java | 78 ++ .../DafnyStdLibs/Wrappers/Option_None.java | 33 + .../DafnyStdLibs/Wrappers/Option_Some.java | 39 + .../DafnyStdLibs/Wrappers/Outcome.java | 82 ++ .../DafnyStdLibs/Wrappers/OutcomeResult.java | 38 + .../Wrappers/OutcomeResult_Fail_k.java | 39 + .../Wrappers/OutcomeResult_Pass_k.java | 33 + .../DafnyStdLibs/Wrappers/Outcome_Fail.java | 39 + .../DafnyStdLibs/Wrappers/Outcome_Pass.java | 33 + .../DafnyStdLibs/Wrappers/Result.java | 105 +++ .../DafnyStdLibs/Wrappers/Result_Failure.java | 39 + .../DafnyStdLibs/Wrappers/Result_Success.java | 39 + .../DafnyStdLibs/Wrappers/__default.java | 22 + .../DafnyRuntimeJs/DafnyStandardLibraries.js | 407 ++++++++++ Source/DafnyRuntime/DafnyRuntimeJs/Makefile | 12 + .../DafnyRuntimePython/DafnyStdLibs.py | 14 + .../DafnyStdLibs_Functions.py | 11 + .../DafnyStdLibs_Relations.py | 12 + .../DafnyStdLibs_Wrappers.py | 288 +++++++ .../DafnyRuntime/DafnyRuntimePython/Makefile | 18 + Source/DafnyRuntime/DafnyStandardLibraries.cs | 726 +++++++++++++++++ Source/DafnyRuntime/Makefile | 13 + 30 files changed, 2974 insertions(+), 1 deletion(-) create mode 100644 Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs/DafnyStdLibs.go create mode 100644 Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Functions/DafnyStdLibs_Functions.go create mode 100644 Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Relations/DafnyStdLibs_Relations.go create mode 100644 Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Wrappers/DafnyStdLibs_Wrappers.go create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option_None.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option_Some.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult_Fail_k.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult_Pass_k.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome_Fail.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome_Pass.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result_Failure.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result_Success.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/__default.java create mode 100644 Source/DafnyRuntime/DafnyRuntimeJs/DafnyStandardLibraries.js create mode 100644 Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs.py create mode 100644 Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Functions.py create mode 100644 Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Relations.py create mode 100644 Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Wrappers.py create mode 100644 Source/DafnyRuntime/DafnyStandardLibraries.cs diff --git a/Source/DafnyDriver/Commands/DafnyCli.cs b/Source/DafnyDriver/Commands/DafnyCli.cs index 2bebce6ef28..ca9347556fe 100644 --- a/Source/DafnyDriver/Commands/DafnyCli.cs +++ b/Source/DafnyDriver/Commands/DafnyCli.cs @@ -488,7 +488,10 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, // which is not handled well. if (options.Get(CommonOptionBag.UseStandardLibraries)) { options.CliRootSourceUris.Add(StandardLibrariesDooUri); - dafnyFiles.Add(new DafnyFile(options, StandardLibrariesDooUri)); + var stdlibDooFile = new DafnyFile(options, StandardLibrariesDooUri); + // Precompiled into the runtimes + stdlibDooFile.IsPrecompiled = true; + dafnyFiles.Add(stdlibDooFile); } return ExitValue.SUCCESS; diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj index 5a4a4d8598a..43416965397 100644 --- a/Source/DafnyPipeline/DafnyPipeline.csproj +++ b/Source/DafnyPipeline/DafnyPipeline.csproj @@ -57,6 +57,10 @@ DafnyRuntimeCsharp Always + + DafnyRuntimeCsharp + Always + DafnyRuntimeGo Always diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs/DafnyStdLibs.go b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs/DafnyStdLibs.go new file mode 100644 index 00000000000..3a7e67f6e9e --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs/DafnyStdLibs.go @@ -0,0 +1,23 @@ +// Package DafnyStdLibs +// Dafny module DafnyStdLibs compiled into Go + +package DafnyStdLibs + +import ( + _dafny "dafny" + os "os" + _System "System_" + DafnyStdLibs_Functions "DafnyStdLibs_Functions" + DafnyStdLibs_Relations "DafnyStdLibs_Relations" + DafnyStdLibs_Wrappers "DafnyStdLibs_Wrappers" +) +var _ _dafny.Dummy__ +var _ = os.Args +var _ _System.Dummy__ +var _ DafnyStdLibs_Functions.Dummy__ +var _ DafnyStdLibs_Relations.Dummy__ +var _ DafnyStdLibs_Wrappers.Dummy__ + +type Dummy__ struct{} + + diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Functions/DafnyStdLibs_Functions.go b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Functions/DafnyStdLibs_Functions.go new file mode 100644 index 00000000000..56f632a099e --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Functions/DafnyStdLibs_Functions.go @@ -0,0 +1,17 @@ +// Package DafnyStdLibs_Functions +// Dafny module DafnyStdLibs_Functions compiled into Go + +package DafnyStdLibs_Functions + +import ( + _dafny "dafny" + os "os" + _System "System_" +) +var _ _dafny.Dummy__ +var _ = os.Args +var _ _System.Dummy__ + +type Dummy__ struct{} + + diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Relations/DafnyStdLibs_Relations.go b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Relations/DafnyStdLibs_Relations.go new file mode 100644 index 00000000000..e858cccc560 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Relations/DafnyStdLibs_Relations.go @@ -0,0 +1,19 @@ +// Package DafnyStdLibs_Relations +// Dafny module DafnyStdLibs_Relations compiled into Go + +package DafnyStdLibs_Relations + +import ( + _dafny "dafny" + os "os" + _System "System_" + DafnyStdLibs_Functions "DafnyStdLibs_Functions" +) +var _ _dafny.Dummy__ +var _ = os.Args +var _ _System.Dummy__ +var _ DafnyStdLibs_Functions.Dummy__ + +type Dummy__ struct{} + + diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Wrappers/DafnyStdLibs_Wrappers.go b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Wrappers/DafnyStdLibs_Wrappers.go new file mode 100644 index 00000000000..f76ce326d1c --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyStdLibs_Wrappers/DafnyStdLibs_Wrappers.go @@ -0,0 +1,756 @@ +// Package DafnyStdLibs_Wrappers +// Dafny module DafnyStdLibs_Wrappers compiled into Go + +package DafnyStdLibs_Wrappers + +import ( + _dafny "dafny" + os "os" + _System "System_" + DafnyStdLibs_Functions "DafnyStdLibs_Functions" + DafnyStdLibs_Relations "DafnyStdLibs_Relations" +) +var _ _dafny.Dummy__ +var _ = os.Args +var _ _System.Dummy__ +var _ DafnyStdLibs_Functions.Dummy__ +var _ DafnyStdLibs_Relations.Dummy__ + +type Dummy__ struct{} + + +// Definition of class Default__ +type Default__ struct { + dummy byte +} + +func New_Default___() *Default__ { + _this := Default__{} + + return &_this +} + +type CompanionStruct_Default___ struct { +} +var Companion_Default___ = CompanionStruct_Default___ { +} + +func (_this *Default__) Equals(other *Default__) bool { + return _this == other +} + +func (_this *Default__) EqualsGeneric(x interface{}) bool { + other, ok := x.(*Default__) + return ok && _this.Equals(other) +} + +func (*Default__) String() string { + return "DafnyStdLibs_Wrappers.Default__" +} +func (_this *Default__) ParentTraits_() []*_dafny.TraitID { + return [](*_dafny.TraitID){}; +} +var _ _dafny.TraitOffspring = &Default__{} + +func (_static *CompanionStruct_Default___) Need(condition bool, error_ interface{}) OutcomeResult { + if (condition) { + return Companion_OutcomeResult_.Create_Pass_k_() + } else { + return Companion_OutcomeResult_.Create_Fail_k_(error_) + } +} +// End of class Default__ + +// Definition of datatype Option +type Option struct { + Data_Option_ +} + +func (_this Option) Get_() Data_Option_ { + return _this.Data_Option_ +} + +type Data_Option_ interface { + isOption() +} + +type CompanionStruct_Option_ struct { +} +var Companion_Option_ = CompanionStruct_Option_ { +} + +type Option_None struct { +} + +func (Option_None) isOption() {} + +func (CompanionStruct_Option_) Create_None_() Option { + return Option{Option_None{}} +} + +func (_this Option) Is_None() bool { + _, ok := _this.Get_().(Option_None) + return ok +} + +type Option_Some struct { + Value interface{} +} + +func (Option_Some) isOption() {} + +func (CompanionStruct_Option_) Create_Some_(Value interface{}) Option { + return Option{Option_Some{Value}} +} + +func (_this Option) Is_Some() bool { + _, ok := _this.Get_().(Option_Some) + return ok +} + +func (CompanionStruct_Option_) Default() Option { + return Companion_Option_.Create_None_() +} + +func (_this Option) Dtor_value() interface{} { + return _this.Get_().(Option_Some).Value +} + +func (_this Option) String() string { + switch data := _this.Get_().(type) { + case nil: return "null" + case Option_None: { + return "Wrappers.Option.None" + } + case Option_Some: { + return "Wrappers.Option.Some" + "(" + _dafny.String(data.Value) + ")" + } + default: { + return "" + } + } +} + +func (_this Option) Equals(other Option) bool { + switch data1 := _this.Get_().(type) { + case Option_None: { + _, ok := other.Get_().(Option_None) + return ok + } + case Option_Some: { + data2, ok := other.Get_().(Option_Some) + return ok && _dafny.AreEqual(data1.Value, data2.Value) + } + default: { + return false; // unexpected + } + } +} + +func (_this Option) EqualsGeneric(other interface{}) bool { + typed, ok := other.(Option) + return ok && _this.Equals(typed) +} + +func Type_Option_() _dafny.TypeDescriptor { + return type_Option_{} +} + +type type_Option_ struct { +} + +func (_this type_Option_) Default() interface{} { + return Companion_Option_.Default(); +} + +func (_this type_Option_) String() string { + return "DafnyStdLibs_Wrappers.Option" +} +func (_this Option) ParentTraits_() []*_dafny.TraitID { + return [](*_dafny.TraitID){}; +} +var _ _dafny.TraitOffspring = Option{} + +func (_this Option) IsFailure() bool { + { + return (_this).Is_None() + } +} +func (_this Option) PropagateFailure() Option { + { + return Companion_Option_.Create_None_() + } +} +func (_this Option) Extract() interface{} { + { + return (_this).Dtor_value() + } +} +func (_this Option) GetOr(default_ interface{}) interface{} { + { + var _source0 Option = _this + _ = _source0 + if (_source0.Is_None()) { + return default_ + } else { + var _0___mcc_h0 interface{} = _source0.Get_().(Option_Some).Value + _ = _0___mcc_h0 + var _1_v interface{} = _0___mcc_h0 + _ = _1_v + return _1_v + } + } +} +func (_this Option) ToResult(error_ interface{}) Result { + { + var _source1 Option = _this + _ = _source1 + if (_source1.Is_None()) { + return Companion_Result_.Create_Failure_(error_) + } else { + var _2___mcc_h0 interface{} = _source1.Get_().(Option_Some).Value + _ = _2___mcc_h0 + var _3_v interface{} = _2___mcc_h0 + _ = _3_v + return Companion_Result_.Create_Success_(_3_v) + } + } +} +func (_this Option) ToOutcome(error_ interface{}) Outcome { + { + var _source2 Option = _this + _ = _source2 + if (_source2.Is_None()) { + return Companion_Outcome_.Create_Fail_(error_) + } else { + var _4___mcc_h0 interface{} = _source2.Get_().(Option_Some).Value + _ = _4___mcc_h0 + var _5_v interface{} = _4___mcc_h0 + _ = _5_v + return Companion_Outcome_.Create_Pass_() + } + } +} +func (_this Option) Map(rewrap func (Option) interface{}) interface{} { + { + return (rewrap)(_this) + } +} +// End of datatype Option + +// Definition of datatype Result +type Result struct { + Data_Result_ +} + +func (_this Result) Get_() Data_Result_ { + return _this.Data_Result_ +} + +type Data_Result_ interface { + isResult() +} + +type CompanionStruct_Result_ struct { +} +var Companion_Result_ = CompanionStruct_Result_ { +} + +type Result_Success struct { + Value interface{} +} + +func (Result_Success) isResult() {} + +func (CompanionStruct_Result_) Create_Success_(Value interface{}) Result { + return Result{Result_Success{Value}} +} + +func (_this Result) Is_Success() bool { + _, ok := _this.Get_().(Result_Success) + return ok +} + +type Result_Failure struct { + Error interface{} +} + +func (Result_Failure) isResult() {} + +func (CompanionStruct_Result_) Create_Failure_(Error interface{}) Result { + return Result{Result_Failure{Error}} +} + +func (_this Result) Is_Failure() bool { + _, ok := _this.Get_().(Result_Failure) + return ok +} + +func (CompanionStruct_Result_) Default(_default_R interface{}) Result { + return Companion_Result_.Create_Success_(_default_R) +} + +func (_this Result) Dtor_value() interface{} { + return _this.Get_().(Result_Success).Value +} + +func (_this Result) Dtor_error() interface{} { + return _this.Get_().(Result_Failure).Error +} + +func (_this Result) String() string { + switch data := _this.Get_().(type) { + case nil: return "null" + case Result_Success: { + return "Wrappers.Result.Success" + "(" + _dafny.String(data.Value) + ")" + } + case Result_Failure: { + return "Wrappers.Result.Failure" + "(" + _dafny.String(data.Error) + ")" + } + default: { + return "" + } + } +} + +func (_this Result) Equals(other Result) bool { + switch data1 := _this.Get_().(type) { + case Result_Success: { + data2, ok := other.Get_().(Result_Success) + return ok && _dafny.AreEqual(data1.Value, data2.Value) + } + case Result_Failure: { + data2, ok := other.Get_().(Result_Failure) + return ok && _dafny.AreEqual(data1.Error, data2.Error) + } + default: { + return false; // unexpected + } + } +} + +func (_this Result) EqualsGeneric(other interface{}) bool { + typed, ok := other.(Result) + return ok && _this.Equals(typed) +} + +func Type_Result_(Type_R_ _dafny.TypeDescriptor) _dafny.TypeDescriptor { + return type_Result_{Type_R_} +} + +type type_Result_ struct { + Type_R_ _dafny.TypeDescriptor +} + +func (_this type_Result_) Default() interface{} { + Type_R_ := _this.Type_R_ + _ = Type_R_ + return Companion_Result_.Default(Type_R_.Default()); +} + +func (_this type_Result_) String() string { + return "DafnyStdLibs_Wrappers.Result" +} +func (_this Result) ParentTraits_() []*_dafny.TraitID { + return [](*_dafny.TraitID){}; +} +var _ _dafny.TraitOffspring = Result{} + +func (_this Result) IsFailure() bool { + { + return (_this).Is_Failure() + } +} +func (_this Result) PropagateFailure() Result { + { + return Companion_Result_.Create_Failure_((_this).Dtor_error()) + } +} +func (_this Result) Extract() interface{} { + { + return (_this).Dtor_value() + } +} +func (_this Result) GetOr(default_ interface{}) interface{} { + { + var _source3 Result = _this + _ = _source3 + if (_source3.Is_Success()) { + var _6___mcc_h0 interface{} = _source3.Get_().(Result_Success).Value + _ = _6___mcc_h0 + var _7_s interface{} = _6___mcc_h0 + _ = _7_s + return _7_s + } else { + var _8___mcc_h1 interface{} = _source3.Get_().(Result_Failure).Error + _ = _8___mcc_h1 + var _9_e interface{} = _8___mcc_h1 + _ = _9_e + return default_ + } + } +} +func (_this Result) ToOption() Option { + { + var _source4 Result = _this + _ = _source4 + if (_source4.Is_Success()) { + var _10___mcc_h0 interface{} = _source4.Get_().(Result_Success).Value + _ = _10___mcc_h0 + var _11_s interface{} = _10___mcc_h0 + _ = _11_s + return Companion_Option_.Create_Some_(_11_s) + } else { + var _12___mcc_h1 interface{} = _source4.Get_().(Result_Failure).Error + _ = _12___mcc_h1 + var _13_e interface{} = _12___mcc_h1 + _ = _13_e + return Companion_Option_.Create_None_() + } + } +} +func (_this Result) ToOutcome() Outcome { + { + var _source5 Result = _this + _ = _source5 + if (_source5.Is_Success()) { + var _14___mcc_h0 interface{} = _source5.Get_().(Result_Success).Value + _ = _14___mcc_h0 + var _15_s interface{} = _14___mcc_h0 + _ = _15_s + return Companion_Outcome_.Create_Pass_() + } else { + var _16___mcc_h1 interface{} = _source5.Get_().(Result_Failure).Error + _ = _16___mcc_h1 + var _17_e interface{} = _16___mcc_h1 + _ = _17_e + return Companion_Outcome_.Create_Fail_(_17_e) + } + } +} +func (_this Result) Map(rewrap func (Result) interface{}) interface{} { + { + return (rewrap)(_this) + } +} +func (_this Result) MapFailure(reWrap func (interface{}) interface{}) Result { + { + var _source6 Result = _this + _ = _source6 + if (_source6.Is_Success()) { + var _18___mcc_h0 interface{} = _source6.Get_().(Result_Success).Value + _ = _18___mcc_h0 + var _19_s interface{} = _18___mcc_h0 + _ = _19_s + return Companion_Result_.Create_Success_(_19_s) + } else { + var _20___mcc_h1 interface{} = _source6.Get_().(Result_Failure).Error + _ = _20___mcc_h1 + var _21_e interface{} = _20___mcc_h1 + _ = _21_e + return Companion_Result_.Create_Failure_((reWrap)(_21_e)) + } + } +} +// End of datatype Result + +// Definition of datatype Outcome +type Outcome struct { + Data_Outcome_ +} + +func (_this Outcome) Get_() Data_Outcome_ { + return _this.Data_Outcome_ +} + +type Data_Outcome_ interface { + isOutcome() +} + +type CompanionStruct_Outcome_ struct { +} +var Companion_Outcome_ = CompanionStruct_Outcome_ { +} + +type Outcome_Pass struct { +} + +func (Outcome_Pass) isOutcome() {} + +func (CompanionStruct_Outcome_) Create_Pass_() Outcome { + return Outcome{Outcome_Pass{}} +} + +func (_this Outcome) Is_Pass() bool { + _, ok := _this.Get_().(Outcome_Pass) + return ok +} + +type Outcome_Fail struct { + Error interface{} +} + +func (Outcome_Fail) isOutcome() {} + +func (CompanionStruct_Outcome_) Create_Fail_(Error interface{}) Outcome { + return Outcome{Outcome_Fail{Error}} +} + +func (_this Outcome) Is_Fail() bool { + _, ok := _this.Get_().(Outcome_Fail) + return ok +} + +func (CompanionStruct_Outcome_) Default() Outcome { + return Companion_Outcome_.Create_Pass_() +} + +func (_this Outcome) Dtor_error() interface{} { + return _this.Get_().(Outcome_Fail).Error +} + +func (_this Outcome) String() string { + switch data := _this.Get_().(type) { + case nil: return "null" + case Outcome_Pass: { + return "Wrappers.Outcome.Pass" + } + case Outcome_Fail: { + return "Wrappers.Outcome.Fail" + "(" + _dafny.String(data.Error) + ")" + } + default: { + return "" + } + } +} + +func (_this Outcome) Equals(other Outcome) bool { + switch data1 := _this.Get_().(type) { + case Outcome_Pass: { + _, ok := other.Get_().(Outcome_Pass) + return ok + } + case Outcome_Fail: { + data2, ok := other.Get_().(Outcome_Fail) + return ok && _dafny.AreEqual(data1.Error, data2.Error) + } + default: { + return false; // unexpected + } + } +} + +func (_this Outcome) EqualsGeneric(other interface{}) bool { + typed, ok := other.(Outcome) + return ok && _this.Equals(typed) +} + +func Type_Outcome_() _dafny.TypeDescriptor { + return type_Outcome_{} +} + +type type_Outcome_ struct { +} + +func (_this type_Outcome_) Default() interface{} { + return Companion_Outcome_.Default(); +} + +func (_this type_Outcome_) String() string { + return "DafnyStdLibs_Wrappers.Outcome" +} +func (_this Outcome) ParentTraits_() []*_dafny.TraitID { + return [](*_dafny.TraitID){}; +} +var _ _dafny.TraitOffspring = Outcome{} + +func (_this Outcome) IsFailure() bool { + { + return (_this).Is_Fail() + } +} +func (_this Outcome) PropagateFailure() Outcome { + { + return _this + } +} +func (_this Outcome) ToOption(r interface{}) Option { + { + var _source7 Outcome = _this + _ = _source7 + if (_source7.Is_Pass()) { + return Companion_Option_.Create_Some_(r) + } else { + var _22___mcc_h0 interface{} = _source7.Get_().(Outcome_Fail).Error + _ = _22___mcc_h0 + var _23_e interface{} = _22___mcc_h0 + _ = _23_e + return Companion_Option_.Create_None_() + } + } +} +func (_this Outcome) ToResult(r interface{}) Result { + { + var _source8 Outcome = _this + _ = _source8 + if (_source8.Is_Pass()) { + return Companion_Result_.Create_Success_(r) + } else { + var _24___mcc_h0 interface{} = _source8.Get_().(Outcome_Fail).Error + _ = _24___mcc_h0 + var _25_e interface{} = _24___mcc_h0 + _ = _25_e + return Companion_Result_.Create_Failure_(_25_e) + } + } +} +func (_this Outcome) Map(rewrap func (Outcome) interface{}) interface{} { + { + return (rewrap)(_this) + } +} +func (_this Outcome) MapFailure(rewrap func (interface{}) interface{}, default_ interface{}) Result { + { + var _source9 Outcome = _this + _ = _source9 + if (_source9.Is_Pass()) { + return Companion_Result_.Create_Success_(default_) + } else { + var _26___mcc_h0 interface{} = _source9.Get_().(Outcome_Fail).Error + _ = _26___mcc_h0 + var _27_e interface{} = _26___mcc_h0 + _ = _27_e + return Companion_Result_.Create_Failure_((rewrap)(_27_e)) + } + } +} +func (_static CompanionStruct_Outcome_) Need(condition bool, error_ interface{}) Outcome { + if (condition) { + return Companion_Outcome_.Create_Pass_() + } else { + return Companion_Outcome_.Create_Fail_(error_) + } +} +// End of datatype Outcome + +// Definition of datatype OutcomeResult +type OutcomeResult struct { + Data_OutcomeResult_ +} + +func (_this OutcomeResult) Get_() Data_OutcomeResult_ { + return _this.Data_OutcomeResult_ +} + +type Data_OutcomeResult_ interface { + isOutcomeResult() +} + +type CompanionStruct_OutcomeResult_ struct { +} +var Companion_OutcomeResult_ = CompanionStruct_OutcomeResult_ { +} + +type OutcomeResult_Pass_k struct { +} + +func (OutcomeResult_Pass_k) isOutcomeResult() {} + +func (CompanionStruct_OutcomeResult_) Create_Pass_k_() OutcomeResult { + return OutcomeResult{OutcomeResult_Pass_k{}} +} + +func (_this OutcomeResult) Is_Pass_k() bool { + _, ok := _this.Get_().(OutcomeResult_Pass_k) + return ok +} + +type OutcomeResult_Fail_k struct { + Error interface{} +} + +func (OutcomeResult_Fail_k) isOutcomeResult() {} + +func (CompanionStruct_OutcomeResult_) Create_Fail_k_(Error interface{}) OutcomeResult { + return OutcomeResult{OutcomeResult_Fail_k{Error}} +} + +func (_this OutcomeResult) Is_Fail_k() bool { + _, ok := _this.Get_().(OutcomeResult_Fail_k) + return ok +} + +func (CompanionStruct_OutcomeResult_) Default() OutcomeResult { + return Companion_OutcomeResult_.Create_Pass_k_() +} + +func (_this OutcomeResult) Dtor_error() interface{} { + return _this.Get_().(OutcomeResult_Fail_k).Error +} + +func (_this OutcomeResult) String() string { + switch data := _this.Get_().(type) { + case nil: return "null" + case OutcomeResult_Pass_k: { + return "Wrappers.OutcomeResult.Pass'" + } + case OutcomeResult_Fail_k: { + return "Wrappers.OutcomeResult.Fail'" + "(" + _dafny.String(data.Error) + ")" + } + default: { + return "" + } + } +} + +func (_this OutcomeResult) Equals(other OutcomeResult) bool { + switch data1 := _this.Get_().(type) { + case OutcomeResult_Pass_k: { + _, ok := other.Get_().(OutcomeResult_Pass_k) + return ok + } + case OutcomeResult_Fail_k: { + data2, ok := other.Get_().(OutcomeResult_Fail_k) + return ok && _dafny.AreEqual(data1.Error, data2.Error) + } + default: { + return false; // unexpected + } + } +} + +func (_this OutcomeResult) EqualsGeneric(other interface{}) bool { + typed, ok := other.(OutcomeResult) + return ok && _this.Equals(typed) +} + +func Type_OutcomeResult_() _dafny.TypeDescriptor { + return type_OutcomeResult_{} +} + +type type_OutcomeResult_ struct { +} + +func (_this type_OutcomeResult_) Default() interface{} { + return Companion_OutcomeResult_.Default(); +} + +func (_this type_OutcomeResult_) String() string { + return "DafnyStdLibs_Wrappers.OutcomeResult" +} +func (_this OutcomeResult) ParentTraits_() []*_dafny.TraitID { + return [](*_dafny.TraitID){}; +} +var _ _dafny.TraitOffspring = OutcomeResult{} + +func (_this OutcomeResult) IsFailure() bool { + { + return (_this).Is_Fail_k() + } +} +func (_this OutcomeResult) PropagateFailure() Result { + { + return Companion_Result_.Create_Failure_((_this).Dtor_error()) + } +} +// End of datatype OutcomeResult diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/Makefile b/Source/DafnyRuntime/DafnyRuntimeGo/Makefile index 2965c62acc0..cdcc4f7e8f6 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimeGo/Makefile @@ -5,6 +5,9 @@ DAFNY = dotnet run --project ../../Dafny --no-build -- GENERATED_SYSTEM_MODULE_SOURCE=../obj/systemModulePopulator-go/src/System_/System_.go GENERATED_SYSTEM_MODULE_TARGET=System_/System_.go +GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-go/src/DafnyStdLibs +GENERATED_STDLIBS_TARGET=DafnyStdLibs + all: check-system-module test test: @@ -18,3 +21,18 @@ check-system-module: build-system-module update-system-module: build-system-module cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET) + +build-stdlibs: + $(DAFNY) translate go --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries + +check-stdlibs: build-stdlibs + diff $(GENERATED_STDLIBS_SOURCE)/DafnyStdLibs.go $(GENERATED_STDLIBS_TARGET)/DafnyStdLibs.go + diff $(GENERATED_STDLIBS_SOURCE)_Functions/DafnyStdLibs_Functions.go $(GENERATED_STDLIBS_TARGET)_Functions/DafnyStdLibs_Functions.go + diff $(GENERATED_STDLIBS_SOURCE)_Relations/DafnyStdLibs_Relations.go $(GENERATED_STDLIBS_TARGET)_Relations/DafnyStdLibs_Relations.go + diff $(GENERATED_STDLIBS_SOURCE)_Wrappers/DafnyStdLibs_Wrappers.go $(GENERATED_STDLIBS_TARGET)_Wrappers/DafnyStdLibs_Wrappers.go + +update-stdlibs: build-stdlibs + cp $(GENERATED_STDLIBS_SOURCE)/DafnyStdLibs.go $(GENERATED_STDLIBS_TARGET)/DafnyStdLibs.go + cp $(GENERATED_STDLIBS_SOURCE)_Functions/DafnyStdLibs_Functions.go $(GENERATED_STDLIBS_TARGET)_Functions/DafnyStdLibs_Functions.go + cp $(GENERATED_STDLIBS_SOURCE)_Relations/DafnyStdLibs_Relations.go $(GENERATED_STDLIBS_TARGET)_Relations/DafnyStdLibs_Relations.go + cp $(GENERATED_STDLIBS_SOURCE)_Wrappers/DafnyStdLibs_Wrappers.go $(GENERATED_STDLIBS_TARGET)_Wrappers/DafnyStdLibs_Wrappers.go diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/Makefile b/Source/DafnyRuntime/DafnyRuntimeJava/Makefile index 4bd3c3b50fb..5ca3159c53f 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJava/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimeJava/Makefile @@ -8,6 +8,9 @@ GENERATED_SYSTEM_MODULE_TARGET=src/main/dafny-generated/_System GENERATED_DAFNY_MODULE_SOURCE=../obj/systemModulePopulator-java/dafny GENERATED_DAFNY_MODULE_TARGET=src/main/dafny-generated/dafny +GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-java/DafnyStdLibs +GENERATED_STDLIBS_TARGET=src/main/dafny-generated/DafnyStdLibs + all: check-system-module test test: @@ -26,3 +29,13 @@ update-system-module: build-system-module cp -r $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET) rm -rf $(GENERATED_DAFNY_MODULE_TARGET) cp -r $(GENERATED_DAFNY_MODULE_SOURCE) $(GENERATED_DAFNY_MODULE_TARGET) + +build-stdlibs: + $(DAFNY) translate java --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries + +check-stdlibs: build-stdlibs + diff $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET) + +update-stdlibs: build-stdlibs + rm -rf $(GENERATED_STDLIBS_TARGET) + cp -r $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET) diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option.java new file mode 100644 index 00000000000..9aa56a60a8d --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option.java @@ -0,0 +1,78 @@ +// Class Option +// Dafny class Option compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public abstract class Option { + protected dafny.TypeDescriptor _td_T; + public Option(dafny.TypeDescriptor _td_T) { + this._td_T = _td_T; + } + + public static Option Default(dafny.TypeDescriptor _td_T) { + return DafnyStdLibs.Wrappers.Option.create_None(_td_T); + } + public static dafny.TypeDescriptor> _typeDescriptor(dafny.TypeDescriptor _td_T) { + return (dafny.TypeDescriptor>) (dafny.TypeDescriptor) dafny.TypeDescriptor.>referenceWithInitializer(Option.class, () -> Option.Default(_td_T)); + } + public static Option create_None(dafny.TypeDescriptor _td_T) { + return new Option_None(_td_T); + } + public static Option create_Some(dafny.TypeDescriptor _td_T, T value) { + return new Option_Some(_td_T, value); + } + public boolean is_None() { return this instanceof Option_None; } + public boolean is_Some() { return this instanceof Option_Some; } + public T dtor_value() { + Option d = this; + return ((Option_Some)d)._value; + } + public boolean IsFailure(dafny.TypeDescriptor _td_T) { + return (this).is_None(); + } + public <__U> Option<__U> PropagateFailure(dafny.TypeDescriptor _td_T, dafny.TypeDescriptor<__U> _td___U) + { + return DafnyStdLibs.Wrappers.Option.<__U>create_None(_td___U); + } + public T Extract(dafny.TypeDescriptor _td_T) { + return (this).dtor_value(); + } + public T GetOr(dafny.TypeDescriptor _td_T, T default_) + { + Option _source0 = this; + if (_source0.is_None()) { + return default_; + } else { + T _0___mcc_h0 = ((DafnyStdLibs.Wrappers.Option_Some)_source0)._value; + T _1_v = _0___mcc_h0; + return _1_v; + } + } + public <__E> Result ToResult(dafny.TypeDescriptor _td_T, dafny.TypeDescriptor<__E> _td___E, __E error) + { + Option _source1 = this; + if (_source1.is_None()) { + return DafnyStdLibs.Wrappers.Result.create_Failure(_td_T, _td___E, error); + } else { + T _2___mcc_h0 = ((DafnyStdLibs.Wrappers.Option_Some)_source1)._value; + T _3_v = _2___mcc_h0; + return DafnyStdLibs.Wrappers.Result.create_Success(_td_T, _td___E, _3_v); + } + } + public <__E> Outcome<__E> ToOutcome(dafny.TypeDescriptor _td_T, dafny.TypeDescriptor<__E> _td___E, __E error) + { + Option _source2 = this; + if (_source2.is_None()) { + return DafnyStdLibs.Wrappers.Outcome.<__E>create_Fail(_td___E, error); + } else { + T _4___mcc_h0 = ((DafnyStdLibs.Wrappers.Option_Some)_source2)._value; + T _5_v = _4___mcc_h0; + return DafnyStdLibs.Wrappers.Outcome.<__E>create_Pass(_td___E); + } + } + public <__FC> __FC Map(dafny.TypeDescriptor _td_T, dafny.TypeDescriptor<__FC> _td___FC, java.util.function.Function, __FC> rewrap) + { + return ((__FC)(java.lang.Object)((rewrap).apply(this))); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option_None.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option_None.java new file mode 100644 index 00000000000..311789e9401 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option_None.java @@ -0,0 +1,33 @@ +// Class Option_None +// Dafny class Option_None compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public class Option_None extends Option { + public Option_None (dafny.TypeDescriptor _td_T) { + super(_td_T); + } + + @Override + public boolean equals(Object other) { + if (this == other) return true; + if (other == null) return false; + if (getClass() != other.getClass()) return false; + Option_None o = (Option_None)other; + return true; + } + @Override + public int hashCode() { + long hash = 5381; + hash = ((hash << 5) + hash) + 0; + return (int)hash; + } + + @Override + public String toString() { + StringBuilder s = new StringBuilder(); + s.append("Wrappers.Option.None"); + return s.toString(); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option_Some.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option_Some.java new file mode 100644 index 00000000000..31261b46820 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Option_Some.java @@ -0,0 +1,39 @@ +// Class Option_Some +// Dafny class Option_Some compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public class Option_Some extends Option { + public T _value; + public Option_Some (dafny.TypeDescriptor _td_T, T value) { + super(_td_T); + this._value = value; + } + + @Override + public boolean equals(Object other) { + if (this == other) return true; + if (other == null) return false; + if (getClass() != other.getClass()) return false; + Option_Some o = (Option_Some)other; + return true && java.util.Objects.equals(this._value, o._value); + } + @Override + public int hashCode() { + long hash = 5381; + hash = ((hash << 5) + hash) + 1; + hash = ((hash << 5) + hash) + java.util.Objects.hashCode(this._value); + return (int)hash; + } + + @Override + public String toString() { + StringBuilder s = new StringBuilder(); + s.append("Wrappers.Option.Some"); + s.append("("); + s.append(dafny.Helpers.toString(this._value)); + s.append(")"); + return s.toString(); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome.java new file mode 100644 index 00000000000..a9886c9d583 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome.java @@ -0,0 +1,82 @@ +// Class Outcome +// Dafny class Outcome compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public abstract class Outcome { + protected dafny.TypeDescriptor _td_E; + public Outcome(dafny.TypeDescriptor _td_E) { + this._td_E = _td_E; + } + + public static Outcome Default(dafny.TypeDescriptor _td_E) { + return DafnyStdLibs.Wrappers.Outcome.create_Pass(_td_E); + } + public static dafny.TypeDescriptor> _typeDescriptor(dafny.TypeDescriptor _td_E) { + return (dafny.TypeDescriptor>) (dafny.TypeDescriptor) dafny.TypeDescriptor.>referenceWithInitializer(Outcome.class, () -> Outcome.Default(_td_E)); + } + public static Outcome create_Pass(dafny.TypeDescriptor _td_E) { + return new Outcome_Pass(_td_E); + } + public static Outcome create_Fail(dafny.TypeDescriptor _td_E, E error) { + return new Outcome_Fail(_td_E, error); + } + public boolean is_Pass() { return this instanceof Outcome_Pass; } + public boolean is_Fail() { return this instanceof Outcome_Fail; } + public E dtor_error() { + Outcome d = this; + return ((Outcome_Fail)d)._error; + } + public boolean IsFailure(dafny.TypeDescriptor _td_E) { + return (this).is_Fail(); + } + public Outcome PropagateFailure(dafny.TypeDescriptor _td_E) { + return this; + } + public <__R> Option<__R> ToOption(dafny.TypeDescriptor _td_E, dafny.TypeDescriptor<__R> _td___R, __R r) + { + Outcome _source7 = this; + if (_source7.is_Pass()) { + return DafnyStdLibs.Wrappers.Option.<__R>create_Some(_td___R, r); + } else { + E _22___mcc_h0 = ((DafnyStdLibs.Wrappers.Outcome_Fail)_source7)._error; + E _23_e = _22___mcc_h0; + return DafnyStdLibs.Wrappers.Option.<__R>create_None(_td___R); + } + } + public <__R> Result<__R, E> ToResult(dafny.TypeDescriptor _td_E, dafny.TypeDescriptor<__R> _td___R, __R r) + { + Outcome _source8 = this; + if (_source8.is_Pass()) { + return DafnyStdLibs.Wrappers.Result.<__R, E>create_Success(_td___R, _td_E, r); + } else { + E _24___mcc_h0 = ((DafnyStdLibs.Wrappers.Outcome_Fail)_source8)._error; + E _25_e = _24___mcc_h0; + return DafnyStdLibs.Wrappers.Result.<__R, E>create_Failure(_td___R, _td_E, _25_e); + } + } + public <__FC> __FC Map(dafny.TypeDescriptor _td_E, dafny.TypeDescriptor<__FC> _td___FC, java.util.function.Function, __FC> rewrap) + { + return ((__FC)(java.lang.Object)((rewrap).apply(this))); + } + public <__T, __NewE> Result<__T, __NewE> MapFailure(dafny.TypeDescriptor _td_E, dafny.TypeDescriptor<__T> _td___T, dafny.TypeDescriptor<__NewE> _td___NewE, java.util.function.Function rewrap, __T default_) + { + Outcome _source9 = this; + if (_source9.is_Pass()) { + return DafnyStdLibs.Wrappers.Result.<__T, __NewE>create_Success(_td___T, _td___NewE, default_); + } else { + E _26___mcc_h0 = ((DafnyStdLibs.Wrappers.Outcome_Fail)_source9)._error; + E _27_e = _26___mcc_h0; + return DafnyStdLibs.Wrappers.Result.<__T, __NewE>create_Failure(_td___T, _td___NewE, ((__NewE)(java.lang.Object)((rewrap).apply(_27_e)))); + } + } + public static Outcome Need(dafny.TypeDescriptor _td_E, boolean condition, E error) + { + if (condition) { + return DafnyStdLibs.Wrappers.Outcome.create_Pass(_td_E); + } else { + return DafnyStdLibs.Wrappers.Outcome.create_Fail(_td_E, error); + } + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult.java new file mode 100644 index 00000000000..a9581950e86 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult.java @@ -0,0 +1,38 @@ +// Class OutcomeResult +// Dafny class OutcomeResult compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public abstract class OutcomeResult { + protected dafny.TypeDescriptor _td_E; + public OutcomeResult(dafny.TypeDescriptor _td_E) { + this._td_E = _td_E; + } + + public static OutcomeResult Default(dafny.TypeDescriptor _td_E) { + return DafnyStdLibs.Wrappers.OutcomeResult.create_Pass_k(_td_E); + } + public static dafny.TypeDescriptor> _typeDescriptor(dafny.TypeDescriptor _td_E) { + return (dafny.TypeDescriptor>) (dafny.TypeDescriptor) dafny.TypeDescriptor.>referenceWithInitializer(OutcomeResult.class, () -> OutcomeResult.Default(_td_E)); + } + public static OutcomeResult create_Pass_k(dafny.TypeDescriptor _td_E) { + return new OutcomeResult_Pass_k(_td_E); + } + public static OutcomeResult create_Fail_k(dafny.TypeDescriptor _td_E, E error) { + return new OutcomeResult_Fail_k(_td_E, error); + } + public boolean is_Pass_k() { return this instanceof OutcomeResult_Pass_k; } + public boolean is_Fail_k() { return this instanceof OutcomeResult_Fail_k; } + public E dtor_error() { + OutcomeResult d = this; + return ((OutcomeResult_Fail_k)d)._error; + } + public boolean IsFailure(dafny.TypeDescriptor _td_E) { + return (this).is_Fail_k(); + } + public <__U> Result<__U, E> PropagateFailure(dafny.TypeDescriptor _td_E, dafny.TypeDescriptor<__U> _td___U) + { + return DafnyStdLibs.Wrappers.Result.<__U, E>create_Failure(_td___U, _td_E, (this).dtor_error()); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult_Fail_k.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult_Fail_k.java new file mode 100644 index 00000000000..3fb604db1f5 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult_Fail_k.java @@ -0,0 +1,39 @@ +// Class OutcomeResult_Fail_k +// Dafny class OutcomeResult_Fail_k compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public class OutcomeResult_Fail_k extends OutcomeResult { + public E _error; + public OutcomeResult_Fail_k (dafny.TypeDescriptor _td_E, E error) { + super(_td_E); + this._error = error; + } + + @Override + public boolean equals(Object other) { + if (this == other) return true; + if (other == null) return false; + if (getClass() != other.getClass()) return false; + OutcomeResult_Fail_k o = (OutcomeResult_Fail_k)other; + return true && java.util.Objects.equals(this._error, o._error); + } + @Override + public int hashCode() { + long hash = 5381; + hash = ((hash << 5) + hash) + 1; + hash = ((hash << 5) + hash) + java.util.Objects.hashCode(this._error); + return (int)hash; + } + + @Override + public String toString() { + StringBuilder s = new StringBuilder(); + s.append("Wrappers.OutcomeResult.Fail'"); + s.append("("); + s.append(dafny.Helpers.toString(this._error)); + s.append(")"); + return s.toString(); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult_Pass_k.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult_Pass_k.java new file mode 100644 index 00000000000..32e1db71e80 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/OutcomeResult_Pass_k.java @@ -0,0 +1,33 @@ +// Class OutcomeResult_Pass_k +// Dafny class OutcomeResult_Pass_k compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public class OutcomeResult_Pass_k extends OutcomeResult { + public OutcomeResult_Pass_k (dafny.TypeDescriptor _td_E) { + super(_td_E); + } + + @Override + public boolean equals(Object other) { + if (this == other) return true; + if (other == null) return false; + if (getClass() != other.getClass()) return false; + OutcomeResult_Pass_k o = (OutcomeResult_Pass_k)other; + return true; + } + @Override + public int hashCode() { + long hash = 5381; + hash = ((hash << 5) + hash) + 0; + return (int)hash; + } + + @Override + public String toString() { + StringBuilder s = new StringBuilder(); + s.append("Wrappers.OutcomeResult.Pass'"); + return s.toString(); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome_Fail.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome_Fail.java new file mode 100644 index 00000000000..4662de0a199 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome_Fail.java @@ -0,0 +1,39 @@ +// Class Outcome_Fail +// Dafny class Outcome_Fail compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public class Outcome_Fail extends Outcome { + public E _error; + public Outcome_Fail (dafny.TypeDescriptor _td_E, E error) { + super(_td_E); + this._error = error; + } + + @Override + public boolean equals(Object other) { + if (this == other) return true; + if (other == null) return false; + if (getClass() != other.getClass()) return false; + Outcome_Fail o = (Outcome_Fail)other; + return true && java.util.Objects.equals(this._error, o._error); + } + @Override + public int hashCode() { + long hash = 5381; + hash = ((hash << 5) + hash) + 1; + hash = ((hash << 5) + hash) + java.util.Objects.hashCode(this._error); + return (int)hash; + } + + @Override + public String toString() { + StringBuilder s = new StringBuilder(); + s.append("Wrappers.Outcome.Fail"); + s.append("("); + s.append(dafny.Helpers.toString(this._error)); + s.append(")"); + return s.toString(); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome_Pass.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome_Pass.java new file mode 100644 index 00000000000..c6e39654ed7 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Outcome_Pass.java @@ -0,0 +1,33 @@ +// Class Outcome_Pass +// Dafny class Outcome_Pass compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public class Outcome_Pass extends Outcome { + public Outcome_Pass (dafny.TypeDescriptor _td_E) { + super(_td_E); + } + + @Override + public boolean equals(Object other) { + if (this == other) return true; + if (other == null) return false; + if (getClass() != other.getClass()) return false; + Outcome_Pass o = (Outcome_Pass)other; + return true; + } + @Override + public int hashCode() { + long hash = 5381; + hash = ((hash << 5) + hash) + 0; + return (int)hash; + } + + @Override + public String toString() { + StringBuilder s = new StringBuilder(); + s.append("Wrappers.Outcome.Pass"); + return s.toString(); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result.java new file mode 100644 index 00000000000..963ad2c9de1 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result.java @@ -0,0 +1,105 @@ +// Class Result +// Dafny class Result compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public abstract class Result { + protected dafny.TypeDescriptor _td_R; + protected dafny.TypeDescriptor _td_E; + public Result(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E) { + this._td_R = _td_R; + this._td_E = _td_E; + } + + public static Result Default(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E, R _default_R) { + return DafnyStdLibs.Wrappers.Result.create_Success(_td_R, _td_E, _default_R); + } + public static dafny.TypeDescriptor> _typeDescriptor(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E) { + return (dafny.TypeDescriptor>) (dafny.TypeDescriptor) dafny.TypeDescriptor.>referenceWithInitializer(Result.class, () -> Result.Default(_td_R, _td_E, _td_R.defaultValue())); + } + public static Result create_Success(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E, R value) { + return new Result_Success(_td_R, _td_E, value); + } + public static Result create_Failure(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E, E error) { + return new Result_Failure(_td_R, _td_E, error); + } + public boolean is_Success() { return this instanceof Result_Success; } + public boolean is_Failure() { return this instanceof Result_Failure; } + public R dtor_value() { + Result d = this; + return ((Result_Success)d)._value; + } + public E dtor_error() { + Result d = this; + return ((Result_Failure)d)._error; + } + public boolean IsFailure(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E) + { + return (this).is_Failure(); + } + public <__U> Result<__U, E> PropagateFailure(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E, dafny.TypeDescriptor<__U> _td___U) + { + return DafnyStdLibs.Wrappers.Result.<__U, E>create_Failure(_td___U, _td_E, (this).dtor_error()); + } + public R Extract(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E) + { + return (this).dtor_value(); + } + public R GetOr(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E, R default_) + { + Result _source3 = this; + if (_source3.is_Success()) { + R _6___mcc_h0 = ((DafnyStdLibs.Wrappers.Result_Success)_source3)._value; + R _7_s = _6___mcc_h0; + return _7_s; + } else { + E _8___mcc_h1 = ((DafnyStdLibs.Wrappers.Result_Failure)_source3)._error; + E _9_e = _8___mcc_h1; + return default_; + } + } + public Option ToOption(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E) + { + Result _source4 = this; + if (_source4.is_Success()) { + R _10___mcc_h0 = ((DafnyStdLibs.Wrappers.Result_Success)_source4)._value; + R _11_s = _10___mcc_h0; + return DafnyStdLibs.Wrappers.Option.create_Some(_td_R, _11_s); + } else { + E _12___mcc_h1 = ((DafnyStdLibs.Wrappers.Result_Failure)_source4)._error; + E _13_e = _12___mcc_h1; + return DafnyStdLibs.Wrappers.Option.create_None(_td_R); + } + } + public Outcome ToOutcome(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E) + { + Result _source5 = this; + if (_source5.is_Success()) { + R _14___mcc_h0 = ((DafnyStdLibs.Wrappers.Result_Success)_source5)._value; + R _15_s = _14___mcc_h0; + return DafnyStdLibs.Wrappers.Outcome.create_Pass(_td_E); + } else { + E _16___mcc_h1 = ((DafnyStdLibs.Wrappers.Result_Failure)_source5)._error; + E _17_e = _16___mcc_h1; + return DafnyStdLibs.Wrappers.Outcome.create_Fail(_td_E, _17_e); + } + } + public <__FC> __FC Map(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E, dafny.TypeDescriptor<__FC> _td___FC, java.util.function.Function, __FC> rewrap) + { + return ((__FC)(java.lang.Object)((rewrap).apply(this))); + } + public <__NewE> Result MapFailure(dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E, dafny.TypeDescriptor<__NewE> _td___NewE, java.util.function.Function reWrap) + { + Result _source6 = this; + if (_source6.is_Success()) { + R _18___mcc_h0 = ((DafnyStdLibs.Wrappers.Result_Success)_source6)._value; + R _19_s = _18___mcc_h0; + return DafnyStdLibs.Wrappers.Result.create_Success(_td_R, _td___NewE, _19_s); + } else { + E _20___mcc_h1 = ((DafnyStdLibs.Wrappers.Result_Failure)_source6)._error; + E _21_e = _20___mcc_h1; + return DafnyStdLibs.Wrappers.Result.create_Failure(_td_R, _td___NewE, ((__NewE)(java.lang.Object)((reWrap).apply(_21_e)))); + } + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result_Failure.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result_Failure.java new file mode 100644 index 00000000000..4095115e800 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result_Failure.java @@ -0,0 +1,39 @@ +// Class Result_Failure +// Dafny class Result_Failure compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public class Result_Failure extends Result { + public E _error; + public Result_Failure (dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E, E error) { + super(_td_R, _td_E); + this._error = error; + } + + @Override + public boolean equals(Object other) { + if (this == other) return true; + if (other == null) return false; + if (getClass() != other.getClass()) return false; + Result_Failure o = (Result_Failure)other; + return true && java.util.Objects.equals(this._error, o._error); + } + @Override + public int hashCode() { + long hash = 5381; + hash = ((hash << 5) + hash) + 1; + hash = ((hash << 5) + hash) + java.util.Objects.hashCode(this._error); + return (int)hash; + } + + @Override + public String toString() { + StringBuilder s = new StringBuilder(); + s.append("Wrappers.Result.Failure"); + s.append("("); + s.append(dafny.Helpers.toString(this._error)); + s.append(")"); + return s.toString(); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result_Success.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result_Success.java new file mode 100644 index 00000000000..1eb528afcd2 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/Result_Success.java @@ -0,0 +1,39 @@ +// Class Result_Success +// Dafny class Result_Success compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public class Result_Success extends Result { + public R _value; + public Result_Success (dafny.TypeDescriptor _td_R, dafny.TypeDescriptor _td_E, R value) { + super(_td_R, _td_E); + this._value = value; + } + + @Override + public boolean equals(Object other) { + if (this == other) return true; + if (other == null) return false; + if (getClass() != other.getClass()) return false; + Result_Success o = (Result_Success)other; + return true && java.util.Objects.equals(this._value, o._value); + } + @Override + public int hashCode() { + long hash = 5381; + hash = ((hash << 5) + hash) + 0; + hash = ((hash << 5) + hash) + java.util.Objects.hashCode(this._value); + return (int)hash; + } + + @Override + public String toString() { + StringBuilder s = new StringBuilder(); + s.append("Wrappers.Result.Success"); + s.append("("); + s.append(dafny.Helpers.toString(this._value)); + s.append(")"); + return s.toString(); + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/__default.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/__default.java new file mode 100644 index 00000000000..870afd64beb --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/dafny-generated/DafnyStdLibs/Wrappers/__default.java @@ -0,0 +1,22 @@ +// Class __default +// Dafny class __default compiled into Java +package DafnyStdLibs.Wrappers; + + +@SuppressWarnings({"unchecked", "deprecation"}) +public class __default { + public __default() { + } + public static <__E> OutcomeResult<__E> Need(dafny.TypeDescriptor<__E> _td___E, boolean condition, __E error) + { + if (condition) { + return DafnyStdLibs.Wrappers.OutcomeResult.<__E>create_Pass_k(_td___E); + } else { + return DafnyStdLibs.Wrappers.OutcomeResult.<__E>create_Fail_k(_td___E, error); + } + } + @Override + public java.lang.String toString() { + return "DafnyStdLibs.Wrappers._default"; + } +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJs/DafnyStandardLibraries.js b/Source/DafnyRuntime/DafnyRuntimeJs/DafnyStandardLibraries.js new file mode 100644 index 00000000000..7b667ae13a1 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimeJs/DafnyStandardLibraries.js @@ -0,0 +1,407 @@ +// Dafny program the_program compiled into JavaScript +let DafnyStdLibs_Functions = (function() { + let $module = {}; + + return $module; +})(); // end of module DafnyStdLibs_Functions +let DafnyStdLibs_Relations = (function() { + let $module = {}; + + return $module; +})(); // end of module DafnyStdLibs_Relations +let DafnyStdLibs_Wrappers = (function() { + let $module = {}; + + $module.__default = class __default { + constructor () { + this._tname = "DafnyStdLibs.Wrappers._default"; + } + _parentTraits() { + return []; + } + static Need(condition, error) { + if (condition) { + return DafnyStdLibs_Wrappers.OutcomeResult.create_Pass_k(); + } else { + return DafnyStdLibs_Wrappers.OutcomeResult.create_Fail_k(error); + } + }; + }; + + $module.Option = class Option { + constructor(tag) { + this.$tag = tag; + } + static create_None() { + let $dt = new Option(0); + return $dt; + } + static create_Some(value) { + let $dt = new Option(1); + $dt.value = value; + return $dt; + } + get is_None() { return this.$tag === 0; } + get is_Some() { return this.$tag === 1; } + get dtor_value() { return this.value; } + toString() { + if (this.$tag === 0) { + return "Wrappers.Option.None"; + } else if (this.$tag === 1) { + return "Wrappers.Option.Some" + "(" + _dafny.toString(this.value) + ")"; + } else { + return ""; + } + } + equals(other) { + if (this === other) { + return true; + } else if (this.$tag === 0) { + return other.$tag === 0; + } else if (this.$tag === 1) { + return other.$tag === 1 && _dafny.areEqual(this.value, other.value); + } else { + return false; // unexpected + } + } + static Default() { + return DafnyStdLibs_Wrappers.Option.create_None(); + } + static Rtd() { + return class { + static get Default() { + return Option.Default(); + } + }; + } + IsFailure() { + let _this = this; + return (_this).is_None; + }; + PropagateFailure() { + let _this = this; + return DafnyStdLibs_Wrappers.Option.create_None(); + }; + Extract() { + let _this = this; + return (_this).dtor_value; + }; + GetOr(_$$_default) { + let _this = this; + let _source0 = _this; + if (_source0.is_None) { + return _$$_default; + } else { + let _0___mcc_h0 = (_source0).value; + let _1_v = _0___mcc_h0; + return _1_v; + } + }; + ToResult(error) { + let _this = this; + let _source1 = _this; + if (_source1.is_None) { + return DafnyStdLibs_Wrappers.Result.create_Failure(error); + } else { + let _2___mcc_h0 = (_source1).value; + let _3_v = _2___mcc_h0; + return DafnyStdLibs_Wrappers.Result.create_Success(_3_v); + } + }; + ToOutcome(error) { + let _this = this; + let _source2 = _this; + if (_source2.is_None) { + return DafnyStdLibs_Wrappers.Outcome.create_Fail(error); + } else { + let _4___mcc_h0 = (_source2).value; + let _5_v = _4___mcc_h0; + return DafnyStdLibs_Wrappers.Outcome.create_Pass(); + } + }; + Map(rewrap) { + let _this = this; + return (rewrap)(_this); + }; + } + + $module.Result = class Result { + constructor(tag) { + this.$tag = tag; + } + static create_Success(value) { + let $dt = new Result(0); + $dt.value = value; + return $dt; + } + static create_Failure(error) { + let $dt = new Result(1); + $dt.error = error; + return $dt; + } + get is_Success() { return this.$tag === 0; } + get is_Failure() { return this.$tag === 1; } + get dtor_value() { return this.value; } + get dtor_error() { return this.error; } + toString() { + if (this.$tag === 0) { + return "Wrappers.Result.Success" + "(" + _dafny.toString(this.value) + ")"; + } else if (this.$tag === 1) { + return "Wrappers.Result.Failure" + "(" + _dafny.toString(this.error) + ")"; + } else { + return ""; + } + } + equals(other) { + if (this === other) { + return true; + } else if (this.$tag === 0) { + return other.$tag === 0 && _dafny.areEqual(this.value, other.value); + } else if (this.$tag === 1) { + return other.$tag === 1 && _dafny.areEqual(this.error, other.error); + } else { + return false; // unexpected + } + } + static Default(_default_R) { + return DafnyStdLibs_Wrappers.Result.create_Success(_default_R); + } + static Rtd(rtd$_R) { + return class { + static get Default() { + return Result.Default(rtd$_R.Default); + } + }; + } + IsFailure() { + let _this = this; + return (_this).is_Failure; + }; + PropagateFailure() { + let _this = this; + return DafnyStdLibs_Wrappers.Result.create_Failure((_this).dtor_error); + }; + Extract() { + let _this = this; + return (_this).dtor_value; + }; + GetOr(_$$_default) { + let _this = this; + let _source3 = _this; + if (_source3.is_Success) { + let _6___mcc_h0 = (_source3).value; + let _7_s = _6___mcc_h0; + return _7_s; + } else { + let _8___mcc_h1 = (_source3).error; + let _9_e = _8___mcc_h1; + return _$$_default; + } + }; + ToOption() { + let _this = this; + let _source4 = _this; + if (_source4.is_Success) { + let _10___mcc_h0 = (_source4).value; + let _11_s = _10___mcc_h0; + return DafnyStdLibs_Wrappers.Option.create_Some(_11_s); + } else { + let _12___mcc_h1 = (_source4).error; + let _13_e = _12___mcc_h1; + return DafnyStdLibs_Wrappers.Option.create_None(); + } + }; + ToOutcome() { + let _this = this; + let _source5 = _this; + if (_source5.is_Success) { + let _14___mcc_h0 = (_source5).value; + let _15_s = _14___mcc_h0; + return DafnyStdLibs_Wrappers.Outcome.create_Pass(); + } else { + let _16___mcc_h1 = (_source5).error; + let _17_e = _16___mcc_h1; + return DafnyStdLibs_Wrappers.Outcome.create_Fail(_17_e); + } + }; + Map(rewrap) { + let _this = this; + return (rewrap)(_this); + }; + MapFailure(reWrap) { + let _this = this; + let _source6 = _this; + if (_source6.is_Success) { + let _18___mcc_h0 = (_source6).value; + let _19_s = _18___mcc_h0; + return DafnyStdLibs_Wrappers.Result.create_Success(_19_s); + } else { + let _20___mcc_h1 = (_source6).error; + let _21_e = _20___mcc_h1; + return DafnyStdLibs_Wrappers.Result.create_Failure((reWrap)(_21_e)); + } + }; + } + + $module.Outcome = class Outcome { + constructor(tag) { + this.$tag = tag; + } + static create_Pass() { + let $dt = new Outcome(0); + return $dt; + } + static create_Fail(error) { + let $dt = new Outcome(1); + $dt.error = error; + return $dt; + } + get is_Pass() { return this.$tag === 0; } + get is_Fail() { return this.$tag === 1; } + get dtor_error() { return this.error; } + toString() { + if (this.$tag === 0) { + return "Wrappers.Outcome.Pass"; + } else if (this.$tag === 1) { + return "Wrappers.Outcome.Fail" + "(" + _dafny.toString(this.error) + ")"; + } else { + return ""; + } + } + equals(other) { + if (this === other) { + return true; + } else if (this.$tag === 0) { + return other.$tag === 0; + } else if (this.$tag === 1) { + return other.$tag === 1 && _dafny.areEqual(this.error, other.error); + } else { + return false; // unexpected + } + } + static Default() { + return DafnyStdLibs_Wrappers.Outcome.create_Pass(); + } + static Rtd() { + return class { + static get Default() { + return Outcome.Default(); + } + }; + } + IsFailure() { + let _this = this; + return (_this).is_Fail; + }; + PropagateFailure() { + let _this = this; + return _this; + }; + ToOption(r) { + let _this = this; + let _source7 = _this; + if (_source7.is_Pass) { + return DafnyStdLibs_Wrappers.Option.create_Some(r); + } else { + let _22___mcc_h0 = (_source7).error; + let _23_e = _22___mcc_h0; + return DafnyStdLibs_Wrappers.Option.create_None(); + } + }; + ToResult(r) { + let _this = this; + let _source8 = _this; + if (_source8.is_Pass) { + return DafnyStdLibs_Wrappers.Result.create_Success(r); + } else { + let _24___mcc_h0 = (_source8).error; + let _25_e = _24___mcc_h0; + return DafnyStdLibs_Wrappers.Result.create_Failure(_25_e); + } + }; + Map(rewrap) { + let _this = this; + return (rewrap)(_this); + }; + MapFailure(rewrap, _$$_default) { + let _this = this; + let _source9 = _this; + if (_source9.is_Pass) { + return DafnyStdLibs_Wrappers.Result.create_Success(_$$_default); + } else { + let _26___mcc_h0 = (_source9).error; + let _27_e = _26___mcc_h0; + return DafnyStdLibs_Wrappers.Result.create_Failure((rewrap)(_27_e)); + } + }; + static Need(condition, error) { + if (condition) { + return DafnyStdLibs_Wrappers.Outcome.create_Pass(); + } else { + return DafnyStdLibs_Wrappers.Outcome.create_Fail(error); + } + }; + } + + $module.OutcomeResult = class OutcomeResult { + constructor(tag) { + this.$tag = tag; + } + static create_Pass_k() { + let $dt = new OutcomeResult(0); + return $dt; + } + static create_Fail_k(error) { + let $dt = new OutcomeResult(1); + $dt.error = error; + return $dt; + } + get is_Pass_k() { return this.$tag === 0; } + get is_Fail_k() { return this.$tag === 1; } + get dtor_error() { return this.error; } + toString() { + if (this.$tag === 0) { + return "Wrappers.OutcomeResult.Pass'"; + } else if (this.$tag === 1) { + return "Wrappers.OutcomeResult.Fail'" + "(" + _dafny.toString(this.error) + ")"; + } else { + return ""; + } + } + equals(other) { + if (this === other) { + return true; + } else if (this.$tag === 0) { + return other.$tag === 0; + } else if (this.$tag === 1) { + return other.$tag === 1 && _dafny.areEqual(this.error, other.error); + } else { + return false; // unexpected + } + } + static Default() { + return DafnyStdLibs_Wrappers.OutcomeResult.create_Pass_k(); + } + static Rtd() { + return class { + static get Default() { + return OutcomeResult.Default(); + } + }; + } + IsFailure() { + let _this = this; + return (_this).is_Fail_k; + }; + PropagateFailure() { + let _this = this; + return DafnyStdLibs_Wrappers.Result.create_Failure((_this).dtor_error); + }; + } + return $module; +})(); // end of module DafnyStdLibs_Wrappers +let DafnyStdLibs = (function() { + let $module = {}; + + return $module; +})(); // end of module DafnyStdLibs diff --git a/Source/DafnyRuntime/DafnyRuntimeJs/Makefile b/Source/DafnyRuntime/DafnyRuntimeJs/Makefile index 4728cbd2a47..cef49199e81 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJs/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimeJs/Makefile @@ -5,6 +5,9 @@ DAFNY = dotnet run --project ../../Dafny --no-build -- GENERATED_SYSTEM_MODULE_SOURCE=../obj/systemModulePopulator.js GENERATED_SYSTEM_MODULE_TARGET=DafnyRuntimeSystemModule.js +GENERATED_STDLIBS_SOURCE=obj/DafnyStandardLibraries.js +GENERATED_STDLIBS_TARGET=DafnyStandardLibraries.js + all: check-system-module build-system-module: @@ -15,3 +18,12 @@ check-system-module: build-system-module update-system-module: build-system-module cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET) + +build-stdlibs: + $(DAFNY) translate js --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries + +check-stdlibs: build-stdlibs + diff $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET) + +update-stdlibs: build-stdlibs + cp $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET) diff --git a/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs.py b/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs.py new file mode 100644 index 00000000000..bcdd16d7b57 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs.py @@ -0,0 +1,14 @@ +import sys +from typing import Callable, Any, TypeVar, NamedTuple +from math import floor +from itertools import count + +import module_ +import _dafny +import System_ +import DafnyStdLibs_Functions +import DafnyStdLibs_Relations +import DafnyStdLibs_Wrappers + +# Module: DafnyStdLibs + diff --git a/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Functions.py b/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Functions.py new file mode 100644 index 00000000000..514e6f7049f --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Functions.py @@ -0,0 +1,11 @@ +import sys +from typing import Callable, Any, TypeVar, NamedTuple +from math import floor +from itertools import count + +import module_ +import _dafny +import System_ + +# Module: DafnyStdLibs_Functions + diff --git a/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Relations.py b/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Relations.py new file mode 100644 index 00000000000..9bff4a7ccf3 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Relations.py @@ -0,0 +1,12 @@ +import sys +from typing import Callable, Any, TypeVar, NamedTuple +from math import floor +from itertools import count + +import module_ +import _dafny +import System_ +import DafnyStdLibs_Functions + +# Module: DafnyStdLibs_Relations + diff --git a/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Wrappers.py b/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Wrappers.py new file mode 100644 index 00000000000..7431004c542 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimePython/DafnyStdLibs_Wrappers.py @@ -0,0 +1,288 @@ +import sys +from typing import Callable, Any, TypeVar, NamedTuple +from math import floor +from itertools import count + +import module_ +import _dafny +import System_ +import DafnyStdLibs_Functions +import DafnyStdLibs_Relations + +# Module: DafnyStdLibs_Wrappers + +class default__: + def __init__(self): + pass + + @staticmethod + def Need(condition, error): + if condition: + return OutcomeResult_Pass_k() + elif True: + return OutcomeResult_Fail_k(error) + + +class Option: + @classmethod + def default(cls, ): + return lambda: Option_None() + def __ne__(self, __o: object) -> bool: + return not self.__eq__(__o) + @property + def is_None(self) -> bool: + return isinstance(self, Option_None) + @property + def is_Some(self) -> bool: + return isinstance(self, Option_Some) + def IsFailure(self): + return (self).is_None + + def PropagateFailure(self): + return Option_None() + + def Extract(self): + return (self).value + + def GetOr(self, default): + source0_ = self + if source0_.is_None: + return default + elif True: + d_0___mcc_h0_ = source0_.value + d_1_v_ = d_0___mcc_h0_ + return d_1_v_ + + def ToResult(self, error): + source1_ = self + if source1_.is_None: + return Result_Failure(error) + elif True: + d_2___mcc_h0_ = source1_.value + d_3_v_ = d_2___mcc_h0_ + return Result_Success(d_3_v_) + + def ToOutcome(self, error): + source2_ = self + if source2_.is_None: + return Outcome_Fail(error) + elif True: + d_4___mcc_h0_ = source2_.value + d_5_v_ = d_4___mcc_h0_ + return Outcome_Pass() + + def Map(self, rewrap): + return rewrap(self) + + +class Option_None(Option, NamedTuple('None_', [])): + def __dafnystr__(self) -> str: + return f'Wrappers.Option.None' + def __eq__(self, __o: object) -> bool: + return isinstance(__o, Option_None) + def __hash__(self) -> int: + return super().__hash__() + +class Option_Some(Option, NamedTuple('Some', [('value', Any)])): + def __dafnystr__(self) -> str: + return f'Wrappers.Option.Some({_dafny.string_of(self.value)})' + def __eq__(self, __o: object) -> bool: + return isinstance(__o, Option_Some) and self.value == __o.value + def __hash__(self) -> int: + return super().__hash__() + + +class Result: + @classmethod + def default(cls, default_R): + return lambda: Result_Success(default_R()) + def __ne__(self, __o: object) -> bool: + return not self.__eq__(__o) + @property + def is_Success(self) -> bool: + return isinstance(self, Result_Success) + @property + def is_Failure(self) -> bool: + return isinstance(self, Result_Failure) + def IsFailure(self): + return (self).is_Failure + + def PropagateFailure(self): + return Result_Failure((self).error) + + def Extract(self): + return (self).value + + def GetOr(self, default): + source3_ = self + if source3_.is_Success: + d_6___mcc_h0_ = source3_.value + d_7_s_ = d_6___mcc_h0_ + return d_7_s_ + elif True: + d_8___mcc_h1_ = source3_.error + d_9_e_ = d_8___mcc_h1_ + return default + + def ToOption(self): + source4_ = self + if source4_.is_Success: + d_10___mcc_h0_ = source4_.value + d_11_s_ = d_10___mcc_h0_ + return Option_Some(d_11_s_) + elif True: + d_12___mcc_h1_ = source4_.error + d_13_e_ = d_12___mcc_h1_ + return Option_None() + + def ToOutcome(self): + source5_ = self + if source5_.is_Success: + d_14___mcc_h0_ = source5_.value + d_15_s_ = d_14___mcc_h0_ + return Outcome_Pass() + elif True: + d_16___mcc_h1_ = source5_.error + d_17_e_ = d_16___mcc_h1_ + return Outcome_Fail(d_17_e_) + + def Map(self, rewrap): + return rewrap(self) + + def MapFailure(self, reWrap): + source6_ = self + if source6_.is_Success: + d_18___mcc_h0_ = source6_.value + d_19_s_ = d_18___mcc_h0_ + return Result_Success(d_19_s_) + elif True: + d_20___mcc_h1_ = source6_.error + d_21_e_ = d_20___mcc_h1_ + return Result_Failure(reWrap(d_21_e_)) + + +class Result_Success(Result, NamedTuple('Success', [('value', Any)])): + def __dafnystr__(self) -> str: + return f'Wrappers.Result.Success({_dafny.string_of(self.value)})' + def __eq__(self, __o: object) -> bool: + return isinstance(__o, Result_Success) and self.value == __o.value + def __hash__(self) -> int: + return super().__hash__() + +class Result_Failure(Result, NamedTuple('Failure', [('error', Any)])): + def __dafnystr__(self) -> str: + return f'Wrappers.Result.Failure({_dafny.string_of(self.error)})' + def __eq__(self, __o: object) -> bool: + return isinstance(__o, Result_Failure) and self.error == __o.error + def __hash__(self) -> int: + return super().__hash__() + + +class Outcome: + @classmethod + def default(cls, ): + return lambda: Outcome_Pass() + def __ne__(self, __o: object) -> bool: + return not self.__eq__(__o) + @property + def is_Pass(self) -> bool: + return isinstance(self, Outcome_Pass) + @property + def is_Fail(self) -> bool: + return isinstance(self, Outcome_Fail) + def IsFailure(self): + return (self).is_Fail + + def PropagateFailure(self): + return self + + def ToOption(self, r): + source7_ = self + if source7_.is_Pass: + return Option_Some(r) + elif True: + d_22___mcc_h0_ = source7_.error + d_23_e_ = d_22___mcc_h0_ + return Option_None() + + def ToResult(self, r): + source8_ = self + if source8_.is_Pass: + return Result_Success(r) + elif True: + d_24___mcc_h0_ = source8_.error + d_25_e_ = d_24___mcc_h0_ + return Result_Failure(d_25_e_) + + def Map(self, rewrap): + return rewrap(self) + + def MapFailure(self, rewrap, default): + source9_ = self + if source9_.is_Pass: + return Result_Success(default) + elif True: + d_26___mcc_h0_ = source9_.error + d_27_e_ = d_26___mcc_h0_ + return Result_Failure(rewrap(d_27_e_)) + + @staticmethod + def Need(condition, error): + if condition: + return Outcome_Pass() + elif True: + return Outcome_Fail(error) + + +class Outcome_Pass(Outcome, NamedTuple('Pass', [])): + def __dafnystr__(self) -> str: + return f'Wrappers.Outcome.Pass' + def __eq__(self, __o: object) -> bool: + return isinstance(__o, Outcome_Pass) + def __hash__(self) -> int: + return super().__hash__() + +class Outcome_Fail(Outcome, NamedTuple('Fail', [('error', Any)])): + def __dafnystr__(self) -> str: + return f'Wrappers.Outcome.Fail({_dafny.string_of(self.error)})' + def __eq__(self, __o: object) -> bool: + return isinstance(__o, Outcome_Fail) and self.error == __o.error + def __hash__(self) -> int: + return super().__hash__() + + +class OutcomeResult: + @classmethod + def default(cls, ): + return lambda: OutcomeResult_Pass_k() + def __ne__(self, __o: object) -> bool: + return not self.__eq__(__o) + @property + def is_Pass_k(self) -> bool: + return isinstance(self, OutcomeResult_Pass_k) + @property + def is_Fail_k(self) -> bool: + return isinstance(self, OutcomeResult_Fail_k) + def IsFailure(self): + return (self).is_Fail_k + + def PropagateFailure(self): + return Result_Failure((self).error) + + +class OutcomeResult_Pass_k(OutcomeResult, NamedTuple('Pass_k', [])): + def __dafnystr__(self) -> str: + return f'Wrappers.OutcomeResult.Pass\'' + def __eq__(self, __o: object) -> bool: + return isinstance(__o, OutcomeResult_Pass_k) + def __hash__(self) -> int: + return super().__hash__() + +class OutcomeResult_Fail_k(OutcomeResult, NamedTuple('Fail_k', [('error', Any)])): + def __dafnystr__(self) -> str: + return f'Wrappers.OutcomeResult.Fail\'({_dafny.string_of(self.error)})' + def __eq__(self, __o: object) -> bool: + return isinstance(__o, OutcomeResult_Fail_k) and self.error == __o.error + def __hash__(self) -> int: + return super().__hash__() + diff --git a/Source/DafnyRuntime/DafnyRuntimePython/Makefile b/Source/DafnyRuntime/DafnyRuntimePython/Makefile index a84b57ef0b9..e3e80fac0d2 100644 --- a/Source/DafnyRuntime/DafnyRuntimePython/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimePython/Makefile @@ -5,6 +5,9 @@ DAFNY = dotnet run --project ../../Dafny --no-build -- GENERATED_SYSTEM_MODULE_SOURCE=../obj/systemModulePopulator-py/System_.py GENERATED_SYSTEM_MODULE_TARGET=System_.py +GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-py/DafnyStdLibs +GENERATED_STDLIBS_TARGET=DafnyStdLibs + all: check-system-module build-system-module: @@ -15,3 +18,18 @@ check-system-module: build-system-module update-system-module: build-system-module cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET) + +build-stdlibs: + $(DAFNY) translate py --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries + +check-stdlibs: build-stdlibs + diff $(GENERATED_STDLIBS_SOURCE).py $(GENERATED_STDLIBS_TARGET).py + diff $(GENERATED_STDLIBS_SOURCE)_Functions.py $(GENERATED_STDLIBS_TARGET)_Functions.py + diff $(GENERATED_STDLIBS_SOURCE)_Relations.py $(GENERATED_STDLIBS_TARGET)_Relations.py + diff $(GENERATED_STDLIBS_SOURCE)_Wrappers.py $(GENERATED_STDLIBS_TARGET)_Wrappers.py + +update-stdlibs: build-stdlibs + cp $(GENERATED_STDLIBS_SOURCE).py $(GENERATED_STDLIBS_TARGET).py + cp $(GENERATED_STDLIBS_SOURCE)_Functions.py $(GENERATED_STDLIBS_TARGET)_Functions.py + cp $(GENERATED_STDLIBS_SOURCE)_Relations.py $(GENERATED_STDLIBS_TARGET)_Relations.py + cp $(GENERATED_STDLIBS_SOURCE)_Wrappers.py $(GENERATED_STDLIBS_TARGET)_Wrappers.py diff --git a/Source/DafnyRuntime/DafnyStandardLibraries.cs b/Source/DafnyRuntime/DafnyStandardLibraries.cs new file mode 100644 index 00000000000..e4b03e49a5d --- /dev/null +++ b/Source/DafnyRuntime/DafnyStandardLibraries.cs @@ -0,0 +1,726 @@ +// Dafny program the_program compiled into C# +// To recompile, you will need the libraries +// System.Runtime.Numerics.dll System.Collections.Immutable.dll +// but the 'dotnet' tool in net6.0 should pick those up automatically. +// Optionally, you may want to include compiler switches like +// /debug /nowarn:162,164,168,183,219,436,1717,1718 + +#if ISDAFNYRUNTIMELIB +using System; +using System.Numerics; +using System.Collections; +#endif + +namespace DafnyStdLibs.Functions { + +} // end of namespace DafnyStdLibs.Functions +namespace DafnyStdLibs.Relations { + +} // end of namespace DafnyStdLibs.Relations +namespace DafnyStdLibs.Wrappers { + + public partial class __default { + public static DafnyStdLibs.Wrappers._IOutcomeResult<__E> Need<__E>(bool condition, __E error) + { + if (condition) { + return DafnyStdLibs.Wrappers.OutcomeResult<__E>.create_Pass_k(); + } else { + return DafnyStdLibs.Wrappers.OutcomeResult<__E>.create_Fail_k(error); + } + } + } + + public interface _IOption { + bool is_None { get; } + bool is_Some { get; } + T dtor_value { get; } + _IOption<__T> DowncastClone<__T>(Func converter0); + bool IsFailure(); + DafnyStdLibs.Wrappers._IOption<__U> PropagateFailure<__U>(); + T Extract(); + DafnyStdLibs.Wrappers._IResult ToResult<__E>(__E error); + DafnyStdLibs.Wrappers._IOutcome<__E> ToOutcome<__E>(__E error); + } + public abstract class Option : _IOption { + public Option() { + } + public static DafnyStdLibs.Wrappers._IOption Default() { + return create_None(); + } + public static Dafny.TypeDescriptor> _TypeDescriptor() { + return new Dafny.TypeDescriptor>(DafnyStdLibs.Wrappers.Option.Default()); + } + public static _IOption create_None() { + return new Option_None(); + } + public static _IOption create_Some(T @value) { + return new Option_Some(@value); + } + public bool is_None { get { return this is Option_None; } } + public bool is_Some { get { return this is Option_Some; } } + public T dtor_value { + get { + var d = this; + return ((Option_Some)d)._value; + } + } + public abstract _IOption<__T> DowncastClone<__T>(Func converter0); + public bool IsFailure() { + return (this).is_None; + } + public DafnyStdLibs.Wrappers._IOption<__U> PropagateFailure<__U>() { + return DafnyStdLibs.Wrappers.Option<__U>.create_None(); + } + public T Extract() { + return (this).dtor_value; + } + public static T GetOr(DafnyStdLibs.Wrappers._IOption _this, T @default) { + DafnyStdLibs.Wrappers._IOption _source0 = _this; + if (_source0.is_None) { + return @default; + } else { + T _0___mcc_h0 = _source0.dtor_value; + T _1_v = _0___mcc_h0; + return _1_v; + } + } + public DafnyStdLibs.Wrappers._IResult ToResult<__E>(__E error) { + DafnyStdLibs.Wrappers._IOption _source1 = this; + if (_source1.is_None) { + return DafnyStdLibs.Wrappers.Result.create_Failure(error); + } else { + T _2___mcc_h0 = _source1.dtor_value; + T _3_v = _2___mcc_h0; + return DafnyStdLibs.Wrappers.Result.create_Success(_3_v); + } + } + public DafnyStdLibs.Wrappers._IOutcome<__E> ToOutcome<__E>(__E error) { + DafnyStdLibs.Wrappers._IOption _source2 = this; + if (_source2.is_None) { + return DafnyStdLibs.Wrappers.Outcome<__E>.create_Fail(error); + } else { + T _4___mcc_h0 = _source2.dtor_value; + T _5_v = _4___mcc_h0; + return DafnyStdLibs.Wrappers.Outcome<__E>.create_Pass(); + } + } + public static __FC Map<__FC>(DafnyStdLibs.Wrappers._IOption _this, Func, __FC> rewrap) { + return Dafny.Helpers.Id, __FC>>(rewrap)(_this); + } + } + public class Option_None : Option { + public Option_None() : base() { + } + public override _IOption<__T> DowncastClone<__T>(Func converter0) { + if (this is _IOption<__T> dt) { return dt; } + return new Option_None<__T>(); + } + public override bool Equals(object other) { + var oth = other as DafnyStdLibs.Wrappers.Option_None; + return oth != null; + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 0; + return (int) hash; + } + public override string ToString() { + string s = "Wrappers.Option.None"; + return s; + } + } + public class Option_Some : Option { + public readonly T _value; + public Option_Some(T @value) : base() { + this._value = @value; + } + public override _IOption<__T> DowncastClone<__T>(Func converter0) { + if (this is _IOption<__T> dt) { return dt; } + return new Option_Some<__T>(converter0(_value)); + } + public override bool Equals(object other) { + var oth = other as DafnyStdLibs.Wrappers.Option_Some; + return oth != null && object.Equals(this._value, oth._value); + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 1; + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._value)); + return (int) hash; + } + public override string ToString() { + string s = "Wrappers.Option.Some"; + s += "("; + s += Dafny.Helpers.ToString(this._value); + s += ")"; + return s; + } + } + + public interface _IResult { + bool is_Success { get; } + bool is_Failure { get; } + R dtor_value { get; } + E dtor_error { get; } + _IResult<__R, __E> DowncastClone<__R, __E>(Func converter0, Func converter1); + bool IsFailure(); + DafnyStdLibs.Wrappers._IResult<__U, E> PropagateFailure<__U>(); + R Extract(); + DafnyStdLibs.Wrappers._IOption ToOption(); + DafnyStdLibs.Wrappers._IOutcome ToOutcome(); + } + public abstract class Result : _IResult { + public Result() { + } + public static DafnyStdLibs.Wrappers._IResult Default(R _default_R) { + return create_Success(_default_R); + } + public static Dafny.TypeDescriptor> _TypeDescriptor(Dafny.TypeDescriptor _td_R) { + return new Dafny.TypeDescriptor>(DafnyStdLibs.Wrappers.Result.Default(_td_R.Default())); + } + public static _IResult create_Success(R @value) { + return new Result_Success(@value); + } + public static _IResult create_Failure(E error) { + return new Result_Failure(error); + } + public bool is_Success { get { return this is Result_Success; } } + public bool is_Failure { get { return this is Result_Failure; } } + public R dtor_value { + get { + var d = this; + return ((Result_Success)d)._value; + } + } + public E dtor_error { + get { + var d = this; + return ((Result_Failure)d)._error; + } + } + public abstract _IResult<__R, __E> DowncastClone<__R, __E>(Func converter0, Func converter1); + public bool IsFailure() { + return (this).is_Failure; + } + public DafnyStdLibs.Wrappers._IResult<__U, E> PropagateFailure<__U>() { + return DafnyStdLibs.Wrappers.Result<__U, E>.create_Failure((this).dtor_error); + } + public R Extract() { + return (this).dtor_value; + } + public static R GetOr(DafnyStdLibs.Wrappers._IResult _this, R @default) { + DafnyStdLibs.Wrappers._IResult _source3 = _this; + if (_source3.is_Success) { + R _6___mcc_h0 = _source3.dtor_value; + R _7_s = _6___mcc_h0; + return _7_s; + } else { + E _8___mcc_h1 = _source3.dtor_error; + E _9_e = _8___mcc_h1; + return @default; + } + } + public DafnyStdLibs.Wrappers._IOption ToOption() { + DafnyStdLibs.Wrappers._IResult _source4 = this; + if (_source4.is_Success) { + R _10___mcc_h0 = _source4.dtor_value; + R _11_s = _10___mcc_h0; + return DafnyStdLibs.Wrappers.Option.create_Some(_11_s); + } else { + E _12___mcc_h1 = _source4.dtor_error; + E _13_e = _12___mcc_h1; + return DafnyStdLibs.Wrappers.Option.create_None(); + } + } + public DafnyStdLibs.Wrappers._IOutcome ToOutcome() { + DafnyStdLibs.Wrappers._IResult _source5 = this; + if (_source5.is_Success) { + R _14___mcc_h0 = _source5.dtor_value; + R _15_s = _14___mcc_h0; + return DafnyStdLibs.Wrappers.Outcome.create_Pass(); + } else { + E _16___mcc_h1 = _source5.dtor_error; + E _17_e = _16___mcc_h1; + return DafnyStdLibs.Wrappers.Outcome.create_Fail(_17_e); + } + } + public static __FC Map<__FC>(DafnyStdLibs.Wrappers._IResult _this, Func, __FC> rewrap) { + return Dafny.Helpers.Id, __FC>>(rewrap)(_this); + } + public static DafnyStdLibs.Wrappers._IResult MapFailure<__NewE>(DafnyStdLibs.Wrappers._IResult _this, Func reWrap) { + DafnyStdLibs.Wrappers._IResult _source6 = _this; + if (_source6.is_Success) { + R _18___mcc_h0 = _source6.dtor_value; + R _19_s = _18___mcc_h0; + return DafnyStdLibs.Wrappers.Result.create_Success(_19_s); + } else { + E _20___mcc_h1 = _source6.dtor_error; + E _21_e = _20___mcc_h1; + return DafnyStdLibs.Wrappers.Result.create_Failure(Dafny.Helpers.Id>(reWrap)(_21_e)); + } + } + } + public class Result_Success : Result { + public readonly R _value; + public Result_Success(R @value) : base() { + this._value = @value; + } + public override _IResult<__R, __E> DowncastClone<__R, __E>(Func converter0, Func converter1) { + if (this is _IResult<__R, __E> dt) { return dt; } + return new Result_Success<__R, __E>(converter0(_value)); + } + public override bool Equals(object other) { + var oth = other as DafnyStdLibs.Wrappers.Result_Success; + return oth != null && object.Equals(this._value, oth._value); + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 0; + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._value)); + return (int) hash; + } + public override string ToString() { + string s = "Wrappers.Result.Success"; + s += "("; + s += Dafny.Helpers.ToString(this._value); + s += ")"; + return s; + } + } + public class Result_Failure : Result { + public readonly E _error; + public Result_Failure(E error) : base() { + this._error = error; + } + public override _IResult<__R, __E> DowncastClone<__R, __E>(Func converter0, Func converter1) { + if (this is _IResult<__R, __E> dt) { return dt; } + return new Result_Failure<__R, __E>(converter1(_error)); + } + public override bool Equals(object other) { + var oth = other as DafnyStdLibs.Wrappers.Result_Failure; + return oth != null && object.Equals(this._error, oth._error); + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 1; + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._error)); + return (int) hash; + } + public override string ToString() { + string s = "Wrappers.Result.Failure"; + s += "("; + s += Dafny.Helpers.ToString(this._error); + s += ")"; + return s; + } + } + + public interface _IOutcome { + bool is_Pass { get; } + bool is_Fail { get; } + E dtor_error { get; } + _IOutcome<__E> DowncastClone<__E>(Func converter0); + bool IsFailure(); + DafnyStdLibs.Wrappers._IOutcome PropagateFailure(); + DafnyStdLibs.Wrappers._IOption<__R> ToOption<__R>(__R r); + DafnyStdLibs.Wrappers._IResult<__R, E> ToResult<__R>(__R r); + } + public abstract class Outcome : _IOutcome { + public Outcome() { + } + public static DafnyStdLibs.Wrappers._IOutcome Default() { + return create_Pass(); + } + public static Dafny.TypeDescriptor> _TypeDescriptor() { + return new Dafny.TypeDescriptor>(DafnyStdLibs.Wrappers.Outcome.Default()); + } + public static _IOutcome create_Pass() { + return new Outcome_Pass(); + } + public static _IOutcome create_Fail(E error) { + return new Outcome_Fail(error); + } + public bool is_Pass { get { return this is Outcome_Pass; } } + public bool is_Fail { get { return this is Outcome_Fail; } } + public E dtor_error { + get { + var d = this; + return ((Outcome_Fail)d)._error; + } + } + public abstract _IOutcome<__E> DowncastClone<__E>(Func converter0); + public bool IsFailure() { + return (this).is_Fail; + } + public DafnyStdLibs.Wrappers._IOutcome PropagateFailure() { + return this; + } + public DafnyStdLibs.Wrappers._IOption<__R> ToOption<__R>(__R r) { + DafnyStdLibs.Wrappers._IOutcome _source7 = this; + if (_source7.is_Pass) { + return DafnyStdLibs.Wrappers.Option<__R>.create_Some(r); + } else { + E _22___mcc_h0 = _source7.dtor_error; + E _23_e = _22___mcc_h0; + return DafnyStdLibs.Wrappers.Option<__R>.create_None(); + } + } + public DafnyStdLibs.Wrappers._IResult<__R, E> ToResult<__R>(__R r) { + DafnyStdLibs.Wrappers._IOutcome _source8 = this; + if (_source8.is_Pass) { + return DafnyStdLibs.Wrappers.Result<__R, E>.create_Success(r); + } else { + E _24___mcc_h0 = _source8.dtor_error; + E _25_e = _24___mcc_h0; + return DafnyStdLibs.Wrappers.Result<__R, E>.create_Failure(_25_e); + } + } + public static __FC Map<__FC>(DafnyStdLibs.Wrappers._IOutcome _this, Func, __FC> rewrap) { + return Dafny.Helpers.Id, __FC>>(rewrap)(_this); + } + public static DafnyStdLibs.Wrappers._IResult<__T, __NewE> MapFailure<__T, __NewE>(DafnyStdLibs.Wrappers._IOutcome _this, Func rewrap, __T @default) + { + DafnyStdLibs.Wrappers._IOutcome _source9 = _this; + if (_source9.is_Pass) { + return DafnyStdLibs.Wrappers.Result<__T, __NewE>.create_Success(@default); + } else { + E _26___mcc_h0 = _source9.dtor_error; + E _27_e = _26___mcc_h0; + return DafnyStdLibs.Wrappers.Result<__T, __NewE>.create_Failure(Dafny.Helpers.Id>(rewrap)(_27_e)); + } + } + public static DafnyStdLibs.Wrappers._IOutcome Need(bool condition, E error) + { + if (condition) { + return DafnyStdLibs.Wrappers.Outcome.create_Pass(); + } else { + return DafnyStdLibs.Wrappers.Outcome.create_Fail(error); + } + } + } + public class Outcome_Pass : Outcome { + public Outcome_Pass() : base() { + } + public override _IOutcome<__E> DowncastClone<__E>(Func converter0) { + if (this is _IOutcome<__E> dt) { return dt; } + return new Outcome_Pass<__E>(); + } + public override bool Equals(object other) { + var oth = other as DafnyStdLibs.Wrappers.Outcome_Pass; + return oth != null; + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 0; + return (int) hash; + } + public override string ToString() { + string s = "Wrappers.Outcome.Pass"; + return s; + } + } + public class Outcome_Fail : Outcome { + public readonly E _error; + public Outcome_Fail(E error) : base() { + this._error = error; + } + public override _IOutcome<__E> DowncastClone<__E>(Func converter0) { + if (this is _IOutcome<__E> dt) { return dt; } + return new Outcome_Fail<__E>(converter0(_error)); + } + public override bool Equals(object other) { + var oth = other as DafnyStdLibs.Wrappers.Outcome_Fail; + return oth != null && object.Equals(this._error, oth._error); + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 1; + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._error)); + return (int) hash; + } + public override string ToString() { + string s = "Wrappers.Outcome.Fail"; + s += "("; + s += Dafny.Helpers.ToString(this._error); + s += ")"; + return s; + } + } + + public interface _IOutcomeResult { + bool is_Pass_k { get; } + bool is_Fail_k { get; } + E dtor_error { get; } + _IOutcomeResult<__E> DowncastClone<__E>(Func converter0); + bool IsFailure(); + DafnyStdLibs.Wrappers._IResult<__U, E> PropagateFailure<__U>(); + } + public abstract class OutcomeResult : _IOutcomeResult { + public OutcomeResult() { + } + public static DafnyStdLibs.Wrappers._IOutcomeResult Default() { + return create_Pass_k(); + } + public static Dafny.TypeDescriptor> _TypeDescriptor() { + return new Dafny.TypeDescriptor>(DafnyStdLibs.Wrappers.OutcomeResult.Default()); + } + public static _IOutcomeResult create_Pass_k() { + return new OutcomeResult_Pass_k(); + } + public static _IOutcomeResult create_Fail_k(E error) { + return new OutcomeResult_Fail_k(error); + } + public bool is_Pass_k { get { return this is OutcomeResult_Pass_k; } } + public bool is_Fail_k { get { return this is OutcomeResult_Fail_k; } } + public E dtor_error { + get { + var d = this; + return ((OutcomeResult_Fail_k)d)._error; + } + } + public abstract _IOutcomeResult<__E> DowncastClone<__E>(Func converter0); + public bool IsFailure() { + return (this).is_Fail_k; + } + public DafnyStdLibs.Wrappers._IResult<__U, E> PropagateFailure<__U>() { + return DafnyStdLibs.Wrappers.Result<__U, E>.create_Failure((this).dtor_error); + } + } + public class OutcomeResult_Pass_k : OutcomeResult { + public OutcomeResult_Pass_k() : base() { + } + public override _IOutcomeResult<__E> DowncastClone<__E>(Func converter0) { + if (this is _IOutcomeResult<__E> dt) { return dt; } + return new OutcomeResult_Pass_k<__E>(); + } + public override bool Equals(object other) { + var oth = other as DafnyStdLibs.Wrappers.OutcomeResult_Pass_k; + return oth != null; + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 0; + return (int) hash; + } + public override string ToString() { + string s = "Wrappers.OutcomeResult.Pass'"; + return s; + } + } + public class OutcomeResult_Fail_k : OutcomeResult { + public readonly E _error; + public OutcomeResult_Fail_k(E error) : base() { + this._error = error; + } + public override _IOutcomeResult<__E> DowncastClone<__E>(Func converter0) { + if (this is _IOutcomeResult<__E> dt) { return dt; } + return new OutcomeResult_Fail_k<__E>(converter0(_error)); + } + public override bool Equals(object other) { + var oth = other as DafnyStdLibs.Wrappers.OutcomeResult_Fail_k; + return oth != null && object.Equals(this._error, oth._error); + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 1; + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._error)); + return (int) hash; + } + public override string ToString() { + string s = "Wrappers.OutcomeResult.Fail'"; + s += "("; + s += Dafny.Helpers.ToString(this._error); + s += ")"; + return s; + } + } +} // end of namespace DafnyStdLibs.Wrappers +namespace DafnyStdLibs { + +} // end of namespace DafnyStdLibs +namespace _module { + + public partial class __default { + public static void HasTuples() + { + bool _28_b; + _28_b = true; + _System._ITuple0 _29_has0; + _29_has0 = _System.Tuple0.create(); + _System._ITuple1 _30_has1; + _30_has1 = _System.Tuple1.create(_28_b); + _System._ITuple2 _31_has2; + _31_has2 = _System.Tuple2.create(_28_b, _28_b); + _System._ITuple3 _32_has3; + _32_has3 = _System.Tuple3.create(_28_b, _28_b, _28_b); + _System._ITuple4 _33_has4; + _33_has4 = _System.Tuple4.create(_28_b, _28_b, _28_b, _28_b); + _System._ITuple5 _34_has5; + _34_has5 = _System.Tuple5.create(_28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple6 _35_has6; + _35_has6 = _System.Tuple6.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple7 _36_has7; + _36_has7 = _System.Tuple7.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple8 _37_has8; + _37_has8 = _System.Tuple8.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple9 _38_has9; + _38_has9 = _System.Tuple9.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple10 _39_has10; + _39_has10 = _System.Tuple10.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple11 _40_has11; + _40_has11 = _System.Tuple11.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple12 _41_has12; + _41_has12 = _System.Tuple12.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple13 _42_has13; + _42_has13 = _System.Tuple13.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple14 _43_has14; + _43_has14 = _System.Tuple14.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple15 _44_has15; + _44_has15 = _System.Tuple15.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple16 _45_has16; + _45_has16 = _System.Tuple16.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple17 _46_has17; + _46_has17 = _System.Tuple17.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple18 _47_has18; + _47_has18 = _System.Tuple18.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple19 _48_has19; + _48_has19 = _System.Tuple19.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + _System._ITuple20 _49_has20; + _49_has20 = _System.Tuple20.create(_28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b, _28_b); + } + public static void HasArrows() + { + Func _50_has0; + _50_has0 = ((System.Func)(() => { + return new BigInteger(42); + })); + Func _51_has1; + _51_has1 = ((System.Func)((_52_x1) => { + return new BigInteger(42); + })); + Func _53_has2; + _53_has2 = ((System.Func)((_54_x1, _55_x2) => { + return new BigInteger(42); + })); + Func _56_has3; + _56_has3 = ((System.Func)((_57_x1, _58_x2, _59_x3) => { + return new BigInteger(42); + })); + Func _60_has4; + _60_has4 = ((System.Func)((_61_x1, _62_x2, _63_x3, _64_x4) => { + return new BigInteger(42); + })); + Func _65_has5; + _65_has5 = ((System.Func)((_66_x1, _67_x2, _68_x3, _69_x4, _70_x5) => { + return new BigInteger(42); + })); + Func _71_has6; + _71_has6 = ((System.Func)((_72_x1, _73_x2, _74_x3, _75_x4, _76_x5, _77_x6) => { + return new BigInteger(42); + })); + Func _78_has7; + _78_has7 = ((System.Func)((_79_x1, _80_x2, _81_x3, _82_x4, _83_x5, _84_x6, _85_x7) => { + return new BigInteger(42); + })); + Func _86_has8; + _86_has8 = ((System.Func)((_87_x1, _88_x2, _89_x3, _90_x4, _91_x5, _92_x6, _93_x7, _94_x8) => { + return new BigInteger(42); + })); + Func _95_has9; + _95_has9 = ((System.Func)((_96_x1, _97_x2, _98_x3, _99_x4, _100_x5, _101_x6, _102_x7, _103_x8, _104_x9) => { + return new BigInteger(42); + })); + Func _105_has10; + _105_has10 = ((System.Func)((_106_x1, _107_x2, _108_x3, _109_x4, _110_x5, _111_x6, _112_x7, _113_x8, _114_x9, _115_x10) => { + return new BigInteger(42); + })); + Func _116_has11; + _116_has11 = ((System.Func)((_117_x1, _118_x2, _119_x3, _120_x4, _121_x5, _122_x6, _123_x7, _124_x8, _125_x9, _126_x10, _127_x11) => { + return new BigInteger(42); + })); + Func _128_has12; + _128_has12 = ((System.Func)((_129_x1, _130_x2, _131_x3, _132_x4, _133_x5, _134_x6, _135_x7, _136_x8, _137_x9, _138_x10, _139_x11, _140_x12) => { + return new BigInteger(42); + })); + Func _141_has13; + _141_has13 = ((System.Func)((_142_x1, _143_x2, _144_x3, _145_x4, _146_x5, _147_x6, _148_x7, _149_x8, _150_x9, _151_x10, _152_x11, _153_x12, _154_x13) => { + return new BigInteger(42); + })); + Func _155_has14; + _155_has14 = ((System.Func)((_156_x1, _157_x2, _158_x3, _159_x4, _160_x5, _161_x6, _162_x7, _163_x8, _164_x9, _165_x10, _166_x11, _167_x12, _168_x13, _169_x14) => { + return new BigInteger(42); + })); + Func _170_has15; + _170_has15 = ((System.Func)((_171_x1, _172_x2, _173_x3, _174_x4, _175_x5, _176_x6, _177_x7, _178_x8, _179_x9, _180_x10, _181_x11, _182_x12, _183_x13, _184_x14, _185_x15) => { + return new BigInteger(42); + })); + Func _186_has16; + _186_has16 = ((System.Func)((_187_x1, _188_x2, _189_x3, _190_x4, _191_x5, _192_x6, _193_x7, _194_x8, _195_x9, _196_x10, _197_x11, _198_x12, _199_x13, _200_x14, _201_x15, _202_x16) => { + return new BigInteger(42); + })); + } + public static void HasArrays() + { + byte _203_n; + _203_n = (byte)(0); + bool[] _204_has1; + bool[] _nw0 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _204_has1 = _nw0; + bool[,] _205_has2; + bool[,] _nw1 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _205_has2 = _nw1; + bool[,,] _206_has3; + bool[,,] _nw2 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _206_has3 = _nw2; + bool[,,,] _207_has4; + bool[,,,] _nw3 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _207_has4 = _nw3; + bool[,,,,] _208_has5; + bool[,,,,] _nw4 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _208_has5 = _nw4; + bool[,,,,,] _209_has6; + bool[,,,,,] _nw5 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _209_has6 = _nw5; + bool[,,,,,,] _210_has7; + bool[,,,,,,] _nw6 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _210_has7 = _nw6; + bool[,,,,,,,] _211_has8; + bool[,,,,,,,] _nw7 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _211_has8 = _nw7; + bool[,,,,,,,,] _212_has9; + bool[,,,,,,,,] _nw8 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _212_has9 = _nw8; + bool[,,,,,,,,,] _213_has10; + bool[,,,,,,,,,] _nw9 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _213_has10 = _nw9; + bool[,,,,,,,,,,] _214_has11; + bool[,,,,,,,,,,] _nw10 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _214_has11 = _nw10; + bool[,,,,,,,,,,,] _215_has12; + bool[,,,,,,,,,,,] _nw11 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _215_has12 = _nw11; + bool[,,,,,,,,,,,,] _216_has13; + bool[,,,,,,,,,,,,] _nw12 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _216_has13 = _nw12; + bool[,,,,,,,,,,,,,] _217_has14; + bool[,,,,,,,,,,,,,] _nw13 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _217_has14 = _nw13; + bool[,,,,,,,,,,,,,,] _218_has15; + bool[,,,,,,,,,,,,,,] _nw14 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _218_has15 = _nw14; + bool[,,,,,,,,,,,,,,,] _219_has16; + bool[,,,,,,,,,,,,,,,] _nw15 = new bool[Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit"), Dafny.Helpers.ToIntChecked(_203_n, "array size exceeds memory limit")]; + _219_has16 = _nw15; + } + } + + public partial class @byte { + public static System.Collections.Generic.IEnumerable IntegerRange(BigInteger lo, BigInteger hi) { + for (var j = lo; j < hi; j++) { yield return (byte)j; } + } + private static readonly Dafny.TypeDescriptor _TYPE = new Dafny.TypeDescriptor(0); + public static Dafny.TypeDescriptor _TypeDescriptor() { + return _TYPE; + } + } +} // end of namespace _module diff --git a/Source/DafnyRuntime/Makefile b/Source/DafnyRuntime/Makefile index 1db59c10e66..6ab864c81f5 100644 --- a/Source/DafnyRuntime/Makefile +++ b/Source/DafnyRuntime/Makefile @@ -5,6 +5,9 @@ DAFNY = dotnet run --project ../Dafny --no-build -- GENERATED_SYSTEM_MODULE_SOURCE=obj/systemModulePopulator.cs GENERATED_SYSTEM_MODULE_TARGET=DafnyRuntimeSystemModule.cs +GENERATED_STDLIBS_SOURCE=obj/DafnyStandardLibraries.cs +GENERATED_STDLIBS_TARGET=DafnyStandardLibraries.cs + all: check-system-module build-system-module: @@ -15,4 +18,14 @@ check-system-module: build-system-module update-system-module: build-system-module cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET) + +build-stdlibs: + $(DAFNY) translate cs --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../DafnyStandardLibraries/src/dfyconfig.toml --output:obj/DafnyStandardLibraries.cs + +check-stdlibs: build-stdlibs + diff $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET) + +update-stdlibs: build-stdlibs + cp $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET) + \ No newline at end of file From 77bf47dc8fdcb61d86689b1d27835ec3ceb40a75 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 3 Nov 2023 09:52:12 -0700 Subject: [PATCH 2/7] Generalize Python and Go Makefiles --- Source/DafnyRuntime/DafnyRuntimeGo/Makefile | 17 ++++++----------- Source/DafnyRuntime/DafnyRuntimePython/Makefile | 14 ++++---------- 2 files changed, 10 insertions(+), 21 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/Makefile b/Source/DafnyRuntime/DafnyRuntimeGo/Makefile index cdcc4f7e8f6..472cfd65d0e 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimeGo/Makefile @@ -5,8 +5,8 @@ DAFNY = dotnet run --project ../../Dafny --no-build -- GENERATED_SYSTEM_MODULE_SOURCE=../obj/systemModulePopulator-go/src/System_/System_.go GENERATED_SYSTEM_MODULE_TARGET=System_/System_.go -GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-go/src/DafnyStdLibs -GENERATED_STDLIBS_TARGET=DafnyStdLibs +GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-go/src +GENERATED_STDLIBS_TARGET=. all: check-system-module test @@ -24,15 +24,10 @@ update-system-module: build-system-module build-stdlibs: $(DAFNY) translate go --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries + rm $(GENERATED_STDLIBS_SOURCE)/DafnyStandardLibraries.go check-stdlibs: build-stdlibs - diff $(GENERATED_STDLIBS_SOURCE)/DafnyStdLibs.go $(GENERATED_STDLIBS_TARGET)/DafnyStdLibs.go - diff $(GENERATED_STDLIBS_SOURCE)_Functions/DafnyStdLibs_Functions.go $(GENERATED_STDLIBS_TARGET)_Functions/DafnyStdLibs_Functions.go - diff $(GENERATED_STDLIBS_SOURCE)_Relations/DafnyStdLibs_Relations.go $(GENERATED_STDLIBS_TARGET)_Relations/DafnyStdLibs_Relations.go - diff $(GENERATED_STDLIBS_SOURCE)_Wrappers/DafnyStdLibs_Wrappers.go $(GENERATED_STDLIBS_TARGET)_Wrappers/DafnyStdLibs_Wrappers.go - + diff -r -x Makefile -x System_ -x dafny $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET) + update-stdlibs: build-stdlibs - cp $(GENERATED_STDLIBS_SOURCE)/DafnyStdLibs.go $(GENERATED_STDLIBS_TARGET)/DafnyStdLibs.go - cp $(GENERATED_STDLIBS_SOURCE)_Functions/DafnyStdLibs_Functions.go $(GENERATED_STDLIBS_TARGET)_Functions/DafnyStdLibs_Functions.go - cp $(GENERATED_STDLIBS_SOURCE)_Relations/DafnyStdLibs_Relations.go $(GENERATED_STDLIBS_TARGET)_Relations/DafnyStdLibs_Relations.go - cp $(GENERATED_STDLIBS_SOURCE)_Wrappers/DafnyStdLibs_Wrappers.go $(GENERATED_STDLIBS_TARGET)_Wrappers/DafnyStdLibs_Wrappers.go + rsync -rt $(GENERATED_STDLIBS_SOURCE)/DafnyStdLibs* $(GENERATED_STDLIBS_TARGET) diff --git a/Source/DafnyRuntime/DafnyRuntimePython/Makefile b/Source/DafnyRuntime/DafnyRuntimePython/Makefile index e3e80fac0d2..c73d9f0a776 100644 --- a/Source/DafnyRuntime/DafnyRuntimePython/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimePython/Makefile @@ -5,8 +5,8 @@ DAFNY = dotnet run --project ../../Dafny --no-build -- GENERATED_SYSTEM_MODULE_SOURCE=../obj/systemModulePopulator-py/System_.py GENERATED_SYSTEM_MODULE_TARGET=System_.py -GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-py/DafnyStdLibs -GENERATED_STDLIBS_TARGET=DafnyStdLibs +GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-py +GENERATED_STDLIBS_TARGET=. all: check-system-module @@ -23,13 +23,7 @@ build-stdlibs: $(DAFNY) translate py --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false ../../DafnyStandardLibraries/src/dfyconfig.toml --output:../obj/DafnyStandardLibraries check-stdlibs: build-stdlibs - diff $(GENERATED_STDLIBS_SOURCE).py $(GENERATED_STDLIBS_TARGET).py - diff $(GENERATED_STDLIBS_SOURCE)_Functions.py $(GENERATED_STDLIBS_TARGET)_Functions.py - diff $(GENERATED_STDLIBS_SOURCE)_Relations.py $(GENERATED_STDLIBS_TARGET)_Relations.py - diff $(GENERATED_STDLIBS_SOURCE)_Wrappers.py $(GENERATED_STDLIBS_TARGET)_Wrappers.py + diff -r -x Makefile -x System_.py -x _dafny.py -x __main__.py -x module_.py $(GENERATED_STDLIBS_SOURCE) $(GENERATED_STDLIBS_TARGET) update-stdlibs: build-stdlibs - cp $(GENERATED_STDLIBS_SOURCE).py $(GENERATED_STDLIBS_TARGET).py - cp $(GENERATED_STDLIBS_SOURCE)_Functions.py $(GENERATED_STDLIBS_TARGET)_Functions.py - cp $(GENERATED_STDLIBS_SOURCE)_Relations.py $(GENERATED_STDLIBS_TARGET)_Relations.py - cp $(GENERATED_STDLIBS_SOURCE)_Wrappers.py $(GENERATED_STDLIBS_TARGET)_Wrappers.py + rsync -rt $(GENERATED_STDLIBS_SOURCE)/DafnyStdLibs* $(GENERATED_STDLIBS_TARGET) From 534c2581903860ce7d147ae0e127c99ded8b071e Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 3 Nov 2023 09:58:32 -0700 Subject: [PATCH 3/7] Check generated code in CI --- Source/DafnyRuntime/DafnyRuntimeGo/Makefile | 2 +- Source/DafnyRuntime/DafnyRuntimeJava/Makefile | 2 +- Source/DafnyRuntime/DafnyRuntimeJs/Makefile | 2 +- Source/DafnyRuntime/DafnyRuntimePython/Makefile | 2 +- Source/DafnyRuntime/Makefile | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/Makefile b/Source/DafnyRuntime/DafnyRuntimeGo/Makefile index 472cfd65d0e..9d33cb73edd 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimeGo/Makefile @@ -8,7 +8,7 @@ GENERATED_SYSTEM_MODULE_TARGET=System_/System_.go GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-go/src GENERATED_STDLIBS_TARGET=. -all: check-system-module test +all: check-system-module check-stdlibs test test: cd dafny && GO111MODULE=auto go test diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/Makefile b/Source/DafnyRuntime/DafnyRuntimeJava/Makefile index 5ca3159c53f..70ebe6c7549 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJava/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimeJava/Makefile @@ -11,7 +11,7 @@ GENERATED_DAFNY_MODULE_TARGET=src/main/dafny-generated/dafny GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-java/DafnyStdLibs GENERATED_STDLIBS_TARGET=src/main/dafny-generated/DafnyStdLibs -all: check-system-module test +all: check-system-module check-stdlibs test test: ./gradlew test diff --git a/Source/DafnyRuntime/DafnyRuntimeJs/Makefile b/Source/DafnyRuntime/DafnyRuntimeJs/Makefile index cef49199e81..426491fc698 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJs/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimeJs/Makefile @@ -8,7 +8,7 @@ GENERATED_SYSTEM_MODULE_TARGET=DafnyRuntimeSystemModule.js GENERATED_STDLIBS_SOURCE=obj/DafnyStandardLibraries.js GENERATED_STDLIBS_TARGET=DafnyStandardLibraries.js -all: check-system-module +all: check-system-module check-stdlibs build-system-module: $(DAFNY) translate js --no-verify --use-basename-for-filename --system-module:OmitAllOtherModules ../systemModulePopulator.dfy --output:../obj/systemModulePopulator diff --git a/Source/DafnyRuntime/DafnyRuntimePython/Makefile b/Source/DafnyRuntime/DafnyRuntimePython/Makefile index c73d9f0a776..57ee430ff9b 100644 --- a/Source/DafnyRuntime/DafnyRuntimePython/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimePython/Makefile @@ -8,7 +8,7 @@ GENERATED_SYSTEM_MODULE_TARGET=System_.py GENERATED_STDLIBS_SOURCE=../obj/DafnyStandardLibraries-py GENERATED_STDLIBS_TARGET=. -all: check-system-module +all: check-system-module check-stdlibs build-system-module: $(DAFNY) translate py --no-verify --use-basename-for-filename --system-module:OmitAllOtherModules ../systemModulePopulator.dfy --output:../obj/systemModulePopulator diff --git a/Source/DafnyRuntime/Makefile b/Source/DafnyRuntime/Makefile index 6ab864c81f5..d69798da77a 100644 --- a/Source/DafnyRuntime/Makefile +++ b/Source/DafnyRuntime/Makefile @@ -8,7 +8,7 @@ GENERATED_SYSTEM_MODULE_TARGET=DafnyRuntimeSystemModule.cs GENERATED_STDLIBS_SOURCE=obj/DafnyStandardLibraries.cs GENERATED_STDLIBS_TARGET=DafnyStandardLibraries.cs -all: check-system-module +all: check-system-module check-stdlibs build-system-module: $(DAFNY) translate cs --no-verify --use-basename-for-filename --optimize-erasable-datatype-wrapper:false --system-module:OmitAllOtherModules systemModulePopulator.dfy --output:obj/systemModulePopulator From b02b369595fdabfc11e5dc96447b2db4d537e678 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 3 Nov 2023 13:13:44 -0700 Subject: [PATCH 4/7] =?UTF-8?q?Add=20=E2=80=94default-module,=20unify=20Ma?= =?UTF-8?q?kefile=20testing=20in=20CI?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../{runtime-tests.yml => make-tests.yml} | 46 +++++++------------ Source/DafnyCore/AST/ShouldCompileOrVerify.cs | 10 ++-- .../Compilers/CSharp/Compiler-Csharp.cs | 14 +++--- .../DafnyCore/Compilers/Java/Compiler-java.cs | 4 +- Source/DafnyCore/DafnyOptions.cs | 3 +- Source/DafnyCore/Makefile | 4 +- Source/DafnyCore/Options/CommonOptionBag.cs | 15 ++++-- Source/DafnyCore/Options/DafnyCommands.cs | 3 +- .../DafnyRuntime/DafnyRuntimeDafny/Makefile | 4 +- Source/DafnyRuntime/DafnyRuntimeGo/Makefile | 7 ++- Source/DafnyRuntime/DafnyRuntimeJava/Makefile | 6 +-- Source/DafnyRuntime/DafnyRuntimeJs/Makefile | 6 +-- .../DafnyRuntime/DafnyRuntimePython/Makefile | 6 +-- Source/DafnyRuntime/Makefile | 4 +- 14 files changed, 65 insertions(+), 67 deletions(-) rename .github/workflows/{runtime-tests.yml => make-tests.yml} (54%) diff --git a/.github/workflows/runtime-tests.yml b/.github/workflows/make-tests.yml similarity index 54% rename from .github/workflows/runtime-tests.yml rename to .github/workflows/make-tests.yml index 4152844c4b0..7bfac2c6755 100644 --- a/.github/workflows/runtime-tests.yml +++ b/.github/workflows/make-tests.yml @@ -1,4 +1,4 @@ -name: Build and Test Dafny Runtimes +name: Run Makefile-based tests on: workflow_dispatch: @@ -13,12 +13,23 @@ jobs: check-deep-tests: uses: ./.github/workflows/check-deep-tests-reusable.yml - build: + run-make-tests: needs: check-deep-tests if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' ))) runs-on: ubuntu-latest - + strategy: + matrix: + project: [ + DafnyCore, + DafnyRuntime, + DafnyRuntime/DafnyRuntimeDafny, + DafnyRuntime/DafnyRuntimeGo, + DafnyRuntime/DafnyRuntimeJava, + DafnyRuntime/DafnyRuntimePython, + DafnyRuntime/DafnyRuntimeJs + ] + fail-fast: false steps: - name: Checkout Dafny uses: actions/checkout@v4 @@ -33,32 +44,7 @@ jobs: run: dotnet build Source/Dafny.sln - name: Get Z3 run: make z3-ubuntu - - name: Test DafnyCore + - name: Test ${{ matrix.project }} run: | - cd ./Source/DafnyCore + cd ./Source/${{ matrix.project }} make test - make check-format - - name: Test DafnyRuntime (C#) - run: | - cd ./Source/DafnyRuntime - make all - - name: Test DafnyRuntimeDafny - run: | - cd ./Source/DafnyRuntime/DafnyRuntimeDafny - make all - - name: Test DafnyRuntimeGo - run: | - cd ./Source/DafnyRuntime/DafnyRuntimeGo - make all - - name: Test DafnyRuntimeJava - run: | - cd ./Source/DafnyRuntime/DafnyRuntimeJava - make all - - name: Test DafnyRuntimePython - run: | - cd ./Source/DafnyRuntime/DafnyRuntimePython - make all - - name: Test DafnyRuntimeJs - run: | - cd ./Source/DafnyRuntime/DafnyRuntimeJs - make all diff --git a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs index 103c57e39d6..bad5725c77d 100644 --- a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs +++ b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs @@ -13,17 +13,21 @@ public static bool ShouldCompile(this ModuleDefinition module, CompilationData p } if (module.FullName == "_System") { - return program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.Omit; + return program.Options.SystemModuleTranslationMode != CommonOptionBag.ModuleTranslationMode.Omit; } - if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) { + if (program.Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) { return false; } if (module is DefaultModuleDefinition) { // If things from precompiled files live in the default module, that can cause downstream compilation issues: // https://github.com/dafny-lang/dafny/issues/4009 - return true; + return program.Options.DefaultModuleTranslationMode != CommonOptionBag.ModuleTranslationMode.Omit; + } + if (program.Options.DefaultModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) { + return false; } + return program.UrisToCompile.Contains(module.Tok.Uri); } diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index 4fcbc0dd9c9..a55f28788f5 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs @@ -73,13 +73,13 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { wr.WriteLine("// Optionally, you may want to include compiler switches like"); wr.WriteLine("// /debug /nowarn:162,164,168,183,219,436,1717,1718"); wr.WriteLine(); - if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) { + if (program.Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) { wr.WriteLine("#if ISDAFNYRUNTIMELIB"); } wr.WriteLine("using System;"); wr.WriteLine("using System.Numerics;"); wr.WriteLine("using System.Collections;"); - if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) { + if (program.Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) { wr.WriteLine("#endif"); } Synthesize = ProgramHasMethodsWithAttr(program, "synthesize"); @@ -87,7 +87,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { CsharpSynthesizer.EmitImports(wr); } - if (program.Options.SystemModuleTranslationMode != CommonOptionBag.SystemModuleMode.OmitAllOtherModules) { + if (program.Options.SystemModuleTranslationMode != CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) { EmitDafnySourceAttribute(program, wr); } @@ -131,11 +131,11 @@ void EmitDafnySourceAttribute(Program program, ConcreteSyntaxTree wr) { protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) { switch (Options.SystemModuleTranslationMode) { - case CommonOptionBag.SystemModuleMode.Omit: { + case CommonOptionBag.ModuleTranslationMode.Omit: { CheckCommonSytemModuleLimits(systemModuleManager); break; } - case CommonOptionBag.SystemModuleMode.OmitAllOtherModules: { + case CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules: { CheckSystemModulePopulatedToCommonLimits(systemModuleManager); break; } @@ -150,7 +150,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager // so they don't become duplicates when --include-runtime is used. // See comment at the top of DafnyRuntime.cs. - if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) { + if (Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) { wr.WriteLine("#if ISDAFNYRUNTIMELIB"); } @@ -161,7 +161,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager } EmitFuncExtensions(systemModuleManager, wr); - if (Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) { + if (Options.SystemModuleTranslationMode == CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules) { wr.WriteLine("#endif"); } } diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index a19efbc2831..549c01ef16e 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -312,11 +312,11 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) { switch (Options.SystemModuleTranslationMode) { - case CommonOptionBag.SystemModuleMode.Omit: { + case CommonOptionBag.ModuleTranslationMode.Omit: { CheckCommonSytemModuleLimits(systemModuleManager); return; } - case CommonOptionBag.SystemModuleMode.OmitAllOtherModules: { + case CommonOptionBag.ModuleTranslationMode.OmitAllOtherModules: { CheckSystemModulePopulatedToCommonLimits(systemModuleManager); break; } diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 9e273019b37..b66a8d56d08 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -302,7 +302,8 @@ public enum IncludesModes { public IncludesModes PrintIncludesMode = IncludesModes.None; public int OptimizeResolution = 2; public bool IncludeRuntime = true; - public CommonOptionBag.SystemModuleMode SystemModuleTranslationMode = CommonOptionBag.SystemModuleMode.Omit; + public CommonOptionBag.ModuleTranslationMode SystemModuleTranslationMode = CommonOptionBag.ModuleTranslationMode.Omit; + public CommonOptionBag.ModuleTranslationMode DefaultModuleTranslationMode = CommonOptionBag.ModuleTranslationMode.Include; public bool UseJavadocLikeDocstringRewriter = false; public bool DisableScopes = false; public bool UseStdin = false; diff --git a/Source/DafnyCore/Makefile b/Source/DafnyCore/Makefile index 3efb0477a11..9ab13553c36 100644 --- a/Source/DafnyCore/Makefile +++ b/Source/DafnyCore/Makefile @@ -16,8 +16,10 @@ build-regenerated-from-dafny: chmod u+x DafnyGeneratedFromDafny.sh ./DafnyGeneratedFromDafny.sh $(REGENERATED_FROM_DAFNY) -test: build-regenerated-from-dafny +check-regenerated-from-dafny: build-regenerated-from-dafny (diff $(GENERATED_FROM_DAFNY).cs $(REGENERATED_FROM_DAFNY).cs && (echo 'Consider running ./DafnyGeneratedFromDafny.sh GeneratedFromDafny')) check-format: ../../Scripts/dafny format . --check + +test: check-regenerated-from-dafny check-format diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 87962f5c921..c2ed570ea3b 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -236,15 +236,20 @@ May slow down verification slightly. IsHidden = true }; - public enum SystemModuleMode { + public enum ModuleTranslationMode { Include, Omit, // Used to pre-compile the System module into the runtimes OmitAllOtherModules } - public static readonly Option SystemModule = new("--system-module", () => SystemModuleMode.Omit, - "How to handle the built-in _System module.") { + public static readonly Option SystemModule = new("--system-module", () => ModuleTranslationMode.Omit, + "How to translate the built-in _System module.") { + IsHidden = true + }; + + public static readonly Option DefaultModule = new("--default-module", () => ModuleTranslationMode.Include, + "How to translate the default module.") { IsHidden = true }; @@ -400,6 +405,7 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, DafnyOptions.RegisterLegacyBinding(IncludeRuntimeOption, (options, value) => { options.IncludeRuntime = value; }); DafnyOptions.RegisterLegacyBinding(InternalIncludeRuntimeOptionForExecution, (options, value) => { options.IncludeRuntime = value; }); DafnyOptions.RegisterLegacyBinding(SystemModule, (options, value) => { options.SystemModuleTranslationMode = value; }); + DafnyOptions.RegisterLegacyBinding(DefaultModule, (options, value) => { options.DefaultModuleTranslationMode = value; }); DafnyOptions.RegisterLegacyBinding(UseBaseFileName, (o, f) => o.UseBaseNameForFileName = f); DafnyOptions.RegisterLegacyBinding(UseJavadocLikeDocstringRewriterOption, (options, value) => { options.UseJavadocLikeDocstringRewriter = value; }); @@ -517,7 +523,8 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, UseStandardLibraries, OptimizeErasableDatatypeWrapper, AddCompileSuffix, - SystemModule + SystemModule, + DefaultModule ); } diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 1becf3d1e49..d6f10c15d71 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -53,7 +53,8 @@ static DafnyCommands() { CommonOptionBag.TestAssumptions, DeveloperOptionBag.Bootstrapping, CommonOptionBag.AddCompileSuffix, - CommonOptionBag.SystemModule + CommonOptionBag.SystemModule, + CommonOptionBag.DefaultModule }.Concat(VerificationOptions).ToList(); public static IReadOnlyList