Add optimizable bulk operations to Actions, native and external SetReaders

Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs

@@ -57,7 +57,9 @@ public CppCodeGenerator(DafnyOptions options, ErrorReporter reporter, ReadOnlyCo
       Feature.UnicodeChars,
       Feature.ConvertingValuesToStrings,
       Feature.BuiltinsInRuntime,
-      Feature.RuntimeCoverageReport
+      Feature.RuntimeCoverageReport,
+      Feature.StandardLibraries,
+      Feature.StandardLibrariesActionsExterns
     };
 
     private List<DatatypeDecl> datatypeDecls = [];

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -107,7 +107,9 @@ public void AddUnsupportedFeature(IOrigin tok, Feature feature) {
       Feature.ForLoops,
       Feature.Traits,
       Feature.RuntimeCoverageReport,
-      Feature.NonNativeNewtypes
+      Feature.NonNativeNewtypes,
+      Feature.StandardLibraries,
+      Feature.StandardLibrariesActionsExterns
     };
 
     private readonly List<string> Imports = [DafnyDefaultModule];

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -48,7 +48,8 @@ public GoCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(opti
       Feature.ExternalConstructors,
       Feature.SubsetTypeTests,
       Feature.AllUnderscoreExternalModuleNames,
-      Feature.RuntimeCoverageReport
+      Feature.RuntimeCoverageReport,
+      Feature.StandardLibrariesActionsExterns
     };
 
     public override string ModuleSeparator => "_";

Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs

@@ -27,7 +27,8 @@ public JavaScriptCodeGenerator(DafnyOptions options, ErrorReporter reporter) : b
       Feature.ExternalConstructors,
       Feature.SubsetTypeTests,
       Feature.SeparateCompilation,
-      Feature.RuntimeCoverageReport
+      Feature.RuntimeCoverageReport,
+      Feature.StandardLibrariesActionsExterns
     };
 
     public override string ModuleSeparator => "_";

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -36,7 +36,8 @@ public PythonCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(
     public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
       Feature.SubsetTypeTests,
       Feature.MethodSynthesis,
-      Feature.RuntimeCoverageReport
+      Feature.RuntimeCoverageReport,
+      Feature.StandardLibrariesActionsExterns
     };
 
     public override string ModuleSeparator => "_";

Source/DafnyCore/Feature.cs

@@ -187,7 +187,13 @@ and where at least one variable has potentially infinite bounds.
   BuiltinsInRuntime,
 
   [FeatureDescription("Execution coverage report", "sec-dafny-test")]
-  RuntimeCoverageReport
+  RuntimeCoverageReport,
+
+  [FeatureDescription("Standard libraries", "sec-dafny-standard-libraries")]
+  StandardLibraries,
+
+  [FeatureDescription("Standard library ActionsExterns", "sec-dafny-standard-libraries")]
+  StandardLibrariesActionsExterns
 }
 
 public class UnsupportedFeatureException : Exception {

Source/DafnyCore/GeneratedFromDafny/DCOMP.cs

@@ -1971,7 +1971,7 @@ public RAST._IImplMember GenMethod(DAST._IMethod m, bool forTrait, DAST._IType e
         {
           if (_source0.is_UserDefined) {
             DAST._IResolvedType _11_r = _source0.dtor_resolved;
-            _10_instanceType = DAST.Type.create_UserDefined(Dafny.Helpers.Let<DAST._IResolvedType, DAST._IResolvedType>(_11_r, _pat_let71_0 => Dafny.Helpers.Let<DAST._IResolvedType, DAST._IResolvedType>(_pat_let71_0, _12_dt__update__tmp_h0 => Dafny.Helpers.Let<Dafny.ISequence<DAST._IType>, DAST._IResolvedType>(_pat_let_tv0, _pat_let72_0 => Dafny.Helpers.Let<Dafny.ISequence<DAST._IType>, DAST._IResolvedType>(_pat_let72_0, _13_dt__update_htypeArgs_h0 => DAST.ResolvedType.create((_12_dt__update__tmp_h0).dtor_path, _13_dt__update_htypeArgs_h0, (_12_dt__update__tmp_h0).dtor_kind, (_12_dt__update__tmp_h0).dtor_attributes, (_12_dt__update__tmp_h0).dtor_properMethods, (_12_dt__update__tmp_h0).dtor_extendedTypes))))));
+            _10_instanceType = DAST.Type.create_UserDefined(Dafny.Helpers.Let<DAST._IResolvedType, DAST._IResolvedType>(_11_r, _pat_let72_0 => Dafny.Helpers.Let<DAST._IResolvedType, DAST._IResolvedType>(_pat_let72_0, _12_dt__update__tmp_h0 => Dafny.Helpers.Let<Dafny.ISequence<DAST._IType>, DAST._IResolvedType>(_pat_let_tv0, _pat_let73_0 => Dafny.Helpers.Let<Dafny.ISequence<DAST._IType>, DAST._IResolvedType>(_pat_let73_0, _13_dt__update_htypeArgs_h0 => DAST.ResolvedType.create((_12_dt__update__tmp_h0).dtor_path, _13_dt__update_htypeArgs_h0, (_12_dt__update__tmp_h0).dtor_kind, (_12_dt__update__tmp_h0).dtor_attributes, (_12_dt__update__tmp_h0).dtor_properMethods, (_12_dt__update__tmp_h0).dtor_extendedTypes))))));
             goto after_match0;
           }
         }
@@ -2998,7 +2998,7 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv
               Dafny.ISequence<Dafny.Rune> _80_param;
               _80_param = ((_74_oldEnv).dtor_names).Select(_79_paramI);
               if ((_80_param).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_accumulator"))) {
-                goto continue_3;
+                goto continue_4;
               }
               RAST._IExpr _81_paramInit;
               Defs._IOwnership _82___v43;
@@ -3020,9 +3020,9 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv
                 newEnv = (newEnv).AddAssigned(_84_recVar, _85_declaredType);
               }
               _78_loopBegin = (_78_loopBegin).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _80_param, Std.Wrappers.Option<RAST._IType>.create_None(), Std.Wrappers.Option<RAST._IExpr>.create_Some(RAST.Expr.create_Identifier(_84_recVar))));
-            continue_3: ;
+            continue_4: ;
             }
-          after_3: ;
+          after_4: ;
             RAST._IExpr _86_bodyExpr;
             Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _87_bodyIdents;
             Defs._IEnvironment _88_bodyEnv;
@@ -4279,7 +4279,7 @@ public bool SameTypesButDifferentTypeParameters(DAST._IType fromType, RAST._ITyp
           var arr19 = new Std.Wrappers._IResult<RAST._IExpr, _System._ITuple5<DAST._IType, RAST._IType, DAST._IType, RAST._IType, Dafny.IMap<_System._ITuple2<RAST._IType, RAST._IType>,RAST._IExpr>>>[Dafny.Helpers.ToIntChecked(dim19, "array size exceeds memory limit")];
           for (int i19 = 0; i19 < dim19; i19++) {
             var _13_j = (BigInteger) i19;
-            arr19[(int)(_13_j)] = Dafny.Helpers.Let<BigInteger, Std.Wrappers._IResult<RAST._IExpr, _System._ITuple5<DAST._IType, RAST._IType, DAST._IType, RAST._IType, Dafny.IMap<_System._ITuple2<RAST._IType, RAST._IType>,RAST._IExpr>>>>((_6_indices).Select(_13_j), _pat_let73_0 => Dafny.Helpers.Let<BigInteger, Std.Wrappers._IResult<RAST._IExpr, _System._ITuple5<DAST._IType, RAST._IType, DAST._IType, RAST._IType, Dafny.IMap<_System._ITuple2<RAST._IType, RAST._IType>,RAST._IExpr>>>>(_pat_let73_0, _14_i => (this).UpcastConversionLambda((((_pat_let_tv0).dtor_resolved).dtor_typeArgs).Select(_14_i), ((_pat_let_tv1).dtor_arguments).Select(_14_i), (((_pat_let_tv2).dtor_resolved).dtor_typeArgs).Select(_14_i), ((_pat_let_tv3).dtor_arguments).Select(_14_i), _pat_let_tv4)));
+            arr19[(int)(_13_j)] = Dafny.Helpers.Let<BigInteger, Std.Wrappers._IResult<RAST._IExpr, _System._ITuple5<DAST._IType, RAST._IType, DAST._IType, RAST._IType, Dafny.IMap<_System._ITuple2<RAST._IType, RAST._IType>,RAST._IExpr>>>>((_6_indices).Select(_13_j), _pat_let74_0 => Dafny.Helpers.Let<BigInteger, Std.Wrappers._IResult<RAST._IExpr, _System._ITuple5<DAST._IType, RAST._IType, DAST._IType, RAST._IType, Dafny.IMap<_System._ITuple2<RAST._IType, RAST._IType>,RAST._IExpr>>>>(_pat_let74_0, _14_i => (this).UpcastConversionLambda((((_pat_let_tv0).dtor_resolved).dtor_typeArgs).Select(_14_i), ((_pat_let_tv1).dtor_arguments).Select(_14_i), (((_pat_let_tv2).dtor_resolved).dtor_typeArgs).Select(_14_i), ((_pat_let_tv3).dtor_arguments).Select(_14_i), _pat_let_tv4)));
           }
           return Dafny.Sequence<Std.Wrappers._IResult<RAST._IExpr, _System._ITuple5<DAST._IType, RAST._IType, DAST._IType, RAST._IType, Dafny.IMap<_System._ITuple2<RAST._IType, RAST._IType>,RAST._IExpr>>>>.FromArray(arr19);
         }))());
@@ -7120,7 +7120,7 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir
             for (BigInteger _428_i = BigInteger.Zero; _428_i < _hi16; _428_i++) {
               var _pat_let_tv0 = _425_extraAttributes;
               var _pat_let_tv1 = _426_formals;
-              _427_newFormals = Dafny.Sequence<DAST._IFormal>.Concat(_427_newFormals, Dafny.Sequence<DAST._IFormal>.FromElements(Dafny.Helpers.Let<DAST._IFormal, DAST._IFormal>((_426_formals).Select(_428_i), _pat_let74_0 => Dafny.Helpers.Let<DAST._IFormal, DAST._IFormal>(_pat_let74_0, _429_dt__update__tmp_h0 => Dafny.Helpers.Let<Dafny.ISequence<DAST._IAttribute>, DAST._IFormal>(Dafny.Sequence<DAST._IAttribute>.Concat(_pat_let_tv0, ((_pat_let_tv1).Select(_428_i)).dtor_attributes), _pat_let75_0 => Dafny.Helpers.Let<Dafny.ISequence<DAST._IAttribute>, DAST._IFormal>(_pat_let75_0, _430_dt__update_hattributes_h0 => DAST.Formal.create((_429_dt__update__tmp_h0).dtor_name, (_429_dt__update__tmp_h0).dtor_typ, _430_dt__update_hattributes_h0)))))));
+              _427_newFormals = Dafny.Sequence<DAST._IFormal>.Concat(_427_newFormals, Dafny.Sequence<DAST._IFormal>.FromElements(Dafny.Helpers.Let<DAST._IFormal, DAST._IFormal>((_426_formals).Select(_428_i), _pat_let75_0 => Dafny.Helpers.Let<DAST._IFormal, DAST._IFormal>(_pat_let75_0, _429_dt__update__tmp_h0 => Dafny.Helpers.Let<Dafny.ISequence<DAST._IAttribute>, DAST._IFormal>(Dafny.Sequence<DAST._IAttribute>.Concat(_pat_let_tv0, ((_pat_let_tv1).Select(_428_i)).dtor_attributes), _pat_let76_0 => Dafny.Helpers.Let<Dafny.ISequence<DAST._IAttribute>, DAST._IFormal>(_pat_let76_0, _430_dt__update_hattributes_h0 => DAST.Formal.create((_429_dt__update__tmp_h0).dtor_name, (_429_dt__update__tmp_h0).dtor_typ, _430_dt__update_hattributes_h0)))))));
             }
             DAST._IExpression _431_newLambda;
             DAST._IExpression _432_dt__update__tmp_h1 = _420_lambda;

Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs

@@ -258,7 +258,7 @@ public RAST._IMod ToRust() {
           var arr16 = new RAST._IModDecl[Dafny.Helpers.ToIntChecked(dim16, "array size exceeds memory limit")];
           for (int i16 = 0; i16 < dim16; i16++) {
             var _4_i = (BigInteger) i16;
-            arr16[(int)(_4_i)] = Dafny.Helpers.Let<Dafny.ISequence<Dafny.Rune>, RAST._IModDecl>((_0_keysWithContent).Select(_4_i), _pat_let69_0 => Dafny.Helpers.Let<Dafny.ISequence<Dafny.Rune>, RAST._IModDecl>(_pat_let69_0, _5_moduleName => Dafny.Helpers.Let<RAST._IMod, RAST._IModDecl>((Dafny.Map<Dafny.ISequence<Dafny.Rune>, DafnyCompilerRustUtils._IGatheringModule>.Select(((this).dtor_submodules).dtor_values,_5_moduleName)).ToRust(), _pat_let70_0 => Dafny.Helpers.Let<RAST._IMod, RAST._IModDecl>(_pat_let70_0, _6_submodule => RAST.ModDecl.create_ModDecl(_6_submodule)))));
+            arr16[(int)(_4_i)] = Dafny.Helpers.Let<Dafny.ISequence<Dafny.Rune>, RAST._IModDecl>((_0_keysWithContent).Select(_4_i), _pat_let70_0 => Dafny.Helpers.Let<Dafny.ISequence<Dafny.Rune>, RAST._IModDecl>(_pat_let70_0, _5_moduleName => Dafny.Helpers.Let<RAST._IMod, RAST._IModDecl>((Dafny.Map<Dafny.ISequence<Dafny.Rune>, DafnyCompilerRustUtils._IGatheringModule>.Select(((this).dtor_submodules).dtor_values,_5_moduleName)).ToRust(), _pat_let71_0 => Dafny.Helpers.Let<RAST._IMod, RAST._IModDecl>(_pat_let71_0, _6_submodule => RAST.ModDecl.create_ModDecl(_6_submodule)))));
           }
           return Dafny.Sequence<RAST._IModDecl>.FromArray(arr16);
         }))());

Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs

@@ -35,7 +35,7 @@ public static RAST._IMod applyPrefix(RAST._IMod mod, RAST._IPath SelfPath)
       }
     }
     public static __T UniqueElementOf<__T>(Dafny.ISet<__T> s) {
-      return Dafny.Helpers.Let<int, __T>(0, _let_dummy_68 =>  {
+      return Dafny.Helpers.Let<int, __T>(0, _let_dummy_69 =>  {
         __T _0_e = default(__T);
         foreach (__T _assign_such_that_0 in (s).Elements) {
           _0_e = (__T)_assign_such_that_0;