sparklib_light_internal.gpr

with "sparklib_common";

--  This project file is intended for use with reduced runtimes without
--  Ada.Numerics.Big_Numbers or Ada.Finalization units.

project SPARKlib_Light_Internal is

   for Externally_Built use SPARKlib_common.SPARKlib_Installed;

   -- This project is not supposed to be used directly. Instead, copy
   -- sparklib_light.gpr.templ as sparklib_light.gpr in your code and provide
   -- appropriate values for the object directory Object_Dir (so that compilation
   -- and artifacts are generated in directories under your control) and the list
   -- of excluded source files Excluded_Source_Files (so that you only compile and
   -- analyse files from the library that you need).

   case SPARKlib_common.SPARKlib_Installed is
      when "True" =>
         for Source_Dirs use (SPARKlib_Light_Internal'Project_Dir & "/../../include/spark");
      when others =>
         for Source_Dirs use (SPARKlib_Light_Internal'Project_Dir & "/src");
   end case;

   SPARK_Body_Mode := SPARKlib_common.SPARK_Body_Mode;

   package Compiler renames SPARKlib_common.Compiler;

   package Prove renames SPARKlib_common.Prove;

   Common_Default_Switches := SPARKlib_Common.Common_Default_Switches;

   Common_Excluded_Source_Files :=
     ("spark-containers-formal-holders.adb",
      "spark-containers-formal-holders.ads",
      "spark-containers-formal-ordered_maps.adb",
      "spark-containers-formal-ordered_maps.ads",
      "spark-containers-formal-ordered_sets.adb",
      "spark-containers-formal-ordered_sets.ads",
      "spark-containers-formal-unbounded_doubly_linked_lists.adb",
      "spark-containers-formal-unbounded_doubly_linked_lists.ads",
      "spark-containers-formal-unbounded_hashed_maps.adb",
      "spark-containers-formal-unbounded_hashed_maps.ads",
      "spark-containers-formal-unbounded_hashed_sets.adb",
      "spark-containers-formal-unbounded_hashed_sets.ads",
      "spark-containers-formal-unbounded_ordered_maps.adb",
      "spark-containers-formal-unbounded_ordered_maps.ads",
      "spark-containers-formal-unbounded_ordered_sets.adb",
      "spark-containers-formal-unbounded_ordered_sets.ads",
      "spark-containers-formal-unbounded_vectors.adb",
      "spark-containers-formal-unbounded_vectors.ads",
      "spark-containers-formal-vectors.adb",
      "spark-containers-formal-vectors.ads",
      "spark-containers-functional-base.ads",
      "spark-containers-hash.ads",
      "spark-containers-hash.adb",
      "spark-big_integers.ads",
      "spark-big_intervals.ads",
      "spark-big_reals.ads",
      "spark-containers-functional-infinite_sequences.ads",
      "spark-containers-functional-maps.ads",
      "spark-containers-functional-multisets.ads",
      "spark-containers-functional-sets.ads",
      "spark-containers-functional-vectors.ads",
      "spark-containers-types.ads");

   case SPARK_Body_Mode is
      when "On" =>
         for Excluded_Source_Files use Common_Excluded_Source_Files
           & ("spark.ads");
      when "Off" =>
         for Excluded_Source_Files use Common_Excluded_Source_Files
           & ("spark__exec.ads");
   end case;

   package Naming is
      for Spec ("SPARK.Big_Integers") use "spark-big_integers__light.ads";
      for Body ("SPARK.Big_Integers") use "spark-big_integers__light.adb";
      for Spec ("SPARK.Big_Intervals") use "spark-big_intervals__light.ads";
      for Spec ("SPARK.Big_Reals") use "spark-big_reals__light.ads";
      for Body ("SPARK.Big_Reals") use "spark-big_reals__light.adb";

      for Spec ("SPARK.Containers.Types")
         use "spark-containers-types__light.ads";
      for Spec ("SPARK.Containers.Functional.Base")
         use "spark-containers-functional-base__light.ads";
      for Spec ("SPARK.Containers.Functional.Infinite_Sequences")
         use "spark-containers-functional-infinite_sequences__light.ads";
      for Spec ("SPARK.Containers.Functional.Maps")
         use "spark-containers-functional-maps__light.ads";
      for Spec ("SPARK.Containers.Functional.Multisets")
         use "spark-containers-functional-multisets__light.ads";
      for Spec ("SPARK.Containers.Functional.Sets")
         use "spark-containers-functional-sets__light.ads";
      for Spec ("SPARK.Containers.Functional.Vectors")
         use "spark-containers-functional-vectors__light.ads";
      case SPARK_Body_Mode is
         when "On" =>
            for Spec ("SPARK") use "spark__exec.ads";
         when "Off" => null;
      end case;
   end Naming;

end SPARKlib_Light_Internal;