From patchwork Mon Jul 4 07:50:07 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 55668 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id C9AEF383A314 for ; Mon, 4 Jul 2022 07:51:33 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org C9AEF383A314 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1656921093; bh=ry//tf5Y2LxihrEkAEDUR5l9smZtfEuFhn0tAptuUfw=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=jWy0RC7GOB+v3gfCOCJ/5Wuv7PK1B8yO31N5ro2QHS+wbj+y67KBM/WZvbULLoTmt QwRnV5P7VZn1mKXADc3JF42lS7F8X+I2bAC9g3W6N1r2gZkW8O0TzVlVmX0e9onS7e 3PkIgzJObRRGGJ7ja5XiySB4k3NtF3pyFCDtSW/A= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-ej1-x62e.google.com (mail-ej1-x62e.google.com [IPv6:2a00:1450:4864:20::62e]) by sourceware.org (Postfix) with ESMTPS id 96D91385414C for ; Mon, 4 Jul 2022 07:50:09 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 96D91385414C Received: by mail-ej1-x62e.google.com with SMTP id u12so15203049eja.8 for ; Mon, 04 Jul 2022 00:50:09 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=ry//tf5Y2LxihrEkAEDUR5l9smZtfEuFhn0tAptuUfw=; b=k5RzlxNPqz7vShEu5T9cetG/kP2DCNMjT+C9Mez0WXCeDbLaEixXk0W5Z/b5/18SQ9 9JMAgBFKvFT4OJEu21Mdm1Q/h1yXRzyXVpGzTrHCFSMbeZBAdpjJjzQdFezKRxJpT1jK MdQPSGC5UiqIRJe2DkHQFBSqkE5if2lcHvnxqLmoaualOf6wjaN6xpvZVFHEGzBaGLuK r3b++RTA0kSWVHqHrNGQxl92ApDDryvU4ePa6SDnvhfl2ABfNFxnH0kiIq3mACifACRu rqZwZHCHVw2/Yi+cmWi9Yc/MaktT0QL1RjsA8NlOzYzZ6ATuzaytridqQtdjitx9HheK JMpA== X-Gm-Message-State: AJIora8aoL7WaCI8CjOAmPEdd7S4MEccWHFSI3/MrAYEsqnh7OkUq4Cq jtVGnblwcVTkC0EAah/VlMe5J3PwBPLDng== X-Google-Smtp-Source: AGRyM1vd3dNROPshSgkharbCEJNo1fHqo/fLMEUjg1G34zgYjWOVqO2/0eQZkDO93iKb8ip+9M8c/Q== X-Received: by 2002:a17:906:730b:b0:726:c967:8d17 with SMTP id di11-20020a170906730b00b00726c9678d17mr27530188ejc.763.1656921008444; Mon, 04 Jul 2022 00:50:08 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id fi18-20020a056402551200b0043a43fcde13sm2011669edb.13.2022.07.04.00.50.07 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 04 Jul 2022 00:50:07 -0700 (PDT) Date: Mon, 4 Jul 2022 07:50:07 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Update the documentation of functional containers Message-ID: <20220704075007.GA99018@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.2 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Claire Dross Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" Functional containers are now controlled. Update the documentation accordingly. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * doc/gnat_rm/the_gnat_library.rst: Functional vectors, sets, and maps are now controlled. * gnat_rm.texi: Regenerate. diff --git a/gcc/ada/doc/gnat_rm/the_gnat_library.rst b/gcc/ada/doc/gnat_rm/the_gnat_library.rst --- a/gcc/ada/doc/gnat_rm/the_gnat_library.rst +++ b/gcc/ada/doc/gnat_rm/the_gnat_library.rst @@ -285,17 +285,16 @@ specification of this unit is compatible with SPARK 2014. .. index:: Functional sets This child of ``Ada.Containers`` defines immutable sets. These containers are -unbounded and may contain indefinite elements. Furthermore, to be usable in -every context, they are neither controlled nor limited. As they are functional, -that is, no primitives are provided which would allow modifying an existing -container, these containers can still be used safely. +unbounded and may contain indefinite elements. Their API features functions +creating new containers from existing ones. To remain reasonably efficient, +their implementation involves sharing between data-structures. As they are +functional, that is, no primitives are provided which would allow modifying an +existing container, these containers can still be used safely. -Their API features functions creating new containers from existing ones. -As a consequence, these containers are highly inefficient. They are also -memory consuming, as the allocated memory is not reclaimed when the container -is no longer referenced. Thus, they should in general be used in ghost code -and annotations, so that they can be removed from the final executable. The -specification of this unit is compatible with SPARK 2014. +These containers are controlled so that the allocated memory can be reclaimed +when the container is no longer referenced. Thus, they cannot directly be used +in contexts where controlled types are not supported. +The specification of this unit is compatible with SPARK 2014. .. _`Ada.Containers.Functional_Maps_(a-cofuma.ads)`: @@ -307,17 +306,16 @@ specification of this unit is compatible with SPARK 2014. .. index:: Functional maps This child of ``Ada.Containers`` defines immutable maps. These containers are -unbounded and may contain indefinite elements. Furthermore, to be usable in -every context, they are neither controlled nor limited. As they are functional, -that is, no primitives are provided which would allow modifying an existing -container, these containers can still be used safely. - -Their API features functions creating new containers from existing ones. -As a consequence, these containers are highly inefficient. They are also -memory consuming, as the allocated memory is not reclaimed when the container -is no longer referenced. Thus, they should in general be used in ghost code -and annotations, so that they can be removed from the final executable. The -specification of this unit is compatible with SPARK 2014. +unbounded and may contain indefinite elements. Their API features functions +creating new containers from existing ones. To remain reasonably efficient, +their implementation involves sharing between data-structures. As they are +functional, that is, no primitives are provided which would allow modifying an +existing container, these containers can still be used safely. + +These containers are controlled so that the allocated memory can be reclaimed +when the container is no longer referenced. Thus, they cannot directly be used +in contexts where controlled types are not supported. +The specification of this unit is compatible with SPARK 2014. .. _`Ada.Containers.Bounded_Holders_(a-coboho.ads)`: diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -23520,17 +23520,16 @@ specification of this unit is compatible with SPARK 2014. @geindex Functional sets This child of @code{Ada.Containers} defines immutable sets. These containers are -unbounded and may contain indefinite elements. Furthermore, to be usable in -every context, they are neither controlled nor limited. As they are functional, -that is, no primitives are provided which would allow modifying an existing -container, these containers can still be used safely. +unbounded and may contain indefinite elements. Their API features functions +creating new containers from existing ones. To remain reasonably efficient, +their implementation involves sharing between data-structures. As they are +functional, that is, no primitives are provided which would allow modifying an +existing container, these containers can still be used safely. -Their API features functions creating new containers from existing ones. -As a consequence, these containers are highly inefficient. They are also -memory consuming, as the allocated memory is not reclaimed when the container -is no longer referenced. Thus, they should in general be used in ghost code -and annotations, so that they can be removed from the final executable. The -specification of this unit is compatible with SPARK 2014. +These containers are controlled so that the allocated memory can be reclaimed +when the container is no longer referenced. Thus, they cannot directly be used +in contexts where controlled types are not supported. +The specification of this unit is compatible with SPARK 2014. @node Ada Containers Functional_Maps a-cofuma ads,Ada Containers Bounded_Holders a-coboho ads,Ada Containers Functional_Sets a-cofuse ads,The GNAT Library @anchor{gnat_rm/the_gnat_library ada-containers-functional-maps-a-cofuma-ads}@anchor{2f4}@anchor{gnat_rm/the_gnat_library id16}@anchor{2f5} @@ -23542,17 +23541,16 @@ specification of this unit is compatible with SPARK 2014. @geindex Functional maps This child of @code{Ada.Containers} defines immutable maps. These containers are -unbounded and may contain indefinite elements. Furthermore, to be usable in -every context, they are neither controlled nor limited. As they are functional, -that is, no primitives are provided which would allow modifying an existing -container, these containers can still be used safely. - -Their API features functions creating new containers from existing ones. -As a consequence, these containers are highly inefficient. They are also -memory consuming, as the allocated memory is not reclaimed when the container -is no longer referenced. Thus, they should in general be used in ghost code -and annotations, so that they can be removed from the final executable. The -specification of this unit is compatible with SPARK 2014. +unbounded and may contain indefinite elements. Their API features functions +creating new containers from existing ones. To remain reasonably efficient, +their implementation involves sharing between data-structures. As they are +functional, that is, no primitives are provided which would allow modifying an +existing container, these containers can still be used safely. + +These containers are controlled so that the allocated memory can be reclaimed +when the container is no longer referenced. Thus, they cannot directly be used +in contexts where controlled types are not supported. +The specification of this unit is compatible with SPARK 2014. @node Ada Containers Bounded_Holders a-coboho ads,Ada Command_Line Environment a-colien ads,Ada Containers Functional_Maps a-cofuma ads,The GNAT Library @anchor{gnat_rm/the_gnat_library ada-containers-bounded-holders-a-coboho-ads}@anchor{2f6}@anchor{gnat_rm/the_gnat_library id17}@anchor{2f7}