Add flake

.gitea/workflows/verify.yaml

@@ -26,12 +26,21 @@ jobs:
         if [ "$(uname -m)" == "x86_64" ]; then
           wget -O alr.zip https://github.com/alire-project/alire/releases/download/v2.0.2/alr-2.0.2-bin-x86_64-linux.zip
           unzip alr.zip
+          mv bin/alr /bin/alr
         else
           wget -O alr https://git.nichkara.eu/yannickreiss/alire/raw/branch/main/aarch64/alr
           mv alr /bin/alr
         fi
         chmod +x /bin/alr
+        /bin/alr index --update-all
+        /bin/alr install gnatprove
 
     - name: build project
       run: |
         /bin/alr -n build
+
+    - name: project verify
+      run: |
+        /bin/alr gnatprove --version
+        /bin/alr gnatprove --help
+        /bin/alr gnatprove -v

adj2con.py

@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+"""
+File: adj2con.py
+Author: Nina Chloe Kassandra Reiß <nina.reiss@nickr.eu>
+Created on: Sa 18. Jul 11:30:03 CEST 2026
+Description: Turn adjacency matrices into boolean connectivity matrix
+"""
+adjacency = [[1, 0, 1, 0, 0, 0], [0, 0, 0, 0, 1, 0], [1, 0, 0, 0, 0, 0],
+             [0, 0, 0, 0, 1, 0], [0, 0, 0, 1, 0, 0], [0, 0, 0, 1, 1, 0]]
+
+
+def warshall(adj):
+    n = len(adj)
+
+    # Kopie erzeugen
+    R = [row[:] for row in adj]
+
+    # Jeder Knoten ist von sich selbst erreichbar
+    for i in range(n):
+        R[i][i] = 1
+
+    for k in range(n):
+        for i in range(n):
+            for j in range(n):
+                R[i][j] = R[i][j] or (R[i][k] and R[k][j])
+
+    return R
+
+
+print(warshall(adjacency))

alire.toml

@@ -8,3 +8,6 @@ maintainers-logins = ["nichkara"]
 licenses = "MIT"
 website = ""
 tags = ["routing", "geo", "coordinates", "geography", "graph", "pathfinding", "spark"]
+
+[[depends-on]]
+gnatprove = "^15.1.0"

flake.nix

@@ -0,0 +1,61 @@
+{
+  description = "Ada development environment with Alire";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-26.05";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+
+  outputs =
+    {
+      self,
+      nixpkgs,
+      flake-utils,
+    }:
+    flake-utils.lib.eachDefaultSystem (
+      system:
+      let
+        pkgs = import nixpkgs {
+          inherit system;
+        };
+      in
+      {
+        devShells.default = pkgs.mkShell {
+          packages = with pkgs; [
+            # Ada
+            gnat
+            gprbuild
+            alire
+
+            # Toolchain
+            gcc
+            binutils
+
+            # Build Tools
+            gnumake
+            cmake
+            pkg-config
+
+            # Debugging
+            gdb
+
+            # Utilities
+            git
+            which
+            file
+          ];
+
+          shellHook = ''
+            export ADA_PROJECT_PATH="$PWD''${ADA_PROJECT_PATH:+:$ADA_PROJECT_PATH}"
+
+            echo "Ada + Alire development shell"
+            echo "--------------------------------"
+
+            command -v alr >/dev/null && alr --version
+            command -v gnat >/dev/null && gnat --version | head -n1
+            command -v gprbuild >/dev/null && gprbuild --version | head -n1
+          '';
+        };
+      }
+    );
+}

src/grl-coordinates.adb

@@ -1,3 +1,5 @@
+with Ada.Numerics.Elementary_Functions; use Ada.Numerics.Elementary_Functions;
+
 package body Grl.Coordinates is
 
    function To_DD (DM_Base : Coordinate) return Coordinate is
@@ -5,20 +7,71 @@ package body Grl.Coordinates is
    begin
 
       case DM_Base.Form is
-         when Relative => null;
+         when Relative =>
-         when DD_Fine => null;
+            null;
-         when DD => DD_Target := DM_Base;
+         when DD_Fine =>
+            null;
+         when DD =>
+            DD_Target := DM_Base;
          when DDM =>
             if DM_Base.DDM.Cardinal_Lat = North then
                DD_Target.DD.Latitude :=
-                  DD_Meter_Scale_Lat (DM_Base.DDM.Degree_Lat)
+                 DD_Meter_Scale_Lat (DM_Base.DDM.Degree_Lat) +
-                  +
+                 DD_Meter_Scale_Lat (DM_Base.DDM.Minutes_Lat / 60.0);
-                  DD_Meter_Scale_Lat (DM_Base.DDM.Minutes_Lat / 60.0);
+            else
+               DD_Target.DD.Latitude :=
+                 -1.0 * DD_Meter_Scale_Lat (DM_Base.DDM.Degree_Lat) +
+                 DD_Meter_Scale_Lat (DM_Base.DDM.Minutes_Lat / 60.0);
             end if;
-         when DMS => null;
+            if DM_Base.DDM.Cardinal_Lon = East then
+               DD_Target.DD.Longitude :=
+                 DD_Meter_Scale_Lon (DM_Base.DDM.Degree_Lon) +
+                 DD_Meter_Scale_Lon (DM_Base.DDM.Minutes_Lon / 60.0);
+            else
+               DD_Target.DD.Longitude :=
+                 -1.00 * DD_Meter_Scale_Lon (DM_Base.DDM.Degree_Lon) +
+                 DD_Meter_Scale_Lon (DM_Base.DDM.Minutes_Lon / 60.0);
+            end if;
+         when DMS =>
+            null;
       end case;
 
       return DD_Target;
    end To_DD;
 
+   function Plane_Distance (Origin, Destination : Coordinate) return H is
+      Heuristic      : H;
+      A              : H;
+      DD_Origin      : constant Coordinate := To_DD (Origin);
+      DD_Destination : constant Coordinate := To_DD (Destination);
+      Earth_Radius   : constant H          := 6_371_000.0; --  M
+      Delta_Phi      : constant H          := --  Latitude difference
+        H (DD_Destination.DD.Latitude - DD_Origin.DD.Latitude);
+      Delta_Lambda   : constant H          := -- Longitude difference
+        H (DD_Destination.DD.Longitude - DD_Origin.DD.Longitude);
+
+      --  @name Hav
+      --  @return Float
+      --  @parameter Theta:Float
+      --  @variable Fraction : Float
+      --  @description Compute Haversine function.
+      function Hav (Theta : H) return Float is
+         Fraction : Float;
+      begin
+         Fraction := Float (Theta) / 2.0;
+         return Sin (Fraction)**2;
+      end Hav;
+   begin
+
+      A :=
+        H (Hav (Delta_Phi) +
+           Cos (Float (DD_Origin.DD.Latitude)) *
+             Cos (Float (DD_Destination.DD.Latitude)) * Hav (Delta_Lambda));
+
+      --  Haversine formula
+      Heuristic := Earth_Radius * H (2.0 * Arcsin (Sqrt (Float (A))));
+
+      return Heuristic;
+   end Plane_Distance;
+
 end Grl.Coordinates;

src/grl-coordinates.ads

@@ -1,5 +1,8 @@
-package Grl.Coordinates
+generic
-with SPARK_Mode => On
+   type Meta is private;
+   type H is digits <>;
+package Grl.Coordinates with
+  SPARK_Mode => On
 is
 
    --  ------------  --
@@ -34,53 +37,51 @@ is
 
    --  Meter precision DD coordinates
    type Format_DD is record
-		Latitude       : DD_Meter_Scale_Lat;
+      Latitude  : DD_Meter_Scale_Lat;
-      Longitude      : DD_Meter_Scale_Lon;
+      Longitude : DD_Meter_Scale_Lon;
-	end record;
+   end record;
 
    --  Centimeter precision DD coordinates
    type Format_DD_Fine is record
-		Latitude       : DD_Centimeter_Scale_Lat;
+      Latitude  : DD_Centimeter_Scale_Lat;
-      Longitude      : DD_Centimeter_Scale_Lon;
+      Longitude : DD_Centimeter_Scale_Lon;
-	end record;
+   end record;
 
    --  DMS
    type Format_DMS is record
-		Degree_Lat     : DM_Degree_Lat;
+      Degree_Lat   : DM_Degree_Lat;
-      Degree_Lon     : DM_Degree_Lon;
+      Degree_Lon   : DM_Degree_Lon;
-      Minutes_Lat    : DM_Minutes;
+      Minutes_Lat  : DM_Minutes;
-      Minutes_Lon    : DM_Minutes;
+      Minutes_Lon  : DM_Minutes;
-      Seconds_Lat    : DM_Seconds;
+      Seconds_Lat  : DM_Seconds;
-      Seconds_Lon    : DM_Seconds;
+      Seconds_Lon  : DM_Seconds;
-      Cardinal_Lat   : Cardinal;
+      Cardinal_Lat : Cardinal;
-      Cardinal_Lon   : Cardinal;
+      Cardinal_Lon : Cardinal;
-	end record
+   end record with
-   with Dynamic_Predicate =>
+     Dynamic_Predicate =>
       Format_DMS.Cardinal_Lat in North | South
-      and then
+      and then Format_DMS.Cardinal_Lon in East | West;
-      Format_DMS.Cardinal_Lon in East | West;
 
    --  DDM
    type Format_DDM is record
-		Degree_Lat : DM_Degree_Lat;
+      Degree_Lat   : DM_Degree_Lat;
-      Degree_Lon : DM_Degree_Lon;
+      Degree_Lon   : DM_Degree_Lon;
-      Minutes_Lat : DDM_Minutes;
+      Minutes_Lat  : DDM_Minutes;
-      Minutes_Lon : DDM_Minutes;
+      Minutes_Lon  : DDM_Minutes;
       Cardinal_Lat : Cardinal;
       Cardinal_Lon : Cardinal;
-	end record
+   end record with
-   with Dynamic_Predicate =>
+     Dynamic_Predicate =>
       Format_DDM.Cardinal_Lat in North | South
-      and then
+      and then Format_DDM.Cardinal_Lon in East | West;
-      Format_DDM.Cardinal_Lon in East | West;
 
-   --  --------------------------  --
+     --  --------------------------  --
-   --  Coordinate Type Definition  --
+     --  Coordinate Type Definition  --
-   --  --------------------------  --
+     --  --------------------------  --
 
    type Format is (Relative, DD, DD_Fine, DMS, DDM);
    type Coordinate (Form : Format := Relative) is record
-		case Form is
+      case Form is
          when Relative =>
             null;
          when DD =>
@@ -92,7 +93,16 @@ is
          when DDM =>
             DDM : Format_DDM;
       end case;
-	end record;
+   end record;
+
+   --  ------------------------  --
+   --  Location Type Definition  --
+   --  ------------------------  --
+   type Location is record
+      Where     : Coordinate;
+      Heuristic : H;
+      Data      : Meta;
+   end record;
 
    --  ----------------------------  --
    --  Converter / helper functions  --
@@ -101,12 +111,19 @@ is
    --  Converter with DD target
    --  @name      To_DD
    --  @return    Coordinate
- 	--  @parameter DM_Base  :  Coordinate
+   --  @parameter DM_Base  :  Coordinate
-	--  @description Take any coordinate and return a DD formatted coordinate.
+   --  @description Take any coordinate and return a DD formatted coordinate.
-   function To_DD (DM_Base : Coordinate) return Coordinate
+   function To_DD (DM_Base : Coordinate) return Coordinate with
-      with Pre =>
+     Pre =>
-         (DM_Base.Form = DD) or else
+      (DM_Base.Form = DD) or else (DM_Base.Form = DMS)
-         (DM_Base.Form = DMS) or else
+      or else (DM_Base.Form = DDM);
-         (DM_Base.Form = DDM);
+
+   --  @name Plane_Distance
+   --  @return H
+   --  @parameter Origin:Coordinate
+   --  @parameter Destination:Coordinate
+   --  @variable Heuristic : H
+   --  @description Calculate heuristic between coordinates.
+   function Plane_Distance (Origin, Destination : Coordinate) return H;
 
 end Grl.Coordinates;

src/grl-default.ads

@@ -0,0 +1,3 @@
+with Grl.Coordinates;
+
+package Grl.Default is new Grl.Coordinates (Meta => Natural, H => Float);

src/grl.ads

@@ -1,3 +1,2 @@
 package Grl is
-
 end Grl;